header {* 
  \isaheader{Jinja Assertion Logic} 
*}

theory JBC_SafetyLogic = JBC_SafetyPolicy + VCG:


subsection {* Evaluation of Expressions *}




consts callstate::"jbc_state \<Rightarrow> jbc_state"
recdef callstate "{}"
"callstate (p,(x,h,fr#(st,rg,p')#frs),e) = 
           (p',(None,hd (cs e),(st,rg,p')#frs),e\<lparr>cs:=tl (cs e)\<rparr>)"

"callstate s = s"

consts
catchstate::"(jvm_prog \<times> cname \<times> jbc_state) \<Rightarrow> jbc_state"
recdef catchstate "measure (\<lambda>(P,cn,(p,(x,hp,frs),e)). length frs)"
"catchstate (P,X,(p,(x,h,fr#(st,rg,p')#frs),e)) = 
(let (C,M,pc)=p' in (case (match_ex_table P X pc (ex_table_of P C M))
of None \<Rightarrow> catchstate(P,X,(p',(None,hd (cs e),(st,rg,p')#frs),e\<lparr>cs:=tl(cs e)\<rparr>))
| Some pc' \<Rightarrow> (p',(None,hd (cs e),(st,rg,p')#frs),e\<lparr>cs:=tl (cs e)\<rparr>)))"

"catchstate (P,X,s) = s"


consts
frameCnt:: "jbc_state \<Rightarrow> nat"
defs frameCnt_def [simp]:
"frameCnt s \<equiv> (let (p,\<sigma>,e)=s; (x,h,frs)=\<sigma> in length frs)"


consts callers_sysinv::"(jbc_prog \<times> jbc_state) \<Rightarrow> bool"
recdef callers_sysinv "measure (\<lambda> (\<Pi>,s). frameCnt s)"
"callers_sysinv (\<Pi>,(ps,(x,h,frs),e)) = (case frs
of [] \<Rightarrow> True | fr # frs' \<Rightarrow> (case frs' of [] \<Rightarrow> (let (st,rg,p)=fr in p mem (domC \<Pi>)  
                                                                      \<and> fst p = fst (ipc \<Pi>) 
                                                                      \<and> fst (snd p) = fst (snd (ipc \<Pi>)))
| fr'#frs'' \<Rightarrow> (let (st,rg,p)=fr; (st',rg',p')=fr' 
in (p mem (domC \<Pi>) \<and> (p' \<in> set (callers \<Pi> p) \<and> callers_sysinv (\<Pi>,(p',(None,hd (cs e),frs'),e\<lparr>cs:=tl (cs e)\<rparr>)))))))"



constdefs the_Bool::"val option \<Rightarrow> bool"
"the_Bool v \<equiv> (v = Some (Bool True))"


constdefs
arb::"val"
"arb \<equiv> arbitrary"


consts
evalNewA::"heap \<Rightarrow> nat \<Rightarrow> val"
primrec
"evalNewA h 0 = (case new_Addr h of None \<Rightarrow> Null
                | Some a  \<Rightarrow> Addr a)"
"evalNewA h (Suc n) = evalNewA (h(the (new_Addr h):= Some arbitrary)) n"


consts
evalE::"jbc_prog  \<Rightarrow> jbc_state \<Rightarrow> expr \<Rightarrow> val option"
evalEs::"jbc_prog \<Rightarrow> jbc_state \<Rightarrow> expr list \<Rightarrow> (val option) list"
primrec
evalEs_empty:
"evalEs \<Pi> s [] = []"

evalEs_cons:
"evalEs \<Pi> s (ex#exs) = (evalE \<Pi> s ex)#(evalEs \<Pi> s exs)"

evalE_Rg:
"evalE \<Pi> s (Rg k) = (let (p,\<sigma>,e)=s;(x,h,fs)=\<sigma>; (st,rg,p')=hd fs 
                        in (if k < length rg then Some (rg!k) else None))"

evalE_St:
"evalE \<Pi> s (St k) = (let (p,\<sigma>,e)=s;(x,h,fs)=\<sigma>; (st,rg,p')=hd fs 
                       in (if k < length st then Some (st!k) else None))"

evalE_Lv:
"evalE \<Pi> s (Lv k) = (let (p,\<sigma>,e)=s in ((lv e) k))"

evalE_Cn:
"evalE \<Pi> s (Cn v) = Some v"

evalE_NewA:
"evalE \<Pi> s (NewA n) = (let (p,\<sigma>,e)=s; (x,h,frs)=\<sigma> 
                        in Some (evalNewA h n))"

evalE_Gf:
"evalE \<Pi> s (Gf F C ex) = (case (evalE \<Pi> s ex)
                             of Some v \<Rightarrow> (case v of Addr a \<Rightarrow> Some (let (p,\<sigma>,e)=s; (x,h,frs)=\<sigma>; (D,fs)=the (h a)
                                                                     in the (fs (F,C)))
                                                  | _ \<Rightarrow> None)
                             | _ \<Rightarrow> None)"

evalE_Fr:
"evalE \<Pi> s FrNr = (let (p,\<sigma>,e)=s; (x,h,frs)=\<sigma> in Some (Intg (int (length frs))))"

evalE_Num:
"evalE \<Pi> s (Num e1 no e2) = liftI (numop no, evalE \<Pi> s e1, evalE \<Pi> s e2)"

evalE_Rel:
"evalE \<Pi> s (Rel e1 ro e2) = liftR (relop ro, evalE \<Pi> s e1, evalE \<Pi> s e2)"

evalE_Ite:
"evalE \<Pi> s (Ite b t e) = (if the_Bool (evalE \<Pi> s b) 
                          then evalE \<Pi> s t else evalE \<Pi> s e)"
                                              
evalE_Eq:
"evalE \<Pi> s (Eq e1 e2) = Some (Bool (evalE \<Pi> s e1 = (evalE \<Pi> s e2)))" 

evalE_Neg:
"evalE \<Pi> s (Neg ex) = Some (Bool (\<not> (the_Bool (evalE \<Pi> s ex))))" 

evalE_Imp:
"evalE \<Pi> s (Imp e1 e2) = Some (Bool (the_Bool (evalE \<Pi> s e1) \<longrightarrow> the_Bool (evalE \<Pi> s e2)))"

evalE_And:
"evalE \<Pi> s (And exs) = Some (Bool (list_all (\<lambda>v. the_Bool v) (evalEs \<Pi> s exs)))"

evalE_Forall:
"evalE \<Pi> s (Forall v ex) = (let (p,\<sigma>,e)=s in Some (Bool (\<forall>v'. the_Bool (evalE \<Pi> (p,\<sigma>,e\<lparr>lv:=((lv e)(v:=v'))\<rparr>) ex))))"

evalE_Ty:
"evalE \<Pi> s (Ty ex tp) =  Some (Bool (case (evalE \<Pi> s ex) of None \<Rightarrow> False
                          | Some v \<Rightarrow> (case v            
                           of Unit \<Rightarrow> tp= Void 
                           | Null \<Rightarrow> tp= NT 
                           | Bool b \<Rightarrow> tp= Boolean 
                           | Intg i \<Rightarrow> tp= Integer
                           | Addr a \<Rightarrow> (let (p,\<sigma>,e)=s; (x,hp,frs)=\<sigma> in (case (hp a) of None \<Rightarrow> False | Some ob \<Rightarrow> tp= obj_ty ob)))))"

evalE_Pos:
"evalE \<Pi> s (Pos p) = Some (Bool ((p = fst s) \<and> (let (p,\<sigma>,e)=s; (x,h,frs)=\<sigma> in (case frs of [] \<Rightarrow> False | fr#frs' \<Rightarrow> (let (st,rg,ps)=fr in p = ps)) \<and> x = None)
                                       \<and> callers_sysinv (\<Pi>,s)))"

evalE_Call:
"evalE \<Pi> s (Call ex) = (let (p,\<sigma>,e)=s; (x,h,frs)=\<sigma> 
                              in (if length frs \<le> 1 then None
                                  else evalE \<Pi> (callstate s) ex))"

evalE_Catch:
"evalE \<Pi> s (Catch X ex) = (let (p,\<sigma>,e)=s; (x,h,frs)=\<sigma> 
                              in (if length frs \<le> 1 then None
                                  else evalE \<Pi> (catchstate (fst \<Pi>,X,s)) ex))"


lemma new_Addr_dom:
"\<And>h h'. (Map.dom h) = (Map.dom h') \<Longrightarrow> new_Addr h  = new_Addr h'"
(*<*)
apply (simp add: new_Addr_def dom_def)
apply (rule conjI, rule impI)+
apply (rule eqSOME)
apply (rule allI)
apply blast

apply blast
apply (rule impI)
apply (rule allI)
apply(erule_tac x="a" in allE)
apply (drule_tac x="a" in eqset_imp_iff)
apply (subgoal_tac "a \<in> Map.dom h")
 prefer 2
 apply (erule exE)+
 apply (rule domI)
 apply simp
apply (subgoal_tac "a \<in> Map.dom h'")
 prefer 2
 apply simp
apply (drule_tac m="h'" in domD)
apply fastsimp
done
(*>*)


subsection {* Lemmas on expression evaluation *}


lemma evalNewA_dom:
"\<And>h h'. (Map.dom h) = (Map.dom h') \<Longrightarrow> evalNewA h n = evalNewA h' n"
(*<*)
apply (induct n)
apply simp
apply (drule new_Addr_dom)
apply simp

apply simp
apply (frule new_Addr_dom)
apply atomize
apply (erule_tac x="(h(the (new_Addr h) \<mapsto> arbitrary))" in allE)
apply (erule_tac x="(h'(the (new_Addr h') \<mapsto> arbitrary))" in allE)
apply simp
done
(*>*)


lemma evalEs_evalE:
"ex \<in> set exs \<Longrightarrow> evalE \<Pi> s ex \<in> set (evalEs \<Pi> s exs)" 
(*<*)
apply (induct exs)
apply simp+
apply (erule disjE)
apply simp
apply simp
done
(*>*)


lemma evalE_And_rec:
"evalE \<Pi> s (And (ex#es)) = Some (Bool (the_Bool (evalE \<Pi> s ex) \<and> the_Bool (evalE \<Pi> s (And es))))"
(*<*)
apply (induct_tac es)
apply (simp add: the_Bool_def)

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


lemma evalE_And:
"evalE \<Pi> s (And es) = Some (Bool (\<forall>ex\<in>set es. the_Bool (evalE \<Pi> s ex)))"
(*<*)
apply (induct_tac es)
apply simp

apply (simp only: evalE_And_rec)
apply (simp add: the_Bool_def)
done
(*>*)


lemma subExpr_getPosEx:
"Pos x \<in> set (subExpr Q) \<Longrightarrow> x \<in> set (getPosEx Q)"
(*<*)
apply (erule rev_mp)
apply (rule expr_induct')
apply (simp add: subExpr_def getPosEx_def | fastsimp)+
done
(*>*)


lemma evalEs_map:
"evalEs \<Pi> s exs = map (evalE \<Pi> s) exs"
(*<*)
apply (induct_tac exs)
apply simp
apply simp
done
(*>*)

subsection {* Validity *}


constdefs 
valid::"jbc_prog \<Rightarrow> jbc_state \<Rightarrow> expr \<Rightarrow> bool" ("(_,_ \<Turnstile>  _)" [61,61,60] 60)
"valid \<Pi> s ex \<equiv> (evalE \<Pi> s ex = Some (Bool True))"


subsection {* Provability  *}

text {* Instead of explicit derivation rules, we reuse Isabelle/HOL's
inference rules by defining provability as a HOL formula. We directly
connect provability with validity. *}


consts
safeP::"jbc_prog \<Rightarrow> jbc_state set"  ("safe\<^sub>\<box>_" [70])

inductive "safeP \<Pi>"
intros
init: "\<lbrakk> s \<in> (initS \<Pi>)  \<rbrakk> \<Longrightarrow> s \<in> (safeP \<Pi>)"
step: "\<lbrakk> s \<in> (safeP \<Pi>);  (s,s') \<in> (effS \<Pi>) ;
        \<Pi>,s \<Turnstile> (safeF \<Pi> (fst s)); \<forall>a. anF \<Pi> (fst s) = Some a \<longrightarrow> \<Pi>,s \<Turnstile> a;
        \<Pi>,s' \<Turnstile> (safeF \<Pi> (fst s')); \<forall>a'. anF \<Pi> (fst s') = Some a' \<longrightarrow> \<Pi>,s' \<Turnstile> a' \<rbrakk> 
\<Longrightarrow> s' \<in> (safeP \<Pi>)"


consts
ReachablesAn::"jbc_prog \<Rightarrow> jbc_state set"

inductive "ReachablesAn \<Pi>"
intros
init: "\<lbrakk> s \<in> (initS \<Pi>)  \<rbrakk> \<Longrightarrow> s \<in> (ReachablesAn \<Pi>)"
step: "\<lbrakk> s \<in> (ReachablesAn \<Pi>);  (s,s') \<in> (effS \<Pi>) ;
        \<Pi>,s \<Turnstile> aF \<Pi> (fst s); \<Pi>,s' \<Turnstile> aF \<Pi> (fst s') \<rbrakk> 
\<Longrightarrow> s' \<in> (ReachablesAn \<Pi>)"


constdefs 
deriv ::    "jbc_prog \<Rightarrow> expr list \<Rightarrow> expr \<Rightarrow> bool" ("(_,_ \<turnstile> _)" [61,60,60] 60)
"\<Pi>,A \<turnstile> f \<equiv> (\<forall>s. \<Pi>,s \<Turnstile> Imp (And A) f)"


constdefs
provable :: "jbc_prog \<Rightarrow> expr \<Rightarrow> bool" ("(_ \<turnstile> _)" [61,60] 60)
"\<Pi> \<turnstile> f \<equiv> \<Pi>,[] \<turnstile> f"

lemma provable_conv:
"\<Pi> \<turnstile> f = (\<forall> s. \<Pi>,s \<Turnstile> f)"
(*<*)
by (simp add: provable_def deriv_def valid_def the_Bool_def)
(*>*)


lemma safeP_effS:
"(p,\<sigma>,e) \<in> safeP \<Pi> \<Longrightarrow> \<exists> p0 \<sigma>0 e0. (p0,\<sigma>0,e0) \<in> (initS \<Pi>) \<and> ((p0,\<sigma>0,e0),(p,\<sigma>,e)) \<in> (effS \<Pi>)\<^sup>*"
(*<*)
apply (erule safeP.induct)
apply fastsimp

apply (erule exE)+
apply (rule_tac x="p0" in exI)
apply (rule_tac x="\<sigma>0" in exI)
apply (rule_tac x="e0" in exI)
apply (rule conjI)
apply simp

apply (rule_tac b="s" in rtrancl_into_rtrancl)
apply simp

apply simp
done
(*>*)


lemma safeP_Reachables: 
"s \<in> safeP \<Pi> \<Longrightarrow> s \<in> Reachables \<Pi>"
(*<*)
apply (subgoal_tac "\<exists> p \<sigma> e. s = (p,\<sigma>,e)")
 prefer 2
 apply (rule_tac x="fst s" in exI)
 apply (rule_tac x="fst (snd s)" in exI)
 apply (rule_tac x="snd (snd s)" in exI)
 apply simp
apply (erule exE)+
apply (simp only:)
apply (drule safeP_effS)
apply (simp add: effS_Reachables)
done
(*>*)


theorem correctSafetyLogic:
"\<Pi> \<turnstile> f \<Longrightarrow> \<Pi>,s \<Turnstile> f"
(*<*)
by (simp only: deriv_def provable_conv valid_def the_Bool_def)
(*>*)


theorem completeSafetyLogic:
"\<forall>s. \<Pi>,s \<Turnstile> f \<Longrightarrow> \<Pi> \<turnstile> f"
(*<*)
by (simp add: provable_conv deriv_def valid_def)
(*>*)


constdefs isSafe::"jbc_prog \<Rightarrow> bool"
"isSafe \<Pi> \<equiv> (\<forall> s \<in> Reachables \<Pi>. \<Pi>,s \<Turnstile> safeF \<Pi> (fst s))"


subsection {* Theorems about safe states. *}


lemma initF_startstate:
"ipc \<Pi> mem (domC \<Pi>) \<Longrightarrow> (let \<sigma>=start_state (fst \<Pi>) (fst (ipc \<Pi>)) (fst (snd (ipc \<Pi>))) 
  in \<Pi>,(ipc \<Pi>,\<sigma>,e\<lparr>cs:=[]\<rparr>) \<Turnstile> (initF \<Pi>))"
(*<*)
apply (simp add: Let_def start_state_def initF_def sys_xcptns_def addr_of_sys_xcpt_def 
the_Bool_def not_none_def OutOfMemory_def ClassCast_def NullPointer_def valid_def 
evalE_evalEs.simps evalEs_map ipc_def split_def start_heap_def blank_def set_mem_eq 
list_all_iff)
done
(*>*)


lemma initS_initF:
assumes ipc_domC: "ipc \<Pi> mem (domC \<Pi>)"
assumes s_initS: "s \<in> initS \<Pi>"
shows "\<Pi>,s \<Turnstile> initF \<Pi>"
(*<*)
proof -
obtain p \<sigma> e where s_def: "s = (p,\<sigma>,e)"
 by (cases "s")
from s_def s_initS
have e_cs: "e\<lparr>cs:=[]\<rparr> = e"
 by (simp add: initS_def)

from ipc_domC s_initS s_def e_cs
show ?thesis
  apply -
  apply (drule_tac e="snd (snd s)" in initF_startstate)
  apply (simp add: Let_def split_def)
  apply (simp add: initS_def)
  done
qed
(*>*)


lemma initF_frs:
"\<Pi>, (p,(x,hp,frs),e) \<Turnstile> initF \<Pi> \<Longrightarrow> length frs = 1"
(*<*)
apply (simp add: Let_def start_state_def initF_def sys_xcptns_def addr_of_sys_xcpt_def the_Bool_def
OutOfMemory_def ClassCast_def NullPointer_def valid_def evalE_evalEs.simps ipc_def split_def start_heap_def blank_def)
done
(*>*)


lemma initS_frs:
"(p,(x,hp,frs),e) \<in> initS \<Pi> \<Longrightarrow> length frs = 1"
(*<*)
apply (simp add: Let_def start_state_def initS_def sys_xcptns_def addr_of_sys_xcpt_def
OutOfMemory_def ClassCast_def NullPointer_def valid_def evalE_evalEs.simps ipc_def split_def start_heap_def blank_def)
done
(*>*)


lemma frameCnt_callstate:
"\<And>s. frameCnt s = frameCnt (callstate s) \<Longrightarrow> s = callstate s"
(*<*)
apply (simp add: split_paired_all)
apply (erule rev_mp)+
apply (induct_tac "ba")
apply simp
apply (simp add: frameCnt_def split_def)
apply (case_tac list)
apply simp
apply (simp add: split_paired_all)
done
(*>*)


consts callstates::"jbc_state \<Rightarrow> jbc_state set"

inductive "callstates s"
intros
init: "(callstate s) \<in> (callstates s)"
step: "s' \<in> (callstates s) \<Longrightarrow> (callstate s') \<in> (callstates s)"

lemma callstates_union:
"callstates s = ({callstate s} \<union> (callstates (callstate s)))"
(*<*)
apply (rule set_ext)
apply (rule iffI)
apply (erule callstates.induct)
apply simp
apply simp
apply (erule disjE)
apply (rule disjI2)
apply simp
apply (rule callstates.init)
apply (rule disjI2)
apply (rule callstates.step)
apply assumption

apply simp
apply (case_tac "x = callstate s")
apply simp
apply (rule callstates.init)
apply simp
apply (erule callstates.induct)
apply (subgoal_tac "callstate s \<in> callstates s")
 prefer 2
 apply (rule callstates.init)
apply (rule callstates.step)
apply assumption

apply (rule callstates.step)
apply assumption
done
(*>*)


lemma catchstate_callstates:
"\<And>s. catchstate(P,X,s) \<in> (callstates s)"
(*<*)
apply (subgoal_tac "\<exists>p x h frs e. s=(p,(x,h,frs),e)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply simp
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch5)
apply (rule allI)
apply (induct_tac frs)
apply (rule allI)+
apply (subgoal_tac "catchstate (P, X, p, (x, h, []), e) = callstate (p, (x, h, []), e)")
 prefer 2
 apply simp
apply (simp only:)
apply (rule impI)
apply (rule callstates.init)

apply (rule allI| rule impI)+
apply (case_tac list)
apply simp
apply (subgoal_tac "callstate (p, (x, h, [a]), e) = (p, (x, h, [a]), e)")
 prefer 2
 apply simp
apply (erule_tac V="s = ?P" in thin_rl)
apply (erule_tac t="(p, (x, h, [a]), e)" and P="\<lambda>t. t \<in> callstates (p, (x, h, [a]), e)" in subst)  
apply (rule callstates.init)
apply (subst callstates_union)
apply (simp add: split_paired_all)
done
(*>*)


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


lemma callstate_idem_callstates:
"callstate s = s \<Longrightarrow> callstates s = {s}"
(*<*)
apply (rule set_ext)
apply (rule iffI)
apply simp
apply (erule callstates.induct)
apply simp
apply simp
apply (subgoal_tac "callstate s = x")
 prefer 2
 apply simp
apply (simp only:)
apply (subgoal_tac "callstate s \<in> callstates s") 
 prefer 2
 apply (rule callstates.init)
apply simp
done
(*>*)


lemma callstates_subset:
"s' \<in> callstates s \<Longrightarrow> callstates s' \<subseteq> callstates s"
(*<*)
apply (erule callstates.induct)
apply (cut_tac s="s" in callstates_union)
apply simp
apply (subgoal_tac "callstates s' = {callstate s'} \<union> callstates (callstate s')")
 prefer 2
 apply (rule callstates_union)
apply simp
done
(*>*)


lemma callstates_frs:
"\<And> fr frs fr' frs' p e e' x h. \<lbrakk> frs = pre @ (fr'#frs'); 
  e' = e\<lparr>cs:= drop (length pre) (cs e)\<rparr> \<rbrakk> \<Longrightarrow>
(snd (snd fr'),(None,hd (cs e'),fr'#frs'),e'\<lparr>cs:= tl (cs e')\<rparr>) \<in> 
callstates (p,(x,h,fr#frs),e)"
(*<*)
apply (induct pre)
apply simp
apply (subgoal_tac "(snd (snd fr'), (None, hd (cs e), fr' # frs'), e\<lparr>cs := tl (cs e)\<rparr>) = callstate (p, (x, h, fr # fr' # frs'), e)")
 prefer 2
 apply (simp add: split_paired_all)
apply (simp only: )
apply (rule callstates.init)
apply atomize
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 only:)
apply (subst callstates_union)
apply (simp (no_asm_simp) add: callstate.simps)
apply (erule_tac x="a" in allE)
apply (erule_tac x="pre @ fr' # frs'" in allE)
apply (erule_tac x="fr'" in allE)
apply (erule_tac x="frs'" in allE)
apply (erule_tac x="p_a" in allE)
apply (erule_tac x="e\<lparr>cs:= tl (cs e)\<rparr>" in allE)
apply (erule_tac x="e\<lparr>cs:= drop (Suc (length pre)) (cs e)\<rparr>" in allE)
apply (erule_tac x="None" in allE)
apply (erule_tac x="hd (cs e)" in allE)
apply (simp add: tl_drop drop_drop)
done
(*>*)


lemma callstates_eq:
"\<And> s s' p x h fr frs e p' x' h' fr'. \<lbrakk> s=(p,(x,h,fr#frs),e); s'=(p',(x',h',fr'#frs),e); frs \<noteq> [] \<rbrakk> \<Longrightarrow> callstates s = callstates s'"
(*<*)
apply (rule set_ext)
apply (rule iffI)
apply (erule callstates.induct)
apply (subgoal_tac "callstates s' = {callstate s'} \<union> callstates (callstate s')")
 prefer 2
 apply (rule callstates_union)
apply (case_tac "frs")
apply (simp add: split_paired_all)
apply (simp add: split_paired_all)

apply (rule callstates.step)
apply assumption

apply (erule callstates.induct)
apply (subgoal_tac "callstates s = {callstate s} \<union> callstates (callstate s)")
 prefer 2
 apply (rule callstates_union)
apply (case_tac "frs")
apply (simp add: split_paired_all)
apply (simp add: split_paired_all)

apply (rule callstates.step)
apply assumption
done
(*>*)


lemma callstates_safeP:
assumes s_safeP: "s \<in> (safeP \<Pi>)"
shows "\<forall>s' \<in> (callstates s). s' \<in> (safeP \<Pi>)" using s_safeP
(*<*)
proof (induct rule: safeP.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_safeP: "s \<in> safeP \<Pi>"
  by (rule safeP.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_safeP callstate_s show ?case
    by (simp add: callstate_idem_callstates)

next
  case (step s s')
  assume s_safeP: "s \<in> safeP \<Pi>"
  assume callstates_s_safeP: "\<forall>s'\<in>callstates s. s' \<in> safe\<^sub>\<box>\<Pi>"
  assume s_s'_effS: "(s, s') \<in> effS \<Pi>"
  assume s_safeF: "\<Pi>,s \<Turnstile>  safeF \<Pi> (fst s)"
  assume s_anF: "\<forall>a. anF \<Pi> (fst s) = \<lfloor>a\<rfloor> \<longrightarrow> \<Pi>,s \<Turnstile>  a"
  assume s'_safeF: "\<Pi>,s' \<Turnstile>  safeF \<Pi> (fst s')"
  assume s'_anF: "\<forall>a'. anF \<Pi> (fst s') = \<lfloor>a'\<rfloor> \<longrightarrow> \<Pi>,s' \<Turnstile>  a'"
  have s'_safeP:"s' \<in> safeP \<Pi>"
    by (rule safeP.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 (rule ballI)
    fix sc 
    assume sc_callstates_s': "sc \<in> callstates s'" 
    show "sc \<in> safeP \<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'_safeP 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_safeP 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> safeP \<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'_safeP 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_safeP 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_safeP 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_safeP 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_safeP 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_safeP 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_safeP 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_safeP 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_safeP callst_s_s' sc_callstates_s' s_safeP
	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'_safeP 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_safeP
	  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_safeP callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp
	
      next
	case (IBin no)
	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_safeP 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_safeP 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_safeP 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_safeP 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_safeP 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_safeP:
"\<And> s. s \<in> (safeP \<Pi>) \<Longrightarrow> callstate s \<in> (safeP \<Pi>)"
(*<*)
apply (drule callstates_safeP)
apply (subgoal_tac "callstate s \<in> (callstates s)")
 prefer 2
 apply (rule callstates.init)
apply fastsimp
done
(*>*)


lemma catchstate_safeP:
"s \<in> safeP \<Pi> \<Longrightarrow> catchstate(fst \<Pi>,X,s) \<in> (safeP \<Pi>)"
(*<*)
apply (frule callstates_safeP)
apply (subgoal_tac "catchstate (fst \<Pi>, X, s) \<in> (callstates s)")
 prefer 2
 apply (rule catchstate_callstates)
apply fastsimp
done
(*>*)


lemma callstates_ReachablesAn:
assumes s_ReachablesAn: "s \<in> (ReachablesAn \<Pi>)"
shows "\<forall>s' \<in> (callstates s). s' \<in> (ReachablesAn \<Pi>)" using s_ReachablesAn
(*<*)
proof (induct rule: ReachablesAn.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 obtain s_ReachablesAn: "s \<in> ReachablesAn \<Pi>"
    apply -
    apply (drule ReachablesAn.init)
    apply simp
    done

  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_ReachablesAn callstate_s show ?case
    by (simp add: callstate_idem_callstates)

next

  case (step s s')
  assume s_ReachablesAn: "s \<in> ReachablesAn \<Pi>"
  assume callstates_s_ReachablesAn: "\<forall>s'\<in>callstates s. s' \<in> ReachablesAn \<Pi>"
  assume s_s'_effS: "(s, s') \<in> effS \<Pi>"
  assume s_aF: "\<Pi>,s \<Turnstile> aF \<Pi> (fst s)"
  assume s'_aF: "\<Pi>,s' \<Turnstile>  aF \<Pi> (fst s')"
  have s'_ReachablesAn:"s' \<in> (ReachablesAn \<Pi>)"
    by (rule ReachablesAn.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 (rule ballI)
    fix sc 
    assume sc_callstates_s': "sc \<in> callstates s'" 
    show "sc \<in> ReachablesAn \<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'_ReachablesAn 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_ReachablesAn 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> ReachablesAn \<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'_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn callst_s_s' sc_callstates_s' s_ReachablesAn
	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'_ReachablesAn 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_ReachablesAn
	  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_ReachablesAn callst_s_s' sc_callstates_s'
	show ?thesis
	  by simp
	
      next
	case (IBin no)
	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_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn 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_ReachablesAn:
"\<And> s. s \<in> (ReachablesAn \<Pi>) \<Longrightarrow> callstate s \<in> (ReachablesAn \<Pi>)"
(*<*)
apply (drule callstates_ReachablesAn)
apply (subgoal_tac "callstate s \<in> (callstates s)")
 prefer 2
 apply (rule callstates.init)
apply fastsimp
done
(*>*)


lemma catchstate_ReachablesAn:
"s \<in> ReachablesAn \<Pi> \<Longrightarrow> catchstate(fst \<Pi>,X,s) \<in> (ReachablesAn \<Pi>)"
(*<*)
apply (frule callstates_ReachablesAn)
apply (subgoal_tac "catchstate (fst \<Pi>, X, s) \<in> (callstates s)")
 prefer 2
 apply (rule catchstate_callstates)
apply fastsimp
done
(*>*)


lemma ReachablesAn_Reachables:
"s \<in> ReachablesAn \<Pi> \<Longrightarrow> s \<in> Reachables \<Pi>"
(*<*)
apply (erule ReachablesAn.induct)
apply (rule Reachables.init)
apply simp

apply (rule_tac s="s" in Reachables.step)
apply simp

apply simp
done
(*>*)


lemma ReachablesAn_initS_aF:
"(p,\<sigma>,e) \<in> ReachablesAn \<Pi> \<Longrightarrow> (p,\<sigma>,e) \<in> initS \<Pi> \<or> \<Pi>,(p,\<sigma>,e) \<Turnstile> aF \<Pi> p" 
(*<*)
apply (erule ReachablesAn.elims)
apply simp
apply (drule_tac t="s'" in sym)
apply simp
done
(*>*)


lemma ReachablesAn_initF_aF:
"\<lbrakk> ipc \<Pi> mem (domC \<Pi>); (p,\<sigma>,e) \<in> ReachablesAn \<Pi> \<rbrakk> \<Longrightarrow> (\<Pi>,(p,\<sigma>,e) \<Turnstile> initF \<Pi>) \<or> (\<Pi>,(p,\<sigma>,e) \<Turnstile> aF \<Pi> p)"
(*<*)
apply (drule ReachablesAn_initS_aF)
apply (erule disjE)
apply (drule initS_initF)
apply assumption
apply simp

apply simp
done
(*>*)


constdefs assert :: "jbc_prog \<Rightarrow> pos \<Rightarrow> expr"
"assert \<Pi> p \<equiv> And [safeF \<Pi> p,(case anF \<Pi> p of None \<Rightarrow> TT | Some a \<Rightarrow> a)]"


lemma safeP_initS_assert:
"(p,\<sigma>,e) \<in> safeP \<Pi> \<Longrightarrow> (p,\<sigma>,e) \<in> initS \<Pi> \<or> \<Pi>,(p,\<sigma>,e) \<Turnstile> assert \<Pi> p" 
(*<*)
apply (erule safeP.elims)
apply simp
apply (drule_tac t="s'" in sym)
apply (simp add: assert_def)
apply (case_tac "anF \<Pi> p")
apply (simp add: valid_def the_Bool_def)
apply (simp add: valid_def the_Bool_def)
done
(*>*)


lemma safeP_initF_assert:
"\<lbrakk> ipc \<Pi> mem domC \<Pi>; (p,\<sigma>,e) \<in> safeP \<Pi> \<rbrakk> \<Longrightarrow> \<Pi>,(p,\<sigma>,e) \<Turnstile> initF \<Pi> \<or> \<Pi>,(p,\<sigma>,e) \<Turnstile> assert \<Pi> p" 
(*<*)
apply (drule safeP_initS_assert)
apply (erule disjE)
apply (drule initS_initF)
apply assumption
apply simp

apply simp
done
(*>*)


lemma callstate_lv:
"\<And> p \<sigma> e. callstate (p,\<sigma>,e\<lparr>lv:=lv'\<rparr>) = (let (p',\<sigma>',e') = callstate (p,\<sigma>,e) in (p',\<sigma>',e'\<lparr>lv:=lv'\<rparr>))"
(*<*)
apply (simp add: split_paired_all)
apply (induct_tac ba)
apply simp
apply (simp add: split_paired_all)
apply (case_tac "list")
apply simp
apply (simp add: split_paired_all)
done
(*>*)


lemma catchstate_lv:
"\<And> p \<sigma> e. catchstate (P,X,(p,\<sigma>,e\<lparr>lv:=lv'\<rparr>)) = (let (p',\<sigma>',e') = catchstate (P,X,(p,\<sigma>,e)) in (p',\<sigma>',e'\<lparr>lv:=lv'\<rparr>))"
(*<*)
apply (simp add: split_paired_all)
apply (simp only: atomize_all)
apply (rule forall_switch7)
apply (rule forall_switch7)
apply (rule allI)
apply (induct_tac b)
apply simp

apply (rule allI)+
apply (simp add: split_paired_all)
apply (case_tac "list")
apply simp
apply (simp (no_asm_simp) add: split_paired_all)
apply (rule impI)
apply (erule_tac x="e\<lparr>cs:=tl (cs e)\<rparr>" in allE)
apply (erule_tac x="ab" in allE)
apply (erule_tac x="ac" in allE)
apply (erule_tac x="b" in allE)
apply (erule_tac x="None" in allE)
apply (erule_tac x="hd (cs e)" in allE)
apply (subgoal_tac "e\<lparr>lv := lv', cs := tl (cs e)\<rparr> = e\<lparr>cs := tl (cs e),lv:=lv'\<rparr>")
 prefer 2
 apply simp
apply (simp only:)
done
(*>*)


lemma callstate_lv_inv:
"callstate (p,\<sigma>,e) = (p',\<sigma>',e') \<Longrightarrow> lv e = lv e'"
(*<*)
apply (subgoal_tac "callstate (p,\<sigma>,e) = callstate (p,\<sigma>,e\<lparr>lv:= lv e\<rparr>)")
 prefer 2
 apply (subgoal_tac "e\<lparr>lv:= lv e\<rparr> = e")
  prefer 2
  apply simp
 apply (simp only:)
apply (simp only:)
apply (simp only: callstate_lv)
apply (simp add: Let_def)
apply (drule_tac t="e'" in sym)
apply (subgoal_tac "lv e' = (lv (e'\<lparr>lv:= lv e\<rparr>))")
 prefer 2
 apply simp
apply simp
done
(*>*)


lemma catchstate_lv_inv:
"catchstate (P,X,(p,\<sigma>,e)) = (p',\<sigma>',e') \<Longrightarrow> lv e = lv e'"
(*<*)
apply (subgoal_tac "catchstate (P,X,(p,\<sigma>,e)) = catchstate (P,X,(p,\<sigma>,e\<lparr>lv:= lv e\<rparr>))")
 prefer 2
 apply (subgoal_tac "e\<lparr>lv:= lv e\<rparr> = e")
  prefer 2
  apply simp
 apply (simp only:)
apply (simp only:)
apply (simp only: catchstate_lv)
apply (simp add: Let_def)
apply (drule_tac t="e'" in sym)
apply (subgoal_tac "lv e' = (lv (e'\<lparr>lv:= lv e\<rparr>))")
 prefer 2
 apply simp
apply simp
done
(*>*)


lemma effS_lv:
"((p,\<sigma>,e),(p',\<sigma>',e')) \<in> effS \<Pi> \<Longrightarrow> (((p,\<sigma>,e\<lparr>lv:=lv'\<rparr>)),(p',\<sigma>',e'\<lparr>lv:=lv'\<rparr>)) \<in> effS \<Pi>"
(*<*)
apply (erule effS.induct)
apply (rule_tac P="P" and C="C" and M="M" and pc="pc" and stk="stk" 
       and loc="loc" and frs="frs" and h="h" and xa="xa" and i="i"
       and loc'="loc'" and frs'="frs'" and h'="h'" and bla="bla" in effS.expt)
 apply simp
 apply simp
 apply simp
 apply simp
 apply simp
 apply simp
 apply simp
 apply simp
 apply simp

apply (rule_tac P="P" and C="C" and M="M" and pc="pc" and stk="stk" 
       and loc="loc" and frs="frs" and h="h"and i="i" and h'="h'" and fr'="fr'" and frs'="frs'" in effS.nrml)
 apply simp+
done
(*>*)


lemma effS_lv_inv:
"((p,\<sigma>,e),(p',\<sigma>',e')) \<in> (effS \<Pi>) \<Longrightarrow> lv e = lv e'"
(*<*)
apply (erule effS.induct)
apply simp
apply simp
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> fst (snd (snd (snd fr))) = fst (snd (snd (snd (last pfx))))
      \<and> fst (snd (snd fr)) = fst (snd (snd (last pfx)))"
(*<*)
apply (induct frs)
apply simp
apply (simp add: split_def)
apply fastsimp
apply fastsimp
done
(*>*)


lemma find_handler_simp:
"find_handler ?P ?a ?h (?fr # ?frs) =
(let (stk, loc, C, M, pc) = ?fr
 in case JVMExceptions.match_ex_table ?P (cname_of ?h ?a) pc (ex_table_of ?P C M) of None \<Rightarrow> find_handler ?P ?a ?h ?frs
    | \<lfloor>pc_d\<rfloor> \<Rightarrow> (None, ?h, (Addr ?a # drop (length stk - snd pc_d) stk, loc, C, M, fst pc_d) # ?frs))"
(*<*)
apply simp
done
(*>*)

(*<*)
lemma [simp]: "(map (\<lambda>u. snd (snd u)) l) = (map (snd o snd) l)"
apply (induct l)
apply simp
apply simp
done
(*>*)

lemma safeP_state:
assumes s_safeP: "s \<in> safeP \<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> fst (snd (last (map (snd \<circ> snd) ((st,rg,(C,M,pc))#frs)) ))= fst (snd (ipc \<Pi>))"  using s_safeP
(*<*)
proof (induct rule: safeP.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_safeP: "s \<in> safeP \<Pi>"
  assume safeP_state_s: "\<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>))"
  assume s_s'_effS: "(s, s') \<in> effS \<Pi>"
  assume s_safeF: "\<Pi>,s \<Turnstile>  safeF \<Pi> (fst s)"
  assume s_anF: "\<forall>a. anF \<Pi> (fst s) = \<lfloor>a\<rfloor> \<longrightarrow> \<Pi>,s \<Turnstile>  a"
  assume s'_safeF: "\<Pi>,s' \<Turnstile>  safeF \<Pi> (fst s')"
  assume s'_anF: "\<forall>a'. anF \<Pi> (fst s') = \<lfloor>a'\<rfloor> \<longrightarrow> \<Pi>,s' \<Turnstile>  a'"
  have s'_safeP:"s' \<in> safeP \<Pi>"
    by (rule safeP.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 -
	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)
	by fastsimp
      from i_def[THEN sym] s_s'_def p_def p'_def sigma_def exec_i find_handler_s sigma'_def e'_def safeP_state_s
      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 (erule conjE)+
	apply (case_tac "frs'" rule: rev_cases)
	apply (simp add: last_append)
	apply (drule_tac t="list" and s="ys@[y]" in sym)
	apply simp

	apply simp
	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 safeP_state_s 
    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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 (drule_tac t="fst (snd (ipc \<Pi>))" 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 safeP_state':
"\<And> s. s \<in> safeP \<Pi> \<Longrightarrow> \<exists> p p' x h st rg frs e. s = (p,(x,h,(st,rg,p')#frs),e)"
(*<*)
apply (simp only: split_paired_all)
apply (erule safeP.elims)
apply (drule_tac t="s" in sym)
apply (simp add: initS_def start_state_def start_heap_def ipc_def split_def fst_conv snd_conv)

apply (erule effS.elims)
apply simp
apply fastsimp
apply fastsimp

apply simp
apply fastsimp
done
(*>*)


lemma the_Bool_simp:
"(the_Bool v) = (v = Some (Bool True))"
(*<*)
apply (case_tac "v")
apply (simp add: the_Bool_def)+
done
(*>*)


lemma the_Bool_True:
"the_Bool x \<Longrightarrow> x = Some (Bool True)"
(*<*)
apply (case_tac "x")
apply (simp add: the_Bool_def)+
done
(*>*)


lemma the_Bool_False:
"x \<noteq> Some (Bool True) \<Longrightarrow> the_Bool x = False"
(*<*)
apply (case_tac x)
apply (simp add: the_Bool_def)+
done
(*>*)


lemma evalE_And':
"evalE \<Pi> s (And es) = Some (Bool (list_all (\<lambda> ex. the_Bool (evalE \<Pi> s ex)) es))"
(*<*)
apply (simp add: evalE_And list_all_iff)
apply (rule iffI)
apply (rule ballI)
apply (erule_tac x="evalE \<Pi> s x" in ballE)
apply simp

apply (induct es rule: list.induct)
apply simp

apply simp
apply (case_tac "x = a")
apply simp

apply simp

apply (rule ballI)
apply (induct es rule: list.induct)
apply simp

apply simp
apply (case_tac "x = evalE \<Pi> s a")
apply simp
apply (simp add: the_Bool_def)
done
(*>*)


lemma evalE_Pos':
"the_Bool (evalE \<Pi> s (Pos p)) \<Longrightarrow> fst s = p"
(*<*)
apply (simp add: evalE_Pos the_Bool_def)
done
(*>*)


lemma in_evalEs_conv: "v \<in> set (evalEs \<Pi> s exs) \<Longrightarrow> \<exists> ex \<in> set exs. v = evalE \<Pi> s ex"
(*<*)
apply (induct exs rule: list.induct)
apply simp

apply simp
apply (case_tac "v = evalE \<Pi> s a")
apply simp

apply simp
done
(*>*)


lemma evalE_Or:
"evalE \<Pi> s (Or exs) = Some (Bool (\<exists> ex \<in> set exs. evalE \<Pi> s ex = Some (Bool True)))"
(*<*)
apply (induct exs rule: list.induct)
apply (simp add: Or_def the_Bool_def)

apply (simp add: Or_def the_Bool_def)
done
(*>*)


lemma evalE_none [simp]:
"evalE \<Pi> s none = None"
(*<*) by simp  (*>*)


constdefs subclasses::"jvm_prog \<Rightarrow> cname \<Rightarrow> cname list"
"subclasses P Cl \<equiv> filter (\<lambda> Cl'. P \<turnstile> Cl' \<preceq>\<^sup>* Cl) (map fst P)"


constdefs STy::"jvm_prog \<Rightarrow> expr \<Rightarrow> ty \<Rightarrow> expr"
"STy P ex tp \<equiv> (case tp 
 of Class Cl \<Rightarrow> Or (Ty ex NT#(map (\<lambda> Cl. Ty ex (Class Cl)) (subclasses P Cl)))
 | _ \<Rightarrow> Ty ex tp)"
   
lemma evalE_STy:
"evalE (P,An) s (STy P ex tp) = Some (Bool (\<exists> tp'. evalE (P,An) s (Ty ex tp') = Some (Bool True) \<and> P \<turnstile> tp' \<le> tp \<and> tp' \<in> types P))"
(*<*)
apply (simp add: STy_def)
apply (case_tac "tp")
apply simp+
--{* tp = Class list *}
apply (simp add: evalE_Or)
apply (rule allI | rule impI)+
apply (case_tac "a")
apply simp+
apply (rule iffI)
apply (case_tac "(\<lambda>(p, \<sigma>, e). (\<lambda>(x, hp, frs). case hp nat of None \<Rightarrow> False | \<lfloor>ob\<rfloor> \<Rightarrow> NT = obj_ty ob) \<sigma>) s")
apply (rule_tac x="NT" in exI)
apply simp

apply simp
apply (erule bexE)
apply (rule_tac x="Class exa" in exI)
apply (simp add: subclasses_def is_class_def class_def)
apply (case_tac "map_of P exa")
apply (simp add: map_of_eq_None_iff)

apply fastsimp

--{* iffI 2nd dir *}
apply (erule exE)
apply (erule conjE)+
apply (case_tac "tp'")
apply simp+
--{* tp' = NT *}
apply (rule disjI1)
apply (simp add: split_def obj_ty_def)

--{* tp' = Class lista *}
apply (rule disjI2)
apply (subgoal_tac "lista \<in> set (subclasses P list)")
 prefer 2
 apply (simp add: is_type_def subclasses_def is_class_def class_def)
 apply (erule exE)+
 apply (drule map_of_SomeD)
 apply (subgoal_tac "fst (lista, aa, ab, b) \<in> fst ` set P")
  prefer 2
  apply (rule_tac f="fst" and x="(lista, aa, ab, b)" in imageI)
  apply simp
 apply simp
apply (rule_tac x="lista" in bexI)
apply (simp add: split_def obj_ty_def split_paired_all)

apply assumption
done
(*>*)


section {* Auxiliary Lemmas *}


lemma env_upd_cs:
"e\<lparr>cs:=a, cs:=b\<rparr> = e\<lparr>cs:=b\<rparr>"
(*<*)
apply simp
done
(*>*)


lemma env_cs_upd_cs:
"cs (e\<lparr>cs:= b\<rparr>) = b"
(*<*)
apply simp
done
(*>*)


lemma env_upd_id:
"e\<lparr>cs:= cs e\<rparr> = e"
(*<*)
by simp
(*>*)

(*<*)
lemmas env_upd = env_upd_cs env_upd_id
(*>*)


lemma foldl_map_lookup:
"\<And> es. \<forall>ex\<in> set es. x\<noteq>Gf F C ex \<Longrightarrow> 
\<forall> mp'. (foldl (\<lambda>mp ex. (Gf F C ex, IF substE mp ex \<doteq> St (Suc 0) THEN St 0 
        ELSE Gf F C (substE mp ex)) # mp) mp' es) ? x = mp' ? x"
(*<*)
apply (erule rev_mp)
apply (induct_tac "es")
apply simp

apply (rule impI)
apply (rule allI)
apply simp
apply (erule conjE)+
apply (drule_tac t="x" in not_sym)
apply simp
done
(*>*)


lemma is_Addr'_conv:
"is_Addr' (h,v) = (\<exists> a. v = Addr a \<and> h a \<noteq> None)"
(*<*)
apply (case_tac "v")
apply simp+
done
(*>*)


lemma check_checkinstr:
"check P (None, h, (stk, loc, C, M, pc) # frs) \<Longrightarrow> check_instr ((instrs_of P C M)!pc) P h stk loc C M pc frs"
(*<*)
apply (simp add: check_def split_def)
done
(*>*)


lemma isIntg_conv:
"is_Intg a = (\<exists> i. a = Intg i)"
(*<*)
apply (case_tac a)
apply simp+
done
(*>*)


lemma evalEs_append:
"evalEs \<Pi> s (exs@exs') = evalEs \<Pi> s exs @ (evalEs \<Pi> s exs')"
(*<*)
apply (induct_tac exs)
apply simp
apply simp
done
(*>*)


end