[STATEMENT]
lemma sub_env_trans:
  assumes "sub_env e e'" and "sub_env e' e''"
  shows "sub_env e e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e e''
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub_env e e'
sub_env e' e''

goal (1 subgoal):
 1. sub_env e e''
[PROOF STEP]
unfolding sub_env_def
[PROOF STATE]
proof (prove)
using this:
root e' = root e \<and> visited e \<subseteq> visited e' \<and> explored e \<subseteq> explored e' \<and> (\<forall>v. vsuccs e v \<subseteq> vsuccs e' v) \<and> (\<forall>v. \<S> e v \<subseteq> \<S> e' v) \<and> \<Union> {\<S> e v |v. v \<in> set (stack e)} \<subseteq> \<Union> {\<S> e' v |v. v \<in> set (stack e')}
root e'' = root e' \<and> visited e' \<subseteq> visited e'' \<and> explored e' \<subseteq> explored e'' \<and> (\<forall>v. vsuccs e' v \<subseteq> vsuccs e'' v) \<and> (\<forall>v. \<S> e' v \<subseteq> \<S> e'' v) \<and> \<Union> {\<S> e' v |v. v \<in> set (stack e')} \<subseteq> \<Union> {\<S> e'' v |v. v \<in> set (stack e'')}

goal (1 subgoal):
 1. root e'' = root e \<and> visited e \<subseteq> visited e'' \<and> explored e \<subseteq> explored e'' \<and> (\<forall>v. vsuccs e v \<subseteq> vsuccs e'' v) \<and> (\<forall>v. \<S> e v \<subseteq> \<S> e'' v) \<and> \<Union> {\<S> e v |v. v \<in> set (stack e)} \<subseteq> \<Union> {\<S> e'' v |v. v \<in> set (stack e'')}
[PROOF STEP]
by (metis (no_types, lifting) subset_trans)


[STATEMENT]
lemma min_maxsimpchainD_min_betw:
  "min_maxsimpchain (x#xs@[y]) \<Longrightarrow> maxsimpchain (x#ys@[y]) \<Longrightarrow>
    length ys \<ge> length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>min_maxsimpchain (x # xs @ [y]); maxsimpchain (x # ys @ [y])\<rbrakk> \<Longrightarrow> length xs \<le> length ys
[PROOF STEP]
using is_arg_minD2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_arg_min ?m ?P ?x; ?P ?y\<rbrakk> \<Longrightarrow> \<not> ?m ?y < ?m ?x

goal (1 subgoal):
 1. \<lbrakk>min_maxsimpchain (x # xs @ [y]); maxsimpchain (x # ys @ [y])\<rbrakk> \<Longrightarrow> length xs \<le> length ys
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fv_Cons[simp]: "fv (x # xs) = fv x \<union> fv xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (x # xs) = fv x \<union> fv xs
[PROOF STEP]
by (auto simp add: fv_def supp_Cons)


[STATEMENT]
lemma lift_lemma [simp]: \<open>\<lparr>E\<langle>0:x\<rangle>, F\<rparr> (\<^bold>\<up>t) = \<lparr>E, F\<rparr> t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>E\<langle>0:x\<rangle>, F\<rparr> (\<^bold>\<up> t) = \<lparr>E, F\<rparr> t
[PROOF STEP]
by (induct t) (auto cong: map_cong)


[STATEMENT]
lemma vappend_transfer[transfer_rule]:
  includes lifting_syntax
  shows "(cr_vfsequence ===> cr_vfsequence ===> cr_vfsequence)
    (\<lambda>xs ys. vappend ys xs) append"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_vfsequence ===> cr_vfsequence ===> cr_vfsequence) (\<lambda>xs ys. ys @\<^sub>\<circ> xs) (@)
[PROOF STEP]
by (intro rel_funI, unfold cr_vfsequence_def) (simp add: vappend_def)


[STATEMENT]
lemma rmge2_init:
  "rmge2 (f \<triangleright> n) =
   (if \<forall>i<Suc n. the (f i) < 2 then Some 0
    else Some (the (f (GREATEST i. i < Suc n \<and> the (f i) \<ge> 2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
let ?xs = "prefix f n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
have "f \<triangleright> n = list_encode ?xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)
[PROOF STEP]
by (simp add: init_def)
[PROOF STATE]
proof (state)
this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
have "(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length ?xs. ?xs ! i < 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
have "(GREATEST i. i < Suc n \<and> the (f i) \<ge> 2) =
      (GREATEST i. i < length ?xs \<and> ?xs ! i \<ge> 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
[PROOF STEP]
using length_prefix[of f n] prefix_nth[of _ n f]
[PROOF STATE]
proof (prove)
using this:
length (prefix f n) = Suc n
?k < Suc n \<Longrightarrow> prefix f n ! ?k = the (f ?k)

goal (1 subgoal):
 1. (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
have "(GREATEST i. i < Suc n \<and> the (f i) \<ge> 2) < Suc n"
      if "\<not> (\<forall>i<Suc n. the (f i) < 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n
[PROOF STEP]
using that GreatestI_ex_nat[of "\<lambda>i. i<Suc n \<and> the (f i) \<ge> 2" n]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i<Suc n. the (f i) < 2)
\<lbrakk>\<exists>k<Suc n. 2 \<le> the (f k); \<And>y. y < Suc n \<and> 2 \<le> the (f y) \<Longrightarrow> y \<le> n\<rbrakk> \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n \<and> 2 \<le> the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))

goal (1 subgoal):
 1. (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>i<Suc n. the (f i) < 2) \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
\<not> (\<forall>i<Suc n. the (f i) < 2) \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
\<not> (\<forall>i<Suc n. the (f i) < 2) \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
using rmge2
[PROOF STATE]
proof (prove)
using this:
f \<triangleright> n = Partial_Recursive.list_encode (prefix f n)
(\<forall>i<Suc n. the (f i) < 2) = (\<forall>i<length (prefix f n). prefix f n ! i < 2)
(GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) = (GREATEST i. i < length (prefix f n) \<and> 2 \<le> prefix f n ! i)
\<not> (\<forall>i<Suc n. the (f i) < 2) \<Longrightarrow> (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)) < Suc n
?xs = Partial_Recursive.list_decode ?e \<Longrightarrow> rmge2 ?e = (if \<forall>i<length ?xs. ?xs ! i < 2 then Some 0 else Some (?xs ! (GREATEST i. i < length ?xs \<and> 2 \<le> ?xs ! i)))

goal (1 subgoal):
 1. rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rmge2 (f \<triangleright> n) = (if \<forall>i<Suc n. the (f i) < 2 then Some 0 else Some (the (f (GREATEST i. i < Suc n \<and> 2 \<le> the (f i)))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma justify_conflict:
  assumes TR: "trace_to tr s"
  assumes "pref s uid pid = Conflict"
  shows "conflict_trace uid pid tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflict_trace uid pid tr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
pref s uid pid = Conflict

goal (1 subgoal):
 1. conflict_trace uid pid tr
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pref istate uid pid = Conflict \<Longrightarrow> conflict_trace uid pid []
 2. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
pref istate uid pid = Conflict

goal (2 subgoals):
 1. pref istate uid pid = Conflict \<Longrightarrow> conflict_trace uid pid []
 2. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
pref istate uid pid = Conflict

goal (1 subgoal):
 1. conflict_trace uid pid []
[PROOF STEP]
by (auto simp add: istate_def)
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid []

goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
case (step tr s a ou s')
[PROOF STATE]
proof (state)
this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr
pref s' uid pid = Conflict

goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
let ?trn = "Trans s a ou s'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
proof (cases "pref s uid pid = Conflict")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
 2. pref s uid pid \<noteq> Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
pref s uid pid \<noteq> Conflict

goal (2 subgoals):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
 2. pref s uid pid \<noteq> Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
with step.prems \<open>step s a = (ou, s')\<close>
[PROOF STATE]
proof (chain)
picking this:
pref s' uid pid = Conflict
step s a = (ou, s')
pref s uid pid \<noteq> Conflict
[PROOF STEP]
have "irrev_conflict uid pid ?trn \<or> set_conflict uid pid ?trn"
[PROOF STATE]
proof (prove)
using this:
pref s' uid pid = Conflict
step s a = (ou, s')
pref s uid pid \<noteq> Conflict

goal (1 subgoal):
 1. irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Cact x1\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 2. \<And>x2. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 3. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 4. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 5. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Cact x1\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases x1, auto simp: c_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 2. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 3. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 4. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases x2, auto simp: u_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 2. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 3. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases x3, auto simp: uu_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 2. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')

goal (2 subgoals):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
 2. pref s uid pid \<noteq> Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')

goal (1 subgoal):
 1. conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
unfolding conflict_trace_def
[PROOF STATE]
proof (prove)
using this:
irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')

goal (1 subgoal):
 1. (\<exists>trn\<in>set (tr ## Trans s a ou s'). irrev_conflict uid pid trn) \<or> (\<exists>tr1 trn tr2. tr ## Trans s a ou s' = tr1 @ trn # tr2 \<and> set_conflict uid pid trn \<and> (\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid (tr ## Trans s a ou s')

goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pref s uid pid = Conflict

goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
with step.IH
[PROOF STATE]
proof (chain)
picking this:
pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr
pref s uid pid = Conflict
[PROOF STEP]
have CT: "conflict_trace uid pid tr"
[PROOF STATE]
proof (prove)
using this:
pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr
pref s uid pid = Conflict

goal (1 subgoal):
 1. conflict_trace uid pid tr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid tr

goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
from step.prems \<open>step s a = (ou, s')\<close>
[PROOF STATE]
proof (chain)
picking this:
pref s' uid pid = Conflict
step s a = (ou, s')
[PROOF STEP]
have "\<not>reset_conflict uid pid ?trn"
[PROOF STATE]
proof (prove)
using this:
pref s' uid pid = Conflict
step s a = (ou, s')

goal (1 subgoal):
 1. \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Cact x1\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 2. \<And>x2. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 3. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 4. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 5. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Cact x1_\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 2. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 3. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 4. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
by (cases x2, auto simp: u_defs)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 2. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 3. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<not> reset_conflict uid pid (Trans s a ou s')

goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> reset_conflict uid pid (Trans s a ou s')

goal (1 subgoal):
 1. conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
using CT
[PROOF STATE]
proof (prove)
using this:
\<not> reset_conflict uid pid (Trans s a ou s')
conflict_trace uid pid tr

goal (1 subgoal):
 1. conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
unfolding conflict_trace_def
[PROOF STATE]
proof (prove)
using this:
\<not> reset_conflict uid pid (Trans s a ou s')
(\<exists>trn\<in>set tr. irrev_conflict uid pid trn) \<or> (\<exists>tr1 trn tr2. tr = tr1 @ trn # tr2 \<and> set_conflict uid pid trn \<and> (\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn))

goal (1 subgoal):
 1. (\<exists>trn\<in>set (tr ## Trans s a ou s'). irrev_conflict uid pid trn) \<or> (\<exists>tr1 trn tr2. tr ## Trans s a ou s' = tr1 @ trn # tr2 \<and> set_conflict uid pid trn \<and> (\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tr1 trn tr2. \<lbrakk>\<not> reset_conflict uid pid (Trans s a ou s'); \<not> irrev_conflict uid pid (Trans s a ou s'); \<forall>tr1a trna. set_conflict uid pid trna \<longrightarrow> (\<forall>tr2a. tr1 @ trn # tr2 ## Trans s a ou s' = tr1a @ trna # tr2a \<longrightarrow> (\<exists>x\<in>set tr2a. reset_conflict uid pid x)); tr = tr1 @ trn # tr2; set_conflict uid pid trn; \<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn; \<forall>x\<in>set tr1 \<union> set tr2. \<not> irrev_conflict uid pid x\<rbrakk> \<Longrightarrow> irrev_conflict uid pid trn
[PROOF STEP]
by (metis rotate1.simps(2) set_ConsD set_rotate1)
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid (tr ## Trans s a ou s')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid (tr ## Trans s a ou s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fresher_refl [simp]: "r \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<sqsubseteq> r
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r r < nsqn\<^sub>r r \<or> nsqn\<^sub>r r = nsqn\<^sub>r r \<and> \<pi>\<^sub>5 r \<le> \<pi>\<^sub>5 r
[PROOF STEP]
by simp


[STATEMENT]
lemma adj_sub_geq2_fact:"\<And>i j x1 x2. i\<in>SIGT x2 \<Longrightarrow> j \<in> (case SFunctions \<sigma> i of Some x \<Rightarrow> FVT x | None \<Rightarrow> {}) \<Longrightarrow> Inl i \<in>({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union>
         {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter>
        {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2. \<lbrakk>i \<in> SIGT x2; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}
[PROOF STEP]
unfolding SDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x1 x2. \<lbrakk>i \<in> SIGT x2; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> Inl i \<in> ({Inl x |x. x \<in> dom (SFunctions \<sigma>)} \<union> {Inr (Inl x) |x. x \<in> dom (SContexts \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPredicates \<sigma>)} \<union> {Inr (Inr x) |x. x \<in> dom (SPrograms \<sigma>)}) \<inter> {Inl x |x. x \<in> SIGT x1 \<or> x \<in> SIGT x2}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j x2. \<lbrakk>i \<in> SIGT x2; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> SIGT x2_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x)\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
apply (cases "SFunctions \<sigma> i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> SIGT x2_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = None\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
 2. \<And>a. \<lbrakk>i \<in> SIGT x2_; j \<in> (case SFunctions \<sigma> i of None \<Rightarrow> {} | Some x \<Rightarrow> FVT x); SFunctions \<sigma> i = Some a\<rbrakk> \<Longrightarrow> \<exists>y. SFunctions \<sigma> i = Some y
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma uadmit_mkv_ntadjoint:
  assumes ssafe:"\<And>i. dsafe (\<sigma> i)"
  assumes good_interp:"is_interp I"
  assumes VA:"Vagree \<nu> \<omega> (\<Union>y\<in>{y. Inl (Inr y) \<in> SIGO ODE}. FVT (\<sigma> y))"
  assumes osafe:"osafe ODE"
  shows "mk_v (adjointFO I \<sigma> \<nu>) ODE = mk_v (adjointFO I \<sigma> \<omega>) ODE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_v (adjointFO I \<sigma> \<nu>) ODE = mk_v (adjointFO I \<sigma> \<omega>) ODE
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. mk_v (adjointFO I \<sigma> \<nu>) ODE x = mk_v (adjointFO I \<sigma> \<omega>) ODE x
[PROOF STEP]
subgoal for R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_v (adjointFO I \<sigma> \<nu>) ODE R = mk_v (adjointFO I \<sigma> \<omega>) ODE R
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. mk_v (adjointFO I \<sigma> \<nu>) ODE R x = mk_v (adjointFO I \<sigma> \<omega>) ODE R x
[PROOF STEP]
subgoal for solt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_v (adjointFO I \<sigma> \<nu>) ODE R solt = mk_v (adjointFO I \<sigma> \<omega>) ODE R solt
[PROOF STEP]
apply(rule agree_UNIV_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) UNIV
[PROOF STEP]
using mk_v_agree[of "(adjointFO I \<sigma> \<nu>)" ODE "R" solt]
[PROOF STATE]
proof (prove)
using this:
Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<nu>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) (semBV (adjointFO I \<sigma> \<nu>) ODE)

goal (1 subgoal):
 1. Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) UNIV
[PROOF STEP]
using mk_v_agree[of "(adjointFO I \<sigma> \<omega>)" ODE "R" solt]
[PROOF STATE]
proof (prove)
using this:
Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<nu>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) (semBV (adjointFO I \<sigma> \<nu>) ODE)
Vagree (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<omega>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<omega>) ODE solt) (semBV (adjointFO I \<sigma> \<omega>) ODE)

goal (1 subgoal):
 1. Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) UNIV
[PROOF STEP]
using uadmit_ode_ntadjoint'[OF ssafe good_interp VA osafe]
[PROOF STATE]
proof (prove)
using this:
Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<nu>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) (semBV (adjointFO I \<sigma> \<nu>) ODE)
Vagree (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) R (- semBV (adjointFO I \<sigma> \<omega>) ODE) \<and> Vagree (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) (mk_xode (adjointFO I \<sigma> \<omega>) ODE solt) (semBV (adjointFO I \<sigma> \<omega>) ODE)
ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE

goal (1 subgoal):
 1. Vagree (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) UNIV
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
using this:
((\<forall>i. Inl i \<in> - semBV (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i) \<and> (\<forall>i. Inr i \<in> - semBV (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i)) \<and> (\<forall>i. Inl i \<in> semBV (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) $ i) \<and> (\<forall>i. Inr i \<in> semBV (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd (mk_xode (adjointFO I \<sigma> \<nu>) ODE solt) $ i)
((\<forall>i. Inl i \<in> - semBV (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i) \<and> (\<forall>i. Inr i \<in> - semBV (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i)) \<and> (\<forall>i. Inl i \<in> semBV (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst (mk_xode (adjointFO I \<sigma> \<omega>) ODE solt) $ i) \<and> (\<forall>i. Inr i \<in> semBV (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd (mk_xode (adjointFO I \<sigma> \<omega>) ODE solt) $ i)
ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> UNIV \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i) \<and> (\<forall>i. Inr i \<in> UNIV \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i)\<rbrakk> \<Longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i
 2. \<And>i. \<lbrakk>ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i)\<rbrakk> \<Longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i
[PROOF STEP]
using adjointFO_ode_vars
[PROOF STATE]
proof (prove)
using this:
ODE_vars (adjointFO ?I ?\<sigma> ?\<nu>) ?ODE = ODE_vars (adjointFO ?I ?\<sigma> ?\<omega>) ?ODE

goal (2 subgoals):
 1. \<And>i. \<lbrakk>ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i)\<rbrakk> \<Longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i
 2. \<And>i. \<lbrakk>ODE_sem (adjointFO I \<sigma> \<nu>) ODE = ODE_sem (adjointFO I \<sigma> \<omega>) ODE; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = fst R $ i; \<forall>i. Inl i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inl i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = fst R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd R $ i; \<forall>i. Inr i \<notin> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<and> Inr i \<notin> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = snd R $ i; \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<nu>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i); \<forall>i. (Inl i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i) \<and> (Inl i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> fst (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = solt $ i); \<forall>i. (Inr i \<in> Inl ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i) \<and> (Inr i \<in> Inr ` ODE_vars (adjointFO I \<sigma> \<omega>) ODE \<longrightarrow> snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i = ODE_sem (adjointFO I \<sigma> \<omega>) ODE solt $ i)\<rbrakk> \<Longrightarrow> snd (mk_v (adjointFO I \<sigma> \<nu>) ODE R solt) $ i = snd (mk_v (adjointFO I \<sigma> \<omega>) ODE R solt) $ i
[PROOF STEP]
by metis+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma real_interval_one: "real_interval 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_interval 1 = 1
[PROOF STEP]
by (simp add: interval_eqI)


[STATEMENT]
lemma Methods_into_Methods':
  assumes "Program P \<turnstile> C sees_methods Mm"
  shows "\<exists>Mm'. Methods' P C Mm' \<and> Mm = map_of Mm'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Mm'. Methods' P C Mm' \<and> Mm = map_of Mm'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Program P \<turnstile> C sees_methods Mm

goal (1 subgoal):
 1. \<exists>Mm'. Methods' P C Mm' \<and> Mm = map_of Mm'
[PROOF STEP]
by induct(auto intro: Methods'.intros simp add: map_of_map2 map_add_def)


[STATEMENT]
lemma map_resource_compose [simp]:
  "map_resource a b (map_resource a' b' res) = map_resource (a' \<circ> a) (b \<circ> b') res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_resource a b (map_resource a' b' res) = map_resource (a' \<circ> a) (b \<circ> b') res
[PROOF STEP]
by(coinduction arbitrary: res)(auto 4 3 intro!: rel_funI rel_spmf_reflI simp add: spmf_rel_map)


[STATEMENT]
lemma lossless_resource_coinduct [consumes 1, case_names lossless_resource, case_conclusion lossless_resource lossless step, coinduct pred: lossless_resource]:
  assumes "X res"
    and "\<And>res a. \<lbrakk> X res; a \<in> outs_\<I> \<I> \<rbrakk> \<Longrightarrow> lossless_spmf (run_resource res a) \<and>
          (\<forall>(b, res') \<in> set_spmf (run_resource res a). X res' \<or> lossless_resource \<I> res')"
  shows "lossless_resource \<I> res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_resource \<I> res
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
X res

goal (1 subgoal):
 1. lossless_resource \<I> res
[PROOF STEP]
by(rule lossless_resource.coinduct)(auto dest: assms(2))


[STATEMENT]
lemma mset_insert: "mset_tree(insert x t) = {#x#} + mset_tree t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_tree (insert x t) = {#x#} + mset_tree t
[PROOF STEP]
by(induction t arbitrary: x) (auto simp: ac_simps)


[STATEMENT]
lemma (in Congruence_Rule) Ang_complementary_inside :
  assumes
    "Def (Ang (An p1 p2 p3))"
    "Bet_Point (Se p3 p4) p2"
    "Ang_inside (An p5 p2 p3) p1"
  shows
    "Ang_inside (An p1 p2 p4) p5"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P1 : "Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P2 : "Line_on (Li p2 p3) p4"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. Line_on (Li p2 p3) p4
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p4

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P3 : "Line_on (Li p2 p3) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p3) p2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p2

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P4 : "Line_on (Li p2 p4) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p4) p2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p4) p2

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P5 : "Line_on (Li p2 p4) p4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p4) p4
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p4) p4

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P2 P3 P4 P5 P6
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p3) p4
Line_on (Li p2 p3) p2
Line_on (Li p2 p4) p2
Line_on (Li p2 p4) p4
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P7 : "Eq (Geos (Lin (Li p2 p3)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p3) p4
Line_on (Li p2 p3) p2
Line_on (Li p2 p4) p2
Line_on (Li p2 p4) p4
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li p2 p3)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li p2 p3)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P1 P7
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1
Eq (Geos (Lin (Li p2 p3)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
[PROOF STEP]
have P8 : "Plane_sameside (Li p2 p4) p5 p1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1
Eq (Geos (Lin (Li p2 p3)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li p2 p4) p5 p1
[PROOF STEP]
by (blast intro:Plane_Line_trans)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p2 p4) p5 p1

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P9 : "Line_on (Li p2 p1) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p1) p2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p1) p2

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have "Line_on (Li p2 p1) p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p1) p1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p1) p1

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p1) p1
[PROOF STEP]
have P10 : "Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow>
    Line_on (Li p3 p4) p1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p1) p1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow> Line_on (Li p3 p4) p1
[PROOF STEP]
by (blast intro:Eq_rev Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow> Line_on (Li p3 p4) p1

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1
[PROOF STEP]
have P11 : "\<not> Line_on (Li p2 p3) p1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1

goal (1 subgoal):
 1. \<not> Line_on (Li p2 p3) p1
[PROOF STEP]
by (simp add:Plane_sameside_def)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p2 p3) p1

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P12 : "Line_on (Li p3 p4) p2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. Line_on (Li p3 p4) p2
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p2

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P13 : "Line_on (Li p3 p4) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p3 p4) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p3

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P14 : "Line_on (Li p2 p3) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p3) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p3

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P15 : "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P3 P12 P13 P14 P15
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p3) p2
Line_on (Li p3 p4) p2
Line_on (Li p3 p4) p3
Line_on (Li p2 p3) p3
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P16 : "Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p3) p2
Line_on (Li p3 p4) p2
Line_on (Li p3 p4) p3
Line_on (Li p2 p3) p3
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p3)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p3)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P10 P16
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow> Line_on (Li p3 p4) p1
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p3)) add Emp)
[PROOF STEP]
have P17 : "Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow>
    Line_on (Li p2 p3) p1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow> Line_on (Li p3 p4) p1
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p3)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow> Line_on (Li p2 p3) p1
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow> Line_on (Li p2 p3) p1

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P11 P17
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p2 p3) p1
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow> Line_on (Li p2 p3) p1
[PROOF STEP]
have P18 : "\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p2 p3) p1
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow> Line_on (Li p2 p3) p1

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms P9 P18
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
Line_on (Li p2 p1) p2
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp)
[PROOF STEP]
have P19 : "Plane_diffside (Li p2 p1) p3 p4"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
Line_on (Li p2 p1) p2
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li p2 p1) p3 p4
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li p2 p1) p3 p4

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P20 : "Plane_diffside (Li p2 p1) p3 p5"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. Plane_diffside (Li p2 p1) p3 p5
[PROOF STEP]
by (simp add:Ang_inside_Planeside Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li p2 p1) p3 p5

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p4) p4
[PROOF STEP]
have P21 : "Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow> Line_on (Li p2 p4) p5"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p4) p4

goal (1 subgoal):
 1. Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow> Line_on (Li p2 p4) p5
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow> Line_on (Li p2 p4) p5

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p4) p5 p1
[PROOF STEP]
have P22 : "\<not> Line_on (Li p2 p4) p5"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p4) p5 p1

goal (1 subgoal):
 1. \<not> Line_on (Li p2 p4) p5
[PROOF STEP]
by (simp add:Plane_sameside_def)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p2 p4) p5

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P21 P22
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow> Line_on (Li p2 p4) p5
\<not> Line_on (Li p2 p4) p5
[PROOF STEP]
have P23 : "\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow> Line_on (Li p2 p4) p5
\<not> Line_on (Li p2 p4) p5

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P19 P20 P23
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li p2 p1) p3 p4
Plane_diffside (Li p2 p1) p3 p5
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp)
[PROOF STEP]
have P24 : "Plane_sameside (Li p2 p1) p4 p5"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li p2 p1) p3 p4
Plane_diffside (Li p2 p1) p3 p5
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li p2 p1) p4 p5
[PROOF STEP]
by (simp add:Plane_trans_inv)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p2 p1) p4 p5

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p1) p4 p5
[PROOF STEP]
have P25 : "\<not> Line_on (Li p2 p1) p4"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p1) p4 p5

goal (1 subgoal):
 1. \<not> Line_on (Li p2 p1) p4
[PROOF STEP]
by (simp add:Plane_sameside_def)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p2 p1) p4

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P26 : "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P25 P26
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p2 p1) p4
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
have "Def (Ang (An p2 p1 p4))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p2 p1) p4
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p2 p1 p4))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p2 p1 p4))

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p2 p1 p4))
[PROOF STEP]
have P27 : "Def (Ang (An p1 p2 p4))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p2 p1 p4))

goal (1 subgoal):
 1. Def (Ang (An p1 p2 p4))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p1 p2 p4))

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p4) p5 p1
[PROOF STEP]
have P28 : "Plane_sameside (Li p2 p4) p1 p5"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p4) p5 p1

goal (1 subgoal):
 1. Plane_sameside (Li p2 p4) p1 p5
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p2 p4) p1 p5

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P24 P27 P28
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p1) p4 p5
Def (Ang (An p1 p2 p4))
Plane_sameside (Li p2 p4) p1 p5
[PROOF STEP]
show "Ang_inside (An p1 p2 p4) p5"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p1) p4 p5
Def (Ang (An p1 p2 p4))
Plane_sameside (Li p2 p4) p1 p5

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p1 p2 p4) p5

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compile_env_imp_rel_option:
  assumes "compile_env F1 = Some F2"
  shows "rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
compile_env F1 = Some F2
[PROOF STEP]
obtain xs where
    ap_map_list_F1: "ap_map_list (ap_map_prod Some compile_fundef) (Fstd_to_list F1) = Some xs" and
    F2_def: "F2 = Sinca.Fenv.from_list xs"
[PROOF STATE]
proof (prove)
using this:
compile_env F1 = Some F2

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>ap_map_list (ap_map_prod Some compile_fundef) (Fstd_to_list F1) = Some xs; F2 = Sinca.Fenv.from_list xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: compile_env_def ap_option_eq_Some_conv)
[PROOF STATE]
proof (state)
this:
ap_map_list (ap_map_prod Some compile_fundef) (Fstd_to_list F1) = Some xs
F2 = Sinca.Fenv.from_list xs

goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
unfolding F2_def Sinca.Fenv.from_list_correct[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get (Sinca.Fenv.from_list xs) f)
[PROOF STEP]
unfolding Sinca.Fenv.from_list_correct
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (map_of xs f)
[PROOF STEP]
unfolding Sstd.Fenv.to_list_correct[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (map_of (Fstd_to_list F1) f) (map_of xs f)
[PROOF STEP]
using ap_map_list_F1
[PROOF STATE]
proof (prove)
using this:
ap_map_list (ap_map_prod Some compile_fundef) (Fstd_to_list F1) = Some xs

goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (map_of (Fstd_to_list F1) f) (map_of xs f)
[PROOF STEP]
by (simp add: ap_map_list_ap_map_prod_imp_rel_option_map_of)
[PROOF STATE]
proof (state)
this:
rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isShortestPath_alt:
  "isShortestPath u p v \<longleftrightarrow> isSimplePath u p v \<and> length p = min_dist u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isShortestPath u p v = (isSimplePath u p v \<and> length p = min_dist u v)
[PROOF STEP]
using shortestPath_is_simple isShortestPath_min_dist_def
[PROOF STATE]
proof (prove)
using this:
isShortestPath ?s ?p ?t \<Longrightarrow> isSimplePath ?s ?p ?t
isShortestPath ?u ?p ?v = (isPath ?u ?p ?v \<and> length ?p = min_dist ?u ?v)

goal (1 subgoal):
 1. isShortestPath u p v = (isSimplePath u p v \<and> length p = min_dist u v)
[PROOF STEP]
unfolding isSimplePath_def
[PROOF STATE]
proof (prove)
using this:
isShortestPath ?s ?p ?t \<Longrightarrow> isPath ?s ?p ?t \<and> distinct (pathVertices ?s ?p)
isShortestPath ?u ?p ?v = (isPath ?u ?p ?v \<and> length ?p = min_dist ?u ?v)

goal (1 subgoal):
 1. isShortestPath u p v = ((isPath u p v \<and> distinct (pathVertices u p)) \<and> length p = min_dist u v)
[PROOF STEP]
by auto


[STATEMENT]
lemma adjacent_singleton: "t \<noteq> Leaf \<Longrightarrow> adjacent (l t, r t) [t]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> Leaf \<Longrightarrow> adjacent (l t, r t) [t]
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> Leaf \<Longrightarrow> Leaf \<notin> set [t] \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast [t]) (tl [t]) \<and> ([t] = [] \<or> l (last [t]) = fst (l t, r t) \<and> r (hd [t]) = snd (l t, r t))
[PROOF STEP]
by simp


[STATEMENT]
lemma l_discharge[simp]: "l (discharge a) = l a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l (discharge a) = l a
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma finite_subset_chain:
  fixes Y :: "nat \<Rightarrow> 'a set"
  assumes "chain Y"
  assumes "S \<subseteq> \<Union>(Y ` UNIV)"
  assumes "finite S"
  shows "\<exists>i. S \<subseteq> Y i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> \<Union> (range Y)
[PROOF STEP]
have "\<forall>x \<in> S. \<exists> i. x \<in> Y i"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> \<Union> (range Y)

goal (1 subgoal):
 1. \<forall>x\<in>S. \<exists>i. x \<in> Y i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. \<exists>i. x \<in> Y i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. \<exists>i. x \<in> Y i
[PROOF STEP]
obtain f where f: "\<forall> x\<in> S. x \<in> Y (f x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. \<exists>i. x \<in> Y i

goal (1 subgoal):
 1. (\<And>f. \<forall>x\<in>S. x \<in> Y (f x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. x \<in> Y (f x)

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
define i where "i = Max (f ` S)"
[PROOF STATE]
proof (state)
this:
i = Max (f ` S)

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
from \<open>finite S\<close>
[PROOF STATE]
proof (chain)
picking this:
finite S
[PROOF STEP]
have "finite (f ` S)"
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. finite (f ` S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (f ` S)

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
hence "\<forall> x\<in>S. f x \<le> i"
[PROOF STATE]
proof (prove)
using this:
finite (f ` S)

goal (1 subgoal):
 1. \<forall>x\<in>S. f x \<le> i
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
using this:
finite (f ` S)

goal (1 subgoal):
 1. \<forall>x\<in>S. f x \<le> Max (f ` S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. f x \<le> i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
with chain_mono[OF \<open>chain Y\<close>]
[PROOF STATE]
proof (chain)
picking this:
?i \<le> ?j \<Longrightarrow> Y ?i \<sqsubseteq> Y ?j
\<forall>x\<in>S. f x \<le> i
[PROOF STEP]
have "\<forall> x\<in>S. Y (f x) \<subseteq> Y i"
[PROOF STATE]
proof (prove)
using this:
?i \<le> ?j \<Longrightarrow> Y ?i \<sqsubseteq> Y ?j
\<forall>x\<in>S. f x \<le> i

goal (1 subgoal):
 1. \<forall>x\<in>S. Y (f x) \<subseteq> Y i
[PROOF STEP]
by (auto simp add: below_set_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. Y (f x) \<subseteq> Y i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. x \<in> Y (f x)
\<forall>x\<in>S. Y (f x) \<subseteq> Y i
[PROOF STEP]
have "S \<subseteq> Y i"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. x \<in> Y (f x)
\<forall>x\<in>S. Y (f x) \<subseteq> Y i

goal (1 subgoal):
 1. S \<subseteq> Y i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<subseteq> Y i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> Y i

goal (1 subgoal):
 1. \<exists>i. S \<subseteq> Y i
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>i. S \<subseteq> Y i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma WHILEI_weaken:
  assumes IW: "\<And>x. I x \<Longrightarrow> I' x"
  shows "WHILEI I' b f x \<le> WHILEI I b f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILEI I' b f x \<le> WHILEI I b f x
[PROOF STEP]
unfolding WHILEI_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC (WHILEI_body bind return I' b f) x \<le> REC (WHILEI_body bind return I b f) x
[PROOF STEP]
apply (rule REC_mono_ref[OF WHILEI_body_trimono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D x. WHILEI_body bind return I' b f D x \<le> WHILEI_body bind return I b f D x
[PROOF STEP]
apply (auto simp add: WHILEI_body_def dest: IW)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma add_rel_frac:
  assumes "(r,s) \<in> R \<times> S" "(r',s')\<in> R \<times> S"
  shows "add_rel (r/s) (r'/s') = (r\<cdot>s' + r'\<cdot>s) / (s\<cdot>s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
define x where "x=(SOME x. x\<in>(r/s))"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> r / s)

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
define y where "y=(SOME y. y\<in>(r'/s'))"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> r' / s')

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
obtain s1 where [simp]:"s1 \<in> S" and x_eq:"s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r" and x_RS:"x \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using frac_eq_obtains[OF \<open>(r,s) \<in> R \<times> S\<close> x_def]
[PROOF STATE]
proof (prove)
using this:
(\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<in> S
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
x \<in> R \<times> S

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
obtain s2 where [simp]:"s2 \<in> S" and y_eq:"s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'" and y_RS:"y \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>s2 \<in> S; s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using frac_eq_obtains[OF \<open>(r',s') \<in> R \<times> S\<close> y_def]
[PROOF STATE]
proof (prove)
using this:
(\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s' \<cdot> fst y = s1 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>s2 \<in> S; s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s2 \<in> S
s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'
y \<in> R \<times> S

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
have "add_rel (r/s) (r'/s') = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)
[PROOF STEP]
unfolding add_rel_def add_rel_aux_def x_def y_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s') + fst (SOME y. y \<in> r' / s') \<cdot> snd (SOME x. x \<in> r / s)) / (snd (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s')) = (fst (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s') + fst (SOME y. y \<in> r' / s') \<cdot> snd (SOME x. x \<in> r / s)) / (snd (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_rel (r / s) (r' / s') = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
add_rel (r / s) (r' / s') = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
have "... = (r\<cdot>s' + r'\<cdot>s) / (s\<cdot>s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y) = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
proof (rule frac_eqI[of "s1 \<cdot> s2"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
have "snd y \<cdot>  s' \<cdot> s2 \<cdot> (s1 \<cdot>  s \<cdot> fst x)  = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot>  snd x \<cdot>  r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)
[PROOF STEP]
using x_eq
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r

goal (1 subgoal):
 1. snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)
[PROOF STEP]
have "s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y =  s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'"
[PROOF STATE]
proof (prove)
using this:
snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
[PROOF STEP]
using comm.multiplicative.associative assms x_RS y_RS comm.comm_mult
[PROOF STATE]
proof (prove)
using this:
snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b = ?b \<cdot> ?a

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
have "snd x \<cdot> s \<cdot>s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot>s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
using y_eq
[PROOF STATE]
proof (prove)
using this:
s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'

goal (1 subgoal):
 1. snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
have "s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s"
[PROOF STATE]
proof (prove)
using this:
snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s
[PROOF STEP]
using comm.multiplicative.associative assms x_RS y_RS comm.comm_mult
[PROOF STATE]
proof (prove)
using this:
snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b = ?b \<cdot> ?a

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s
[PROOF STEP]
show "s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x)
        = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)"
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
using comm.multiplicative.associative assms x_RS y_RS comm.distributive
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> (?b + ?c) \<cdot> ?a = ?b \<cdot> ?a + ?c \<cdot> ?a

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)

goal (3 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
show "s1 \<cdot> s2 \<in> S" "(fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S"
        "(r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 \<cdot> s2 \<in> S &&& (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S &&& (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
using assms x_RS y_RS
[PROOF STATE]
proof (prove)
using this:
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S

goal (1 subgoal):
 1. s1 \<cdot> s2 \<in> S &&& (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S &&& (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<in> S
(fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
(r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y) = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supp_transform: "supp (transform a e) \<subseteq> supp e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
note PropApp_eqvt[eqvt_raw] PropLam_eqvt[eqvt_raw] PropLetBody_eqvt[eqvt_raw]  AnalLet_eqvt[eqvt_raw] PropLetHeap_eqvt[eqvt_raw] TransVar_eqvt[eqvt]  TransApp_eqvt[eqvt]  TransLam_eqvt[eqvt] TransLet_eqvt[eqvt]
[PROOF STATE]
proof (state)
this:
?\<pi> \<bullet> PropApp \<equiv> PropApp
?\<pi> \<bullet> PropLam \<equiv> PropLam
?\<pi> \<bullet> PropLetBody \<equiv> PropLetBody
?\<pi> \<bullet> AnalLet \<equiv> AnalLet
?\<pi> \<bullet> PropLetHeap \<equiv> PropLetHeap
?\<pi> \<bullet> TransVar = TransVar
?\<pi> \<bullet> TransApp = TransApp
?\<pi> \<bullet> TransLam = TransLam
?\<pi> \<bullet> TransLet = TransLet

goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
note transform.eqvt[eqvt]
[PROOF STATE]
proof (state)
this:
?p \<bullet> transform ?a ?aa = transform (?p \<bullet> ?a) (?p \<bullet> ?aa)

goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (transform a e) \<subseteq> supp e
[PROOF STEP]
apply (rule supp_fun_app_eqvt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (transform a)
[PROOF STEP]
apply (rule eqvtI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. p \<bullet> transform a \<equiv> transform a
[PROOF STEP]
apply perm_simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. transform a \<equiv> transform a
[PROOF STEP]
apply (rule reflexive)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
supp (transform a e) \<subseteq> supp e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subcs_news: \<open>news c z \<Longrightarrow> subcs c s z = z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news c z \<Longrightarrow> subcs c s z = z
[PROOF STEP]
by (induct z) simp_all


[STATEMENT]
lemma hm_valid_refine: "(hm_valid,h.valid)\<in>hmr_rel \<rightarrow> nat_rel \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_valid, h.valid) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> bool_rel
[PROOF STEP]
apply (intro fun_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> (hm_valid a aa, h.valid a' a'a) \<in> bool_rel
[PROOF STEP]
unfolding hm_valid_def h.valid_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> (0 < aa \<and> aa \<le> hm_length a, 0 < a'a \<and> a'a \<le> length a') \<in> bool_rel
[PROOF STEP]
by (parametricity add: hm_length_refine)


[STATEMENT]
lemma heapmap_nres_rel_prodI:
      assumes "hmx \<le> \<Down>(UNIV \<times>\<^sub>r hmr_rel) h'x"
      assumes "h'x \<le> SPEC (\<lambda>(_,h'). h.heap_invar h')"
      assumes "hmx \<le>\<^sub>n SPEC (\<lambda>(r,hm'). RETURN (r,heapmap_\<alpha> hm') \<le> \<Down>(R\<times>\<^sub>rId) hx)"
      shows "hmx \<le> \<Down>(R\<times>\<^sub>rheapmap_rel) hx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r heapmap_rel) hx
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hmx \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) h'x
h'x \<le> SPEC (\<lambda>(uu_, y). h.heap_invar y)
hmx \<le>\<^sub>n SPEC (\<lambda>(r, hm'). RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> (R \<times>\<^sub>r Id) hx)

goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r heapmap_rel) hx
[PROOF STEP]
unfolding heapmap_rel_def hmr_rel_def br_def heapmap_invar_def
[PROOF STATE]
proof (prove)
using this:
hmx \<le> \<Down> (UNIV \<times>\<^sub>r {(c, a). a = hmr_\<alpha> c \<and> hmr_invar c}) h'x
h'x \<le> SPEC (\<lambda>(uu_, y). h.heap_invar y)
hmx \<le>\<^sub>n SPEC (\<lambda>(r, hm'). RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> (R \<times>\<^sub>r Id) hx)

goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r {(c, a). a = heapmap_\<alpha> c \<and> hmr_invar c \<and> h.heap_invar (hmr_\<alpha> c)}) hx
[PROOF STEP]
apply (auto simp: pw_le_iff pw_leof_iff refine_pw_simps; blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dual_up_closed:
  "up_closed x \<longleftrightarrow> up_closed (x\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_closed x = up_closed (x\<^sup>d)
[PROOF STEP]
by (metis dual_involutive dual_one up_closed_def strong_up_closed_2)


[STATEMENT]
lemma synth_analz_insert_eq [rule_format]:
     "X \<in> synth (analz H)
      \<Longrightarrow> \<forall> G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)
[PROOF STEP]
apply (erule synth.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>X. X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)
 2. \<And>agt. \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert (Agent agt) G)) = (Key K \<in> analz G)
 3. \<And>n. \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert (Number n) G)) = (Key K \<in> analz G)
 4. \<And>X. \<lbrakk>X \<in> synth (analz H); \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)\<rbrakk> \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert (Hash X) G)) = (Key K \<in> analz G)
 5. \<And>X Y. \<lbrakk>X \<in> synth (analz H); \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G); Y \<in> synth (analz H); \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert Y G)) = (Key K \<in> analz G)\<rbrakk> \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert \<lbrace>X, Y\<rbrace> G)) = (Key K \<in> analz G)
 6. \<And>X Ka. \<lbrakk>X \<in> synth (analz H); \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G); Key Ka \<in> analz H\<rbrakk> \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert (Crypt Ka X) G)) = (Key K \<in> analz G)
[PROOF STEP]
apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done