header {* 
  \isaheader{Jinja System Invariants} 
*}

theory JBC_SysInv = JBC_VCG:


section {* Properties of wellformed programs *}

constdefs
wf_md_Ty::"jvm_method wf_mdecl_test"
"wf_md_Ty  \<equiv> (\<lambda>P C (M, Ts, T\<^isub>r, mxs, mxl\<^isub>0, is, xt). wt_method P C Ts T\<^isub>r mxs mxl\<^isub>0 is xt (pTy P C M))"


lemma wf_wfprog:
"wf \<Pi> \<Longrightarrow> wf_prog wf_md_Ty (fst \<Pi>)"
(*<*) by (simp add: wf_def wf_jvm_prog_phi_def wf_md_Ty_def wf_prog_def wf_cdecl_def wf_mdecl_def) (*>*)


lemma wf_ipc_domC:
"wf \<Pi> \<Longrightarrow> ipc \<Pi> \<in> set (domC \<Pi>)"
(*<*) by (simp add: wf_def) (*>*)


lemma main_method_no_args:
"wf (P,An) \<Longrightarrow> fst (snd (method P (fst (ipc (P,An))) (fst (snd (ipc (P,An)))))) = []"
(*<*) by (simp add: JBC_VCG.wf_def) (*>*)


lemma wf_TypeSafe:
"wf \<Pi> \<Longrightarrow> wf_jvm_prog_phi (pTy (fst \<Pi>)) (fst \<Pi>)"
(*<*) by (simp add: JBC_VCG.wf_def)  (*>*)


lemma wf_no_main_call:
"wf \<Pi> \<Longrightarrow> callers \<Pi> (C,fst (snd (ipc \<Pi>)),pc) = []"
(*<*)
apply (simp add: callers_def)
apply (rule filter_False)
apply (rule ballI)
apply (case_tac "cmd \<Pi> x")
apply simp

apply (case_tac "a")
apply simp+
--{* a = Invoke list nat *}
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: JBC_VCG.wf_def checkPos_split split_if[of "\<lambda> x. x" _ _ "False"])
apply (case_tac "anF \<Pi> x")
apply simp

apply (simp split del: option.split_asm)
apply (case_tac "x = ipc \<Pi>")
apply simp

apply (simp split del: option.split_asm)
apply (case_tac "extractTy (aa, St nat)")
apply simp

apply simp
--{* Return bis Throw *}
apply simp+
done
(*>*)


lemma handlesEx'_domC: 
"\<lbrakk> checkExTables (P,An); p \<notin> set (domC (P,An)) \<rbrakk>  \<Longrightarrow> handlesEx' P p = []"
(*<*)
apply (simp only: handlesEx'_def checkExTables_def)
apply (subgoal_tac "\<exists> D. domC (P,An) = D")
 prefer 2
 apply fastsimp
apply (erule exE)
apply (simp only: fst_conv)
apply (erule_tac V="domC (P,An) = D" in thin_rl)
apply (induct P)
apply simp

apply simp
apply atomize
apply (erule_tac x="D" in allE)
apply (subgoal_tac "\<exists> Ca Sa Fsa Msa. a = (Ca,Sa,Fsa,Msa)")
 prefer 2
 apply fastsimp
apply (erule exE | erule conjE)+
apply (simp add: remdups'_append)

apply (rule ballI)
apply (simp only: in_set_conv_decomp)
apply (subgoal_tac "\<exists> M Ts T mxs mxl is et. xs = (M,Ts,T,mxs,mxl,is,et)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply simp
apply (rule ballI)
apply (simp only: in_set_conv_decomp)
apply (subgoal_tac "\<exists> b e cn h d. xsa = (b,e,cn,h,d)")
 prefer 2 
 apply fastsimp
apply (erule exE)+
apply simp
apply (erule conjE | erule exE)+
apply (erule_tac x="ysb" in allE)
apply (erule_tac x="zsb" in allE)
apply (rule classical)
apply simp
done
(*>*)


lemma methodnames_split:
"methodnames (P@P') = methodnames P @ methodnames P'"
(*<*)
apply (induct P)
apply (simp add: methodnames_def)+
done
(*>*)


lemma methodnames_split':
"methodnames (p#P) = methodnames [p] @ methodnames P"
(*<*)
apply (cut_tac P="[p]" and P'="P" in methodnames_split)
apply simp
done
(*>*)


lemma domC_methodnames:
"(C,M,pc) \<in> set (domC (P,An)) \<Longrightarrow> (C,M) \<in> set (methodnames P)"
(*<*)
apply (induct P)
apply (simp add: domC_def)

apply (simp add: methodnames_def domC_def)
apply (case_tac "(\<exists>a\<in>set P. (C, M, pc) \<in> set (domCC a))")
apply simp

apply (subgoal_tac "\<exists> Ca Sa Fsa Msa. a = (Ca,Sa,Fsa,Msa)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add: domCC_split domCC.simps simp_thms)
apply (drule domCC_split_parts)
apply (erule exE)+
apply simp
apply (erule conjE)+
apply (erule imageE)
apply simp
done
(*>*)


constdefs get_mdecl::"jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> mname \<times> ty list \<times> ty \<times> jvm_method"
"get_mdecl P C M \<equiv> hd (concat (map (\<lambda> (C',S,Fs,Ms). [(M',Ts,T,bs)\<in>Ms. M = M' \<and> C = C']) P))"


lemma get_mdecl_append:
"(C,M) \<notin> set (methodnames P) \<Longrightarrow> get_mdecl (P@P') C M = get_mdecl P' C M"
(*<*)
apply (induct P)
apply simp

apply (simp add: get_mdecl_def split_def)
apply (subgoal_tac "methodnames (a # P) = (methodnames [a]) @ (methodnames P)")
 prefer 2
 apply (cut_tac P="[a]" and P'="P" in methodnames_split)
 apply simp
apply (subgoal_tac "\<exists> C S Fs Ms. a = (C,S,Fs,Ms)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add: methodnames_def image_iff)
apply (case_tac "[p\<in>Ms . M = fst p \<and> C = Ca]")
apply simp

apply (simp only:)
apply (subgoal_tac "\<forall>x \<in> set [p\<in>Ms . M = fst p \<and> C = Ca]. M = fst x \<and> C = Ca")
 prefer 2
 apply (simp (no_asm) add: set_filter)
apply (erule_tac x="aa" in ballE)
prefer 2 
apply simp

apply (subgoal_tac "aa \<in> set Ms")
 prefer 2
 apply (rule_tac A="set [p\<in>Ms . M = fst p \<and> C = Ca]" in subsetD)
 apply (rule filter_is_subset)
 apply simp
apply (erule exE | erule conjE)+
apply (erule_tac x="aa" in ballE)
apply (simp add: split_def)
apply simp
done
(*>*)


lemma get_mdecl_append':
"M \<notin> set (map fst Ms) \<Longrightarrow> get_mdecl ((C,S,Fs,Ms@Ms')#P) C M = get_mdecl ((C,S,Fs,Ms')#P) C M"
(*<*)
apply (induct Ms)
apply simp

apply (simp add: split_def get_mdecl_def)
done
(*>*)


lemma methodnames_P:
"(C,M) \<in> set (methodnames P) \<Longrightarrow> \<exists> ps ps' S Fs Ms Ms' Ts T bd. P = ps@(C,S,Fs,Ms@(M,Ts,T,bd)#Ms')#ps' \<and> (C,M) \<notin> set (methodnames ps) \<and> M \<notin> set (map fst Ms) \<and> get_mdecl P C M = (M,Ts,T,bd)"
(*<*)
apply (induct P)
apply (simp add: methodnames_def)
apply (subgoal_tac "methodnames (a # P) = (methodnames [a]) @ (methodnames P)")
 prefer 2
 apply (cut_tac P="[a]" and P'="P" in methodnames_split)
 apply simp
apply (subgoal_tac "\<exists> C S Fs Ms. a = (C,S,Fs,Ms)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (case_tac "(C, M) \<in> set (methodnames [a])")
apply (simp only:)
apply (frule_tac xs="methodnames [(Ca,S,Fs,Ms)]" in in_set_conv_decomp_fst)
apply (erule exE)+
apply (simp add: methodnames_def)
apply (erule conjE)+
apply (drule map_parts)
apply (erule exE | erule conjE)+
apply simp
apply (erule exE)+
apply (rule_tac x="[]" in exI)
apply (rule_tac x="P" in exI)
apply (rule_tac x="S" in exI)
apply (rule_tac x="Fs" in exI)
apply (rule_tac x="xs'" in exI)
apply (rule_tac x="zsa" in exI)
apply (rule_tac x="aa" in exI)
apply (rule_tac x="ab" in exI)
apply (rule_tac x="ac" in exI)
apply (rule_tac x="ad" in exI)
apply (rule_tac x="ae" in exI)
apply (rule_tac x="b" in exI)
apply simp
apply (rule context_conjI)
apply (rule classical)
apply simp
apply (erule imageE)
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: split_def)

apply (simp add: get_mdecl_append' )
apply (simp add: get_mdecl_def)

apply simp
apply (erule exE)+
apply (rule_tac x="(Ca, S, Fs, Ms) # ps" in exI)
apply (rule_tac x="ps'" in exI)
apply (rule_tac x="Sa" in exI)
apply (rule_tac x="Fsa" in exI)
apply (rule_tac x="Msa" in exI)
apply (rule_tac x="Ms'" in exI)
apply (rule_tac x="Ts" in exI)
apply (rule_tac x="T" in exI)
apply (rule_tac x="aa" in exI)
apply (rule_tac x="ab" in exI)
apply (rule_tac x="ac" in exI)
apply (rule_tac x="b" in exI)
apply simp
apply (rule conjI)
apply (simplesubst methodnames_split')
apply simp

apply (drule_tac P="[(Ca, S, Fs, Ms)]" and P'="P" in get_mdecl_append)
apply simp
apply (erule conjE)+
apply simp
done
(*>*)


lemma methodnames_P2:
"\<lbrakk> distinct (classnames P); (C,M) \<in> set (methodnames P) \<rbrakk> \<Longrightarrow> \<exists> ps ps' S Fs Ms Ms' Ts T bd. P = ps@(C,S,Fs,Ms@(M,Ts,T,bd)#Ms')#ps' \<and> (C,M) \<notin> set (methodnames ps) \<and> M \<notin> set (map fst Ms) \<and> get_mdecl P C M = (M,Ts,T,bd) \<and> class P C = Some (S,Fs,Ms@(M,Ts,T,bd)#Ms')"
(*<*)
apply (induct P)
apply (simp add: methodnames_def)
apply (subgoal_tac "methodnames (a # P) = (methodnames [a]) @ (methodnames P)")
 prefer 2
 apply (cut_tac P="[a]" and P'="P" in methodnames_split)
 apply simp
apply (subgoal_tac "\<exists> C S Fs Ms. a = (C,S,Fs,Ms)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (case_tac "(C, M) \<in> set (methodnames [a])")
apply (simp only:)
apply (frule_tac xs="methodnames [(Ca,S,Fs,Ms)]" in in_set_conv_decomp_fst)
apply (erule exE)+
apply (simp add: methodnames_def)
apply (erule conjE)+
apply (drule map_parts)
apply (erule exE | erule conjE)+
apply simp
apply (erule exE)+
apply (rule_tac x="[]" in exI)
apply (rule_tac x="P" in exI)
apply (rule_tac x="S" in exI)
apply (rule_tac x="Fs" in exI)
apply (rule_tac x="xs'" in exI)
apply (rule_tac x="zsa" in exI)
apply (rule_tac x="aa" in exI)
apply (rule_tac x="ab" in exI)
apply (rule_tac x="ac" in exI)
apply (rule_tac x="ad" in exI)
apply (rule_tac x="ae" in exI)
apply (rule_tac x="b" in exI)
apply simp
apply (rule context_conjI)
apply (rule classical)
apply simp
apply (erule imageE)
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: split_def)

apply (simp add: get_mdecl_append' )
apply (simp add: get_mdecl_def)

apply (simp add: classnames_def class_def)

apply (subgoal_tac "distinct (classnames P)")
 prefer 2
 apply (simp add: classnames_def)
apply simp
apply (erule exE)+
apply (rule_tac x="(Ca, S, Fs, Ms) # ps" in exI)
apply (rule_tac x="ps'" in exI)
apply (rule_tac x="Sa" in exI)
apply (rule_tac x="Fsa" in exI)
apply (rule_tac x="Msa" in exI)
apply (rule_tac x="Ms'" in exI)
apply (rule_tac x="Ts" in exI)
apply (rule_tac x="T" in exI)
apply (rule_tac x="aa" in exI)
apply (rule_tac x="ab" in exI)
apply (rule_tac x="ac" in exI)
apply (rule_tac x="b" in exI)
apply simp
apply (rule conjI)
apply (simplesubst methodnames_split')
apply simp

apply (drule_tac P="[(Ca, S, Fs, Ms)]" and P'="P" in get_mdecl_append)
apply simp
apply (erule conjE)+
apply simp

apply (simp add: classnames_def class_def)
apply (rule impI)
apply simp
done
(*>*)


constdefs method'::"jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> cname \<times> ty list \<times> ty \<times> jvm_method"
"method' P C M \<equiv> (let (M',Ts,T,bd)= get_mdecl P C M in (C,Ts,T,bd))"

--{* method' is defined recursively and is thus easier to evaluate for the simplifier than
     method, which is defined inductively. *}

lemma method_method':
"\<lbrakk> wf_prog wf_md P; (C,M) \<in> set (methodnames P) \<rbrakk> \<Longrightarrow> method P C M = method' P C M"
(*<*)
apply (drule methodnames_P)
apply (erule exE | erule conjE)+
apply (simp only: method_def method'_def Let_def split_def fst_conv snd_conv)
apply (rule the_equality)
apply (simp add: split_def)
apply (rule_tac wf_md="wf_md" and S="S" and fs="Fs" and ms="Ms @ (M, Ts, T, bd) # Ms'" in mdecl_visible)
apply simp
apply simp
apply simp

apply (subgoal_tac "\<exists> C' Ts' T' bd'. p = (C',Ts',T',bd')")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply simp
apply (subgoal_tac "Ts' = Ts \<and> T' = T \<and> bd' = bd \<and> C' = C")
 prefer 2
 apply (rule_tac P="ps @ (C, S, Fs, Ms @ (M, Ts, T, bd) # Ms') # ps'" and C="C" and M="M"in  sees_method_fun)
 prefer 2
 apply simp
 apply (rule_tac wf_md="wf_md" and S="S" and fs="Fs" and ms="Ms @ (M, Ts, T, bd) # Ms'" in mdecl_visible)
 apply simp
 apply simp
 apply simp
apply simp
done
(*>*)


constdefs ex_table_of' :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> ex_table"
"ex_table_of' P C M \<equiv> snd (snd (snd (snd (snd (snd(method' P C M))))))"


lemma ex_table_of_ex_table_of':
"\<lbrakk> wf_prog wf_md P; (C,M) \<in> set (methodnames P) \<rbrakk> \<Longrightarrow> ex_table_of P C M = ex_table_of' P C M"
(*<*)
apply (drule method_method')
apply simp
apply (simp add: ex_table_of'_def)
done
(*>*)


lemma match_ex_table_split':
"JVMExceptions.match_ex_table P cn pc et = \<lfloor>(pc',d)\<rfloor> \<Longrightarrow> \<exists> b e c. (b,e,c,pc',d) \<in> set et \<and> P \<turnstile> cn \<preceq>\<^sup>* c"
(*<*)
apply (induct et)
apply simp

apply (subgoal_tac "\<exists> b e c h d. a = (b,e,c,h,d)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply simp
apply (simp add: matches_ex_entry_def split add: split_if_asm)
apply fastsimp

apply (erule exE)+


apply (rule_tac x="ba" in exI)
apply (rule_tac x="ea" in exI)
apply (rule_tac x="ca" in exI)
apply simp
done
(*>*)


lemma match_ex_table_split:
"match_ex_table P cn pc et = \<lfloor>pc'\<rfloor> \<Longrightarrow> \<exists> b e c d. (b,e,c,pc',d) \<in> set et \<and> P \<turnstile> cn \<preceq>\<^sup>* c"
(*<*)
apply (simp only: match_ex_table_def)
apply (case_tac "JVMExceptions.match_ex_table P cn pc et")
apply simp

apply (subgoal_tac "\<exists> h d. a =(h,d)")
 prefer 2
 apply simp
apply (erule exE)+
apply simp
apply (drule match_ex_table_split')
apply fastsimp
done
(*>*)


lemma wf_ex_table_domC:
"\<lbrakk> wf (P,An); (C,M) \<in> set (methodnames P); match_ex_table P X pc (ex_table_of P C M) = Some pc' \<rbrakk> \<Longrightarrow> (C,M,pc') \<in> set (domC (P,An))"
(*<*)
apply (frule methodnames_P)
apply (erule exE)+
apply (subgoal_tac "(ex_table_of P C M) = (ex_table_of' P C M)")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in ex_table_of_ex_table_of')
 apply (drule wf_wfprog)
 apply simp
 apply assumption
apply (erule conjE)+
apply (simp add: wf_def checkExTables_def ex_table_of'_def method'_def split_def)
apply (subgoal_tac "\<exists> mxs mxl is et. bd = (mxs,mxl,is,et)")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (erule exE)+
apply simp

apply (subgoal_tac "\<exists> h d. a = (h,d)")
 prefer 2
 apply simp
apply (erule exE)+
apply simp
apply (drule match_ex_table_split')
apply (erule exE | erule conjE)+
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply simp
done
(*>*)


lemma handlesEx'_ex_table_of:
"\<lbrakk> wf (P,An); (C,M) \<in> set (methodnames P) \<rbrakk> \<Longrightarrow> handlesEx' P (C,M,pc) = remdups' (concat (map (\<lambda>(b, e, cn, h, d). if pc = h then [cn] else []) (ex_table_of P C M)))"
(*<*)
apply (simp only: handlesEx'_def)
apply (subgoal_tac "ex_table_of P C M = ex_table_of' P C M")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in ex_table_of_ex_table_of')
 apply (drule wf_wfprog)
 apply simp
 apply assumption
apply (simp only: ex_table_of'_def method'_def)
apply (drule methodnames_P)
apply (erule exE | erule conjE)+
apply simp 
apply (subgoal_tac "concat (map (\<lambda>(Ca, S, Fs, Ms).
                          concat (map (\<lambda>(Ma, Ts, T, mxs, mxl, is, et).
                                          concat (map (\<lambda>(b, e, cn, h, d). if C = Ca \<and> M = Ma \<and> pc = h then [cn] else []) et))
                                   Ms))
                   ps) = []")
 prefer 2
 apply simp
 apply (rule ballI)
 apply (subgoal_tac "\<exists> Cx Sx Fsx Msx. xs = (Cx,Sx,Fsx,Msx)")
  prefer 2
  apply (erule thin_rl)+
  apply fastsimp
 apply (erule exE)+
 apply simp
 apply (rule ballI)
 apply (simp add: split_def)
 apply (rule ballI)
 apply simp
 apply (erule disjE)
 apply (erule imageE)

 apply (simp only: in_set_conv_decomp)
 apply (erule exE)+
 apply (simp add: methodnames_split methodnames_def)
 apply (erule_tac x="concat (map (split (\<lambda>C. split (\<lambda>S. split (\<lambda>Fs. map (\<lambda>(M, Ts, T, bd). (C, M)))))) ys) @
           map (\<lambda>(M, Ts, T, bd). (Cx, M)) ysa" in allE)
 apply (erule_tac x="map (\<lambda>(M, Ts, T, bd). (Cx, M)) zsa @ concat (map (split (\<lambda>C. split (\<lambda>S. split (\<lambda>Fs. map (\<lambda>(M, Ts, T, bd). (C, M)))))) zs)" in allE)
 apply (simp add: split_def)

 apply (erule imageE)
 apply simp

apply (subgoal_tac "concat (map (\<lambda>(Ma, Ts, T, mxs, mxl, is, et). concat (map (\<lambda>(b, e, cn, h,d). if M = Ma \<and> pc = h then [cn] else []) et)) Ms) = []")
 prefer 2
 apply simp
 apply (rule ballI)
 apply (simp add: split_def)
 apply (rule ballI)
 apply simp
 apply (erule disjE)
 apply (erule imageE)
 apply (simp add: in_set_conv_decomp)

 apply (erule imageE)
 apply simp

apply (subgoal_tac "concat (map (\<lambda>(Ma, Ts, T, mxs, mxl, is, et). concat (map (\<lambda>(b, e, cn, h,d). if M = Ma \<and> pc = h then [cn] else []) et)) Ms') = []")
 prefer 2
 apply (subgoal_tac "M \<notin> fst ` set Ms'")
  prefer 2
  apply (rule classical)
  apply simp
  apply (erule imageE)
  apply (simp add: in_set_conv_decomp)
  apply (erule exE)+
  apply (simp add: wf_def methodnames_split methodnames_def split_def)
  apply simp
 apply (rule ballI)
 apply (simp add: split_def)
 apply (rule ballI)
 apply simp
 apply (erule disjE)
 apply (erule imageE)
 apply (simp add: in_set_conv_decomp)

 apply (erule imageE)
 apply simp
apply (subgoal_tac "concat (map (\<lambda>(Ca, S, Fs, Ms).
                          concat (map (\<lambda>(Ma, Ts, T, mxs, mxl, is, et).
                                          concat (map (\<lambda>(b, e, cn, h,d). if C = Ca \<and> M = Ma \<and> pc = h then [cn] else []) et))
                                   Ms))
                   ps') = []")
 prefer 2
 apply simp
 apply (rule ballI)
 apply (simp add: split_def)
 apply (rule ballI)
 apply (rule ballI)
 apply simp
 apply (erule disjE)
 apply (erule imageE)
 apply (simp add: in_set_conv_decomp)
 apply (erule exE)+
 apply (simp add: wf_def methodnames_split methodnames_def split_def)
 
 apply (erule imageE)
 apply simp

apply (simp only:)
apply (simp add: split_def)
done
(*>*)


lemma has_method_class:
"\<lbrakk> wf (P,An); has_method P C M \<rbrakk> \<Longrightarrow> \<exists> Ts T m. method P C M = (C,Ts,T,m)"
(*<*)
apply (simp only: has_method_def mem_iff)
apply (subgoal_tac "method P C M = method' P C M")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in method_method')
 apply (drule wf_wfprog)
 apply simp
 apply assumption
apply (drule methodnames_P)
apply (erule exE | erule conjE)+
apply (simp add: method'_def)
apply fastsimp
done
(*>*)


lemma wf_extable:
"\<lbrakk> wf (P,An); (C,M) \<in> set (methodnames P); (f,t,c,h,d) \<in> set (ex_table_of P C M) \<rbrakk> \<Longrightarrow> d = 0"
(*<*)
apply (subgoal_tac "ex_table_of P C M = ex_table_of' P C M")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in  ex_table_of_ex_table_of')
 apply (drule wf_wfprog)
 apply simp
 apply assumption
apply (subgoal_tac "distinct (classnames P)")
 prefer 2
 apply (simp add: JBC_VCG.wf_def)
apply (frule methodnames_P2)
apply simp
apply (erule exE | erule conjE)+
apply (simp add: ex_table_of'_def method'_def JBC_VCG.wf_def checkExTables_def)
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: split_def)
done
(*>*)


lemma wf_handlesEx'_length:
"wf (P,An)  \<Longrightarrow> length (handlesEx' P p) \<le> 1"
(*<*)
apply (subgoal_tac "\<exists> C M pc. p = (C,M,pc)")
 prefer 2
 apply (rule_tac x="fst p" in exI)
 apply (rule_tac x="fst (snd p)"  in exI)
 apply (rule_tac x="snd (snd p)" in exI)
 apply simp
apply (erule exE)+
apply (case_tac "p \<in> set (domC (P,An))")
--{* p in domC (P,An) *}
apply (subgoal_tac "(C,M) \<in> set (methodnames P)")
 prefer 2
 apply (rule domC_methodnames)
 apply simp
apply (frule methodnames_P)
apply (frule_tac C="C" and M="M" and pc="pc" in handlesEx'_ex_table_of)
apply assumption
apply (simp only:)
apply (erule_tac V="handlesEx' P (C,M,pc) = ?a" in thin_rl)
apply (subgoal_tac "ex_table_of P C M = ex_table_of' P C M")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in ex_table_of_ex_table_of')
 apply (drule wf_wfprog)
 apply simp
 apply assumption
apply (simp only:)
apply (erule_tac V="ex_table_of P C M = ex_table_of' P C M" in thin_rl)
apply (erule exE | erule conjE)+
apply (simp add: JBC_VCG.wf_def ex_table_of'_def method'_def checkExTables_def)
apply (subgoal_tac "\<exists> mxs mxl is et. bd = (mxs,mxl,is,et)")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (erule exE | erule conjE)+
apply simp 
apply (simp only: length_remdups_set)
apply (rule allI)+
apply (rule impI)
apply simp
apply (erule conjE | erule bexE)+
apply (case_tac "a = aa")
apply (simp add: split_def split add: split_if_asm)

apply (subgoal_tac "(\<exists> ba ea cna ha da. a =(ba,ea,cna,ha,da)) \<and> (\<exists> baa eaa cnaa haa daa. aa =(baa,eaa,cnaa,haa,daa))")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (erule exE | erule conjE)+
apply (case_tac "pc = ha")
prefer 2
apply simp

apply (case_tac "pc = haa")
prefer 2
apply simp

apply (case_tac "cna = cnaa")
apply simp
apply (drule_tac x="a" and y="aa" and s="et" in  in_set_conv_decomp_2)
apply assumption+
apply (erule exE)+
apply (erule disjE)
apply simp
apply (erule conjE)+
apply (subgoal_tac "set (remdups'
         (concat (map (\<lambda>(b, e, cn, h',d'). if h' = ha then [cn] else []) s') @
          cna # concat (map (\<lambda>(b, e, cn, h',d'). if h' = ha then [cn] else []) s'') @
                cnaa # concat (map (\<lambda>(b, e, cn, h',d'). if h' = ha then [cn] else []) s'''))) = set [cna]")
 prefer 2
 apply (simp only: set_remdups')
apply simp

apply simp
apply (erule conjE)+
apply (subgoal_tac "set (remdups'
         (concat (map (\<lambda>(b, e, cn, h',d'). if h' = ha then [cn] else []) s') @
          cnaa #
          concat (map (\<lambda>(b, e, cn, h',d'). if h' = ha then [cn] else []) s'') @
          cna # concat (map (\<lambda>(b, e, cn, h',d'). if h' = ha then [cn] else []) s'''))) = set [cna]")
 prefer 2
 apply (simp only: set_remdups')
apply simp

--{* p notin domC (P,An) *}
apply (subgoal_tac "handlesEx' P p = []")
 prefer 2
 apply (rule_tac An="An" in handlesEx'_domC)
 apply (simp add: JBC_VCG.wf_def)
 apply simp
apply simp
done
(*>*)

(*
lemma wf_handlesEx'_noObject:
"\<lbrakk> wf (P,An);  cn \<in> set (handlesEx' P p) \<rbrakk> \<Longrightarrow> cn \<noteq> Object"
apply (subgoal_tac "\<exists> C M pc. p = (C,M,pc)")
 prefer 2
 apply (rule_tac x="fst p" in exI)
 apply (rule_tac x="fst (snd p)"  in exI)
 apply (rule_tac x="snd (snd p)" in exI)
 apply simp
apply (erule exE)+
apply (case_tac "p \<in> set (domC (P,An))")
apply (subgoal_tac "(C,M) \<in> set (methodnames P)")
 prefer 2
 apply (rule domC_methodnames)
 apply simp
apply (frule methodnames_P)
apply (frule_tac C="C" and M="M" and pc="pc" in handlesEx'_ex_table_of)
apply assumption
apply (simp only:)
apply (erule_tac V="handlesEx' P (C,M,pc) = ?a" in thin_rl)
apply (subgoal_tac "ex_table_of P C M = ex_table_of' P C M")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in ex_table_of_ex_table_of')
 apply (drule wf_wfprog)
 apply simp
 apply assumption
apply (simp only:)
apply (erule_tac V="ex_table_of P C M = ex_table_of' P C M" in thin_rl)
apply (erule exE | erule conjE)+
apply (simp add: JBC_VCG.wf_def ex_table_of'_def method'_def checkExTables_def)
apply (subgoal_tac "\<exists> mxs mxl is et. bd = (mxs,mxl,is,et)")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (erule exE | erule conjE)+
apply (simp add: set_remdups')
apply (erule bexE) 
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (subgoal_tac "(\<exists> ba ea cna ha da. a =(ba,ea,cna,ha,da))")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (erule exE | erule conjE)+
apply simp
apply (case_tac "pc = ha")
apply simp
apply (case_tac "ysd")
apply simp

apply simp

apply simp

apply (subgoal_tac "handlesEx' P p = []")
 prefer 2
 apply (rule_tac An="An" in handlesEx'_domC)
 apply (simp add: JBC_VCG.wf_def)
 apply simp
apply simp
done
*)

lemma wf_domC_cmd:
assumes wf_Pi: "wf \<Pi>"
shows "set (domC \<Pi>) = {p. cmd \<Pi> p \<noteq> None}"
(*<*)
proof (intro set_ext iffI)
fix p
assume p_domC: "p \<in> set (domC \<Pi>)"
show "p \<in> {p. cmd \<Pi> p \<noteq> None}"
proof -
  obtain C M pc
  where p_def: "p = (C,M,pc)"
    by (cases p)

  obtain P An
  where Pi_def: "\<Pi> = (P,An)"
    by (cases \<Pi>)
  
  from p_def p_domC Pi_def
  have C_M_methodnames: "(C,M) \<in> set (methodnames P)"
    by (simp add: domC_methodnames)

  from wf_Pi Pi_def
  have distinct_classnames: "distinct (classnames P)"
    by (simp add: wf_def)

  from wf_Pi Pi_def
  have distinct_methodnames: "distinct (methodnames P)"
    by (simp add: wf_def)

  from distinct_classnames C_M_methodnames Pi_def
  obtain ps ps' S Fs Ms Ms' Ts T bd
  where P_split: "P = ps @ (C, S, Fs, Ms @ (M, Ts, T, bd) # Ms') # ps'"
  and C_M_out_ps: "(C,M) \<notin> set (methodnames ps)"
  and M_out_Ms: "M \<notin> set (map fst Ms)"
  and get_mdecl_P_C_M: "get_mdecl P C M = (M,Ts,T,bd)"
  and class_P_C: "class P C = Some (S, Fs, Ms @ (M, Ts, T, bd) # Ms')"
    apply -
    apply (rule methodnames_P2[elim_format])
    apply simp
    apply assumption
    apply (erule conjE | erule exE)+
    apply (rule that)
    apply assumption+
    done

  from M_out_Ms 
  have map_of_Ms_M_None: "map_of Ms M = None"
    by (simp add: map_of_eq_None_iff)

  have p_out_domCC_ps: "p \<notin> set (concat (map domCC ps))"
    proof (rule ccontr)
      assume contr: "\<not> (p \<notin> set (concat (map domCC ps)))" 
      show "False"
	proof -

	  from contr
	  have p_in_domCC_ps: "p \<in> set (concat (map domCC ps))"
	    by simp

	  from p_in_domCC_ps
	  obtain c psc psc' where ps_split: "ps = psc @ c#psc'"
                            and p_domCC_c: "p \<in> set (domCC c)"
	    apply -
	    apply simp
	    apply (erule bexE)
	    apply (subgoal_tac "\<exists> psa psa'. ps = psa @ a#psa'")
	     prefer 2
	     apply (simp only: in_set_conv_decomp)
	    apply (erule exE)+
	    apply (rule that)
	    apply assumption
	    apply assumption
	    done

	  obtain c_C c_S c_fs' c_ms 
	    where c_def: "c = (c_C,c_S,c_fs',c_ms)"
	    by (cases c)
	  
	  from p_def  p_domCC_c c_def 
	  obtain c_ms' c_ms'' Ts_c T_c m_c mxs_c mxl_c is_c et_c
	    where c_ms_split: "c_ms = c_ms' @ (M,Ts_c,T_c,mxs_c,mxl_c,is_c,et_c) # c_ms''"
	    and p_domMC_c: "p \<in> set (domMC (c_C,M,mxs_c,mxl_c,is_c,et_c))"
	    apply -
	    apply (simp only:)
	    apply (erule domCC_split_parts[elim_format])
	    apply (erule conjE | erule exE)+
	    apply (rule that)
	    apply assumption
	    apply (simp only:)
	    done

	  from p_def p_domMC_c
	  have c_C_eq_C: "c_C = C"
	    apply -
	    apply (simp only:)
	    apply (drule domMC_props)
	    apply simp
	    done

	  from P_split ps_split c_def c_ms_split c_C_eq_C distinct_methodnames
	  show "False"
	    apply -
	    apply (simp only: methodnames_def map_append split_def fst_conv snd_conv map.simps)
	    apply simp
	    done
	qed
      qed

  have p_out_domCC_ps': "p \<notin> set (concat (map domCC ps'))"
    proof (rule ccontr)
      assume contr: "\<not> (p \<notin> set (concat (map domCC ps')))" 
      show "False"
	proof -

	  from contr
	  have p_in_domCC_ps': "p \<in> set (concat (map domCC ps'))"
	    by simp

	  from p_in_domCC_ps'
	  obtain c ps'c ps'c' where ps'_split: "ps' = ps'c @ c#ps'c'"
                            and p_domCC_c: "p \<in> set (domCC c)"
	    apply -
	    apply simp
	    apply (erule bexE)
	    apply (subgoal_tac "\<exists> ps'a ps'a'. ps' = ps'a @ a#ps'a'")
	     prefer 2
	     apply (simp only: in_set_conv_decomp)
	    apply (erule exE)+
	    apply (rule that)
	    apply assumption
	    apply assumption
	    done

	  obtain c_C c_S c_fs' c_ms 
	    where c_def: "c = (c_C,c_S,c_fs',c_ms)"
	    by (cases c)
	  
	  from p_def  p_domCC_c c_def 
	  obtain c_ms' c_ms'' Ts_c T_c m_c mxs_c mxl_c is_c et_c
	    where c_ms_split: "c_ms = c_ms' @ (M,Ts_c,T_c,mxs_c,mxl_c,is_c,et_c) # c_ms''"
	    and p_domMC_c: "p \<in> set (domMC (c_C,M,mxs_c,mxl_c,is_c,et_c))"
	    apply -
	    apply (simp only:)
	    apply (erule domCC_split_parts[elim_format])
	    apply (erule conjE | erule exE)+
	    apply (rule that)
	    apply assumption
	    apply (simp only:)
	    done

	  from p_def p_domMC_c
	  have c_C_eq_C: "c_C = C"
	    apply -
	    apply (simp only:)
	    apply (drule domMC_props)
	    apply simp
	    done

	  from P_split ps'_split c_def c_ms_split c_C_eq_C distinct_methodnames
	  show "False"
	    apply -
	    apply (simp only: methodnames_def map_append split_def fst_conv snd_conv map.simps)
	    apply simp
	    done
	qed
      qed

    from p_out_domCC_ps p_out_domCC_ps' p_domC Pi_def P_split
    have p_domCC: "p \<in> set (domCC (C, S, Fs, Ms @ (M, Ts, T, bd) # Ms'))"
      by (simp add: domC_def domCC_split)

    have p_out_domMC_Ms: "p \<notin> set (concat (map (\<lambda> (M,Ts,T,m). domMC (C,M,m)) Ms))"
      proof (rule ccontr)
	assume contr: "\<not> p \<notin> set (concat (map (\<lambda>(M, Ts, T, m). domMC (C, M, m)) Ms))"
	show "False"
	  proof -
	    from contr have p_domMC_Ms: "p \<in> set (concat (map (\<lambda>(M, Ts, T, m). domMC (C, M, m)) Ms))"
	      by blast

	    from p_domMC_Ms
	    obtain mt Ms_mt Ms_mt' 
	      where p_domMC_mt: "p \<in> set (domMC ((\<lambda> (M,Ts,T,m). (C,M,m)) mt))"
	      and Ms_split: "Ms = Ms_mt @ (mt#Ms_mt')"
	      apply -
	      apply simp
	      apply (erule bexE)
	      apply (simp add: split_def)
	      apply atomize
	      apply (erule_tac x="a" in allE)
	      apply simp
	      apply (simp only: in_set_conv_decomp)
	      done

	    obtain mt_M mt_Ts mt_T mt_m
	      where mt_def: "mt = (mt_M,mt_Ts,mt_T,mt_m)"
	      by (cases mt)

	    from mt_def p_domMC_mt p_def
	    have mt_M_eq_M: "mt_M = M"
	      apply -
	      apply (simp only: split_def fst_conv snd_conv)
	      apply (drule domMC_props)
	      apply simp
	      done
	   
	    from distinct_methodnames P_split Ms_split mt_def mt_M_eq_M
	    show "False"
            apply -
	    apply (simp only: methodnames_def map_append split_def fst_conv snd_conv map.simps)
	    apply simp
	    done
	qed
      qed

  have p_out_domMC_Ms': "p \<notin> set (concat (map (\<lambda> (M,Ts,T,m). domMC (C,M,m)) Ms'))"
      proof (rule ccontr)
	assume contr: "\<not> p \<notin> set (concat (map (\<lambda>(M, Ts, T, m). domMC (C, M, m)) Ms'))"
	show "False"
	  proof -
	    from contr have p_domMC_Ms': "p \<in> set (concat (map (\<lambda>(M, Ts, T, m). domMC (C, M, m)) Ms'))"
	      by blast

	    from p_domMC_Ms'
	    obtain mt Ms'_mt Ms'_mt' 
	      where p_domMC_mt: "p \<in> set (domMC ((\<lambda> (M,Ts,T,m). (C,M,m)) mt))"
	      and Ms'_split: "Ms' = Ms'_mt @ (mt#Ms'_mt')"
	      apply -
	      apply simp
	      apply (erule bexE)
	      apply (simp add: split_def)
	      apply atomize
	      apply (erule_tac x="a" in allE)
	      apply simp
	      apply (simp only: in_set_conv_decomp)
	      done

	    obtain mt_M mt_Ts mt_T mt_m
	      where mt_def: "mt = (mt_M,mt_Ts,mt_T,mt_m)"
	      by (cases mt)

	    from mt_def p_domMC_mt p_def
	    have mt_M_eq_M: "mt_M = M"
	      apply -
	      apply (simp only: split_def fst_conv snd_conv)
	      apply (drule domMC_props)
	      apply simp
	      done
	   
	    from distinct_methodnames P_split Ms'_split mt_def mt_M_eq_M
	    show "False"
            apply -
	    apply (simp only: methodnames_def map_append split_def fst_conv snd_conv map.simps)
	    apply simp
	    done
	qed
      qed

      from p_domCC p_out_domMC_Ms p_out_domMC_Ms' p_def
      have p_domMC: "p \<in> set (domMC (C,M,bd))"
	apply -
	apply (simp only: domCC_map)
	apply simp
	done

      from p_domMC p_def
      have pc_in_bd: "pc < length (fst (snd (snd bd)))"
	apply -
	apply (simp only:)
	apply (drule domMC_props)
	apply simp
	done
      
  
  from class_P_C get_mdecl_P_C_M map_of_Ms_M_None p_def Pi_def pc_in_bd
  have cmd_p_Some: "cmd \<Pi> p = Some (fst (snd (snd bd)) ! pc)"
    apply -
    apply (simp only: cmd_def fst_conv snd_conv  split_def
           map_of_append map_add_def get_mdecl_def option.cases)
    apply simp
    done

  from cmd_p_Some
  show "p \<in> {p. cmd \<Pi> p \<noteq> None}"
    by blast
qed

next

fix p
assume cmd_p_neq_None: "p \<in> {p. cmd \<Pi> p \<noteq> None}"
show "p \<in> set (domC \<Pi>)"
proof -
  from cmd_p_neq_None
  obtain i where cmd_p_Some: "cmd \<Pi> p = Some i"
    by fastsimp

  from cmd_p_Some
  show "p \<in> set (domC \<Pi>)"
    proof (rule cmd_domC)
    qed
  qed
qed
(*>*)

lemma has_method_has_method:
"TypeRel.has_method P C M \<Longrightarrow> \<exists> D Ts T m. has_method P D M \<and> P \<turnstile> C \<preceq>\<^sup>* D \<and> method P C M = (D,Ts,T,m) \<and> method P D M = (D,Ts,T,m)"
(*<*)
apply (simp add: TypeRel.has_method_def Method_def)
apply (erule exE | erule conjE)+
apply (erule_tac P="Mm M = Some ((Ts, T, a, aa, ab, b), D)" in rev_mp)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch8)
apply (rule allI)
apply (simp only: all_simps(6))
apply (rule impI)
apply (erule Methods.induct)
--{* rule: sees-methods-Object *}
apply (rule allI)+
apply (rule impI)
apply (simp add: has_method_def mem_iff methodnames_def)
apply (rule conjI)
apply (simp add: class_def)
apply (drule map_of_SomeD)
apply (rule_tac x="(Object,(D,fs,ms))" in bexI)
 prefer 2
 apply simp
apply (erule conjE)+
apply simp
apply (drule map_of_SomeD)
apply (drule_tac x="(M, Ts, T, a, aa, ab, b)" and f="(\<lambda>(M, Ts, T, bd). (Object, M))" in imageI)
apply simp

apply (subgoal_tac "(Object, Mma) \<in> Methods P")
 prefer 2
 apply (rule_tac D="D" and fs="fs" and ms="ms" in sees_methods_Object)
 apply assumption
 apply assumption
apply (rule_tac x="Ts" in exI)
apply (rule_tac x="T" in exI)
apply (rule_tac x="a" in exI)
apply (rule_tac x="aa" in exI)
apply (rule_tac x="ab" in exI)
apply (rule_tac x="b" in exI)
apply (rule method_def2)
apply (simp add: Method_def)
apply (rule_tac x="Mma" in exI)
apply simp

--{* rule: sees-methods-rec *}
apply (rule allI)+
apply (rule impI)
apply (subgoal_tac "P \<turnstile> C sees_methods Mm'")
 prefer 2
 apply (rule_tac D="D" and fs="fs" and ms="ms" and Mm="Mma" in sees_methods_rec)
 apply (simp add: class_def)
 apply assumption
 apply assumption
 apply assumption
apply (simp add: map_add_def)
apply (erule exE | erule conjE)+
apply (rule_tac x="Db" in exI)
apply (rule conjI)
apply simp
apply (rule conjI)
apply (rule_tac b="D" in converse_rtrancl_into_rtrancl)
apply (rule_tac rest="(fs,ms)" in subcls1I)
apply assumption
apply assumption
apply assumption
apply (subgoal_tac "method P D M = (Da, Ts, T, a, aa, ab, b)")
 prefer 2
 apply (rule method_def2)
 apply (simp only: Method_def)
 apply (rule_tac x="Mma" in exI)
 apply simp
apply (rule_tac x="Ts" in exI)
apply (rule_tac x="T" in exI)
apply (rule_tac x="a" in exI)
apply (rule_tac x="aa" in exI)
apply (rule_tac x="ab" in exI)
apply (rule_tac x="b" in exI)
apply (rule conjI)
apply (rule method_def2)
apply (simp only: Method_def)
apply (rule_tac x="(\<lambda>x. option_case (Mma x) Some (option_map (\<lambda>m. (m, C)) (map_of ms x)))" in exI)
apply simp

apply simp

apply (erule exE | erule conjE)+
apply (drule_tac s="C" and t="Da" in sym)
apply (simp only:)
apply (rule_tac x="C" in exI)

apply (rule conjI)
apply (simp add: has_method_def class_def mem_iff methodnames_def)
apply (drule map_of_SomeD)+
apply (rule_tac x="(C,D,fs,ms)" in bexI)
 prefer 2
 apply simp
apply simp
apply (drule_tac x="(M, Ts, T, a, aa, ab, b)" and f="(\<lambda>(M, Ts, T, bd). (C, M))" in imageI)
apply simp

apply (rule conjI)
apply simp

apply (rule_tac x="Ts" in exI)
apply (rule_tac x="T" in exI)
apply (rule_tac x="a" in exI)
apply (rule_tac x="aa" in exI)
apply (rule_tac x="ab" in exI)
apply (rule_tac x="b" in exI)
apply (simp (no_asm_simp))
apply (rule method_def2)
apply (simp add: Method_def)
apply (rule_tac x="(\<lambda>x. option_case (Mma x) Some (option_map (\<lambda>m. (m, C)) (map_of ms x)))" in exI)
apply simp
done
(*>*)

lemma domC_cmd_instr_of:
"\<lbrakk> wf \<Pi>; (C,M,pc) \<in> set (domC \<Pi>) \<rbrakk> \<Longrightarrow> cmd \<Pi> (C,M,pc) = Some (instrs_of (fst \<Pi>) C M ! pc)"
(*<*)
apply (subgoal_tac "\<exists> P An. \<Pi> = (P,An)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply simp
apply (frule domC_methodnames)
apply (subgoal_tac "method P C M = method' P C M")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in method_method')
 apply (drule wf_wfprog)
 apply simp
 apply simp
apply (unfold JBC_VCG.wf_def)
apply (erule conjE)+
apply (frule methodnames_P2)
apply simp

apply (erule exE | erule conjE)+
apply (simp only: cmd_def split_def fst_conv snd_conv)
apply (simp only: method'_def Let_def split_def fst_conv snd_conv option.cases) 
apply (subgoal_tac "map_of (Ms @ (M, Ts, T, bd) # Ms') M = Some (Ts,T,bd)")
 prefer 2
 apply (subgoal_tac " map_of (Ms @ ((M, Ts, T, bd) # Ms')) M = map_of ((M, Ts, T, bd) # Ms') M")
  prefer 2
  apply (rule map_of_append')
  apply simp
 apply simp
apply (simp only: option.cases)
apply (simp add: domC_def domCC_split del: domCC.simps)
apply (subgoal_tac "(C, M, pc) \<in> set (domMC (C, M, bd))")
 prefer 2
 apply (case_tac "\<exists>a\<in>set ps. (C, M, pc) \<in> set (domCC a)")
 apply (erule bexE)
 apply (subgoal_tac "\<exists> Ca Ca' Fsa Msa. a = (Ca,Ca',Fsa,Msa)")
  prefer 2
  apply (simp (no_asm) add: split_paired_all)
 apply (erule exE)+
 apply (simp only: domCC_map)
 apply (simp add: set_concat_map split_def)
 apply (erule bexE)
 apply (drule domMC_props)
 apply (erule conjE)+
 apply (simp add: classnames_def)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE)+
 apply simp

 apply (case_tac "(\<exists>a\<in>set ps'. (C, M, pc) \<in> set (domCC a))")
 apply (erule bexE)
 apply (subgoal_tac "\<exists> Ca Ca' Fsa Msa. a = (Ca,Ca',Fsa,Msa)")
  prefer 2
  apply (simp (no_asm) add: split_paired_all)
 apply (erule exE)+
 apply (simp only: domCC_map)
 apply (simp add: set_concat_map split_def)
 apply (erule bexE)
 apply (drule domMC_props)
 apply (erule conjE)+
 apply (simp add: classnames_def)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE)+
 apply simp

 apply (case_tac "(C, M, pc) \<in> set (domCC (C, S, Fs, Ms'))")
 apply (simp only: domCC_map)
 apply (simp add: set_concat_map split_def)
 apply (erule bexE)
 apply (drule domMC_props)
 apply (erule conjE)+
 apply (simp add: classnames_def methodnames_def)
 apply (erule conjE)+
 apply (erule_tac P="a \<in> set Ms'" in rev_mp)
 apply (erule_tac P="(C, fst a) \<notin> (\<lambda>(M, Ts, T, bd). (C, M)) ` set Ms'" in rev_mp)
 apply (erule thin_rl)+
 apply (rule impI)+
 apply (simp only: in_set_conv_decomp)
 apply (erule exE)+
 apply (simp add: split_def)

 apply (case_tac "(C, M, pc) \<in> set (domCC (C, S, Fs, Ms))")
 apply (simp only: domCC_map)
 apply (simp add: set_concat_map split_def)
 apply (erule bexE)
 apply (drule domMC_props)
 apply (erule conjE)+
 apply (simp add: classnames_def methodnames_def)
 apply simp
apply (drule domMC_props)
apply simp
done
(*>*)


lemma startstate_initS:
"wf (P,An) \<Longrightarrow> (p,\<sigma>,e) \<in> (initS (P,An)) \<Longrightarrow> \<exists> C M T m. \<sigma> = start_state P C M \<and> (P \<turnstile> C sees M:[]\<rightarrow>T = m in C)"
(*<*)
apply (simp only: initS_def)
apply (rule_tac x="fst (ipc (P,An))" in exI)
apply (rule_tac x="fst (snd (ipc (P,An)))" in exI)
apply (subgoal_tac "ipc (P,An) \<in> set (domC (P,An))")
 prefer 2
 apply (simp add: JBC_VCG.wf_def)
apply (simp only: ipc_def)
apply (drule domC_methodnames)
apply (frule methodnames_P)
apply (erule conjE | erule exE)+
apply (subgoal_tac "P \<turnstile> Start sees main: Ts \<rightarrow> T = bd in Start")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" and S="S" and fs="Fs" and ms="Ms @ (main, Ts, T, bd) # Ms'" in  mdecl_visible)
 apply (drule wf_wfprog)
 apply simp 
 apply simp
 apply simp
apply (subgoal_tac "method' P Start main = (Start,Ts,T,bd)")
 prefer 2
 apply (simp add: method'_def)
apply (subgoal_tac "method' P Start main = method P Start main")
 prefer 2
 apply (rule_tac wf_md1="wf_md_Ty" in  method_method'[THEN sym])
 apply (drule wf_wfprog)
 apply simp
 
 apply simp
apply (simp only:)
apply (erule_tac V="method' ?P Start main = method ?P Start main" in thin_rl)
apply (drule_tac s="(Start,Ts,T,bd)" in sym)
apply (drule main_method_no_args)
apply (simp only: ipc_def fst_conv snd_conv)
apply (rule_tac x="T" in exI)
apply (rule_tac x="bd" in exI)
apply simp
done
(*>*)


lemma wf_safeP_domC:
"\<lbrakk> wf \<Pi>; (p,\<sigma>,e) \<in> safeP \<Pi> \<rbrakk> \<Longrightarrow> p \<in> set (domC \<Pi>)"
(*<*)
apply (erule safeP.elims)
apply (simp add: JBC_VCG.wf_def initS_def)
apply (drule_tac t="s" in sym)
apply simp

apply (simp add: safeF_def valid_def)
apply (drule_tac t="s'" in sym)
apply simp
apply (drule cmd_domC)+
apply assumption
done
(*>*)


lemma drop_length_eq:
"\<And> st st'. \<lbrakk> drop k st = []; length st = length st' \<rbrakk> \<Longrightarrow> drop k st' = []"
(*<*)
apply (induct k)
apply simp

apply (case_tac "st")
apply simp
apply (case_tac "st'")
apply simp

apply simp
done
(*>*)


lemma drop_le: "\<And> L. drop k L = [] \<Longrightarrow> length L \<le> k"
(*<*)
apply (induct k)
apply simp
apply (case_tac "L")
apply simp
apply atomize
apply (erule_tac x="list" in allE)
apply (simp only: drop.simps nat.cases refl simp_thms)
apply simp
done
(*>*)


lemma jbc_sim_jvm:
"wf (P,An) \<Longrightarrow> ((p,\<sigma>,e),(p',\<sigma>',e')) \<in> effS (P,An) \<Longrightarrow> (\<sigma>,\<sigma>') \<in> exec_1 P"
(*<*)
apply (rule exec_1I) 
apply (erule effS.elims)
apply simp

apply simp
done
(*>*)


lemma jbc_sim_jvm_d:
"wf (P,An) \<Longrightarrow> check P \<sigma> \<Longrightarrow> ((p,\<sigma>,e),(p',\<sigma>',e')) \<in> effS (P,An) \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow>\<^isub>1 Normal \<sigma>'"
(*<*)
apply (rule exec_1_d_NormalI)
apply (simp add: exec_d_def)
apply (frule jbc_sim_jvm)
apply assumption
apply (simp only: exec_1_iff)
done
(*>*)


lemma effS_jvmd_hull:
"wf (P,An) \<Longrightarrow> (p,\<sigma>,e) \<in> initS (P,An) \<Longrightarrow> ((p,\<sigma>,e),(p',\<sigma>',e')) \<in> (effS (P,An))\<^sup>* \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow> Normal \<sigma>'"
(*<*)
apply (subgoal_tac "(\<lambda> xa xb.  P \<turnstile> Normal (fst (snd xa)) -jvmd\<rightarrow> Normal (fst (snd xb))) (p,\<sigma>,e) (p',\<sigma>',e')") 
 prefer 2
 apply (erule_tac P="(p,\<sigma>,e) \<in> initS (P,An)" in rev_mp)
 apply (erule rtrancl.induct)
 apply (simp add: exec_all_d_def1)

 apply (rule impI)
 apply (simp add: exec_all_d_def1)
 apply (rule_tac b="Normal (fst (snd b))" in rtrancl_into_rtrancl)
 apply simp
 apply (subgoal_tac "check P (fst (snd b))")
  prefer 2
  apply (subgoal_tac "\<exists> C M T m. fst (snd a) = start_state P C M \<and> (P \<turnstile> C sees M:[]\<rightarrow>T = m in C)")
   prefer 2
   apply (rule_tac p="fst a" and e="snd (snd a)" in startstate_initS)
   apply assumption
   apply simp
  apply (erule conjE | erule exE)+
  apply (rule_tac \<sigma>="fst (snd a)" and C="C" and M="M" and T="T" and m="m" in check_inv)
  apply (simp add: wf_def jvm_kildall_correct wf_jvm_prog_def)
  apply (rule_tac x="(JBC_VCG.pTy P)" in exI)
  apply simp

  apply simp

  apply (rule defensive_imp_aggressive)
  apply (simp add: exec_all_d_def1)
 apply (rule_tac An="An" and p="fst b" and p'="fst c" and e="snd (snd b)" and e'="snd (snd c)" in jbc_sim_jvm_d)
 apply assumption
 apply assumption
 apply simp
apply simp
done
(*>*)


lemma effS_jvm_hull:
"wf (P,An) \<Longrightarrow> (p,\<sigma>,e) \<in> initS (P,An) \<Longrightarrow> ((p,\<sigma>,e),(p',\<sigma>',e')) \<in> (effS (P,An))\<^sup>* \<Longrightarrow> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'"
(*<*)
by (rule defensive_imp_aggressive, rule effS_jvmd_hull, assumption+)
(*>*)


lemma wf_ipc_no_Invoke:
assumes wf_Pi: "wf \<Pi>"
shows "\<forall> Mn n. cmd \<Pi> (ipc \<Pi>) \<noteq> Some (Invoke Mn n)"
(*<*)
--{* Initial stack is empty, but Invoke expects a reference. *}
proof (cases "cmd \<Pi> (ipc \<Pi>)")

case None
from None show ?thesis
  by simp

next

case (Some i)

obtain \<Phi>k where PhiK_def: "\<Phi>k = (convert_pt (prog_kil (fst \<Pi>)))"
  by fastsimp
from PhiK_def 

obtain \<Phi> where Phi_def: "\<Phi> = map_of2 \<Phi>k"
  by fastsimp
from wf_Pi Phi_def PhiK_def 

have wt_Pi: "wf_jvm_prog_phi \<Phi> (fst \<Pi>)"
  apply -
  apply (drule wf_TypeSafe)
  apply (simp add: pTy_def)
  done

obtain P An where Pi_def: "\<Pi> = (P,An)"
  by fastsimp

from Some Pi_def
have ipc_methodnames: "(Start,main) \<in> set (methodnames P)"
  apply -
  apply (drule cmd_domC)
  apply (simp only: ipc_def)
  apply (rule_tac pc="0" and An="An" and P="P" in domC_methodnames)
  apply simp
  done

from wf_Pi Pi_def have classnames_P:"distinct (classnames P)"
  by (simp add: wf_def)

from ipc_methodnames classnames_P
obtain ps ps' S Fs Ms Ms' Ts Tr mxs mxl0 bd xt 
where P_format: "P = ps@(Start, S, Fs, Ms @ (main, Ts, Tr, (mxs,mxl0,bd,xt)) # Ms')#ps' \<and> (Start, main) \<notin> set (methodnames ps) \<and>
        main \<notin> set (map fst Ms) \<and>  get_mdecl P Start main = (main,Ts,Tr,(mxs,mxl0,bd,xt)) \<and> class P Start = \<lfloor>(S, Fs, Ms @ (main, Ts, Tr,(mxs,mxl0,bd,xt)) # Ms')\<rfloor>"
      apply -
      apply atomize
      apply (frule methodnames_P2)
      apply simp
      apply (erule exE | erule conjE)+
      apply (erule_tac x="ps" in allE)
      apply (erule_tac x="S" in allE)
      apply (erule_tac x="Fs" in allE)
      apply (erule_tac x="Ms" in allE)
      apply (erule_tac x="Ts" in allE)
      apply (erule_tac x="T" in allE)
      apply (erule_tac x="fst bd" in allE)
      apply (erule_tac x="fst (snd bd)" in allE)
      apply (erule_tac x="fst (snd (snd bd))" in allE)
      apply (erule_tac x="snd (snd (snd bd))" in allE)
      apply (erule_tac x="Ms'" in allE)
      apply (erule_tac x="ps'" in allE)
      apply simp
      done

from wt_Pi Pi_def
have wf_prog_P: "wf_prog (\<lambda>P C (M, Ts, Tr, mxs, mxl\<^isub>0, is, xt). wt_method P C Ts Tr mxs mxl\<^isub>0 is xt (\<Phi> C M)) P"
  by (simp add: wf_jvm_prog_phi_def)

from wf_prog_P Pi_def P_format ipc_methodnames
have method_P_Start_main: "method P Start main = (Start,Ts,Tr,(mxs,mxl0,bd,xt))"
  apply -
      apply (drule method_method')
      apply simp

      apply simp
      apply (erule conjE)+
      apply (simp only: method'_def Let_def split_def fst_conv snd_conv)
      done

from P_format wf_prog_P
have wt_m_Start_main:"wt_method P Start Ts Tr mxs mxl0 bd xt (\<Phi> Start main)"
  apply (simp add: wf_prog_def wf_cdecl_def wf_mdecl_def)
  done

from wt_m_Start_main
have wt_start: "wt_start P Start Ts mxl0 (\<Phi> Start main)"
 by (simp add: wt_method_def)

from wt_m_Start_main have wt_Start_main:"bd \<noteq> [] \<and> length (\<Phi> Start main) = length bd 
  \<and> OK ` set (\<Phi> Start main) \<subseteq> states P mxs (1 + length Ts + mxl0) \<and> 
  wt_app_eff (sup_state_opt P) (\<lambda>pc. app (bd ! pc) P mxs Tr pc (length bd) xt) (\<lambda>pc. eff (bd ! pc) P pc xt) (\<Phi> Start main)"
      by (simp add: TF_JVM.JVM_sl.wt_method_def2)

from Some P_format method_P_Start_main Pi_def wf_Pi
have pc_in_bd: "0 < length bd \<and> bd ! 0 = i"
  apply -
  apply (erule conjE)+
  apply (frule domC_cmd_instr_of)
  apply (rule cmd_domC)
  apply (simp add: ipc_def)
  
  apply (simp add: cmd_def split_def get_mdecl_def map_add_def ipc_def)
  apply (drule_tac t="a" in sym)
  apply simp
  apply (case_tac "0 < length bd")
  apply simp
      
  apply simp

  apply (drule map_of_SomeD)
  apply (simp only: in_set_conv_decomp)
  apply (erule exE | erule conjE)+
  apply simp
  done

from pc_in_bd wt_Start_main have app_i: "app i P mxs Tr 0 (length bd) xt ((\<Phi> Start main) ! 0)"
  apply -
  apply (simp add: wt_app_eff_def)
  apply (erule conjE)+
  apply (erule_tac x="0" in allE)
  apply simp
  done
    
 from  wt_start pc_in_bd obtain \<tau> where tau_intro: "(\<Phi> Start main) ! 0 = Some \<tau>"
   apply -
   apply (simp only: wt_start_def)
   apply (case_tac "\<Phi> Start main ! 0 = None")
   apply simp
   
   apply simp
   apply (erule exE)+
   apply simp
   done

 obtain ST LT where tau_def: "\<tau> = (ST,LT)"
   by fastsimp

 from wt_start tau_intro tau_def have ST_Nil: "ST = []"
   apply -
   apply (simp add: wt_start_def)
   done

 from app_i Some tau_intro tau_def ST_Nil
 show ?thesis
   apply -
   apply (rule classical)
   apply simp
   apply (erule exE)+
   apply (simp add: app_def)
   done
 qed
(*>*)

section {* Welltypedness guarantees successful instruction checks. *}

--{* checkinstr' is a weaker variant of checkinstr *}

consts
  check_instr' :: "[instr, jvm_prog, heap, val list, val list, 
                  cname, mname, pc, frame list] \<Rightarrow> bool"
primrec 
check_instr'_Load:
  "check_instr' (Load n) P h stk loc C M\<^isub>0 pc frs = 
  (n < length loc)"

check_instr'_Store:
  "check_instr' (Store n) P h stk loc C\<^isub>0 M\<^isub>0 pc frs = 
  (0 < length stk \<and> n < length loc)"

check_instr'_Push:
  "check_instr' (Push v) P h stk loc C\<^isub>0 M\<^isub>0 pc frs = 
  (\<not>is_Addr v)"

check_instr'_New:
  "check_instr' (New C) P h stk loc C\<^isub>0 M\<^isub>0 pc frs = 
  is_class P C"

check_instr'_Getfield:
  "check_instr' (Getfield F C) P h stk loc C\<^isub>0 M\<^isub>0 pc frs = 
  (0 < length stk \<and> is_Ref' h (hd stk))"

check_instr'_Putfield:
  "check_instr' (Putfield F C) P h stk loc C\<^isub>0 M\<^isub>0 pc frs = 
  (1 < length stk \<and> is_Ref' h (hd (tl stk)))"


check_instr'_Checkcast:
  "check_instr' (Checkcast C) P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (0 < length stk \<and> is_class P C \<and> is_Ref' h (hd stk))"

check_instr'_Invoke:
  "check_instr' (Invoke M n) P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (n < length stk \<and> is_Ref' h (stk!n) \<and> (stk!n \<noteq> Null \<longrightarrow> TypeRel.has_method P (cname_of h (the_Addr (stk!n)))  M))"

 
check_instr'_Return:
  "check_instr' Return P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (0 < length stk)"


 check_instr'_Pop:
  "check_instr' Pop P h stk loc C\<^isub>0 M\<^isub>0 pc frs = 
  (0 < length stk)"

check_instr'_IBin:
  "check_instr' (IBin no) P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (1 < length stk \<and> is_Intg (hd stk) \<and> is_Intg (hd (tl stk)))"

check_instr'_IfIntCmp:
  "check_instr' (IfIntCmp ro b) P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (1 < length stk \<and> is_Intg (hd stk) \<and> is_Intg (hd (tl stk)) \<and> 0 \<le> int pc + b)"

check_instr'_IfFalse:
  "check_instr' (IfFalse b) P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (0 < length stk \<and> is_Bool (hd stk) \<and> 0 \<le> int pc+b)"

check_instr'_CmpEq:
  "check_instr' CmpEq P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (1 < length stk)"

check_instr'_Goto:
  "check_instr' (Goto b) P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (0 \<le> int pc+b)"

check_instr'_Throw:
  "check_instr' Throw P h stk loc C\<^isub>0 M\<^isub>0 pc frs =
  (0 < length stk \<and> is_Ref' h (hd stk))"

(*<*) lemmas vs [simp] = evalE_evalEs.simps valid_def the_Bool_def (*>*)


lemma wf_invTys_check':
assumes wf_Pi: "wf \<Pi>"
assumes s_def: "s = (p,\<sigma>,e)"
assumes p_def: "p = (C,M,pc)"
assumes sigma_def: "\<sigma> = (None,h,(stk,loc,(C,M,pc))#frs)"
assumes s_invTy: "\<Pi>,s \<Turnstile> inv_Ty \<Pi> p"
assumes cmd_p: "cmd \<Pi> p = Some i"
shows "check_instr' i (fst \<Pi>) h stk loc C M pc frs"
(*<*)
proof -
    obtain \<Phi>k where PhiK_def: "\<Phi>k = (convert_pt (prog_kil (fst \<Pi>)))"
      by fastsimp
    from PhiK_def 
    obtain \<Phi> where Phi_def: "\<Phi> = map_of2 \<Phi>k"
      by fastsimp
    from wf_Pi Phi_def PhiK_def 
    have wt_Pi: "wf_jvm_prog_phi \<Phi> (fst \<Pi>)"
      apply -
      apply (drule wf_TypeSafe)
      apply (simp add: pTy_def)
      done
    obtain P An where Pi_def: "\<Pi> = (P,An)"
      by fastsimp

    from cmd_p p_def Pi_def
    have C_M_methodnames: "(C,M) \<in> set (methodnames P)"
      apply -
      apply (drule cmd_domC)
      apply (rule_tac pc="pc" and An="An" and P="P" in domC_methodnames)
      apply simp
      done

    from wf_Pi Pi_def have classnames_P:"distinct (classnames P)"
      by (simp add: wf_def)

    from C_M_methodnames classnames_P
    obtain ps ps' S Fs Ms Ms' Ts Tr mxs mxl0 bd xt 
    where P_format: "P = ps@(C, S, Fs, Ms @ (M, Ts, Tr, (mxs,mxl0,bd,xt)) # Ms')#ps' \<and> (C, M) \<notin> set (methodnames ps) \<and>
        M \<notin> set (map fst Ms) \<and>  get_mdecl P C M = (M,Ts,Tr,(mxs,mxl0,bd,xt)) \<and> class P C = \<lfloor>(S, Fs, Ms @ (M, Ts, Tr,(mxs,mxl0,bd,xt)) # Ms')\<rfloor>"
      apply -
      apply atomize
      apply (frule methodnames_P2)
      apply simp
      apply (erule exE | erule conjE)+
      apply (erule_tac x="ps" in allE)
      apply (erule_tac x="S" in allE)
      apply (erule_tac x="Fs" in allE)
      apply (erule_tac x="Ms" in allE)
      apply (erule_tac x="Ts" in allE)
      apply (erule_tac x="T" in allE)
      apply (erule_tac x="fst bd" in allE)
      apply (erule_tac x="fst (snd bd)" in allE)
      apply (erule_tac x="fst (snd (snd bd))" in allE)
      apply (erule_tac x="snd (snd (snd bd))" in allE)
      apply (erule_tac x="Ms'" in allE)
      apply (erule_tac x="ps'" in allE)
      apply simp
      done

    from wt_Pi Pi_def
    have wf_prog_P: "wf_prog (\<lambda>P C (M, Ts, Tr, mxs, mxl\<^isub>0, is, xt). wt_method P C Ts Tr mxs mxl\<^isub>0 is xt (\<Phi> C M)) P"
      by (simp add: wf_jvm_prog_phi_def)

    from wf_prog_P Pi_def P_format C_M_methodnames
    have method_P_C_M: "method P C M = (C,Ts,Tr,(mxs,mxl0,bd,xt))"
      apply -
      apply (drule method_method')
      apply simp

      apply simp
      apply (erule conjE)+
      apply (simp only: method'_def Let_def split_def fst_conv snd_conv)
      done

    from P_format wf_prog_P
    have wt_m_C_M:"wt_method P C Ts Tr mxs mxl0 bd xt (\<Phi> C M)"
      apply -
      apply (simp add: wf_prog_def wf_cdecl_def wf_mdecl_def)
      done

    from wt_m_C_M have wt_C_M:"bd \<noteq> [] \<and> length (\<Phi> C M) = length bd 
    \<and> OK ` set (\<Phi> C M) \<subseteq> states P mxs (1 + length Ts + mxl0) \<and> 
    wt_app_eff (sup_state_opt P) (\<lambda>pc. app (bd ! pc) P mxs Tr pc (length bd) xt) (\<lambda>pc. eff (bd ! pc) P pc xt) (\<Phi> C M)"
      by (simp add: TF_JVM.JVM_sl.wt_method_def2)

    from cmd_p p_def P_format method_P_C_M Pi_def wf_Pi
    have pc_in_bd: "pc < length bd \<and> bd ! pc = i"
      apply -
      apply (erule conjE)+
      apply (frule domC_cmd_instr_of)
      apply (rule cmd_domC)
      apply simp
      apply (simp add: cmd_def split_def get_mdecl_def map_add_def)
      apply (drule_tac t="a" in sym)
      apply simp
      apply (case_tac "pc < length bd")
      apply simp
      
      apply simp

      apply (drule map_of_SomeD)
      apply (simp only: in_set_conv_decomp)
      apply (erule exE | erule conjE)+
      apply simp
      done

    from pc_in_bd wt_C_M have app_i: "app i P mxs Tr pc (length bd) xt ((\<Phi> C M) ! pc)"
      apply -
      apply (simp add: wt_app_eff_def)
      apply (erule conjE)+
      apply (erule_tac x="pc" in allE)
      apply simp
      done

    from s_invTy s_def p_def C_M_methodnames Pi_def wt_C_M pc_in_bd obtain \<tau> where tau_intro: "(\<Phi> C M) ! pc = Some \<tau>"
      by (simp add: inv_Ty_def annotate_types_def mem_iff Phi_def PhiK_def map_of2_def lookup_map_of valid_def)

    obtain ST LT where tau_def: "\<tau> = (ST,LT)"
      by fastsimp

    from Pi_def s_def p_def sigma_def tau_intro C_M_methodnames wt_C_M pc_in_bd tau_def s_invTy
    have s_tau: "\<Pi>,s \<Turnstile> conv_st P (ST,LT)"
      by (simp add: inv_Ty_def annotate_types_def Phi_def PhiK_def map_of2_def lookup_map_of mem_iff)

    from s_tau 
    have s_ST: "\<forall> n < length ST. \<Pi>,s \<Turnstile> STy P (St n) (ST ! n)"
      by (simp add: conv_st_def evalEs_map list_all_iff)

    from s_tau
    have s_LT: "\<forall> n < length LT. \<forall> lty. LT ! n = OK lty \<longrightarrow> \<Pi>,s \<Turnstile> STy P (Rg n) lty"
      apply -
      apply (rule allI | rule impI)+
      apply (simp add: conv_st_def evalEs_map list_all_iff)
      apply (erule_tac x="evalE \<Pi> s (STy P (Rg n) lty)" in ballE)
      apply simp

      apply (simp add: image_iff)
      apply (erule conjE)+
      apply (erule_tac x="n" in allE)+
      apply simp
      done

    from s_tau
    have s_LT: "\<forall> n < length LT. (\<forall> lty. LT ! n = OK lty \<longrightarrow> \<Pi>,s \<Turnstile> STy P (Rg n) lty) \<and> (LT ! n = Err \<longrightarrow> \<Pi>,s \<Turnstile> not_none (Rg n))"
      apply -
      apply (rule allI | rule impI)+
      apply (simp add: conv_st_def evalEs_map list_all_iff)
      apply (case_tac "LT ! n = Err")
      apply (erule_tac x="evalE \<Pi> s (not_none (Rg n))" in ballE)
      apply simp

      apply (simp add: image_iff)
      apply (erule conjE)+
      apply (erule_tac x="n" in allE)+
      apply simp

      apply simp
      apply (erule exE)
      apply (erule_tac x="evalE \<Pi> s (STy P (Rg n) a)" in ballE)
      apply simp

      apply (simp add: image_iff)
      apply (erule conjE)+
      apply (erule_tac x="n" in allE)+
      apply simp
      done

    show "check_instr' i (fst \<Pi>) h stk loc C M pc frs"
      proof (cases i)
	case (Load n)
	from Load app_i s_LT tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule exE | erule conjE)+
	  apply (erule_tac x="n" in allE)
	  apply (simp add: evalE_STy)
	  apply (case_tac "n < length loc")
	  apply simp
	  
	  apply simp
	  done

      next

	case (Store n)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule exE | erule conjE)+
	  apply (erule_tac x="n" in allE)
	  apply (erule_tac x="0" in allE)
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp

	  apply simp
	  apply (case_tac "n < length loc")
	  apply simp

	  apply (simp add: not_none_def none_def)
	  done

      next

	case (Push v)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule exE | erule conjE)+
	  apply (case_tac "v::val")
	  apply simp
	  apply simp
	  apply simp
	  apply simp
	  apply simp
	  done
	
      next

	case (New Cln)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  by (simp add: app_def)

      next

	case (Getfield Fn Cln)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule conjE | erule exE)+
	  apply (erule_tac x="0" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp

	  apply simp
	  apply (case_tac "a::val")
	  apply simp
	  apply simp
	  apply simp
	  apply simp
	  apply (simp add: is_Ref'_def)
	  done
	
      next

	case (Putfield Fn Cln)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule conjE | erule exE)+
	  apply (erule_tac x="1" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp

	  apply (case_tac "list")
	  apply simp

	  apply simp
	  apply (case_tac "a::val")
	  apply simp
	  apply simp
	  apply simp
	  apply simp
	  apply (simp add: is_Ref'_def)
	  done

      next

	case (Checkcast Cln)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule conjE | erule exE)+
	  apply (erule_tac x="0" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp

	  apply simp
	  apply (case_tac "a::val")
	  apply (simp add: is_refT_def) 
	  apply (simp add: is_refT_def)
	  apply (simp add: is_refT_def)
	  apply (simp add: is_refT_def)
	  apply (simp add: is_refT_def is_Ref'_def)
	  done

      next
	
	case (Invoke Mn n)

	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule conjE | erule exE)+
	  apply (erule_tac x="n" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "n < length stk")
	  prefer 2
	  apply simp

	  apply (case_tac "a::val")
	  apply simp
	  apply simp
	  apply simp
	  apply simp
	  apply (simp add: is_Ref'_def)
	  apply (case_tac "ST ! n = NT")
	  apply (simp add: obj_ty_def)

	  apply (simp add: obj_ty_def has_method_def)
	  apply (erule exE | erule conjE)+
	  apply (subgoal_tac "\<exists>D' Ts' T' m'. P \<turnstile> (fst aa) sees Mn: Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T")
	   prefer 2
	   apply (rule_tac C="Ca" and wf_md="wf_md_Ty" in sees_method_mono)
	   apply simp

	   apply (cut_tac wf_Pi)
	   apply (drule wf_wfprog)
	   apply (simp add: Pi_def)

	   apply simp
	  apply (erule exE | erule conjE)+
	  apply (simp only: TypeRel.has_method_def)
	  apply (rule_tac x="Ts'" in exI)
	  apply (rule_tac x="T'" in exI)
	  apply (rule_tac x="m'" in exI)
	  apply (rule_tac x="D'" in exI)
	  apply assumption
	  done

      next

	case Return
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule exE | erule conjE)+
	  apply (erule_tac x="0" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp
	  apply simp
	  done

      next 

	case Pop	
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule exE | erule conjE)+
	  apply (erule_tac x="0" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp
	  apply simp
	  done

      next

	case (IBin no)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (subgoal_tac "evalE (P, An) ((C, M, pc), (None, h, (stk, loc, C, M, pc) # frs), e) (STy P (St 1) (ST ! 1)) = \<lfloor>Bool True\<rfloor>")
	   prefer 2
	   apply (erule exE | erule conjE)+
	   apply (erule_tac x="1" in allE)+
	   apply simp
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp

	  apply (case_tac "list")
	  apply simp
	  
	  apply (subgoal_tac "is_Intg a")
	   prefer 2
	   apply (case_tac "a::val")
	   apply simp
	   apply simp
	   apply simp
	   apply simp
	   apply (simp add: obj_ty_def)
	  apply (subgoal_tac "is_Intg aa")
	   prefer 2
	   apply (erule_tac x="0" in allE)
	   apply (simp add: evalE_STy)
	   apply (case_tac "aa::val")
	   apply simp
	   apply simp
	   apply simp
	   apply simp
	   apply (simp add: obj_ty_def)
	  apply simp
	  done

      next

	case (Goto t)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  by (simp add: app_def)

      next

	case CmpEq
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule exE | erule conjE)+
	  apply (erule_tac x="Suc 0" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "Suc 0 < length stk")
	  apply simp
	  
	  apply simp
	  done

      next
	
	case (IfIntCmp ro t)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (subgoal_tac "evalE (P, An) ((C, M, pc), (None, h, (stk, loc, C, M, pc) # frs), e) (STy P (St 1) (ST ! 1)) = \<lfloor>Bool True\<rfloor>")
	   prefer 2
	   apply (erule exE | erule conjE)+
	   apply (erule_tac x="1" in allE)+
	   apply simp
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp

	  apply (case_tac "list")
	  apply simp
	  
	  apply (subgoal_tac "is_Intg a")
	   prefer 2
	   apply (case_tac "a::val")
	   apply simp
	   apply simp
	   apply simp
	   apply simp
	   apply (simp add: obj_ty_def)
	  apply (subgoal_tac "is_Intg aa")
	   prefer 2
	   apply (erule_tac x="0" in allE)
	   apply (simp add: evalE_STy)
	   apply (case_tac "aa::val")
	   apply simp
	   apply simp
	   apply simp
	   apply simp
	   apply (simp add: obj_ty_def)
	  apply simp
	  done

      next

	case (IfFalse t)
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule exE | erule conjE)+
	  apply (erule_tac x="0" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp

	  apply simp
	  apply (case_tac "a::val")
	  apply (simp add: obj_ty_def)+
	  done

      next
	case Throw
	from this app_i s_LT s_ST tau_intro tau_def s_def p_def sigma_def Pi_def 
	show ?thesis
	  apply (simp add: app_def)
	  apply (erule exE | erule conjE)+
	  apply (erule_tac x="0" in allE)+
	  apply (simp add: evalE_STy)
	  apply (case_tac "stk")
	  apply simp

	  apply simp
	  apply (case_tac "a::val")
	  apply (simp add: obj_ty_def is_refT_def is_Ref'_def)+
	  done

      qed
qed
(*>*)

lemma Reachables_conv:
"s \<in> (Reachables \<Pi>) = (\<exists>s0. s0 \<in> initS \<Pi> \<and> (s0, s) \<in> (effS \<Pi>)\<^sup>* )"
(*<*) by (rule effS_Reachables) (*>*)


lemma ReachableFromInv_S_I:
"s \<in> ReachableFromInv R S I \<Longrightarrow> s \<in> S \<or> s \<in>  I"
(*<*)
apply (erule ReachableFromInv.elims)
apply simp

apply simp
done
(*>*)


lemma ReachablesAn_ReachableFromInv:
"ReachablesAn \<Pi> = ReachableFromInv (effS \<Pi>) (initS \<Pi>) {s. \<Pi>,s \<Turnstile> aF \<Pi> (fst s)}"
(*<*)
apply (rule set_ext)
apply (rule iffI)
apply (erule ReachablesAn.induct)
apply (rule ReachableFromInv.init)
apply simp

apply (rule ReachableFromInv.step)
apply simp

apply simp

apply simp

apply simp

--{* iffI 2nd dir *}
apply (erule ReachableFromInv.induct)
apply (rule ReachablesAn.init)
apply simp

apply (rule ReachablesAn.step)
apply simp

apply simp

apply simp

apply simp
done
(*>*)


lemma wf_Reachables_check:
"\<lbrakk> wf \<Pi>; s \<in> Reachables \<Pi> \<rbrakk> \<Longrightarrow> check (fst \<Pi>) (fst (snd s))"
(*<*)
apply (simp only: Reachables_conv)
apply (erule conjE | erule exE)+
apply (subgoal_tac "\<exists> p0 \<sigma>0 e0. s0 = (p0,\<sigma>0,e0)") 
 prefer 2
 apply fastsimp
apply (subgoal_tac "\<exists> P An. \<Pi> = (P,An)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp only:)
apply (subgoal_tac "\<exists>C M T m. \<sigma>0 = start_state P C M \<and> P \<turnstile> C sees M: []\<rightarrow>T = m in C")
 prefer 2
 apply (rule startstate_initS)
 apply simp
 apply simp
apply (erule exE)+

apply (subgoal_tac "wf_jvm_prog (fst \<Pi>)")
 prefer 2
 apply (drule wf_TypeSafe)
 apply (simp only: wf_jvm_prog_def)
 apply (rule_tac x="pTy (fst \<Pi>)" in exI)
 apply simp

apply (rule_tac \<sigma>="\<sigma>0" and C="C" and M="M" and T="T" and m="m" in check_inv)
apply (simp only: jvm_kildall_correct)

apply simp

apply (subgoal_tac "exec_all P \<sigma>0 (fst (snd s))")
 prefer 2
 apply (rule_tac p'="fst s" and e'="snd (snd s)" in effS_jvm_hull)
 apply simp
 apply simp
 apply simp
apply simp
done
(*>*)


section {* System Exceptions *}


lemma sys_xcpt_invariant:
"\<And> s p x h frs e. \<lbrakk> s=(p,(x,h,frs),e); s \<in> safeP \<Pi>; C \<in> sys_xcpts \<rbrakk> 
 \<Longrightarrow> (\<exists>ob. (h (addr_of_sys_xcpt C)) = Some ob \<and> obj_ty ob = Class C)"
(*<*)
apply (erule rev_mp)+
apply (simp only: atomize_all all_simps)
apply (rule impI)
apply (rule allI)
apply (rule impI)

apply (erule safeP.induct)

apply (rule allI)+
apply (rule impI)
apply (erule exE)+
apply (simp add: initS_def start_state_def start_heap_def sys_xcpts_def sys_xcptns_def obj_ty_def addr_of_sys_xcpt_def split_def ClassCast_def NullPointer_def OutOfMemory_def)
apply (case_tac "C = NullPointer")
apply (simp add: NullPointer_def blank_def)
apply (case_tac "C = ClassCast")
apply (simp add: ClassCast_def blank_def)
apply (case_tac "C = OutOfMemory")
apply (simp add: OutOfMemory_def blank_def)
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def)

apply (subgoal_tac "\<exists>pa xa ha frsa ea. sa = (pa,(xa,ha,frsa),ea)")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (rule allI)+
apply (rule impI)
apply (erule exE)+
apply (erule_tac x="pa" in allE)
apply (erule_tac x="xa" in allE)
apply (erule_tac x="ha" in allE)
apply (subgoal_tac "(\<exists>frs e. sa = (pa, (xa, ha, frs), e))")
 prefer 2
 apply (simp only:)
 apply (erule thin_rl)+
 apply fastsimp
apply (drule mp, assumption)

apply (erule effS.elims)
--{* Exception Case *}
apply (case_tac "i")

apply simp+

--{* Normal Execution *}
apply (erule conjE)+
apply (drule_tac t="instrs_of (fst \<Pi>) Ca M ! pc" in sym)
apply (case_tac "i")
apply simp+


--{* New *}
apply (simp add: sys_xcptns_def sys_xcpts_def  addr_of_sys_xcpt_def new_Addr_def blank_def OutOfMemory_def ClassCast_def NullPointer_def)
apply (erule conjE)+
apply (drule_tac s="hb(a \<mapsto> (list, init_fields (TypeRel.fields (fst \<Pi>) list)))" in sym)
apply (case_tac "C = ''OutOfMemory''")
apply (simp add: sys_xcptns_def sys_xcpts_def  addr_of_sys_xcpt_def new_Addr_def blank_def OutOfMemory_def ClassCast_def NullPointer_def)
apply (rule impI)
apply (case_tac "\<exists>a. hb a = None")
apply (simp add: some_eq_ex[THEN sym])
apply simp

apply (case_tac "C = ''ClassCast''")
apply (simp add: sys_xcptns_def sys_xcpts_def  addr_of_sys_xcpt_def new_Addr_def blank_def OutOfMemory_def ClassCast_def NullPointer_def)
apply (rule impI)
apply (case_tac "\<exists>a. hb a = None")
apply (simp add: some_eq_ex[THEN sym])
apply simp

apply simp
apply (rule impI)
apply (case_tac "\<exists>a. hb a = None")
apply (simp add: some_eq_ex[THEN sym])
apply simp

--{* Getfield *}
apply (simp add: split_def)

--{* Putfield *}
apply (simp add: simp_thms split_def sys_xcptns_def sys_xcpts_def  addr_of_sys_xcpt_def new_Addr_def blank_def OutOfMemory_def ClassCast_def NullPointer_def)
apply (erule conjE)+
apply (drule_tac t="h'" in sym)+
apply (drule_tac t="h" in sym)
apply (erule disjE)
apply simp
apply (erule exE)+
apply simp

apply (erule disjE)
apply simp
apply (erule exE)+
apply (simp add: ClassCast_def)
apply (rule impI)
apply (drule_tac s="Suc 0" in sym)
apply simp

apply (simp add: OutOfMemory_def ClassCast_def)
apply (erule exE)+
apply simp

--{* Checkcast *}
apply simp

--{* Invoke *}
apply (simp add: split_def)

--{* Return *}
apply (case_tac "frsb")
apply (simp add: split_def)

apply (simp add: split_def)

--{* Pop *}
apply simp+
done
(*>*)


lemma sys_xcpt_class:
"\<lbrakk> wf \<Pi>; C \<in> sys_xcpts \<rbrakk> \<Longrightarrow> (\<exists> fs ms. class (fst \<Pi>) C = Some (Exception,fs,ms))"
(*<*)
apply (simp add: initF_def sys_xcpts_def sys_xcptns_def obj_ty_def addr_of_sys_xcpt_def split_def ClassCast_def NullPointer_def OutOfMemory_def JBC_VCG.wf_def SystemClasses_def ObjectC_def NullPointerC_def OutOfMemoryC_def ClassCastC_def ExceptionC_def Object_def Exception_def class_def)
apply (erule conjE )+
apply (erule disjE, simp, fastsimp)+
apply (simp, fastsimp)
done
(*>*)


lemma callstates_callers_sysinv:
"\<And> s s'. \<lbrakk> callers_sysinv (\<Pi>,s); s' \<in> (callstates s) \<rbrakk> \<Longrightarrow> callers_sysinv (\<Pi>,s')"
(*<*)
apply (erule callstates.induct)
apply (simp add: split_paired_all del: callers_sysinv.simps)
apply (case_tac "ba")
apply simp
apply (case_tac "list")
apply simp
apply (simp add: split_paired_all)

apply (simp add: split_paired_all del: callers_sysinv.simps)
apply (case_tac "bd")
apply simp
apply (case_tac "list")
apply simp
apply (simp add: split_paired_all)
done
(*>*)


lemma Reachables_pos:
"\<lbrakk> wf \<Pi>; (p,(x,h,(st,rg,p')#frs),e) \<in> Reachables \<Pi> \<rbrakk> \<Longrightarrow> p = p'"
(*<*)
apply (subgoal_tac "(\<lambda> (p,\<sigma>,e). p = snd (snd (hd (snd (snd \<sigma>))))) (p,(x,h,(st,rg,p')#frs),e)")
 prefer 2
 apply (erule_tac P="\<lambda> (p,\<sigma>,e). p = snd (snd (hd (snd (snd \<sigma>))))" and xa="(p,(x,h,(st,rg,p')#frs),e)" in Reachables.induct)
 apply (simp add: initS_def start_state_def split_def ipc_def split add: list.split list.split_asm)

 apply (simp add: split_def split_paired_all)
 apply (erule effS.elims)
 apply simp

 apply simp
apply simp
done
(*>*)


lemma safeP_pos:
"\<lbrakk> wf \<Pi>; (p,(x,h,(st,rg,p')#frs),e) \<in> safeP \<Pi> \<rbrakk> \<Longrightarrow> p = p'"
(*<*)
apply (drule safeP_Reachables)
apply (rule Reachables_pos)
apply assumption
apply assumption
done
(*>*)


lemma callers_sysinv_domC:
"\<And> p x h e. callers_sysinv (\<Pi>,(p,(x,h,frs),e)) \<Longrightarrow>  \<forall> p \<in> set (map (snd \<circ> snd) frs). p \<in> set (domC \<Pi>)"
(*<*)
apply (induct frs)
apply simp

apply atomize
apply (drule_tac P="\<lambda> x. x" in subst[OF callers_sysinv.simps])
apply (case_tac "frs")
apply (simp add: Let_def split_def mem_iff del: callers_sysinv.simps)

apply (simp add: Let_def split_def mem_iff del: callers_sysinv.simps)
apply (subgoal_tac "(\<exists>a ab b x h e. callers_sysinv (\<Pi>, (a, ab, b), (x, h, aa # list), e))")
 prefer 2
 apply (rule_tac x="fst (snd (snd aa))" in exI)
 apply (rule_tac x="fst (snd (snd (snd aa)))" in exI)
 apply (rule_tac x="snd (snd (snd (snd aa)))" in exI)
 apply (rule_tac x="None" in exI)
 apply (rule_tac x="hd (cs e)" in exI)
 apply (rule_tac x="e\<lparr>cs := tl (cs e)\<rparr>" in exI)
 apply simp
apply simp
done
(*>*)


lemma catchstate_eq:
"\<forall> P X p x h h' fr fr' fc frs e. catchstate (P,X,(p,(x,h,fr#fc#frs),e)) = catchstate (P,X,(p,(x,h',fr'#fc#frs),e))"
(*<*)
apply (rule allI)
apply (simp add: split_paired_all)
done
(*>*)


lemma callers_eq:
"callers \<Pi> (C,M,pc) = callers \<Pi> (C,M,pc')"
(*<*)
apply (simp add: callers_def)
apply (induct "domC \<Pi>")
apply simp

apply simp
apply (case_tac "cmd \<Pi> a")
apply simp

apply (case_tac "aa")
apply simp+
done
(*>*)


lemma callers_eq_Suc: "callers \<Pi> (C,M,Suc pc) = callers \<Pi> (C,M,pc)"
(*<*) by (rule callers_eq) (*>*)


lemma callers_eq_Add: "callers \<Pi> (C,M,nat (int pc) + b) = callers \<Pi> (C,M,pc)"
(*<*) by (rule callers_eq) (*>*)


lemma callers_eq_Add2: "callers \<Pi> (C,M,nat (int pc + b)) = callers \<Pi> (C,M,pc)"
(*<*) by (rule callers_eq) (*>*)


(*<*)
lemmas callers_simps = callers_eq_Suc callers_eq_Add callers_eq_Add2
(*>*)


lemma callers_sysinv_env:
"\<And> p h h' e e'. callers_sysinv (\<Pi>,(p,(None,h,frs),e)) = callers_sysinv (\<Pi>,(p,(None,h',frs),e'))"
(*<*)
apply (simp only: atomize_all)
apply (induct_tac frs)
apply simp

apply (rule allI)+

apply (simp (no_asm_simp))
apply (case_tac "list")
apply simp



apply (simp (no_asm_simp) add: split_def del: callers_sysinv.simps)
apply fastsimp
done
(*>*)


lemma match_ex_table_handlesEx':
"\<lbrakk> wf (P,An); (C,M) \<in> set (methodnames P); match_ex_table P cn pc (ex_table_of P C M) = Some pc' \<rbrakk> \<Longrightarrow> \<exists>cns cn' cns'. handlesEx' P (C,M,pc') = cns@ cn'#cns' \<and>  P \<turnstile> cn \<preceq>\<^sup>* cn'"
(*<*)
apply (simp only: handlesEx'_ex_table_of)

apply (simp only: list_set_pred set_remdups') 

apply (induct "ex_table_of P C M")
apply  simp

apply atomize

apply (subgoal_tac "\<exists> b e c h. a = (b,e,c,h)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (case_tac "matches_ex_entry P cn pc a")

apply (simp add: matches_ex_entry_def split_paired_all split_def)

apply (simp add: split_def)
apply (rule impI)
apply simp
done
(*>*)


lemma handlesEx_domC:
"\<lbrakk> wf (P,An); handlesEx P p = Some C \<rbrakk> \<Longrightarrow> p \<in> set (domC (P,An)) "
(*<*)
apply (simp add: handlesEx_def)
apply (rule classical)
apply (subgoal_tac "handlesEx' P p =  []")
 prefer 2
 apply (rule_tac An="An" in handlesEx'_domC)
 apply (simp add: JBC_VCG.wf_def)
 apply assumption
apply simp
done
(*>*)


lemma findhandler_handlesEx':
"\<And> p'. \<lbrakk> wf (P,An);  find_handler P xa h frs = (None, h, ([Addr xa], loc', p') # frs'); handlesEx' P p' \<noteq> [] \<rbrakk>
\<Longrightarrow> \<exists> cns cn cns'. handlesEx' P p' = cns@cn# cns' \<and> P \<turnstile> (cname_of h xa) \<preceq>\<^sup>* cn"
(*<*)
apply (subgoal_tac "\<exists>p'C p'M p'pc. p' = (p'C,p'M,p'pc)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp only:)
apply (induct frs)
apply (simp add: split_def)

apply (subgoal_tac "(p'C,p'M,p'pc) \<in> set (domC (P,An))")
 prefer 2
 apply (rule classical)
 apply (subgoal_tac "handlesEx' P (p'C,p'M,p'pc) = []")
 prefer 2
 apply (rule_tac An="An" in handlesEx'_domC)
 apply (simp add: JBC_VCG.wf_def)
 apply assumption
apply simp

apply (erule_tac P="find_handler P xa h ?a = (?b xa h)" in rev_mp)
apply (simp (no_asm_simp))
apply (simp add: split_def del: find_handler.simps)
apply atomize
apply (rule allI)
apply (rule impI)+
apply (drule_tac C="p'C" and M="p'M" and cn="cname_of h xa" and pc'="p'pc" and pc="(snd (snd (snd (snd a))))" in match_ex_table_handlesEx')
apply (rule_tac pc="p'pc" and An="An" in domC_methodnames)
apply assumption
apply simp

apply simp
done
(*>*)

lemma exception_ext_object:
"wf (P,An) \<Longrightarrow> (Exception,Object) \<in> subcls1 P"
apply (rule subcls1I)
apply (simp add: wf_def)
apply (erule conjE | erule exE)+
apply (simp add: SystemClasses_def Exception_def Object_def class_def ObjectC_def ExceptionC_def)

apply (simp add: Exception_def Object_def)
done

lemma exception_ext_object_only:
"wf (P,An) \<Longrightarrow> (Exception,c) \<in> subcls1 P \<Longrightarrow> c = Object"
apply (erule subcls1.elims)
apply (simp add: wf_def)
apply (erule conjE | erule exE)+
apply (simp add: SystemClasses_def Exception_def Object_def class_def ObjectC_def ExceptionC_def)
done

lemma no_cyclic_inheritance:
"wf (P,An) \<Longrightarrow> (c,c) \<notin> (subcls1 P)"
sorry

lemma object_sup:
"wf (P,An) \<Longrightarrow> (Object,c) \<notin> (subcls1 P)"
sorry

lemma sys_xcpts_ext_exception:
"\<lbrakk> wf (P,An);  cn \<in> sys_xcpts \<rbrakk> \<Longrightarrow> (cn,Exception) \<in> subcls1 P"
apply  (rule subcls1I)
apply (simp add: wf_def)
apply (erule conjE | erule exE)+
apply (simp add: sys_xcpts_def OutOfMemory_def ClassCast_def NullPointer_def 
       SystemClasses_def NullPointerC_def OutOfMemoryC_def ClassCastC_def
       Exception_def Object_def class_def ObjectC_def ExceptionC_def)
apply (erule disjE | simp)+

apply (simp add: sys_xcpts_def OutOfMemory_def ClassCast_def NullPointer_def 
       SystemClasses_def NullPointerC_def OutOfMemoryC_def ClassCastC_def
       Exception_def Object_def class_def ObjectC_def ExceptionC_def)
apply (erule disjE | simp)+
done


lemma sysxpct_no_object:
"\<And> cn cn'. \<lbrakk> wf (P,An); P \<turnstile> cn' \<preceq>\<^sup>* cn; cn \<notin> {Exception,Object}; cn' \<in> sys_xcpts \<rbrakk> \<Longrightarrow> cn = cn'"
(*<*)
apply (erule_tac P="cn  \<notin> {Exception,Object}" in rev_mp)
apply (erule_tac P="cn' \<in> sys_xcpts" in rev_mp)
apply (erule rtrancl.induct)
apply simp

apply (rule impI)+
apply (case_tac "b = Object")
apply (drule_tac c="c" in object_sup)
apply simp

apply (case_tac "b = Exception")
apply (drule_tac c="c" in exception_ext_object_only)
apply simp
apply simp

apply simp

apply (subgoal_tac "P \<turnstile> a \<prec>\<^sup>1 Exception")
 prefer 2
 apply (rule sys_xcpts_ext_exception)
 apply simp
 apply simp
apply (erule subcls1.elims)+
apply simp
done
(*>*)



lemma findhandler_handlesEx:
"\<lbrakk> wf (P,An);  find_handler P xa h frs = (None, h, ([Addr xa], loc', p') # frs'); 
   handlesEx P p' = Some cn \<rbrakk> \<Longrightarrow> P \<turnstile> cname_of h xa \<preceq>\<^sup>* cn"
(*<*)
apply (simp only: handlesEx_def)
apply (case_tac "handlesEx' P p' = []")
apply simp

apply (frule findhandler_handlesEx')
apply simp
apply assumption

apply (erule exE | erule conjE)+
apply (frule_tac p="p'" in wf_handlesEx'_length)
apply (case_tac "cns")
prefer 2
apply simp
apply (case_tac "cns'")
prefer 2
apply simp
apply simp
(* apply (frule_tac p="p'" and cn="cn" in  wf_handlesEx'_noObject)
apply simp
apply simp *)
done
(*>*)


lemma match_ex_table_subtype_None:
"\<lbrakk> match_ex_table P cn pc et = None;  P \<turnstile>  cn \<preceq>\<^sup>* cn' \<rbrakk> 
 \<Longrightarrow> match_ex_table P cn' pc et = None"
(*<*)
apply (induct et)
apply simp
apply atomize
apply (simp split del: option.split_asm)
apply (case_tac "matches_ex_entry P cn pc a")
apply simp

apply simp
apply (rule classical)
apply (simp add: split_paired_all matches_ex_entry_def)
apply (erule conjE)+
apply (subgoal_tac " P \<turnstile> cn \<preceq>\<^sup>* ab")
 prefer 2
 apply (rule_tac b="cn'" in rtrancl_trans)
 apply assumption+
apply simp
done
(*>*)


lemma handlesEx_match_ex_table:
"\<And> d. \<lbrakk> wf (P,An); (C,M) \<in> set (methodnames P); handlesEx P (C,M,pc') = Some cn; 
   match_ex_table P cn' pc (ex_table_of P C M) = Some pc' \<rbrakk> 
\<Longrightarrow> match_ex_table P cn pc (ex_table_of P C M) = Some pc'"
(*<*)
apply (subgoal_tac "handlesEx' P (C,M,pc') = [cn]")
 prefer 2
 apply (drule_tac p="(C,M,pc')" in wf_handlesEx'_length)
 apply (case_tac "handlesEx' P (C,M,pc')")
 apply (simp add: handlesEx_def)
 apply (case_tac "list")
 apply (simp add: handlesEx_def)
 apply simp
apply (erule_tac V="handlesEx P ?p = Some cn" in thin_rl)
apply (simp only: handlesEx'_ex_table_of)
apply (subgoal_tac "set (concat (map (\<lambda>(b, e, cn, h,d). if pc' = h then [cn] else []) (ex_table_of P C M))) = set [cn]")
  prefer 2
  apply (drule_tac t="[cn]" in sym)
  apply (simp add: set_remdups')
apply (erule_tac V="remdups' ?a = ?b" in thin_rl)

apply (subgoal_tac "\<forall> (b,e,cn',h,d) \<in> set (ex_table_of P C M). pc' = h \<longrightarrow> cn' = cn")
 prefer 2
 apply (rule ballI)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE)+
 apply (simp add: split_def)
 apply (rule impI)
 apply simp
apply (erule_tac V="set ?a = set [cn]" in thin_rl)


apply (induct "ex_table_of P C M")
apply simp

apply atomize
apply (drule mp, assumption)+
apply (case_tac "cn = cn'")
apply simp

apply (case_tac "matches_ex_entry P cn pc a")
apply (simp split del: option.split_asm)
apply (case_tac " pc' = fst (snd (snd (snd a)))")
apply simp

apply (case_tac " matches_ex_entry P cn' pc a")
apply simp

apply (simp add: split_def)
apply (subgoal_tac "match_ex_table P cn' pc list = \<lfloor>fst aa\<rfloor>")
 prefer 2
 apply simp
apply (drule_tac cn="cn'" in match_ex_table_split)
apply (erule exE | erule conjE)+
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: matches_ex_entry_def split_def)
apply (subgoal_tac " P \<turnstile> cn' \<preceq>\<^sup>* (fst (snd (snd a)))")
 prefer 2
 apply (rule_tac b="cn" in rtrancl_trans)
 apply assumption+
 apply simp
apply simp

apply (simp split del: option.split_asm)
apply (case_tac "matches_ex_entry P cn' pc a")
apply (simp add: split_def matches_ex_entry_def)

apply simp
apply (rule allI)
apply fastsimp
done
(*>*)


lemma find_handler_catchstate:
"\<And> st' loc p e. \<lbrakk> wf (P,An); find_handler P xa h ((st',loc,p)#frs) = 
 (None,h,([Addr xa],loc',C',M',pc')#frs'); handlesEx P (C',M',pc') = Some cn \<rbrakk> 
\<Longrightarrow> (\<exists>h' stk' pc''. catchstate (P,cn,(p,(None,h,(stk,loc,p)#frs),e)) = 
((C',M',pc''),(None,h',(stk',loc',C',M',pc'')#frs'),e\<lparr>cs:=drop (length frs - length frs') (cs e)\<rparr>)
\<and> (match_ex_table P (cname_of h xa) pc'' (ex_table_of P C' M')) = Some pc') \<or> frs = frs'"
(*<*)
apply (induct frs)
apply (simp add: split_def)

apply atomize
apply (erule_tac P="find_handler P xa h ?a = ?b" in rev_mp)
apply (simp (no_asm))
apply (simp (no_asm) add: split_def del: find_handler.simps)
apply (rule impI)+
apply (erule_tac x="fst a" in allE)
apply (erule_tac x="fst (snd a)" in allE)
apply (erule_tac x="snd (snd a)" in allE)
apply (simp only: all_simps)
apply (subgoal_tac "(fst a,fst (snd a),snd (snd a)) = a")
 prefer 2
 apply simp
apply (simp only: simp_thms)
apply (case_tac "frs = frs'")
apply (simp add: split_def)
apply (drule find_handler_frs)
apply simp
apply (rule_tac x="hd (cs e)" in exI)
apply (rule_tac x="fst a" in exI)
apply (rule_tac x="snd (snd (snd (snd a)))" in exI)
apply (rule conjI)
apply (subgoal_tac "\<exists> st_a rg_a p_a. a = (st_a,rg_a,p_a)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add: split_def)

apply (subgoal_tac "\<exists> st_a rg_a p_a. a = (st_a,rg_a,p_a)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="C'" in sym)
apply (drule_tac t="M'" in sym)
apply (subgoal_tac "match_ex_table P cn (snd (snd p_a)) (ex_table_of P C' M') = \<lfloor>pc'\<rfloor>")
 prefer 2 
 apply (rule_tac cn'="cname_of h xa" and cn="cn" and An="An" in handlesEx_match_ex_table)
 apply assumption
 apply (rule_tac pc="pc'" and P="P" and An="An" in domC_methodnames)
 apply (rule classical)
 apply (subgoal_tac "handlesEx' P (C',M',pc') = []")
  prefer 2
  apply (rule_tac An="An" in handlesEx'_domC)
  apply (simp add: JBC_VCG.wf_def)
  apply assumption
 apply (simp add: handlesEx_def)

 apply simp
 apply (drule_tac s="fst aa" in sym)
 apply simp

apply (simp add: tl_drop)
apply (rule allI, rule impI)
apply (erule exE)
apply simp

apply (rule disjI1)
apply (simp del: find_handler.simps)
apply (erule_tac x="e\<lparr>cs:= tl (cs e)\<rparr>" in allE)
apply (erule exE | erule conjE)+
apply (rule_tac x="h'" in exI)
apply (rule_tac x="stk'" in exI)
apply (rule_tac x="pc''" in exI)
apply (subgoal_tac "\<exists> st_a rg_a p_a. a = (st_a,rg_a,p_a)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (rule conjI)
apply (simp add: split_def env_upd_cs tl_drop drop_drop)

apply (case_tac "frs")
apply simp

apply (rule allI)
apply (erule_tac x="ac" in allE)
apply (cut_tac catchstate_eq)
apply (erule_tac x="P" in allE)
apply (erule_tac x="cn" in allE)
apply (erule_tac x="p_a" in allE)
apply (erule_tac x="None" in allE)
apply (erule_tac x="hd (cs e)" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="(st_a,rg_a,p_a)" in allE)
apply (erule_tac x="(stk,rg_a,p_a)" in allE)
apply (erule_tac x="ab" in allE)
apply (erule_tac x="list" in allE)
apply (erule_tac x="e\<lparr>cs:= drop (Suc 0) (cs e)\<rparr>" in allE)
apply (simp only:)
apply (subgoal_tac "(Suc (length (ab # list)) - length frs') = (Suc (length (ab # list) - length frs'))")
 prefer 2
 apply (subgoal_tac "length frs' \<le> length (ab # list)")
  prefer 2
  apply (drule find_handler_frs)
  apply (erule exE)+
  apply simp
  apply (case_tac "pfx")
  apply simp
  apply simp
  apply (case_tac "lista")
  apply simp
  apply simp
 apply arith
apply (simp only:)

apply (erule disjE)
apply simp
apply (rule impI)
apply simp
apply (erule_tac x="b" in allE)
apply simp

apply (rule impI)
apply (simp del: find_handler.simps add: split_def)
apply (subgoal_tac "match_ex_table P cn (snd (snd p_a)) (ex_table_of P (fst p_a) (fst (snd p_a))) = None")
 prefer 2
 apply (drule_tac P="P" and xa="xa" and h="h" and frs = "ab # list" and loc'="loc'" and p'="(C',M',pc')" and frs'="frs'" in findhandler_handlesEx)
 apply (simp add: split_def)
 apply (rule allI)+
 apply (rule impI)
 apply simp

 apply simp

 apply (erule conjE | erule exE)+
 apply (rule_tac cn="cname_of h xa" in match_ex_table_subtype_None)
 apply (simp add: split_def)
 apply simp
apply (simp add: tl_drop)
done
(*>*)


lemma find_handler_catchstate':
"\<And> st' loc p e. \<lbrakk> find_handler P xa h ((st',loc,p)#frs)=(None,h,([Addr xa],loc',C',M',pc')#frs')
 \<rbrakk> \<Longrightarrow> (\<exists>h' stk' pc''. catchstate (P,(fst (the (h xa))),(p,(None,h,(stk,loc,p)#frs),e)) = 
((C',M',pc''),(None,h',(stk',loc',C',M',pc'')#frs'),e\<lparr>cs:=drop (length frs - length frs') (cs e)\<rparr>)
 \<and> (match_ex_table P (fst (the (h xa))) pc'' (ex_table_of P C' M')) = Some pc') \<or> frs = frs'"
(*<*)
apply (induct frs)
apply (simp add: split_def)

apply atomize
apply (erule_tac P="find_handler P xa h ?a = ?b" in rev_mp)
apply (simp (no_asm))
apply (simp (no_asm) add: split_def del: find_handler.simps)
apply (rule impI)+
apply (erule_tac x="fst a" in allE)
apply (erule_tac x="fst (snd a)" in allE)
apply (erule_tac x="snd (snd a)" in allE)
apply (simp only: all_simps)
apply (subgoal_tac "(fst a,fst (snd a),snd (snd a)) = a")
 prefer 2
 apply simp
apply (simp only: simp_thms)
apply (case_tac "frs = frs'")
apply (simp add: split_def)
apply (drule find_handler_frs)
apply simp

apply (rule_tac x="hd (cs e)" in exI)
apply (rule_tac x="fst a" in exI)
apply (rule_tac x="snd (snd (snd (snd a)))" in exI)
apply (rule conjI)

apply (subgoal_tac "\<exists> st_a rg_a p_a. a = (st_a,rg_a,p_a)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="C'" in sym)
apply (drule_tac t="M'" in sym)
apply (rule allI, rule impI)
apply (erule exE)
apply (subgoal_tac "\<exists> sta rga pa. a = (sta,rga,pa)")
 prefer 2 
 apply fastsimp
apply (erule exE)+
apply (simp add: tl_drop split_def)

apply (rule disjI1)
apply (simp del: find_handler.simps)
apply (erule_tac x="e\<lparr>cs:= tl (cs e)\<rparr>" in allE)
apply (erule exE | erule conjE)+
apply (rule_tac x="h'" in exI)
apply (rule_tac x="stk'" in exI)
apply (rule_tac x="pc''" in exI)
apply (subgoal_tac "\<exists> st_a rg_a p_a. a = (st_a,rg_a,p_a)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (rule conjI)
apply (simp add: split_def env_upd_cs tl_drop drop_drop)

apply (case_tac "frs")
apply simp

apply (rule allI)
apply (erule_tac x="ac" in allE)
apply (cut_tac catchstate_eq)
apply (erule_tac x="P" in allE)
apply (erule_tac x="fst (the (h xa))" in allE)
apply (erule_tac x="p_a" in allE)
apply (erule_tac x="None" in allE)
apply (erule_tac x="hd (cs e)" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="(st_a,rg_a,p_a)" in allE)
apply (erule_tac x="(stk,rg_a,p_a)" in allE)
apply (erule_tac x="ab" in allE)
apply (erule_tac x="list" in allE)
apply (erule_tac x="e\<lparr>cs:= drop (Suc 0) (cs e)\<rparr>" in allE)
apply (simp only:)
apply (subgoal_tac "(Suc (length (ab # list)) - length frs') = (Suc (length (ab # list) - length frs'))")
 prefer 2
 apply (subgoal_tac "length frs' \<le> length (ab # list)")
  prefer 2
  apply (drule find_handler_frs)
  apply (erule exE)+
  apply simp
  apply (case_tac "pfx")
  apply simp
  apply simp
  apply (case_tac "lista")
  apply simp
  apply simp
 apply arith
apply (simp only:)

apply (erule disjE)
apply simp
apply (rule impI)
apply simp
apply (erule_tac x="b" in allE)
apply simp

apply (rule impI)
apply (simp del: find_handler.simps add: split_def)

apply (simp add: tl_drop)
apply (subgoal_tac "\<exists> st_ab rg_ab p_ab. ab = (st_ab,rg_ab,p_ab)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add: split_def)
done
(*>*)

lemma callers_sysinv_Reachables:
"\<lbrakk> wf \<Pi>; s \<in> Reachables \<Pi> \<rbrakk> \<Longrightarrow> callers_sysinv (\<Pi>,s)"
(*<*)
apply (erule Reachables.induct)
apply (simp add: split_paired_all initS_def split_def  callers_sysinv.simps start_state_def wf_def mem_iff ipc_def)

--{* induction case *}
apply (subgoal_tac "check (fst \<Pi>) (fst (snd s'))")
 prefer 2
 apply (rule wf_Reachables_check)
 apply assumption
 apply (rule_tac s="s" in Reachables.step)
 apply assumption
 apply assumption
apply (erule effS.elims)
--{* Exception case *}
apply (subgoal_tac "\<exists> An. \<Pi> = (P,An)")
 prefer 2
 apply (rule_tac x="snd \<Pi>" in exI)
 apply simp
apply (erule exE | erule conjE)+
apply (erule_tac V="P = fst \<Pi>" in thin_rl)
apply (simp only: )
apply (subgoal_tac "\<exists>C' M' pc'. p' = (C',M',pc')")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (erule exE)+
apply (simp only:)
apply (frule_tac stk="stk" and e="e" in  find_handler_catchstate')
apply (case_tac "frs = frs'")
apply (simp split del: option.splits option.split_asm)
apply (case_tac "match_ex_table P (cname_of h xa) pc (ex_table_of P C M)")
apply simp
apply (drule find_handler_frs)
apply simp
apply (subgoal_tac "(C',M',pc') \<in> set (domC (P,An))")
 prefer 2
 apply (rule_tac pc="pc" and X="(cname_of h xa)" in wf_ex_table_domC)
 apply assumption
 apply (simp add: has_method_def mem_iff)
 apply simp
 apply (drule_tac s="fst aa" and t="pc'" in sym)
 apply fastsimp
apply (case_tac "frs'")
apply (simp add: ipc_def mem_iff)
--{* frs' = aa list *}
apply (simp add: Let_def split_def env_upd_cs mem_iff)
apply (subgoal_tac "(callers \<Pi> (C', M', pc'))  = (callers \<Pi> (C', M', pc))")
 prefer 2
 apply (rule callers_eq)
apply (simp add: mem_iff)

--{* frs ~= frs' *}
apply (erule disjE)
apply (erule exE)+
apply (subgoal_tac "catchstate (P,fst (the (h xa)),s) \<in> callstates s")
 prefer 2
 apply (rule catchstate_callstates)
apply (drule_tac s'="catchstate (P,fst (the (h xa)),s)" in callstates_callers_sysinv)
apply assumption

apply (simp add: Let_def split_def env_upd_cs mem_iff)
apply (subgoal_tac "(C',M',pc') \<in> set (domC (P,An))")
 prefer 2
 apply (rule_tac pc="pc''" and X="(cname_of h xa)" in wf_ex_table_domC)
 apply assumption
 apply (rule_tac pc="pc''" and An="An" in domC_methodnames)
 apply (case_tac "frs'")
 apply (simp add: ipc_def mem_iff)
 apply (erule conjE)+
 apply (simp only:)

 apply (simp add: mem_iff)
 
 apply (drule_tac s="fst a" and t="pc'" in sym)
 apply simp

apply (case_tac "frs'")
apply (simp add: Let_def split_def env_upd_cs mem_iff ipc_def)

--{* frs' = aa list *}
apply (simp add: Let_def split_def env_upd_cs mem_iff)
apply (erule conjE)+
apply (subgoal_tac "(callers \<Pi> (C', M', pc''))  = (callers \<Pi> (C', M', pc'))")
 prefer 2
 apply (rule callers_eq)
apply (simp only:)

apply simp

--{* Normal Excecution *}
apply (subgoal_tac "\<exists> An. \<Pi> = (P,An)")
 prefer 2
 apply (rule_tac x="snd \<Pi>" in exI)
 apply simp
apply (erule exE)+
apply (erule_tac V="P = fst \<Pi>" in thin_rl)
apply (drule_tac s="i" in sym)
apply (drule_tac s="exec_instr i P h stk loc C M pc frs" in sym)
apply (subgoal_tac "\<exists>ps ps' S Fs Ms Ms' Ts T bd. P = ps @ (C, S, Fs, Ms @ (M, Ts, T, bd) # Ms') # ps' \<and> get_mdecl P C M = (M, Ts, T, bd)")
 prefer 2
 apply (simp only: has_method_def mem_iff)
 apply (drule methodnames_P)
 apply (erule exE | erule conjE)+
 apply (rule_tac x="ps" in exI)
 apply (rule_tac x="ps'" in exI)
 apply (rule_tac x="S" in exI)
 apply (rule_tac x="Fs" in exI) 
 apply (rule_tac x="Ms" in exI)
 apply (rule_tac x="Ms'" in exI)
 apply (rule_tac x="Ts" in exI)
 apply (rule_tac x="T" in exI)
 apply (rule_tac x="bd" in exI)
 apply simp
apply (erule exE | erule conjE)+
apply (subgoal_tac "method P C M = method' P C M")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in method_method')
 apply (drule wf_wfprog)
 apply simp

 apply (simp only: has_method_def mem_iff)
apply (subgoal_tac "\<exists> mxs mxl ins et. bd = (mxs,mxl,ins,et)")
 prefer 2
 apply (rule_tac x="fst bd" in exI)
 apply (rule_tac x="fst (snd bd)" in exI)
 apply (rule_tac x="fst (snd (snd bd))" in exI)
 apply (rule_tac x="snd (snd (snd bd))" in exI)
 apply simp
apply (erule exE)+

apply (case_tac "i")
--{* Load nat *}
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* Store nat *}
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* Push val *}
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* New list *}
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)


--{* Getfield list1 list2 *}
apply simp
apply(case_tac "hd stk = Null")
apply (simp add: split_def)

apply (simp add:  check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)

apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)


--{* Putfield list1 list2 *}

apply simp
apply(case_tac "hd (tl stk) = Null")
apply (simp add: split_def)

apply (simp add:  check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)

apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* Checkcast list *}
apply simp
apply(case_tac "\<not> cast_ok P list h (hd stk)")
apply (simp add: split_def)

apply (simp add:  check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)

apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* Invoke list nat *}
apply simp

apply (case_tac "stk ! nat = Null")
apply (simp add: split_def)



apply (drule_tac s="P" in sym)
apply (simp only:)
apply (subgoal_tac "p \<in> set (domC (P,An))")
  prefer 2
  apply (case_tac "frs")
  apply (simp add: ipc_def mem_iff)
  apply (erule conjE)+
  apply simp

  apply (simp add: mem_iff)
apply (simp only:)
apply (frule domC_methodnames)
apply (drule methodnames_P)
apply (erule exE | erule conjE)+
apply (subgoal_tac "cmd \<Pi> p = Some (Invoke list nat)")
  prefer 2
  apply (drule_tac C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
  apply simp
  apply simp

apply (subgoal_tac "check P (None, h, (stk, loc, C, M, pc) # frs)")
 prefer 2
 apply (drule_tac s="s" in wf_Reachables_check)
 apply simp
 apply simp

apply (simp add: check_def method'_def split_def)
apply (erule conjE)+
apply (frule_tac C="(cname_of h (the_Addr (stk ! nat)))" and M="list" in has_method_has_method)
apply (erule exE | erule conjE)+
apply simp
apply (subgoal_tac "(D,list,0) \<in> set (domC \<Pi>)")
 prefer 2
 apply (drule_tac s="P" in sym)
 apply (simp only: has_method_def mem_iff)
 apply (subgoal_tac "method P D list = method' P D list")
  prefer 2
  apply (rule_tac wf_md="wf_md_Ty" in  method_method')
  apply (drule wf_wfprog)
  apply simp
  apply assumption
 apply (drule_tac C="D" and M="list" in methodnames_P)
 apply (erule exE | erule conjE)+
 apply (simp add: domC_def domCC_split method'_def)
 apply (subgoal_tac "\<exists> mxs_b mxl_b bd_b et_b. bdb = (mxs_b,mxl_b,bd_b,et_b)")
  prefer 2
  apply (erule thin_rl)+
  apply (rule_tac x="fst bdb" in exI)
  apply (rule_tac x="fst (snd (bdb))" in exI)
  apply (rule_tac x="fst (snd (snd bdb))" in exI)
  apply (rule_tac x="snd (snd (snd bdb))" in exI)
  apply simp
 apply (erule exE)+
 apply simp

apply (rule conjI)
apply (simp add: mem_iff)

apply (rule conjI)
apply (simp add: callers_def)

apply (case_tac "frs")
apply (simp add: split_def)

apply (simp add: split_def del: callers_sysinv.simps)

--{* Return *}
apply (simp add:  check_def method'_def split_def)
apply (case_tac "frs")
apply simp

apply (simp add: split_def env_upd_cs del: callers_sysinv.simps)
apply (case_tac "list")
apply (simp add: split_def ipc_def mem_iff)
apply (subgoal_tac "(Start,main) \<in> (set (methodnames P))")
 prefer 2
 apply (rule_tac pc="0" and An="An" in domC_methodnames)
 apply (simp add: wf_def ipc_def)
apply (subgoal_tac "method P Start main = method' P Start main")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in method_method')
 apply (drule_tac wf_wfprog)
 apply simp
 apply assumption
apply (drule_tac s="P" in sym)
apply (simp only:)
apply (drule_tac C="Start" and M="main" in methodnames_P)
apply (erule exE | erule conjE)+
apply (simp add: method'_def domC_def domCC_split)
 apply (subgoal_tac "\<exists> mxs_a mxl_a bd_a et_a. bda = (mxs_a,mxl_a,bd_a,et_a)")
  prefer 2
  apply (erule thin_rl)+
  apply (rule_tac x="fst bda" in exI)
  apply (rule_tac x="fst (snd (bda))" in exI)
  apply (rule_tac x="fst (snd (snd bda))" in exI)
  apply (rule_tac x="snd (snd (snd bda))" in exI)
  apply simp
apply (erule exE)+
apply simp

--{* list = aa lista *}
apply (simp add: split_def ipc_def mem_iff)
apply (subgoal_tac "(callers (P, An) (fst (snd (snd a)), fst (snd (snd (snd a))), Suc (snd (snd (snd (snd a)))))) = 
                    (callers (P, An) (fst (snd (snd a)), fst (snd (snd (snd a))), (snd (snd (snd (snd a))))))")
 prefer 2
 apply (rule callers_eq)
apply simp
apply (erule conjE)+
apply (drule_tac s="P" in sym)
apply (simp only:)
apply (subgoal_tac "(fst (snd (snd a)),fst (snd (snd (snd a)))) \<in> set (methodnames P)")
 prefer 2
 apply (rule_tac pc="snd (snd (snd (snd a)))" and An="An" in domC_methodnames)
 apply simp
apply (subgoal_tac "method P (fst (snd (snd a))) (fst (snd (snd (snd a)))) = method' P (fst (snd (snd a))) (fst (snd (snd (snd a))))")
 prefer 2
 apply (rule_tac wf_md="wf_md_Ty" in method_method')
 apply (drule wf_wfprog)
 apply simp
 apply assumption
apply (drule_tac C="(fst (snd (snd a)))" and M="(fst (snd (snd (snd a))))" in methodnames_P)
apply (erule conjE | erule exE)+
apply (simp add: method'_def domC_def domCC_split)
apply (subgoal_tac "\<exists> mxs_a mxl_a bd_a et_a. bda = (mxs_a,mxl_a,bd_a,et_a)")
  prefer 2
  apply (erule thin_rl)+
  apply (rule_tac x="fst bda" in exI)
  apply (rule_tac x="fst (snd (bda))" in exI)
  apply (rule_tac x="fst (snd (snd bda))" in exI)
  apply (rule_tac x="snd (snd (snd bda))" in exI)
  apply simp
apply (erule exE)+
apply simp

--{* Pop *}
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* IBin *}
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* Goto int *}
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,nat (int pc + inta)) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* CmpEq *}
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* IfIntCmp *}
apply simp
apply (case_tac "relop rel_op (the_Intg (hd (tl stk))) (the_Intg (hd stk))")
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,nat (int pc + inta)) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* IfFalse *}
apply simp
apply (case_tac "hd stk = Bool False")
apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,nat (int pc + inta)) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

apply (simp add: check_def method'_def split_def)
apply (case_tac "frs")
apply (simp add: ipc_def mem_iff domC_def domCC_split)
--{* frs = a list *}
apply (subgoal_tac "callers (P, An) (C,M,Suc pc) = callers (P, An) (C,M,pc)")
 prefer 2
 apply (rule callers_eq)
apply (simp add: split_def env_upd_cs mem_iff domC_def domCC_split del: callers_sysinv.simps)

--{* Throw *}
apply simp
done
(*>*)



lemma safeP_callers_sysinv:
"\<lbrakk> wf \<Pi>; s \<in> safeP \<Pi> \<rbrakk> \<Longrightarrow> callers_sysinv (\<Pi>,s)"
(*<*)
apply (drule safeP_Reachables)
apply (rule callers_sysinv_Reachables)
apply assumption+
done
(*>*)


lemma find_handler_frs':
"find_handler P x h frs = (None,h,fr#frs') 
 \<Longrightarrow> \<exists>pfx. frs = pfx @ frs' \<and> pfx \<noteq> [] \<and> (let (C0,M0,pc0) = snd (snd fr);
                                               (C0',M0',pc0') = (snd (snd (last pfx)))
                                           in (C0 = C0' \<and> M0 = M0'))"
(*<*)
apply (induct frs)
apply simp
apply (simp add: split_def)
apply fastsimp
apply fastsimp
done
(*>*)


lemma Reachables_state:
assumes s_Reach: "s \<in> Reachables \<Pi>"
shows "\<exists> C M pc h st rg frs e. s = ((C,M,pc),(None,h,(st,rg,(C,M,pc))#frs),e) 
       \<and> (let (C0,M0,pc0) = last (map (snd \<circ> snd) ((st,rg,(C,M,pc))#frs));
               (C0',M0',pc0') = ipc \<Pi> 
           in (C0 = C0' \<and> M0 = M0'))"  using s_Reach
(*<*)
proof (induct rule: Reachables.induct)
  case (init s)
  from this have s_initS:"s \<in> initS \<Pi>" 
  by assumption

  from s_initS show ?case
   apply (simp add: split_paired_all initS_def start_state_def ipc_def)
   apply (simp add: split_def)
   apply (rule_tac x="Start" in exI)
   apply (rule_tac x="main" in exI)
   apply (rule_tac x="0" in exI)
   apply (rule_tac x="start_heap (fst \<Pi>)" in exI)
   apply (rule_tac x="[]" in exI)
   apply (rule_tac x="Null # replicate (fst (snd (snd (snd (snd (method (fst \<Pi>) Start main)))))) arbitrary" in exI)
   apply (rule_tac x="[]" in exI)
   apply simp
   apply fastsimp
   done

next
  case (step s s')
  assume s_Reach: "s \<in> Reachables \<Pi>"
  assume s_Reach_state: "\<exists>C M pc h st rg frs e.
     s = ((C, M, pc), (None, h, (st, rg, C, M, pc) # frs), e) \<and>
     (let (C0,M0,pc0) = last (map (snd \<circ> snd) ((st,rg,(C,M,pc))#frs));
               (C0',M0',pc0') = ipc \<Pi> 
           in (C0 = C0' \<and> M0 = M0'))"
  assume s_s'_effS: "(s, s') \<in> effS \<Pi>"
  have s'_Reach:"s' \<in> Reachables \<Pi>"
    by (rule Reachables.step)
  show ?case
  proof (rule effS.elims[OF s_s'_effS])
  fix p \<sigma> e p' \<sigma>' e' P C M pc i h stk loc frs
  assume s_s'_def:    "(s, s') = ((p, \<sigma>, e), p', \<sigma>', e')"
  assume P_def:       "P = fst \<Pi>"
  assume p_def:       "p = (C, M, pc)"
  assume i_def:       "i = instrs_of P C M ! pc"
  assume sigma_def:   "\<sigma> = (None, h, (stk, loc, p) # frs)"
  assume has_method_C_M: "JBC_Semantics.has_method P C M"
  { --{* EXCEPTIONAL EXECUTION *}
    fix xa h' frs'' loc' frs' 
    assume exec_i: "exec_instr i P h stk loc C M pc frs = (\<lfloor>xa\<rfloor>, h', frs'')"
    assume find_handler_s: "find_handler P xa h ((stk, loc, p) # frs) = \<sigma>'"
    assume sigma'_def: "\<sigma>' = (None, h, ([Addr xa], loc', p') # frs')"
    assume e'_def: "e' = e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>"
    show ?case
      proof -
      from P_def obtain An where Pi_def : "\<Pi> = (P,An)"
	by (case_tac "\<Pi>", simp)
      obtain C' M' pc' where p'_def: "p' = (C',M',pc')"
	apply atomize
	apply (erule_tac x="fst p'" in allE)
	apply (erule_tac x="fst (snd p')" in allE)
	apply (erule_tac x="snd (snd p')" in allE)
	apply simp
	done
      from i_def[THEN sym] s_s'_def p_def sigma_def exec_i find_handler_s sigma'_def e'_def p'_def s_Reach_state
      show ?case
	apply -
	apply (simp del: find_handler.simps split del: option.split_asm)
	apply (frule find_handler_frs')
	apply (erule exE)
	apply (case_tac "pfx")
	apply simp

	apply (case_tac "frs" rule: rev_cases)
	apply (simp add: split_def)
	apply (drule_tac t="a" in sym)
	apply simp

	apply (case_tac "frs'" rule: rev_cases)
	apply simp
	apply (simp add: split_def)
	apply (frule find_handler_frs')
	apply (erule exE)
	apply simp
	apply (drule_tac s="ys @ [y]" in sym)
	apply (erule conjE)+
	apply (simp add: split_def)
	apply (simp add: Let_def)
	done
      qed

  next 
    --{* Normal Execution *}
    fix h' fr' frs'
    assume exec_i: "exec_instr i P h stk loc C M pc frs = (None, h', fr' # frs')"
    assume sigma'_def: "\<sigma>' = (None, h', fr' # frs')"
    assume p'_def: "p' = snd (snd fr')"
    assume e'_def: "e' = e\<lparr>cs := if \<exists>M n. i = Invoke M n then h # cs e else if i = Return then tl (cs e) else cs e\<rparr>"
    from P_def obtain An where Pi_def : "\<Pi> = (P,An)"
      by (case_tac "\<Pi>", simp)
    note exec_simp = i_def[THEN sym] s_s'_def p_def sigma_def exec_i sigma'_def p'_def e'_def s_Reach_state 
    show ?thesis
      proof (cases i)
	case (Load "nat")
	from Load exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done
      next
	case (Store "nat")
	from Store exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
	
      next
	case (Push "val")
	from Push exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
      next
	case (New "list")
	from New exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
      next
	case (Getfield "list1" "list2")
	from Getfield exec_simp show ?thesis
	  apply (simp add: split_def)
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
    
      next
	case (Putfield "list1" "list2")
	from Putfield exec_simp show ?thesis
	  apply (simp add: split_def)
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done
	
      next
	case (Checkcast "list")
	from Checkcast exec_simp show ?thesis
	  apply (simp add: split_def)
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done
      
      next
	case (Invoke "list" "nat")
	from Invoke exec_simp show ?thesis
	  apply (simp add: split_def)
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (erule exE)+
	  apply (erule conjE)+
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
      next
	case Return
	from Return exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (case_tac "frs::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp
	  
	  apply (simp add: split_def)
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
      next
	case Pop
	from Pop exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	

      next
	case (IBin no)
	from IBin exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
	
      next
	case (Goto "t")
	from Goto exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
      next
	case CmpEq
	from CmpEq exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
      next
	case (IfIntCmp "ro" "t")
	from IfIntCmp exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
	
      next
	case (IfFalse "t")
	from IfFalse exec_simp show ?thesis
	  apply simp
	  apply (erule conjE)+
	  apply (drule_tac t="fr'" in sym)
	  apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
	  apply simp

	  apply simp
	  done	
	
      next
	case Throw
	from Throw exec_simp show ?thesis
	 by (simp add: split_def split add: split_if_asm)
     qed
 
    }
qed
qed
(*>*)


lemma wf_Reachables_domC:
"\<lbrakk> wf \<Pi>; s \<in> Reachables \<Pi> \<rbrakk> \<Longrightarrow> fst s \<in> set (domC \<Pi>)"
(*<*)
apply (frule Reachables_state)
apply (erule exE | erule conjE)+
apply (drule callers_sysinv_Reachables)
apply simp
apply (simp add: split_def)
apply (case_tac "frs")
apply (simp add: mem_iff)

apply (simp add: mem_iff)
done
(*>*)


lemma wf_Reachables_domC':
"\<And> p x h e. \<lbrakk> wf \<Pi>; (p,(x,h,frs),e) \<in> Reachables \<Pi> \<rbrakk> \<Longrightarrow> \<forall> p \<in> set (map (snd \<circ> snd) frs). p \<in> set (domC \<Pi>)"
(*<*)
apply (drule callers_sysinv_Reachables)
apply simp
apply (drule callers_sysinv_domC)
apply simp
done
(*>*)


lemma wf_safeP_domC':
"\<And> p x h e. \<lbrakk> wf \<Pi>; (p,(x,h,frs),e) \<in> safeP \<Pi> \<rbrakk> \<Longrightarrow> \<forall> p \<in> set (map (snd \<circ> snd) frs). p \<in> set (domC \<Pi>)"
(*<*)
apply (drule safeP_Reachables)
apply (rule wf_Reachables_domC')
apply simp
apply simp
done
(*>*)


lemma callers_sysinv_trans:
"\<And> p x h  e. callers_sysinv (\<Pi>,(p,(x,h,frs),e)) = (\<forall> i < length frs. snd (snd (frs ! i)) \<in> set (domC \<Pi>) \<and> 
                                       (if Suc i = length frs 
                                        then fst (snd (snd (frs ! i))) = fst (ipc \<Pi>) 
                                             \<and> fst (snd (snd (snd (frs ! i)))) = fst (snd (ipc \<Pi>))
                                        else snd (snd (frs ! (Suc i))) \<in> set (callers \<Pi> (snd (snd (frs ! i))))))"
(*<*)
apply (induct frs)
apply simp

apply atomize
apply (subst callers_sysinv.simps)
apply (erule_tac x="snd (snd (frs ! 0))" in allE)
apply (erule_tac x="None" in allE)
apply (erule_tac x="hd (cs e)" in allE)
apply (erule_tac x="e\<lparr>cs:= tl (cs e)\<rparr>" in allE)
apply (simp del: callers_sysinv.simps split del: split_if)
apply (case_tac "frs")
apply (simp add: split_def mem_iff del: callers_sysinv.simps)

apply (rule iffI)
apply (simp add: split_def mem_iff forall_expand del: callers_sysinv.simps split del: split_if)
apply (erule conjE)+
apply (rule conjI)
apply (case_tac "list")
apply simp

apply (simp add: split_def mem_iff del: callers_sysinv.simps split del: split_if)

apply (rule allI)
apply (erule_tac x="i" in allE)
apply (rule impI)
apply (drule mp, assumption)
apply (erule conjE)
apply (case_tac "Suc i = length list")
apply (simp add: split_def mem_iff forall_expand del: callers_sysinv.simps)

apply (simp add: split_def mem_iff forall_expand del: callers_sysinv.simps)

apply (simp add: split_def mem_iff forall_expand del: callers_sysinv.simps split del: split_if)
apply (case_tac "list = []")
apply simp

apply (simp add: split_def mem_iff del: callers_sysinv.simps split del: split_if)
apply (erule conjE)+
apply (rule allI)
apply (erule_tac x="i" in allE)
apply (rule impI)
apply (drule mp, assumption)
apply (erule conjE)
apply (case_tac "Suc i = length list")
apply (simp add: split_def mem_iff del: callers_sysinv.simps)

apply (simp add: split_def mem_iff del: callers_sysinv.simps)
done
(*>*)


lemma no_recursive_main:
"\<lbrakk> wf \<Pi>; s \<in> Reachables \<Pi> \<rbrakk> \<Longrightarrow> 
  fst (snd (ipc \<Pi>)) \<notin> set (butlast (map (fst o snd o snd o snd) (snd (snd (fst (snd s))))))"
(*<*)
apply (erule Reachables.induct)
apply (simp add: initS_def start_state_def split_def)

apply (erule effS.elims)

--{* Exceptional Execution *}
apply (drule Reachables_state)
apply (erule exE | erule conjE)+
apply (simp only:)
apply (drule find_handler_frs')
apply (erule exE | erule conjE)+
apply simp
apply (rule impI)
apply (rule_tac xs="pfx" in rev_cases)
apply simp

apply (simp add: split_def)
apply (case_tac "ys")
apply simp
apply (erule conjE)+
apply (drule_tac t="y" in sym)
apply simp

--{* ys ~= [] *}
apply (simp add: butlast_append)

--{* Normal execution *}
apply (subgoal_tac "p \<in> set (domC \<Pi>)")
 prefer 2
 apply (drule wf_Reachables_domC)
 apply simp
 apply simp
apply (frule_tac C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
apply simp

apply (subgoal_tac "\<exists> An. \<Pi> = (P,An)")
 prefer 2
 apply (rule_tac x="snd \<Pi>" in exI)
 apply simp
apply (erule exE)+
apply (erule_tac V="P = fst \<Pi>" in thin_rl)

apply simp
apply (drule_tac t="instrs_of P C M ! pc" in sym)
apply (simp only:)
apply (case_tac "i")
--{* Load nat *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Store nat *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Push val *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* New list *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Getfield list1 list2 *}
apply (simp add: split_def)
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Putfield list1 list2 *}
apply (simp add: split_def)
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Checkcast *}
apply (simp add: split_def)
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Invoke list nat *}
apply (subgoal_tac "\<exists> dC dC'. domC \<Pi> = dC @ (C,M,pc)#dC'")
 prefer 2
 apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: split_def JBC_VCG.wf_def checkPos_split split_if)
apply (erule conjE)+
apply (case_tac "anF \<Pi> (C,M,pc)")
apply simp

apply simp
apply (drule_tac t="fr'" in sym)
apply simp
apply (rule impI)

apply (case_tac "(C,M,pc) = ipc \<Pi>")
apply simp

apply simp
apply (erule conjE)+
apply (case_tac "extractTy (a, St nat)")
apply simp

apply simp
apply (erule conjE)+
apply (rule conjI)
apply (rule not_sym)
apply assumption

apply (drule_tac t="frs'" in sym)
apply simp

--{* Return *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (case_tac "frs")
apply simp

apply (simp add: split_def )
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Pop *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* IBin *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Goto int *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* CmpEq *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* IfIntCmp *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* IfFalse *}
apply simp
apply (rule impI)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp

--{* Throw *}
apply (simp split add: split_if_asm)
done
(*>*)


section {* Frame Stack Size *}

lemma inv_FrNr_Reachable:
"\<lbrakk> wf \<Pi>; s \<in> Reachables \<Pi> \<rbrakk> \<Longrightarrow> \<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
(*<*)
apply (frule no_recursive_main)
apply assumption

apply (drule Reachables_state)
apply (erule exE)+
apply (simp add: inv_FrNr_def ipc_def split_def)
apply (rule_tac xs="frs" in rev_cases)
apply simp

apply simp
apply (erule conjE)+
apply (rule conjI)
apply (rule impI)
apply (rule not_sym)
apply simp

apply (rule impI)
apply (simp add: relop_def liftR_def)
done
(*>*)


section {* Position information *}


lemma addPos_append:
"addPos p (es@es') = addPos p es @ addPos p es'"
(*<*)
apply (induct es)
apply (simp add: addPos_def)+
done
(*>*)


lemma addPos_cons:
"addPos p ((p',B)#es) = addPos p [(p',B)] @ addPos p es"
(*<*)
apply (subgoal_tac "addPos p ([(p',B)]@es) = addPos p [(p',B)] @ addPos p es")
 prefer 2
 apply (simp only: addPos_append)
apply simp
done
(*>*)


lemma addPos_single:
"addPos p [(p', B)] = [(p', And [Pos p,B])]"
(*<*)
apply (simp add: addPos_def)
done
(*>*)


lemma addPos_map_fst:
"map fst (addPos p xs) = map fst xs"
(*<*)
apply (induct xs)
apply (simp add: addPos_def)
apply (simp add: addPos_def split_paired_all split_def )
done
(*>*)


lemma inv_Pos_Reachable:
"\<lbrakk> wf \<Pi> ; s \<in> Reachables \<Pi> \<rbrakk> \<Longrightarrow> \<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
(*<*)
apply (frule Reachables_state)
apply (frule callers_sysinv_Reachables)
apply assumption
apply (erule exE | erule conjE)+
apply (simp add: Let_def inv_Pos_def)
done
(*>*)


section {* System Exception Types *}


lemma inv_ExTys_Reachable:
"s \<in> Reachables \<Pi> \<Longrightarrow> \<Pi>, s \<Turnstile> inv_ExTys \<Pi> (fst s)"
(*<*)
apply (erule Reachables.induct)
apply (simp add: obj_ty_def blank_def initS_def start_state_def start_heap_def NullPointer_def ClassCast_def 
       OutOfMemory_def split_def split_paired_all inv_ExTys_def addr_of_sys_xcpt_def)
apply (erule effS.elims)
--{* Exceptional Execution *}
apply (simp add: inv_ExTys_def)

--{* Normal Execution *}
apply (simp add: inv_ExTys_def)
apply (drule_tac s="i" in sym)
apply (case_tac "i")
--{* Load nat *}
apply (simp add: obj_ty_def split_paired_all)
--{* Store nat *}
apply (simp add: obj_ty_def split_paired_all)
--{* Push val *}
apply (simp add: obj_ty_def split_paired_all)
--{* New list *}
apply (simp add: obj_ty_def split_paired_all)
apply (subgoal_tac "aw \<noteq> addr_of_sys_xcpt ClassCast")
 prefer 2
 apply (drule_tac a="aw" in new_Addr_SomeD)
 apply (rule classical)
 apply simp
apply (subgoal_tac "aw \<noteq> addr_of_sys_xcpt NullPointer")
 prefer 2
 apply (drule_tac a="aw" in new_Addr_SomeD)
 apply (rule classical)
 apply simp
apply (subgoal_tac "aw \<noteq> addr_of_sys_xcpt OutOfMemory")
 prefer 2
 apply (drule_tac a="aw" in new_Addr_SomeD)
 apply (rule classical)
 apply simp
apply (erule conjE)+
apply (drule_tac t="h'" in sym)+
apply (erule_tac V="h' = ak" in thin_rl)
apply (erule_tac V="h' = ag" in thin_rl)
apply simp

--{* Getfield *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* Putfield *}
apply (simp add: obj_ty_def split_paired_all split_def)
apply (erule conjE)+
apply (drule_tac t="h'" and s="h(the_Addr (hd (tl stk)) \<mapsto>
        (cname_of h (the_Addr (hd (tl stk))), snd (the (h (the_Addr (hd (tl stk)))))((list1, list2) \<mapsto> hd stk)))" in sym)
apply simp
apply (drule_tac s="NullPointer" in sym)
apply (drule_tac s="OutOfMemory" in sym)
apply (drule_tac s="ClassCast" in sym)
apply (rule conjI | rule impI)+
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (rule conjI | rule impI)+
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (rule conjI | rule impI)+
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (rule conjI | rule impI)+
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (rule conjI | rule impI)+
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (rule conjI | rule impI)+
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (rule conjI | rule impI)+
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)
apply (rule conjI | rule impI)+
apply (simp add: NullPointer_def ClassCast_def OutOfMemory_def addr_of_sys_xcpt_def)

--{* Checkcast *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* Invoke *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* Return *}
apply (simp add: obj_ty_def split_paired_all split_def)
apply (case_tac "frs")
apply simp
apply (simp add: split_def)

--{* Pop *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* IBin *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* Goto *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* CmpEq *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* IfIntCmp *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* IfFalse *}
apply (simp add: obj_ty_def split_paired_all split_def)

--{* Throw *}
apply (simp split add: split_if_asm)
done
(*>*)


lemma extractTy_sem:
"\<And> tys. \<lbrakk> \<Pi>,s \<Turnstile> A; extractTy (A,ex) = tys; tys \<noteq> [] \<rbrakk> \<Longrightarrow> \<exists> tp \<in> set tys. \<Pi>,s \<Turnstile> Ty ex tp"
(*<*)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule_tac P="\<lambda> u v. (\<forall> tys. tys \<noteq> [] \<longrightarrow> extractTy (u,v) = tys \<longrightarrow> \<Pi>,s \<Turnstile> u \<longrightarrow> (\<exists> tp\<in> set tys. \<Pi>,s \<Turnstile> Ty v tp))" and u="A" and v="ex" in extractTy.induct)
--{* u = And [] *}
apply (simp, blast)
--{* u = And ex' # exs *}
apply (rule allI, (rule impI)+)
apply simp
apply (drule_tac t="tys" in sym)
apply (simp only:)
apply (case_tac "extractTy (ex',ex) = []")
apply simp
--{* case: extractTy (ex',ex) ~= [] *}
apply (case_tac "extractTy (And exs,ex) = []")
apply simp
--{* case: extractTy (And exs,ex) ~= [] *}
apply simp
apply (erule bexE)+
apply (case_tac "evalE \<Pi> s ex")
apply simp
--{* case: evalE Pi s ex = Some a *}
apply (case_tac "a")
apply simp+
apply (rule_tac x="tp" in bexI)
 prefer 2
 apply simp
apply simp
--{* Ty ex' tp *}
apply (rule allI | rule impI)+
apply (drule_tac t="tys" in sym)
apply (subgoal_tac "ex' = ex")
 prefer 2
 apply (rule classical)
 apply simp
apply simp
--{* Neg (And []) *}
apply simp
--{* Neg (And (Neg ex' # exs)) *}
apply (rule allI, (rule impI)+)
apply simp
apply (case_tac "isNegTy (Neg ex', ex) \<and> list_all (\<lambda>ex''. isNegTy (ex'', ex)) exs")
prefer 2
apply simp

apply simp
apply (case_tac "the_Bool (evalE \<Pi> s ex')")
apply (simp only: the_Bool_simp simp_thms)
apply (subgoal_tac "extractTy (ex',ex) \<noteq> []")
 prefer 2
 apply (case_tac "ex'")
 apply simp+
apply (erule conjE)+
apply (erule bexE)
apply (drule_tac t="tys" in sym)
apply (rule_tac x="tp" in bexI)
apply simp
apply simp

--{* not (theBool evalE Pi s ex') *}
apply simp
apply (subgoal_tac "extractTy (Neg (And exs), ex) \<noteq> []")
 prefer 2
 apply (case_tac "exs")
 apply simp

 apply (case_tac "a")
 apply simp+
 apply (case_tac "expr")
 apply simp+
apply (drule_tac t="tys" in sym)
apply (erule conjE)+
apply (erule bexE)
apply (rule_tac x="tp" in bexI)
apply simp

apply simp
--{* Rg w . . . *}
apply simp+
done
(*>*)


section {* Type Conformance *}


lemma methodnames_prog_kil:
"(C,M) \<in> set (methodnames P) \<Longrightarrow> (\<exists> \<tau>. (prog_kil P) ? (C,M) = Some \<tau>)"
(*<*)
apply (simp add: prog_kil_def lookup_map)
apply (induct "methodnames P")
apply simp

apply (case_tac "(C,M) = a")
apply (simp add: split_def)

apply simp
done
(*>*)


lemma state_format: "\<lbrakk> s0 \<in> initS \<Pi>; (s0,s)\<in> (effS \<Pi>)\<^sup>* \<rbrakk> \<Longrightarrow> \<exists> p h st rg frs e. s = (p,(None,h,(st,rg,p)#frs),e)"
(*<*)
apply (erule rev_mp)
apply (erule rtrancl.induct) 
apply (simp add: initS_def start_state_def ipc_def split_def split_paired_all)

apply (rule impI, drule mp, assumption)
apply (erule exE)+
apply (erule effS.elims)
--{* exceptional execution *}
apply (erule Pair_inject)+
apply (simp only:)
apply (rule_tac x="p'" in exI)
apply (rule_tac x="ha" in exI)
apply (rule_tac x="[Addr xa]" in exI)
apply (rule_tac x="loc'" in exI)
apply (rule_tac x="frs'" in exI)
apply (rule_tac x="ea\<lparr>cs := drop (length frsa - length frs') (cs ea)\<rparr>" in exI)
apply (simp (no_asm))

--{* normal execution *}
apply (erule Pair_inject)+
apply (simp only:)
apply (rule_tac x="snd (snd fr')" in exI)
apply (rule_tac x="h'" in exI)
apply (rule_tac x="fst fr'" in exI)
apply (rule_tac x="fst (snd fr')" in exI)
apply (rule_tac x="frs'" in exI)
apply (rule_tac x="ea
               \<lparr>cs := if \<exists>Ma n. instrs_of (fst \<Pi>) C M ! pc = Invoke Ma n then ha # cs ea
                      else if instrs_of (fst \<Pi>) C M ! pc = Return then tl (cs ea) else cs ea\<rparr>" in exI)
apply (simp (no_asm))
done
(*>*)


lemma inv_Ty_Reachable:
assumes wf_Pi: "wf \<Pi>"
assumes s_Reachables: "s \<in> Reachables \<Pi>"
shows "\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
(*<*)
proof -
from s_Reachables obtain s0 
  where s0_intro: "s0 \<in> initS \<Pi> \<and> (s0,s) \<in> (effS \<Pi>)\<^sup>*"
  apply (simp only: effS_Reachables)
  apply fastsimp
  done
from s0_intro have
 s0_initS: "s0 \<in> initS \<Pi>"
  by simp
from s0_intro have
 s0_s_effS: "(s0,s) \<in> (effS \<Pi>)\<^sup>*"
  by simp

show "\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  proof -
    obtain \<Phi>k where PhiK_def: "\<Phi>k = (convert_pt (prog_kil (fst \<Pi>)))"
      by fastsimp
    from PhiK_def 
    obtain \<Phi> where Phi_def: "\<Phi> = map_of2 \<Phi>k"
      by fastsimp
    from wf_Pi Phi_def PhiK_def 
    have wt_Pi: "wf_jvm_prog_phi \<Phi> (fst \<Pi>)"
      apply -
      apply (drule wf_TypeSafe)
      apply (simp add: pTy_def)
      done
    obtain P An where Pi_def: "\<Pi> = (P,An)"
      by fastsimp
    obtain p \<sigma> e where s_def: "s = (p,\<sigma>,e)"
      by (cases s)
      
    obtain p0 \<sigma>0 e0 where s0_def: "s0 = (p0,\<sigma>0,e0)"  
      by (cases s0)
     
    obtain C M pc where p_def: "p=(C,M,pc)"
      by (cases p)
      
    from s0_initS s_def s0_s_effS
    obtain h st rg frs 
    where sigma_def: "\<sigma> = (None,h,(st,rg,p)#frs)"
      apply atomize
      apply (drule state_format)
      apply simp
      apply (erule exE)+
      apply fastsimp
      done

    from s0_def s0_initS wf_Pi Pi_def obtain C0 M0 T0 m0
      where s0_startstate: "\<sigma>0 = start_state P C0 M0 \<and> P \<turnstile> C0 sees M0: []\<rightarrow>T0 = m0 in C0"
      apply atomize
      apply simp
      apply (drule startstate_initS)
      apply simp
      apply simp
      done

    from wf_Pi Pi_def s0_initS s0_s_effS s0_def s_def 
    have s0_s_jvm: "P \<turnstile> \<sigma>0 -jvm\<rightarrow> \<sigma>"
      apply -
      apply (rule_tac An="An" in effS_jvm_hull)
      apply simp
      apply simp
      apply simp
      done
      
    from wt_Pi s0_startstate s0_s_jvm Pi_def 
    have sigma_correct: "P,\<Phi> \<turnstile> \<sigma> \<surd>"
      apply -
      apply (rule_tac C="C0" and M="M0" and T="T0" and m="m0" in typesafe)
      apply simp
      apply simp
      apply simp
      done

    obtain ps ps' S Fs Ms Ms' Ts Tr mxs mxl0 bd xt 
    where C_M_format: "(C,M) \<in> set (methodnames P) \<Longrightarrow> (P = ps@(C, S, Fs, Ms @ (M, Ts, Tr, (mxs,mxl0,bd,xt)) # Ms')#ps' \<and> get_mdecl P C M = (M,Ts,Tr,(mxs,mxl0,bd,xt)))"
      apply -
      apply atomize
      apply (case_tac "(C, M) \<in> set (methodnames P)")
      apply (frule methodnames_P)
      apply (erule exE | erule conjE)+
      apply (erule_tac x="ps" in allE)
      apply (erule_tac x="S" in allE)
      apply (erule_tac x="Fs" in allE)
      apply (erule_tac x="Ms" in allE)
      apply (erule_tac x="Ts" in allE)
      apply (erule_tac x="T" in allE)
      apply (erule_tac x="fst bd" in allE)
      apply (erule_tac x="fst (snd bd)" in allE)
      apply (erule_tac x="fst (snd (snd bd))" in allE)
      apply (erule_tac x="snd (snd (snd bd))" in allE)
      apply (erule_tac x="Ms'" in allE)
      apply (erule_tac x="ps'" in allE)
      apply simp

      apply simp
      done

    from wt_Pi Pi_def
    have wf_prog_P: "wf_prog (\<lambda>P C (M, Ts, Tr, mxs, mxl\<^isub>0, is, xt). wt_method P C Ts Tr mxs mxl\<^isub>0 is xt (\<Phi> C M)) P"
      by (simp add: wf_jvm_prog_phi_def)
    
    from wf_prog_P Pi_def C_M_format 
    have method_P_C_M: "(C,M) \<in> set (methodnames P) \<Longrightarrow> method P C M = (C,Ts,Tr,(mxs,mxl0,bd,xt))"
      apply -
      apply (drule method_method')
      apply simp

      apply simp
      apply (erule conjE)+
      apply (simp only: method'_def Let_def split_def fst_conv snd_conv)
      done

    from C_M_format wf_prog_P
    have wt_m_C_M:"(C,M) \<in> set (methodnames P) \<Longrightarrow> wt_method P C Ts Tr mxs mxl0 bd xt (\<Phi> C M)"
      apply -
      apply (simp add: wf_prog_def wf_cdecl_def wf_mdecl_def)
      done

    from wt_m_C_M have wt_C_M:"(C,M) \<in> set (methodnames P) \<Longrightarrow> (bd \<noteq> [] \<and> length (\<Phi> C M) = length bd)"
      by (simp add: TF_JVM.JVM_sl.wt_method_def2)

    from sigma_correct Phi_def sigma_def p_def s_def
    obtain sty rty where sty_rty: "(C,M) \<in> set (methodnames P) \<Longrightarrow> \<Phi> C M ! pc = Some (sty,rty) \<and>  P,h \<turnstile> st [:\<le>] sty \<and> P,h \<turnstile> rg [:\<le>\<^sub>\<top>] rty"
      apply atomize
      apply (case_tac "(C,M) \<in> set (methodnames P)")
      apply (simp add: correct_state_def conf_f_def)
      apply (erule conjE | erule exE)+
      apply fastsimp

      apply simp
      done

    from wf_prog_P C_M_format sty_rty
    have sty_rty_types_P: "\<lbrakk> (C,M) \<in> set (methodnames P); pc < length (\<Phi> C M) \<rbrakk>  \<Longrightarrow> 
    sty \<in> (\<Union>{list n (types P) |n. n \<le> mxs}) \<and> rty \<in> (list (Suc (length Ts + mxl0)) (err (types P)))"
      apply (subgoal_tac "OK ` set (\<Phi> C M) \<subseteq> states P mxs (Suc (length Ts + mxl0))")
       prefer 2
       apply (simp add: wf_prog_def wf_cdecl_def wf_mdecl_def wt_method_def check_types_def)
      apply (simp add: subset_def)
      apply (erule_tac x="Some (sty,rty)" in ballE)
       prefer 2
       apply (drule nth_mem)      
       apply simp
      apply (simp add: subset_def states_def sl_def Err.sl_def 
             Err.esl_def Opt.esl_def Product.esl_def stk_esl_def 
             upto_esl_def SemiType.esl_def Listn.sl_def split_def loc_sl_def JVM_SemiType.sl_def)
      done

    from sty_rty_types_P have sty_types_P: "\<And> k. \<lbrakk> (C,M) \<in> set (methodnames P); 
    pc < length (\<Phi> C M); k < length sty \<rbrakk> \<Longrightarrow> is_type P (sty ! k)" 
      apply (simp add: subset_def)
      done
    
    from sty_rty_types_P have rty_types_P: "\<And> k tp. \<lbrakk> (C,M) \<in> set (methodnames P); 
    pc < length (\<Phi> C M); k < length rty; rty ! k = OK tp \<rbrakk> \<Longrightarrow> is_type P tp" 
      apply simp
      apply (erule conjE | erule in_listE)+
      apply (drule nth_mem)+
      apply (simp add: subset_def err_def)
      apply (erule_tac x="OK tp" in ballE)
       prefer 2
       apply simp
      apply simp
      done

   
    have goal: "\<Pi>,(p,\<sigma>,e) \<Turnstile> annotate_types P \<Phi>k p"
      proof (cases "(C,M) \<in> set (methodnames P)")
	case False
	 from this s_def p_def sigma_def Phi_def sigma_correct 
	 show ?thesis
	   by (simp add: annotate_types_def mem_iff)

       next
	 
	 case True
	 show ?thesis
	   proof (cases "map_of \<Phi>k (C,M)")
	     
	     case None
	     from this True p_def sty_rty Phi_def wt_C_M show ?thesis
	       by  (simp add: map_of2_def)
	     
	     next
	       
	       case (Some mty)
	       from this True sty_rty Phi_def
	       have mty_pc: "mty ! pc = Some (sty,rty)"
		 by (simp add: map_of2_def)
	       from Some Phi_def have mty_def: "mty = \<Phi> C M"
		 by (simp add: map_of2_def)
	       from Some True mty_pc mty_def s_def p_def sigma_def Phi_def sigma_correct sty_rty
	       show ?thesis
		 apply (simp add: annotate_types_def lookup_map_of mem_iff)
		 apply (rule impI)
		 apply (simp add: conv_st_def list_all_iff)
		 apply (rule ballI)
		 apply (drule in_evalEs_conv)
		 apply (erule bexE)
		 apply simp
		 apply (erule disjE)

		 --{* Stack *}
		 apply (erule imageE)
		 apply simp
		 apply (subgoal_tac "P,h \<turnstile> st ! n :\<le> sty ! n")
		  prefer 2
		  apply (simp add: list_all2_conv_all_nth)
		 apply (subgoal_tac "length st = length sty")
		  prefer 2
		  apply (simp add: list_all2_def)
		 apply (subgoal_tac "is_type P (sty ! n)")
		  prefer 2
		  apply (rule sty_types_P)
		  apply assumption
		  apply simp
		  apply assumption	  
		 apply (case_tac "(sty ! n)::ty")
		 --{* sty ! n = Void *}
		 apply (simp add: STy_def)
		 apply (case_tac "(st ! n)::val")
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def obj_ty_def split_def)

		 --{* sty ! n = Boolean *} 
		 apply (simp add: STy_def)
		 apply (case_tac "(st ! n)::val")
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def obj_ty_def split_def)

		 --{* sty ! n = Integer *} 
		 apply (simp add: STy_def)
		 apply (case_tac "(st ! n)::val")
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def obj_ty_def split_def)

		 --{* sty ! n = NT *} 
		 apply (simp add: STy_def)

		 --{* sty ! n = Class list *} 
		 apply (simp add: STy_def evalE_Or)
		 apply (case_tac "(st ! n)::val")
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def) 
		 --{* st ! n = Addr nat *}
		 apply (simp add: conf_def) 
		 apply (rule allI)
		 apply (rule impI)
		 apply (erule exE)
		 apply (simp add: obj_ty_def)
		 apply (drule_tac t="T'" in sym)
		 apply (simp add: subclasses_def)
		 apply (erule converse_rtranclE)
		 apply (simp add: is_class_def class_def)
		 apply (erule exE)+
		 apply (drule map_of_SomeD)+
		 apply (drule_tac A = "set P" and f="fst" in imageI)
		 apply simp

		 --{* aa < y and y <=* list *}
		 apply (erule subcls1.elims)
		 apply (simp add: class_def)
		 apply (drule map_of_SomeD)+
		 apply (drule_tac A="set P" and f="fst" in imageI)
		 apply simp

		 --{* Register *}
		 apply (erule imageE)
		 apply simp
		 apply (subgoal_tac "P,h \<turnstile> rg ! n :\<le>\<^sub>\<top> rty ! n")
		  prefer 2
		  apply (simp add: list_all2_conv_all_nth)
		 apply (subgoal_tac "length rg = length rty")
		  prefer 2
		  apply (simp add: list_all2_def)
		 apply (case_tac "(rty ! n):: ty err")
		 --{* Err *}
		 apply (simp add:  not_none_def none_def)

		 --{* rty ! n = OK a *}
		 apply (subgoal_tac "is_type P a")
		  prefer 2
		  apply (rule rty_types_P)
		  apply assumption
		  apply simp
		  apply assumption
		  apply assumption
		 apply (case_tac "a::ty")
		 --{* a = Void *}
		 apply (simp add: STy_def)
		 apply (case_tac "(rg ! n)::val")
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def obj_ty_def split_def)

		 --{* a = Boolean *} 
		 apply (simp add: STy_def)
		 apply (case_tac "(rg ! n)::val")
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def obj_ty_def split_def)

		 --{* a = Integer *} 
		 apply (simp add: STy_def)
		 apply (case_tac "(rg ! n)::val")
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def)
		 apply (simp add: conf_def obj_ty_def split_def)

		 --{* a = NT *} 
		 apply (simp add: STy_def)

		 --{* a = Class list *} 
		 apply (simp add: STy_def evalE_Or)
		 apply (case_tac "(rg ! n)::val")
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def) 
		 apply (simp add: conf_def) 
		 --{* a = Addr nat *}
		 apply (simp add: conf_def) 
		 apply (rule allI)
		 apply (rule impI)
		 apply (erule exE)
		 apply (simp add: obj_ty_def)
		 apply (drule_tac t="T'" in sym)
		 apply (simp add: subclasses_def)
		 apply (erule converse_rtranclE)
		 apply (simp add: is_class_def class_def)
		 apply (erule exE)+
		 apply (drule map_of_SomeD)+
		 apply (drule_tac A = "set P" and f="fst" in imageI)
		 apply simp

		 --{* aa < y and y <=* list *}
		 apply (erule subcls1.elims)
		 apply (simp add: class_def)
		 apply (drule map_of_SomeD)+
		 apply (drule_tac A="set P" and f="fst" in imageI)
		 apply simp
		 done
	       qed
	     qed
	     from this Phi_def PhiK_def s_def Pi_def
	     show ?thesis
	       by (simp add: inv_Ty_def)
	     qed
qed
(*>*)


lemma statesplit_Reachables:
"s \<in> Reachables \<Pi> \<Longrightarrow> \<exists> C M pc h st rg frs e. s = ((C,M,pc),(None,h,(st,rg,(C,M,pc))#frs),e) \<and> fst (snd (last (map (snd \<circ> snd) ((st,rg,(C,M,pc))#frs)) )) = fst (snd (ipc \<Pi>))"
(*<*)
apply (erule Reachables.induct)
--{* init *}
apply (simp add: split_paired_all initS_def start_state_def ipc_def)
apply (simp add: split_def)
apply (rule_tac x="start_heap (fst \<Pi>)" in exI)
apply (rule_tac x="[]" in exI)
apply (rule_tac x="Null # replicate (fst (snd (snd (snd (snd (method (fst \<Pi>) Start main)))))) arbitrary" in exI)
apply (rule_tac x="[]" in exI)
apply simp

--{* step *}
apply (erule conjE | erule exE)+
apply (simp del: last.simps)

apply (erule effS.elims)
--{* EXCEPTIONAL EXECUTION *}
apply (subgoal_tac "\<exists> An. \<Pi> = (P,An)")
 prefer 2
 apply (rule_tac x="snd \<Pi>" in exI)
 apply simp
apply (erule exE)
apply (erule_tac V="P = fst \<Pi>" in thin_rl)
apply (drule_tac s="i" in sym)
apply (simp only:)
apply (rule_tac x="fst p'" in exI)
apply (rule_tac x="fst (snd p')" in exI)
apply (rule_tac x="(snd (snd p'))" in exI)
apply (rule_tac x="ha" in exI)
apply (rule_tac x="[Addr xa]" in exI)
apply (rule_tac x="loc'" in exI)
apply (rule_tac x="frs'" in exI)
apply (frule find_handler_frs')
apply (erule exE)
apply (case_tac "pfx")
apply simp

apply simp
apply (case_tac "frs" rule: rev_cases)
apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="p'" in sym)
apply (drule_tac t="a" in sym)
apply simp

apply (case_tac "frs'" rule: rev_cases)
apply (simp add: split_def)
apply (frule find_handler_frs')
apply (erule exE)
apply simp
apply (drule_tac s="ys @ [y]" in sym)
apply (simp add: split_paired_all)

apply simp

--{* NORMAL EXECUTION *}
apply (subgoal_tac "\<exists> An. \<Pi> = (P,An)")
 prefer 2
 apply (rule_tac x="snd \<Pi>" in exI)
 apply simp
apply (erule exE)
apply (erule_tac V="P = fst \<Pi>" in thin_rl)
apply (drule_tac s="i" in sym)
apply (simp only:)
apply (rule_tac x="fst p'" in exI)
apply (rule_tac x="fst (snd p')" in exI)
apply (rule_tac x="(snd (snd p'))" in exI)
apply (rule_tac x="h'" in exI)
apply (rule_tac x="fst fr'" in exI)
apply (rule_tac x="fst (snd fr')" in exI)
apply (rule_tac x="frs'" in exI)
apply (simp del: last.simps)

apply (case_tac "i")
--{* Load *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* Store *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* Push *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* New *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* Getfield *}
apply (simp del: last.simps)
apply (case_tac "hd stk = Null")
apply (simp add: split_def)

apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* Putfield *}
apply (simp del: last.simps)
apply (case_tac "hd (tl stk) = Null")
apply (simp add: split_def)

apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* Checkcast *}
apply (simp del: last.simps)
apply (case_tac "\<not> cast_ok P list ha (hd stk)")
apply (simp add: split_def)

apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* Invoke *}
apply (simp del: last.simps)
apply (case_tac "stk ! nat = Null")
apply (simp add: split_def)

apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="a" in sym)
apply (simp del: last.simps)
apply (case_tac "lista")
apply simp

apply simp

--{* Return *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (case_tac "frsa")
apply simp

apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp
apply (case_tac "frs'")
apply simp

apply simp

--{* Pop *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* IBin *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp
--{* Goto *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp

--{* CmpEq *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp

--{* IfIntCmp *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp

--{* IfFalse *}
apply (simp del: last.simps)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (simp only: fst_conv snd_conv)
apply (case_tac "frs'")
apply simp

apply simp

--{* Throw *}
apply simp
apply (case_tac " hd stk = Null")
apply simp

apply simp
done
(*>*)


lemma callstates_Reachables:
assumes s_Reachables: "s \<in> (Reachables \<Pi>)"
shows "\<forall>s' \<in> (callstates s). s' \<in> (Reachables \<Pi>)" using s_Reachables
(*<*)
proof (induct rule: Reachables.induct)
  case (init s)
  from this have s_initS:"s \<in> initS \<Pi>" 
  by assumption
  obtain p x h frs e where s_def: "s = (p,(x,h,frs),e)"
    by (cases "s") (fastsimp simp add: split_paired_all)
  from s_initS have s_Reachables: "s \<in> Reachables \<Pi>"
  by (rule Reachables.init)
  from s_initS s_def obtain st rg where init_frs: "frs = [(st,rg,p)]"
    apply -
    apply simp
    apply (frule initS_frs)
    apply (cases frs)
    apply simp
    apply (case_tac "a")
    apply (case_tac "b")
    apply (simp add: initS_def start_state_def split_def ipc_def)
    apply fastsimp
    done
  from s_def init_frs have callstate_s: "callstate s = s"
    by simp
  from s_def init_frs s_Reachables callstate_s show ?case
    by (simp add: callstate_idem_callstates)

next
  case (step s s')
  assume s_Reachables: "s \<in> Reachables \<Pi>"
  assume callstates_s_Reachables: "\<forall>s'\<in>callstates s. s' \<in> Reachables \<Pi>"
  assume s_s'_effS: "(s, s') \<in> effS \<Pi>"
  have s'_Reachables:"s' \<in> Reachables \<Pi>"
    by (rule Reachables.step)
  show ?case
  proof (rule effS.elims[OF s_s'_effS])
  fix p \<sigma> e p' \<sigma>' e' P C M pc i h stk loc frs
  assume s_s'_def:    "(s, s') = ((p, \<sigma>, e), p', \<sigma>', e')"
  assume P_def:       "P = fst \<Pi>"
  assume p_def:       "p = (C, M, pc)"
  assume i_def:       "i = instrs_of P C M ! pc"
  assume sigma_def:   "\<sigma> = (None, h, (stk, loc, p) # frs)"
 (* assume check_sigma: "check P \<sigma>" *)
  assume has_method_C_M: "JBC_Semantics.has_method P C M"
  { --{* EXCEPTIONAL EXECUTION *}
    fix xa h' frs'' loc' frs' 
    assume exec_i: "exec_instr i P h stk loc C M pc frs = (\<lfloor>xa\<rfloor>, h', frs'')"
    assume find_handler_s: "find_handler P xa h ((stk, loc, p) # frs) = \<sigma>'"
    assume sigma'_def: "\<sigma>' = (None, h, ([Addr xa], loc', p') # frs')"
    assume e'_def: "e' = e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>"
    show ?case
    proof (rule ballI)
    fix sc 
    assume sc_callstates_s': "sc \<in> callstates s'" 
    show "sc \<in> Reachables \<Pi>"
    proof (cases frs')
      case Nil
      from s_s'_def Nil sigma'_def 
      have callstate_s': "callstate s' = s'"
	by simp
      from callstate_s' sc_callstates_s' 
      have sc_s': "sc = s'"
	by (simp add:  callstate_idem_callstates)
      from sc_s' s'_Reachables show ?thesis by simp
    next
      case (Cons a list)
      obtain st_a rg_a p_a where a_def: "a = (st_a,rg_a,p_a)"
	by (cases "a", fastsimp)
      from find_handler_s sigma'_def 
      obtain pfx where frs_pfx_frs': "frs = pfx @ frs'"
	apply -
	apply (simp only:)
	apply (drule find_handler_frs)
	apply (erule exE)
	apply (case_tac "pfx")
	apply simp

	apply simp
	done
      from s_s'_def e'_def sigma'_def Cons a_def frs_pfx_frs' 
      have callstate_s'_in_callstates_s: "callstate s' \<in> callstates s"
	apply -	
	apply (simp only: Pair_eq callstate.simps)
	apply (subgoal_tac "(snd (snd (st_a,rg_a,p_a)), (None, hd (cs e'), (st_a, rg_a, p_a) # list), e'\<lparr>cs := tl (cs e')\<rparr>) 
               \<in> callstates (p,(None, h, (stk, loc, p) # frs), e)")
	 prefer 2
	 apply (rule callstates_frs)
	 apply simp

	 apply simp
	apply (simp add: sigma_def)
	done
      from callstate_s'_in_callstates_s 
      have callstates_s'_subset_s: "callstates (callstate s') \<subseteq> callstates s"
	by (rule callstates_subset)
      from callstates_s'_subset_s sc_callstates_s' callstates_s_Reachables callstate_s'_in_callstates_s
      show ?thesis
      apply (drule_tac P="\<lambda> S. sc \<in> S" in subst[OF callstates_union])
      apply simp
      apply (erule disjE)
      apply simp
      
      apply (simp add: subsetD)
      done
    qed
    qed
     next
  --{* Normal Execution *}
  fix h' fr' frs'
  assume exec_i: "exec_instr i P h stk loc C M pc frs = (None, h', fr' # frs')"
  assume sigma'_def: "\<sigma>' = (None, h', fr' # frs')"
  assume p'_def: "p' = snd (snd fr')"
  assume e'_def: "e' = e\<lparr>cs := if \<exists>M n. i = Invoke M n then h # cs e else if i = Return then tl (cs e) else cs e\<rparr>"
  show ?case
  proof (rule ballI)
    fix sc 
    assume sc_callstates_s': "sc \<in> callstates s'" 
    show "sc \<in> Reachables \<Pi>"
    proof (cases frs')
      case Nil
      from s_s'_def Nil sigma'_def 
      have callstate_s': "callstate s' = s'"
	by simp
      from callstate_s' sc_callstates_s' 
      have sc_s': "sc = s'"
	by (simp add:  callstate_idem_callstates)
      from sc_s' s'_Reachables show ?thesis by simp
  next
    case (Cons a list)
      obtain st_a rg_a p_a where a_def: "a = (st_a,rg_a,p_a)"
	by (cases "a", fastsimp)
      note exec_simp = Cons s_s'_def p_def sigma_def sigma'_def p'_def e'_def exec_i
      show ?thesis
	proof (cases "i")
	  case (Load "nat")
	  from Load exec_simp
          have callst_s_s': "callstates s = callstates s'"
	    apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
                 and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	    by simp+
	  from callstates_s_Reachables callst_s_s' sc_callstates_s'
	  show ?thesis
	  by simp
	
      next
	case (Store "nat")
	from Store exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
            and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by simp+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp

      next
	case (Push "val")
	from Push exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h" 
            and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by simp+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp
	
      next
	case (New "list")
	from New exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
            and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by simp+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp
	
      next
	case (Getfield "list1" "list2")
	from Getfield exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
            and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp

      next
	case (Putfield "list1" "list2")
	from Putfield exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
            and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp
	
      next
	case (Checkcast "list")
	from Checkcast exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
            and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp	

      next
	case (Invoke "list" "nat")
	from Invoke exec_simp a_def
	have callstate_s'_s: "callstate s' = s"
	  by (simp add: split_def)
	from callstate_s'_s 
        have callst_s_s': "callstates s' = {s} \<union> callstates s"
	  by (simp add: callstates_union[of "s'"])
	from callstates_s_Reachables callst_s_s' sc_callstates_s' s_Reachables
	show ?thesis
	  by fastsimp
	
      next
	case Return
	show ?thesis
	proof (cases frs)
	  case Nil
	  from Nil Return exec_simp 
	  have callst_s'_s': "callstates s' = {s'}"
	    by simp
	  from callst_s'_s' s'_Reachables sc_callstates_s'
	  show ?thesis
	    by simp
	  
	next
	  case (Cons cf cfs)
	  obtain st_c rg_c p_c where cf_def : "cf = (st_c,rg_c,p_c)"
	    by (cases "cf")
	  from Cons cf_def Return exec_simp sigma'_def a_def
	  have callst_s'_s: "callstate s' = callstate (callstate s)"
	    by (simp add: split_def)
	  from callst_s'_s sc_callstates_s' callstates_s_Reachables
	  show ?thesis 
	    apply (simp add: callstates_union[of "s'"] callstates_union[of "s"])
	    apply (erule disjE)
	    apply (simp add: callstates_union[of "callstate s"])
	    
	    apply (simp add: callstates_union[of "callstate s"])
	    done	
	qed
	
      next
	case Pop
	from Pop exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
	    and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp
	
      next
	case IBin
	from IBin exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
	    and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp
	
      next
	case (Goto "t")
	from Goto exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
	    and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp
	
      next
	case CmpEq
	from CmpEq exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
	    and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp	    
	
      next
	case (IfIntCmp "ro" "t")
	from IfIntCmp exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
	    and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp	    
	
      next
	case (IfFalse "t")
	from IfFalse exec_simp
        have callst_s_s': "callstates s = callstates s'"
	  apply (rule_tac p="p" and p'="p'" and x="None" and x'="None" and h="h" and h'="h'" 
            and fr="(stk, loc, C, M, pc)" and fr'="fr'" and frs="frs" and e="e" in callstates_eq)
	  by (simp add: split_def)+
	from callstates_s_Reachables callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp

      next	
	case Throw
	from Throw exec_simp
	show ?thesis
	  by (simp add: split_def split add: split_if_asm)
      qed
    qed
  qed
  }
qed
qed
(*>*)


lemma callstate_Reachables:
"\<And> s. s \<in> (Reachables \<Pi>) \<Longrightarrow> callstate s \<in> (Reachables \<Pi>)"
(*<*)
apply (drule callstates_Reachables)
apply (subgoal_tac "callstate s \<in> (callstates s)")
 prefer 2
 apply (rule callstates.init)
apply fastsimp
done
(*>*)


lemma callers_sysinv_pos:
"callers_sysinv (\<Pi>,(p,(x,h,frs),e)) = callers_sysinv (\<Pi>,(p',(x,h,frs),e))"
(*<*)
apply (case_tac "frs")
apply simp

apply (case_tac "list")
apply simp
apply simp
done
(*>*)



lemma callers_sysinv_append:
"\<And> p fr fr' frs' h e. callers_sysinv (\<Pi>,(p,(None,h,frs@fr#fr'#frs')::jvm_state,e)) \<Longrightarrow> snd (snd fr') \<in> set (callers \<Pi> (snd (snd fr))) \<and> (\<forall> p' h' e'. callers_sysinv (\<Pi>,(p',(None,h',fr'#frs'),e')))"
proof (induct frs)

case Nil
 from Nil show ?case
   apply -
   apply (case_tac "frs'\<Colon>val list ~~> val list \<times> char list \<times> char list \<times> nat")
   apply (simp add: split_def)

   apply (simp add: split_def)
   apply (rule allI)+
   apply (erule conjE)+
   apply (case_tac "list")
   apply simp

   apply (simp add: split_def del: callers_sysinv.simps)
   apply (subgoal_tac "callers_sysinv (\<Pi>, snd (snd aa), (None, hd (tl (tl (cs e))), aa # lista), e\<lparr>cs := tl (tl (tl (cs e)))\<rparr>) =
                       callers_sysinv (\<Pi>, snd (snd aa), (None, hd (tl (cs e')), aa # lista), e'\<lparr>cs := tl (tl (cs e'))\<rparr>)")
    prefer 2
    apply (rule callers_sysinv_env)
   apply simp
   done

next

  case (Cons fr'' frs'')
  from Cons show ?case
    apply -
    apply (drule_tac P="\<lambda> x. x" in subst[OF callers_sysinv.simps])
    apply (simp del: callers_sysinv.simps)
    apply (case_tac "(frs'' @ fr # fr' # frs')")
    apply (simp del: callers_sysinv.simps)

    apply (simp only: list.cases)
    apply (drule_tac t="a # list" in sym)
    apply (simp only:)
    apply (simp add: Let_def split_def fst_conv snd_conv  del: callers_sysinv.simps)
    apply atomize
    apply (erule_tac x="snd (snd a)" in allE)
    apply (erule_tac x="hd (cs e)" in allE)
    apply (erule_tac x="fr" in allE)
    apply (erule_tac x="fr'" in allE)
    apply (erule_tac x="frs'" in allE)
    apply (erule_tac x="e\<lparr>cs := tl (cs e)\<rparr>" in allE)
    apply (erule conjE)+
    apply (drule mp, assumption)
    apply simp
    done
  qed


lemma statesplit_Pos:
assumes s_Pos: "\<Pi>,s \<Turnstile> Pos (fst s)"
shows "\<exists> C M pc h st rg frs e. s = ((C, M, pc), (None, h, (st, rg, C, M, pc) # frs), e)"
(*<*)
proof -
  obtain p \<sigma> e where s_def: "s = (p,\<sigma>,e)"
    apply atomize
    apply (erule_tac x="fst s" in allE)
    apply (erule_tac x="fst (snd s)" in allE)
    apply (erule_tac x="snd (snd s)" in allE)
    apply simp
    done
  obtain C M pc where p_def: "p = (C,M,pc)"
    apply atomize
    apply (erule_tac x="fst p" in allE)
    apply (erule_tac x="fst (snd p)" in allE)
    apply (erule_tac x="snd (snd p)" in allE)
    apply simp
    done
  from s_def p_def s_Pos
  obtain h st rg frs where sigma_def: "\<sigma> = (None,h,(st,rg,C,M,pc)#frs)"
    apply atomize
    apply (simp add: split_def)
    apply (subgoal_tac "\<exists> h st rg frs. \<sigma> = (None, h, (st, rg, C, M, pc) # frs)")
     prefer 2
     apply (rule_tac x="fst (snd \<sigma>)" in exI)
     apply (case_tac "snd (snd \<sigma>) = []")
     apply simp
     apply (subgoal_tac "\<exists> fr frs. snd (snd \<sigma>) = fr#frs")
      prefer 2
      apply (simp add: neq_Nil_conv)
     apply (erule exE)+
     apply (rule_tac x="fst fr" in exI)
     apply (rule_tac x="fst (snd fr)" in exI)
     apply (rule_tac x="frs" in exI)
     apply simp
     apply (drule_tac t="fr # frs" in sym)
     apply (simp add: split_def split_paired_all)
     apply (erule conjE)+
     apply (subgoal_tac "(fst \<sigma>,snd \<sigma>) = \<sigma>")
      prefer 2
      apply (erule thin_rl)+
      apply fastsimp
     apply (simp only:)
    apply simp
    done
  from p_def s_def sigma_def
  show ?thesis
    by simp
qed
(*>*)


lemma callers_sysinv_Pos: "\<Pi>,s \<Turnstile> Pos (fst s) \<Longrightarrow> callers_sysinv (\<Pi>,s)"
(*<*)
by simp
(*>*)


constdefs correctAn::"jbc_prog \<Rightarrow> bool"
"correctAn \<Pi> \<equiv> (\<forall> s \<in> Reachables \<Pi>. (\<forall> An. (anF \<Pi> (fst s) = Some An) \<longrightarrow> \<Pi>,s \<Turnstile> An))" 


lemma correct_state_inv:
assumes wt:"wf_jvm_prog\<^isub>k P"
assumes sees_mthd:"P \<turnstile> C sees M:[]\<rightarrow>T = m in C"
assumes reachable:"P \<turnstile> start_state P C M -jvm\<rightarrow> \<sigma>'"
shows "\<exists> \<Phi>. P,\<Phi> \<turnstile> \<sigma>' \<surd>"
(*<*)
proof -
 from wt have wf_P:"\<exists> \<Phi>. wf_jvm_prog\<^sub>\<Phi>  P " by (simp add: jvm_kildall_correct wf_jvm_prog_def)
 from sees_mthd reachable show ?thesis 
  proof -
  from wf_P obtain \<Phi> where wf_P': "wf_jvm_prog\<^sub>\<Phi>  P" ..
   from this have state_ok: "P,\<Phi> \<turnstile> \<sigma>' \<surd>" 
   proof (rule typesafe)
    from sees_mthd show "P \<turnstile> C sees M: []\<rightarrow>T = m in C" .
    from sees_mthd reachable show "P \<turnstile> start_state P C M -jvm\<rightarrow> \<sigma>'" by simp
   qed
  from this show ?thesis proof (rule_tac x="\<Phi>" in exI, assumption) qed
 qed
qed
(*>*)

section{* Wellformed Control Flow *}

lemma succsF_domC:
"\<lbrakk> wf \<Pi>; (p',B) \<in> set (succsF \<Pi> p) \<rbrakk> \<Longrightarrow> (p \<in> set (domC \<Pi>) \<and> p' \<in> set (domC \<Pi>))"
(*<*)
apply (case_tac "cmd \<Pi> p")
apply (simp add: succsF_def succsNormal_def succsExcept_def addPos_def)

--{* cmd Pi p = Some a *}
apply (drule cmd_domC)
apply (subgoal_tac "\<exists> dC dC'. domC \<Pi> = dC@p#dC'")
 prefer 2
 apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: wf_def checkPos_split if_then_else_False list_all_iff)
apply (erule conjE)+
apply (erule_tac x="p'" in ballE)
 prefer 2
 apply (simp add: succsF_def addPos_def)
 apply (erule disjE)
 apply (erule imageE)
 apply (simp add: split_def)

 apply (erule imageE)
 apply (simp add: split_def)
apply (simp add: set_mem_eq)
done
(*>*)

lemma succsXpt_xcpt_cond:
"\<And> L. \<lbrakk> fst ` set (succsXpt (\<Pi>, X, L)) \<subset> set (domC \<Pi>); 
  (p',B) \<in> set (succsXpt (\<Pi>, X, L));
  (\<exists> L'. L = L'@[p]) \<rbrakk>
\<Longrightarrow> \<exists> As. B = And (As@[xcpt_cond \<Pi> X p])"
(*<*)
apply (subgoal_tac "\<exists> k. length (domC \<Pi>) - length L = k")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule_tac forall_switch3)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI | rule impI)+

apply (subgoal_tac "\<exists> P An. \<Pi> = (P,An)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp only:)
apply (drule_tac P="\<lambda> S. (p',B) \<in> set S" in subst[OF succsXpt.simps])
apply (case_tac "length (domC (P, An)) \<le> length (L' @ [p])")
apply (simp add: map_fst_tuple image_fst_tuple)

apply (simp del: succsXpt.simps)
apply (case_tac "L' @ [p]")
apply simp

apply (simp del: succsXpt.simps add: split_def)
apply (erule bexE)
apply (erule_tac x="length (domC (P,An)) - length (aa#L)" in allE)
apply (subgoal_tac "length (domC (P, An)) - length (aa # L) < n")
 prefer 2
 apply (erule_tac V="(p', B) \<in> set (succsXpt ((P, An), X, aa # a # list))" in thin_rl)
 apply (erule_tac V="?S \<subset> ?S'" in thin_rl)
 apply (erule_tac V="?T = None" in thin_rl)
 apply (erule_tac V="?P \<longrightarrow> ?Q" in thin_rl)
 apply (drule_tac t="a # list" in sym)
 apply simp
 apply arith
apply (drule mp, assumption)
apply (erule_tac x="aa # L" in allE)
apply (simp only: simp_thms)
apply (erule_tac x="aa # L'" in allE)
apply (subgoal_tac "aa # a # list = (aa # L') @ [p]")
 prefer 2
 apply (drule_tac t="a # list" in sym)
 apply simp
apply (drule mp, assumption)
apply (subgoal_tac "(p', B) \<in> set (succsXpt ((P, An), X, (aa # L') @ [p]))")
 prefer 2
 apply (simp only: simp_thms)
apply (drule mp, assumption)
apply (subgoal_tac " fst ` set (succsXpt ((P, An), X, (aa # L') @ [p])) \<subset> set (domC (P, An))")
 prefer 2
 apply (drule_tac P="\<lambda> S. fst ` set S \<subset> set (domC (P,An))" in subst[OF succsXpt.simps])
 apply (drule_tac t="a # list" in sym)
 apply (simp del: succsXpt.simps)
 apply (drule_tac s="a # list" in sym)
 apply (simp del: succsXpt.simps add: split_def in_set_conv_decomp) 
 apply (erule exE)+
 apply (simp del: succsXpt.simps)
 apply (simp only: insert_def)
 apply (simp only: image_Un simp_thms,drule un_subset_drop,assumption)
apply (drule mp,assumption)
apply assumption

apply (case_tac "list" rule: rev_cases)
apply simp

apply (simp del: succsXpt.simps)
done
(*>*)

lemma wf_succsXpt_xcpt_cond:
assumes wf_Pi: "wf \<Pi>"
and cmd_p: "cmd \<Pi> p = Some i"
and i_not_Throw: "i \<noteq> Throw"
and p'_succsExcept_p: "(p',B) \<in> set (succsExcept \<Pi> p)"
shows "\<exists> As. B = And (As @ [xcpt_cond \<Pi> (sys_xcpt_of i) p])"
proof -

from cmd_p
have p_domC: "p \<in> set (domC \<Pi>)"
  by (rule cmd_domC)

from p_domC obtain dC dC' 
where dC_p_dC': "domC \<Pi> = dC @ p # dC'"
  apply -
  apply (simp add: in_set_conv_decomp)
  apply fastsimp
  done

from dC_p_dC' wf_Pi cmd_p p'_succsExcept_p i_not_Throw
have subset_domC:"fst ` set (succsXpt (\<Pi>, (sys_xcpt_of i), [p])) \<subset> set (domC \<Pi>)"
  apply -
  apply (simp add: wf_def checkPos_split succsExcept_def 
         split add: split_if_asm split del: option.split_asm option.split)
  apply (case_tac "i")
  apply (simp add: sys_xcpt_of_def split del: option.split_asm option.split)+
  done

from p'_succsExcept_p i_not_Throw cmd_p
have p'_succsXpt_p: "(p',B) \<in> set (succsXpt (\<Pi>,sys_xcpt_of i,[p]))"
  apply -
  apply (simp add: succsExcept_def split del: option.split_asm option.split)
  apply (case_tac "i")
  apply (simp add: sys_xcpt_of_def split del: option.split_asm option.split)+
  done

from p'_succsXpt_p subset_domC show ?thesis
  apply -
  apply (rule succsXpt_xcpt_cond)
  apply assumption
  apply assumption
  apply simp
  done
qed


end