[STATEMENT]
lemma cmbi:"m O b^-1 \<subseteq> b^-1 \<union> m^-1 \<union> s^-1 \<union> ov^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m O b\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cbmi
[PROOF STATE]
proof (prove)
using this:
b O m\<inverse> \<subseteq> b \<union> m \<union> ov \<union> s \<union> d

goal (1 subgoal):
 1. m O b\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma covmi:"ov O m^-1 \<subseteq> ov^-1 \<union> d^-1 \<union> s^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov O m\<inverse> \<subseteq> ov\<inverse> \<union> d\<inverse> \<union> s\<inverse>
[PROOF STEP]
using  cmovi
[PROOF STATE]
proof (prove)
using this:
m O ov\<inverse> \<subseteq> s \<union> ov \<union> d

goal (1 subgoal):
 1. ov O m\<inverse> \<subseteq> ov\<inverse> \<union> d\<inverse> \<union> s\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma covbi:"ov O b^-1 \<subseteq> b^-1 \<union> m^-1 \<union> s^-1 \<union> ov^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov O b\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cbovi
[PROOF STATE]
proof (prove)
using this:
b O ov\<inverse> \<subseteq> b \<union> m \<union> ov \<union> s \<union> d

goal (1 subgoal):
 1. ov O b\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cfiovi:"f^-1 O ov^-1 \<subseteq> ov^-1 \<union> s^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<inverse> O ov\<inverse> \<subseteq> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
using covf
[PROOF STATE]
proof (prove)
using this:
ov O f \<subseteq> s \<union> ov \<union> d

goal (1 subgoal):
 1. f\<inverse> O ov\<inverse> \<subseteq> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cfimi:"(f^-1 O m^-1) \<subseteq> s^-1 \<union> ov^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<inverse> O m\<inverse> \<subseteq> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cmf
[PROOF STATE]
proof (prove)
using this:
m O f \<subseteq> s \<union> ov \<union> d

goal (1 subgoal):
 1. f\<inverse> O m\<inverse> \<subseteq> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cfibi:"f^-1 O b^-1 \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> s^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<inverse> O b\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cbf
[PROOF STATE]
proof (prove)
using this:
b O f \<subseteq> b \<union> m \<union> ov \<union> s \<union> d

goal (1 subgoal):
 1. f\<inverse> O b\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cdif:"d^-1 O f \<subseteq> ov^-1 \<union> s^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<inverse> O f \<subseteq> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cfid
[PROOF STATE]
proof (prove)
using this:
f\<inverse> O d \<subseteq> s \<union> ov \<union> d

goal (1 subgoal):
 1. d\<inverse> O f \<subseteq> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cdiovi:"d^-1 O ov ^-1 \<subseteq> ov^-1 \<union> s^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<inverse> O ov\<inverse> \<subseteq> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
using covd
[PROOF STATE]
proof (prove)
using this:
ov O d \<subseteq> s \<union> ov \<union> d

goal (1 subgoal):
 1. d\<inverse> O ov\<inverse> \<subseteq> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cdimi:"d^-1 O m^-1 \<subseteq> s^-1 \<union> ov^-1 \<union> d^-1 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<inverse> O m\<inverse> \<subseteq> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cmd
[PROOF STATE]
proof (prove)
using this:
m O d \<subseteq> s \<union> ov \<union> d

goal (1 subgoal):
 1. d\<inverse> O m\<inverse> \<subseteq> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cdibi:"d^-1 O b^-1 \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> s^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<inverse> O b\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cbd
[PROOF STATE]
proof (prove)
using this:
b O d \<subseteq> b \<union> m \<union> ov \<union> s \<union> d

goal (1 subgoal):
 1. d\<inverse> O b\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma csd:"s O d \<subseteq> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s O d \<subseteq> d
[PROOF STEP]
using cdisi
[PROOF STATE]
proof (prove)
using this:
d\<inverse> O s\<inverse> \<subseteq> d\<inverse>

goal (1 subgoal):
 1. s O d \<subseteq> d
[PROOF STEP]
by auto


[STATEMENT]
lemma csf:"s O f \<subseteq> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s O f \<subseteq> d
[PROOF STEP]
using cfisi
[PROOF STATE]
proof (prove)
using this:
f\<inverse> O s\<inverse> \<subseteq> d\<inverse>

goal (1 subgoal):
 1. s O f \<subseteq> d
[PROOF STEP]
by auto


[STATEMENT]
lemma csovi:"s O ov^-1 \<subseteq> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s O ov\<inverse> \<subseteq> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using covsi
[PROOF STATE]
proof (prove)
using this:
ov O s\<inverse> \<subseteq> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. s O ov\<inverse> \<subseteq> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma csbi:"s O b^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cbsi
[PROOF STATE]
proof (prove)
using this:
b O s\<inverse> \<subseteq> b

goal (1 subgoal):
 1. s O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma csisi:"s^-1 O s^-1 \<subseteq> s^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<inverse> O s\<inverse> \<subseteq> s\<inverse>
[PROOF STEP]
using css
[PROOF STATE]
proof (prove)
using this:
s O s \<subseteq> s

goal (1 subgoal):
 1. s\<inverse> O s\<inverse> \<subseteq> s\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma csid:"s^-1 O d \<subseteq> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<inverse> O d \<subseteq> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using cdis
[PROOF STATE]
proof (prove)
using this:
d\<inverse> O s \<subseteq> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. s\<inverse> O d \<subseteq> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma csif:"s^-1 O f \<subseteq> ov^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<inverse> O f \<subseteq> ov\<inverse>
[PROOF STEP]
using cfis
[PROOF STATE]
proof (prove)
using this:
f\<inverse> O s \<subseteq> ov

goal (1 subgoal):
 1. s\<inverse> O f \<subseteq> ov\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma csiovi:"s^-1 O ov^-1 \<subseteq> ov^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<inverse> O ov\<inverse> \<subseteq> ov\<inverse>
[PROOF STEP]
using covs
[PROOF STATE]
proof (prove)
using this:
ov O s \<subseteq> ov

goal (1 subgoal):
 1. s\<inverse> O ov\<inverse> \<subseteq> ov\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma csimi:"s^-1 O m^-1 \<subseteq> m^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<inverse> O m\<inverse> \<subseteq> m\<inverse>
[PROOF STEP]
using cms
[PROOF STATE]
proof (prove)
using this:
m O s \<subseteq> m

goal (1 subgoal):
 1. s\<inverse> O m\<inverse> \<subseteq> m\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma csibi:"s^-1 O b^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s\<inverse> O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cbs
[PROOF STATE]
proof (prove)
using this:
b O s \<subseteq> b

goal (1 subgoal):
 1. s\<inverse> O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cds:"d O s \<subseteq> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O s \<subseteq> d
[PROOF STEP]
using csidi
[PROOF STATE]
proof (prove)
using this:
s\<inverse> O d\<inverse> \<subseteq> d\<inverse>

goal (1 subgoal):
 1. d O s \<subseteq> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cdd:"d O d \<subseteq> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O d \<subseteq> d
[PROOF STEP]
using cdidi
[PROOF STATE]
proof (prove)
using this:
d\<inverse> O d\<inverse> \<subseteq> d\<inverse>

goal (1 subgoal):
 1. d O d \<subseteq> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cdf:"d O f \<subseteq> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O f \<subseteq> d
[PROOF STEP]
using cfidi
[PROOF STATE]
proof (prove)
using this:
f\<inverse> O d\<inverse> \<subseteq> d\<inverse>

goal (1 subgoal):
 1. d O f \<subseteq> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cdovi:"d O ov^-1 \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O ov\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using covdi
[PROOF STATE]
proof (prove)
using this:
ov O d\<inverse> \<subseteq> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. d O ov\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cdmi:"d O m^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cmdi
[PROOF STATE]
proof (prove)
using this:
m O d\<inverse> \<subseteq> b

goal (1 subgoal):
 1. d O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cdbi:"d O b^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cbdi
[PROOF STATE]
proof (prove)
using this:
b O d\<inverse> \<subseteq> b

goal (1 subgoal):
 1. d O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cfdi:"f O d^-1 \<subseteq>  b^-1 \<union> m^-1 \<union> ov^-1 \<union> s^-1 \<union> d^-1 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O d\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cdfi
[PROOF STATE]
proof (prove)
using this:
d O f\<inverse> \<subseteq> b \<union> m \<union> ov \<union> s \<union> d

goal (1 subgoal):
 1. f O d\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cfs:"f O s \<subseteq> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O s \<subseteq> d
[PROOF STEP]
using csifi
[PROOF STATE]
proof (prove)
using this:
s\<inverse> O f\<inverse> \<subseteq> d\<inverse>

goal (1 subgoal):
 1. f O s \<subseteq> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cfsi:"f O s^-1 \<subseteq> b ^-1 \<union> m^-1 \<union> ov ^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O s\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse>
[PROOF STEP]
using csfi
[PROOF STATE]
proof (prove)
using this:
s O f\<inverse> \<subseteq> b \<union> m \<union> ov

goal (1 subgoal):
 1. f O s\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cfd:"f O d \<subseteq> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O d \<subseteq> d
[PROOF STEP]
using cdifi
[PROOF STATE]
proof (prove)
using this:
d\<inverse> O f\<inverse> \<subseteq> d\<inverse>

goal (1 subgoal):
 1. f O d \<subseteq> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cff:"f O f \<subseteq> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O f \<subseteq> f
[PROOF STEP]
using cfifi
[PROOF STATE]
proof (prove)
using this:
f\<inverse> O f\<inverse> \<subseteq> f\<inverse>

goal (1 subgoal):
 1. f O f \<subseteq> f
[PROOF STEP]
by auto


[STATEMENT]
lemma cfovi:"f O ov^-1 \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O ov\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse>
[PROOF STEP]
using covfi
[PROOF STATE]
proof (prove)
using this:
ov O f\<inverse> \<subseteq> b \<union> m \<union> ov

goal (1 subgoal):
 1. f O ov\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cfmi:"f O m^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cmfi
[PROOF STATE]
proof (prove)
using this:
m O f\<inverse> \<subseteq> b

goal (1 subgoal):
 1. f O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cfbi:"f O b^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cbfi
[PROOF STATE]
proof (prove)
using this:
b O f\<inverse> \<subseteq> b

goal (1 subgoal):
 1. f O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma covifi:"ov^-1 O f^-1 \<subseteq> ov^-1 \<union> s^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O f\<inverse> \<subseteq> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cfov
[PROOF STATE]
proof (prove)
using this:
f O ov \<subseteq> ov \<union> s \<union> d

goal (1 subgoal):
 1. ov\<inverse> O f\<inverse> \<subseteq> ov\<inverse> \<union> s\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma covidi:"ov^-1 O d^-1 \<subseteq> b^-1 \<union> m^-1 \<union> s^-1 \<union> ov^-1 \<union> d^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O d\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
using cdov
[PROOF STATE]
proof (prove)
using this:
d O ov \<subseteq> b \<union> m \<union> ov \<union> s \<union> d

goal (1 subgoal):
 1. ov\<inverse> O d\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> s\<inverse> \<union> ov\<inverse> \<union> d\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma covis:"ov^-1 O s \<subseteq> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O s \<subseteq> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using csiov
[PROOF STATE]
proof (prove)
using this:
s\<inverse> O ov \<subseteq> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. ov\<inverse> O s \<subseteq> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma covisi:"ov^-1 O s^-1 \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O s\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse>
[PROOF STEP]
using csov
[PROOF STATE]
proof (prove)
using this:
s O ov \<subseteq> b \<union> m \<union> ov

goal (1 subgoal):
 1. ov\<inverse> O s\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma covid:"ov^-1 O d \<subseteq> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O d \<subseteq> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using cdiov
[PROOF STATE]
proof (prove)
using this:
d\<inverse> O ov \<subseteq> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. ov\<inverse> O d \<subseteq> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma covif:"ov^-1 O f \<subseteq> ov^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O f \<subseteq> ov\<inverse>
[PROOF STEP]
using cfiov
[PROOF STATE]
proof (prove)
using this:
f\<inverse> O ov \<subseteq> ov

goal (1 subgoal):
 1. ov\<inverse> O f \<subseteq> ov\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma coviovi:"ov^-1 O ov^-1 \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O ov\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse>
[PROOF STEP]
using covov
[PROOF STATE]
proof (prove)
using this:
ov O ov \<subseteq> b \<union> m \<union> ov

goal (1 subgoal):
 1. ov\<inverse> O ov\<inverse> \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma covimi:"ov^-1 O m^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cmov
[PROOF STATE]
proof (prove)
using this:
m O ov \<subseteq> b

goal (1 subgoal):
 1. ov\<inverse> O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma covibi:"ov^-1 O b^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ov\<inverse> O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cbov
[PROOF STATE]
proof (prove)
using this:
b O ov \<subseteq> b

goal (1 subgoal):
 1. ov\<inverse> O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cmiov:"m^-1 O ov \<subseteq> ov^-1 \<union> d \<union> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O ov \<subseteq> ov\<inverse> \<union> d \<union> f
[PROOF STEP]
using covim
[PROOF STATE]
proof (prove)
using this:
ov\<inverse> O m \<subseteq> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. m\<inverse> O ov \<subseteq> ov\<inverse> \<union> d \<union> f
[PROOF STEP]
by auto


[STATEMENT]
lemma cmifi:"m^-1 O f^-1 \<subseteq> m^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O f\<inverse> \<subseteq> m\<inverse>
[PROOF STEP]
using cfm
[PROOF STATE]
proof (prove)
using this:
f O m \<subseteq> m

goal (1 subgoal):
 1. m\<inverse> O f\<inverse> \<subseteq> m\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cmidi:"m^-1 O d^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O d\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cdm
[PROOF STATE]
proof (prove)
using this:
d O m \<subseteq> b

goal (1 subgoal):
 1. m\<inverse> O d\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cmis:"m^-1 O s \<subseteq> ov^-1 \<union> d \<union> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O s \<subseteq> ov\<inverse> \<union> d \<union> f
[PROOF STEP]
using csim
[PROOF STATE]
proof (prove)
using this:
s\<inverse> O m \<subseteq> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. m\<inverse> O s \<subseteq> ov\<inverse> \<union> d \<union> f
[PROOF STEP]
by auto


[STATEMENT]
lemma cmisi:"m^-1 O s^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O s\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using csm
[PROOF STATE]
proof (prove)
using this:
s O m \<subseteq> b

goal (1 subgoal):
 1. m\<inverse> O s\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cmid:"m^-1 O d \<subseteq> ov^-1 \<union> d \<union> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O d \<subseteq> ov\<inverse> \<union> d \<union> f
[PROOF STEP]
using cdim
[PROOF STATE]
proof (prove)
using this:
d\<inverse> O m \<subseteq> ov \<union> d\<inverse> \<union> f\<inverse>

goal (1 subgoal):
 1. m\<inverse> O d \<subseteq> ov\<inverse> \<union> d \<union> f
[PROOF STEP]
by auto


[STATEMENT]
lemma cmif:"m^-1 O f \<subseteq> m^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O f \<subseteq> m\<inverse>
[PROOF STEP]
using cfim
[PROOF STATE]
proof (prove)
using this:
f\<inverse> O m \<subseteq> m

goal (1 subgoal):
 1. m\<inverse> O f \<subseteq> m\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cmiovi:"m^-1 O ov^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O ov\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using covm
[PROOF STATE]
proof (prove)
using this:
ov O m \<subseteq> b

goal (1 subgoal):
 1. m\<inverse> O ov\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cmimi:"m^-1 O m^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cmm
[PROOF STATE]
proof (prove)
using this:
m O m \<subseteq> b

goal (1 subgoal):
 1. m\<inverse> O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cmibi:"m^-1 O b^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m\<inverse> O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cbm
[PROOF STATE]
proof (prove)
using this:
b O m \<subseteq> b

goal (1 subgoal):
 1. m\<inverse> O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cbim:"b^-1 O m \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O m \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using cmib
[PROOF STATE]
proof (prove)
using this:
m\<inverse> O b \<subseteq> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. b\<inverse> O m \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cbiov:"b^-1 O ov \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O ov \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using covib
[PROOF STATE]
proof (prove)
using this:
ov\<inverse> O b \<subseteq> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. b\<inverse> O ov \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cbifi:"b^-1 O f^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O f\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cfb
[PROOF STATE]
proof (prove)
using this:
f O b \<subseteq> b

goal (1 subgoal):
 1. b\<inverse> O f\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cbidi:"b^-1 O d^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O d\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cdb
[PROOF STATE]
proof (prove)
using this:
d O b \<subseteq> b

goal (1 subgoal):
 1. b\<inverse> O d\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cbis:"b^-1 O s \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O s \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using csib
[PROOF STATE]
proof (prove)
using this:
s\<inverse> O b \<subseteq> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. b\<inverse> O s \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cbisi:"b^-1 O s^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O s\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using csb
[PROOF STATE]
proof (prove)
using this:
s O b \<subseteq> b

goal (1 subgoal):
 1. b\<inverse> O s\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cbid:"b^-1 O d  \<subseteq> b^-1 \<union> m^-1 \<union> ov^-1 \<union> f \<union> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O d \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
using cdib
[PROOF STATE]
proof (prove)
using this:
d\<inverse> O b \<subseteq> b \<union> m \<union> ov \<union> f\<inverse> \<union> d\<inverse>

goal (1 subgoal):
 1. b\<inverse> O d \<subseteq> b\<inverse> \<union> m\<inverse> \<union> ov\<inverse> \<union> f \<union> d
[PROOF STEP]
by auto


[STATEMENT]
lemma cbif:"b^-1 O f \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O f \<subseteq> b\<inverse>
[PROOF STEP]
using cfib
[PROOF STATE]
proof (prove)
using this:
f\<inverse> O b \<subseteq> b

goal (1 subgoal):
 1. b\<inverse> O f \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cbiovi:"b^-1 O ov^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O ov\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using covb
[PROOF STATE]
proof (prove)
using this:
ov O b \<subseteq> b

goal (1 subgoal):
 1. b\<inverse> O ov\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cbimi:"b^-1 O m^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cmb
[PROOF STATE]
proof (prove)
using this:
m O b \<subseteq> b

goal (1 subgoal):
 1. b\<inverse> O m\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma cbibi:"b^-1 O b^-1 \<subseteq> b^-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b\<inverse> O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
using cbb
[PROOF STATE]
proof (prove)
using this:
b O b \<subseteq> b

goal (1 subgoal):
 1. b\<inverse> O b\<inverse> \<subseteq> b\<inverse>
[PROOF STEP]
by auto


[STATEMENT]
lemma mgp_pre_iso_test: "minGraphProps g \<Longrightarrow> pre_iso_test(fgraph g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minGraphProps g \<Longrightarrow> pre_iso_test (fgraph g)
[PROOF STEP]
apply(simp add:pre_iso_test_def fgraph_def image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minGraphProps g \<Longrightarrow> (\<forall>x\<in>\<F> g. [] \<noteq> vertices x) \<and> (\<forall>x. (\<exists>xa\<in>\<F> g. x = vertices xa) \<longrightarrow> distinct x) \<and> distinct (map (rotate_min \<circ> vertices) (faces g))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. minGraphProps g \<Longrightarrow> \<forall>x\<in>\<F> g. [] \<noteq> vertices x
 2. minGraphProps g \<Longrightarrow> (\<forall>x. (\<exists>xa\<in>\<F> g. x = vertices xa) \<longrightarrow> distinct x) \<and> distinct (map (rotate_min \<circ> vertices) (faces g))
[PROOF STEP]
apply(blast dest: mgp_vertices_nonempty[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minGraphProps g \<Longrightarrow> (\<forall>x. (\<exists>xa\<in>\<F> g. x = vertices xa) \<longrightarrow> distinct x) \<and> distinct (map (rotate_min \<circ> vertices) (faces g))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. minGraphProps g \<Longrightarrow> \<forall>x. (\<exists>xa\<in>\<F> g. x = vertices xa) \<longrightarrow> distinct x
 2. minGraphProps g \<Longrightarrow> distinct (map (rotate_min \<circ> vertices) (faces g))
[PROOF STEP]
apply(blast intro:minGraphProps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minGraphProps g \<Longrightarrow> distinct (map (rotate_min \<circ> vertices) (faces g))
[PROOF STEP]
apply(drule minGraphProps11)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (normFaces (faces g)) \<Longrightarrow> distinct (map (rotate_min \<circ> vertices) (faces g))
[PROOF STEP]
apply(simp add:normFaces_def normFace_def verticesFrom_def minVertex_def
               rotate_min_def o_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma trie_all_eq_set_of_trie:
  "invar_trie t \<Longrightarrow> all_trie (list_all P) t = (\<forall>v \<in> set_tries t. P v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar_trie t \<Longrightarrow> all_trie (list_all P) t = (\<forall>v\<in>set_tries t. P v)
[PROOF STEP]
by(simp add: all_trie_eq_ran set_tries_eq_ran)


[STATEMENT]
lemma samet_imp_iso_seteq:
assumes pre1: "\<And>gs g. gsopt = Some gs \<Longrightarrow> g \<in> set_tries gs \<Longrightarrow> pre_iso_test g"
and pre2: "\<And>g. g \<in> set arch \<Longrightarrow> pre_iso_test g"
and inv: "\<And>gs. gsopt = Some gs \<Longrightarrow> invar_trie gs"
and same: "samet gsopt arch"
shows "\<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch
[PROOF STEP]
obtain gs where [simp]: "gsopt = Some gs" and test1: "\<And>g. g \<in> set_tries gs \<Longrightarrow>
    \<exists>h \<in> set arch. iso_test g h" and test2: "\<And>g. g \<in> set arch \<Longrightarrow>
    \<exists>h \<in> set_tries gs. iso_test g h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>gs. \<lbrakk>gsopt = Some gs; \<And>g. g \<in> set_tries gs \<Longrightarrow> \<exists>h\<in>set arch. iso_test g h; \<And>g. g \<in> set arch \<Longrightarrow> \<exists>h\<in>set_tries gs. iso_test g h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using same inv
[PROOF STATE]
proof (prove)
using this:
samet gsopt arch
gsopt = Some ?gs \<Longrightarrow> invar_trie ?gs

goal (1 subgoal):
 1. (\<And>gs. \<lbrakk>gsopt = Some gs; \<And>g. g \<in> set_tries gs \<Longrightarrow> \<exists>h\<in>set arch. iso_test g h; \<And>g. g \<in> set arch \<Longrightarrow> \<exists>h\<in>set_tries gs. iso_test g h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force simp: samet_def trie_all_eq_set_of_trie invar_of_list all_tries_def
      split:option.splits
      dest: in_set_lookup_of_listD in_set_lookup_set_triesD)
[PROOF STATE]
proof (state)
this:
gsopt = Some gs
?g \<in> set_tries gs \<Longrightarrow> \<exists>h\<in>set arch. iso_test ?g h
?g \<in> set arch \<Longrightarrow> \<exists>h\<in>set_tries gs. iso_test ?g h

goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch
[PROOF STEP]
have "set_tries gs \<subseteq>\<^sub>\<simeq> set arch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_tries gs \<subseteq>\<^sub>\<simeq> set arch
[PROOF STEP]
proof (auto simp:qle_gr.defs)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_tries gs \<Longrightarrow> \<exists>y\<in>set arch. x \<simeq> y
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_tries gs \<Longrightarrow> \<exists>y\<in>set arch. x \<simeq> y
[PROOF STEP]
assume g: "g \<in> set_tries gs"
[PROOF STATE]
proof (state)
this:
g \<in> set_tries gs

goal (1 subgoal):
 1. \<And>x. x \<in> set_tries gs \<Longrightarrow> \<exists>y\<in>set arch. x \<simeq> y
[PROOF STEP]
obtain h where h: "h \<in> set arch" and test: "iso_test g h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> set arch; iso_test g h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using test1[OF g]
[PROOF STATE]
proof (prove)
using this:
\<exists>h\<in>set arch. iso_test g h

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> set arch; iso_test g h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h \<in> set arch
iso_test g h

goal (1 subgoal):
 1. \<And>x. x \<in> set_tries gs \<Longrightarrow> \<exists>y\<in>set arch. x \<simeq> y
[PROOF STEP]
thus "\<exists>h\<in>set arch. g \<simeq> h"
[PROOF STATE]
proof (prove)
using this:
h \<in> set arch
iso_test g h

goal (1 subgoal):
 1. \<exists>h\<in>set arch. g \<simeq> h
[PROOF STEP]
using h pre1[OF _ g] pre2[OF h]
[PROOF STATE]
proof (prove)
using this:
h \<in> set arch
iso_test g h
h \<in> set arch
gsopt = Some gs \<Longrightarrow> pre_iso_test g
pre_iso_test h

goal (1 subgoal):
 1. \<exists>h\<in>set arch. g \<simeq> h
[PROOF STEP]
by (auto simp:iso_test_correct)
[PROOF STATE]
proof (state)
this:
\<exists>h\<in>set arch. g \<simeq> h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_tries gs \<subseteq>\<^sub>\<simeq> set arch

goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_tries gs \<subseteq>\<^sub>\<simeq> set arch

goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch
[PROOF STEP]
have "set arch \<subseteq>\<^sub>\<simeq> set_tries gs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set arch \<subseteq>\<^sub>\<simeq> set_tries gs
[PROOF STEP]
proof (auto simp:qle_gr.defs)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set arch \<Longrightarrow> \<exists>y\<in>set_tries gs. x \<simeq> y
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set arch \<Longrightarrow> \<exists>y\<in>set_tries gs. x \<simeq> y
[PROOF STEP]
assume g: "g \<in> set arch"
[PROOF STATE]
proof (state)
this:
g \<in> set arch

goal (1 subgoal):
 1. \<And>x. x \<in> set arch \<Longrightarrow> \<exists>y\<in>set_tries gs. x \<simeq> y
[PROOF STEP]
obtain h where h: "h \<in> set_tries gs" and test: "iso_test g h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> set_tries gs; iso_test g h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using test2[OF g]
[PROOF STATE]
proof (prove)
using this:
\<exists>h\<in>set_tries gs. iso_test g h

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> set_tries gs; iso_test g h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h \<in> set_tries gs
iso_test g h

goal (1 subgoal):
 1. \<And>x. x \<in> set arch \<Longrightarrow> \<exists>y\<in>set_tries gs. x \<simeq> y
[PROOF STEP]
thus "\<exists>h \<in> set_tries gs. g \<simeq> h"
[PROOF STATE]
proof (prove)
using this:
h \<in> set_tries gs
iso_test g h

goal (1 subgoal):
 1. \<exists>h\<in>set_tries gs. g \<simeq> h
[PROOF STEP]
using h pre1[OF _ h] pre2[OF g]
[PROOF STATE]
proof (prove)
using this:
h \<in> set_tries gs
iso_test g h
h \<in> set_tries gs
gsopt = Some gs \<Longrightarrow> pre_iso_test h
pre_iso_test g

goal (1 subgoal):
 1. \<exists>h\<in>set_tries gs. g \<simeq> h
[PROOF STEP]
by (auto simp:iso_test_correct)
[PROOF STATE]
proof (state)
this:
\<exists>h\<in>set_tries gs. g \<simeq> h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set arch \<subseteq>\<^sub>\<simeq> set_tries gs

goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set_tries gs \<subseteq>\<^sub>\<simeq> set arch
set arch \<subseteq>\<^sub>\<simeq> set_tries gs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set_tries gs \<subseteq>\<^sub>\<simeq> set arch
set arch \<subseteq>\<^sub>\<simeq> set_tries gs

goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch
[PROOF STEP]
by (auto simp: qle_gr.seteq_qle_def)
[PROOF STATE]
proof (state)
this:
\<exists>gs. gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set arch

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma samet_imp_iso_subseteq:
assumes pre1: "\<And>gs g. gsopt = Some gs \<Longrightarrow> g \<in> set_tries gs \<Longrightarrow> pre_iso_test g"
and pre2: "\<And>g. g \<in> set arch \<Longrightarrow> pre_iso_test g"
and inv: "\<And>gs. gsopt = Some gs \<Longrightarrow> invar_trie gs"
and same: "samet gsopt arch"
shows "\<exists>gs. gsopt = Some gs \<and> set_tries gs \<subseteq>\<^sub>\<simeq> set arch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs \<subseteq>\<^sub>\<simeq> set arch
[PROOF STEP]
using qle_gr.seteq_qle_def assms samet_imp_iso_seteq
[PROOF STATE]
proof (prove)
using this:
?M =\<^sub>\<simeq> ?N \<equiv> ?M \<subseteq>\<^sub>\<simeq> ?N \<and> ?N \<subseteq>\<^sub>\<simeq> ?M
\<lbrakk>gsopt = Some ?gs; ?g \<in> set_tries ?gs\<rbrakk> \<Longrightarrow> pre_iso_test ?g
?g \<in> set arch \<Longrightarrow> pre_iso_test ?g
gsopt = Some ?gs \<Longrightarrow> invar_trie ?gs
samet gsopt arch
\<lbrakk>\<And>gs g. \<lbrakk>?gsopt = Some gs; g \<in> set_tries gs\<rbrakk> \<Longrightarrow> pre_iso_test g; \<And>g. g \<in> set ?arch \<Longrightarrow> pre_iso_test g; \<And>gs. ?gsopt = Some gs \<Longrightarrow> invar_trie gs; samet ?gsopt ?arch\<rbrakk> \<Longrightarrow> \<exists>gs. ?gsopt = Some gs \<and> set_tries gs =\<^sub>\<simeq> set ?arch

goal (1 subgoal):
 1. \<exists>gs. gsopt = Some gs \<and> set_tries gs \<subseteq>\<^sub>\<simeq> set arch
[PROOF STEP]
by metis


[STATEMENT]
lemma TameEnum_tameEnumFilter:
  "tameEnumFilter p = Some t \<Longrightarrow>  set_tries t  =\<^sub>\<simeq> fgraph ` TameEnum\<^bsub>p\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tameEnumFilter p = Some t \<Longrightarrow> set_tries t =\<^sub>\<simeq> fgraph ` TameEnum\<^bsub>p\<^esub>
[PROOF STEP]
apply(auto simp: tameEnumFilter_def TameEnumP_def enum_filter_finals_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. worklist_tree_coll_trie next_tame\<^bsub>p\<^esub> final fgraph [Seed\<^bsub>p\<^esub>] = Some t \<Longrightarrow> set_tries t =\<^sub>\<simeq> fgraph ` {g. Seed\<^bsub>p\<^esub> [next_tame\<^bsub>p\<^esub>]\<rightarrow>* g \<and> final g}
[PROOF STEP]
apply(drule set_mod_trie.worklist_tree_coll_equiv[OF _ inv_inv_next_tame])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>set [Seed\<^bsub>p\<^esub>]. Invariants.inv x
 2. \<And>x. Invariants.inv x \<Longrightarrow> pre_iso_test (fgraph x)
 3. map.set_of t =\<^sub>\<simeq> fgraph ` {x \<in> (Rel next_tame\<^bsub>p\<^esub>)\<^sup>* `` set [Seed\<^bsub>p\<^esub>]. final x} \<Longrightarrow> set_tries t =\<^sub>\<simeq> fgraph ` {g. Seed\<^bsub>p\<^esub> [next_tame\<^bsub>p\<^esub>]\<rightarrow>* g \<and> final g}
[PROOF STEP]
apply (auto simp: set_of_conv inv_Seed mgp_pre_iso_test RTranCl_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tameEnumFilter_subseteq_TameEnum:
  "tameEnumFilter p = Some t \<Longrightarrow> set_tries t \<subseteq> fgraph ` TameEnum\<^bsub>p\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tameEnumFilter p = Some t \<Longrightarrow> set_tries t \<subseteq> fgraph ` TameEnum\<^bsub>p\<^esub>
[PROOF STEP]
by(auto simp add:tameEnumFilter_def TameEnumP_def enum_filter_finals_def
     set_of_conv inv_Seed mgp_pre_iso_test RTranCl_conv
     dest!: set_mod_trie.worklist_tree_coll_subseteq[OF _ inv_inv_next_tame])


[STATEMENT]
lemma inv_tries_tameEnumFilter:
  "tameEnumFilter p = Some t \<Longrightarrow> invar_trie t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tameEnumFilter p = Some t \<Longrightarrow> invar_trie t
[PROOF STEP]
unfolding tameEnumFilter_def enum_filter_finals_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. worklist_tree_coll_trie next_tame\<^bsub>p\<^esub> final fgraph [Seed\<^bsub>p\<^esub>] = Some t \<Longrightarrow> invar_trie t
[PROOF STEP]
by(erule set_mod_trie.worklist_tree_coll_inv)


[STATEMENT]
theorem combine_evals_filter:
 "\<forall>g \<in> set arch. pre_iso_test g \<Longrightarrow> samet (tameEnumFilter p) arch
  \<Longrightarrow> fgraph ` TameEnum\<^bsub>p\<^esub> \<subseteq>\<^sub>\<simeq> set arch"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>g\<in>set arch. pre_iso_test g; samet (tameEnumFilter p) arch\<rbrakk> \<Longrightarrow> fgraph ` TameEnum\<^bsub>p\<^esub> \<subseteq>\<^sub>\<simeq> set arch
[PROOF STEP]
apply(subgoal_tac "\<exists>t. tameEnumFilter p = Some t \<and> set_tries t \<subseteq>\<^sub>\<simeq> set arch")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>g\<in>set arch. pre_iso_test g; samet (tameEnumFilter p) arch; \<exists>t. tameEnumFilter p = Some t \<and> set_tries t \<subseteq>\<^sub>\<simeq> set arch\<rbrakk> \<Longrightarrow> fgraph ` TameEnum\<^bsub>p\<^esub> \<subseteq>\<^sub>\<simeq> set arch
 2. \<lbrakk>\<forall>g\<in>set arch. pre_iso_test g; samet (tameEnumFilter p) arch\<rbrakk> \<Longrightarrow> \<exists>t. tameEnumFilter p = Some t \<and> set_tries t \<subseteq>\<^sub>\<simeq> set arch
[PROOF STEP]
apply(metis TameEnum_tameEnumFilter qle_gr.seteq_qle_def qle_gr.subseteq_qle_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>g\<in>set arch. pre_iso_test g; samet (tameEnumFilter p) arch\<rbrakk> \<Longrightarrow> \<exists>t. tameEnumFilter p = Some t \<and> set_tries t \<subseteq>\<^sub>\<simeq> set arch
[PROOF STEP]
apply(fastforce intro!: samet_imp_iso_subseteq
  dest: inv_tries_tameEnumFilter tameEnumFilter_subseteq_TameEnum mgp_TameEnum mgp_pre_iso_test)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma refinesI[intro]:
  "\<lbrakk> \<And>P. sound P \<Longrightarrow> wp prog P \<tturnstile> wp prog' P \<rbrakk> \<Longrightarrow> prog \<sqsubseteq> prog'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. sound P \<Longrightarrow> wp prog P \<tturnstile> wp prog' P) \<Longrightarrow> prog \<sqsubseteq> prog'
[PROOF STEP]
unfolding refines_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. sound P \<Longrightarrow> wp prog P \<tturnstile> wp prog' P) \<Longrightarrow> \<forall>P. sound P \<longrightarrow> wp prog P \<tturnstile> wp prog' P
[PROOF STEP]
by(simp)


[STATEMENT]
lemma refinesD[dest]:
  "\<lbrakk> prog \<sqsubseteq> prog'; sound P \<rbrakk> \<Longrightarrow> wp prog P \<tturnstile> wp prog' P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prog \<sqsubseteq> prog'; sound P\<rbrakk> \<Longrightarrow> wp prog P \<tturnstile> wp prog' P
[PROOF STEP]
unfolding refines_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>P. sound P \<longrightarrow> wp prog P \<tturnstile> wp prog' P; sound P\<rbrakk> \<Longrightarrow> wp prog P \<tturnstile> wp prog' P
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pequivI[intro]:
  "\<lbrakk> \<And>P. sound P \<Longrightarrow> wp prog P = wp prog' P \<rbrakk> \<Longrightarrow> prog \<simeq> prog'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. sound P \<Longrightarrow> wp prog P = wp prog' P) \<Longrightarrow> prog \<simeq> prog'
[PROOF STEP]
unfolding pequiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. sound P \<Longrightarrow> wp prog P = wp prog' P) \<Longrightarrow> \<forall>P. sound P \<longrightarrow> wp prog P = wp prog' P
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pequivD[dest,simp]:
  "\<lbrakk> prog \<simeq> prog'; sound P \<rbrakk> \<Longrightarrow> wp prog P = wp prog' P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prog \<simeq> prog'; sound P\<rbrakk> \<Longrightarrow> wp prog P = wp prog' P
[PROOF STEP]
unfolding pequiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>P. sound P \<longrightarrow> wp prog P = wp prog' P; sound P\<rbrakk> \<Longrightarrow> wp prog P = wp prog' P
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pequiv_equiv_trans:
  "a \<simeq> b \<longleftrightarrow> equiv_trans (wp a) (wp b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<simeq> b = equiv_trans (wp a) (wp b)
[PROOF STEP]
by(auto)


[STATEMENT]
lemma DC_comm[ac_simps]:
  "a \<Sqinter> b = b \<Sqinter> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<Sqinter> b = b \<Sqinter> a
[PROOF STEP]
unfolding DC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>ab Q s. min (a ab Q s) (b ab Q s)) = (\<lambda>ab Q s. min (b ab Q s) (a ab Q s))
[PROOF STEP]
by(simp add:ac_simps)


[STATEMENT]
lemma DC_assoc[ac_simps]:
  "a \<Sqinter> (b \<Sqinter> c) = (a \<Sqinter> b) \<Sqinter> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<Sqinter> b \<Sqinter> c = (a \<Sqinter> b) \<Sqinter> c
[PROOF STEP]
unfolding DC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>ab Q s. min (a ab Q s) (min (b ab Q s) (c ab Q s))) = (\<lambda>ab Q s. min (min (a ab Q s) (b ab Q s)) (c ab Q s))
[PROOF STEP]
by(simp add:ac_simps)


[STATEMENT]
lemma DC_idem:
  "a \<Sqinter> a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<Sqinter> a = a
[PROOF STEP]
unfolding DC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>ab Q s. min (a ab Q s) (a ab Q s)) = a
[PROOF STEP]
by(simp)


[STATEMENT]
lemma AC_comm[ac_simps]:
  "a \<Squnion> b = b \<Squnion> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<Squnion> b = b \<Squnion> a
[PROOF STEP]
unfolding AC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>ab Q s. max (a ab Q s) (b ab Q s)) = (\<lambda>ab Q s. max (b ab Q s) (a ab Q s))
[PROOF STEP]
by(simp add:ac_simps)


[STATEMENT]
lemma AC_assoc[ac_simps]:
  "a \<Squnion> (b \<Squnion> c) = (a \<Squnion> b) \<Squnion> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<Squnion> b \<Squnion> c = (a \<Squnion> b) \<Squnion> c
[PROOF STEP]
unfolding AC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>ab Q s. max (a ab Q s) (max (b ab Q s) (c ab Q s))) = (\<lambda>ab Q s. max (max (a ab Q s) (b ab Q s)) (c ab Q s))
[PROOF STEP]
by(simp add:ac_simps)


[STATEMENT]
lemma AC_idem:
  "a \<Squnion> a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<Squnion> a = a
[PROOF STEP]
unfolding AC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>ab Q s. max (a ab Q s) (a ab Q s)) = a
[PROOF STEP]
by(simp)


[STATEMENT]
lemma PC_quasi_comm:
  "a \<^bsub>p\<^esub>\<oplus> b = b \<^bsub>(\<lambda>s. 1 - p s)\<^esub>\<oplus> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<^bsub>p\<^esub>\<oplus> b = b \<^bsub>(\<lambda>s. 1 - p s)\<^esub>\<oplus> a
[PROOF STEP]
unfolding PC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>ab Q s. p s * a ab Q s + (1 - p s) * b ab Q s) = (\<lambda>ab Q s. (1 - p s) * b ab Q s + (1 - (1 - p s)) * a ab Q s)
[PROOF STEP]
by(simp add:algebra_simps)


[STATEMENT]
lemma PC_idem:
  "a \<^bsub>p\<^esub>\<oplus> a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<^bsub>p\<^esub>\<oplus> a = a
[PROOF STEP]
unfolding PC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>ab Q s. p s * a ab Q s + (1 - p s) * a ab Q s) = a
[PROOF STEP]
by(simp add:algebra_simps)


[STATEMENT]
lemma Seq_assoc[ac_simps]:
  "A ;; (B ;; C) = A ;; B ;; C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ;; (B ;; C) = A ;; B ;; C
[PROOF STEP]
by(simp add:Seq_def o_def)


[STATEMENT]
lemma Abort_refines[intro]:
  "well_def a \<Longrightarrow> Abort \<sqsubseteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_def a \<Longrightarrow> Abort \<sqsubseteq> a
[PROOF STEP]
by(rule refinesI, unfold wp_eval, auto dest!:well_def_wp_healthy)


[STATEMENT]
lemma left_refines_DC:
  "(a \<Sqinter> b) \<sqsubseteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<Sqinter> b) \<sqsubseteq> a
[PROOF STEP]
by(auto intro!:refinesI simp:wp_eval)


[STATEMENT]
lemma right_refines_DC:
  "(a \<Sqinter> b) \<sqsubseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<Sqinter> b) \<sqsubseteq> b
[PROOF STEP]
by(auto intro!:refinesI simp:wp_eval)


[STATEMENT]
lemma DC_refines:
  fixes a::"'s prog" and b and c
  assumes rab: "a \<sqsubseteq> b" and rac: "a \<sqsubseteq> c"
  shows "a \<sqsubseteq> (b \<Sqinter> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqsubseteq> (b \<Sqinter> c)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp a P \<tturnstile> wp (b \<Sqinter> c) P
[PROOF STEP]
fix P::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp a P \<tturnstile> wp (b \<Sqinter> c) P
[PROOF STEP]
assume sP: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp a P \<tturnstile> wp (b \<Sqinter> c) P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
a \<sqsubseteq> b
a \<sqsubseteq> c
sound P
[PROOF STEP]
have "wp a P \<tturnstile> wp b P" and "wp a P \<tturnstile> wp c P"
[PROOF STATE]
proof (prove)
using this:
a \<sqsubseteq> b
a \<sqsubseteq> c
sound P

goal (1 subgoal):
 1. wp a P \<tturnstile> wp b P &&& wp a P \<tturnstile> wp c P
[PROOF STEP]
by(auto dest:refinesD)
[PROOF STATE]
proof (state)
this:
wp a P \<tturnstile> wp b P
wp a P \<tturnstile> wp c P

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp a P \<tturnstile> wp (b \<Sqinter> c) P
[PROOF STEP]
thus "wp a P \<tturnstile> wp (b \<Sqinter> c) P"
[PROOF STATE]
proof (prove)
using this:
wp a P \<tturnstile> wp b P
wp a P \<tturnstile> wp c P

goal (1 subgoal):
 1. wp a P \<tturnstile> wp (b \<Sqinter> c) P
[PROOF STEP]
by(auto simp:wp_eval intro:min.boundedI)
[PROOF STATE]
proof (state)
this:
wp a P \<tturnstile> wp (b \<Sqinter> c) P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DC_mono:
  fixes a::"'s prog"
  assumes rab: "a \<sqsubseteq> b" and rcd: "c \<sqsubseteq> d"
  shows "(a \<Sqinter> c) \<sqsubseteq> (b \<Sqinter> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<Sqinter> c) \<sqsubseteq> (b \<Sqinter> d)
[PROOF STEP]
proof(rule refinesI, unfold wp_eval, rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp c P x) \<le> min (wp b P x) (wp d P x)
[PROOF STEP]
fix P::"'s \<Rightarrow> real" and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp c P x) \<le> min (wp b P x) (wp d P x)
[PROOF STEP]
assume sP: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp c P x) \<le> min (wp b P x) (wp d P x)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
a \<sqsubseteq> b
c \<sqsubseteq> d
sound P
[PROOF STEP]
have "wp a P s \<le> wp b P s" and "wp c P s \<le> wp d P s"
[PROOF STATE]
proof (prove)
using this:
a \<sqsubseteq> b
c \<sqsubseteq> d
sound P

goal (1 subgoal):
 1. wp a P s \<le> wp b P s &&& wp c P s \<le> wp d P s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp a P s \<le> wp b P s
wp c P s \<le> wp d P s

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp c P x) \<le> min (wp b P x) (wp d P x)
[PROOF STEP]
thus "min (wp a P s) (wp c P s) \<le> min (wp b P s) (wp d P s)"
[PROOF STATE]
proof (prove)
using this:
wp a P s \<le> wp b P s
wp c P s \<le> wp d P s

goal (1 subgoal):
 1. min (wp a P s) (wp c P s) \<le> min (wp b P s) (wp d P s)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
min (wp a P s) (wp c P s) \<le> min (wp b P s) (wp d P s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma left_refines_AC:
  "a \<sqsubseteq> (a \<Squnion> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqsubseteq> (a \<Squnion> b)
[PROOF STEP]
by(auto intro!:refinesI simp:wp_eval)


[STATEMENT]
lemma right_refines_AC:
  "b \<sqsubseteq> (a \<Squnion> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqsubseteq> (a \<Squnion> b)
[PROOF STEP]
by(auto intro!:refinesI simp:wp_eval)


[STATEMENT]
lemma AC_refines:
  fixes a::"'s prog" and b and c
  assumes rac: "a \<sqsubseteq> c" and rbc: "b \<sqsubseteq> c"
  shows "(a \<Squnion> b) \<sqsubseteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<Squnion> b) \<sqsubseteq> c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp (a \<Squnion> b) P \<tturnstile> wp c P
[PROOF STEP]
fix P::"'s \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp (a \<Squnion> b) P \<tturnstile> wp c P
[PROOF STEP]
assume sP: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp (a \<Squnion> b) P \<tturnstile> wp c P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
a \<sqsubseteq> c
b \<sqsubseteq> c
sound P
[PROOF STEP]
have "\<And>s. wp a P s \<le> wp c P s"
              and "\<And>s. wp b P s \<le> wp c P s"
[PROOF STATE]
proof (prove)
using this:
a \<sqsubseteq> c
b \<sqsubseteq> c
sound P

goal (1 subgoal):
 1. (\<And>s. wp a P s \<le> wp c P s) &&& (\<And>s. wp b P s \<le> wp c P s)
[PROOF STEP]
by(auto dest:refinesD)
[PROOF STATE]
proof (state)
this:
wp a P ?s \<le> wp c P ?s
wp b P ?s \<le> wp c P ?s

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp (a \<Squnion> b) P \<tturnstile> wp c P
[PROOF STEP]
thus "wp (a \<Squnion> b) P \<tturnstile> wp c P"
[PROOF STATE]
proof (prove)
using this:
wp a P ?s \<le> wp c P ?s
wp b P ?s \<le> wp c P ?s

goal (1 subgoal):
 1. wp (a \<Squnion> b) P \<tturnstile> wp c P
[PROOF STEP]
unfolding wp_eval
[PROOF STATE]
proof (prove)
using this:
wp a P ?s \<le> wp c P ?s
wp b P ?s \<le> wp c P ?s

goal (1 subgoal):
 1. \<lambda>s. max (wp a P s) (wp b P s) \<tturnstile> wp c P
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp (a \<Squnion> b) P \<tturnstile> wp c P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma AC_mono:
  fixes a::"'s prog"
  assumes rab: "a \<sqsubseteq> b" and rcd: "c \<sqsubseteq> d"
  shows "(a \<Squnion> c) \<sqsubseteq> (b \<Squnion> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<Squnion> c) \<sqsubseteq> (b \<Squnion> d)
[PROOF STEP]
proof(rule refinesI, unfold wp_eval, rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> max (wp a P x) (wp c P x) \<le> max (wp b P x) (wp d P x)
[PROOF STEP]
fix P::"'s \<Rightarrow> real" and s::'s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> max (wp a P x) (wp c P x) \<le> max (wp b P x) (wp d P x)
[PROOF STEP]
assume sP: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> max (wp a P x) (wp c P x) \<le> max (wp b P x) (wp d P x)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
a \<sqsubseteq> b
c \<sqsubseteq> d
sound P
[PROOF STEP]
have "wp a P s \<le> wp b P s" and "wp c P s \<le> wp d P s"
[PROOF STATE]
proof (prove)
using this:
a \<sqsubseteq> b
c \<sqsubseteq> d
sound P

goal (1 subgoal):
 1. wp a P s \<le> wp b P s &&& wp c P s \<le> wp d P s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp a P s \<le> wp b P s
wp c P s \<le> wp d P s

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> max (wp a P x) (wp c P x) \<le> max (wp b P x) (wp d P x)
[PROOF STEP]
thus "max (wp a P s) (wp c P s) \<le> max (wp b P s) (wp d P s)"
[PROOF STATE]
proof (prove)
using this:
wp a P s \<le> wp b P s
wp c P s \<le> wp d P s

goal (1 subgoal):
 1. max (wp a P s) (wp c P s) \<le> max (wp b P s) (wp d P s)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
max (wp a P s) (wp c P s) \<le> max (wp b P s) (wp d P s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DC_refines_PC:
  assumes unit: "unitary p"
  shows "(a \<Sqinter> b) \<sqsubseteq> (a \<^bsub>p\<^esub>\<oplus> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<Sqinter> b) \<sqsubseteq> (a \<^bsub>p\<^esub>\<oplus> b)
[PROOF STEP]
proof(rule refinesI, unfold wp_eval, rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp b P x) \<le> p x * wp a P x + (1 - p x) * wp b P x
[PROOF STEP]
fix s and P::"'a \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp b P x) \<le> p x * wp a P x + (1 - p x) * wp b P x
[PROOF STEP]
assume sound: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp b P x) \<le> p x * wp a P x + (1 - p x) * wp b P x
[PROOF STEP]
from unit
[PROOF STATE]
proof (chain)
picking this:
unitary p
[PROOF STEP]
have nn_p: "0 \<le> p s"
[PROOF STATE]
proof (prove)
using this:
unitary p

goal (1 subgoal):
 1. 0 \<le> p s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> p s

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp b P x) \<le> p x * wp a P x + (1 - p x) * wp b P x
[PROOF STEP]
from unit
[PROOF STATE]
proof (chain)
picking this:
unitary p
[PROOF STEP]
have "p s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary p

goal (1 subgoal):
 1. p s \<le> 1
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
p s \<le> 1

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp b P x) \<le> p x * wp a P x + (1 - p x) * wp b P x
[PROOF STEP]
hence nn_np: "0 \<le> 1 - p s"
[PROOF STATE]
proof (prove)
using this:
p s \<le> 1

goal (1 subgoal):
 1. 0 \<le> 1 - p s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
0 \<le> 1 - p s

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> min (wp a P x) (wp b P x) \<le> p x * wp a P x + (1 - p x) * wp b P x
[PROOF STEP]
show "min (wp a P s) (wp b P s) \<le> p s * wp a P s + (1 - p s) * wp b P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (wp a P s) (wp b P s) \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
proof(cases "wp a P s \<le> wp b P s",
      simp_all add:min.absorb1 min.absorb2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
wp a P s \<le> wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
note le = this
[PROOF STATE]
proof (state)
this:
wp a P s \<le> wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
have "wp a P s = (p s + (1 - p s)) * wp a P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp a P s = (p s + (1 - p s)) * wp a P s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp a P s = (p s + (1 - p s)) * wp a P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp a P s = (p s + (1 - p s)) * wp a P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
have "... = p s * wp a P s + (1 - p s) * wp a P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p s + (1 - p s)) * wp a P s = p s * wp a P s + (1 - p s) * wp a P s
[PROOF STEP]
by(simp only: distrib_right)
[PROOF STATE]
proof (state)
this:
(p s + (1 - p s)) * wp a P s = p s * wp a P s + (1 - p s) * wp a P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(p s + (1 - p s)) * wp a P s = p s * wp a P s + (1 - p s) * wp a P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(p s + (1 - p s)) * wp a P s = p s * wp a P s + (1 - p s) * wp a P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
from le and nn_np
[PROOF STATE]
proof (chain)
picking this:
wp a P s \<le> wp b P s
0 \<le> 1 - p s
[PROOF STEP]
have "(1 - p s) * wp a P s \<le> (1 - p s) * wp b P s"
[PROOF STATE]
proof (prove)
using this:
wp a P s \<le> wp b P s
0 \<le> 1 - p s

goal (1 subgoal):
 1. (1 - p s) * wp a P s \<le> (1 - p s) * wp b P s
[PROOF STEP]
by(rule mult_left_mono)
[PROOF STATE]
proof (state)
this:
(1 - p s) * wp a P s \<le> (1 - p s) * wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
hence "p s * wp a P s + (1 - p s) * wp a P s \<le>
        p s * wp a P s + (1 - p s) * wp b P s"
[PROOF STATE]
proof (prove)
using this:
(1 - p s) * wp a P s \<le> (1 - p s) * wp b P s

goal (1 subgoal):
 1. p s * wp a P s + (1 - p s) * wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
by(rule add_left_mono)
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
show "wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s"
[PROOF STATE]
proof (prove)
using this:
wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s

goal (1 subgoal):
 1. wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wp a P s \<le> p s * wp a P s + (1 - p s) * wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> wp a P s \<le> wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> wp a P s \<le> wp b P s
[PROOF STEP]
have le: "wp b P s \<le> wp a P s"
[PROOF STATE]
proof (prove)
using this:
\<not> wp a P s \<le> wp b P s

goal (1 subgoal):
 1. wp b P s \<le> wp a P s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp b P s \<le> wp a P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
have "wp b P s = (p s + (1 - p s)) * wp b P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp b P s = (p s + (1 - p s)) * wp b P s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
wp b P s = (p s + (1 - p s)) * wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp b P s = (p s + (1 - p s)) * wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
have "... = p s * wp b P s + (1 - p s) * wp b P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p s + (1 - p s)) * wp b P s = p s * wp b P s + (1 - p s) * wp b P s
[PROOF STEP]
by(simp only:distrib_right)
[PROOF STATE]
proof (state)
this:
(p s + (1 - p s)) * wp b P s = p s * wp b P s + (1 - p s) * wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(p s + (1 - p s)) * wp b P s = p s * wp b P s + (1 - p s) * wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(p s + (1 - p s)) * wp b P s = p s * wp b P s + (1 - p s) * wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
from le and nn_p
[PROOF STATE]
proof (chain)
picking this:
wp b P s \<le> wp a P s
0 \<le> p s
[PROOF STEP]
have "p s * wp b P s \<le> p s * wp a P s"
[PROOF STATE]
proof (prove)
using this:
wp b P s \<le> wp a P s
0 \<le> p s

goal (1 subgoal):
 1. p s * wp b P s \<le> p s * wp a P s
[PROOF STEP]
by(rule mult_left_mono)
[PROOF STATE]
proof (state)
this:
p s * wp b P s \<le> p s * wp a P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
hence "p s * wp b P s + (1 - p s) * wp b P s \<le>
        p s * wp a P s + (1 - p s) * wp b P s"
[PROOF STATE]
proof (prove)
using this:
p s * wp b P s \<le> p s * wp a P s

goal (1 subgoal):
 1. p s * wp b P s + (1 - p s) * wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
by(rule add_right_mono)
[PROOF STATE]
proof (state)
this:
p s * wp b P s + (1 - p s) * wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p s * wp b P s + (1 - p s) * wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
show "wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s"
[PROOF STATE]
proof (prove)
using this:
wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s

goal (1 subgoal):
 1. wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wp b P s \<le> p s * wp a P s + (1 - p s) * wp b P s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
min (wp a P s) (wp b P s) \<le> p s * wp a P s + (1 - p s) * wp b P s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PC_refines_AC:
  assumes unit: "unitary p"
  shows "(a \<^bsub>p\<^esub>\<oplus> b) \<sqsubseteq> (a \<Squnion> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<^bsub>p\<^esub>\<oplus> b) \<sqsubseteq> (a \<Squnion> b)
[PROOF STEP]
proof(rule refinesI, unfold wp_eval, rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> p x * wp a P x + (1 - p x) * wp b P x \<le> max (wp a P x) (wp b P x)
[PROOF STEP]
fix s and P::"'a \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> p x * wp a P x + (1 - p x) * wp b P x \<le> max (wp a P x) (wp b P x)
[PROOF STEP]
assume sound: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> p x * wp a P x + (1 - p x) * wp b P x \<le> max (wp a P x) (wp b P x)
[PROOF STEP]
from unit
[PROOF STATE]
proof (chain)
picking this:
unitary p
[PROOF STEP]
have "p s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary p

goal (1 subgoal):
 1. p s \<le> 1
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
p s \<le> 1

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> p x * wp a P x + (1 - p x) * wp b P x \<le> max (wp a P x) (wp b P x)
[PROOF STEP]
hence nn_np: "0 \<le> 1 - p s"
[PROOF STATE]
proof (prove)
using this:
p s \<le> 1

goal (1 subgoal):
 1. 0 \<le> 1 - p s
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
0 \<le> 1 - p s

goal (1 subgoal):
 1. \<And>P x. sound P \<Longrightarrow> p x * wp a P x + (1 - p x) * wp b P x \<le> max (wp a P x) (wp b P x)
[PROOF STEP]
show "p s * wp a P s + (1 - p s) * wp b P s \<le>
        max (wp a P s) (wp b P s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
proof(cases "wp a P s \<le> wp b P s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
wp a P s \<le> wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
note leab = this
[PROOF STATE]
proof (state)
this:
wp a P s \<le> wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
with unit nn_np
[PROOF STATE]
proof (chain)
picking this:
unitary p
0 \<le> 1 - p s
wp a P s \<le> wp b P s
[PROOF STEP]
have "p s * wp a P s + (1 - p s) * wp b P s \<le>
          p s * wp b P s + (1 - p s) * wp b P s"
[PROOF STATE]
proof (prove)
using this:
unitary p
0 \<le> 1 - p s
wp a P s \<le> wp b P s

goal (1 subgoal):
 1. p s * wp a P s + (1 - p s) * wp b P s \<le> p s * wp b P s + (1 - p s) * wp b P s
[PROOF STEP]
by(auto intro:add_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp b P s \<le> p s * wp b P s + (1 - p s) * wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp b P s \<le> p s * wp b P s + (1 - p s) * wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
have "... = wp b P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p s * wp b P s + (1 - p s) * wp b P s = wp b P s
[PROOF STEP]
by(auto simp:field_simps)
[PROOF STATE]
proof (state)
this:
p s * wp b P s + (1 - p s) * wp b P s = wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p s * wp b P s + (1 - p s) * wp b P s = wp b P s

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
from leab
[PROOF STATE]
proof (chain)
picking this:
wp a P s \<le> wp b P s
[PROOF STEP]
have "... = max (wp a P s) (wp b P s)"
[PROOF STATE]
proof (prove)
using this:
wp a P s \<le> wp b P s

goal (1 subgoal):
 1. wp b P s = max (wp a P s) (wp b P s)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp b P s = max (wp a P s) (wp b P s)

goal (2 subgoals):
 1. wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
 2. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)

goal (1 subgoal):
 1. p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> wp a P s \<le> wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
note leba = this
[PROOF STATE]
proof (state)
this:
\<not> wp a P s \<le> wp b P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
with unit nn_np
[PROOF STATE]
proof (chain)
picking this:
unitary p
0 \<le> 1 - p s
\<not> wp a P s \<le> wp b P s
[PROOF STEP]
have "p s * wp a P s + (1 - p s) * wp b P s \<le>
          p s * wp a P s + (1 - p s) * wp a P s"
[PROOF STATE]
proof (prove)
using this:
unitary p
0 \<le> 1 - p s
\<not> wp a P s \<le> wp b P s

goal (1 subgoal):
 1. p s * wp a P s + (1 - p s) * wp b P s \<le> p s * wp a P s + (1 - p s) * wp a P s
[PROOF STEP]
by(auto intro:add_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp b P s \<le> p s * wp a P s + (1 - p s) * wp a P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp b P s \<le> p s * wp a P s + (1 - p s) * wp a P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
have "... = wp a P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p s * wp a P s + (1 - p s) * wp a P s = wp a P s
[PROOF STEP]
by(auto simp:field_simps)
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp a P s = wp a P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp a P s = wp a P s

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
from leba
[PROOF STATE]
proof (chain)
picking this:
\<not> wp a P s \<le> wp b P s
[PROOF STEP]
have "... = max (wp a P s) (wp b P s)"
[PROOF STATE]
proof (prove)
using this:
\<not> wp a P s \<le> wp b P s

goal (1 subgoal):
 1. wp a P s = max (wp a P s) (wp b P s)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
wp a P s = max (wp a P s) (wp b P s)

goal (1 subgoal):
 1. \<not> wp a P s \<le> wp b P s \<Longrightarrow> p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)

goal (1 subgoal):
 1. p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p s * wp a P s + (1 - p s) * wp b P s \<le> max (wp a P s) (wp b P s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DC_refines_AC:
  "(a \<Sqinter> b) \<sqsubseteq> (a \<Squnion> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<Sqinter> b) \<sqsubseteq> (a \<Squnion> b)
[PROOF STEP]
by(auto intro!:refinesI simp:wp_eval)


[STATEMENT]
lemma pr_trans[trans]:
  fixes A::"'a prog"
  assumes prAB: "A \<sqsubseteq> B"
      and prBC: "B \<sqsubseteq> C"
  shows "A \<sqsubseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq> C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp A P \<tturnstile> wp C P
[PROOF STEP]
fix P::"'a \<Rightarrow> real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp A P \<tturnstile> wp C P
[PROOF STEP]
assume sP: "sound P"
[PROOF STATE]
proof (state)
this:
sound P

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp A P \<tturnstile> wp C P
[PROOF STEP]
with prAB
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubseteq> B
sound P
[PROOF STEP]
have "wp A P \<tturnstile> wp B P"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubseteq> B
sound P

goal (1 subgoal):
 1. wp A P \<tturnstile> wp B P
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
wp A P \<tturnstile> wp B P

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp A P \<tturnstile> wp C P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wp A P \<tturnstile> wp B P

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp A P \<tturnstile> wp C P
[PROOF STEP]
from sP and prBC
[PROOF STATE]
proof (chain)
picking this:
sound P
B \<sqsubseteq> C
[PROOF STEP]
have "... \<tturnstile> wp C P"
[PROOF STATE]
proof (prove)
using this:
sound P
B \<sqsubseteq> C

goal (1 subgoal):
 1. wp B P \<tturnstile> wp C P
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
wp B P \<tturnstile> wp C P

goal (1 subgoal):
 1. \<And>P. sound P \<Longrightarrow> wp A P \<tturnstile> wp C P
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wp A P \<tturnstile> wp C P
[PROOF STEP]
show "wp A P \<tturnstile> ..."
[PROOF STATE]
proof (prove)
using this:
wp A P \<tturnstile> wp C P

goal (1 subgoal):
 1. wp A P \<tturnstile> wp C P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wp A P \<tturnstile> wp C P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pequiv_refl[intro!,simp]:
  "a \<simeq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<simeq> a
[PROOF STEP]
by(auto)


[STATEMENT]
lemma pequiv_comm[ac_simps]:
  "a \<simeq> b \<longleftrightarrow> b \<simeq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<simeq> b = b \<simeq> a
[PROOF STEP]
unfolding pequiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>P. sound P \<longrightarrow> wp a P = wp b P) = (\<forall>P. sound P \<longrightarrow> wp b P = wp a P)
[PROOF STEP]
by(rule iffI, safe, simp_all)


[STATEMENT]
lemma pequiv_pr[dest]:
  "a \<simeq> b \<Longrightarrow> a \<sqsubseteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<simeq> b \<Longrightarrow> a \<sqsubseteq> b
[PROOF STEP]
by(auto)


[STATEMENT]
lemma pequiv_trans[intro,trans]:
  "\<lbrakk> a \<simeq> b; b \<simeq> c \<rbrakk> \<Longrightarrow> a \<simeq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<simeq> b; b \<simeq> c\<rbrakk> \<Longrightarrow> a \<simeq> c
[PROOF STEP]
unfolding pequiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>P. sound P \<longrightarrow> wp a P = wp b P; \<forall>P. sound P \<longrightarrow> wp b P = wp c P\<rbrakk> \<Longrightarrow> \<forall>P. sound P \<longrightarrow> wp a P = wp c P
[PROOF STEP]
by(auto intro!:order_trans)


[STATEMENT]
lemma pequiv_pr_trans[intro,trans]:
  "\<lbrakk> a \<simeq> b; b \<sqsubseteq> c \<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<simeq> b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c
[PROOF STEP]
unfolding pequiv_def refines_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>P. sound P \<longrightarrow> wp a P = wp b P; \<forall>P. sound P \<longrightarrow> wp b P \<tturnstile> wp c P\<rbrakk> \<Longrightarrow> \<forall>P. sound P \<longrightarrow> wp a P \<tturnstile> wp c P
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pr_pequiv_trans[intro,trans]:
  "\<lbrakk> a \<sqsubseteq> b; b \<simeq> c \<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<sqsubseteq> b; b \<simeq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c
[PROOF STEP]
unfolding pequiv_def refines_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>P. sound P \<longrightarrow> wp a P \<tturnstile> wp b P; \<forall>P. sound P \<longrightarrow> wp b P = wp c P\<rbrakk> \<Longrightarrow> \<forall>P. sound P \<longrightarrow> wp a P \<tturnstile> wp c P
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pequiv_antisym:
  "\<lbrakk> a \<sqsubseteq> b; b \<sqsubseteq> a \<rbrakk> \<Longrightarrow> a \<simeq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<sqsubseteq> b; b \<sqsubseteq> a\<rbrakk> \<Longrightarrow> a \<simeq> b
[PROOF STEP]
by(auto intro:antisym)


[STATEMENT]
lemma pequiv_DC:
  "\<lbrakk> a \<simeq> c; b \<simeq> d \<rbrakk> \<Longrightarrow> (a \<Sqinter> b) \<simeq> (c \<Sqinter> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<simeq> c; b \<simeq> d\<rbrakk> \<Longrightarrow> (a \<Sqinter> b) \<simeq> (c \<Sqinter> d)
[PROOF STEP]
by(auto intro!:DC_mono pequiv_antisym simp:ac_simps)


[STATEMENT]
lemma pequiv_AC:
  "\<lbrakk> a \<simeq> c; b \<simeq> d \<rbrakk> \<Longrightarrow> (a \<Squnion> b) \<simeq> (c \<Squnion> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<simeq> c; b \<simeq> d\<rbrakk> \<Longrightarrow> (a \<Squnion> b) \<simeq> (c \<Squnion> d)
[PROOF STEP]
by(auto intro!:AC_mono pequiv_antisym simp:ac_simps)