[STATEMENT]
lemma list_match_cong[sepref_frame_match_rules]:
  "\<lbrakk>\<And>x x'. \<lbrakk>x\<in>set l; x'\<in>set l'\<rbrakk> \<Longrightarrow> hn_ctxt A x x' \<Longrightarrow>\<^sub>t hn_ctxt A' x x' \<rbrakk> \<Longrightarrow> hn_ctxt (list_assn A) l l' \<Longrightarrow>\<^sub>t hn_ctxt (list_assn A') l l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x x'. \<lbrakk>x \<in> set l; x' \<in> set l'\<rbrakk> \<Longrightarrow> hn_ctxt A x x' \<Longrightarrow>\<^sub>t hn_ctxt A' x x') \<Longrightarrow> hn_ctxt (list_assn A) l l' \<Longrightarrow>\<^sub>t hn_ctxt (list_assn A') l l'
[PROOF STEP]
unfolding hn_ctxt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x x'. \<lbrakk>x \<in> set l; x' \<in> set l'\<rbrakk> \<Longrightarrow> A x x' \<Longrightarrow>\<^sub>t A' x x') \<Longrightarrow> list_assn A l l' \<Longrightarrow>\<^sub>t list_assn A' l l'
[PROOF STEP]
by (induct A l l' rule: list_assn.induct) (simp_all add: entt_star_mono)


[STATEMENT]
lemma list_merge_cong[sepref_frame_merge_rules]:
  assumes "\<And>x x'. \<lbrakk>x\<in>set l; x'\<in>set l'\<rbrakk> \<Longrightarrow> hn_ctxt A x x' \<or>\<^sub>A hn_ctxt A' x x' \<Longrightarrow>\<^sub>t hn_ctxt Am x x'"
  shows "hn_ctxt (list_assn A) l l' \<or>\<^sub>A hn_ctxt (list_assn A') l l' \<Longrightarrow>\<^sub>t hn_ctxt (list_assn Am) l l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (list_assn A) l l' \<or>\<^sub>A hn_ctxt (list_assn A') l l' \<Longrightarrow>\<^sub>t hn_ctxt (list_assn Am) l l'
[PROOF STEP]
apply (blast intro: entt_disjE list_match_cong entt_disjD1[OF assms] entt_disjD2[OF assms])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma invalid_list_split:
  "invalid_assn (list_assn A) (x#xs) (y#ys) \<Longrightarrow>\<^sub>t invalid_assn A x y * invalid_assn (list_assn A) xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn (list_assn A) (x # xs) (y # ys) \<Longrightarrow>\<^sub>t invalid_assn A x y * invalid_assn (list_assn A) xs ys
[PROOF STEP]
by (fastforce simp: invalid_assn_def intro!: enttI simp: mod_star_conv)


[STATEMENT]
lemma entt_invalid_list: "hn_invalid (list_assn A) l l' \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn A)) l l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid (list_assn A) l l' \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn A)) l l'
[PROOF STEP]
apply (induct A l l' rule: list_assn.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>P. hn_invalid (list_assn P) [] [] \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn P)) [] []
 2. \<And>P a as c cs. hn_invalid (list_assn P) as cs \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn P)) as cs \<Longrightarrow> hn_invalid (list_assn P) (a # as) (c # cs) \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn P)) (a # as) (c # cs)
 3. \<And>uu_ v va. hn_invalid (list_assn uu_) (v # va) [] \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn uu_)) (v # va) []
 4. \<And>uu_ v va. hn_invalid (list_assn uu_) [] (v # va) \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn uu_)) [] (v # va)
[PROOF STEP]
applyS simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>P a as c cs. hn_invalid (list_assn P) as cs \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn P)) as cs \<Longrightarrow> hn_invalid (list_assn P) (a # as) (c # cs) \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn P)) (a # as) (c # cs)
 2. \<And>uu_ v va. hn_invalid (list_assn uu_) (v # va) [] \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn uu_)) (v # va) []
 3. \<And>uu_ v va. hn_invalid (list_assn uu_) [] (v # va) \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn uu_)) [] (v # va)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn P_)) as_ cs_ \<Longrightarrow> hn_invalid (list_assn P_) (a_ # as_) (c_ # cs_) \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn P_)) (a_ # as_) (c_ # cs_)
[PROOF STEP]
apply1 (simp add: hn_ctxt_def cong del: invalid_assn_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow> invalid_assn (list_assn P_) (a_ # as_) (c_ # cs_) \<Longrightarrow>\<^sub>t invalid_assn P_ a_ c_ * list_assn (invalid_assn P_) as_ cs_
[PROOF STEP]
apply1 (rule entt_trans[OF invalid_list_split])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow> invalid_assn P_ a_ c_ * invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t invalid_assn P_ a_ c_ * list_assn (invalid_assn P_) as_ cs_
[PROOF STEP]
apply (rule entt_star_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow> invalid_assn P_ a_ c_ \<Longrightarrow>\<^sub>t invalid_assn P_ a_ c_
 2. invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow> invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_
[PROOF STEP]
applyS simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow> invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_
[PROOF STEP]
apply (rule entt_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow> invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t ?B12
 2. invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow> ?B12 \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_
[PROOF STEP]
applyS assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn (list_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow> list_assn (invalid_assn P_) as_ cs_ \<Longrightarrow>\<^sub>t list_assn (invalid_assn P_) as_ cs_
[PROOF STEP]
applyS simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uu_ v va. hn_invalid (list_assn uu_) (v # va) [] \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn uu_)) (v # va) []
 2. \<And>uu_ v va. hn_invalid (list_assn uu_) [] (v # va) \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn uu_)) [] (v # va)
[PROOF STEP]
applyS (simp add: hn_ctxt_def invalid_assn_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ v va. hn_invalid (list_assn uu_) [] (v # va) \<Longrightarrow>\<^sub>t hn_ctxt (list_assn (invalid_assn uu_)) [] (v # va)
[PROOF STEP]
applyS (simp add: hn_ctxt_def invalid_assn_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_comp[fcomp_norm_unfold]: "hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) = list_assn (hr_comp A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) = list_assn (hr_comp A B)
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) x xa = list_assn (hr_comp A B) x xa
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) x xa = list_assn (hr_comp A B) x xa
[PROOF STEP]
fix x l y m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) x xa = list_assn (hr_comp A B) x xa
[PROOF STEP]
have "hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (x # l) (y # m) =
      hr_comp A B x y * hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (x # l) (y # m) = hr_comp A B x y * hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l m
[PROOF STEP]
by (sep_auto
        simp: hr_comp_def list_rel_split_left_iff
        intro!: ent_ex_preI ent_iffI)
[PROOF STATE]
proof (state)
this:
hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (x # l) (y # m) = hr_comp A B x y * hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l m

goal (1 subgoal):
 1. \<And>x xa. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) x xa = list_assn (hr_comp A B) x xa
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (?x2 # ?l2) (?y2 # ?m2) = hr_comp A B ?x2 ?y2 * hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) ?l2 ?m2

goal (1 subgoal):
 1. \<And>x xa. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) x xa = list_assn (hr_comp A B) x xa
[PROOF STEP]
note aux = this
[PROOF STATE]
proof (state)
this:
hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (?x2 # ?l2) (?y2 # ?m2) = hr_comp A B ?x2 ?y2 * hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) ?l2 ?m2

goal (1 subgoal):
 1. \<And>x xa. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) x xa = list_assn (hr_comp A B) x xa
[PROOF STEP]
fix l li
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) x xa = list_assn (hr_comp A B) x xa
[PROOF STEP]
show "hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li
[PROOF STEP]
apply (induction l arbitrary: li; case_tac li; intro ent_iffI)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>li. li = [] \<Longrightarrow> hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) [] li \<Longrightarrow>\<^sub>A list_assn (hr_comp A B) [] li
 2. \<And>li. li = [] \<Longrightarrow> list_assn (hr_comp A B) [] li \<Longrightarrow>\<^sub>A hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) [] li
 3. \<And>li a list. li = a # list \<Longrightarrow> hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) [] li \<Longrightarrow>\<^sub>A list_assn (hr_comp A B) [] li
 4. \<And>li a list. li = a # list \<Longrightarrow> list_assn (hr_comp A B) [] li \<Longrightarrow>\<^sub>A hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) [] li
 5. \<And>a l li. \<lbrakk>\<And>li. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li; li = []\<rbrakk> \<Longrightarrow> hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (a # l) li \<Longrightarrow>\<^sub>A list_assn (hr_comp A B) (a # l) li
 6. \<And>a l li. \<lbrakk>\<And>li. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li; li = []\<rbrakk> \<Longrightarrow> list_assn (hr_comp A B) (a # l) li \<Longrightarrow>\<^sub>A hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (a # l) li
 7. \<And>a l li aa list. \<lbrakk>\<And>li. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li; li = aa # list\<rbrakk> \<Longrightarrow> hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (a # l) li \<Longrightarrow>\<^sub>A list_assn (hr_comp A B) (a # l) li
 8. \<And>a l li aa list. \<lbrakk>\<And>li. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li; li = aa # list\<rbrakk> \<Longrightarrow> list_assn (hr_comp A B) (a # l) li \<Longrightarrow>\<^sub>A hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (a # l) li
[PROOF STEP]
apply (sep_auto simp: hr_comp_def; fail)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l li aa list. \<lbrakk>\<And>li. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li; li = aa # list\<rbrakk> \<Longrightarrow> hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (a # l) li \<Longrightarrow>\<^sub>A list_assn (hr_comp A B) (a # l) li
 2. \<And>a l li aa list. \<lbrakk>\<And>li. hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li; li = aa # list\<rbrakk> \<Longrightarrow> list_assn (hr_comp A B) (a # l) li \<Longrightarrow>\<^sub>A hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) (a # l) li
[PROOF STEP]
by (simp_all add: aux)
[PROOF STATE]
proof (state)
this:
hr_comp (list_assn A) (\<langle>B\<rangle>list_rel) l li = list_assn (hr_comp A B) l li

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hn_ctxt_eq: "A x y = z \<Longrightarrow> hn_ctxt A x y = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A x y = z \<Longrightarrow> hn_ctxt A x y = z
[PROOF STEP]
by (simp add: hn_ctxt_def)


[STATEMENT]
lemma hn_case_list[sepref_prep_comb_rule, sepref_comb_rules]:
  fixes p p' P
  defines [simp]: "INVE \<equiv> hn_invalid (list_assn P) p p'"
  assumes FR: "\<Gamma> \<Longrightarrow>\<^sub>t hn_ctxt (list_assn P) p p' * F"
  assumes Rn: "p=[] \<Longrightarrow> hn_refine (hn_ctxt (list_assn P) p p' * F) f1' (hn_ctxt XX1 p p' * \<Gamma>1') R f1"
  assumes Rs: "\<And>x l x' l'. \<lbrakk> p=x#l; p'=x'#l' \<rbrakk> \<Longrightarrow>
    hn_refine (hn_ctxt P x x' * hn_ctxt (list_assn P) l l' * INVE * F) (f2' x' l') (hn_ctxt P1' x x' * hn_ctxt (list_assn P2') l l' * hn_ctxt XX2 p p' * \<Gamma>2') R (f2 x l)"
  assumes MERGE1[unfolded hn_ctxt_def]: "\<And>x x'. hn_ctxt P1' x x' \<or>\<^sub>A hn_ctxt P2' x x' \<Longrightarrow>\<^sub>t hn_ctxt P' x x'"
  assumes MERGE2: "\<Gamma>1' \<or>\<^sub>A \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'"
  shows "hn_refine \<Gamma> (case_list f1' f2' p') (hn_ctxt (list_assn P') p p' * \<Gamma>') R (case_list$f1$(\<lambda>\<^sub>2x l. f2 x l)$p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (case p' of [] \<Rightarrow> f1' | x # xa \<Rightarrow> f2' x xa) (hn_ctxt (list_assn P') p p' * \<Gamma>') R (case_list $ f1 $ (\<lambda>x. (#\<lambda>xa. (#f2 x xa#)#)) $ p)
[PROOF STEP]
apply (rule hn_refine_cons_pre[OF FR])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (list_assn P) p p' * F) (case p' of [] \<Rightarrow> f1' | x # xa \<Rightarrow> f2' x xa) (hn_ctxt (list_assn P') p p' * \<Gamma>') R (case_list $ f1 $ (\<lambda>x. (#\<lambda>xa. (#f2 x xa#)#)) $ p)
[PROOF STEP]
apply1 extract_hnr_invalids
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 h2. \<lbrakk>h2 \<Turnstile> F; hn_invalid (list_assn P) p p' = true\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn P) p p' * F) (case p' of [] \<Rightarrow> f1' | x # xa \<Rightarrow> f2' x xa) (hn_ctxt (list_assn P') p p' * \<Gamma>') R (case_list $ f1 $ (\<lambda>x. (#\<lambda>xa. (#f2 x xa#)#)) $ p)
[PROOF STEP]
apply (cases p; cases p'; simp add: list_assn.simps[THEN hn_ctxt_list])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h2. \<lbrakk>h2 \<Turnstile> F; hn_invalid (list_assn P) [] [] = true; p = []; p' = []\<rbrakk> \<Longrightarrow> hn_refine F f1' \<Gamma>' R f1
 2. \<And>h2 a list aa lista. \<lbrakk>h2 \<Turnstile> F; hn_invalid (list_assn P) (a # list) (aa # lista) = true; p = a # list; p' = aa # lista\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt P a aa * hn_ctxt (list_assn P) list lista * F) (f2' aa lista) (hn_ctxt P' a aa * hn_ctxt (list_assn P') list lista * \<Gamma>') R (f2 a list)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) [] [] = true; p = []; p' = []\<rbrakk> \<Longrightarrow> hn_refine F f1' \<Gamma>' R f1
[PROOF STEP]
apply (rule hn_refine_cons[OF _ Rn _ entt_refl]; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) [] [] = true; p = []; p' = []\<rbrakk> \<Longrightarrow> F \<Longrightarrow>\<^sub>t hn_ctxt (list_assn P) p p' * F
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) [] [] = true; p = []; p' = []\<rbrakk> \<Longrightarrow> hn_ctxt XX1 p p' * \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) [] [] = true; p = []; p' = []\<rbrakk> \<Longrightarrow> hn_ctxt XX1 p p' * \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply (subst mult.commute, rule entt_fr_drop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) [] [] = true; p = []; p' = []\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply (rule entt_trans[OF _ MERGE2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) [] [] = true; p = []; p' = []\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>1' \<or>\<^sub>A \<Gamma>2'
[PROOF STEP]
apply (simp add: ent_disjI1' ent_disjI2')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h2 a list aa lista. \<lbrakk>h2 \<Turnstile> F; hn_invalid (list_assn P) (a # list) (aa # lista) = true; p = a # list; p' = aa # lista\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt P a aa * hn_ctxt (list_assn P) list lista * F) (f2' aa lista) (hn_ctxt P' a aa * hn_ctxt (list_assn P') list lista * \<Gamma>') R (f2 a list)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt P a_ aa_ * hn_ctxt (list_assn P) list_ lista_ * F) (f2' aa_ lista_) (hn_ctxt P' a_ aa_ * hn_ctxt (list_assn P') list_ lista_ * \<Gamma>') R (f2 a_ list_)
[PROOF STEP]
apply (rule hn_refine_cons[OF _ Rs _ entt_refl]; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt P a_ aa_ * hn_ctxt (list_assn P) list_ lista_ * F \<Longrightarrow>\<^sub>t hn_ctxt P a_ aa_ * hn_ctxt (list_assn P) list_ lista_ * INVE * F
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt P1' a_ aa_ * hn_ctxt (list_assn P2') list_ lista_ * hn_ctxt XX2 p p' * \<Gamma>2' \<Longrightarrow>\<^sub>t hn_ctxt P' a_ aa_ * hn_ctxt (list_assn P') list_ lista_ * \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt P1' a_ aa_ * hn_ctxt (list_assn P2') list_ lista_ * hn_ctxt XX2 p p' * \<Gamma>2' \<Longrightarrow>\<^sub>t hn_ctxt P' a_ aa_ * hn_ctxt (list_assn P') list_ lista_ * \<Gamma>'
[PROOF STEP]
apply (rule entt_star_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt P1' a_ aa_ * hn_ctxt (list_assn P2') list_ lista_ * hn_ctxt XX2 p p' \<Longrightarrow>\<^sub>t hn_ctxt P' a_ aa_ * hn_ctxt (list_assn P') list_ lista_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_fr_drop)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt P1' a_ aa_ * hn_ctxt (list_assn P2') list_ lista_ \<Longrightarrow>\<^sub>t hn_ctxt P' a_ aa_ * hn_ctxt (list_assn P') list_ lista_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply (rule entt_star_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt P1' a_ aa_ \<Longrightarrow>\<^sub>t hn_ctxt P' a_ aa_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn P2') list_ lista_ \<Longrightarrow>\<^sub>t hn_ctxt (list_assn P') list_ lista_
 3. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; invalid_assn (\<lambda>b c. P a_ aa_ * list_assn P list_ lista_) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> P1' a_ aa_ \<Longrightarrow>\<^sub>t P' a_ aa_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn P2') list_ lista_ \<Longrightarrow>\<^sub>t hn_ctxt (list_assn P') list_ lista_
 3. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_trans[OF _ MERGE1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; invalid_assn (\<lambda>b c. P a_ aa_ * list_assn P list_ lista_) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> P1' a_ aa_ \<Longrightarrow>\<^sub>t P1' a_ aa_ \<or>\<^sub>A P2' a_ aa_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn P2') list_ lista_ \<Longrightarrow>\<^sub>t hn_ctxt (list_assn P') list_ lista_
 3. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn P2') list_ lista_ \<Longrightarrow>\<^sub>t hn_ctxt (list_assn P') list_ lista_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; invalid_assn (\<lambda>b c. P a_ aa_ * list_assn P list_ lista_) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> list_assn P2' list_ lista_ \<Longrightarrow>\<^sub>t list_assn P' list_ lista_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply (rule list_assn_monot)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x'. \<lbrakk>h2_ \<Turnstile> F; invalid_assn (\<lambda>b c. P a_ aa_ * list_assn P list_ lista_) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> P2' x x' \<Longrightarrow>\<^sub>t P' x x'
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_trans[OF _ MERGE1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x'. \<lbrakk>h2_ \<Turnstile> F; invalid_assn (\<lambda>b c. P a_ aa_ * list_assn P list_ lista_) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> P2' x x' \<Longrightarrow>\<^sub>t P1' x x' \<or>\<^sub>A P2' x x'
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_trans[OF _ MERGE2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (list_assn P) (a_ # list_) (aa_ # lista_) = true; p = a_ # list_; p' = aa_ # lista_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>1' \<or>\<^sub>A \<Gamma>2'
[PROOF STEP]
applyS (simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hn_Nil[sepref_fr_rules]:
  "hn_refine emp (return []) emp (list_assn P) (RETURN$[])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine emp (return []) emp (list_assn P) (RETURN $ [])
[PROOF STEP]
unfolding hn_refine_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (RETURN $ []) \<longrightarrow> <emp> return [] <\<lambda>r. emp * (\<exists>\<^sub>Ax. list_assn P x r * \<up> (RETURN x \<le> RETURN $ []))>\<^sub>t
[PROOF STEP]
by sep_auto


[STATEMENT]
lemma hn_Cons[sepref_fr_rules]: "hn_refine (hn_ctxt P x x' * hn_ctxt (list_assn P) xs xs')
  (return (x'#xs')) (hn_invalid P x x' * hn_invalid (list_assn P) xs xs') (list_assn P)
  (RETURN$((#) $x$xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt P x x' * hn_ctxt (list_assn P) xs xs') (return (x' # xs')) (hn_invalid P x x' * hn_invalid (list_assn P) xs xs') (list_assn P) (RETURN $ ((#) $ x $ xs))
[PROOF STEP]
unfolding hn_refine_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (RETURN $ ((#) $ x $ xs)) \<longrightarrow> <hn_ctxt P x x' * hn_ctxt (list_assn P) xs xs'> return (x' # xs') <\<lambda>r. hn_invalid P x x' * hn_invalid (list_assn P) xs xs' * (\<exists>\<^sub>Axa. list_assn P xa r * \<up> (RETURN xa \<le> RETURN $ ((#) $ x $ xs)))>\<^sub>t
[PROOF STEP]
apply (sep_auto simp: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x x' * list_assn P xs xs' \<Longrightarrow>\<^sub>A invalid_assn P x x' * invalid_assn (list_assn P) xs xs' * P x x' * list_assn P xs xs' * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF invalidate_clone'[of P]], frame_inference)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn P x x' * P x x' * true * list_assn P xs xs' \<Longrightarrow>\<^sub>A invalid_assn P x x' * invalid_assn (list_assn P) xs xs' * P x x' * list_assn P xs xs' * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF invalidate_clone'[of "list_assn P"]], frame_inference)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invalid_assn (list_assn P) xs xs' * list_assn P xs xs' * true * (invalid_assn P x x' * P x x' * true) \<Longrightarrow>\<^sub>A invalid_assn P x x' * invalid_assn (list_assn P) xs xs' * P x x' * list_assn P xs xs' * true
[PROOF STEP]
apply solve_entails
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_len:
  "list_assn P l l' = list_assn P l l' * \<up>(length l = length l')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P l l' = list_assn P l l' * \<up> (length l = length l')
[PROOF STEP]
apply (induct P\<equiv>P l l' rule: list_assn.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. list_assn P [] [] = list_assn P [] [] * \<up> (length [] = length [])
 2. \<And>a as c cs. list_assn P as cs = list_assn P as cs * \<up> (length as = length cs) \<Longrightarrow> list_assn P (a # as) (c # cs) = list_assn P (a # as) (c # cs) * \<up> (length (a # as) = length (c # cs))
 3. \<And>v va. list_assn P (v # va) [] = list_assn P (v # va) [] * \<up> (length (v # va) = length [])
 4. \<And>v va. list_assn P [] (v # va) = list_assn P [] (v # va) * \<up> (length [] = length (v # va))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as c cs. list_assn P as cs = list_assn P as cs * \<up> (length as = length cs) \<Longrightarrow> P a c * list_assn P as cs = P a c * list_assn P as cs * \<up> (length as = length cs)
[PROOF STEP]
subgoal for a as c cs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P as cs = list_assn P as cs * \<up> (length as = length cs) \<Longrightarrow> P a c * list_assn P as cs = P a c * list_assn P as cs * \<up> (length as = length cs)
[PROOF STEP]
by (erule_tac t="list_assn P as cs" in subst[OF sym]) simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_eqlen_simp:
  "vassn_tag (list_assn P l l') \<Longrightarrow> length l' = length l"
  "h \<Turnstile> (list_assn P l l') \<Longrightarrow> length l' = length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vassn_tag (list_assn P l l') \<Longrightarrow> length l' = length l) &&& (h \<Turnstile> list_assn P l l' \<Longrightarrow> length l' = length l)
[PROOF STEP]
apply (subst (asm) list_assn_aux_len; auto simp: vassn_tag_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hn_append[sepref_fr_rules]: "hn_refine (hn_ctxt (list_assn P) l1 l1' * hn_ctxt (list_assn P) l2 l2')
  (return (l1'@l2')) (hn_invalid (list_assn P) l1 l1' * hn_invalid (list_assn P) l2 l2') (list_assn P)
  (RETURN$((@) $l1$l2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (list_assn P) l1 l1' * hn_ctxt (list_assn P) l2 l2') (return (l1' @ l2')) (hn_invalid (list_assn P) l1 l1' * hn_invalid (list_assn P) l2 l2') (list_assn P) (RETURN $ ((@) $ l1 $ l2))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (RETURN $ ((@) $ l1 $ l2)) \<Longrightarrow> <hn_ctxt (list_assn P) l1 l1' * hn_ctxt (list_assn P) l2 l2'> return (l1' @ l2') <\<lambda>r. hn_invalid (list_assn P) l1 l1' * hn_invalid (list_assn P) l2 l2' * (\<exists>\<^sub>Ax. list_assn P x r * \<up> (RETURN x \<le> RETURN $ ((@) $ l1 $ l2)))>\<^sub>t
[PROOF STEP]
apply (sep_auto simp: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P l1 l1' * list_assn P l2 l2' \<Longrightarrow>\<^sub>A invalid_assn (list_assn P) l1 l1' * invalid_assn (list_assn P) l2 l2' * list_assn P (l1 @ l2) (l1' @ l2') * true
[PROOF STEP]
apply (subst list_assn_aux_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P l1 l1' * \<up> (length l1 = length l1') * list_assn P l2 l2' \<Longrightarrow>\<^sub>A invalid_assn (list_assn P) l1 l1' * invalid_assn (list_assn P) l2 l2' * list_assn P (l1 @ l2) (l1' @ l2') * true
[PROOF STEP]
apply (sep_auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l1 = length l1' \<Longrightarrow> list_assn P l1 l1' * list_assn P l2 l2' \<Longrightarrow>\<^sub>A invalid_assn (list_assn P) l1 l1' * invalid_assn (list_assn P) l2 l2' * list_assn P l1 l1' * list_assn P l2 l2' * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF invalidate_clone'[of "list_assn P"]], frame_inference)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l1 = length l1' \<Longrightarrow> invalid_assn (list_assn P) l2 l2' * list_assn P l2 l2' * true * list_assn P l1 l1' \<Longrightarrow>\<^sub>A invalid_assn (list_assn P) l1 l1' * invalid_assn (list_assn P) l2 l2' * list_assn P l1 l1' * list_assn P l2 l2' * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF invalidate_clone'[of "list_assn P"]], frame_inference)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l1 = length l1' \<Longrightarrow> invalid_assn (list_assn P) l1 l1' * list_assn P l1 l1' * true * (invalid_assn (list_assn P) l2 l2' * list_assn P l2 l2' * true) \<Longrightarrow>\<^sub>A invalid_assn (list_assn P) l1 l1' * invalid_assn (list_assn P) l2 l2' * list_assn P l1 l1' * list_assn P l2 l2' * true
[PROOF STEP]
apply solve_entails
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_cons_conv1:
  "list_assn R (a#l) m = (\<exists>\<^sub>Ab m'. R a b * list_assn R l m' * \<up>(m=b#m'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn R (a # l) m = (\<exists>\<^sub>Ab m'. R a b * list_assn R l m' * \<up> (m = b # m'))
[PROOF STEP]
apply (cases m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. m = [] \<Longrightarrow> list_assn R (a # l) m = (\<exists>\<^sub>Ab m'. R a b * list_assn R l m' * \<up> (m = b # m'))
 2. \<And>aa list. m = aa # list \<Longrightarrow> list_assn R (a # l) m = (\<exists>\<^sub>Ab m'. R a b * list_assn R l m' * \<up> (m = b # m'))
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa list. m = aa # list \<Longrightarrow> list_assn R (a # l) m = (\<exists>\<^sub>Ab m'. R a b * list_assn R l m' * \<up> (m = b # m'))
[PROOF STEP]
apply (sep_auto intro!: ent_iffI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_cons_conv2:
  "list_assn R l (b#m) = (\<exists>\<^sub>Aa l'. R a b * list_assn R l' m * \<up>(l=a#l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn R l (b # m) = (\<exists>\<^sub>Aa l'. R a b * list_assn R l' m * \<up> (l = a # l'))
[PROOF STEP]
apply (cases l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> list_assn R l (b # m) = (\<exists>\<^sub>Aa l'. R a b * list_assn R l' m * \<up> (l = a # l'))
 2. \<And>a list. l = a # list \<Longrightarrow> list_assn R l (b # m) = (\<exists>\<^sub>Aa l'. R a b * list_assn R l' m * \<up> (l = a # l'))
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> list_assn R l (b # m) = (\<exists>\<^sub>Aa l'. R a b * list_assn R l' m * \<up> (l = a # l'))
[PROOF STEP]
apply (sep_auto intro!: ent_iffI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_append_conv1:
  "list_assn R (l1@l2) m = (\<exists>\<^sub>Am1 m2. list_assn R l1 m1 * list_assn R l2 m2 * \<up>(m=m1@m2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn R (l1 @ l2) m = (\<exists>\<^sub>Am1 m2. list_assn R l1 m1 * list_assn R l2 m2 * \<up> (m = m1 @ m2))
[PROOF STEP]
apply (induction l1 arbitrary: m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m. list_assn R ([] @ l2) m = (\<exists>\<^sub>Am1 m2. list_assn R [] m1 * list_assn R l2 m2 * \<up> (m = m1 @ m2))
 2. \<And>a l1 m. (\<And>m. list_assn R (l1 @ l2) m = (\<exists>\<^sub>Am1 m2. list_assn R l1 m1 * list_assn R l2 m2 * \<up> (m = m1 @ m2))) \<Longrightarrow> list_assn R ((a # l1) @ l2) m = (\<exists>\<^sub>Am1 m2. list_assn R (a # l1) m1 * list_assn R l2 m2 * \<up> (m = m1 @ m2))
[PROOF STEP]
apply (sep_auto intro!: ent_iffI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l1 m. (\<And>m. list_assn R (l1 @ l2) m = (\<exists>\<^sub>Am1 m2. list_assn R l1 m1 * list_assn R l2 m2 * \<up> (m = m1 @ m2))) \<Longrightarrow> list_assn R ((a # l1) @ l2) m = (\<exists>\<^sub>Am1 m2. list_assn R (a # l1) m1 * list_assn R l2 m2 * \<up> (m = m1 @ m2))
[PROOF STEP]
apply (sep_auto intro!: ent_iffI simp: list_assn_aux_cons_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_assn_aux_append_conv2:
  "list_assn R l (m1@m2) = (\<exists>\<^sub>Al1 l2. list_assn R l1 m1 * list_assn R l2 m2 * \<up>(l=l1@l2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn R l (m1 @ m2) = (\<exists>\<^sub>Al1 l2. list_assn R l1 m1 * list_assn R l2 m2 * \<up> (l = l1 @ l2))
[PROOF STEP]
apply (induction m1 arbitrary: l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. list_assn R l ([] @ m2) = (\<exists>\<^sub>Al1 l2. list_assn R l1 [] * list_assn R l2 m2 * \<up> (l = l1 @ l2))
 2. \<And>a m1 l. (\<And>l. list_assn R l (m1 @ m2) = (\<exists>\<^sub>Al1 l2. list_assn R l1 m1 * list_assn R l2 m2 * \<up> (l = l1 @ l2))) \<Longrightarrow> list_assn R l ((a # m1) @ m2) = (\<exists>\<^sub>Al1 l2. list_assn R l1 (a # m1) * list_assn R l2 m2 * \<up> (l = l1 @ l2))
[PROOF STEP]
apply (sep_auto intro!: ent_iffI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a m1 l. (\<And>l. list_assn R l (m1 @ m2) = (\<exists>\<^sub>Al1 l2. list_assn R l1 m1 * list_assn R l2 m2 * \<up> (l = l1 @ l2))) \<Longrightarrow> list_assn R l ((a # m1) @ m2) = (\<exists>\<^sub>Al1 l2. list_assn R l1 (a # m1) * list_assn R l2 m2 * \<up> (l = l1 @ l2))
[PROOF STEP]
apply (sep_auto intro!: ent_iffI simp: list_assn_aux_cons_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sum_assn_pure[safe_constraint_rules]: "\<lbrakk>is_pure A; is_pure B\<rbrakk> \<Longrightarrow> is_pure (sum_assn A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_pure A; is_pure B\<rbrakk> \<Longrightarrow> is_pure (A +\<^sub>a B)
[PROOF STEP]
apply (auto simp: is_pure_iff_pure_assn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x'. \<lbrakk>\<forall>x x'. is_pure_assn (A x x'); \<forall>x x'. is_pure_assn (B x x')\<rbrakk> \<Longrightarrow> is_pure_assn ((A +\<^sub>a B) x x')
[PROOF STEP]
apply (rename_tac x x')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x'. \<lbrakk>\<forall>x x'. is_pure_assn (A x x'); \<forall>x x'. is_pure_assn (B x x')\<rbrakk> \<Longrightarrow> is_pure_assn ((A +\<^sub>a B) x x')
[PROOF STEP]
apply (case_tac x; case_tac x'; simp add: pure_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sum_assn_id[simp]: "sum_assn id_assn id_assn = id_assn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id_assn +\<^sub>a id_assn = id_assn
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (id_assn +\<^sub>a id_assn) x xa = id_assn x xa
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (id_assn +\<^sub>a id_assn) x y = id_assn x y
[PROOF STEP]
by (cases x; cases y; simp add: pure_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sum_assn_pure_conv[simp]: "sum_assn (pure A) (pure B) = pure (\<langle>A,B\<rangle>sum_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure A +\<^sub>a pure B = pure (\<langle>A, B\<rangle>sum_rel)
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (pure A +\<^sub>a pure B) x xa = pure (\<langle>A, B\<rangle>sum_rel) x xa
[PROOF STEP]
subgoal for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pure A +\<^sub>a pure B) a b = pure (\<langle>A, B\<rangle>sum_rel) a b
[PROOF STEP]
by (cases a; cases b; auto simp: pure_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sum_match_cong[sepref_frame_match_rules]:
  "\<lbrakk>
    \<And>x y. \<lbrakk>e = Inl x; e'=Inl y\<rbrakk> \<Longrightarrow> hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y;
    \<And>x y. \<lbrakk>e = Inr x; e'=Inr y\<rbrakk> \<Longrightarrow> hn_ctxt B x y \<Longrightarrow>\<^sub>t hn_ctxt B' x y
  \<rbrakk> \<Longrightarrow> hn_ctxt (sum_assn A B) e e' \<Longrightarrow>\<^sub>t hn_ctxt (sum_assn A' B') e e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. \<lbrakk>e = Inl x; e' = Inl y\<rbrakk> \<Longrightarrow> hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt A' x y; \<And>x y. \<lbrakk>e = Inr x; e' = Inr y\<rbrakk> \<Longrightarrow> hn_ctxt B x y \<Longrightarrow>\<^sub>t hn_ctxt B' x y\<rbrakk> \<Longrightarrow> hn_ctxt (A +\<^sub>a B) e e' \<Longrightarrow>\<^sub>t hn_ctxt (A' +\<^sub>a B') e e'
[PROOF STEP]
by (cases e; cases e'; simp add: hn_ctxt_def entt_star_mono)


[STATEMENT]
lemma enum_merge_cong[sepref_frame_merge_rules]:
  assumes "\<And>x y. \<lbrakk>e=Inl x; e'=Inl y\<rbrakk> \<Longrightarrow> hn_ctxt A x y \<or>\<^sub>A hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y"
  assumes "\<And>x y. \<lbrakk>e=Inr x; e'=Inr y\<rbrakk> \<Longrightarrow> hn_ctxt B x y \<or>\<^sub>A hn_ctxt B' x y \<Longrightarrow>\<^sub>t hn_ctxt Bm x y"
  shows "hn_ctxt (sum_assn A B) e e' \<or>\<^sub>A hn_ctxt (sum_assn A' B') e e' \<Longrightarrow>\<^sub>t hn_ctxt (sum_assn Am Bm) e e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (A +\<^sub>a B) e e' \<or>\<^sub>A hn_ctxt (A' +\<^sub>a B') e e' \<Longrightarrow>\<^sub>t hn_ctxt (Am +\<^sub>a Bm) e e'
[PROOF STEP]
apply (rule entt_disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. hn_ctxt (A +\<^sub>a B) e e' \<Longrightarrow>\<^sub>t hn_ctxt (Am +\<^sub>a Bm) e e'
 2. hn_ctxt (A' +\<^sub>a B') e e' \<Longrightarrow>\<^sub>t hn_ctxt (Am +\<^sub>a Bm) e e'
[PROOF STEP]
apply (rule sum_match_cong)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>e = Inl x; e' = Inl y\<rbrakk> \<Longrightarrow> hn_ctxt A x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y
 2. \<And>x y. \<lbrakk>e = Inr x; e' = Inr y\<rbrakk> \<Longrightarrow> hn_ctxt B x y \<Longrightarrow>\<^sub>t hn_ctxt Bm x y
 3. hn_ctxt (A' +\<^sub>a B') e e' \<Longrightarrow>\<^sub>t hn_ctxt (Am +\<^sub>a Bm) e e'
[PROOF STEP]
apply (rule entt_disjD1[OF assms(1)]; simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>e = Inr x; e' = Inr y\<rbrakk> \<Longrightarrow> hn_ctxt B x y \<Longrightarrow>\<^sub>t hn_ctxt Bm x y
 2. hn_ctxt (A' +\<^sub>a B') e e' \<Longrightarrow>\<^sub>t hn_ctxt (Am +\<^sub>a Bm) e e'
[PROOF STEP]
apply (rule entt_disjD1[OF assms(2)]; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (A' +\<^sub>a B') e e' \<Longrightarrow>\<^sub>t hn_ctxt (Am +\<^sub>a Bm) e e'
[PROOF STEP]
apply (rule sum_match_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>e = Inl x; e' = Inl y\<rbrakk> \<Longrightarrow> hn_ctxt A' x y \<Longrightarrow>\<^sub>t hn_ctxt Am x y
 2. \<And>x y. \<lbrakk>e = Inr x; e' = Inr y\<rbrakk> \<Longrightarrow> hn_ctxt B' x y \<Longrightarrow>\<^sub>t hn_ctxt Bm x y
[PROOF STEP]
apply (rule entt_disjD2[OF assms(1)]; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>e = Inr x; e' = Inr y\<rbrakk> \<Longrightarrow> hn_ctxt B' x y \<Longrightarrow>\<^sub>t hn_ctxt Bm x y
[PROOF STEP]
apply (rule entt_disjD2[OF assms(2)]; simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma entt_invalid_sum: "hn_invalid (sum_assn A B) e e' \<Longrightarrow>\<^sub>t hn_ctxt (sum_assn (invalid_assn A) (invalid_assn B)) e e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_invalid (A +\<^sub>a B) e e' \<Longrightarrow>\<^sub>t hn_ctxt (invalid_assn A +\<^sub>a invalid_assn B) e e'
[PROOF STEP]
apply (simp add: hn_ctxt_def invalid_assn_def[abs_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> (\<exists>a b. (a, b) \<Turnstile> (A +\<^sub>a B) e e') \<Longrightarrow>\<^sub>t ((\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> A x y) * true) +\<^sub>a (\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> B x y) * true)) e e'
[PROOF STEP]
apply (rule enttI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> (\<exists>a b. (a, b) \<Turnstile> (A +\<^sub>a B) e e') \<Longrightarrow>\<^sub>A ((\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> A x y) * true) +\<^sub>a (\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> B x y) * true)) e e' * true
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> (A +\<^sub>a B) e e' \<Longrightarrow> emp \<Longrightarrow>\<^sub>A ((\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> A x y) * true) +\<^sub>a (\<lambda>x y. \<up> (\<exists>a b. (a, b) \<Turnstile> B x y) * true)) e e' * true
[PROOF STEP]
apply (cases e; cases e'; auto simp: mod_star_conv pure_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [sepref_fr_rules]: "(return o Inl,RETURN o Inl) \<in> A\<^sup>d \<rightarrow>\<^sub>a sum_assn A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> Inl, RETURN \<circ> Inl) \<in> A\<^sup>d \<rightarrow>\<^sub>a A +\<^sub>a B
[PROOF STEP]
by sepref_to_hoare sep_auto


[STATEMENT]
lemma [sepref_fr_rules]: "(return o Inr,RETURN o Inr) \<in> B\<^sup>d \<rightarrow>\<^sub>a sum_assn A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> Inr, RETURN \<circ> Inr) \<in> B\<^sup>d \<rightarrow>\<^sub>a A +\<^sub>a B
[PROOF STEP]
by sepref_to_hoare sep_auto


[STATEMENT]
lemma [sepref_monadify_arity]: "case_sum \<equiv> \<lambda>\<^sub>2f1 f2 x. SP case_sum$(\<lambda>\<^sub>2x. f1$x)$(\<lambda>\<^sub>2x. f2$x)$x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case_sum \<equiv> \<lambda>x. (#\<lambda>xa. (#\<lambda>xb. (#SP case_sum $ (\<lambda>xa. (#x $ xa#)) $ (\<lambda>x. (#xa $ x#)) $ xb#)#)#)
[PROOF STEP]
by simp


[STATEMENT]
lemma [sepref_monadify_comb]: "case_sum$f1$f2$x \<equiv> (\<bind>) $(EVAL$x)$(\<lambda>\<^sub>2x. SP case_sum$f1$f2$x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case_sum $ f1 $ f2 $ x \<equiv> (\<bind>) $ (EVAL $ x) $ (\<lambda>x. (#SP case_sum $ f1 $ f2 $ x#))
[PROOF STEP]
by simp


[STATEMENT]
lemma [sepref_monadify_comb]: "EVAL$(case_sum$(\<lambda>\<^sub>2x. f1 x)$(\<lambda>\<^sub>2x. f2 x)$x)
  \<equiv> (\<bind>) $(EVAL$x)$(\<lambda>\<^sub>2x. SP case_sum$(\<lambda>\<^sub>2x. EVAL $ f1 x)$(\<lambda>\<^sub>2x. EVAL $ f2 x)$x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EVAL $ (case_sum $ (\<lambda>x. (#f1 x#)) $ (\<lambda>x. (#f2 x#)) $ x) \<equiv> (\<bind>) $ (EVAL $ x) $ (\<lambda>x. (#SP case_sum $ (\<lambda>x. (#EVAL $ f1 x#)) $ (\<lambda>x. (#EVAL $ f2 x#)) $ x#))
[PROOF STEP]
apply (rule eq_reflection)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EVAL $ (case_sum $ (\<lambda>x. (#f1 x#)) $ (\<lambda>x. (#f2 x#)) $ x) = (\<bind>) $ (EVAL $ x) $ (\<lambda>x. (#SP case_sum $ (\<lambda>x. (#EVAL $ f1 x#)) $ (\<lambda>x. (#EVAL $ f2 x#)) $ x#))
[PROOF STEP]
by (simp split: sum.splits)


[STATEMENT]
lemma sum_assn_ctxt: "sum_assn A B x y = z \<Longrightarrow> hn_ctxt (sum_assn A B) x y = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A +\<^sub>a B) x y = z \<Longrightarrow> hn_ctxt (A +\<^sub>a B) x y = z
[PROOF STEP]
by (simp add: hn_ctxt_def)


[STATEMENT]
lemma sum_cases_hnr:
  fixes A B e e'
  defines [simp]: "INVe \<equiv> hn_invalid (sum_assn A B) e e'"
  assumes FR: "\<Gamma> \<Longrightarrow>\<^sub>t hn_ctxt (sum_assn A B) e e' * F"
  assumes E1: "\<And>x1 x1a. \<lbrakk>e = Inl x1; e' = Inl x1a\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt A x1 x1a * INVe * F) (f1' x1a) (hn_ctxt A' x1 x1a * hn_ctxt XX1 e e' * \<Gamma>1') R (f1 x1)"
  assumes E2: "\<And>x2 x2a. \<lbrakk>e = Inr x2; e' = Inr x2a\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt B x2 x2a * INVe * F) (f2' x2a) (hn_ctxt B' x2 x2a * hn_ctxt XX2 e e' * \<Gamma>2') R (f2 x2)"
  assumes MERGE[unfolded hn_ctxt_def]: "\<Gamma>1' \<or>\<^sub>A \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'"
  shows "hn_refine \<Gamma> (case_sum f1' f2' e') (hn_ctxt (sum_assn A' B') e e' * \<Gamma>') R (case_sum$(\<lambda>\<^sub>2x. f1 x)$(\<lambda>\<^sub>2x. f2 x)$e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine \<Gamma> (case e' of Inl x \<Rightarrow> f1' x | Inr x \<Rightarrow> f2' x) (hn_ctxt (A' +\<^sub>a B') e e' * \<Gamma>') R (case_sum $ (\<lambda>x. (#f1 x#)) $ (\<lambda>x. (#f2 x#)) $ e)
[PROOF STEP]
apply (rule hn_refine_cons_pre[OF FR])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (hn_ctxt (A +\<^sub>a B) e e' * F) (case e' of Inl x \<Rightarrow> f1' x | Inr x \<Rightarrow> f2' x) (hn_ctxt (A' +\<^sub>a B') e e' * \<Gamma>') R (case_sum $ (\<lambda>x. (#f1 x#)) $ (\<lambda>x. (#f2 x#)) $ e)
[PROOF STEP]
apply1 extract_hnr_invalids
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h1 h2. \<lbrakk>h2 \<Turnstile> F; hn_invalid (A +\<^sub>a B) e e' = true\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (A +\<^sub>a B) e e' * F) (case e' of Inl x \<Rightarrow> f1' x | Inr x \<Rightarrow> f2' x) (hn_ctxt (A' +\<^sub>a B') e e' * \<Gamma>') R (case_sum $ (\<lambda>x. (#f1 x#)) $ (\<lambda>x. (#f2 x#)) $ e)
[PROOF STEP]
apply (cases e; cases e'; simp add: sum_assn.simps[THEN sum_assn_ctxt])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h2 a aa. \<lbrakk>h2 \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a) (Inl aa) = true; e = Inl a; e' = Inl aa\<rbrakk> \<Longrightarrow> hn_refine (A a aa * F) (f1' aa) (A' a aa * \<Gamma>') R (f1 a)
 2. \<And>h2 b ba. \<lbrakk>h2 \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b) (Inr ba) = true; e = Inr b; e' = Inr ba\<rbrakk> \<Longrightarrow> hn_refine (B b ba * F) (f2' ba) (B' b ba * \<Gamma>') R (f2 b)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> hn_refine (A a_ aa_ * F) (f1' aa_) (A' a_ aa_ * \<Gamma>') R (f1 a_)
[PROOF STEP]
apply (rule hn_refine_cons[OF _ E1 _ entt_refl]; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> A a_ aa_ * F \<Longrightarrow>\<^sub>t hn_ctxt A a_ aa_ * INVe * F
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> hn_ctxt A' a_ aa_ * hn_ctxt XX1 e e' * \<Gamma>1' \<Longrightarrow>\<^sub>t A' a_ aa_ * \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def) \<comment> \<open>Match precondition for case, get \<open>enum_assn\<close> from assumption generated by \<open>extract_hnr_invalids\<close>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> hn_ctxt A' a_ aa_ * hn_ctxt XX1 e e' * \<Gamma>1' \<Longrightarrow>\<^sub>t A' a_ aa_ * \<Gamma>'
[PROOF STEP]
apply (rule entt_star_mono) \<comment> \<open>Split postcondition into pairs for compounds and frame, drop \<open>hn_ctxt XX\<close>\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> hn_ctxt A' a_ aa_ * hn_ctxt XX1 e e' \<Longrightarrow>\<^sub>t A' a_ aa_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_fr_drop)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> hn_ctxt A' a_ aa_ \<Longrightarrow>\<^sub>t A' a_ aa_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def entt_disjI1' entt_disjI2')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_trans[OF _ MERGE])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inl a_) (Inl aa_) = true; e = Inl a_; e' = Inl aa_\<rbrakk> \<Longrightarrow> \<Gamma>1' \<Longrightarrow>\<^sub>t \<Gamma>1' \<or>\<^sub>A \<Gamma>2'
[PROOF STEP]
applyS (simp add: entt_disjI1' entt_disjI2')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h2 b ba. \<lbrakk>h2 \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b) (Inr ba) = true; e = Inr b; e' = Inr ba\<rbrakk> \<Longrightarrow> hn_refine (B b ba * F) (f2' ba) (B' b ba * \<Gamma>') R (f2 b)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> hn_refine (B b_ ba_ * F) (f2' ba_) (B' b_ ba_ * \<Gamma>') R (f2 b_)
[PROOF STEP]
apply (rule hn_refine_cons[OF _ E2 _ entt_refl]; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> B b_ ba_ * F \<Longrightarrow>\<^sub>t hn_ctxt B b_ ba_ * INVe * F
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> hn_ctxt B' b_ ba_ * hn_ctxt XX2 e e' * \<Gamma>2' \<Longrightarrow>\<^sub>t B' b_ ba_ * \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> hn_ctxt B' b_ ba_ * hn_ctxt XX2 e e' * \<Gamma>2' \<Longrightarrow>\<^sub>t B' b_ ba_ * \<Gamma>'
[PROOF STEP]
apply (rule entt_star_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> hn_ctxt B' b_ ba_ * hn_ctxt XX2 e e' \<Longrightarrow>\<^sub>t B' b_ ba_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_fr_drop)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> hn_ctxt B' b_ ba_ \<Longrightarrow>\<^sub>t B' b_ ba_
 2. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
applyS (simp add: hn_ctxt_def entt_disjI1' entt_disjI2')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>'
[PROOF STEP]
apply1 (rule entt_trans[OF _ MERGE])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h2_ \<Turnstile> F; hn_invalid (A +\<^sub>a B) (Inr b_) (Inr ba_) = true; e = Inr b_; e' = Inr ba_\<rbrakk> \<Longrightarrow> \<Gamma>2' \<Longrightarrow>\<^sub>t \<Gamma>1' \<or>\<^sub>A \<Gamma>2'
[PROOF STEP]
applyS (simp add: entt_disjI1' entt_disjI2')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isl_hnr[sepref_fr_rules]: "(return o isl,RETURN o isl) \<in> (sum_assn A B)\<^sup>k \<rightarrow>\<^sub>a bool_assn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> isl, RETURN \<circ> isl) \<in> (A +\<^sub>a B)\<^sup>k \<rightarrow>\<^sub>a bool_assn
[PROOF STEP]
apply sepref_to_hoare
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xi. \<lbrakk>x ::\<^sub>i TYPE('c + 'd); nofail (RETURN (isl x))\<rbrakk> \<Longrightarrow> <(A +\<^sub>a B) x xi> return (isl xi) <\<lambda>r. (A +\<^sub>a B) x xi * (\<exists>\<^sub>Axa. \<up> ((r, xa) \<in> bool_rel) * \<up> (RETURN xa \<le> RETURN (isl x)))>\<^sub>t
[PROOF STEP]
subgoal for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a ::\<^sub>i TYPE('c + 'd); nofail (RETURN (isl a))\<rbrakk> \<Longrightarrow> <(A +\<^sub>a B) a b> return (isl b) <\<lambda>r. (A +\<^sub>a B) a b * (\<exists>\<^sub>Ax. \<up> ((r, x) \<in> bool_rel) * \<up> (RETURN x \<le> RETURN (isl a)))>\<^sub>t
[PROOF STEP]
by (cases a; cases b; sep_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma projl_hnr[sepref_fr_rules]: "(return o projl,RETURN o projl) \<in> [isl]\<^sub>a (sum_assn A B)\<^sup>d \<rightarrow> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> projl, RETURN \<circ> projl) \<in> [isl]\<^sub>a (A +\<^sub>a B)\<^sup>d \<rightarrow> A
[PROOF STEP]
apply sepref_to_hoare
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xi. \<lbrakk>isl x; x ::\<^sub>i TYPE('c + 'd); nofail (RETURN (projl x))\<rbrakk> \<Longrightarrow> <(A +\<^sub>a B) x xi> return (projl xi) <\<lambda>r. true * (\<exists>\<^sub>Axa. A xa r * \<up> (RETURN xa \<le> RETURN (projl x)))>\<^sub>t
[PROOF STEP]
subgoal for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isl a; a ::\<^sub>i TYPE('c + 'd); nofail (RETURN (projl a))\<rbrakk> \<Longrightarrow> <(A +\<^sub>a B) a b> return (projl b) <\<lambda>r. true * (\<exists>\<^sub>Ax. A x r * \<up> (RETURN x \<le> RETURN (projl a)))>\<^sub>t
[PROOF STEP]
by (cases a; cases b; sep_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma projr_hnr[sepref_fr_rules]: "(return o projr,RETURN o projr) \<in> [Not o isl]\<^sub>a (sum_assn A B)\<^sup>d \<rightarrow> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> projr, RETURN \<circ> projr) \<in> [Not \<circ> isl]\<^sub>a (A +\<^sub>a B)\<^sup>d \<rightarrow> B
[PROOF STEP]
apply sepref_to_hoare
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xi. \<lbrakk>(Not \<circ> isl) x; x ::\<^sub>i TYPE('c + 'd); nofail (RETURN (projr x))\<rbrakk> \<Longrightarrow> <(A +\<^sub>a B) x xi> return (projr xi) <\<lambda>r. true * (\<exists>\<^sub>Axa. B xa r * \<up> (RETURN xa \<le> RETURN (projr x)))>\<^sub>t
[PROOF STEP]
subgoal for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Not \<circ> isl) a; a ::\<^sub>i TYPE('c + 'd); nofail (RETURN (projr a))\<rbrakk> \<Longrightarrow> <(A +\<^sub>a B) a b> return (projr b) <\<lambda>r. true * (\<exists>\<^sub>Ax. B x r * \<up> (RETURN x \<le> RETURN (projr a)))>\<^sub>t
[PROOF STEP]
by (cases a; cases b; sep_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma empty_literal_hnr [sepref_import_param]:
  "(String.empty_literal, PR_CONST String.empty_literal) \<in> Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (STR '''', PR_CONST STR '''') \<in> Id
[PROOF STEP]
by simp


[STATEMENT]
lemma empty_literal_pat [def_pat_rules]:
  "String.empty_literal \<equiv> UNPROTECT String.empty_literal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. STR '''' \<equiv> UNPROTECT STR ''''
[PROOF STEP]
by simp


[STATEMENT]
lemma Literal_hnr [sepref_import_param]:
  "(String.Literal b0 b1 b2 b3 b4 b5 b6 s,
    PR_CONST (String.Literal b0 b1 b2 b3 b4 b5 b6 s)) \<in> Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (String.Literal b0 b1 b2 b3 b4 b5 b6 s, PR_CONST (String.Literal b0 b1 b2 b3 b4 b5 b6 s)) \<in> Id
[PROOF STEP]
by simp


[STATEMENT]
lemma Literal_pat [def_pat_rules]:
  "String.Literal $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ s \<equiv>
    UNPROTECT (String.Literal $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. String.Literal $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ s \<equiv> UNPROTECT (String.Literal $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ s)
[PROOF STEP]
by simp


[STATEMENT]
lemma fixes is_lub
  shows WT_compP: "is_lub,P,E \<turnstile> e :: T \<Longrightarrow> is_lub,compP f P,E \<turnstile> e :: T"
  and WTs_compP: "is_lub,P,E \<turnstile> es [::] Ts \<Longrightarrow> is_lub,compP f P,E \<turnstile> es [::] Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_lub,P,E \<turnstile> e :: T \<Longrightarrow> is_lub,compP f P,E \<turnstile> e :: T) &&& (is_lub,P,E \<turnstile> es [::] Ts \<Longrightarrow> is_lub,compP f P,E \<turnstile> es [::] Ts)
[PROOF STEP]
proof(induct rule: WT_WTs.inducts)
[PROOF STATE]
proof (state)
goal (24 subgoals):
 1. \<And>C E. is_class P C \<Longrightarrow> is_lub,compP f P,E \<turnstile> new C :: Class C
 2. \<And>E e T. \<lbrakk>is_lub,P,E \<turnstile> e :: Integer; is_lub,compP f P,E \<turnstile> e :: Integer; is_type P (T\<lfloor>\<rceil>)\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> newA T\<lfloor>e\<rceil> :: T\<lfloor>\<rceil>
 3. \<And>E e T U. \<lbrakk>is_lub,P,E \<turnstile> e :: T; is_lub,compP f P,E \<turnstile> e :: T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Cast U e :: U
 4. \<And>E e T U. \<lbrakk>is_lub,P,E \<turnstile> e :: T; is_lub,compP f P,E \<turnstile> e :: T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e instanceof U :: Boolean
 5. \<And>v T E. typeof v = \<lfloor>T\<rfloor> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Val v :: T
 6. \<And>E V T. E V = \<lfloor>T\<rfloor> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Var V :: T
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>is_lub,P,E \<turnstile> e1 :: T1; is_lub,compP f P,E \<turnstile> e1 :: T1; is_lub,P,E \<turnstile> e2 :: T2; is_lub,compP f P,E \<turnstile> e2 :: T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e1 \<guillemotleft>bop\<guillemotright> e2 :: T
 8. \<And>E V T e T'. \<lbrakk>E V = \<lfloor>T\<rfloor>; is_lub,P,E \<turnstile> e :: T'; is_lub,compP f P,E \<turnstile> e :: T'; P \<turnstile> T' \<le> T; V \<noteq> this\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> V:=e :: Void
 9. \<And>E a T i. \<lbrakk>is_lub,P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,compP f P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,P,E \<turnstile> i :: Integer; is_lub,compP f P,E \<turnstile> i :: Integer\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> a\<lfloor>i\<rceil> :: T
 10. \<And>E a T i e T'. \<lbrakk>is_lub,P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,compP f P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,P,E \<turnstile> i :: Integer; is_lub,compP f P,E \<turnstile> i :: Integer; is_lub,P,E \<turnstile> e :: T'; is_lub,compP f P,E \<turnstile> e :: T'; P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> a\<lfloor>i\<rceil> := e :: Void
A total of 24 subgoals...
[PROOF STEP]
case (WTCall E e U C M Ts T meth D es Ts')
[PROOF STATE]
proof (state)
this:
is_lub,P,E \<turnstile> e :: U
is_lub,compP f P,E \<turnstile> e :: U
class_type_of' U = \<lfloor>C\<rfloor>
P \<turnstile> C sees M: Ts\<rightarrow>T = meth in D
is_lub,P,E \<turnstile> es [::] Ts'
is_lub,compP f P,E \<turnstile> es [::] Ts'
P \<turnstile> Ts' [\<le>] Ts

goal (24 subgoals):
 1. \<And>C E. is_class P C \<Longrightarrow> is_lub,compP f P,E \<turnstile> new C :: Class C
 2. \<And>E e T. \<lbrakk>is_lub,P,E \<turnstile> e :: Integer; is_lub,compP f P,E \<turnstile> e :: Integer; is_type P (T\<lfloor>\<rceil>)\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> newA T\<lfloor>e\<rceil> :: T\<lfloor>\<rceil>
 3. \<And>E e T U. \<lbrakk>is_lub,P,E \<turnstile> e :: T; is_lub,compP f P,E \<turnstile> e :: T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Cast U e :: U
 4. \<And>E e T U. \<lbrakk>is_lub,P,E \<turnstile> e :: T; is_lub,compP f P,E \<turnstile> e :: T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e instanceof U :: Boolean
 5. \<And>v T E. typeof v = \<lfloor>T\<rfloor> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Val v :: T
 6. \<And>E V T. E V = \<lfloor>T\<rfloor> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Var V :: T
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>is_lub,P,E \<turnstile> e1 :: T1; is_lub,compP f P,E \<turnstile> e1 :: T1; is_lub,P,E \<turnstile> e2 :: T2; is_lub,compP f P,E \<turnstile> e2 :: T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e1 \<guillemotleft>bop\<guillemotright> e2 :: T
 8. \<And>E V T e T'. \<lbrakk>E V = \<lfloor>T\<rfloor>; is_lub,P,E \<turnstile> e :: T'; is_lub,compP f P,E \<turnstile> e :: T'; P \<turnstile> T' \<le> T; V \<noteq> this\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> V:=e :: Void
 9. \<And>E a T i. \<lbrakk>is_lub,P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,compP f P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,P,E \<turnstile> i :: Integer; is_lub,compP f P,E \<turnstile> i :: Integer\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> a\<lfloor>i\<rceil> :: T
 10. \<And>E a T i e T'. \<lbrakk>is_lub,P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,compP f P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,P,E \<turnstile> i :: Integer; is_lub,compP f P,E \<turnstile> i :: Integer; is_lub,P,E \<turnstile> e :: T'; is_lub,compP f P,E \<turnstile> e :: T'; P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> a\<lfloor>i\<rceil> := e :: Void
A total of 24 subgoals...
[PROOF STEP]
from \<open>P \<turnstile> C sees M: Ts\<rightarrow>T = meth in D\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C sees M: Ts\<rightarrow>T = meth in D
[PROOF STEP]
have "compP f P \<turnstile> C sees M: Ts\<rightarrow>T = map_option (f D M Ts T) meth in D"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees M: Ts\<rightarrow>T = meth in D

goal (1 subgoal):
 1. compP f P \<turnstile> C sees M: Ts\<rightarrow>T = map_option (f D M Ts T) meth in D
[PROOF STEP]
by(auto dest: sees_method_compP[where f=f])
[PROOF STATE]
proof (state)
this:
compP f P \<turnstile> C sees M: Ts\<rightarrow>T = map_option (f D M Ts T) meth in D

goal (24 subgoals):
 1. \<And>C E. is_class P C \<Longrightarrow> is_lub,compP f P,E \<turnstile> new C :: Class C
 2. \<And>E e T. \<lbrakk>is_lub,P,E \<turnstile> e :: Integer; is_lub,compP f P,E \<turnstile> e :: Integer; is_type P (T\<lfloor>\<rceil>)\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> newA T\<lfloor>e\<rceil> :: T\<lfloor>\<rceil>
 3. \<And>E e T U. \<lbrakk>is_lub,P,E \<turnstile> e :: T; is_lub,compP f P,E \<turnstile> e :: T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Cast U e :: U
 4. \<And>E e T U. \<lbrakk>is_lub,P,E \<turnstile> e :: T; is_lub,compP f P,E \<turnstile> e :: T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e instanceof U :: Boolean
 5. \<And>v T E. typeof v = \<lfloor>T\<rfloor> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Val v :: T
 6. \<And>E V T. E V = \<lfloor>T\<rfloor> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Var V :: T
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>is_lub,P,E \<turnstile> e1 :: T1; is_lub,compP f P,E \<turnstile> e1 :: T1; is_lub,P,E \<turnstile> e2 :: T2; is_lub,compP f P,E \<turnstile> e2 :: T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e1 \<guillemotleft>bop\<guillemotright> e2 :: T
 8. \<And>E V T e T'. \<lbrakk>E V = \<lfloor>T\<rfloor>; is_lub,P,E \<turnstile> e :: T'; is_lub,compP f P,E \<turnstile> e :: T'; P \<turnstile> T' \<le> T; V \<noteq> this\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> V:=e :: Void
 9. \<And>E a T i. \<lbrakk>is_lub,P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,compP f P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,P,E \<turnstile> i :: Integer; is_lub,compP f P,E \<turnstile> i :: Integer\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> a\<lfloor>i\<rceil> :: T
 10. \<And>E a T i e T'. \<lbrakk>is_lub,P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,compP f P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,P,E \<turnstile> i :: Integer; is_lub,compP f P,E \<turnstile> i :: Integer; is_lub,P,E \<turnstile> e :: T'; is_lub,compP f P,E \<turnstile> e :: T'; P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> a\<lfloor>i\<rceil> := e :: Void
A total of 24 subgoals...
[PROOF STEP]
with WTCall
[PROOF STATE]
proof (chain)
picking this:
is_lub,P,E \<turnstile> e :: U
is_lub,compP f P,E \<turnstile> e :: U
class_type_of' U = \<lfloor>C\<rfloor>
P \<turnstile> C sees M: Ts\<rightarrow>T = meth in D
is_lub,P,E \<turnstile> es [::] Ts'
is_lub,compP f P,E \<turnstile> es [::] Ts'
P \<turnstile> Ts' [\<le>] Ts
compP f P \<turnstile> C sees M: Ts\<rightarrow>T = map_option (f D M Ts T) meth in D
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_lub,P,E \<turnstile> e :: U
is_lub,compP f P,E \<turnstile> e :: U
class_type_of' U = \<lfloor>C\<rfloor>
P \<turnstile> C sees M: Ts\<rightarrow>T = meth in D
is_lub,P,E \<turnstile> es [::] Ts'
is_lub,compP f P,E \<turnstile> es [::] Ts'
P \<turnstile> Ts' [\<le>] Ts
compP f P \<turnstile> C sees M: Ts\<rightarrow>T = map_option (f D M Ts T) meth in D

goal (1 subgoal):
 1. is_lub,compP f P,E \<turnstile> e\<bullet>M(es) :: T
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
is_lub,compP f P,E \<turnstile> e\<bullet>M(es) :: T

goal (23 subgoals):
 1. \<And>C E. is_class P C \<Longrightarrow> is_lub,compP f P,E \<turnstile> new C :: Class C
 2. \<And>E e T. \<lbrakk>is_lub,P,E \<turnstile> e :: Integer; is_lub,compP f P,E \<turnstile> e :: Integer; is_type P (T\<lfloor>\<rceil>)\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> newA T\<lfloor>e\<rceil> :: T\<lfloor>\<rceil>
 3. \<And>E e T U. \<lbrakk>is_lub,P,E \<turnstile> e :: T; is_lub,compP f P,E \<turnstile> e :: T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Cast U e :: U
 4. \<And>E e T U. \<lbrakk>is_lub,P,E \<turnstile> e :: T; is_lub,compP f P,E \<turnstile> e :: T; P \<turnstile> U \<le> T \<or> P \<turnstile> T \<le> U; is_type P U; is_refT U\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e instanceof U :: Boolean
 5. \<And>v T E. typeof v = \<lfloor>T\<rfloor> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Val v :: T
 6. \<And>E V T. E V = \<lfloor>T\<rfloor> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Var V :: T
 7. \<And>E e1 T1 e2 T2 bop T. \<lbrakk>is_lub,P,E \<turnstile> e1 :: T1; is_lub,compP f P,E \<turnstile> e1 :: T1; is_lub,P,E \<turnstile> e2 :: T2; is_lub,compP f P,E \<turnstile> e2 :: T2; P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 :: T\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e1 \<guillemotleft>bop\<guillemotright> e2 :: T
 8. \<And>E V T e T'. \<lbrakk>E V = \<lfloor>T\<rfloor>; is_lub,P,E \<turnstile> e :: T'; is_lub,compP f P,E \<turnstile> e :: T'; P \<turnstile> T' \<le> T; V \<noteq> this\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> V:=e :: Void
 9. \<And>E a T i. \<lbrakk>is_lub,P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,compP f P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,P,E \<turnstile> i :: Integer; is_lub,compP f P,E \<turnstile> i :: Integer\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> a\<lfloor>i\<rceil> :: T
 10. \<And>E a T i e T'. \<lbrakk>is_lub,P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,compP f P,E \<turnstile> a :: T\<lfloor>\<rceil>; is_lub,P,E \<turnstile> i :: Integer; is_lub,compP f P,E \<turnstile> i :: Integer; is_lub,P,E \<turnstile> e :: T'; is_lub,compP f P,E \<turnstile> e :: T'; P \<turnstile> T' \<le> T\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> a\<lfloor>i\<rceil> := e :: Void
A total of 23 subgoals...
[PROOF STEP]
qed(auto simp del: fun_upd_apply)


[STATEMENT]
lemma fixes is_lub
  shows Anno_compP: "is_lub,P,E \<turnstile> e \<leadsto> e' \<Longrightarrow> is_lub,compP f P,E \<turnstile> e \<leadsto> e'"
  and Annos_compP: "is_lub,P,E \<turnstile> es [\<leadsto>] es' \<Longrightarrow> is_lub,compP f P,E \<turnstile> es [\<leadsto>] es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_lub,P,E \<turnstile> e \<leadsto> e' \<Longrightarrow> is_lub,compP f P,E \<turnstile> e \<leadsto> e') &&& (is_lub,P,E \<turnstile> es [\<leadsto>] es' \<Longrightarrow> is_lub,compP f P,E \<turnstile> es [\<leadsto>] es')
[PROOF STEP]
apply(induct rule: Anno_Annos.inducts)
[PROOF STATE]
proof (prove)
goal (29 subgoals):
 1. \<And>E C. is_lub,compP f P,E \<turnstile> new C \<leadsto> new C
 2. \<And>E i i' T. \<lbrakk>is_lub,P,E \<turnstile> i \<leadsto> i'; is_lub,compP f P,E \<turnstile> i \<leadsto> i'\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> newA T\<lfloor>i\<rceil> \<leadsto> newA T\<lfloor>i'\<rceil>
 3. \<And>E e e' C. \<lbrakk>is_lub,P,E \<turnstile> e \<leadsto> e'; is_lub,compP f P,E \<turnstile> e \<leadsto> e'\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Cast C e \<leadsto> Cast C e'
 4. \<And>E e e' T. \<lbrakk>is_lub,P,E \<turnstile> e \<leadsto> e'; is_lub,compP f P,E \<turnstile> e \<leadsto> e'\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e instanceof T \<leadsto> e' instanceof T
 5. \<And>E v. is_lub,compP f P,E \<turnstile> Val v \<leadsto> Val v
 6. \<And>E V T. \<lbrakk>E V = \<lfloor>T\<rfloor>; V \<noteq> Annotate.super\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Var V \<leadsto> Var V
 7. \<And>E V C T fm D. \<lbrakk>E V = None; V \<noteq> Annotate.super; E this = \<lfloor>Class C\<rfloor>; P \<turnstile> C sees V:T (fm) in D\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> Var V \<leadsto> Var this\<bullet>V{D}
 8. \<And>E e1 e1' e2 e2' bop. \<lbrakk>is_lub,P,E \<turnstile> e1 \<leadsto> e1'; is_lub,compP f P,E \<turnstile> e1 \<leadsto> e1'; is_lub,P,E \<turnstile> e2 \<leadsto> e2'; is_lub,compP f P,E \<turnstile> e2 \<leadsto> e2'\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> e1 \<guillemotleft>bop\<guillemotright> e2 \<leadsto> e1' \<guillemotleft>bop\<guillemotright> e2'
 9. \<And>E V T e e'. \<lbrakk>E V = \<lfloor>T\<rfloor>; V \<noteq> Annotate.super; is_lub,P,E \<turnstile> e \<leadsto> e'; is_lub,compP f P,E \<turnstile> e \<leadsto> e'\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> V:=e \<leadsto> V:=e'
 10. \<And>E V C T fm D e e'. \<lbrakk>E V = None; V \<noteq> Annotate.super; E this = \<lfloor>Class C\<rfloor>; P \<turnstile> C sees V:T (fm) in D; is_lub,P,E \<turnstile> e \<leadsto> e'; is_lub,compP f P,E \<turnstile> e \<leadsto> e'\<rbrakk> \<Longrightarrow> is_lub,compP f P,E \<turnstile> V:=e \<leadsto> Var this\<bullet>V{D} := e'
A total of 29 subgoals...
[PROOF STEP]
apply(auto intro: Anno_Annos.intros simp del: fun_upd_apply dest: WT_compP simp add: compC_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma annotate_prog_code_eq_annotate_prog:
  assumes wf: "wf_J_prog (annotate_prog_code P)"
  shows "annotate_prog_code P = annotate_prog P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
let ?wf_md = "\<lambda>_ _ (_,_,_,_,body). set (block_types body) \<subseteq> types P"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_J_prog (annotate_prog_code P)
[PROOF STEP]
have "wf_prog ?wf_md (annotate_prog_code P)"
[PROOF STATE]
proof (prove)
using this:
wf_J_prog (annotate_prog_code P)

goal (1 subgoal):
 1. wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (annotate_prog_code P)
[PROOF STEP]
unfolding annotate_prog_code_def
[PROOF STATE]
proof (prove)
using this:
wf_J_prog (compP (annotate_Mb_code P) P)

goal (1 subgoal):
 1. wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P)
[PROOF STEP]
by(rule wf_prog_lift)(auto dest!: WT_block_types_is_type[OF wf[unfolded annotate_prog_code_def]] simp add: wf_J_mdecl_def)
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (annotate_prog_code P)

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
hence wf': "wf_prog ?wf_md P"
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (annotate_prog_code P)

goal (1 subgoal):
 1. wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P
[PROOF STEP]
unfolding annotate_prog_code_def [abs_def]
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P)

goal (1 subgoal):
 1. wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P
[PROOF STEP]
proof(rule wf_prog_compPD)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C M Ts T m. \<lbrakk>compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C; wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>m\<rfloor>)
[PROOF STEP]
fix C M Ts T m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C M Ts T m. \<lbrakk>compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C; wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>m\<rfloor>)
[PROOF STEP]
assume "compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C"
      and "wf_mdecl ?wf_md (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)"
[PROOF STATE]
proof (state)
this:
compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C
wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)

goal (1 subgoal):
 1. \<And>C M Ts T m. \<lbrakk>compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C; wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>m\<rfloor>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C
wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)

goal (1 subgoal):
 1. \<And>C M Ts T m. \<lbrakk>compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C; wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>m\<rfloor>)
[PROOF STEP]
obtain pns body where "m = (pns, body)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pns body. m = (pns, body) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases m)
[PROOF STATE]
proof (state)
this:
m = (pns, body)

goal (1 subgoal):
 1. \<And>C M Ts T m. \<lbrakk>compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C; wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)\<rbrakk> \<Longrightarrow> wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>m\<rfloor>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C
wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)
m = (pns, body)
[PROOF STEP]
show "wf_mdecl ?wf_md P C (M, Ts, T, \<lfloor>m\<rfloor>)"
[PROOF STATE]
proof (prove)
using this:
compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor> in C
wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) (compP (annotate_Mb_code P) P) C (M, Ts, T, \<lfloor>annotate_Mb_code P C M Ts T m\<rfloor>)
m = (pns, body)

goal (1 subgoal):
 1. wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>m\<rfloor>)
[PROOF STEP]
by(fastforce simp add: annotate_Mb_code_def annotate_code_def wf_mdecl_def THE_default_def the_equality Anno_code_def split: if_split_asm dest: Anno_block_types)
[PROOF STATE]
proof (state)
this:
wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>m\<rfloor>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
fix C D fs ms M Ts T pns body
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
assume "(C, D, fs, ms) \<in> set (classes P)"
      and "(M, Ts, T, \<lfloor>(pns, body)\<rfloor>) \<in> set ms"
[PROOF STATE]
proof (state)
this:
(C, D, fs, ms) \<in> set (classes P)
(M, Ts, T, \<lfloor>(pns, body)\<rfloor>) \<in> set ms

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
from \<open>(C, D, fs, ms) \<in> set (classes P)\<close>
[PROOF STATE]
proof (chain)
picking this:
(C, D, fs, ms) \<in> set (classes P)
[PROOF STEP]
have "class P C = \<lfloor>(D, fs, ms)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
(C, D, fs, ms) \<in> set (classes P)

goal (1 subgoal):
 1. class P C = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
using wf'
[PROOF STATE]
proof (prove)
using this:
(C, D, fs, ms) \<in> set (classes P)
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P

goal (1 subgoal):
 1. class P C = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
by(cases P)(auto simp add: wf_prog_def dest: map_of_SomeI)
[PROOF STATE]
proof (state)
this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
with wf'
[PROOF STATE]
proof (chain)
picking this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P
class P C = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
have sees: "P \<turnstile> C sees M:Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in C"
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in C
[PROOF STEP]
using \<open>(M, Ts, T, \<lfloor>(pns, body)\<rfloor>) \<in> set ms\<close>
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P
class P C = \<lfloor>(D, fs, ms)\<rfloor>
(M, Ts, T, \<lfloor>(pns, body)\<rfloor>) \<in> set ms

goal (1 subgoal):
 1. P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in C
[PROOF STEP]
by(rule mdecl_visible)
[PROOF STATE]
proof (state)
this:
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in C

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
from sees_method_compP[OF this, where f="annotate_Mb_code P"]
[PROOF STATE]
proof (chain)
picking this:
compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option (annotate_Mb_code P C M Ts T) \<lfloor>(pns, body)\<rfloor> in C
[PROOF STEP]
have sees': "annotate_prog_code P \<turnstile> C sees M:Ts\<rightarrow>T = \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor> in C"
[PROOF STATE]
proof (prove)
using this:
compP (annotate_Mb_code P) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option (annotate_Mb_code P C M Ts T) \<lfloor>(pns, body)\<rfloor> in C

goal (1 subgoal):
 1. annotate_prog_code P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor> in C
[PROOF STEP]
unfolding annotate_prog_code_def annotate_Mb_code_def
[PROOF STATE]
proof (prove)
using this:
compP (\<lambda>uu uua uub uuc uud. (case uud of (pns, e) \<Rightarrow> \<lambda>P C M Ts T. (pns, annotate_code P [this # pns [\<mapsto>] Class C # Ts] e)) P uu uua uub uuc) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option (\<lambda>uu. (case uu of (pns, e) \<Rightarrow> \<lambda>P C M Ts T. (pns, annotate_code P [this # pns [\<mapsto>] Class C # Ts] e)) P C M Ts T) \<lfloor>(pns, body)\<rfloor> in C

goal (1 subgoal):
 1. compP (\<lambda>uu uua uub uuc uud. (case uud of (pns, e) \<Rightarrow> \<lambda>P C M Ts T. (pns, annotate_code P [this # pns [\<mapsto>] Class C # Ts] e)) P uu uua uub uuc) P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor> in C
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
annotate_prog_code P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor> in C

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_J_prog (annotate_prog_code P)
annotate_prog_code P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor> in C
[PROOF STEP]
have "wf_mdecl wf_J_mdecl (annotate_prog_code P) C (M, Ts, T, \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor>)"
[PROOF STATE]
proof (prove)
using this:
wf_J_prog (annotate_prog_code P)
annotate_prog_code P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor> in C

goal (1 subgoal):
 1. wf_mdecl wf_J_mdecl (annotate_prog_code P) C (M, Ts, T, \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor>)
[PROOF STEP]
by(rule sees_wf_mdecl)
[PROOF STATE]
proof (state)
this:
wf_mdecl wf_J_mdecl (annotate_prog_code P) C (M, Ts, T, \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor>)

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
hence "set Ts \<subseteq> types P"
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wf_J_mdecl (annotate_prog_code P) C (M, Ts, T, \<lfloor>(pns, annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)\<rfloor>)

goal (1 subgoal):
 1. set Ts \<subseteq> types P
[PROOF STEP]
by(auto simp add: wf_mdecl_def annotate_prog_code_def)
[PROOF STATE]
proof (state)
this:
set Ts \<subseteq> types P

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set Ts \<subseteq> types P

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
from sees
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in C
[PROOF STEP]
have "is_class P C"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in C

goal (1 subgoal):
 1. is_class P C
[PROOF STEP]
by(rule sees_method_is_class)
[PROOF STATE]
proof (state)
this:
is_class P C

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_class P C

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
from wf' sees
[PROOF STATE]
proof (chain)
picking this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in C
[PROOF STEP]
have "wf_mdecl ?wf_md P C (M, Ts, T, \<lfloor>(pns, body)\<rfloor>)"
[PROOF STATE]
proof (prove)
using this:
wf_prog (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in C

goal (1 subgoal):
 1. wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>(pns, body)\<rfloor>)
[PROOF STEP]
by(rule sees_wf_mdecl)
[PROOF STATE]
proof (state)
this:
wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>(pns, body)\<rfloor>)

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
hence "set (block_types body) \<subseteq> types P"
[PROOF STATE]
proof (prove)
using this:
wf_mdecl (\<lambda>_ _ (uu_, uu_, uu_, uu_, body). set (block_types body) \<subseteq> types P) P C (M, Ts, T, \<lfloor>(pns, body)\<rfloor>)

goal (1 subgoal):
 1. set (block_types body) \<subseteq> types P
[PROOF STEP]
by(simp add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
set (block_types body) \<subseteq> types P

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set Ts \<subseteq> types P
is_class P C
set (block_types body) \<subseteq> types P
[PROOF STEP]
have "ran [this \<mapsto> Class C, pns [\<mapsto>] Ts] \<union> set (block_types body) \<subseteq> types P"
[PROOF STATE]
proof (prove)
using this:
set Ts \<subseteq> types P
is_class P C
set (block_types body) \<subseteq> types P

goal (1 subgoal):
 1. ran [this \<mapsto> Class C, pns [\<mapsto>] Ts] \<union> set (block_types body) \<subseteq> types P
[PROOF STEP]
by(auto simp add: ran_def wf_mdecl_def map_upds_def split: if_split_asm dest!: map_of_SomeD set_zip_rightD)
[PROOF STATE]
proof (state)
this:
ran [this \<mapsto> Class C, pns [\<mapsto>] Ts] \<union> set (block_types body) \<subseteq> types P

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
hence "annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body = annotate P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body"
[PROOF STATE]
proof (prove)
using this:
ran [this \<mapsto> Class C, pns [\<mapsto>] Ts] \<union> set (block_types body) \<subseteq> types P

goal (1 subgoal):
 1. annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body = annotate P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body
[PROOF STEP]
unfolding annotate_code_def annotate_def
[PROOF STATE]
proof (prove)
using this:
ran [this \<mapsto> Class C, pns [\<mapsto>] Ts] \<union> set (block_types body) \<subseteq> types P

goal (1 subgoal):
 1. THE_default body (Anno_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body) = THE_default body (Anno' P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body)
[PROOF STEP]
by -(rule arg_cong[where f="THE_default body"], auto intro!: ext intro: Anno_code_into_Anno[OF wf'] Anno_into_Anno_code[OF wf'])
[PROOF STATE]
proof (state)
this:
annotate_code P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body = annotate P [this \<mapsto> Class C, pns [\<mapsto>] Ts] body

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?C3, ?D3, ?fs3, ?ms3) \<in> set (classes P); (?M3, ?Ts3, ?T3, \<lfloor>(?pns3, ?body3)\<rfloor>) \<in> set ?ms3\<rbrakk> \<Longrightarrow> annotate_code P [this \<mapsto> Class ?C3, ?pns3 [\<mapsto>] ?Ts3] ?body3 = annotate P [this \<mapsto> Class ?C3, ?pns3 [\<mapsto>] ?Ts3] ?body3

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?C3, ?D3, ?fs3, ?ms3) \<in> set (classes P); (?M3, ?Ts3, ?T3, \<lfloor>(?pns3, ?body3)\<rfloor>) \<in> set ?ms3\<rbrakk> \<Longrightarrow> annotate_code P [this \<mapsto> Class ?C3, ?pns3 [\<mapsto>] ?Ts3] ?body3 = annotate P [this \<mapsto> Class ?C3, ?pns3 [\<mapsto>] ?Ts3] ?body3

goal (1 subgoal):
 1. annotate_prog_code P = annotate_prog P
[PROOF STEP]
unfolding annotate_prog_code_def annotate_prog_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?C3, ?D3, ?fs3, ?ms3) \<in> set (classes P); (?M3, ?Ts3, ?T3, \<lfloor>(?pns3, ?body3)\<rfloor>) \<in> set ?ms3\<rbrakk> \<Longrightarrow> annotate_code P [this \<mapsto> Class ?C3, ?pns3 [\<mapsto>] ?Ts3] ?body3 = annotate P [this \<mapsto> Class ?C3, ?pns3 [\<mapsto>] ?Ts3] ?body3

goal (1 subgoal):
 1. compP (annotate_Mb_code P) P = compP (annotate_Mb P) P
[PROOF STEP]
by(cases P)(auto simp add: compC_def compM_def annotate_Mb_def annotate_Mb_code_def map_option_case)
[PROOF STATE]
proof (state)
this:
annotate_prog_code P = annotate_prog P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_of_rat_ineq: assumes "real_of_rat x \<le> z"
  shows "x \<le> of_int \<lceil>z\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> rat_of_int \<lceil>z\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> rat_of_int \<lceil>z\<rceil>
[PROOF STEP]
have "z \<le> of_int \<lceil>z\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<le> real_of_int \<lceil>z\<rceil>
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
z \<le> real_of_int \<lceil>z\<rceil>

goal (1 subgoal):
 1. x \<le> rat_of_int \<lceil>z\<rceil>
[PROOF STEP]
from order_trans[OF assms this]
[PROOF STATE]
proof (chain)
picking this:
real_of_rat x \<le> real_of_int \<lceil>z\<rceil>
[PROOF STEP]
have "real_of_rat x \<le> real_of_rat (of_int \<lceil>z\<rceil>)"
[PROOF STATE]
proof (prove)
using this:
real_of_rat x \<le> real_of_int \<lceil>z\<rceil>

goal (1 subgoal):
 1. real_of_rat x \<le> real_of_rat (rat_of_int \<lceil>z\<rceil>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_rat x \<le> real_of_rat (rat_of_int \<lceil>z\<rceil>)

goal (1 subgoal):
 1. x \<le> rat_of_int \<lceil>z\<rceil>
[PROOF STEP]
thus "x \<le> of_int \<lceil>z\<rceil>"
[PROOF STATE]
proof (prove)
using this:
real_of_rat x \<le> real_of_rat (rat_of_int \<lceil>z\<rceil>)

goal (1 subgoal):
 1. x \<le> rat_of_int \<lceil>z\<rceil>
[PROOF STEP]
using of_rat_less_eq
[PROOF STATE]
proof (prove)
using this:
real_of_rat x \<le> real_of_rat (rat_of_int \<lceil>z\<rceil>)
(of_rat ?r \<le> of_rat ?s) = (?r \<le> ?s)

goal (1 subgoal):
 1. x \<le> rat_of_int \<lceil>z\<rceil>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<le> rat_of_int \<lceil>z\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aNeg_aEval : "aEval a L \<longleftrightarrow> (\<not> aEval (aNeg a) L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aEval a L = (\<not> aEval (aNeg a) L)
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. a = Less x1 \<Longrightarrow> aEval a L = (\<not> aEval (aNeg a) L)
 2. \<And>x2. a = Eq x2 \<Longrightarrow> aEval a L = (\<not> aEval (aNeg a) L)
 3. \<And>x3. a = Leq x3 \<Longrightarrow> aEval a L = (\<not> aEval (aNeg a) L)
 4. \<And>x4. a = Neq x4 \<Longrightarrow> aEval a L = (\<not> aEval (aNeg a) L)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>a = Less x1; insertion (nth_default 0 L) x1 < 0; insertion (nth_default 0 L) (- x1) \<le> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x1. \<lbrakk>a = Less x1; \<not> insertion (nth_default 0 L) (- x1) \<le> 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 L) x1 < 0
 3. \<And>x3. \<lbrakk>a = Leq x3; insertion (nth_default 0 L) x3 \<le> 0; insertion (nth_default 0 L) (- x3) < 0\<rbrakk> \<Longrightarrow> False
 4. \<And>x3. \<lbrakk>a = Leq x3; \<not> insertion (nth_default 0 L) (- x3) < 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 L) x3 \<le> 0
[PROOF STEP]
apply(smt insertionNegative)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>a = Less x1; \<not> insertion (nth_default 0 L) (- x1) \<le> 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 L) x1 < 0
 2. \<And>x3. \<lbrakk>a = Leq x3; insertion (nth_default 0 L) x3 \<le> 0; insertion (nth_default 0 L) (- x3) < 0\<rbrakk> \<Longrightarrow> False
 3. \<And>x3. \<lbrakk>a = Leq x3; \<not> insertion (nth_default 0 L) (- x3) < 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 L) x3 \<le> 0
[PROOF STEP]
apply(smt insertionNegative)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>a = Leq x3; insertion (nth_default 0 L) x3 \<le> 0; insertion (nth_default 0 L) (- x3) < 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x3. \<lbrakk>a = Leq x3; \<not> insertion (nth_default 0 L) (- x3) < 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 L) x3 \<le> 0
[PROOF STEP]
apply(smt insertionNegative)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>a = Leq x3; \<not> insertion (nth_default 0 L) (- x3) < 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 L) x3 \<le> 0
[PROOF STEP]
apply(smt insertionNegative)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "eval (ExQ (Or (Atom A) (Atom B))) xs =  eval (Or (ExQ(Atom A)) (ExQ(Atom B))) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExQ (Or (fm.Atom A) (fm.Atom B))) xs = eval (Or (ExQ (fm.Atom A)) (ExQ (fm.Atom B))) xs
[PROOF STEP]
by(auto)