[STATEMENT]
lemma iter_dom_invariant_complete:
    shows "\<And>res.  iter f step start (unstables r step start) = (ss',w') \<longrightarrow> i < n \<and> ss'!i =  res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>res. iter f step start (unstables r step start) = (ss', w') \<longrightarrow> i < n \<and> ss' ! i = res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i
[PROOF STEP]
apply (unfold iter_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>res. while (\<lambda>(\<tau>s, w). w \<noteq> []) (\<lambda>(\<tau>s, w). let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w)) (start, unstables r step start) = (ss', w') \<longrightarrow> i < n \<and> ss' ! i = res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i
[PROOF STEP]
apply(rule_tac
      P = "(\<lambda>(ss, w). wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss!i =  rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i))" and
      r = "{(ss',ss). ss [\<sqsubset>\<^sub>r] ss'} <*lex*> (\<lambda>(x,y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset"
      in while_rule)
  \<comment> \<open>Invariant holds initially:\<close>
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>res. case (start, unstables r step start) of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i)
 2. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w) of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i)
 3. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> i < n \<and> ss' ! i = res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i
 4. \<And>res. wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 5. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. wf_dom start (unstables r step start) \<and> (\<forall>i. i < n \<and> k \<notin> set (start ! i) \<longrightarrow> non_strict_dominate k i)
 2. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w) of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i)
 3. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> i < n \<and> ss' ! i = res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i
 4. \<And>res. wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 5. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply (fastforce simp add:start_non_sdom wf_start)

  \<comment> \<open>Invariant is preserved:\<close>
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> case case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w) of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i)
 2. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> i < n \<and> ss' ! i = res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i
 3. \<And>res. wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 4. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply (fastforce dest:propa_dom_invariant_complete)

  \<comment> \<open>Postcondition holds upon termination:\<close>
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); \<not> (case s of (\<tau>s, w) \<Rightarrow> w \<noteq> [])\<rbrakk> \<Longrightarrow> s = (ss', w') \<longrightarrow> i < n \<and> ss' ! i = res \<and> k \<notin> set res \<longrightarrow> non_strict_dominate k i
 2. \<And>res. wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 3. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply clarsimp

  \<comment> \<open>Well-foundedness of the termination relation:\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>res. wf ({(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset)
 2. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply (simp add:wf_listn_termination_rel)

  \<comment> \<open>Loop decreases along termination relation:\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>res s. \<lbrakk>case s of (ss, w) \<Rightarrow> wf_dom ss w \<and> (\<forall>i. (\<exists>rs. i < n \<and> ss ! i = rs \<and> k \<notin> set rs) \<longrightarrow> non_strict_dominate k i); case s of (\<tau>s, w) \<Rightarrow> w \<noteq> []\<rbrakk> \<Longrightarrow> (case s of (\<tau>s, w) \<Rightarrow> let p = hd w in propa f (step p (\<tau>s ! p)) \<tau>s (tl w), s) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>(x, y). (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b \<noteq> []; wf_dom a b; \<forall>i. i < n \<and> k \<notin> set (a ! i) \<longrightarrow> non_strict_dominate k i\<rbrakk> \<Longrightarrow> (propa f (step (hd b) (a ! hd b)) a (tl b), a, b) \<in> {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'} <*lex*> (\<lambda>x. case x of (x, y) \<Rightarrow> (sorted_list_of_set x, sorted_list_of_set y)) ` finite_psubset
[PROOF STEP]
apply (fastforce dest:propa_termination)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s
[PROOF STEP]
by blast


[STATEMENT]
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t"
shows "t = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = s
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. t = s
[PROOF STEP]
proof cases  \<comment> \<open>inverting assms\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
 2. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
case IfTrue
[PROOF STATE]
proof (state)
this:
bval b s
(SKIP, s) \<Rightarrow> t

goal (2 subgoals):
 1. \<lbrakk>bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
 2. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
thm IfTrue
[PROOF STATE]
proof (state)
this:
bval b s
(SKIP, s) \<Rightarrow> t

goal (2 subgoals):
 1. \<lbrakk>bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
 2. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bval b s
(SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. t = s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t = s

goal (1 subgoal):
 1. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
case IfFalse
[PROOF STATE]
proof (state)
this:
\<not> bval b s
(SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> t\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s
(SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. t = s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t = s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t = s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma assign_simp:
  "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ::= a, s) \<Rightarrow> s' = (s' = s(x := aval a s))
[PROOF STEP]
by auto


[STATEMENT]
lemma Seq_assoc:
  "(c1;; c2;; c3, s) \<Rightarrow> s' \<longleftrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c1;; c2;; c3, s) \<Rightarrow> s' = (c1;; (c2;; c3), s) \<Rightarrow> s'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (c1;; c2;; c3, s) \<Rightarrow> s' \<Longrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'
 2. (c1;; (c2;; c3), s) \<Rightarrow> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
assume "(c1;; c2;; c3, s) \<Rightarrow> s'"
[PROOF STATE]
proof (state)
this:
(c1;; c2;; c3, s) \<Rightarrow> s'

goal (2 subgoals):
 1. (c1;; c2;; c3, s) \<Rightarrow> s' \<Longrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'
 2. (c1;; (c2;; c3), s) \<Rightarrow> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
obtain s1 s2 where
    c1: "(c1, s) \<Rightarrow> s1" and
    c2: "(c2, s1) \<Rightarrow> s2" and
    c3: "(c3, s2) \<Rightarrow> s'"
[PROOF STATE]
proof (prove)
using this:
(c1;; c2;; c3, s) \<Rightarrow> s'

goal (1 subgoal):
 1. (\<And>s1 s2. \<lbrakk>(c1, s) \<Rightarrow> s1; (c2, s1) \<Rightarrow> s2; (c3, s2) \<Rightarrow> s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(c1, s) \<Rightarrow> s1
(c2, s1) \<Rightarrow> s2
(c3, s2) \<Rightarrow> s'

goal (2 subgoals):
 1. (c1;; c2;; c3, s) \<Rightarrow> s' \<Longrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'
 2. (c1;; (c2;; c3), s) \<Rightarrow> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
from c2 c3
[PROOF STATE]
proof (chain)
picking this:
(c2, s1) \<Rightarrow> s2
(c3, s2) \<Rightarrow> s'
[PROOF STEP]
have "(c2;; c3, s1) \<Rightarrow> s'"
[PROOF STATE]
proof (prove)
using this:
(c2, s1) \<Rightarrow> s2
(c3, s2) \<Rightarrow> s'

goal (1 subgoal):
 1. (c2;; c3, s1) \<Rightarrow> s'
[PROOF STEP]
by (rule Seq)
[PROOF STATE]
proof (state)
this:
(c2;; c3, s1) \<Rightarrow> s'

goal (2 subgoals):
 1. (c1;; c2;; c3, s) \<Rightarrow> s' \<Longrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> s'
 2. (c1;; (c2;; c3), s) \<Rightarrow> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
with c1
[PROOF STATE]
proof (chain)
picking this:
(c1, s) \<Rightarrow> s1
(c2;; c3, s1) \<Rightarrow> s'
[PROOF STEP]
show "(c1;; (c2;; c3), s) \<Rightarrow> s'"
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<Rightarrow> s1
(c2;; c3, s1) \<Rightarrow> s'

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> s'
[PROOF STEP]
by (rule Seq)
[PROOF STATE]
proof (state)
this:
(c1;; (c2;; c3), s) \<Rightarrow> s'

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
next
  \<comment> \<open>The other direction is analogous\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
assume "(c1;; (c2;; c3), s) \<Rightarrow> s'"
[PROOF STATE]
proof (state)
this:
(c1;; (c2;; c3), s) \<Rightarrow> s'

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
thus "(c1;; c2;; c3, s) \<Rightarrow> s'"
[PROOF STATE]
proof (prove)
using this:
(c1;; (c2;; c3), s) \<Rightarrow> s'

goal (1 subgoal):
 1. (c1;; c2;; c3, s) \<Rightarrow> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(c1;; c2;; c3, s) \<Rightarrow> s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unfold_while:
  "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
proof -
  \<comment> \<open>to show the equivalence, we look at the derivation tree for\<close>
  \<comment> \<open>each side and from that construct a derivation tree for the other side\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
fix s t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
assume "(?w, s) \<Rightarrow> t"
    \<comment> \<open>as a first thing we note that, if @{text b} is @{text False} in state @{text s},\<close>
    \<comment> \<open>then both statements do nothing:\<close>
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
assume "\<not>bval b s"
[PROOF STATE]
proof (state)
this:
\<not> bval b s

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
hence "t = s"
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s

goal (1 subgoal):
 1. t = s
[PROOF STEP]
using \<open>(?w,s) \<Rightarrow> t\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s
(WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. t = s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t = s

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
hence "(?iw, s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
t = s

goal (1 subgoal):
 1. (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
[PROOF STEP]
using \<open>\<not>bval b s\<close>
[PROOF STATE]
proof (prove)
using this:
t = s
\<not> bval b s

goal (1 subgoal):
 1. (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> bval b s \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
moreover
    \<comment> \<open>on the other hand, if @{text b} is @{text True} in state @{text s},\<close>
    \<comment> \<open>then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"}\<close>
[PROOF STATE]
proof (state)
this:
\<not> bval b s \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> bval b s \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
assume "bval b s"
[PROOF STATE]
proof (state)
this:
bval b s

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
with \<open>(?w, s) \<Rightarrow> t\<close>
[PROOF STATE]
proof (chain)
picking this:
(WHILE b DO c, s) \<Rightarrow> t
bval b s
[PROOF STEP]
obtain s' where
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
(WHILE b DO c, s) \<Rightarrow> t
bval b s

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>(c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
      \<comment> \<open>now we can build a derivation tree for the @{text IF}\<close>
      \<comment> \<open>first, the body of the True-branch:\<close>
[PROOF STATE]
proof (state)
this:
(c, s) \<Rightarrow> s'
(WHILE b DO c, s') \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
hence "(c;; ?w, s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
(c, s) \<Rightarrow> s'
(WHILE b DO c, s') \<Rightarrow> t

goal (1 subgoal):
 1. (c;; WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
by (rule Seq)
      \<comment> \<open>then the whole @{text IF}\<close>
[PROOF STATE]
proof (state)
this:
(c;; WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
with \<open>bval b s\<close>
[PROOF STATE]
proof (chain)
picking this:
bval b s
(c;; WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
have "(?iw, s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
bval b s
(c;; WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
[PROOF STEP]
by (rule IfTrue)
[PROOF STATE]
proof (state)
this:
(IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
bval b s \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
ultimately
    \<comment> \<open>both cases together give us what we want:\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> bval b s \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
bval b s \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
[PROOF STEP]
have "(?iw, s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
bval b s \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. (IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, ?s2) \<Rightarrow> ?t2 \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, ?s2) \<Rightarrow> ?t2

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
moreover
  \<comment> \<open>now the other direction:\<close>
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, ?s2) \<Rightarrow> ?t2 \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, ?s2) \<Rightarrow> ?t2

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, ?s2) \<Rightarrow> ?t2 \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, ?s2) \<Rightarrow> ?t2

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
fix s t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
assume "(?iw, s) \<Rightarrow> t"
    \<comment> \<open>again, if @{text b} is @{text False} in state @{text s}, then the False-branch\<close>
    \<comment> \<open>of the @{text IF} is executed, and both statements do nothing:\<close>
[PROOF STATE]
proof (state)
this:
(IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
assume "\<not>bval b s"
[PROOF STATE]
proof (state)
this:
\<not> bval b s

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
hence "s = t"
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s

goal (1 subgoal):
 1. s = t
[PROOF STEP]
using \<open>(?iw, s) \<Rightarrow> t\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s
(IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s = t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
hence "(?w, s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
s = t

goal (1 subgoal):
 1. (WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
using \<open>\<not>bval b s\<close>
[PROOF STATE]
proof (prove)
using this:
s = t
\<not> bval b s

goal (1 subgoal):
 1. (WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
moreover
    \<comment> \<open>on the other hand, if @{text b} is @{text True} in state @{text s},\<close>
    \<comment> \<open>then this time only the @{text IfTrue} rule can have be used\<close>
[PROOF STATE]
proof (state)
this:
\<not> bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
assume "bval b s"
[PROOF STATE]
proof (state)
this:
bval b s

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
with \<open>(?iw, s) \<Rightarrow> t\<close>
[PROOF STATE]
proof (chain)
picking this:
(IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
bval b s
[PROOF STEP]
have "(c;; ?w, s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
(IF b THEN c;; WHILE b DO c ELSE SKIP, s) \<Rightarrow> t
bval b s

goal (1 subgoal):
 1. (c;; WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
by auto
      \<comment> \<open>and for this, only the Seq-rule is applicable:\<close>
[PROOF STATE]
proof (state)
this:
(c;; WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c;; WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
obtain s' where
        "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
(c;; WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>(c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
      \<comment> \<open>with this information, we can build a derivation tree for the @{text WHILE}\<close>
[PROOF STATE]
proof (state)
this:
(c, s) \<Rightarrow> s'
(WHILE b DO c, s') \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
with \<open>bval b s\<close>
[PROOF STATE]
proof (chain)
picking this:
bval b s
(c, s) \<Rightarrow> s'
(WHILE b DO c, s') \<Rightarrow> t
[PROOF STEP]
have "(?w, s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
bval b s
(c, s) \<Rightarrow> s'
(WHILE b DO c, s') \<Rightarrow> t

goal (1 subgoal):
 1. (WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
by (rule WhileTrue)
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
ultimately
    \<comment> \<open>both cases together again give us what we want:\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> t
bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
have "(?w, s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> t
bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. (WHILE b DO c, s) \<Rightarrow> t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(IF b THEN c;; WHILE b DO c ELSE SKIP, ?s2) \<Rightarrow> ?t2 \<Longrightarrow> (WHILE b DO c, ?s2) \<Rightarrow> ?t2

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(WHILE b DO c, ?s2) \<Rightarrow> ?t2 \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, ?s2) \<Rightarrow> ?t2
(IF b THEN c;; WHILE b DO c ELSE SKIP, ?s2) \<Rightarrow> ?t2 \<Longrightarrow> (WHILE b DO c, ?s2) \<Rightarrow> ?t2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(WHILE b DO c, ?s2) \<Rightarrow> ?t2 \<Longrightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP, ?s2) \<Rightarrow> ?t2
(IF b THEN c;; WHILE b DO c ELSE SKIP, ?s2) \<Rightarrow> ?t2 \<Longrightarrow> (WHILE b DO c, ?s2) \<Rightarrow> ?t2

goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma while_unfold:
  "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILE b DO c \<sim> IF b THEN c;; WHILE b DO c ELSE SKIP
[PROOF STEP]
by blast


[STATEMENT]
lemma triv_if:
  "(IF b THEN c ELSE c) \<sim> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IF b THEN c ELSE c \<sim> c
[PROOF STEP]
by blast


[STATEMENT]
lemma commute_if:
  "(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2)
   \<sim>
   (IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IF b1 THEN IF b2 THEN c11 ELSE c12 ELSE c2 \<sim> IF b2 THEN IF b1 THEN c11 ELSE c2 ELSE IF b1 THEN c12 ELSE c2
[PROOF STEP]
by blast


[STATEMENT]
lemma sim_while_cong_aux:
  "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow> c \<sim> c' \<Longrightarrow>  (WHILE b DO c',s) \<Rightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(WHILE b DO c, s) \<Rightarrow> t; c \<sim> c'\<rbrakk> \<Longrightarrow> (WHILE b DO c', s) \<Rightarrow> t
[PROOF STEP]
apply(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b s c. \<lbrakk>\<not> bval b s; c \<sim> c'\<rbrakk> \<Longrightarrow> (WHILE b DO c', s) \<Rightarrow> s
 2. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>b ca. \<lbrakk>c = WHILE b DO ca; ca \<sim> c'\<rbrakk> \<Longrightarrow> (WHILE b DO c', s\<^sub>1) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; c \<sim> c' \<Longrightarrow> (WHILE b DO c', s\<^sub>2) \<Rightarrow> s\<^sub>3; c \<sim> c'\<rbrakk> \<Longrightarrow> (WHILE b DO c', s\<^sub>1) \<Rightarrow> s\<^sub>3
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>b ca. \<lbrakk>c = WHILE b DO ca; ca \<sim> c'\<rbrakk> \<Longrightarrow> (WHILE b DO c', s\<^sub>1) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; c \<sim> c' \<Longrightarrow> (WHILE b DO c', s\<^sub>2) \<Rightarrow> s\<^sub>3; c \<sim> c'\<rbrakk> \<Longrightarrow> (WHILE b DO c', s\<^sub>1) \<Rightarrow> s\<^sub>3
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_while_cong: "c \<sim> c' \<Longrightarrow> WHILE b DO c \<sim> WHILE b DO c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sim> c' \<Longrightarrow> WHILE b DO c \<sim> WHILE b DO c'
[PROOF STEP]
by (metis sim_while_cong_aux)


[STATEMENT]
lemma sim_refl:  "c \<sim> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sim> c
[PROOF STEP]
by simp


[STATEMENT]
lemma sim_sym:   "(c \<sim> c') = (c' \<sim> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c \<sim> c') = (c' \<sim> c)
[PROOF STEP]
by auto


[STATEMENT]
lemma sim_trans: "c \<sim> c' \<Longrightarrow> c' \<sim> c'' \<Longrightarrow> c \<sim> c''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<sim> c'; c' \<sim> c''\<rbrakk> \<Longrightarrow> c \<sim> c''
[PROOF STEP]
by auto


[STATEMENT]
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(c, s) \<Rightarrow> t; (c, s) \<Rightarrow> u\<rbrakk> \<Longrightarrow> u = t
[PROOF STEP]
by (induction arbitrary: u rule: big_step.induct) blast+


[STATEMENT]
lemma mIf_rule[sep_decon_rules]:
    "<P> do { bb \<leftarrow> b; if bb then t else e } <Q> \<Longrightarrow> <P> mIf b t e <Q>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <P> b \<bind> (\<lambda>bb. if bb then t else e) <Q> \<Longrightarrow> <P> if\<^sub>m b then t else e <Q>
[PROOF STEP]
unfolding mIf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <P> b \<bind> (\<lambda>bb. if bb then t else e) <Q> \<Longrightarrow> <P> b \<bind> (\<lambda>bb. if bb then t else e) <Q>
[PROOF STEP]
by simp


[STATEMENT]
lemma mmap_pure_aux:
    assumes "\<And>x. x\<in>set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up>(r = f x)>"
    shows "<P> mmap fi xs <\<lambda>ys. P * \<up>(ys = map f xs )>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> <P> fi ?x <\<lambda>r. P * \<up> (r = f ?x)>

goal (1 subgoal):
 1. <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi [] <\<lambda>ys. P * \<up> (ys = map f [])>
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>\<rbrakk> \<Longrightarrow> <P> mmap fi (a # xs) <\<lambda>ys. P * \<up> (ys = map f (a # xs))>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?x \<in> set [] \<Longrightarrow> <P> fi ?x <\<lambda>r. P * \<up> (r = f ?x)>

goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi [] <\<lambda>ys. P * \<up> (ys = map f [])>
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>\<rbrakk> \<Longrightarrow> <P> mmap fi (a # xs) <\<lambda>ys. P * \<up> (ys = map f (a # xs))>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set [] \<Longrightarrow> <P> fi ?x <\<lambda>r. P * \<up> (r = f ?x)>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x \<in> set [] \<Longrightarrow> <P> fi ?x <\<lambda>r. P * \<up> (r = f ?x)>

goal (1 subgoal):
 1. <P> mmap fi [] <\<lambda>ys. P * \<up> (ys = map f [])>
[PROOF STEP]
by sep_auto
[PROOF STATE]
proof (state)
this:
<P> mmap fi [] <\<lambda>ys. P * \<up> (ys = map f [])>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>\<rbrakk> \<Longrightarrow> <P> mmap fi (a # xs) <\<lambda>ys. P * \<up> (ys = map f (a # xs))>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>\<rbrakk> \<Longrightarrow> <P> mmap fi (a # xs) <\<lambda>ys. P * \<up> (ys = map f (a # xs))>
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>
?x \<in> set (a # xs) \<Longrightarrow> <P> fi ?x <\<lambda>r. P * \<up> (r = f ?x)>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>\<rbrakk> \<Longrightarrow> <P> mmap fi (a # xs) <\<lambda>ys. P * \<up> (ys = map f (a # xs))>
[PROOF STEP]
note [sep_heap_rules] = Cons
[PROOF STATE]
proof (state)
this:
(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>
?x \<in> set (a # xs) \<Longrightarrow> <P> fi ?x <\<lambda>r. P * \<up> (r = f ?x)>

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P * \<up> (ys = map f xs)>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> <P> fi x <\<lambda>r. P * \<up> (r = f x)>\<rbrakk> \<Longrightarrow> <P> mmap fi (a # xs) <\<lambda>ys. P * \<up> (ys = map f (a # xs))>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <P> mmap fi (a # xs) <\<lambda>ys. P * \<up> (ys = map f (a # xs))>
[PROOF STEP]
by sep_auto
[PROOF STATE]
proof (state)
this:
<P> mmap fi (a # xs) <\<lambda>ys. P * \<up> (ys = map f (a # xs))>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mmap_pres:
    assumes "\<And>x. x\<in>set xs \<Longrightarrow> <P> fi x <\<lambda>r. P>"
    shows "<P> mmap fi xs <\<lambda>ys. P >"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <P> mmap fi xs <\<lambda>ys. P>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> <P> fi ?x <\<lambda>r. P>

goal (1 subgoal):
 1. <P> mmap fi xs <\<lambda>ys. P>
[PROOF STEP]
apply(induction xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> <P> fi x <\<lambda>r. P>) \<Longrightarrow> <P> mmap fi [] <\<lambda>ys. P>
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> <P> fi x <\<lambda>r. P>) \<Longrightarrow> <P> mmap fi xs <\<lambda>ys. P>; \<And>x. x \<in> set (a # xs) \<Longrightarrow> <P> fi x <\<lambda>r. P>\<rbrakk> \<Longrightarrow> <P> mmap fi (a # xs) <\<lambda>ys. P>
[PROOF STEP]
apply sep_auto+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cond_TBOUND_mIf[cond_TBOUND]:
   assumes "\<section> P \<section> TBOUND cond b1"
    and    "\<And> h. \<section> Q (the_res cond h)\<section> TBOUND t b2"
    and    "\<And> h.\<section> Q (the_res cond h) \<section> TBOUND e b3"
    and    "<P> cond <Q>"
  shows    "\<section> P \<section> TBOUND (if\<^sub>m cond then t else e) (b1 + max b2 b3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<section> P \<section> TBOUND if\<^sub>m cond then t else e b1 + max b2 b3
[PROOF STEP]
unfolding mIf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<section> P \<section> TBOUND cond \<bind> (\<lambda>bb. if bb then t else e) b1 + max b2 b3
[PROOF STEP]
apply(rule cond_TBOUND_bind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<section> P \<section> TBOUND cond b1
 2. <P> cond <?Q>
 3. \<And>x h. x = the_res cond h \<Longrightarrow> \<section> ?Q x \<section> TBOUND if x then t else e max b2 b3
[PROOF STEP]
apply (rule assms)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h. x = the_res cond h \<Longrightarrow> \<section> Q x \<section> TBOUND if x then t else e max b2 b3
[PROOF STEP]
subgoal for x h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = the_res cond h \<Longrightarrow> \<section> Q x \<section> TBOUND if x then t else e max b2 b3
[PROOF STEP]
apply(auto split: if_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x; the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q True \<section> TBOUND t max b2 b3
 2. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q False \<section> TBOUND e max b2 b3
[PROOF STEP]
apply(rule cond_TBOUND_mono[where b = b2])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x; the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q True \<section> TBOUND t b2
 2. \<lbrakk>x; the_res cond h\<rbrakk> \<Longrightarrow> b2 \<le> max b2 b3
 3. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q False \<section> TBOUND e max b2 b3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<section> P \<section> TBOUND cond b1
\<section> Q (the_res cond ?h) \<section> TBOUND t b2
\<section> Q (the_res cond ?h) \<section> TBOUND e b3
<P> cond <Q>

goal (3 subgoals):
 1. \<lbrakk>x; the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q True \<section> TBOUND t b2
 2. \<lbrakk>x; the_res cond h\<rbrakk> \<Longrightarrow> b2 \<le> max b2 b3
 3. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q False \<section> TBOUND e max b2 b3
[PROOF STEP]
apply (metis (full_types))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x; the_res cond h\<rbrakk> \<Longrightarrow> b2 \<le> max b2 b3
 2. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q False \<section> TBOUND e max b2 b3
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q False \<section> TBOUND e max b2 b3
[PROOF STEP]
apply(rule cond_TBOUND_mono[where b = b3])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q False \<section> TBOUND e b3
 2. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> b3 \<le> max b2 b3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<section> P \<section> TBOUND cond b1
\<section> Q (the_res cond ?h) \<section> TBOUND t b2
\<section> Q (the_res cond ?h) \<section> TBOUND e b3
<P> cond <Q>

goal (2 subgoals):
 1. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> \<section> Q False \<section> TBOUND e b3
 2. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> b3 \<le> max b2 b3
[PROOF STEP]
apply (metis (full_types))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> x; \<not> the_res cond h\<rbrakk> \<Longrightarrow> b3 \<le> max b2 b3
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma admSI [intro]:
  "\<lbrakk> \<bottom> \<in> R; adm (\<lambda>x. x \<in> R) \<rbrakk> \<Longrightarrow> R \<in> admS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<bottom> \<in> R; adm (\<lambda>x. x \<in> R)\<rbrakk> \<Longrightarrow> R \<in> admS
[PROOF STEP]
unfolding admS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<bottom> \<in> R; adm (\<lambda>x. x \<in> R)\<rbrakk> \<Longrightarrow> R \<in> {R. \<bottom> \<in> R \<and> adm (\<lambda>x. x \<in> R)}
[PROOF STEP]
by simp


[STATEMENT]
lemma bottom_in_unlr [simp]:
  "\<bottom> \<in> unlr R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<in> unlr R
[PROOF STEP]
using admS.unlr [of R]
[PROOF STATE]
proof (prove)
using this:
unlr R \<in> {x. x \<in> admS}

goal (1 subgoal):
 1. \<bottom> \<in> unlr R
[PROOF STEP]
by (simp add: admS_def)


[STATEMENT]
lemma adm_unlr [simp]:
  "adm (\<lambda>x. x \<in> unlr R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> unlr R)
[PROOF STEP]
using admS.unlr [of R]
[PROOF STATE]
proof (prove)
using this:
unlr R \<in> {x. x \<in> admS}

goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> unlr R)
[PROOF STEP]
by (simp add: admS_def)


[STATEMENT]
lemma adm_cont_unlr [intro, simp]:
  "cont f \<Longrightarrow> adm (\<lambda>x. f x \<in> unlr r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont f \<Longrightarrow> adm (\<lambda>x. f x \<in> unlr r)
[PROOF STEP]
by (erule adm_subst) simp


[STATEMENT]
lemma mklr_leq [iff]: "\<lbrakk> x \<in> admS; y \<in> admS \<rbrakk> \<Longrightarrow> (mklr x \<le> mklr y) \<longleftrightarrow> (x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> admS; y \<in> admS\<rbrakk> \<Longrightarrow> (mklr x \<le> mklr y) = (x \<subseteq> y)
[PROOF STEP]
unfolding less_eq_admS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> admS; y \<in> admS\<rbrakk> \<Longrightarrow> (unlr (mklr x) \<subseteq> unlr (mklr y)) = (x \<subseteq> y)
[PROOF STEP]
by simp


[STATEMENT]
lemma unlr_leq: "(unlr x \<le> unlr y) \<longleftrightarrow> (x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (unlr x \<subseteq> unlr y) = (x \<le> y)
[PROOF STEP]
unfolding less_eq_admS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (unlr x \<subseteq> unlr y) = (unlr x \<subseteq> unlr y)
[PROOF STEP]
by simp


[STATEMENT]
lemma unlr_inf: "unlr (inf x y) = unlr x \<inter> unlr y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unlr (inf x y) = unlr x \<inter> unlr y
[PROOF STEP]
unfolding inf_admS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unlr (mklr (unlr x \<inter> unlr y)) = unlr x \<inter> unlr y
[PROOF STEP]
by (simp add: admS_def)


[STATEMENT]
lemma unlr_sup: "unlr (sup x y) = unlr x \<union> unlr y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unlr (sup x y) = unlr x \<union> unlr y
[PROOF STEP]
unfolding sup_admS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unlr (mklr (unlr x \<union> unlr y)) = unlr x \<union> unlr y
[PROOF STEP]
by (simp add: admS_def)


[STATEMENT]
lemma unlr_bot[simp]:
  "unlr bot = {\<bottom>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unlr bot = {\<bottom>}
[PROOF STEP]
by (simp add: admS_def bot_admS_def)


[STATEMENT]
lemma mklr_Inf: "unlr (Inf A) = Inf (unlr ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unlr (Inf A) = \<Inter> (unlr ` A)
[PROOF STEP]
unfolding Inf_admS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unlr (mklr (\<Inter> (unlr ` A))) = \<Inter> (unlr ` A)
[PROOF STEP]
by (simp add: admS_def)


[STATEMENT]
lemma INT_admS_bot [simp]:
  "(\<Inter>R. unlr R) = {\<bottom>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter> (range unlr) = {\<bottom>}
[PROOF STEP]
by (auto, metis singletonE unlr_bot)


[STATEMENT]
lemma sym_lr_mono:
  "mono sym_lr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono sym_lr
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> sym_lr x \<le> sym_lr y
[PROOF STEP]
fix x y :: "'a dual \<times> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> sym_lr x \<le> sym_lr y
[PROOF STEP]
obtain x1 x2 y1 y2 where [simp]: "x = (x1, x2)" "y = (y1, y2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 y1 y2. \<lbrakk>x = (x1, x2); y = (y1, y2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases x, cases y)
[PROOF STATE]
proof (state)
this:
x = (x1, x2)
y = (y1, y2)

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> sym_lr x \<le> sym_lr y
[PROOF STEP]
assume "x \<le> y"
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> sym_lr x \<le> sym_lr y
[PROOF STEP]
with monoF
[PROOF STATE]
proof (chain)
picking this:
mono F
x \<le> y
[PROOF STEP]
have "F x \<le> F y"
[PROOF STATE]
proof (prove)
using this:
mono F
x \<le> y

goal (1 subgoal):
 1. F x \<le> F y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
F x \<le> F y

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> sym_lr x \<le> sym_lr y
[PROOF STEP]
from \<open>x \<le> y\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<le> y
[PROOF STEP]
have "(dual y2, undual y1) \<le> (dual x2, undual x1)"
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. (dual y2, undual y1) \<le> (dual x2, undual x1)
[PROOF STEP]
by (simp_all add: dual_less_eq_iff)
[PROOF STATE]
proof (state)
this:
(dual y2, undual y1) \<le> (dual x2, undual x1)

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> sym_lr x \<le> sym_lr y
[PROOF STEP]
with monoF
[PROOF STATE]
proof (chain)
picking this:
mono F
(dual y2, undual y1) \<le> (dual x2, undual x1)
[PROOF STEP]
have "F (dual y2, undual y1) \<le> F (dual x2, undual x1)"
[PROOF STATE]
proof (prove)
using this:
mono F
(dual y2, undual y1) \<le> (dual x2, undual x1)

goal (1 subgoal):
 1. F (dual y2, undual y1) \<le> F (dual x2, undual x1)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
F (dual y2, undual y1) \<le> F (dual x2, undual x1)

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> sym_lr x \<le> sym_lr y
[PROOF STEP]
with \<open>F x \<le> F y\<close>
[PROOF STATE]
proof (chain)
picking this:
F x \<le> F y
F (dual y2, undual y1) \<le> F (dual x2, undual x1)
[PROOF STEP]
show "sym_lr x \<le> sym_lr y"
[PROOF STATE]
proof (prove)
using this:
F x \<le> F y
F (dual y2, undual y1) \<le> F (dual x2, undual x1)

goal (1 subgoal):
 1. sym_lr x \<le> sym_lr y
[PROOF STEP]
by (simp add: sym_lr_def)
[PROOF STATE]
proof (state)
this:
sym_lr x \<le> sym_lr y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delta:
  "(delta_neg, delta_pos) = f_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (delta_neg, delta_pos) = f_lim
[PROOF STEP]
by (simp add: delta_neg_def delta_pos_def)


[STATEMENT]
lemma delta_neg_sol:
  "delta_neg = dual (F (dual delta_pos, undual delta_neg))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_neg = dual (F (dual delta_pos, undual delta_neg))
[PROOF STEP]
by (metis (no_types, lifting) case_prod_unfold delta_neg_def delta_pos_def fst_conv lfp_unfold sym_lr_def sym_lr_mono)


[STATEMENT]
lemma delta_pos_sol:
  "delta_pos = F (delta_neg, delta_pos)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos = F (delta_neg, delta_pos)
[PROOF STEP]
by (metis (no_types, lifting) case_prod_conv delta lfp_unfold snd_conv sym_lr_def sym_lr_mono)


[STATEMENT]
lemma delta_pos_neg_least:
  assumes rm: "rm \<le> F (dual rp, rm)"
  assumes rp: "F (dual rm, rp) \<le> rp"
  shows "delta_neg \<le> dual rm"
    and "delta_pos \<le> rp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_neg \<le> dual rm &&& delta_pos \<le> rp
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. delta_neg \<le> dual rm
 2. delta_pos \<le> rp
[PROOF STEP]
from rm rp
[PROOF STATE]
proof (chain)
picking this:
rm \<le> F (dual rp, rm)
F (dual rm, rp) \<le> rp
[PROOF STEP]
have "(delta_neg, delta_pos) \<le> (dual rm, rp)"
[PROOF STATE]
proof (prove)
using this:
rm \<le> F (dual rp, rm)
F (dual rm, rp) \<le> rp

goal (1 subgoal):
 1. (delta_neg, delta_pos) \<le> (dual rm, rp)
[PROOF STEP]
by (simp add: delta lfp_lowerbound sym_lr_def)
[PROOF STATE]
proof (state)
this:
(delta_neg, delta_pos) \<le> (dual rm, rp)

goal (2 subgoals):
 1. delta_neg \<le> dual rm
 2. delta_pos \<le> rp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(delta_neg, delta_pos) \<le> (dual rm, rp)
[PROOF STEP]
show "delta_neg \<le> dual rm" and "delta_pos \<le> rp"
[PROOF STATE]
proof (prove)
using this:
(delta_neg, delta_pos) \<le> (dual rm, rp)

goal (1 subgoal):
 1. delta_neg \<le> dual rm &&& delta_pos \<le> rp
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
delta_neg \<le> dual rm
delta_pos \<le> rp

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delta_eq:
  "undual delta_neg = delta_pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. undual delta_neg = delta_pos
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. undual delta_neg \<le> delta_pos
 2. delta_pos \<le> undual delta_neg
[PROOF STEP]
show "delta_pos \<le> undual delta_neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos \<le> undual delta_neg
[PROOF STEP]
by (metis delta_neg_sol delta_pos_neg_least(2) delta_pos_sol order_refl undual_dual)
[PROOF STATE]
proof (state)
this:
delta_pos \<le> undual delta_neg

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
let ?P = "\<lambda>x. eRSV x (delta_neg) (delta_pos)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
have "?P (fix\<cdot>\<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eRSV (fix\<cdot>\<delta>) delta_neg delta_pos
[PROOF STEP]
by (rule fix_ind, simp_all add: inst_fun_pcpo[symmetric])
       (metis delta_neg_sol delta_pos_sol eRSV_deltaF)
[PROOF STATE]
proof (state)
this:
eRSV (fix\<cdot>\<delta>) delta_neg delta_pos

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
with min_inv_ID
[PROOF STATE]
proof (chain)
picking this:
fix\<cdot>\<delta> = ID
eRSV (fix\<cdot>\<delta>) delta_neg delta_pos
[PROOF STEP]
show "undual delta_neg \<le> delta_pos"
[PROOF STATE]
proof (prove)
using this:
fix\<cdot>\<delta> = ID
eRSV (fix\<cdot>\<delta>) delta_neg delta_pos

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
by (fastforce simp: unlr_leq[symmetric])
[PROOF STATE]
proof (state)
this:
undual delta_neg \<le> delta_pos

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delta_sol: "delta = F (dual delta, delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta = F (dual delta, delta)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta = F (dual delta, delta)
[PROOF STEP]
unfolding delta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos = F (dual delta_pos, delta_pos)
[PROOF STEP]
by (subst delta_eq[symmetric], simp, rule delta_pos_sol)


[STATEMENT]
lemma synlrI [intro]:
  "\<lbrakk> \<And>a. (\<bottom>, a) \<in> R; \<And>a. adm (\<lambda>x. (x, a) \<in> R) \<rbrakk> \<Longrightarrow> R \<in> synlr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. (\<bottom>, a) \<in> R; \<And>a. adm (\<lambda>x. (x, a) \<in> R)\<rbrakk> \<Longrightarrow> R \<in> synlr
[PROOF STEP]
unfolding synlr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. (\<bottom>, a) \<in> R; \<And>a. adm (\<lambda>x. (x, a) \<in> R)\<rbrakk> \<Longrightarrow> R \<in> {R. \<forall>a. {d. (d, a) \<in> R} \<in> admS}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma bottom_in_unsynlr [simp]:
  "(\<bottom>, a) \<in> unsynlr R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bottom>, a) \<in> unsynlr R
[PROOF STEP]
using synlr.unsynlr [of R]
[PROOF STATE]
proof (prove)
using this:
unsynlr R \<in> {x. x \<in> synlr}

goal (1 subgoal):
 1. (\<bottom>, a) \<in> unsynlr R
[PROOF STEP]
by (simp add: synlr_def admS_def)


[STATEMENT]
lemma adm_unsynlr [simp]:
  "adm (\<lambda>x. (x, a) \<in> unsynlr R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. (x, a) \<in> unsynlr R)
[PROOF STEP]
using synlr.unsynlr[of R]
[PROOF STATE]
proof (prove)
using this:
unsynlr R \<in> {x. x \<in> synlr}

goal (1 subgoal):
 1. adm (\<lambda>x. (x, a) \<in> unsynlr R)
[PROOF STEP]
by (simp add: synlr_def admS_def)


[STATEMENT]
lemma adm_cont_unsynlr [intro, simp]:
  "cont f \<Longrightarrow> adm (\<lambda>x. (f x, a) \<in> unsynlr r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont f \<Longrightarrow> adm (\<lambda>x. (f x, a) \<in> unsynlr r)
[PROOF STEP]
by (erule adm_subst) simp


[STATEMENT]
lemma mksynlr_leq [iff]: "\<lbrakk> x \<in> synlr; y \<in> synlr \<rbrakk> \<Longrightarrow> (mksynlr x \<le> mksynlr y) \<longleftrightarrow> (x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> synlr; y \<in> synlr\<rbrakk> \<Longrightarrow> (mksynlr x \<le> mksynlr y) = (x \<subseteq> y)
[PROOF STEP]
unfolding less_eq_synlr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> synlr; y \<in> synlr\<rbrakk> \<Longrightarrow> (unsynlr (mksynlr x) \<subseteq> unsynlr (mksynlr y)) = (x \<subseteq> y)
[PROOF STEP]
by simp


[STATEMENT]
lemma unsynlr_leq: "(unsynlr x \<le> unsynlr y) \<longleftrightarrow> (x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (unsynlr x \<subseteq> unsynlr y) = (x \<le> y)
[PROOF STEP]
unfolding less_eq_synlr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (unsynlr x \<subseteq> unsynlr y) = (unsynlr x \<subseteq> unsynlr y)
[PROOF STEP]
by simp


[STATEMENT]
lemma unsynlr_inf: "unsynlr (inf x y) = unsynlr x \<inter> unsynlr y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unsynlr (inf x y) = unsynlr x \<inter> unsynlr y
[PROOF STEP]
unfolding inf_synlr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unsynlr (mksynlr (unsynlr x \<inter> unsynlr y)) = unsynlr x \<inter> unsynlr y
[PROOF STEP]
by (simp add: admS_def synlr_def)


[STATEMENT]
lemma unsynlr_sup: "unsynlr (sup x y) = unsynlr x \<union> unsynlr y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unsynlr (sup x y) = unsynlr x \<union> unsynlr y
[PROOF STEP]
unfolding sup_synlr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unsynlr (mksynlr (unsynlr x \<union> unsynlr y)) = unsynlr x \<union> unsynlr y
[PROOF STEP]
by (simp add: admS_def synlr_def)


[STATEMENT]
lemma unsynlr_bot[simp]:
  "unsynlr bot = {\<bottom>} \<times> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unsynlr bot = {\<bottom>} \<times> UNIV
[PROOF STEP]
by (simp add: admS_def synlr_def bot_synlr_def)


[STATEMENT]
lemma mksynlr_Inf: "unsynlr (Inf A) = Inf (unsynlr ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unsynlr (Inf A) = \<Inter> (unsynlr ` A)
[PROOF STEP]
unfolding Inf_synlr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unsynlr (mksynlr (\<Inter> (unsynlr ` A))) = \<Inter> (unsynlr ` A)
[PROOF STEP]
by (simp add: admS_def synlr_def)


[STATEMENT]
lemma INT_synlr_bot [simp]:
  "(\<Inter>R. unsynlr R) = {\<bottom>} \<times> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter> (range unsynlr) = {\<bottom>} \<times> UNIV
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<forall>x. (a, b) \<in> unsynlr x \<Longrightarrow> a = \<bottom>
[PROOF STEP]
apply (drule spec[of _ "mksynlr ({\<bottom>} \<times> UNIV)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> unsynlr (mksynlr ({\<bottom>} \<times> UNIV)) \<Longrightarrow> a = \<bottom>
[PROOF STEP]
apply (metis bot_synlr_def mem_Sigma_iff singletonE unsynlr_bot)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma delta:
  "(delta_neg, delta_pos) = f_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (delta_neg, delta_pos) = f_lim
[PROOF STEP]
by (simp add: delta_neg_def delta_pos_def)


[STATEMENT]
lemma delta_neg_sol:
  "delta_neg = dual (F (dual delta_pos, undual delta_neg))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_neg = dual (F (dual delta_pos, undual delta_neg))
[PROOF STEP]
by (metis (no_types, lifting) case_prod_unfold delta_neg_def delta_pos_def fst_conv lfp_unfold sym_lr_def sym_lr_mono)


[STATEMENT]
lemma delta_pos_sol:
  "delta_pos = F (delta_neg, delta_pos)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos = F (delta_neg, delta_pos)
[PROOF STEP]
by (metis (no_types, lifting) case_prod_conv delta lfp_unfold snd_conv sym_lr_def sym_lr_mono)


[STATEMENT]
lemma delta_pos_neg_least:
  assumes rm: "rm \<le> F (dual rp, rm)"
  assumes rp: "F (dual rm, rp) \<le> rp"
  shows "delta_neg \<le> dual rm"
    and "delta_pos \<le> rp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_neg \<le> dual rm &&& delta_pos \<le> rp
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. delta_neg \<le> dual rm
 2. delta_pos \<le> rp
[PROOF STEP]
from rm rp
[PROOF STATE]
proof (chain)
picking this:
rm \<le> F (dual rp, rm)
F (dual rm, rp) \<le> rp
[PROOF STEP]
have "(delta_neg, delta_pos) \<le> (dual rm, rp)"
[PROOF STATE]
proof (prove)
using this:
rm \<le> F (dual rp, rm)
F (dual rm, rp) \<le> rp

goal (1 subgoal):
 1. (delta_neg, delta_pos) \<le> (dual rm, rp)
[PROOF STEP]
by (simp add: delta lfp_lowerbound sym_lr_def)
[PROOF STATE]
proof (state)
this:
(delta_neg, delta_pos) \<le> (dual rm, rp)

goal (2 subgoals):
 1. delta_neg \<le> dual rm
 2. delta_pos \<le> rp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(delta_neg, delta_pos) \<le> (dual rm, rp)
[PROOF STEP]
show "delta_neg \<le> dual rm" and "delta_pos \<le> rp"
[PROOF STATE]
proof (prove)
using this:
(delta_neg, delta_pos) \<le> (dual rm, rp)

goal (1 subgoal):
 1. delta_neg \<le> dual rm &&& delta_pos \<le> rp
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
delta_neg \<le> dual rm
delta_pos \<le> rp

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delta_eq:
  "undual delta_neg = delta_pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. undual delta_neg = delta_pos
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. undual delta_neg \<le> delta_pos
 2. delta_pos \<le> undual delta_neg
[PROOF STEP]
show "delta_pos \<le> undual delta_neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos \<le> undual delta_neg
[PROOF STEP]
by (metis delta_neg_sol delta_pos_neg_least(2) delta_pos_sol order_refl undual_dual)
[PROOF STATE]
proof (state)
this:
delta_pos \<le> undual delta_neg

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
let ?P = "\<lambda>x. x\<cdot>\<bottom> = \<bottom> \<and> eRSS x (delta_neg) (delta_pos)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
have "?P (fix\<cdot>\<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>\<delta>\<cdot>\<bottom> = \<bottom> \<and> eRSS (fix\<cdot>\<delta>) delta_neg delta_pos
[PROOF STEP]
by (rule fix_ind, simp_all)
       (metis delta_neg_sol delta_pos_sol eRS_deltaF min_inv_strict)
[PROOF STATE]
proof (state)
this:
fix\<cdot>\<delta>\<cdot>\<bottom> = \<bottom> \<and> eRSS (fix\<cdot>\<delta>) delta_neg delta_pos

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
with min_inv_ID
[PROOF STATE]
proof (chain)
picking this:
fix\<cdot>\<delta> = ID
fix\<cdot>\<delta>\<cdot>\<bottom> = \<bottom> \<and> eRSS (fix\<cdot>\<delta>) delta_neg delta_pos
[PROOF STEP]
show "undual delta_neg \<le> delta_pos"
[PROOF STATE]
proof (prove)
using this:
fix\<cdot>\<delta> = ID
fix\<cdot>\<delta>\<cdot>\<bottom> = \<bottom> \<and> eRSS (fix\<cdot>\<delta>) delta_neg delta_pos

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
by (fastforce simp: unsynlr_leq[symmetric])
[PROOF STATE]
proof (state)
this:
undual delta_neg \<le> delta_pos

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delta_sol:
  "delta = F (dual delta, delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta = F (dual delta, delta)
[PROOF STEP]
unfolding delta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos = F (dual delta_pos, delta_pos)
[PROOF STEP]
by (subst delta_eq[symmetric], simp, rule delta_pos_sol)


[STATEMENT]
lemma delta_unique:
  assumes r: "F (dual r, r) = r"
  shows "r = delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = delta
[PROOF STEP]
unfolding delta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = delta_pos
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<le> delta_pos
 2. delta_pos \<le> r
[PROOF STEP]
show "delta_pos \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos \<le> r
[PROOF STEP]
using assms delta_pos_neg_least[where rm=r and rp=r]
[PROOF STATE]
proof (prove)
using this:
F (dual r, r) = r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_neg \<le> dual r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_pos \<le> r

goal (1 subgoal):
 1. delta_pos \<le> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
delta_pos \<le> r

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
have "delta_neg \<le> dual r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_neg \<le> dual r
[PROOF STEP]
using assms delta_pos_neg_least[where rm=r and rp=r]
[PROOF STATE]
proof (prove)
using this:
F (dual r, r) = r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_neg \<le> dual r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_pos \<le> r

goal (1 subgoal):
 1. delta_neg \<le> dual r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
delta_neg \<le> dual r

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
delta_neg \<le> dual r
[PROOF STEP]
have "r \<le> undual delta_neg"
[PROOF STATE]
proof (prove)
using this:
delta_neg \<le> dual r

goal (1 subgoal):
 1. r \<le> undual delta_neg
[PROOF STEP]
by (simp add: less_eq_dual_def)
[PROOF STATE]
proof (state)
this:
r \<le> undual delta_neg

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<le> undual delta_neg
[PROOF STEP]
show "r \<le> delta_pos"
[PROOF STATE]
proof (prove)
using this:
r \<le> undual delta_neg

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
using delta_eq
[PROOF STATE]
proof (prove)
using this:
r \<le> undual delta_neg
undual delta_neg = delta_pos

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<le> delta_pos

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delta_eq:
  "undual delta_neg = delta_pos"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. undual delta_neg = delta_pos
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. undual delta_neg \<le> delta_pos
 2. delta_pos \<le> undual delta_neg
[PROOF STEP]
show "delta_pos \<le> undual delta_neg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos \<le> undual delta_neg
[PROOF STEP]
by (metis delta_neg_sol delta_pos_neg_least(2) delta_pos_sol order_refl undual_dual)
[PROOF STATE]
proof (state)
this:
delta_pos \<le> undual delta_neg

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
let ?P = "\<lambda>(ea, eb). eRSP ea eb (delta_neg) (delta_pos) \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
have "?P (fix\<cdot>ad, fix\<cdot>bd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case (fix\<cdot>ad, fix\<cdot>bd) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
apply (rule parallel_fix_ind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. adm (\<lambda>x. case (fst x, snd x) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>)
 2. case (\<bottom>, \<bottom>) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>
 3. \<And>x y. case (x, y) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom> \<Longrightarrow> case (ad\<cdot>x, bd\<cdot>y) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. (\<forall>xa\<in>unlr (fst (undual delta_neg)). case xa of (am, bm) \<Rightarrow> (fst x\<cdot>am, fst y\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>xa\<in>unlr (snd (undual delta_neg)). case xa of (av, bv) \<Rightarrow> (snd x\<cdot>av, snd y\<cdot>bv) \<in> unlr (snd delta_pos)) \<and> fst x\<cdot>\<bottom> = \<bottom> \<and> snd x\<cdot>\<bottom> = \<bottom> \<and> fst y\<cdot>\<bottom> = \<bottom> \<and> snd y\<cdot>\<bottom> = \<bottom> \<Longrightarrow> (\<forall>xa\<in>unlr (fst (undual delta_neg)). case xa of (am, bm) \<Rightarrow> (fst (ad\<cdot>x)\<cdot>am, fst (bd\<cdot>y)\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>xa\<in>unlr (snd (undual delta_neg)). case xa of (av, bv) \<Rightarrow> (snd (ad\<cdot>x)\<cdot>av, snd (bd\<cdot>y)\<cdot>bv) \<in> unlr (snd delta_pos)) \<and> fst (ad\<cdot>x)\<cdot>\<bottom> = \<bottom> \<and> snd (ad\<cdot>x)\<cdot>\<bottom> = \<bottom> \<and> fst (bd\<cdot>y)\<cdot>\<bottom> = \<bottom> \<and> snd (bd\<cdot>y)\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
using ad_strict bd_strict
[PROOF STATE]
proof (prove)
using this:
fst (ad\<cdot>?r)\<cdot>\<bottom> = \<bottom>
snd (ad\<cdot>?r)\<cdot>\<bottom> = \<bottom>
fst (bd\<cdot>?r)\<cdot>\<bottom> = \<bottom>
snd (bd\<cdot>?r)\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. \<And>x y. (\<forall>xa\<in>unlr (fst (undual delta_neg)). case xa of (am, bm) \<Rightarrow> (fst x\<cdot>am, fst y\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>xa\<in>unlr (snd (undual delta_neg)). case xa of (av, bv) \<Rightarrow> (snd x\<cdot>av, snd y\<cdot>bv) \<in> unlr (snd delta_pos)) \<and> fst x\<cdot>\<bottom> = \<bottom> \<and> snd x\<cdot>\<bottom> = \<bottom> \<and> fst y\<cdot>\<bottom> = \<bottom> \<and> snd y\<cdot>\<bottom> = \<bottom> \<Longrightarrow> (\<forall>xa\<in>unlr (fst (undual delta_neg)). case xa of (am, bm) \<Rightarrow> (fst (ad\<cdot>x)\<cdot>am, fst (bd\<cdot>y)\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>xa\<in>unlr (snd (undual delta_neg)). case xa of (av, bv) \<Rightarrow> (snd (ad\<cdot>x)\<cdot>av, snd (bd\<cdot>y)\<cdot>bv) \<in> unlr (snd delta_pos)) \<and> fst (ad\<cdot>x)\<cdot>\<bottom> = \<bottom> \<and> snd (ad\<cdot>x)\<cdot>\<bottom> = \<bottom> \<and> fst (bd\<cdot>y)\<cdot>\<bottom> = \<bottom> \<and> snd (bd\<cdot>y)\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> eRSP (ad\<cdot>(a, b)) (bd\<cdot>(aa, ba)) delta_neg delta_pos
[PROOF STEP]
apply (cut_tac ea="(a, b)" and eb="(aa, ba)" in eRSP_deltaF[where R=delta_neg and S=delta_pos])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> eRSP (a, b) (aa, ba) delta_neg delta_pos
 2. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> fst (a, b)\<cdot>\<bottom> = \<bottom>
 3. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> snd (a, b)\<cdot>\<bottom> = \<bottom>
 4. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> fst (aa, ba)\<cdot>\<bottom> = \<bottom>
 5. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> snd (a, b)\<cdot>\<bottom> = \<bottom>
 6. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>; eRSP (ad\<cdot>(a, b)) (bd\<cdot>(aa, ba)) (dual (F (dual delta_pos, undual delta_neg))) (F (delta_neg, delta_pos))\<rbrakk> \<Longrightarrow> eRSP (ad\<cdot>(a, b)) (bd\<cdot>(aa, ba)) delta_neg delta_pos
[PROOF STEP]
apply (simp_all add: delta_pos_sol[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>; (\<forall>x\<in>unlr (fst (F (dual delta_pos, undual delta_neg))). case x of (am, bm) \<Rightarrow> (fst (ad\<cdot>(a, b))\<cdot>am, fst (bd\<cdot>(aa, ba))\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>x\<in>unlr (snd (F (dual delta_pos, undual delta_neg))). case x of (av, bv) \<Rightarrow> (snd (ad\<cdot>(a, b))\<cdot>av, snd (bd\<cdot>(aa, ba))\<cdot>bv) \<in> unlr (snd delta_pos))\<rbrakk> \<Longrightarrow> eRSP (ad\<cdot>(a, b)) (bd\<cdot>(aa, ba)) delta_neg delta_pos
[PROOF STEP]
apply (subst delta_neg_sol)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>; (\<forall>x\<in>unlr (fst (F (dual delta_pos, undual delta_neg))). case x of (am, bm) \<Rightarrow> (fst (ad\<cdot>(a, b))\<cdot>am, fst (bd\<cdot>(aa, ba))\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>x\<in>unlr (snd (F (dual delta_pos, undual delta_neg))). case x of (av, bv) \<Rightarrow> (snd (ad\<cdot>(a, b))\<cdot>av, snd (bd\<cdot>(aa, ba))\<cdot>bv) \<in> unlr (snd delta_pos))\<rbrakk> \<Longrightarrow> (\<forall>(am, bm)\<in>unlr (fst (undual (dual (F (dual delta_pos, undual delta_neg))))). (fst (ad\<cdot>(a, b))\<cdot>am, fst (bd\<cdot>(aa, ba))\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>(av, bv)\<in>unlr (snd (undual delta_neg)). (snd (ad\<cdot>(a, b))\<cdot>av, snd (bd\<cdot>(aa, ba))\<cdot>bv) \<in> unlr (snd delta_pos))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>; (\<forall>x\<in>unlr (fst (F (dual delta_pos, undual delta_neg))). case x of (am, bm) \<Rightarrow> (fst (ad\<cdot>(a, b))\<cdot>am, fst (bd\<cdot>(aa, ba))\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>x\<in>unlr (snd (F (dual delta_pos, undual delta_neg))). case x of (av, bv) \<Rightarrow> (snd (ad\<cdot>(a, b))\<cdot>av, snd (bd\<cdot>(aa, ba))\<cdot>bv) \<in> unlr (snd delta_pos))\<rbrakk> \<Longrightarrow> \<forall>(av, bv)\<in>unlr (snd (undual delta_neg)). (snd (ad\<cdot>(a, b))\<cdot>av, snd (bd\<cdot>(aa, ba))\<cdot>bv) \<in> unlr (snd delta_pos)
[PROOF STEP]
apply (subst delta_neg_sol)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<And>a b. fst (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (ad\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. fst (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<And>a b. snd (bd\<cdot>(a, b))\<cdot>\<bottom> = \<bottom>; \<forall>x\<in>unlr (fst (undual delta_neg)). case x of (am, bm) \<Rightarrow> (a\<cdot>am, aa\<cdot>bm) \<in> unlr (fst delta_pos); \<forall>x\<in>unlr (snd (undual delta_neg)). case x of (av, bv) \<Rightarrow> (b\<cdot>av, ba\<cdot>bv) \<in> unlr (snd delta_pos); a\<cdot>\<bottom> = \<bottom>; b\<cdot>\<bottom> = \<bottom>; aa\<cdot>\<bottom> = \<bottom>; ba\<cdot>\<bottom> = \<bottom>; (\<forall>x\<in>unlr (fst (F (dual delta_pos, undual delta_neg))). case x of (am, bm) \<Rightarrow> (fst (ad\<cdot>(a, b))\<cdot>am, fst (bd\<cdot>(aa, ba))\<cdot>bm) \<in> unlr (fst delta_pos)) \<and> (\<forall>x\<in>unlr (snd (F (dual delta_pos, undual delta_neg))). case x of (av, bv) \<Rightarrow> (snd (ad\<cdot>(a, b))\<cdot>av, snd (bd\<cdot>(aa, ba))\<cdot>bv) \<in> unlr (snd delta_pos))\<rbrakk> \<Longrightarrow> \<forall>(av, bv)\<in>unlr (snd (undual (dual (F (dual delta_pos, undual delta_neg))))). (snd (ad\<cdot>(a, b))\<cdot>av, snd (bd\<cdot>(aa, ba))\<cdot>bv) \<in> unlr (snd delta_pos)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
case (fix\<cdot>ad, fix\<cdot>bd) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
case (fix\<cdot>ad, fix\<cdot>bd) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
have "?P ((ID, ID), (ID, ID))"
[PROOF STATE]
proof (prove)
using this:
case (fix\<cdot>ad, fix\<cdot>bd) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. case ((ID, ID), ID, ID) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (simp only: ad_ID bd_ID)
[PROOF STATE]
proof (state)
this:
case ((ID, ID), ID, ID) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
case ((ID, ID), ID, ID) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
show "undual delta_neg \<le> delta_pos"
[PROOF STATE]
proof (prove)
using this:
case ((ID, ID), ID, ID) of (ea, eb) \<Rightarrow> eRSP ea eb delta_neg delta_pos \<and> fst ea\<cdot>\<bottom> = \<bottom> \<and> snd ea\<cdot>\<bottom> = \<bottom> \<and> fst eb\<cdot>\<bottom> = \<bottom> \<and> snd eb\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. undual delta_neg \<le> delta_pos
[PROOF STEP]
by (fastforce simp: unlr_leq[symmetric] less_eq_prod_def)
[PROOF STATE]
proof (state)
this:
undual delta_neg \<le> delta_pos

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachNT_non_isRevNth:
assumes "reachNT s" and "uid \<in> UIDs"
shows "\<not> isRevNth s cid uid PID N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rev PID N \<notin> set (roles s cid uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachNT s
uid \<in> UIDs

goal (1 subgoal):
 1. Rev PID N \<notin> set (roles s cid uid)
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. uid \<in> UIDs \<Longrightarrow> Rev PID N \<notin> set (roles istate cid uid)
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> Rev PID N \<notin> set (roles (srcOf trn) cid uid); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> Rev PID N \<notin> set (roles (tgtOf trn) cid uid)
[PROOF STEP]
apply (auto simp: istate_def)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> Rev PID N \<notin> set (roles (srcOf trn) cid uid); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> Rev PID N \<notin> set (roles (tgtOf trn) cid uid)
[PROOF STEP]
subgoal for trn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> Rev PID N \<notin> set (roles (srcOf trn) cid uid); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> Rev PID N \<notin> set (roles (tgtOf trn) cid uid)
[PROOF STEP]
apply(cases trn, auto simp: T.simps reachNT_reach isREVNth_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma P_\<phi>_\<gamma>:
assumes 1: "reachNT s" and 2: "step s a = (ou,s')" "\<phi> (Trans s a ou s')"
shows "\<not> \<gamma> (Trans s a ou s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
using reachNT_non_isRevNth[OF 1] 2
[PROOF STATE]
proof (prove)
using this:
?uid \<in> UIDs \<Longrightarrow> Rev PID N \<notin> set (roles s ?cid ?uid)
step s a = (ou, s')
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
unfolding T.simps \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
?uid \<in> UIDs \<Longrightarrow> Rev PID N \<notin> set (roles s ?cid ?uid)
step s a = (ou, s')
ou = outOK \<and> (\<exists>cid uid p rc. a = Uact (uReview cid uid p PID N rc) \<or> a = UUact (uuReview cid uid p PID N rc))

goal (1 subgoal):
 1. \<not> \<gamma> (Trans s a ou s')
[PROOF STEP]
apply (auto simp add: u_defs uu_defs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cid uid aa aaa b x1 x2 x3 x4 x5 x6. \<lbrakk>ou = outOK; uid \<in> UIDs; a = Uact (uReview cid uid (pass s uid) PID N (aa, aaa, b)); \<And>uid cid. uid \<in> UIDs \<Longrightarrow> Rev PID N \<notin> set (roles s cid uid); cid \<in>\<in> confIDs s; uid \<in>\<in> userIDs s; PID \<in>\<in> paperIDs s cid; phase s cid = revPH; isRev s cid uid PID; getReviewIndex s cid uid PID = N; paper s PID = Paper x1 x2 x3 x4 x5 x6; s' = s\<lparr>paper := (paper s)(PID := Paper x1 x2 x3 (x4[N := (aa, aaa, b) # emptyReview]) x5 x6)\<rparr>\<rbrakk> \<Longrightarrow> False
 2. \<And>cid uid aa aaa b x1 x2 x3 x4 x5 x6. \<lbrakk>ou = outOK; uid \<in> UIDs; a = UUact (uuReview cid uid (pass s uid) PID N (aa, aaa, b)); \<And>uid cid. uid \<in> UIDs \<Longrightarrow> Rev PID N \<notin> set (roles s cid uid); cid \<in>\<in> confIDs s; uid \<in>\<in> userIDs s; PID \<in>\<in> paperIDs s cid; phase s cid = disPH; isRev s cid uid PID; getReviewIndex s cid uid PID = N; paper s PID = Paper x1 x2 x3 x4 x5 x6; s' = s\<lparr>paper := (paper s)(PID := Paper x1 x2 x3 (x4[N := (aa, aaa, b) # x4 ! N]) x5 x6)\<rparr>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis isRev_imp_isRevNth_getReviewIndex)+