header {* 
  \isaheader{succsF approximates real control flow.} 
*}

theory JBC_succsFcorrect = JBC_SysInv:


section {* Auxiliary Definitions and Lemmas *}


lemma catchstate_succsXpt:
"\<And> p ps h stk loc e. \<lbrakk> catchstate (P,X,(p,(None,h,(stk,loc,p)#frs),e)) = (p',(None,h',(stk',loc',p')#frs'),e');
 match_ex_table_e P X (snd (snd p')) (ex_table_of P (fst p') (fst (snd p'))) = Some en; 
  pc_h = fst (snd (snd (snd en))); X' = fst (snd (snd en));
 (fst p',fst (snd p'),pc_h) \<in> set (domC (P,An));
 callers_sysinv ((P,An),(p,(None,h,(stk,loc,p)#frs),e)); 
 (\<forall>q\<in>set (p#ps). match_ex_table_e P X (snd (snd q)) (ex_table_of P (fst q) (fst (snd q))) = None)
 \<rbrakk> \<Longrightarrow> 
 (\<exists>B. ((fst p',fst (snd p'),pc_h),B) \<in> set (succsXpt ((P,An),X,p#ps)) \<and> 
 (B=TT \<or> B=And [xcpt_cond (P,An) X (last (p#ps))] \<or> 
  B= And [Catch X' (aF (P,An) p'),Catch X (Pos p'), xcpt_cond (P,An) X (last (p#ps))]))"
(*<*)
apply (induct frs)
apply simp

apply atomize
apply (simp (no_asm_simp) split del: split_if split_if_asm)
apply (case_tac "length (domC (P, An)) \<le> Suc (length ps)")
apply (simp split del: split_if split_if_asm)
apply (rule_tac x="TT" in exI)
apply simp

apply (erule_tac P="callers_sysinv (?P,?s)" in rev_mp)
apply (simplesubst callers_sysinv.simps)
apply (simp (no_asm_simp) add: split_def simp_thms bool.cases list.cases del: succsXpt.simps callers_sysinv.simps split del: split_if split_if_asm)
(* apply (rule conjI) *)
apply (rule impI)+
apply (subgoal_tac "\<exists> st_a rg_a p_a. a = (st_a,rg_a,p_a)")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (erule exE)+
apply (erule_tac x="p_a" in allE )
apply (erule_tac x="p # ps" in allE)
apply (erule_tac x="hd (cs e)" in allE)
apply (erule_tac x="st_a" in allE)
apply (erule_tac x="rg_a" in allE)
apply (erule_tac x="e\<lparr>cs:=tl (cs e)\<rparr>" in allE)
apply (simp add: split_def del: succsXpt.simps callers_sysinv.simps split del: option.split option.split_asm split_if split_if_asm)
apply (case_tac "JVMExceptions.match_ex_table P X (snd (snd p_a)) (ex_table_of P (fst p_a) (fst (snd p_a)))")
apply (subgoal_tac "match_ex_table_e P X (snd (snd p_a)) (ex_table_of P (fst p_a) (fst (snd p_a))) = None")
 prefer 2
 apply (rule classical)
 apply simp
 apply (erule exE)+
 apply (drule_tac e="(aa, ab, ac, ad, b)" in match_ex_table_e_sim)
 apply simp
apply (simp del: catchstate.simps succsXpt.simps callers_sysinv.simps  split del: split_if split_if_asm)
apply (erule exE)+
apply (rule_tac x="B" in exI)
apply (rule conjI)
apply (rule_tac x="p_a" in bexI)
apply (erule conjE)+
apply assumption

apply (erule conjE)+
apply assumption

apply (erule conjE)+
apply assumption

--{* 1 subgoal *}
apply (frule_tac pc_h="aa" in match_ex_table_e_sim2)
apply (erule exE)
apply (simp del: catchstate.simps succsXpt.simps callers_sysinv.simps split del: option.split option.split_asm split_if split_if_asm)
apply (simp add: succsXpt.simps split del: option.split option.split_asm split_if split_if_asm)
apply (case_tac "length (domC (P, An)) \<le> Suc (Suc (length ps))")
apply (rule_tac x="TT" in exI)
apply (simp only: bool.cases simp_thms in_set_conv_decomp)
apply (erule exE)+
apply (rule_tac x="p'" in bexI)
apply fastsimp

apply (simp add: in_set_conv_decomp)

apply (simp only: list.cases bool.cases)
apply (rule_tac x="And [Catch X' (aF (P, An) p'),Catch X (Pos p'), xcpt_cond (P, An) X (if ps = [] then p else last ps)]" in exI)
apply (simp only: simp_thms)
apply (rule_tac x="p'" in bexI)
apply(simp add: Let_def split_def split del:  split_if split_if_asm)

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


lemma wf_match_ex_table_d:
"\<lbrakk> wf (P,An); (C,M) \<in> set (methodnames P); JVMExceptions.match_ex_table P X p (ex_table_of P C M) = Some (h,d)  \<rbrakk> \<Longrightarrow> d = 0"
(*<*)
apply (subgoal_tac "\<exists> et. (ex_table_of P C M) = et")
 prefer 2
 apply simp
apply (erule exE)+
apply (simp only:)
apply (subgoal_tac "set et \<subseteq> set (ex_table_of P C M)")
 prefer 2
 apply simp
apply (erule_tac V=" ex_table_of P C M = et" in thin_rl)
apply (erule_tac P="JVMExceptions.match_ex_table P X p et = \<lfloor>(h, d)\<rfloor>" in rev_mp)
apply (erule_tac P="set et \<subseteq> ?A" in rev_mp)
apply (induct_tac "et")
apply simp

apply (rule impI)+
apply simp
apply (case_tac "matches_ex_entry P X p a")
apply simp
apply (subgoal_tac "\<exists> fa ta ca ha da. a=(fa,ta,ca,ha,da)")
 prefer 2
 apply (simp (no_asm) add: split_paired_all)
apply (erule exE | erule conjE)+
apply simp
apply (drule wf_extable)
apply simp
apply simp
apply simp

apply simp
done
(*>*)


lemma findhandler_stk:
"\<And> p. \<lbrakk> wf \<Pi>; \<forall>p \<in> set (map (snd \<circ> snd) ((st',loc,p)#frs)). p \<in> set (domC \<Pi>);  find_handler (fst \<Pi>) xa h ((st',loc,p)#frs) = (None,h,fr'#frs') \<rbrakk> \<Longrightarrow> fst fr' = [Addr xa]"
(*<*)
apply (induct frs)
apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (subgoal_tac "\<exists> P An. \<Pi> = (P,An)")
 prefer 2
 apply (simp (no_asm) add: split_paired_all)
apply (erule exE)+
apply simp
apply (frule_tac P="P" and X="(cname_of h xa)" and p="snd (snd p)"  and C="fst p" and M="fst (snd p)" and h="fst a" and d="snd a" in wf_match_ex_table_d)
apply (simp add: domC_methodnames split_paired_all)
apply simp
apply simp

--{* Induction case *}
apply (simp add: split_def)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply (subgoal_tac "\<exists> P An. \<Pi> = (P,An)")
 prefer 2
 apply (simp (no_asm) add: split_paired_all)
apply (erule exE)+
apply (atomize)
apply (erule_tac  V="\<forall> p. ?P p" in thin_rl)
apply simp
apply (frule_tac P="P" and X="(cname_of h xa)" and p="(snd (snd (snd (snd a))))"  and C="(fst (snd (snd a)))" and M="(fst (snd (snd (snd a))))" and h="fst aa" and d="snd aa" in wf_match_ex_table_d)
apply (erule_tac P="snd (snd a) \<in> set (domC (P,An))" in rev_mp)
apply (erule thin_rl)+
apply (simp add: domC_methodnames split_paired_all)
apply simp
apply simp

apply atomize
apply (erule_tac  V="\<forall> p. ?P p" in thin_rl)
apply (erule conjE)+
apply (drule_tac t="fr'" in sym)
apply simp
apply (subgoal_tac "\<exists> P An. \<Pi> = (P,An)")
 prefer 2
 apply (simp (no_asm) add: split_paired_all)
apply (erule exE)+
apply simp
apply (frule_tac P="P" and X="(cname_of h xa)" and p="(snd (snd p))"  and C=" (fst p)" and M="(fst (snd p))" and h="fst aa" and d="snd aa" in wf_match_ex_table_d)
apply (simp add: domC_methodnames split_paired_all)
apply simp
apply simp
done
(*>*)


lemma catchstate_Invoke:
"\<And> s p e h fr fr'. \<lbrakk> wf \<Pi>; s=(p,(None,h,fr#fr'#frs),e); s \<in> Reachables \<Pi> \<rbrakk>\<Longrightarrow> (\<exists>M n. cmd \<Pi> (fst (catchstate (P,X,s))) = Some (Invoke M n))"
(*<*)
apply (induct frs)
apply (frule callers_sysinv_Reachables)
apply simp
apply (subgoal_tac "\<exists>st_fr rg_fr p_fr. fr = (st_fr,rg_fr,p_fr)")
 prefer 2
 apply fastsimp
apply (subgoal_tac "\<exists>st_fr' rg_fr' p_fr'. fr' = (st_fr',rg_fr',p_fr')")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add: split_def)
apply (case_tac "match_ex_table P X (snd (snd p_fr')) (ex_table_of P (fst p_fr') (fst (snd p_fr'))) = None")
apply (simp add: callers_def)
apply (case_tac "cmd \<Pi> p_fr'")
apply simp+
apply (case_tac "a")
apply simp+

--{* case:  matchextable P X (snd (snd pfr')) (ex_table_of P (fst pfr') (fst (snd pfr'))) = Some a *}

apply (simp add: callers_def)
apply (case_tac "cmd \<Pi> p_fr'")
apply simp+
apply (case_tac "aa")
apply simp+


--{* induction case *}
apply atomize
apply (frule callers_sysinv_Reachables)
apply simp
apply (subgoal_tac "\<exists>st_fr rg_fr p_fr. fr = (st_fr,rg_fr,p_fr)")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (subgoal_tac "\<exists>st_fr' rg_fr' p_fr'. fr' = (st_fr',rg_fr',p_fr')")
 prefer 2
 apply (erule thin_rl)+
 apply fastsimp
apply (erule exE)+
apply (simp only:)
apply (erule_tac P="callers_sysinv (?P,?s)" in rev_mp)
apply (simplesubst callers_sysinv.simps)
apply (simp (no_asm_simp) add: split_def del: callers_sysinv.simps)
apply (rule conjI)
apply (rule impI)+
apply (erule_tac x="(p_fr', (None, hd (cs e), (st_fr', rg_fr', p_fr') # a # frs), e\<lparr>cs := tl (cs e)\<rparr>)" in allE)
apply (erule_tac x="p_fr'" in allE)
apply (erule_tac x=" e\<lparr>cs := tl (cs e)\<rparr>" in allE)
apply (erule_tac x="hd (cs e)" in allE)
apply (erule_tac x="fr'" in allE)
apply (erule_tac x="a" in allE)
apply (subgoal_tac "callstate s \<in> Reachables \<Pi>")
 prefer 2
 apply (rule callstate_Reachables)
 apply simp
apply simp

apply (rule impI)+
apply (erule_tac V="\<forall>s. ?P s" in thin_rl)
apply (simp add: callers_def)
apply (case_tac "cmd \<Pi> p_fr'")
apply simp

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


lemma sys_xcpt_Reachables:
"\<And> s p x h frs e. \<lbrakk> s=(p,(x,h,frs),e); s \<in> Reachables \<Pi>; C \<in> sys_xcpts \<rbrakk> \<Longrightarrow> (fst (the (h (addr_of_sys_xcpt C)))) = C"
(*<*)
apply (drule inv_ExTys_Reachable)
apply (simp add: inv_ExTys_def sys_xcpts_def)
apply (erule disjE | simp add: obj_ty_def)+
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 obtain s_Reachables: "s \<in> Reachables \<Pi>"
    apply -
    apply (drule Reachables.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_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 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 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_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 catchstate_Reachables:
"s \<in> Reachables \<Pi> \<Longrightarrow> catchstate(fst \<Pi>,X,s) \<in> (Reachables \<Pi>)"
(*<*)
apply (frule callstates_Reachables)
apply (subgoal_tac "catchstate (fst \<Pi>, X, s) \<in> (callstates s)")
 prefer 2
 apply (rule catchstate_callstates)
apply fastsimp
done
(*>*)

lemma match_ex_table_e_sim3:
"(match_ex_table_e P C pc et = None) = (JVMExceptions.match_ex_table P C pc et = None)"
apply (induct et)
apply simp

apply simp
done


lemma match_ex_table_e_matches_ex_entry:
"match_ex_table_e P C pc et = Some e \<Longrightarrow> matches_ex_entry P C pc e"
apply (induct et)
apply simp
apply (simp split add: split_if_asm)
done

lemma match_ex_table_e_Some_X_X':
"\<lbrakk> match_ex_table_e P X pc et = Some (f,t,X',pch,d) \<rbrakk> \<Longrightarrow> match_ex_table_e P X' pc et = Some (f,t,X',pch,d)"
apply (induct et)
apply simp

apply (simp add: matches_ex_entry_def split_def split add: split_if_asm)
apply (rule impI)
apply (erule conjE)+
apply simp
apply (drule match_ex_table_e_matches_ex_entry)
apply (drule match_ex_table_e_matches_ex_entry)
apply (simp add: matches_ex_entry_def)
apply (subgoal_tac "P \<turnstile> X \<preceq>\<^sup>* fst (snd (snd a))")
 prefer 2
 apply (rule_tac b="X'" in rtrancl_trans)
 apply simp
 apply simp
apply simp
done

lemma match_ex_table_e_None_X_X':
"\<lbrakk> match_ex_table_e P X pc et = None; P \<turnstile> X \<preceq>\<^sup>* X' \<rbrakk> \<Longrightarrow> match_ex_table_e P X' pc et = None"
apply (induct et)
apply simp

apply (simp add: matches_ex_entry_def split_def split add: split_if_asm)
apply (rule impI)+
apply simp
apply (rule classical)
apply (subgoal_tac "P \<turnstile> X \<preceq>\<^sup>* fst (snd (snd a))")
 prefer 2
 apply (rule_tac b="X'" in rtrancl_trans)
 apply simp
 apply simp
apply simp
done

lemma catchstate_X_X':
assumes sigma_def: "\<sigma> = (None, h, (stk, loc, p) # frs)"
assumes p'_def: "p' = (C',M',pc')"
assumes \<sigma>'_def: "\<sigma>' = (None, h', (stk', loc', p') # frs')"
assumes catchstate_X: "catchstate (P,X,(p,\<sigma>,e)) = (p',\<sigma>',e')"
assumes match_ex_table_e_pc': "match_ex_table_e P X pc' (ex_table_of P C' M') = Some (f,t,X',pch,d)"
shows  "catchstate (P, X', (p, \<sigma> , e)) = (p',\<sigma>',e')"
proof -
from match_ex_table_e_pc' 
have X_subcls_X': "P \<turnstile> X \<preceq>\<^sup>* X'"
  apply -
  apply (drule match_ex_table_e_matches_ex_entry)
  apply (simp add: matches_ex_entry_def)
  done

have aux: "\<forall> \<sigma> stk loc (p::pos) (h::heap) (e::env). \<sigma> = (None,h,(stk,loc,p)#frs) \<longrightarrow>  
          catchstate (P,X,(p,\<sigma>,e)) = (p',\<sigma>',e') \<longrightarrow> 
          catchstate (P,X',(p,\<sigma>,e)) = (p',\<sigma>',e')" 
  proof (induct frs, intro allI impI)
    case Nil
    fix \<sigma> stk loc p h e
    assume sigma_def: "(\<sigma>:: jvm_state) = (None, h, [((stk::val list), (loc::val list), (p::pos))])"
    assume catchstate_X: "catchstate (P, X, (p, \<sigma>, e)) = (p', \<sigma>', e')"
    from sigma_def catchstate_X
    show "catchstate (P, X', (p, \<sigma>, e)) = (p', \<sigma>', e')"
      by fastsimp

  next
    
    case Cons
    fix fr frss
    assume hyp: "\<forall>\<sigma> stk loc p h e.
               \<sigma> = (None, h, (stk, loc, p) # frss) \<longrightarrow>
               catchstate (P, X, p, \<sigma>, e) = (p', \<sigma>', e') \<longrightarrow> catchstate (P, X', p, \<sigma>, e) = (p', \<sigma>', e')"
    show "\<forall>\<sigma> stk loc p h e.
               \<sigma> = (None, h, (stk, loc, p) # fr # frss) \<longrightarrow>
               catchstate (P, X, p, \<sigma>, e) = (p', \<sigma>', e') \<longrightarrow> catchstate (P, X', p, \<sigma>, e) = (p', \<sigma>', e')"
      proof (intro allI impI)
	fix \<sigma> stk loc p h e
	assume sigma_def: "(\<sigma>::jvm_state) = (None, h, ((stk::val list), (loc::val list), (p::pos)) # fr # frss)"
	assume catchstate_X: "catchstate (P, X, p, \<sigma>, e) = (p', \<sigma>', e')"
	obtain fr_stk fr_loc fr_p
	  where fr_def: "fr = (fr_stk,fr_loc,fr_p)"
	  by (cases fr)
	obtain fr_C fr_M fr_pc
	  where fr_p_def: "fr_p = (fr_C,fr_M,fr_pc)"
	  by (cases "fr_p")
	show "catchstate (P, X', p, \<sigma>, e) = (p', \<sigma>', e')"
	  proof (cases "match_ex_table_e P X fr_pc (ex_table_of P fr_C fr_M)")
	   case None
	   note X_None = None
	   from X_None X_subcls_X'
	   have X'_None: 
	     "match_ex_table_e P X' fr_pc (ex_table_of P fr_C fr_M) = None"
	     by (rule match_ex_table_e_None_X_X')

	   from X_None X'_None catchstate_X fr_def fr_p_def sigma_def
	   show ?thesis
	     apply -
	     apply (simp add: match_ex_table_e_sim3)
	     apply (cut_tac hyp)
	     apply (erule_tac x="(None,hd (cs e),(fr_stk, fr_loc, fr_C, fr_M, fr_pc) # frss)" in allE)
	     apply (erule_tac x="fr_stk" in allE)
	     apply (erule_tac x="fr_loc" in allE)
	     apply (erule_tac x="fr_p" 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
	     done

	 next

	   case Some

	   fix en'
	   assume X_en': "match_ex_table_e P X fr_pc (ex_table_of P fr_C fr_M) = \<lfloor>en'\<rfloor>"
	   show "catchstate (P, X', p, \<sigma>, e) = (p', \<sigma>', e')"
	     proof -

	       from X_en' 
	       obtain pcd 
		 where X_pcd: "JVMExceptions.match_ex_table P X fr_pc (ex_table_of P fr_C fr_M) = \<lfloor>pcd\<rfloor>"
		 and pcd_def: "pcd = snd (snd (snd en'))"
		 apply -
		 apply (drule match_ex_table_e_sim)
		 by fastsimp
		 
	       from X_en' X_pcd pcd_def sigma_def catchstate_X fr_def fr_p_def
                    \<sigma>'_def p'_def match_ex_table_e_pc'
	       show "?thesis"
		 apply -
		 apply (simp split del: option.split_asm)
		 apply (drule_tac t="en'" in sym)
		 apply simp
		 apply (drule match_ex_table_e_Some_X_X')
		 apply (drule match_ex_table_e_sim)
		 apply simp
		 done
	     qed
	   qed
	 qed
       qed
from aux catchstate_X sigma_def
show ?thesis
  apply -
  apply (erule_tac x="\<sigma>" in allE)
  apply (erule_tac x="stk" in allE)
  apply (erule_tac x="loc" in allE)
  apply (erule_tac x="p" in allE)
  apply (erule_tac x="h" in allE)
  apply (erule_tac x="e" in allE)
  by fastsimp
qed
  
lemma findhandler_succsXpt:
assumes wf_Pi: "wf \<Pi>"
assumes s_ReachablesAn:"s \<in> ReachablesAn \<Pi>"
assumes s_def: "(s::jbc_state) = (p,(None,h,(stk,loc,p)#frs),e)"
assumes p_def: " p = (C,M,pc)"
assumes cmd_p: "cmd \<Pi> p = Some i"
assumes check_s: "check (fst \<Pi>) (None,h,(stk,loc,p)#frs)"
assumes exec_i: "exec_instr i (fst \<Pi>) h stk loc C M pc frs = (Some xa,h',frs'')"
assumes find_handler_s: "find_handler (fst \<Pi>) xa h ((stk,loc,p)#frs) = (None,h,fr'#frs')"
assumes X_def: "fst (the (h xa)) = X"
shows "\<exists>B. (snd (snd (fr')),B) \<in> set (succsXpt (\<Pi>,X,[p])) \<and> \<Pi>,s \<Turnstile> B"
proof -
from s_ReachablesAn
have s_Reachables: "s \<in> Reachables \<Pi>"
  by (rule ReachablesAn_Reachables)

from wf_Pi s_Reachables s_def
have frs_domC: "\<forall>p\<in>set (map (snd \<circ> snd) ((stk, loc, p) # frs)). p \<in> set (domC \<Pi>)"
  apply (rule_tac p="p" and x="None" and h="h" and 
         frs="(stk,loc,p)#frs" and e="e" in  wf_Reachables_domC')
  apply assumption
  apply simp
  done

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

from wf_Pi find_handler_s frs_domC
have fst_fr': "fst fr' = [Addr xa]"
 apply (frule_tac xa="xa" and h="h" and st'="stk" and loc="loc" and p="p" 
         and frs="frs" and fr'="fr'" and frs'="frs'" in findhandler_stk)
 by assumption+

from fst_fr'
obtain loc' C' M' pc' where fr'_def: "fr'=([Addr xa],loc',C',M',pc')"
  apply (cases "fr'")
  by fastsimp
 
obtain P An where Pi_def: "\<Pi> = (P,An)"
  by (cases "\<Pi>")

from wf_Pi Pi_def cmd_p p_domC p_def
have i_instrs_of: "(instrs_of P C M ! pc) = i"
  apply -
  apply (drule domC_cmd_instr_of)
  apply simp
  apply simp
  done


from find_handler_s p_def obtain pfx 
where pfx_def: "(stk, loc, C, M, pc) # frs = pfx @ frs'" 
 and pfx_ne_Nil: "pfx \<noteq> []"
  apply -
  apply (drule find_handler_frs)
  by fastsimp

show ?thesis
proof (cases "frs = frs'")

case True

note frs_eq_frs' = True

show ?thesis
proof (cases "JVMExceptions.match_ex_table P X pc (ex_table_of P C M)")

case None
 from None frs_eq_frs' find_handler_s s_def p_def Pi_def X_def
 show ?thesis
   apply simp
   apply (drule find_handler_frs)
   apply simp
   done

next

case (Some pcd)

from Some
obtain en 
where en_intro: "match_ex_table_e P X pc (ex_table_of P C M) = Some en" 
and en_pcd: "snd (snd (snd en)) = pcd"
 apply -
 apply (drule match_ex_table_e_sim2)
 apply (erule exE | erule conjE)+
 by fastsimp

from en_pcd
obtain f t X' 
where en_def: "en = (f,t,X',pcd)"
  apply (cases "en")
  by fastsimp

from p_domC p_def Pi_def
have C_M_methodnames: "(C,M) \<in> set (methodnames P)"
  by (rule_tac pc="pc" and An="An" in domC_methodnames,simp)

from frs_eq_frs' Some find_handler_s s_def fr'_def X_def Pi_def p_def
obtain d where CeqC': "C = C'" 
  and MeqM': "M = M'"
  and pcd_pc': "pcd = (pc',d)"
  apply (cases pcd)
  by fastsimp

from Some wf_Pi C_M_methodnames Pi_def p_def CeqC' MeqM' pcd_pc'
have p'_domC: "(C',M',pc') \<in> set (domC (P,An))"
 apply -
 apply (rule_tac X="X" and pc="pc" and pc'="pc'" in wf_ex_table_domC)
 apply simp+
 done

show ?thesis
proof (cases "length (domC (P, An)) \<le> Suc 0")

case True
from True p'_domC fr'_def Pi_def
show ?thesis
  apply -
  apply (rule_tac x="TT" in exI)
  apply simp
  done

next

case False

note domC_length = False

note mainsimps = en_intro en_def domC_length Pi_def cmd_p exec_i 
                 p_def fr'_def pcd_pc' CeqC' MeqM' xcpt_cond_def s_def
                 check_s i_instrs_of
show ?thesis
proof (cases i)

case (Load n)
from this Pi_def cmd_p exec_i 
show ?thesis
  by simp

next

case (Store n)
from this Pi_def cmd_p exec_i 
show ?thesis
  by simp

next

case (Push v)
from this Pi_def cmd_p exec_i 
show ?thesis
  by simp

next
  
case (New Cl)
from this mainsimps
show ?thesis
  by simp

next

case (Getfield F C)
from this mainsimps 
show ?thesis
  apply -
  apply (case_tac "stk")
  apply (simp add: split_def check_def split add: split_if_asm)
  apply (simp add: split_def split add: split_if_asm)
  done

next

case (Putfield F C)
from this mainsimps
show ?thesis
  apply -
  apply (case_tac "stk")
  apply (simp add: split_def check_def split add: split_if_asm)

  apply (simp add: split_def  hd_list_def split add: split_if_asm)
  apply (case_tac "list")
  apply (simp add: split_def check_def)
  apply simp
  done

next

case (Checkcast Cl)

show ?thesis
  proof (cases "cast_ok P Cl h (hd stk)")
    case True
    from True Checkcast mainsimps
    show ?thesis
      by simp
    
  next
    
    case False
    from Checkcast s_def check_s Pi_def i_instrs_of p_def
    obtain r stks
    where stk_def: "stk = r#stks"
    and r_isRef': "is_Ref' h r"
    and is_class_Cl: "is_class P Cl"
      apply (cases stk)
      apply (simp add: check_def split_def)
      apply (simp add: check_def split_def)
      apply fastsimp
      done

    from False stk_def r_isRef' is_Ref'_def
    obtain r' where r_Addr: "r = Addr r' \<and> h r' \<noteq> None"
      apply -
      apply (simp add: cast_ok_def)
      apply (case_tac "r::val")
      apply simp+
      apply fastsimp
      done
    
    from False Checkcast mainsimps stk_def r_Addr is_class_Cl is_Ref'_def 
    show ?thesis
      apply -
      apply (simp add: evalEs_map cast_ok_def list_all_iff)
      apply (rule allI)+
      apply (rule impI)+
      apply (case_tac "x = a")
      apply (erule conjE | erule exE)+
      apply simp

      apply simp
      done
  qed
  
  next
    case (Invoke Mn n)
    from this mainsimps
    show ?thesis
      apply (case_tac "stk ! n = Null")
      apply (simp add: check_def split_def)

      apply (simp add: split_def)
      done
  next
    case Return
    from this mainsimps
    show ?thesis
      by simp

  next
    
    case Pop
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp

  next
    
    case IBin
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp
 
  next
    
    case (Goto t)
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp

  next
    
    case CmpEq
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp
 
  next
    
    case (IfIntCmp ro t)
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp

 next
    
    case (IfFalse  t)
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp

  next
    case Throw

    from Throw s_def check_s Pi_def i_instrs_of p_def
    obtain v stks
    where stk_def: "stk = v#stks"
    and v_isRef'_Null: "is_Ref' h v \<or> v = Null"
      apply (cases stk)
      apply (simp add: check_def split_def)
      apply (simp add: check_def split_def)
      apply fastsimp
      done

    from stk_def v_isRef'_Null is_Ref'_def
    obtain r where v_Addr: "v \<noteq> Null \<longrightarrow> (v = Addr r \<and> h r \<noteq> None)"
      apply -
      apply (case_tac "v::val")
      apply simp+
      apply fastsimp
      done

    from s_Reachables s_def sys_xcpts_def
    have cname_NullPointer: "cname_of h (addr_of_sys_xcpt NullPointer) = NullPointer"
      apply -
      apply (rule sys_xcpt_Reachables)
      apply assumption
      apply assumption
      apply simp
      done
    
    from Throw mainsimps stk_def v_Addr X_def cname_NullPointer
    show ?thesis
      apply -
      apply simp
      apply (erule conjE | erule exE)+
      apply (drule_tac t="frs''" in sym)
      apply simp
      apply (case_tac "v = Null")
      apply simp
      
      apply simp
      apply fastsimp
      done
  qed
qed
qed

next
--{* frs ~= frs' *}
case False
note frs_neq_frs' = False

from frs_neq_frs' s_def fr'_def find_handler_s Pi_def p_def X_def
obtain hc stkc pcc where catchstate_s: 
"catchstate (P, X, p, (None, h, (stk, loc, p) # frs), e) =
((C', M', pcc), (None, hc, (stkc, loc', C', M', pcc) # frs'), e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>)"
and match_ex_table_pc':"JBC_VCG.match_ex_table P X pcc (ex_table_of P C' M') = \<lfloor>pc'\<rfloor>"
  apply -
  apply (simp only:)
  apply (frule_tac stk="stk" and e="e" in find_handler_catchstate')
  apply (simp only: simp_thms)
  apply (erule exE | erule conjE)+
  apply fastsimp
  done

from match_ex_table_pc'
obtain pcd where pcd_intro: "JVMExceptions.match_ex_table P X pcc (ex_table_of P C' M') = \<lfloor>pcd\<rfloor>"
           and pcd_pc': "fst pcd = pc'"
  apply -
  apply (rule classical)
  apply simp
  apply fastsimp
  done

from pcd_pc'
obtain d where pcd_def: "pcd = (pc',d)"
  apply (cases pcd)
  by fastsimp
  
from pcd_intro
obtain en 
where en_intro: "match_ex_table_e P X pcc (ex_table_of P C' M') = Some en" 
and en_pcd: "snd (snd (snd en)) = pcd"
 apply -
 apply (drule match_ex_table_e_sim2)
 apply (erule exE | erule conjE)+
 by fastsimp

from en_pcd
obtain f t X' 
where en_def: "en = (f,t,X',pcd)"
  apply (cases "en")
  by fastsimp

from pcd_intro Pi_def p_def
have p'_domC: "(C',M',pc') \<in> set (domC \<Pi>)"
  proof -
    from frs_domC find_handler_s s_def fr'_def Pi_def
    have methodnames_C'M': "(C',M') \<in> set (methodnames P)"
      apply -
      apply (drule find_handler_frs')
      apply (erule conjE | erule exE)+
      apply simp
      apply (rule_tac xs="pfx" in rev_cases)
      apply simp

      apply (simp only: last_snoc)
      apply (subgoal_tac "\<exists> y1 y2 y3 y4 y5. y = (y1,y2,y3,y4,y5)")
       prefer 2
       apply fastsimp
      apply (erule exE)+
      apply (simp add: split_def)
      apply (erule conjE)+
      apply (rule_tac An="An" and pc="snd (snd (snd (snd y)))" in domC_methodnames)
      apply simp
      done
    from wf_Pi pcd_intro methodnames_C'M' pcd_def Pi_def
    show ?thesis
      apply -
      apply (simp only:)
      apply (drule wf_ex_table_domC)
      apply assumption
      apply assumption
      apply assumption
      done
  qed

from wf_Pi s_Reachables
have callers_sysinv_s: "callers_sysinv (\<Pi>,s)"
  by (rule callers_sysinv_Reachables)

from frs_neq_frs' find_handler_s s_def p_def Pi_def X_def
have no_match_ex_table_e_p: "match_ex_table_e P X pc (ex_table_of P C M) = None"
  apply -
  apply simp
  apply (rule classical)
  apply simp
  apply (erule exE)+
  apply (drule match_ex_table_e_sim)
  apply simp
  done

from catchstate_s en_intro en_pcd en_def pcd_def p'_domC callers_sysinv_s s_def no_match_ex_table_e_p Pi_def p_def X_def   
obtain B 
where p'_B_succsXpt:  "((C',M',pc'), B) \<in> set (succsXpt (\<Pi>, X, [p]))"
and B_def:"B = TT \<or> B = And [xcpt_cond (P,An) X (last [p])] \<or> 
           B= And [ Catch X' (aF \<Pi> (C',M',pcc)), Catch X (Pos (C',M',pcc)), xcpt_cond \<Pi> X p]"
  apply - 
  apply (drule_tac P="P" and An="An" and X="X" and X'="X'" and p="p" and h="h" and stk="stk" and loc="loc" 
                 and frs="frs" and e="e" and h'="hc" and stk'="stkc" and loc'="loc'" and p'="(C',M',pcc)" 
                 and frs'="frs'" and e'="e\<lparr>cs:=drop (length frs - length frs') (cs e)\<rparr>" and ps="[]" in catchstate_succsXpt) 
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply (erule exE | erule conjE)+
  apply fastsimp
  done

obtain \<sigma>' e' p' 
where catchstate_s_def2: "catchstate (P,X,s) = (p',\<sigma>',e')"
  by (cases "catchstate (P,X,s)")

from catchstate_s s_def catchstate_s_def2
have p'_def: "p' = (C',M',pcc)"
 and \<sigma>'_def: "\<sigma>' = (None, hc, (stkc, loc', C', M', pcc) # frs')"
 and e'_def: "e' = e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>"
  apply -
  apply fastsimp+
  done

from s_def catchstate_s_def2 p'_def \<sigma>'_def e'_def en_intro en_pcd pcd_def en_def p'_def
have catchstate_s_X_X':
"catchstate (P,X',s) = (p',\<sigma>',e')"
  apply -
  apply (simp only:)
  apply (rule_tac h="h" and stk="stk" and loc="loc" and frs="frs" and pch="pc'"
         and C'="C'" and M'="M'" and pc'="pcc" and h'="hc" and stk'="stkc"
         and loc'="loc'" and frs'="frs'" and X="X" and f="f" and t="t" and d="d" 
         in catchstate_X_X')
  apply (rule refl)
  apply (rule refl)
  apply (rule refl)
  apply assumption
  apply simp
  done

from frs_neq_frs' pfx_def pfx_ne_Nil
obtain fr2 frs2 where frs_def: "frs = fr2#frs2"
  apply -
  apply (case_tac "frs")
  apply (simp add: neq_Nil_conv)
  apply (erule exE)+
  apply simp

  apply fastsimp
  done

have catchstate_s_aF: "\<Pi>,(p',\<sigma>',e') \<Turnstile> (aF \<Pi> p')"
  proof -
    from Pi_def s_ReachablesAn catchstate_s_X_X'
    have catchstate_s_ReachablesAn: "(p',\<sigma>',e') \<in> ReachablesAn \<Pi>"
      apply -
      apply (drule_tac X="X'" in catchstate_ReachablesAn)
      apply simp
      done

    from wf_Pi 
    have ipc_domC: "ipc \<Pi> \<in> set (domC \<Pi>)"
      by (rule wf_ipc_domC)

    from wf_Pi ipc_domC catchstate_s_ReachablesAn Pi_def catchstate_s_X_X'
    have catchstate_s_initF_aF: "\<Pi>,(p',\<sigma>',e') \<Turnstile> initF \<Pi> \<or> \<Pi>,(p',\<sigma>',e') \<Turnstile> aF \<Pi> p'" 
      apply -
      apply (rule ReachablesAn_initF_aF)
      apply (simp add: mem_iff)+
      done
    
    show ?thesis
    proof (cases "\<Pi>,(p',\<sigma>',e') \<Turnstile> initF \<Pi>")

      case True
      note catchstate_s_initF = True

      from catchstate_s_initF 
      have p'_ipc: "p' = ipc \<Pi>"
	by (simp add: initF_def)

      from wf_Pi s_def frs_def s_Reachables Pi_def p_def catchstate_s_X_X'
      obtain Mn n 
	where cmd_p': "cmd \<Pi> p' = Some (Invoke Mn n)"
	apply -
	apply (drule_tac X="X'" and P="P" in catchstate_Invoke)
	apply simp
	apply simp
	apply fastsimp
	done

      from cmd_p' p'_ipc wf_Pi
      show ?thesis
	apply -
	apply (drule wf_ipc_no_Invoke)
	apply simp
	done

    next

      case False

      from False catchstate_s_X_X' catchstate_s_initF_aF p'_def
      show ?thesis
	by simp
    qed
  qed

from Pi_def s_Reachables
have catchstate_s_Reachables: "catchstate (P,X',s) \<in> Reachables \<Pi>"
  apply -
  apply (drule catchstate_Reachables)
  apply simp
  done

from wf_Pi catchstate_s catchstate_s_def2 catchstate_s_X_X' catchstate_s_Reachables
have catchstate_s_Pos_p': "\<Pi>,(p',\<sigma>',e') \<Turnstile> Pos p'"
  apply -
  apply (drule_tac s="(p',\<sigma>',e')" in inv_Pos_Reachable)
  apply simp
  apply (simp add: inv_Pos_def)
  done
  
note mainsimps = en_intro en_def Pi_def cmd_p exec_i 
                 p_def fr'_def pcd_pc' p'_def xcpt_cond_def s_def
                 check_s i_instrs_of

have s_xcpt_cond: "\<Pi>,s \<Turnstile> xcpt_cond \<Pi> X p"
proof (cases i)

case (Load n)
from this Pi_def cmd_p exec_i 
show ?thesis
  by simp

next

case (Store n)
from this Pi_def cmd_p exec_i 
show ?thesis
  by simp

next

case (Push v)
from this Pi_def cmd_p exec_i 
show ?thesis
  by simp

next
  
case (New Cl)
from this mainsimps
show ?thesis
  by simp

next

case (Getfield F C)
from this mainsimps 
show ?thesis
  apply -
  apply (case_tac "stk")
  apply (simp add: split_def check_def split add: split_if_asm)
  apply (simp add: split_def split add: split_if_asm)
  done

next

case (Putfield F C)
from this mainsimps
show ?thesis
  apply -
  apply (case_tac "stk")
  apply (simp add: split_def check_def split add: split_if_asm)

  apply (simp add: split_def  hd_list_def split add: split_if_asm)
  apply (case_tac "list")
  apply (simp add: split_def check_def)
  apply simp
  done

next

case (Checkcast Cl)

show ?thesis
  proof (cases "cast_ok P Cl h (hd stk)")
    case True
    from True Checkcast mainsimps
    show ?thesis
      by simp
    
  next
    
    case False
    from Checkcast s_def check_s Pi_def i_instrs_of p_def
    obtain r stks
    where stk_def: "stk = r#stks"
    and r_isRef': "is_Ref' h r"
    and is_class_Cl: "is_class P Cl"
      apply (cases stk)
      apply (simp add: check_def split_def)
      apply (simp add: check_def split_def)
      apply fastsimp
      done

    from False stk_def r_isRef' is_Ref'_def
    obtain r' where r_Addr: "r = Addr r' \<and> h r' \<noteq> None"
      apply -
      apply (simp add: cast_ok_def)
      apply (case_tac "r::val")
      apply simp+
      apply fastsimp
      done
    
    from False Checkcast mainsimps stk_def r_Addr is_class_Cl is_Ref'_def 
    show ?thesis
      apply -
      apply (simp add: evalEs_map cast_ok_def list_all_iff)
      apply (rule allI)+
      apply (rule impI)+
      apply (case_tac "x = a")
      apply (erule conjE | erule exE)+
      apply simp

      apply simp
      done
  qed
  
  next
    case (Invoke Mn n)
    from this mainsimps
    show ?thesis
      apply (case_tac "stk ! n = Null")
      apply (simp add: check_def split_def)

      apply (simp add: split_def)
      done
  next
    case Return
    from this mainsimps
    show ?thesis
      by simp

  next
    
    case Pop
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp

  next
    
    case IBin
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp
 
  next
    
    case (Goto t)
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp

  next
    
    case CmpEq
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp
 
  next
    
    case (IfIntCmp ro t)
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp

 next
    
    case (IfFalse  t)
    from this Pi_def cmd_p exec_i 
    show ?thesis
      by simp

  next
    case Throw

    from Throw s_def check_s Pi_def i_instrs_of p_def
    obtain v stks
    where stk_def: "stk = v#stks"
    and v_isRef'_Null: "is_Ref' h v \<or> v = Null"
      apply (cases stk)
      apply (simp add: check_def split_def)
      apply (simp add: check_def split_def)
      apply fastsimp
      done

    from stk_def v_isRef'_Null is_Ref'_def
    obtain r where v_Addr: "v \<noteq> Null \<longrightarrow> (v = Addr r \<and> h r \<noteq> None)"
      apply -
      apply (case_tac "v::val")
      apply simp+
      apply fastsimp
      done

    from s_Reachables s_def sys_xcpts_def
    have cname_NullPointer: "cname_of h (addr_of_sys_xcpt NullPointer) = NullPointer"
      apply -
      apply (rule sys_xcpt_Reachables)
      apply assumption
      apply assumption
      apply simp
      done
    
    from Throw mainsimps stk_def v_Addr X_def cname_NullPointer
    show ?thesis
      apply -
      apply simp
      apply (erule conjE | erule exE)+
      apply (drule_tac t="frs''" in sym)
      apply simp
      apply (case_tac "v = Null")
      apply simp
      
      apply simp
      apply fastsimp
      done
  qed

  from p'_B_succsXpt B_def catchstate_s_X_X' catchstate_s_def2 catchstate_s_Pos_p' 
       p'_def catchstate_s_aF fr'_def s_xcpt_cond Pi_def s_def frs_def
  show ?thesis
    apply -
    apply (erule disjE)
    apply (rule_tac x="TT" in exI)
    apply simp

    apply (erule disjE)
    apply (rule_tac x="And [xcpt_cond (P, An) X (last [p])]" in exI)
    apply simp

    apply (rule_tac x="And [Catch X' (aF \<Pi> p'), Catch X (Pos p'), xcpt_cond \<Pi> X p]" in exI)
    apply (simp del: succsXpt.simps)
    done
qed
qed
(*>*)


section {* succsF correct *}


lemma succsF_correct:
assumes wf_Pi:"wf \<Pi>"
assumes in_ReachablesAn:"s \<in> (ReachablesAn \<Pi>)"
assumes s_s'_effS: "(s,s') \<in> (effS \<Pi>)"
shows "(\<exists>B. (fst s',B) \<in> set (succsF \<Pi> (fst s)) \<and> \<Pi>,s \<Turnstile> B)"
(*<*)
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   "\<exists>B. (fst s', B) \<in> set (succsF \<Pi> (fst s)) \<and> \<Pi>,s \<Turnstile>  B"
 proof -
 from s_s'_def have s_def: "s = (p,\<sigma>,e)" by simp
 from s_s'_def have s'_def: "s' = (p',\<sigma>',e')" by simp
 from wf_Pi in_ReachablesAn s_def have p_domC: "p \<in> set (domC \<Pi>)"
  apply -
  apply (drule ReachablesAn_Reachables)
  apply (drule_tac s="s" in wf_Reachables_domC)
  apply simp
  apply simp
  done

 from P_def obtain An where Pi_def: "\<Pi> = (P,An)"
  apply simp
  apply atomize
  apply (erule_tac x="snd \<Pi>" in allE)
  apply simp
  done
 from wf_Pi p_domC i_def p_def Pi_def have cmd_p: "cmd \<Pi> p = Some i"
  apply -
  apply (frule domC_cmd_instr_of)
  apply simp
  apply simp
  done

 from in_ReachablesAn have s_Reachables: "s \<in> Reachables \<Pi>"
   by (rule ReachablesAn_Reachables)

 from wf_Pi s_Reachables s_def Pi_def have check_sigma: "check P \<sigma>"
   apply -
   apply (drule_tac s="s" in wf_Reachables_check)
   apply assumption
   apply simp
   done

 from check_sigma i_def sigma_def p_def
 have check_i:"check_instr i P h stk loc C M pc frs"
  apply -
  apply simp
  apply (rule check_checkinstr)
  apply simp
  done 

 from wf_Pi s_Reachables s_def have s_invPos: "\<Pi>,s \<Turnstile> Pos p"
   apply -
   apply (drule inv_Pos_Reachable)
   apply assumption
   apply (simp add: inv_Pos_def)
   done

 note main_prems = wf_Pi in_ReachablesAn s_Reachables s_def s'_def Pi_def p_def i_def[THEN sym] sigma_def check_sigma
      has_method_C_M exec_i find_handler_s sigma'_def e'_def p_domC cmd_p check_i s_invPos
 note main_simps = succsF_def succsExcept_def fst_conv set_append mem_simps split_def Pair_eq option.cases 
 show ?thesis proof (cases i)
 case Load
 from this main_prems show ?thesis by (simp add: main_simps)
next 
 case Store
 from this main_prems show ?thesis by (simp add: main_simps)
next 
 case Push
 from this main_prems show ?thesis by (simp add: main_simps)
next
 case New
 from New main_prems show ?thesis 
 apply (simp only: main_simps del: New)
 apply (simp only: Pair_eq instr.cases exec_instr.simps simp_thms  split add: option.split_asm,clarify)
 
 apply (drule_tac  xa="addr_of_sys_xcpt OutOfMemory" and frs="frs" and stk="stk" and loc="loc" and e="e" and X="OutOfMemory" and h'="h'"
       and frs'="frs'"  in findhandler_succsXpt)
 apply (simp only:)

 apply (simp only:)

 apply (simp only:)

 apply (simp only:)

 apply simp

 apply simp

 apply (simp del: find_handler.simps split del: option.split_asm)

 apply (simp add: sys_xcpt_Reachables)

apply (erule exE | erule conjE)+
apply (simp only: in_set_conv_decomp)
apply (erule exE )+
apply (simp add: addPos_append split del: option.split option.split_asm)
apply (simplesubst addPos_cons)
apply (rule_tac x="And [Pos (C,M,pc),B]" in exI)
apply (rule conjI)
apply (rule_tac x="addPos (C, M, pc) (succsNormal (P, An) (C, M, pc)) @
             addPos (C, M, pc) ysa" in exI)
apply (rule_tac x="addPos (C, M, pc) zsa" in exI)
apply (simp add: addPos_single  split del: option.split_asm)

apply (simp add: addPos_single)

apply simp
done

next 
 case Getfield
 from Getfield main_prems show ?thesis 
 apply (simp only: main_simps del: Getfield)
 apply (simp only: Pair_eq instr.cases exec_instr.simps simp_thms  split add: option.split_asm,clarify)
 apply (drule_tac xa="xa" and frs="frs" and stk="stk" and loc="loc" and e="e" 
                  and X="NullPointer" and h'="h'" and frs'="frs'" in findhandler_succsXpt)
 apply (simp only:)

 apply (simp only:)

 apply (simp only:)

 apply (simp only:)

 apply simp

 apply simp

 apply simp

 apply (simp add: split_def is_Ref_def is_Ref'_def split del: split_if split_if_asm option.split option.split_asm)
 apply (case_tac "hd stk = Null")
 apply (simp split del: option.split_asm)
 apply (erule conjE)+
 apply (drule_tac t="xa" in sym)
 apply (simp add:  sys_xcpt_Reachables)

 apply simp

 apply (erule exE)
 apply (rule_tac x="And [Pos p,B]" in exI)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE | erule conjE)+
 apply (cut_tac p_def)
 apply (simp add: addPos_append  del: succsXpt.simps split del: option.split_asm)
 apply (simplesubst addPos_cons)
 apply (rule_tac x="addPos (C, M, pc) (succsNormal (P, An) (C, M, pc)) @ addPos (C, M, pc) ysa" in exI)
 apply (rule_tac x="addPos (C, M, pc) zsa" in exI)
 apply (simp split del: split_if split_if_asm option.split option.split_asm)
 apply (simp add: addPos_def)
 done 

next
 case Putfield
 from Putfield main_prems show ?thesis 
 apply (simp only: main_simps del: Putfield)
 apply (simp only: Pair_eq instr.cases exec_instr.simps simp_thms  split add: option.split_asm,clarify)
 apply (drule_tac xa="xa" and frs="frs" and stk="stk" and loc="loc" and e="e" 
                  and X="NullPointer" and h'="h'" and frs'="frs'" in findhandler_succsXpt)
 apply (simp only:)

 apply (simp only:)

 apply (simp only:)
 
 apply simp

 apply simp

 apply simp

 apply simp

 apply (simp add: split_def is_Ref_def is_Ref'_def split del: split_if split_if_asm option.split option.split_asm)
 apply (case_tac "hd (tl stk) = Null")
 apply (simp split del: option.split_asm)
 apply (erule conjE)+
 apply (drule_tac t="xa" in sym)
 apply (simp add:  sys_xcpt_Reachables)

 apply simp

 apply (erule exE)
 apply (rule_tac x="And [Pos p,B]" in exI)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE | erule conjE)+
 apply (cut_tac p_def)
 apply (simp add:  addPos_append  del: succsXpt.simps split del: option.split_asm)
 apply (simplesubst addPos_cons)
 apply (rule_tac x="addPos (C, M, pc) (succsNormal (P, An) (C, M, pc)) @ addPos (C, M, pc) ysa" in exI)
 apply (rule_tac x="addPos (C, M, pc) zsa" in exI)
 apply (simp split del: split_if split_if_asm option.split option.split_asm)
 apply (simp add: addPos_def)
 done

next

 case Checkcast
 from Checkcast obtain Cl where Checkcast':"i = Checkcast Cl"
  by fastsimp
 from Checkcast' main_prems show ?thesis 
 apply (simp only: main_simps del: Checkcast')
 apply (simp only: Pair_eq instr.cases exec_instr.simps simp_thms  split add: option.split_asm,clarify)
 apply (drule_tac xa="xa" and frs="frs" and stk="stk" and loc="loc" and e="e" 
                  and X="ClassCast" and h'="h" and frs'="frs'" in findhandler_succsXpt)
 apply (simp only:)

 apply (simp only:)

 apply (simp only:)
 
 apply simp

 apply simp

 apply (simp split del: option.split_asm)
 apply (case_tac " \<not> (cast_ok P Cl h (hd stk))")
 apply simp

 apply simp

 apply simp

 apply (simp split del: option.split_asm)
 apply (case_tac " \<not> (cast_ok P Cl h (hd stk))")
 apply (simp split del: option.split_asm)
 apply (erule conjE)+
 apply (drule_tac t="xa" in sym)
 apply (simp add: sys_xcpt_Reachables)

 apply simp

 apply (erule exE)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE | erule conjE)+
 apply (rule_tac x="And [Pos (C,M,pc), B]" in exI)
 apply (simp add: addPos_append del: succsXpt.simps split del: option.split_asm)
 apply (simplesubst addPos_cons)
 apply (rule_tac x="addPos (C, M, pc) (succsNormal (P, An) (C, M, pc)) @ addPos (C, M, pc) ysa" in exI)
 apply (rule_tac x="addPos (C, M, pc) zsa" in exI)
 apply (simp split del: split_if split_if_asm option.split option.split_asm)
 apply (simp add: addPos_def)
 done

next
 case Invoke
 from Invoke obtain Mn na where Invoke':"i = Invoke Mn na"
  by fastsimp
 from Invoke' main_prems show ?thesis 
 apply (simp only: main_simps del: Invoke')
 apply (simp only: Pair_eq instr.cases exec_instr.simps simp_thms  split add: option.split_asm,clarify)
 apply (drule_tac xa="xa" and frs="frs" and stk="stk" and loc="loc" and e="e" 
                  and X="NullPointer" and h'="h'" and frs'="frs'" in findhandler_succsXpt)
 apply (simp only:)

 apply (simp only:)

 apply (simp only:)
 
 apply simp

 apply simp

 apply (simp split del: option.split_asm)

 apply simp

 apply (simp add: split_def split del: option.split_asm)
 apply (case_tac "stk ! na = Null") 
 apply (simp split del: option.split_asm)
 apply (erule conjE)+
 apply (drule_tac t="xa" in sym)
 apply (simp add: sys_xcpt_Reachables)

 apply simp

 apply (erule exE)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE | erule conjE)+
 apply (rule_tac x="And [Pos (C,M,pc), B]" in exI)
 apply (simp add: addPos_append del: succsXpt.simps split del: option.split_asm)
 apply (simplesubst addPos_cons)
 apply (rule_tac x="addPos (C, M, pc) (succsNormal (P, An) (C, M, pc)) @ addPos (C, M, pc) ysa" in exI)
 apply (rule_tac x="addPos (C, M, pc) zsa" in exI)
 apply (simp split del: split_if split_if_asm option.split option.split_asm)
 apply (simp add: addPos_def)
 done

next
 case Return
 from this main_prems show ?thesis 
 apply (simp only: main_simps del: Return)
 apply (simp only: Pair_eq instr.cases exec_instr.simps simp_thms  split add: option.split_asm,clarify)
 apply (case_tac "frs:: val list ~~> val list \<times> char list \<times> char list \<times> nat")
 apply (simp split del: option.split option.split_asm)

 apply (simp add: split_def split del: option.split option.split_asm)
 done

next 
 case Pop
 from this main_prems show ?thesis by (simp add: main_simps)

next 
 case (IBin no)
 from this main_prems show ?thesis by (simp add: main_simps)

next 
 case Goto
 from this main_prems show ?thesis by (simp add: main_simps)

next 
 case CmpEq
 from this main_prems show ?thesis by (simp add: main_simps)

next 
 case IfIntCmp
 from this main_prems show ?thesis by (simp add: main_simps)

next 
 case IfFalse
 from this main_prems show ?thesis by (simp add: main_simps)


next
 case Throw
 from Throw main_prems show ?thesis 
 apply (simp only: main_simps del: Throw)
 apply (simp only: Pair_eq instr.cases exec_instr.simps simp_thms  split add: option.split_asm,clarify)
 apply (drule_tac xa="if (hd stk = Null) then (addr_of_sys_xcpt NullPointer) else xa" and frs="frs" and stk="stk" and loc="loc" and e="e" 
                  and X="if (hd stk = Null) then NullPointer else (cname_of h' xa)" and h'="h'" and frs'="frs'" in findhandler_succsXpt)
 apply (simp only:)

 apply (simp only:)

 apply (simp only:)

 apply simp

 apply simp

 apply simp
 apply (case_tac "hd stk = Null")
 apply simp

 apply simp

 apply simp
 apply (case_tac "hd stk = Null")
 apply simp

 apply simp

 apply simp
 apply (case_tac "hd stk = Null")
 apply simp
 apply (erule conjE)+
 apply (drule_tac t="xa" in sym)
 apply (simp add: sys_xcpt_Reachables)

 apply simp

apply (erule exE)
apply (simp only: in_set_conv_decomp)
apply (erule exE | erule conjE)+
apply (simp add: addPos_append del: succsXpt.simps split del: option.split_asm option.split)

apply (rule_tac x="And [Pos (C, M, pc),B]" in exI)
apply (rule conjI)
prefer 2
apply (erule conjE)+
apply (drule_tac t="frs''" in sym)
apply simp

apply (case_tac "hd stk = Null")
apply (rule_tac x="addPos (C, M, pc) (succsNormal (P, An) (C, M, pc)) @
             addPos (C, M, pc) ysa" in exI)
apply (rule_tac x="addPos (C, M, pc) (zsa @ (case anF (P, An) (C, M, pc) of None \<Rightarrow> []
                        | \<lfloor>a\<rfloor> \<Rightarrow>  concat (map (ty_case [] [] [] [] (\<lambda>X. succsXpt ((P, An), X, [(C, M, pc)]))) (extractTy (a, St 0)))))" in exI)
apply (simp add: addPos_append addPos_single  split del: option.split_asm option.split)
apply (simplesubst addPos_cons)
apply (simp add: addPos_single)

--{* hd st ~= Null *}

apply (subgoal_tac "checkPos (P, An) (domC (P, An))")
 prefer 2
 apply (cut_tac wf_Pi Pi_def)
 apply (simp only: JBC_VCG.wf_def)
apply (frule cmd_domC)
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (case_tac "anF (P,An) (C,M,pc)")
apply (simp add: checkPos_split )
--{* anF  = Some a *}
apply (subgoal_tac "\<Pi>,s \<Turnstile> a")
 prefer 2
 apply (drule ReachablesAn_initS_aF)
 apply (erule disjE)
 apply (simp add: initS_def ipc_def start_state_def checkPos_split)

 apply (simp add: Pi_def s_def p_def sigma_def aF_def)
apply (subgoal_tac "\<exists> tp \<in> set (extractTy (a,St 0)). \<Pi>,s \<Turnstile> Ty (St 0) tp")
 prefer 2
 apply (rule_tac A="a" in extractTy_sem)
 apply assumption
 apply (rule refl)
 apply (case_tac "extractTy (a, St 0)")
 apply (simp add: checkPos_split split add: split_if_asm) 
 
 apply simp
apply (erule bexE)
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: checkPos_split del: succsXpt.simps split add: split_if_asm)
apply (case_tac "ysc @ tp # zsc")
apply simp

apply (simp only: list.cases if_False)
apply (drule_tac t="ab # list" in sym)
apply (simp only: list_all_iff)
apply (erule_tac  x="tp" in ballE)
 prefer 2
 apply (drule_tac s="ysc @ tp # zsc" in sym)
 apply simp
apply (case_tac "tp")
apply simp
apply simp
apply simp
apply simp
--{* tp = Class lista *}
apply (drule_tac t="frs''" in sym)
apply (simp add: s_def sigma_def p_def del: succsXpt.simps split del: option.split option.split_asm)
apply (subgoal_tac "cname_of h' xa = lista")
 prefer 2
 apply (case_tac "stk::val list")
 apply simp

 apply (case_tac "aa")
 apply simp
 apply simp
 apply simp
 apply simp
 --{* aa = Addr nat *}
 apply (simp add: s_def p_def sigma_def split del: option.split_asm)
 apply (simp add: obj_ty_def)
apply (simp only:)
apply (simp only: addPos_append)
apply (simplesubst addPos_cons)
apply (rule_tac x="addPos (C, M, pc) (succsNormal (P, An) (C, M, pc)) @
                  addPos (C, M, pc) (succsXpt ((P, An), NullPointer, [(C, M, pc)])) @
                  addPos (C, M, pc)
                   (concat (map (ty_case [] [] [] [] (\<lambda>X. succsXpt ((P, An), X, [(C, M, pc)]))) ysc)) @
                  addPos (C, M, pc) ysa" in exI)
apply (rule_tac x="addPos (C, M, pc) zsa @ 
                   addPos (C,M,pc) (concat (map (ty_case [] [] [] [] (\<lambda>X. succsXpt ((P, An), X, [(C, M, pc)]))) zsc))" in exI)
apply (simp only: addPos_single)
apply (simp del: succsXpt.simps split del: option.split_asm)
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  "\<exists>B. (fst s', B) \<in> set (succsF \<Pi> (fst s)) \<and> \<Pi>,s \<Turnstile>  B"
 proof -
 from s_s'_def have s_def: "s = (p,\<sigma>,e)" by simp
 from s_s'_def have s'_def: "s' = (p',\<sigma>',e')" by simp
 from wf_Pi in_ReachablesAn s_def have p_domC: "p \<in> set (domC \<Pi>)"
  apply -
  apply (drule ReachablesAn_Reachables)
  apply (drule_tac s="s" in wf_Reachables_domC)
  apply simp
  apply simp
  done
 from P_def obtain An where Pi_def: "\<Pi> = (P,An)"
  apply simp
  apply atomize
  apply (erule_tac x="snd \<Pi>" in allE)
  apply simp
  done
 from wf_Pi p_domC i_def p_def Pi_def have cmd_p: "cmd \<Pi> p = Some i"
  apply -
  apply (frule domC_cmd_instr_of)
  apply simp
  apply simp
  done

 from in_ReachablesAn have s_Reachables: "s \<in> Reachables \<Pi>"
   by (rule ReachablesAn_Reachables)

 from wf_Pi s_Reachables s_def Pi_def have check_sigma: "check P \<sigma>"
   apply -
   apply (drule_tac s="s" in wf_Reachables_check)
   apply assumption
   apply simp
   done

 from check_sigma i_def sigma_def p_def
 have check_i:"check_instr i P h stk loc C M pc frs"
  apply -
  apply simp
  apply (rule check_checkinstr)
  apply simp
  done

 from wf_Pi s_Reachables s_def have s_invPos: "\<Pi>,s \<Turnstile> Pos p"
   apply -
   apply (drule inv_Pos_Reachable)
   apply assumption
   apply (simp add: inv_Pos_def)
   done

 note main_prems = wf_Pi in_ReachablesAn s_def s'_def Pi_def p_def i_def[THEN sym] sigma_def check_sigma 
      has_method_C_M exec_i  sigma'_def p'_def e'_def  p_domC cmd_p check_i s_invPos
 note main_simps = succsF_def succsNormal_def incA_def  
 show ?thesis proof (cases i)

case Load
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (rule_tac x="And [Pos p,TT]" in exI)
 apply (simp add: p_def addPos_def)
 done

next

case Store
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (rule_tac x="And [Pos p,TT]" in exI)
 apply (simp add: p_def addPos_def)
 done

next

case Push
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (rule_tac x="And [Pos p,TT]" in exI)
 apply (simp add: p_def addPos_def)
 done

next

case New
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (rule_tac x="And [Pos p,Neg (xcpt_cond (P,An) OutOfMemory (C,M,pc))]" in exI)
 apply (simp add: p_def addPos_def xcpt_cond_def)
 done

next
case Getfield
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (case_tac "hd stk = Null")
 apply (simp add: split_def)
 apply (simp add: split_def)
 apply (rule_tac x="And [Pos p,Neg (xcpt_cond (P,An) NullPointer (C,M,pc))]" in exI)
 apply (case_tac "stk::val list")
 apply (simp  add: addPos_def xcpt_cond_def hd_list_def nth_list_def)

 apply (drule_tac t="fr'" in sym)
 apply (simp  add: p_def addPos_def xcpt_cond_def)
 apply (case_tac "frs'::val list ~~> val list \<times> char list \<times> char list \<times> nat")
 apply simp
 apply simp
 done

next

case Putfield
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (case_tac "hd (tl stk) = Null")
 apply (simp add: split_def)
 apply (simp add: split_def)
 apply (rule_tac x="And [Pos p,Neg (xcpt_cond (P,An) NullPointer (C,M,pc))]" in exI)
 apply (case_tac "stk::val list")
 apply (simp  add: addPos_def xcpt_cond_def hd_list_def nth_list_def)
 apply (case_tac "list")
 apply (simp  add: addPos_def xcpt_cond_def hd_list_def nth_list_def)
 
 apply clarify
 apply (simp  add: p_def addPos_def xcpt_cond_def)
 done

next

case (Checkcast Cl)
 from Checkcast main_prems show ?thesis 
 apply (simp only: main_simps del: Checkcast)
 apply (simp add: main_simps del: callers_sysinv.simps option.splits, clarify)
 apply (case_tac "\<not> cast_ok P Cl h' (hd stk)")
 apply (simp add: split_def)
 
 apply (simp add: split_def del: callers_sysinv.simps)
 apply (rule_tac x="And [Pos p,Neg (xcpt_cond (P,An) ClassCast (C,M,pc))]" in exI)
 apply (case_tac "stk::val list")
 apply (simp  add: addPos_def xcpt_cond_def hd_list_def nth_list_def del: callers_sysinv.simps)
 
 apply (simp  add: addPos_def xcpt_cond_def cast_ok_def is_Ref_def is_Ref'_def check_def split_def del: callers_sysinv.simps)
 apply (case_tac "a = Null")
 apply (simp add: p_def del: callers_sysinv.simps)
 
 apply (simp add: p_def del: callers_sysinv.simps)
 apply (subgoal_tac "cname_of h' (the_Addr a) \<in> set (classnames P)")
  prefer 2
  apply (erule converse_rtranclE)
  apply (simp add: is_class_def classnames_def class_def)
  apply (erule exE)+
  apply (drule map_of_SomeD)
  apply (drule_tac x="(Cl,aa,ab,b)" and f="fst" and A="set P" in imageI)
  apply simp
 
  apply (drule subcls1D)
  apply (erule exE | erule conjE)+
  apply (simp add: is_class_def classnames_def class_def)
  apply (erule exE)+
  apply (drule map_of_SomeD)
  apply (drule_tac x=" (cname_of h' (the_Addr a), y, fs, ms)" and f="fst" and A="set P" in imageI)
  apply simp
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: list_all_iff)
apply (rule_tac x="evalE (P,An) ((C, M, pc), (None, h', (a # list, loc, C, M, pc) # frs), e) (Neg (Ty (St 0) (Class (cname_of h' (the_Addr a)))))" in bexI)
apply simp
apply (case_tac a)
apply simp+

apply (case_tac a)
apply simp+
apply (erule conjE | erule exE)+
--{* h nat = Some (aa,b) *}
apply (simp add: evalEs_map)
done

next

case (Invoke Mn na)
 from Invoke main_prems s_def show ?thesis 
 apply (simp only: main_simps del: Invoke)
 apply (simp add: main_simps del: option.splits callers_sysinv.simps, clarify)
 apply (case_tac "stk ! na = Null")
 apply (simp add: split_def)
 
 apply (simp add: split_def del: callers_sysinv.simps)
 apply (frule cmd_domC)
 apply (simp only: JBC_VCG.wf_def)
 apply (subgoal_tac "JBC_VCG.wf (P,An)")
  prefer 2
  apply (simp add: JBC_VCG.wf_def)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE)+
 apply (case_tac "anF (P,An) (C,M,pc)")
 apply (simp add: checkPos_split )
--{* anF . = Some a *}
 apply (subgoal_tac "\<Pi>,s \<Turnstile> a")
  prefer 2
  apply (drule ReachablesAn_initS_aF)
  apply (erule disjE)
  apply (simp add: initS_def ipc_def start_state_def checkPos_split )

  apply (simp add: aF_def s_def p_def sigma_def Pi_def)
 apply (subgoal_tac "\<exists> tp \<in> set (extractTy (a,St na)). \<Pi>,s \<Turnstile> Ty (St na) tp")
  prefer 2
  apply (rule_tac A="a" in extractTy_sem)
  apply assumption
  apply (rule refl)
  apply (case_tac "extractTy (a,St na)")
  apply (simp add: checkPos_split  split add: split_if_asm)

  apply simp
 apply (erule bexE)
 apply (simp only: in_set_conv_decomp)
 apply (erule exE)+
 apply (simp add: checkPos_split del: callers_sysinv.simps  split add: split_if_asm)
 apply (case_tac "ysa @ tp # zsa")
 apply simp
 
 apply (simp only: list.cases if_False)
 apply (drule_tac t="ac # list" in sym)
 apply (simp only: list_all_iff)
 apply (erule conjE)+
 apply (erule_tac x="tp" in ballE)
  prefer 2
  apply (drule_tac s="ysa @ tp # zsa" in sym)
  apply simp
 
 apply (case_tac "tp")
 apply simp
 apply simp
 apply simp
 --{* tp = NT *}
 apply (cut_tac s_def sigma_def)
 apply simp
 apply (case_tac "aa")
 apply simp
 apply simp
 apply simp
 apply simp
 apply simp
 --{* tp = Class lista *}
 apply (simp del:  callers_sysinv.simps split del: option.splits option.split_asm)
 apply (rule_tac x="And [Pos p,And [Neg (xcpt_cond (P, An) NullPointer (C, M, pc)), Ty (St na) (Class lista)]]" in exI)
 apply (rule conjI)
 apply (simp only: addPos_append)
 apply (simplesubst addPos_cons)
 apply (drule_tac t="fr'" in sym)
 apply (simp only: snd_conv)
 apply (subgoal_tac "fst (method (SystemClasses @ cdl) ab Mn) = lista \<and> ab = lista")
  prefer 2
  apply (subgoal_tac "ab = lista")
   prefer 2 
   apply (drule_tac t="frs'" in sym)
   apply (simp add: s_def p_def sigma_def)
   apply (case_tac "aa::val")
   apply simp
   apply simp
   apply simp
   apply simp
   --{* stk ! na = Addr nat *}
   apply (simp add: s_def p_def sigma_def obj_ty_def)
  apply (simp only:)
  apply (subgoal_tac "\<exists> Ts T m. method P lista Mn = (lista,Ts,T,m)")
   prefer 2
   apply (rule_tac An="An" in has_method_class)
   apply simp
   apply simp
  apply (erule exE)+
  apply simp
 apply (erule conjE)+
 apply (simp only:)
 apply (rule_tac x="addPos (C, M, pc)
                   (concat (map (ty_case [] [] [] []
                                  (\<lambda>X. [((fst (method (SystemClasses @ cdl) X Mn), Mn, 0),
                                         And [Neg (xcpt_cond (SystemClasses @ cdl, An) NullPointer (C, M, pc)), Ty (St na) (Class X)])]))
                             ysa))" in exI)
 apply (rule_tac x=" addPos (C, M, pc)
                (concat (map (ty_case [] [] [] []
                               (\<lambda>X. [((fst (method (SystemClasses @ cdl) X Mn), Mn, 0),
                                      And [Neg (xcpt_cond (SystemClasses @ cdl, An) NullPointer (C, M, pc)), Ty (St na) (Class X)])]))
                          zsa) @
                 succsExcept (SystemClasses @ cdl, An) (C, M, pc))" in exI)
 apply (simp only: addPos_append)
 apply (simplesubst addPos_cons)
 apply (simp only: addPos_single p_def)
 apply (simp add: addPos_def)

 apply (drule_tac t="frs'" in sym)
 apply (simp add: s_def p_def sigma_def obj_ty_def)
 apply (case_tac "aa::val")
 apply simp
 apply simp
 apply simp
 apply simp
 apply (simp add: s_def p_def sigma_def obj_ty_def xcpt_cond_def)
 done

next
 case Return
 from this main_prems show ?thesis
 apply (simp add: main_simps del: callers_sysinv.simps  del: option.splits, clarify)
 apply (case_tac "frs::val list ~~> val list \<times> char list \<times> char list \<times> nat")
 apply simp

 apply (simp only: Pair_eq list.simps if_False Let_def neq_Nil_conv split_def simp_thms del: callers_sysinv.simps)
 apply (subgoal_tac "p' = incA (fst (callstate s))")
  prefer 2
  apply (erule conjE)+
  apply (drule_tac t="fr'" in sym)
  apply (simp only: split_def fst_conv snd_conv hd.simps incA_def callstate.simps split_paired_all s_def sigma_def p'_def del: callers_sysinv.simps)
 apply (subgoal_tac "\<exists> st_a rg_a p_a. a = (st_a,rg_a,p_a)")
  prefer 2
  apply (erule thin_rl)+
  apply fastsimp
 apply (erule exE)+
 apply (subgoal_tac "fst (callstate ((p, \<sigma>, e))) = (fst p_a,fst (snd p_a),snd (snd p_a))")
  prefer 2
  apply (erule conjE)+
  apply (drule_tac t="fr'" in sym)
  apply (simp only: Pair_eq p'_def fst_conv snd_conv hd.simps split_def incA_def s_def simp_thms)
  apply (erule conjE)+
  apply (erule_tac P="(snd (snd p_a)) + 1 = snd (snd (fst (callstate (p, \<sigma>, e)))) + 1" in rev_mp)
  apply (erule thin_rl)+
  apply (rule impI)
  apply simp
 apply (subgoal_tac "fst (callstate s) \<in> set (callers (P,An) (C,M,pc))")
  prefer 2
  apply (frule callers_sysinv_Reachables)
  apply (rule ReachablesAn_Reachables)
  apply assumption
  apply (erule conjE)+
  apply (drule_tac t="fr'" in sym)
  apply (erule_tac V="e\<lparr>cs := tl (cs e)\<rparr> = e\<lparr>cs := if \<exists>M n. Return = Invoke M n then h' # cs e else if True then tl (cs e) else cs e\<rparr>" in thin_rl)
  apply (simp add: callers_def fst_conv snd_conv Pair_eq s_def p'_def incA_def split_def)
 apply (rule_tac x="And [Pos p, Call (And [aF (P,An) p_a,Pos p_a])]" in exI)
 apply (rule conjI)
 apply (drule_tac t="incA (fst (callstate s))" in sym)
 apply (erule conjE)+
 apply (simp add: in_set_conv_decomp succsF_def succsNormal_def succsExcept_def del: callers_sysinv.simps)
 apply (erule exE)+
 apply (simp add: addPos_append)
 apply (simplesubst addPos_cons)
 apply (rule_tac x="addPos (C, M, pc) (map (\<lambda>p'. ((fst p', fst (snd p'), Suc (snd (snd p'))), Call (And [aF (P, An) p', Pos p']))) ysb)" in exI)
 apply (rule_tac x="addPos (C, M, pc)
                 (map (\<lambda>p'. ((fst p', fst (snd p'), Suc (snd (snd p'))), Call (And [aF (P, An) p',Pos p']))) zsa )" in exI)
 apply (simp add: addPos_single incA_def split_def p'_def p_def s_def)

 apply (subgoal_tac "callstate s \<in> ReachablesAn \<Pi>")
  prefer 2
  apply (rule callstate_ReachablesAn)
  apply assumption
 apply (subgoal_tac "\<exists> cs_p cs_s cs_e. callstate s = (cs_p,cs_s,cs_e)")
  prefer 2
  apply (erule thin_rl)+
  apply (rule_tac x="fst (callstate s)" in exI)
  apply (rule_tac x="fst (snd (callstate s))" in exI)
  apply (rule_tac x="snd (snd (callstate s))" in exI)
  apply simp
 apply (erule exE)+
 apply (simp only:)
 apply (subgoal_tac "ipc \<Pi> mem domC \<Pi>")
  prefer 2
  apply (drule wf_ipc_domC)
  apply (simp only: mem_iff Pi_def)
 apply (frule_tac p="cs_p" and \<sigma>="cs_s" and e="cs_e" in  ReachablesAn_initF_aF)
 apply assumption
 apply (erule_tac V="e\<lparr>cs := tl (cs e)\<rparr> = e\<lparr>cs := if \<exists>M n. Return = Invoke M n then h' # cs e else if True then tl (cs e) else cs e\<rparr>" in thin_rl)
 apply (erule disjE)
 apply (simp add: initF_def callers_def p_def)
 apply (erule conjE)+
 apply (case_tac "cmd (P,An) cs_p")
 apply simp
 
 apply (case_tac "aa")
 apply simp+
    --{* aa = Invoke M nat *}
 apply (erule_tac V="(C, M, pc) \<in> set (domC (P, An))" in thin_rl)
 apply (simp only: JBC_VCG.wf_def in_set_conv_decomp)
 apply (erule exE | erule conjE)+
 apply (simp add: checkPos_split p_def split add: split_if_asm)
 apply (erule conjE)+
 apply (case_tac "anF (P, An) cs_p")
 apply simp

 apply (drule_tac t="cs_p" in sym)
 apply (simp add: Pi_def)
 
 --{* Return .. Throw *}
 apply simp+
 

 apply (erule conjE)+
 apply (simp add: p'_def incA_def split_def s_def sigma_def p_def Pi_def)
 apply (erule conjE)+
 apply (drule_tac t="cs_s" in sym)
 apply simp
 done

next
 case Pop
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (rule_tac x="And [Pos p,TT]" in exI)
 apply (simp add: p_def addPos_def)
 done

next
 case (IBin no)
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (rule_tac x="And [Pos p,TT]" in exI)
 apply (simp add: p_def addPos_def)
 done

next
 case Goto
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (rule_tac x="And [Pos p,TT]" in exI)
 apply (simp add: p_def addPos_def)
 done

next
 case CmpEq
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (rule_tac x="And [Pos p,TT]" in exI)
 apply (simp add: p_def addPos_def)
 done

next
 case (IfIntCmp "ro" "t")
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (case_tac "relop ro (the_Intg (hd (tl stk))) (the_Intg (hd stk))")
 apply simp
 apply (rule_tac x="And [Pos p,Rel (St 1) ro (St 0)]" in exI)
 apply (rule conjI)
 apply (simp add: addPos_def p_def)

 apply (simp add: p_def)
 apply (case_tac "stk::val list")
 apply simp
 apply (case_tac "list")
 apply simp

 apply (case_tac "a")
 apply simp+
 apply (case_tac "aa")
 apply (simp add: relop_def)+
 
 apply (rule_tac x="And [Pos p, Neg (Rel (St 1) ro (St 0))]" in exI)
 apply (simp add: addPos_def) 
 apply (case_tac "stk::val list")
 apply simp
 apply (case_tac "list")
 apply simp
 apply (case_tac "a")
 apply simp+
 apply (case_tac "aa")
 apply simp+
 apply (simp add: p_def relop_def)+
 done

next
 case IfFalse
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (case_tac "hd stk = Bool False")
 apply simp
 apply (rule_tac x="And [Pos p,(St 0 \<doteq> FF)]" in exI)
 apply (rule conjI)
 apply (simp add: addPos_def p_def)

 apply (simp add: p_def)
 apply (case_tac "stk::val list")
 apply simp
 apply simp

 apply simp
 apply (rule_tac x="And [Pos p, Neg (St 0 \<doteq> FF)]" in exI)
 apply (simp add: addPos_def) 
 apply (case_tac "stk::val list")
 apply simp
 apply (simp add: p_def)
 done


next 
 case Throw
 from this main_prems show ?thesis
 apply (simp add: main_simps del: option.splits, clarify)
 apply (case_tac "hd stk = Null")
 apply simp

 apply simp
 done
 qed
 qed
}
qed
(*>*)

end