[STATEMENT]
lemma eval_hext: "P,E \<turnstile> \<langle>e,(h,l)\<rangle> \<Rightarrow> \<langle>e',(h',l')\<rangle> \<Longrightarrow> h \<unlhd> h'"
and evals_hext:  "P,E \<turnstile> \<langle>es,(h,l)\<rangle> [\<Rightarrow>] \<langle>es',(h',l')\<rangle> \<Longrightarrow> h \<unlhd> h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<Rightarrow> \<langle>e',(h', l')\<rangle> \<Longrightarrow> h \<unlhd> h') &&& (P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<Rightarrow>] \<langle>es',(h', l')\<rangle> \<Longrightarrow> h \<unlhd> h')
[PROOF STEP]
proof (induct rule:eval_evals_inducts)
[PROOF STATE]
proof (state)
goal (48 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C)))\<rbrakk> \<Longrightarrow> h \<unlhd> h'
 2. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 3. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 4. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 5. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 6. \<And>E e a b aa Cs ab ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; C \<notin> set Cs\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 7. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>throw e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 8. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 9. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 10. \<And>E e a b aa Cs h l D S C Cs'. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(h, l)\<rangle>; a \<unlhd> h; h aa = \<lfloor>(D, S)\<rfloor>; P \<turnstile> Path D to C via Cs' ; P \<turnstile> Path D to C unique\<rbrakk> \<Longrightarrow> a \<unlhd> h
A total of 48 subgoals...
[PROOF STEP]
case New
[PROOF STATE]
proof (state)
this:
new_Addr h_ = \<lfloor>a_\<rfloor>
h'_ = h_(a_ \<mapsto> (C_, Collect (init_obj P C_)))

goal (48 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C)))\<rbrakk> \<Longrightarrow> h \<unlhd> h'
 2. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 3. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 4. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 5. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 6. \<And>E e a b aa Cs ab ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; C \<notin> set Cs\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 7. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>throw e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 8. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 9. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 10. \<And>E e a b aa Cs h l D S C Cs'. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(h, l)\<rangle>; a \<unlhd> h; h aa = \<lfloor>(D, S)\<rfloor>; P \<turnstile> Path D to C via Cs' ; P \<turnstile> Path D to C unique\<rbrakk> \<Longrightarrow> a \<unlhd> h
A total of 48 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
new_Addr h_ = \<lfloor>a_\<rfloor>
h'_ = h_(a_ \<mapsto> (C_, Collect (init_obj P C_)))

goal (1 subgoal):
 1. h_ \<unlhd> h'_
[PROOF STEP]
by(fastforce intro!: hext_new intro:someI simp:new_Addr_def
                split:if_split_asm simp del:fun_upd_apply)
[PROOF STATE]
proof (state)
this:
h_ \<unlhd> h'_

goal (47 subgoals):
 1. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 2. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 3. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 4. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 5. \<And>E e a b aa Cs ab ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; C \<notin> set Cs\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 6. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>throw e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 7. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 8. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 9. \<And>E e a b aa Cs h l D S C Cs'. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(h, l)\<rangle>; a \<unlhd> h; h aa = \<lfloor>(D, S)\<rfloor>; P \<turnstile> Path D to C via Cs' ; P \<turnstile> Path D to C unique\<rbrakk> \<Longrightarrow> a \<unlhd> h
 10. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
A total of 47 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (47 subgoals):
 1. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 2. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 3. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 4. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 5. \<And>E e a b aa Cs ab ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; C \<notin> set Cs\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 6. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>throw e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 7. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 8. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 9. \<And>E e a b aa Cs h l D S C Cs'. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(h, l)\<rangle>; a \<unlhd> h; h aa = \<lfloor>(D, S)\<rfloor>; P \<turnstile> Path D to C via Cs' ; P \<turnstile> Path D to C unique\<rbrakk> \<Longrightarrow> a \<unlhd> h
 10. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
A total of 47 subgoals...
[PROOF STEP]
case FAss
[PROOF STATE]
proof (state)
this:
P,E_ \<turnstile> \<langle>e\<^sub>1_,(a___, b___)\<rangle> \<Rightarrow> \<langle>ref (aa___, Cs'_),(a_, b_)\<rangle>
a___ \<unlhd> a_
P,E_ \<turnstile> \<langle>e\<^sub>2_,(a_, b_)\<rangle> \<Rightarrow> \<langle>Val v_,(h\<^sub>2_, l\<^sub>2_)\<rangle>
a_ \<unlhd> h\<^sub>2_
h\<^sub>2_ aa___ = \<lfloor>(D_, S_)\<rfloor>
P \<turnstile> last Cs'_ has least F_:T_ via Cs_
P \<turnstile> T_ casts v_ to v'_
Ds_ = Cs'_ @\<^sub>p Cs_
(Ds_, fs_) \<in> S_
fs'_ = fs_(F_ \<mapsto> v'_)
S'_ = S_ - {(Ds_, fs_)} \<union> {(Ds_, fs'_)}
h\<^sub>2'_ = h\<^sub>2_(aa___ \<mapsto> (D_, S'_))

goal (47 subgoals):
 1. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 2. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 3. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 4. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 5. \<And>E e a b aa Cs ab ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; C \<notin> set Cs\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 6. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>throw e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 7. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 8. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 9. \<And>E e a b aa Cs h l D S C Cs'. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(h, l)\<rangle>; a \<unlhd> h; h aa = \<lfloor>(D, S)\<rfloor>; P \<turnstile> Path D to C via Cs' ; P \<turnstile> Path D to C unique\<rbrakk> \<Longrightarrow> a \<unlhd> h
 10. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
A total of 47 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E_ \<turnstile> \<langle>e\<^sub>1_,(a___, b___)\<rangle> \<Rightarrow> \<langle>ref (aa___, Cs'_),(a_, b_)\<rangle>
a___ \<unlhd> a_
P,E_ \<turnstile> \<langle>e\<^sub>2_,(a_, b_)\<rangle> \<Rightarrow> \<langle>Val v_,(h\<^sub>2_, l\<^sub>2_)\<rangle>
a_ \<unlhd> h\<^sub>2_
h\<^sub>2_ aa___ = \<lfloor>(D_, S_)\<rfloor>
P \<turnstile> last Cs'_ has least F_:T_ via Cs_
P \<turnstile> T_ casts v_ to v'_
Ds_ = Cs'_ @\<^sub>p Cs_
(Ds_, fs_) \<in> S_
fs'_ = fs_(F_ \<mapsto> v'_)
S'_ = S_ - {(Ds_, fs_)} \<union> {(Ds_, fs'_)}
h\<^sub>2'_ = h\<^sub>2_(aa___ \<mapsto> (D_, S'_))

goal (1 subgoal):
 1. a___ \<unlhd> h\<^sub>2'_
[PROOF STEP]
by(auto simp:sym[THEN hext_upd_obj] simp del:fun_upd_apply
            elim!: hext_trans)
[PROOF STATE]
proof (state)
this:
a___ \<unlhd> h\<^sub>2'_

goal (46 subgoals):
 1. \<And>h E C l. new_Addr h = None \<Longrightarrow> h \<unlhd> h
 2. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 3. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 4. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 5. \<And>E e a b aa Cs ab ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; C \<notin> set Cs\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 6. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>throw e',(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
 7. \<And>E e a b aa Cs ab ba C Cs' Ds. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(ab, ba)\<rangle>; a \<unlhd> ab; P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 8. \<And>E e a b aa Cs C Cs' ab ba. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs @ [C] @ Cs'),(ab, ba)\<rangle>; a \<unlhd> ab\<rbrakk> \<Longrightarrow> a \<unlhd> ab
 9. \<And>E e a b aa Cs h l D S C Cs'. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>ref (aa, Cs),(h, l)\<rangle>; a \<unlhd> h; h aa = \<lfloor>(D, S)\<rfloor>; P \<turnstile> Path D to C via Cs' ; P \<turnstile> Path D to C unique\<rbrakk> \<Longrightarrow> a \<unlhd> h
 10. \<And>E e a b aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; a \<unlhd> aa\<rbrakk> \<Longrightarrow> a \<unlhd> aa
A total of 46 subgoals...
[PROOF STEP]
qed (auto elim!: hext_trans)


[STATEMENT]
lemma conf_hext: "h \<unlhd> h' \<Longrightarrow> P,h \<turnstile> v :\<le> T \<Longrightarrow> P,h' \<turnstile> v :\<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> P,h' \<turnstile> v :\<le> T
[PROOF STEP]
by(cases T)(induct v,auto dest: hext_objD split:if_split_asm)+


[STATEMENT]
lemma confs_hext: "P,h \<turnstile> vs [:\<le>] Ts \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> vs [:\<le>] Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> vs [:\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,h' \<turnstile> vs [:\<le>] Ts
[PROOF STEP]
by (erule list_all2_mono, erule conf_hext, assumption)


[STATEMENT]
lemma fconf_hext: "\<lbrakk> P,h \<turnstile> fs (:\<le>) E; h \<unlhd> h' \<rbrakk> \<Longrightarrow> P,h' \<turnstile> fs (:\<le>) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> fs (:\<le>) E; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,h' \<turnstile> fs (:\<le>) E
[PROOF STEP]
apply (unfold fconf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>FD T. E FD = \<lfloor>T\<rfloor> \<longrightarrow> (\<exists>v. fs FD = \<lfloor>v\<rfloor> \<and> P,h \<turnstile> v :\<le> T); h \<unlhd> h'\<rbrakk> \<Longrightarrow> \<forall>FD T. E FD = \<lfloor>T\<rfloor> \<longrightarrow> (\<exists>v. fs FD = \<lfloor>v\<rfloor> \<and> P,h' \<turnstile> v :\<le> T)
[PROOF STEP]
apply  (fast elim: conf_hext)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oconf_hext: "P,h \<turnstile> obj \<surd> \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> obj \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> obj \<surd>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,h' \<turnstile> obj \<surd>
[PROOF STEP]
apply (auto simp:oconf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S Cs fs'. \<lbrakk>h \<unlhd> h'; obj = (C, S); \<forall>Cs. Subobjs P C Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> S); \<forall>Cs fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P C Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs); (Cs, fs') \<in> S\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h' \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (erule allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S Cs fs'. \<lbrakk>h \<unlhd> h'; obj = (C, S); \<forall>Cs fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P C Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs); (Cs, fs') \<in> S; Subobjs P C (?Cs14 C S Cs fs') \<longrightarrow> (\<exists>!fs'a. (?Cs14 C S Cs fs', fs'a) \<in> S)\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h' \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (erule_tac x="Cs" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S Cs fs'. \<lbrakk>h \<unlhd> h'; obj = (C, S); (Cs, fs') \<in> S; Subobjs P C (?Cs14 C S Cs fs') \<longrightarrow> (\<exists>!fs'a. (?Cs14 C S Cs fs', fs'a) \<in> S); \<forall>fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P C Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h' \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (erule_tac x="fs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C S Cs fs'. \<lbrakk>h \<unlhd> h'; obj = (C, S); (Cs, fs') \<in> S; Subobjs P C (?Cs14 C S Cs fs') \<longrightarrow> (\<exists>!fs'a. (?Cs14 C S Cs fs', fs'a) \<in> S); (Cs, fs') \<in> S \<longrightarrow> Subobjs P C Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h' \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (fastforce elim:fconf_hext)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hconf_upd_obj:
"\<lbrakk> P \<turnstile> h\<surd>; h a = Some(C,S); P,h \<turnstile> (C,S')\<surd> \<rbrakk> \<Longrightarrow> P \<turnstile> h(a\<mapsto>(C,S'))\<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> h \<surd>; h a = \<lfloor>(C, S)\<rfloor>; P,h \<turnstile> (C, S') \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h(a \<mapsto> (C, S')) \<surd>
[PROOF STEP]
by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)


[STATEMENT]
lemma lconf_hext: "\<lbrakk> P,h \<turnstile> l (:\<le>)\<^sub>w E; h \<unlhd> h' \<rbrakk> \<Longrightarrow> P,h' \<turnstile> l (:\<le>)\<^sub>w E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> l (:\<le>)\<^sub>w E; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
apply (unfold lconf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>V v. l V = \<lfloor>v\<rfloor> \<longrightarrow> (\<exists>T. E V = \<lfloor>T\<rfloor> \<and> P,h \<turnstile> v :\<le> T); h \<unlhd> h'\<rbrakk> \<Longrightarrow> \<forall>V v. l V = \<lfloor>v\<rfloor> \<longrightarrow> (\<exists>T. E V = \<lfloor>T\<rfloor> \<and> P,h' \<turnstile> v :\<le> T)
[PROOF STEP]
apply  (fast elim: conf_hext)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hext_typeof_mono: "\<lbrakk> h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = Some T \<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = Some T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
[PROOF STEP]
apply(cases v)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Unit\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 2. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Null\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 3. \<And>x3. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Bool x3\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 4. \<And>x4. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Intg x4\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 5. \<And>x5. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Ref x5\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Null\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 2. \<And>x3. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Bool x3\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 3. \<And>x4. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Intg x4\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 4. \<And>x5. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Ref x5\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Bool x3\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 2. \<And>x4. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Intg x4\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 3. \<And>x5. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Ref x5\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Intg x4\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
 2. \<And>x5. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Ref x5\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>h \<unlhd> h'; P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; v = Ref x5\<rbrakk> \<Longrightarrow> P \<turnstile> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
[PROOF STEP]
apply(fastforce simp:hext_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WTrt_hext_mono: "P,E,h \<turnstile> e : T \<Longrightarrow> (\<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T)"
and WTrts_hext_mono: "P,E,h \<turnstile> es [:] Ts \<Longrightarrow> (\<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E,h \<turnstile> e : T \<Longrightarrow> (\<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T)) &&& (P,E,h \<turnstile> es [:] Ts \<Longrightarrow> (\<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts))
[PROOF STEP]
apply(induct rule: WTrt_inducts)
[PROOF STATE]
proof (prove)
goal (21 subgoals):
 1. \<And>C E h h'. \<lbrakk>is_class P C; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> new C : Class C
 2. \<And>E h e T C h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; is_refT T; is_class P C; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Cast C e : Class C
 3. \<And>E h e T C h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; is_refT T; is_class P C; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> \<lparr>C\<rparr>e : Class C
 4. \<And>h v T E h'. \<lbrakk>P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Val v : T
 5. \<And>E V T h h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Var V : T
 6. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 bop T h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; case bop of Eq \<Rightarrow> T = Boolean | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T
 7. \<And>E V T h e T' h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> V:=e : T
 8. \<And>E h e C Cs F T h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 9. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 10. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
A total of 21 subgoals...
[PROOF STEP]
apply(simp add: WTrtNew)
[PROOF STATE]
proof (prove)
goal (20 subgoals):
 1. \<And>E h e T C h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; is_refT T; is_class P C; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Cast C e : Class C
 2. \<And>E h e T C h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; is_refT T; is_class P C; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> \<lparr>C\<rparr>e : Class C
 3. \<And>h v T E h'. \<lbrakk>P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Val v : T
 4. \<And>E V T h h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Var V : T
 5. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 bop T h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; case bop of Eq \<Rightarrow> T = Boolean | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T
 6. \<And>E V T h e T' h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> V:=e : T
 7. \<And>E h e C Cs F T h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 8. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 9. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 10. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
A total of 20 subgoals...
[PROOF STEP]
apply(fastforce intro: WTrtDynCast)
[PROOF STATE]
proof (prove)
goal (19 subgoals):
 1. \<And>E h e T C h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; is_refT T; is_class P C; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> \<lparr>C\<rparr>e : Class C
 2. \<And>h v T E h'. \<lbrakk>P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Val v : T
 3. \<And>E V T h h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Var V : T
 4. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 bop T h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; case bop of Eq \<Rightarrow> T = Boolean | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T
 5. \<And>E V T h e T' h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> V:=e : T
 6. \<And>E h e C Cs F T h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 7. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 8. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 9. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 10. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
A total of 19 subgoals...
[PROOF STEP]
apply(fastforce intro: WTrtStaticCast)
[PROOF STATE]
proof (prove)
goal (18 subgoals):
 1. \<And>h v T E h'. \<lbrakk>P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Val v : T
 2. \<And>E V T h h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Var V : T
 3. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 bop T h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; case bop of Eq \<Rightarrow> T = Boolean | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T
 4. \<And>E V T h e T' h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> V:=e : T
 5. \<And>E h e C Cs F T h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 6. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 7. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 8. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 9. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 10. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
A total of 18 subgoals...
[PROOF STEP]
apply(fastforce simp: WTrtVal dest:hext_typeof_mono)
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<And>E V T h h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Var V : T
 2. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 bop T h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; case bop of Eq \<Rightarrow> T = Boolean | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T
 3. \<And>E V T h e T' h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> V:=e : T
 4. \<And>E h e C Cs F T h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 5. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 6. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 7. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 8. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 9. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 10. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
A total of 17 subgoals...
[PROOF STEP]
apply(simp add: WTrtVar)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 bop T h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; case bop of Eq \<Rightarrow> T = Boolean | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T
 2. \<And>E V T h e T' h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> V:=e : T
 3. \<And>E h e C Cs F T h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 4. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 5. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 6. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 7. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 8. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 9. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 10. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
A total of 16 subgoals...
[PROOF STEP]
apply(fastforce simp add: WTrtBinOp)
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>E V T h e T' h'. \<lbrakk>E V = \<lfloor>T\<rfloor>; P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> V:=e : T
 2. \<And>E h e C Cs F T h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 3. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 4. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 5. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 6. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 7. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 8. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 9. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 10. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
A total of 15 subgoals...
[PROOF STEP]
apply(fastforce simp add: WTrtLAss)
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>E h e C Cs F T h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 2. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 3. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 4. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 5. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 6. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 7. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 8. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 9. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 10. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
A total of 14 subgoals...
[PROOF STEP]
apply(fastforce simp: WTrtFAcc del:WTrt_WTrts.intros WTrt_elim_cases)
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>E h e F Cs T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<bullet>F{Cs} : T
 2. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 3. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 4. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 5. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 6. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 7. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 8. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 9. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 10. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
A total of 13 subgoals...
[PROOF STEP]
apply(simp add: WTrtFAccNT)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>E h e\<^sub>1 C Cs F T e\<^sub>2 T' h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : Class C; Cs \<noteq> []; P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 2. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 3. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 4. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 5. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 6. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 7. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 8. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 9. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 10. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
A total of 12 subgoals...
[PROOF STEP]
apply(fastforce simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>E h e\<^sub>1 e\<^sub>2 T' T F Cs h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : NT; P,E,h \<turnstile> e\<^sub>2 : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T'; P \<turnstile> T' \<le> T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1\<bullet>F{Cs} := e\<^sub>2 : T
 2. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 3. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 4. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 5. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 6. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 7. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 8. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 9. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 10. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
A total of 11 subgoals...
[PROOF STEP]
apply(fastforce simp: WTrtFAssNT del:WTrt_WTrts.intros WTrt_elim_cases)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>E h e C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e None M es : T
 2. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 3. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 4. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 5. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 6. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 7. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 8. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 9. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 10. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(fastforce simp: WTrtCall del:WTrt_WTrts.intros WTrt_elim_cases)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>E h e C' C M Ts T a b Cs es Ts' h'. \<lbrakk>P,E,h \<turnstile> e : Class C'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique; P \<turnstile> C has least M = (Ts, T, a, b) via Cs; P,E,h \<turnstile> es [:] Ts'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts'; P \<turnstile> Ts' [\<le>] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e \<lfloor>C\<rfloor> M es : T
 2. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 3. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 4. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 5. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 6. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 7. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 8. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 9. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(fastforce simp: WTrtStaticCall del:WTrt_WTrts.intros WTrt_elim_cases)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>E h e es Ts Copt M T h'. \<lbrakk>P,E,h \<turnstile> e : NT; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> Call e Copt M es : T
 2. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 3. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 4. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 5. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 6. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 7. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 8. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(fastforce simp: WTrtCallNT del:WTrt_WTrts.intros WTrt_elim_cases)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>E V T h e T' h'. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E(V \<mapsto> T),h' \<turnstile> e : T'; is_type P T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> {V:T; e} : T'
 2. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 3. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 4. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 5. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 6. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 7. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>E h e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T\<^sub>1; P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T\<^sub>2; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1;; e\<^sub>2 : T\<^sub>2
 2. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 3. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 4. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 5. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 6. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(fastforce simp add: WTrtSeq)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>E h e e\<^sub>1 T e\<^sub>2 h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> e\<^sub>1 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>1 : T; P,E,h \<turnstile> e\<^sub>2 : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e\<^sub>2 : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T
 2. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 3. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 4. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 5. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(fastforce simp add: WTrtCond)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>E h e c T h'. \<lbrakk>P,E,h \<turnstile> e : Boolean; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : Boolean; P,E,h \<turnstile> c : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> c : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> while (e) c : Void
 2. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 3. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 4. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(fastforce simp add: WTrtWhile)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>E h e T' T h'. \<lbrakk>P,E,h \<turnstile> e : T'; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T'; is_refT T'; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> throw e : T
 2. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 3. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(fastforce simp add: WTrtThrow)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>E h h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> [] [:] []
 2. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(simp add: WTrtNil)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>E h e T es Ts h'. \<lbrakk>P,E,h \<turnstile> e : T; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts; \<And>h'. h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,E,h' \<turnstile> e # es [:] T # Ts
[PROOF STEP]
apply(simp add: WTrtCons)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nat_less_mult_monoish: "\<lbrakk> a < b; c < (d :: nat) \<rbrakk> \<Longrightarrow> (a + 1) * (c + 1) <= b * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; c < d\<rbrakk> \<Longrightarrow> (a + 1) * (c + 1) \<le> b * d
[PROOF STEP]
apply (drule Suc_leI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc a \<le> b; Suc c \<le> d\<rbrakk> \<Longrightarrow> (a + 1) * (c + 1) \<le> b * d
[PROOF STEP]
apply (drule(1) mult_le_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc c \<le> d; Suc a * Suc c \<le> b * d\<rbrakk> \<Longrightarrow> (a + 1) * (c + 1) \<le> b * d
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma if_and_helper:
  "(If x v v') AND v'' = If x (v AND v'') (v' AND v'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x then v else v') AND v'' = (if x then v AND v'' else v' AND v'')
[PROOF STEP]
by (rule if_distrib)


[STATEMENT]
lemma eq_eqI:
  "a = b \<Longrightarrow> (a = x) = (b = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b \<Longrightarrow> (a = x) = (b = x)
[PROOF STEP]
by simp


[STATEMENT]
lemma map2_Cons_2_3:
  "(map2 f xs (y # ys) = (z # zs)) = (\<exists>x xs'. xs = x # xs' \<and> f x y = z \<and> map2 f xs' ys = zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map2 f xs (y # ys) = z # zs) = (\<exists>x xs'. xs = x # xs' \<and> f x y = z \<and> map2 f xs' ys = zs)
[PROOF STEP]
by (case_tac xs, simp_all)


[STATEMENT]
lemma map2_xor_replicate_False:
  "map2 (\<lambda>x y. x \<longleftrightarrow> \<not> y) xs (replicate n False) = take n xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<lambda>x y. x = (\<not> y)) xs (replicate n False) = take n xs
[PROOF STEP]
apply (induct xs arbitrary: n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs n. (\<And>n. map2 (\<lambda>x y. x = (\<not> y)) xs (replicate n False) = take n xs) \<Longrightarrow> map2 (\<lambda>x y. x = (\<not> y)) (a # xs) (replicate n False) = take n (a # xs)
[PROOF STEP]
apply (case_tac n; simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma plus_Collect_helper:
  "(+) x ` {xa. P (xa :: 'a :: len word)} = {xa. P (xa - x)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (+) x ` {xa. P xa} = {xa. P (xa - x)}
[PROOF STEP]
by (fastforce simp add: image_def)


[STATEMENT]
lemma plus_Collect_helper2:
  "(+) (- x) ` {xa. P (xa :: 'a :: len word)} = {xa. P (x + xa)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (+) (- x) ` {xa. P xa} = {xa. P (x + xa)}
[PROOF STEP]
using plus_Collect_helper [of "- x" P]
[PROOF STATE]
proof (prove)
using this:
(+) (- x) ` {xa. P xa} = {xa. P (xa - - x)}

goal (1 subgoal):
 1. (+) (- x) ` {xa. P xa} = {xa. P (x + xa)}
[PROOF STEP]
by (simp add: ac_simps)


[STATEMENT]
lemma range_subset_eq2:
  "{a :: 'a :: len word .. b} \<noteq> {} \<Longrightarrow> ({a .. b} \<subseteq> {c .. d}) = (c \<le> a \<and> b \<le> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a..b} \<noteq> {} \<Longrightarrow> ({a..b} \<subseteq> {c..d}) = (c \<le> a \<and> b \<le> d)
[PROOF STEP]
by simp


[STATEMENT]
lemma nat_mod_power_lem:
  fixes a :: nat
  shows "1 < a \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < a \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc 0 < a; m \<le> n\<rbrakk> \<Longrightarrow> a ^ n mod a ^ m = 0
[PROOF STEP]
apply (clarsimp simp add: le_iff_add power_add)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_hate_words_helper:
  "i \<le> (j - k :: nat) \<Longrightarrow> i \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j - k \<Longrightarrow> i \<le> j
[PROOF STEP]
by simp


[STATEMENT]
lemma i_hate_words:
  "unat (a :: 'a word) \<le> unat (b :: 'a :: len word) - Suc 0
    \<Longrightarrow> a \<noteq> -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat a \<le> unat b - Suc 0 \<Longrightarrow> a \<noteq> - 1
[PROOF STEP]
apply (frule i_hate_words_helper)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a \<le> unat b - Suc 0; unat a \<le> unat b\<rbrakk> \<Longrightarrow> a \<noteq> - 1
[PROOF STEP]
apply (subst(asm) word_le_nat_alt[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a \<le> unat b - Suc 0; a \<le> b\<rbrakk> \<Longrightarrow> a \<noteq> - 1
[PROOF STEP]
apply (clarsimp simp only: word_minus_one_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (- 1) \<le> unat (- 1) - Suc 0; b = - 1; a = - 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp only: linorder_not_less[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> unat (- 1) - Suc 0 < unat (- 1); b = - 1; a = - 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = - 1; a = - 1\<rbrakk> \<Longrightarrow> unat (- 1) - Suc 0 < unat (- 1)
[PROOF STEP]
apply (rule diff_Suc_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = - 1; a = - 1\<rbrakk> \<Longrightarrow> 0 < unat (- 1)
[PROOF STEP]
apply (subst neq0_conv[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = - 1; a = - 1\<rbrakk> \<Longrightarrow> unat (- 1) \<noteq> 0
[PROOF STEP]
apply (subst unat_eq_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = - 1; a = - 1\<rbrakk> \<Longrightarrow> - 1 \<noteq> 0
[PROOF STEP]
apply (rule notI, drule arg_cong[where f="(+) 1"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = - 1; - 1 = 0; 1 + b = 1 + - 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma If_eq_obvious:
  "x \<noteq> z \<Longrightarrow> ((if P then x else y) = z) = (\<not> P \<and> y = z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> z \<Longrightarrow> ((if P then x else y) = z) = (\<not> P \<and> y = z)
[PROOF STEP]
by simp


[STATEMENT]
lemma Some_to_the:
  "v = Some x \<Longrightarrow> x = the v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = Some x \<Longrightarrow> x = the v
[PROOF STEP]
by simp


[STATEMENT]
lemma dom_if_Some:
  "dom (\<lambda>x. if P x then Some (f x) else g x) = {x. P x} \<union> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if P x then Some (f x) else g x) = {x. P x} \<union> dom g
[PROOF STEP]
by fastforce


[STATEMENT]
lemma dom_insert_absorb:
  "x \<in> dom f \<Longrightarrow> insert x (dom f) = dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> dom f \<Longrightarrow> insert x (dom f) = dom f
[PROOF STEP]
by (fact insert_absorb)


[STATEMENT]
lemma emptyE2:
  "\<lbrakk> S = {}; x \<in> S \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {}; x \<in> S\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by simp


[STATEMENT]
lemma ptr_add_image_multI:
  "\<lbrakk> \<And>x y. (x * val = y * val') = (x * val'' = y); x * val'' \<in> S \<rbrakk> \<Longrightarrow>
     ptr_add ptr (x * val) \<in> (\<lambda>p. ptr_add ptr (p * val')) ` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. (x * val = y * val') = (x * val'' = y); x * val'' \<in> S\<rbrakk> \<Longrightarrow> ptr_add ptr (x * val) \<in> (\<lambda>p. ptr_add ptr (p * val')) ` S
[PROOF STEP]
by (auto simp add: image_iff) metis


[STATEMENT]
lemma dom_if:
  "dom (\<lambda>a. if a \<in> addrs then Some (f a) else g a)  = addrs \<union> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>a. if a \<in> addrs then Some (f a) else g a) = addrs \<union> dom g
[PROOF STEP]
by (auto simp: dom_def split: if_split)


[STATEMENT]
lemma drop_append_miracle:
  "n = length xs \<Longrightarrow> drop n (xs @ ys) = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> drop n (xs @ ys) = ys
[PROOF STEP]
by simp


[STATEMENT]
lemma foldr_does_nothing_to_xf:
  "\<lbrakk> \<And>x s. x \<in> set xs \<Longrightarrow> xf (f x s) = xf s \<rbrakk> \<Longrightarrow> xf (foldr f xs s) = xf s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x s. x \<in> set xs \<Longrightarrow> xf (f x s) = xf s) \<Longrightarrow> xf (foldr f xs s) = xf s
[PROOF STEP]
by (induct xs, simp_all)


[STATEMENT]
lemma mod_mod_power_int:
  fixes k :: int
  shows "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ (min m n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n
[PROOF STEP]
by (fact mod_exp_eq)


[STATEMENT]
lemma le_step_down_nat:"\<lbrakk>(i::nat) \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by arith


[STATEMENT]
lemma le_step_down_int:"\<lbrakk>(i::int) \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by arith


[STATEMENT]
lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replicate (numeral k) x = x # replicate (pred_numeral k) x
[PROOF STEP]
by (simp add: numeral_eq_Suc)


[STATEMENT]
lemma list_exhaust_size_gt0:
  assumes "\<And>a list. y = a # list \<Longrightarrow> P"
  shows "0 < length y \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length y \<Longrightarrow> P
[PROOF STEP]
apply (cases y)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < length y; y = []\<rbrakk> \<Longrightarrow> P
 2. \<And>a list. \<lbrakk>0 < length y; y = a # list\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>0 < length y; y = a # list\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (rule assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>0 < length y; y = a # list\<rbrakk> \<Longrightarrow> y = ?a1 a list # ?list1 a list
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_exhaust_size_eq0:
  assumes "y = [] \<Longrightarrow> P"
  shows "length y = 0 \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length y = 0 \<Longrightarrow> P
[PROOF STEP]
apply (cases y)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length y = 0; y = []\<rbrakk> \<Longrightarrow> P
 2. \<And>a list. \<lbrakk>length y = 0; y = a # list\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (rule assms)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length y = 0; y = []\<rbrakk> \<Longrightarrow> y = []
 2. \<And>a list. \<lbrakk>length y = 0; y = a # list\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length y = 0; y = a # list\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma size_Cons_lem_eq: "y = xa # list \<Longrightarrow> size y = Suc k \<Longrightarrow> size list = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y = xa # list; length y = Suc k\<rbrakk> \<Longrightarrow> length list = k
[PROOF STEP]
by auto


[STATEMENT]
lemma takeWhile_take_has_property:
  "n \<le> length (takeWhile P xs) \<Longrightarrow> \<forall>x \<in> set (take n xs). P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length (takeWhile P xs) \<Longrightarrow> \<forall>x\<in>set (take n xs). P x
[PROOF STEP]
by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all)


[STATEMENT]
lemma takeWhile_take_has_property_nth:
  "\<lbrakk> n < length (takeWhile P xs) \<rbrakk> \<Longrightarrow> P (xs ! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length (takeWhile P xs) \<Longrightarrow> P (xs ! n)
[PROOF STEP]
by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all)


[STATEMENT]
lemma takeWhile_replicate:
  "takeWhile f (replicate len x) = (if f x then replicate len x else [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takeWhile f (replicate len x) = (if f x then replicate len x else [])
[PROOF STEP]
by (induct_tac len) auto


[STATEMENT]
lemma takeWhile_replicate_empty:
  "\<not> f x \<Longrightarrow> takeWhile f (replicate len x) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> f x \<Longrightarrow> takeWhile f (replicate len x) = []
[PROOF STEP]
by (simp add: takeWhile_replicate)


[STATEMENT]
lemma takeWhile_replicate_id:
  "f x \<Longrightarrow> takeWhile f (replicate len x) = replicate len x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<Longrightarrow> takeWhile f (replicate len x) = replicate len x
[PROOF STEP]
by (simp add: takeWhile_replicate)


[STATEMENT]
lemma nth_rev: "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)
[PROOF STEP]
using rev_nth
[PROOF STATE]
proof (prove)
using this:
?n < length ?xs \<Longrightarrow> rev ?xs ! ?n = ?xs ! (length ?xs - Suc ?n)

goal (1 subgoal):
 1. n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)
[PROOF STEP]
by simp


[STATEMENT]
lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)
[PROOF STEP]
by (simp add: nth_rev)


[STATEMENT]
lemma hd_butlast: "length xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length xs \<Longrightarrow> hd (butlast xs) = hd xs
[PROOF STEP]
by (cases xs) auto


[STATEMENT]
lemma split_upt_on_n:
  "n < m \<Longrightarrow> [0 ..< m] = [0 ..< n] @ [n] @ [Suc n ..< m]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> [0..<m] = [0..<n] @ [n] @ [Suc n..<m]
[PROOF STEP]
by (metis append_Cons append_Nil less_Suc_eq_le less_imp_le_nat upt_add_eq_append'
            upt_rec zero_less_Suc)


[STATEMENT]
lemma drop_eq_mono:
  assumes le: "m \<le> n"
  assumes drop: "drop m xs = drop m ys"
  shows "drop n xs = drop n ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop n xs = drop n ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. drop n xs = drop n ys
[PROOF STEP]
have ex: "\<exists>p. n = p + m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. n = p + m
[PROOF STEP]
by (rule exI[of _ "n - m"]) (simp add: le)
[PROOF STATE]
proof (state)
this:
\<exists>p. n = p + m

goal (1 subgoal):
 1. drop n xs = drop n ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. n = p + m
[PROOF STEP]
obtain p where p: "n = p + m"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. n = p + m

goal (1 subgoal):
 1. (\<And>p. n = p + m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n = p + m

goal (1 subgoal):
 1. drop n xs = drop n ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop n xs = drop n ys
[PROOF STEP]
unfolding p drop_drop[symmetric] drop
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop p (drop m ys) = drop p (drop m ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop n xs = drop n ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drop_Suc_nth:
  "n < length xs \<Longrightarrow> drop n xs = xs!n # drop (Suc n) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> drop n xs = xs ! n # drop (Suc n) xs
[PROOF STEP]
by (simp add: Cons_nth_drop_Suc)


[STATEMENT]
lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys
[PROOF STEP]
by auto


[STATEMENT]
lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (if p then xs else ys) = (if p then tl xs else tl ys)
[PROOF STEP]
by auto


[STATEMENT]
lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (if p then xs else ys) = (if p then hd xs else hd ys)
[PROOF STEP]
by auto