header {* 
  \isaheader{Branch conditions guarantee progress} 
*}

theory JBC_succsFprogress = JBC_VCG_Correctness:


(*<*)
declare map_fst_tuple[simp]
declare image_fst_tuple [simp]
(*>*)


lemma catchstate_find_handler:
"\<And> st rg C M pc e stk. \<lbrakk> 
wf (P,An); 
\<forall> p \<in> set (map (snd \<circ> snd) ((st,rg,(C,M,pc))#frs)). p \<in> set (domC (P,An)); (C',M',pc') \<in> set (domC (P,An));
catchstate (P,(cname_of h xa),((C,M,pc),(None,h,(st,rg,(C,M,pc))#frs),e)) = 
           ((C',M',pc'),(x',h',(st',rg',(C',M',pc'))#frs'),e');
JVMExceptions.match_ex_table P (cname_of h xa) pc' (ex_table_of P C' M') = Some (pch,d);
JVMExceptions.match_ex_table P (cname_of h xa) pc (ex_table_of P C M) = None
 \<rbrakk> \<Longrightarrow> find_handler P xa h ((stk,rg,(C,M,pc))#frs) = (None,h,([Addr xa],rg',(C',M',pch))#frs')"
(*<*)
apply (induct frs)
apply (subgoal_tac "d = 0")
 prefer 2
 apply (rule wf_match_ex_table_d)
 apply assumption
 apply (erule_tac x="(C,M,pc)" in ballE)
 apply (rule domC_methodnames)
 apply simp
 apply simp
 apply simp
apply simp

apply (subgoal_tac "d = 0")
 prefer 2
 apply (rule_tac X="(cname_of h xa)" and p="pc'" and h="pch" in wf_match_ex_table_d)
 apply assumption
 apply (rule domC_methodnames)
 apply simp
 apply simp
apply (subgoal_tac "\<exists> sta rga pa. a = (sta,rga,pa)")
 prefer 2
 apply (fastsimp)
apply (erule exE)+
apply (subgoal_tac "\<exists> Ca Ma pca. pa = (Ca,Ma,pca)")
 prefer 2
 apply (fastsimp)
apply (erule exE)+

apply (simplesubst find_handler_simp)
apply (simp (no_asm_simp) del: find_handler.simps)

apply atomize
apply (erule_tac x="sta" in allE)
apply (erule_tac x="rga" in allE)
apply (erule_tac x="Ca" in allE)
apply (erule_tac x="Ma" in allE)
apply (erule_tac x="pca" in allE)
apply (erule_tac x="e\<lparr>cs:= tl (cs e)\<rparr>" in allE)
apply (erule_tac x="sta" in allE)
apply (simp del: catchstate.simps find_handler.simps split del: option.split_asm)
apply (case_tac "frs")
apply simp
apply (drule_tac t="aa" in sym)
apply simp

apply (subgoal_tac "catchstate (P, cname_of h xa, (Ca, Ma, pca), (None, h, (sta, rga, Ca, Ma, pca) # aa # list), e\<lparr>cs := tl (cs e)\<rparr>)
                   =catchstate (P, cname_of h xa, (Ca, Ma, pca), (None, hd (cs e), (sta, rga, Ca, Ma, pca) # aa # list), e\<lparr>cs := tl (cs e)\<rparr>)")
 prefer 2
 apply (cut_tac catchstate_eq)
 apply (erule_tac x="P" in allE) 
 apply (erule_tac x="cname_of h xa" in allE)
 apply (erule_tac x="(Ca, Ma, pca)" in allE)
 apply (erule_tac x="None" in allE)
 apply (erule_tac x="h" in allE)
 apply (erule_tac x="hd (cs e)" in allE)
 apply (erule_tac x="(sta, rga, Ca, Ma, pca)" in allE)
 apply (erule_tac x="(sta, rga, Ca, Ma, pca)" in allE)
 apply (erule_tac x="aa" in allE)
 apply (erule_tac x="list" in allE) 
 apply (erule_tac x="e\<lparr>cs:=tl (cs e)\<rparr>" in allE)
 apply (simp only:)
apply (simp only:)
apply simp
apply (drule_tac t="ab" in sym)
apply simp
done
(*>*)


consts callchain::"jbc_prog \<Rightarrow> pos list \<Rightarrow> bool"
primrec 
"callchain \<Pi> [] = True"
"callchain \<Pi> (p#ps) = (case ps of [] \<Rightarrow> True
                       | p'#ps' \<Rightarrow> p \<in> set (callers \<Pi> p') \<and> callchain \<Pi> ps)"


lemma callchain_append:
"\<And> p ps'. callchain \<Pi> (ps@p#ps') = (callchain \<Pi> (ps@[p]) \<and> callchain \<Pi> (p#ps'))"
(*<*)
apply (induct ps)
apply simp

apply simp
apply (case_tac "ps @ p # ps'")
apply simp

apply (case_tac "ps @ [p]")
apply simp

apply simp

apply (atomize)

apply (erule_tac x="p" in allE)
apply (erule_tac x="ps'" in allE)
apply (subgoal_tac "aa = ab" )
 prefer 2
 apply (subgoal_tac "ps @ (p # ps') = (ps @ [p]) @ ps'")
  prefer 2
  apply (induct_tac ps)
  apply simp
  apply simp
 apply simp
apply (simp only: cong del: case_cong)
apply simp
done
(*>*)


lemmas succsXpt_def = succsXpt.simps

lemma succsXpt_simp: "succsXpt ((P, An), X, ps) =
(case length (domC (P, An)) \<le> length ps of True \<Rightarrow> map (\<lambda>p. (p, TT)) (domC (P, An))
 | False \<Rightarrow> case ps of [] \<Rightarrow> map (\<lambda>p. (p, TT)) (domC (P, An))
           | p # pss \<Rightarrow>
               let (C, M, pc) = p; et = ex_table_of P C M; A = aF (P, An) p
               in (case match_ex_table_e P X pc et of None \<Rightarrow> concat (map (\<lambda>p'. succsXpt ((P, An), X, p' # ps)) (callers (P, An) p))
                  | \<lfloor>en\<rfloor> \<Rightarrow> (let (f,t,X',pc',d) = en
                            in [((C, M, pc'), And ((if pss = [] then []
                            else [Catch X' A, Catch X (Pos p)])@[xcpt_cond (P, An) X (last ps)]))])))"
(*<*)
by  simp
(*>*)





lemma catchstate_form':
"\<And> p h e stk loc frs. \<exists> p' h' st' rg' frs' e'. catchstate (P,X,(p,(None,h,(stk,loc,p)#frs),e)) = (p',(None,h',(st',rg',p')#frs'),e')"
(*<*)
apply (subgoal_tac "\<exists> n.  length ((stk,loc,p)#frs) = n")
 prefer 2
 apply fastsimp
apply (erule exE)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch7)
apply (rule allI)
apply (rule_tac n="n" in nat_less_induct)
apply (rule allI)+
apply (case_tac "frs")
apply fastsimp

apply (subgoal_tac "\<exists> sta lca pa. a = (sta,lca,pa)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply simp
apply (rule impI)
apply (simp add: split_def)
apply (rule conjI)
apply (rule impI)

apply (erule_tac x="Suc (length list)" in allE)
apply simp
apply (erule_tac x="fst pa" in allE)
apply (erule_tac x="fst (snd pa)" in allE)
apply (erule_tac x="snd (snd pa)" 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 (erule_tac x="sta" in allE)
apply (erule_tac x="lca" in allE)
apply (erule_tac x="list" in allE)
apply simp

apply (rule impI)
apply fastsimp
done
(*>*)


lemma succsXpt_findhandler:
assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
assumes wf_Pi:"wf \<Pi>"
assumes p'_B_succsXpt:"(p',B) \<in> set (succsXpt (\<Pi>,X,[p]))"
assumes valid_B:"\<Pi>,s \<Turnstile> B"
assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
assumes X_def: "X = cname_of h xa"
assumes succsXpt_domC: "fst ` set (succsXpt (\<Pi>, X, [p])) \<subset> set (domC \<Pi>)"
shows 
"\<exists> rg' frs'. find_handler (fst \<Pi>) xa h ((st,rg,p)#frs) = (None,h,([Addr xa],rg',p')#frs')"
proof -

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

obtain C M pc
where p_def:"p = (C,M,pc)"
  by (cases "p")

from s_inv_Pos have 
callers_sysinv_s:"callers_sysinv (\<Pi>,s)"
  apply -
  apply (rule callers_sysinv_Pos)
  by (simp add: inv_Pos_def)

from callers_sysinv_s s_def
obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
  apply -
  apply (simp only: callers_sysinv_trans)
  apply (erule_tac x="0" in allE)
  apply (simp add: in_set_conv_decomp)
  apply (erule conjE | erule exE)+
  by fastsimp


have succsXpt_induct: 
  "\<And> k L. length (domC \<Pi>) - length L = k 
  \<Longrightarrow> fst ` set (succsXpt (\<Pi>, X, L)) \<subset> set (domC \<Pi>) 
  \<Longrightarrow> (\<exists>L'. L = L' @ [p]) 
  \<Longrightarrow> (p', B) \<in> set (succsXpt (\<Pi>, X, L)) 
  \<Longrightarrow> (\<forall>(C', M', pc')\<in>set (tl L). JBC_VCG.match_ex_table P X pc' (ex_table_of P C' M') = None) 
  \<Longrightarrow> callchain \<Pi> L \<Longrightarrow> 
  \<exists> rg' frs'. find_handler P xa h ((st,rg,p)#frs) = (None,h,([Addr xa],rg',p')#frs')" (is "\<And>k. PROP ?P k")
proof -
  fix k show "PROP ?P k"
  proof (induct "k" rule: nat_less_induct)
    case (1 n)
    assume IH:"\<forall>m<n. \<forall>x. length (domC \<Pi>) - length x = m \<longrightarrow>
      fst ` set (succsXpt (\<Pi>, X, x)) \<subset> set (domC \<Pi>) \<longrightarrow>
      (\<exists>L'. x = L' @ [p]) \<longrightarrow>
      (p', B) \<in> set (succsXpt (\<Pi>, X, x)) \<longrightarrow>
      (\<forall>(C', M', pc')\<in>set (tl x). JBC_VCG.match_ex_table P X pc' (ex_table_of P C' M') = None) \<longrightarrow>
      callchain \<Pi> x \<longrightarrow> (\<exists> rg' frs'. find_handler P xa h ((st,rg,p)#frs) = (None,h,([Addr xa],rg',p')#frs')) "
    assume length_L_n:"length (domC \<Pi>) - length L = n"
    assume succsX_domC:"fst ` set (succsXpt (\<Pi>, X, L)) \<subset> set (domC \<Pi>)"
    assume appL_L':"\<exists>L'. L = L' @ [p]"
    assume p'_B_succsX_L:"(p', B) \<in> set (succsXpt (\<Pi>, X, L))"
    assume match_ex_tab_L:"\<forall>u\<in>set (tl L). (\<lambda>(C', M', pc'). JBC_VCG.match_ex_table P X pc' (ex_table_of P C' M') = None) u"
    assume callchain_L: "callchain \<Pi> L"	 
    show "\<exists> rg' frs'. find_handler P xa h ((st,rg,p)#frs) = (None,h,([Addr xa],rg',p')#frs')"
    proof -
      
      from succsX_domC have domC_L:"\<not> (length (domC \<Pi>) \<le> length L)" 
	by (simp add: succsXpt.simps Pi_def split add: bool.split_asm)
      
      from succsX_domC domC_L appL_L' obtain Ca Ma pca list where L_cons: "L = (Ca,Ma,pca)#list"
	apply (case_tac "L = []")
	apply simp
	apply (simp add: neq_Nil_conv, (erule exE)+,blast)
	done

      show ?thesis
      proof (cases "JVMExceptions.match_ex_table P X pca (ex_table_of P Ca Ma)")
	case None
	from None domC_L L_cons p'_B_succsX_L Pi_def
	have succsXpt_rec: "(\<exists>a\<in>set (callers \<Pi> (Ca, Ma, pca)). (p',B) \<in> set (succsXpt (\<Pi>, X, a # (Ca, Ma, pca) # list)))"
	  apply (simp only: Pi_def)
	  apply (drule_tac P="\<lambda> S.  (p', B) \<in> set S" in  subst[OF succsXpt_simp])
	  apply (simp del: succsXpt.simps  split del: option.split_asm)
	  apply (simp add: set_concat_map split_def del: succsXpt.simps )
	  apply (drule match_ex_table_e_sim)
	  apply simp
	  done

	from succsXpt_rec obtain a
	  where succsXpt_rec':"  
	  a\<in>set (callers \<Pi> (Ca, Ma, pca)) 
	  \<and> (p',B) \<in> set (succsXpt (\<Pi>, X, a # (Ca, Ma, pca) # list))"
	  apply blast
	  done
		
	from length_L_n  L_cons domC_L have length_a_L :"length (domC \<Pi>) - length (a # (Ca, Ma, pca) # list) < n"
	  by (simp, arith)
	
	from succsXpt_rec' succsX_domC L_cons domC_L None
	have succsX_a_domC: "fst ` set (succsXpt (\<Pi>, X, a # (Ca, Ma, pca) # list)) \<subset> set (domC \<Pi>)"
	  apply simp
	  apply (erule conjE)+
	  apply (simp only: in_set_conv_decomp)
	  apply (erule exE)+
	  apply (simp add: Pi_def image_Un)  
	  apply (simp only: insert_def) 
	  apply (drule un_subset_drop', assumption)
	  apply (drule match_ex_table_e_sim)
	  apply simp
	  done

	from L_cons have appL_L'_a: "(\<exists>L'. a # ((Ca, Ma, pca) # list) = L' @ [p])"
	  apply (cut_tac appL_L')
	  apply (erule exE)
	  apply (rule_tac x="a # L'" in exI)
	  apply simp	
	  done

	from succsX_a_domC succsXpt_rec' length_a_L IH length_L_n succsX_domC L_cons None
          p'_B_succsX_L match_ex_tab_L callchain_L 
	show ?thesis
	  apply simp
	  apply (erule_tac x="length (domC \<Pi>) - length (a # (Ca, Ma, pca) # list)" in allE)
	  apply simp
	  apply (erule_tac x="a # (Ca, Ma, pca) # list" in allE)
	  apply simp
	  apply (cut_tac appL_L'_a)
	  apply (drule mp, assumption)
	  apply simp
	  done

      next

	case (Some "aa")
        from L_cons appL_L' callchain_L have domC_Ca_Ma_pca:"(Ca,Ma,pca) \<in> set (domC \<Pi>)" 
	proof (cases list)
	  case Nil
	  from Nil L_cons appL_L' 
	  show ?thesis 
            by (simp add: domC_p)

	next
	  case Cons
	  from Cons callchain_L  L_cons appL_L' show ?thesis
            by (simp add: callers_def)
	qed		   
		 from Some wf_Pi p_def domC_Ca_Ma_pca Pi_def 
		 have snd_aa_0:"snd aa = 0"
		   apply (rule_tac d="snd aa" and P="P" and An="An" and C="Ca" and M="Ma"
		      and h="fst aa" and p="pca" and X="X" in wf_match_ex_table_d)
		   apply (simp add: wf_def Pi_def)
		   apply (rule_tac pc="pca" and An="An" in domC_methodnames, simp)
		   apply simp
		   done
		 from appL_L' have last_L_p: "last L = p" 
		   by fastsimp
	
	
		 from p'_B_succsX_L succsX_domC appL_L' Pi_def 
		 have B'_xcpt_cond: "\<exists> As. B = And (As@[xcpt_cond (P,An) X p])"
		   apply -
		   apply (rule_tac L="L" and p'="p'" in succsXpt_xcpt_cond)
		   apply simp 
		   apply simp
		   apply simp
		   done
 
		 from p'_B_succsX_L valid_B B'_xcpt_cond 
		 have valid_xcpt_cond: "\<Pi>,s \<Turnstile> (xcpt_cond \<Pi> X p)"
		   apply -
		   apply (erule exE)+
		   apply (simp add: Pi_def del: succsXpt.simps)
		   apply (simp add: evalEs_map)
		   done

		 show ?thesis 
		 proof (cases list rule:rev_cases[consumes 1,case_names "rev_Nil" "rev_cons"])
		   case rev_Nil
		   from rev_Nil appL_L' L_cons p_def have p_def': "(Ca,Ma,pca) = (C,M,pc)"
		     by simp

		   from Some rev_Nil p_def' p_def snd_aa_0 X_def
		   have find_handler_p:"find_handler P xa h ((st,rg,p)#frs) = 
		     (None,h,([Addr xa],rg,(C,M,fst aa))#frs)"
		     apply -
		     apply simp
		     done

		   from Some obtain en 
		     where en_intro: "match_ex_table_e P X pca (ex_table_of P Ca Ma) = \<lfloor>en\<rfloor>" 
                     and en_def: "snd (snd (snd en)) = aa"
		     apply -
		     apply (drule match_ex_table_e_sim2)
		     apply (erule exE | erule conjE)+
		     apply fastsimp
		     done

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

                   
                   from p_def p_def' rev_Nil L_cons p'_B_succsX_L en_def en_intro Pi_def succsX_domC
		   have p'_def: "p' = (C,M,fst aa)"
		     apply -
		     apply simp
		     apply (case_tac "length (domC (P, An)) \<le> Suc 0")
		     apply simp

		     apply (simp add: split_def split del: option.split_asm)
		     done
		    
		     from find_handler_p p'_def show ?thesis 
		       by fastsimp

		 next
		   case (rev_cons "ys" "y")
		   from rev_cons L_cons have L_cons': "L = (Ca,Ma,pca)#ys@[p]"
		     apply simp
		     apply (cut_tac appL_L')
		     apply (erule exE)
		     apply simp
		     done
		   
		   from L_cons' match_ex_tab_L p_def 
		   have no_match_p: "JVMExceptions.match_ex_table P X pc (ex_table_of P C M) = None"
		     by simp

		    from Some obtain en 
		     where en_intro: "match_ex_table_e P X pca (ex_table_of P Ca Ma) = \<lfloor>en\<rfloor>" 
                     and en_def: "snd (snd (snd en)) = aa"
		     apply -
		     apply (drule match_ex_table_e_sim2)
		     apply (erule exE | erule conjE)+
		     apply fastsimp
		     done

		   from en_def 
		   obtain f t X' where en_def: "en = (f,t,X',aa)"
		     apply (cases en)
		     by fastsimp
		   
		   from en_def en_intro domC_L L_cons'  p'_B_succsX_L 
		   have p'_B_def:"p' = (Ca, Ma, fst aa) \<and> 
		        B = And [Catch X' (aF (P, An) (Ca, Ma, pca)), Catch X (Pos (Ca, Ma, pca)), 
                                             xcpt_cond (P, An) X p]"
		     apply -
		     apply (simp only: Pi_def)
		     apply (drule_tac P="\<lambda> S. (p', B) \<in>  (set S)" in  
		       subst[OF succsXpt_simp[of "P" "An" "X" "(Ca,Ma,pca)#(ys@[p])"]])
		     apply (simp del: succsXpt.simps)
		     apply (simp add: split_def)
		     done

		   
		   from Pi_def s_def obtain cp ch cst crg cfrs ce 
		   where catchstate_s: "catchstate (P, X, s) = (cp, (None, ch, (cst, crg, cp) # cfrs), ce)" 
		     apply -
		     apply (subgoal_tac "\<exists>p' h' st' rg' frs' e'. catchstate (P, X, s) = (p', (None, h', (st', rg', p') # frs'), e')")
		      prefer 2
		      apply (simp only:)
		      apply (rule catchstate_form')
		     apply (erule exE)+
		     apply blast
		     done
	  

		   from Pi_def catchstate_s p'_B_def valid_B s_def
		   have cp_simp: "cp = (Ca,Ma,pca)"
		     apply (simp del: catchstate.simps)
		     apply (case_tac "frs")
		     apply simp

		     apply simp
		     done

		 
		   from callers_sysinv_s s_def p_def Pi_def 
		   have frs_domC: "\<forall>p\<in>set (map (snd \<circ> snd) ((st, rg, C, M, pc) # frs)). p \<in> set (domC (P, An))"
		     apply -
		     apply (simp add: callers_sysinv_trans del: callers_sysinv.simps)
		     apply (case_tac "frs")
		     apply (simp add: mem_iff)
		     
		     apply (erule conjE)+
		     apply (rule ballI)
		     apply (subgoal_tac "\<exists> frs1 frs2. frs = frs1 @ pa#frs2")
		      prefer 2
		      apply (simp only: in_set_conv_decomp)
		     apply (erule exE)+
		     apply (erule_tac x="length frs1" in allE)
		     apply (drule_tac t="a # list" in sym)
		     apply (simp add: nth_append)
		     done

		   from cp_simp catchstate_s domC_Ca_Ma_pca s_def frs_domC wf_Pi Pi_def no_match_p Some p_def X_def
		   have find_handler_s: "find_handler P xa h ((st,rg,(C,M,pc))#frs) = 
		                         (None,h,([Addr xa],crg,(Ca,Ma,fst aa))#cfrs)"
		     apply - 
		     apply (rule_tac P="P" and C="C" and M="M" and xa="xa" and h="h" and e="e" and d="snd aa"
		            and stk="st" and rg="rg" and rg'="crg" and C'="Ca" and M'="Ma" and pch="fst aa" and x'="None" and frs'="cfrs"
		            and An="An" and st="st" and frs="frs" and pc'="snd (snd cp)" and st'="cst" and h'="ch" and e'="ce"
		            in catchstate_find_handler)
		     apply (simp add: wf_def)

		     apply assumption

		     apply simp

		     apply simp
		     		     
		     apply simp

		     apply simp
		     done

		   from p_def rev_cons L_cons p'_B_succsX_L en_def en_intro Pi_def succsX_domC
		   have p'_def: "p' = (Ca,Ma,fst aa)"
		     apply -
		     apply simp
		     apply (case_tac "length (domC (P, An)) \<le> Suc 0")
		     apply simp

		     apply (case_tac "length (domC (P, An)) \<le> Suc (Suc (length ys))")
		     apply simp

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

		   from find_handler_s p'_def p_def
		   show ?thesis
		     by fastsimp
		 qed
	       qed
	     qed
	   qed
	 qed

from succsXpt_induct[where k="length (domC \<Pi>) - 1" and L="[p]"] 
     succsXpt_domC p'_B_succsXpt Pi_def
show ?thesis
  by (simp del: find_handler.simps)
qed


lemma succsF_progress_Throw:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
 (* assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some Throw"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -

  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  from cmd_p Pi_def wf_Pi p_def
  have instr_p:"instrs_of P C M ! pc = Throw"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

 obtain i where i_def: "i = Throw"
   by fastsimp

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done

  from check_s s_def  p_def instr_p i_def obtain r rst 
   where st_def:"st = r#rst" 
   and is_Ref_r:"is_Ref' h r"
   apply (simp add: neq_Nil_conv split_def)
   apply (erule conjE | erule exE)+
   apply atomize
   apply (erule_tac x="y" in allE)
   apply (erule_tac x="ys" in allE)
   apply simp
   done
    
  from s_inv_ExTys s_def have cname_sysxcpt: "(cname_of h (addr_of_sys_xcpt NullPointer)) = NullPointer"
    apply (simp add: inv_ExTys_def obj_ty_def)
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    show ?thesis
      apply (simp add: succsNormal_def)
      done
  
  next
   
    assume xcpt: "?xcpt"


    from wf_Pi cmd_p domC_p
    obtain A tys where wf_Throw:"anF \<Pi> p = Some A 
    \<and> extractTy (A,St 0) = tys \<and> tys \<noteq> [] \<and> (\<forall> tp\<in> (set tys). \<exists> XA. tp = Class XA) \<and> p \<noteq> ipc \<Pi>"
      apply (simp add: wf_def JBC_VCG.wf_def checkPos_split  split_if[of "\<lambda> x. x" _ _ "False"])
      apply (case_tac "anF \<Pi> p")
      apply simp

      apply (case_tac "p = ipc \<Pi>")
      apply simp
      
      apply simp
      apply atomize
      apply (erule_tac x="a" in allE)
      apply (erule_tac x="extractTy (a,St 0)" in allE)
      apply (erule conjE)+
      apply (case_tac "extractTy (a,St 0)")
      apply simp

      apply (simp only: list.cases if_False)
      apply (drule_tac t="aa # list" in sym)
      apply (simp only: list_all_iff)
      apply (subgoal_tac "(\<forall>tp\<in>set (extractTy (a, St 0)). \<exists>XA. tp = Class XA)")
       prefer 2
       apply (rule ballI)
       apply (erule_tac x="tp" in ballE)
        prefer 2
	apply simp
       apply (case_tac "tp")
       apply simp
       apply simp
       apply simp
       apply simp
       apply simp
      apply (drule_tac t="extractTy (a, St 0)" in sym)
      apply simp
      done

(*
    from this valid_An s_def
    have s_A :"\<Pi>,s \<Turnstile> A"
      by simp
*)
    from wf_Throw
    have anF_p: "anF \<Pi> p = Some A"
      by simp

(*
    from wf_Throw s_def wf_Pi cmd_p domC_p s_A
    have r_ty': "\<exists>tp \<in> set (extractTy (A,St 0)). \<Pi>,s \<Turnstile> Ty (St 0) tp"
      apply (rule_tac A="A" and tys="(extractTy (A,St 0))" in extractTy_sem)
      apply (simp add: assert_def)
      apply simp
      apply simp
      done

    from r_ty' wf_Throw
    obtain XA where r_ty: "\<Pi>,s \<Turnstile> Ty (St 0) (Class XA) \<and> Class XA \<in> set (extractTy (A,St 0))"
      apply atomize
      apply (erule bexE)
      apply (erule conjE)+
      apply (erule_tac x="tp" in ballE)
       prefer 2
       apply simp
      apply (erule exE)
      apply (erule_tac x="XA" in allE)
      apply simp
      done
 *)
    
    from xcpt s_def cmd_p i_def anF_p
    have succsExcept_exp: 
      "set (succsExcept \<Pi> p) =  set (succsXpt (\<Pi>, NullPointer, [p])) \<union> 
        (\<Union>a\<in>set (extractTy (A,St 0)). set (case a of Class X \<Rightarrow> succsXpt (\<Pi>, X, [p]) | _ \<Rightarrow> []))"  
      by (simp add: image_Un cmd_p succsExcept_def split del: option.split_asm)
    
    from wf_Pi domC_p have succsExcept_domC:
      "fst ` (set (succsExcept \<Pi> p)) \<subset> set (domC \<Pi>)"
     by (simp add: wf_def JBC_VCG.wf_def checkPos_split split_if[of "\<lambda> x. x" _ _ "False"] )
    
   from xcpt wf_Throw
    have xcpt_cases: 
      "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsXpt (\<Pi>, NullPointer, [p])) \<or>
       (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` (\<Union>a\<in>set (extractTy (A,St 0)). set (case a of Class X \<Rightarrow> succsXpt (\<Pi>, X, [p]) | _ \<Rightarrow> []))" (is "?NP \<or> ?XA")
     by (simp add: image_Un cmd_p succsExcept_def split del: option.split_asm)

    from xcpt_cases show ?thesis 
     proof
       assume np_case:
       "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsXpt (\<Pi>, NullPointer, [p]))"
       show ?thesis
	 proof -

	   from np_case obtain B'
	     where p'_B'_succsXpt: "(p',B') \<in> set (succsXpt (\<Pi>,NullPointer,[p]))"
	     and B_def: "B = And [Pos p,B']"
	     apply -
	     apply (erule imageE)
	     apply (simp add: split_def)
	     by fastsimp

	   from xcpt succsExcept_domC cmd_p
	   have succsXpt_domC: "fst ` (set (succsXpt (\<Pi>,NullPointer,[p]))) \<subset> set (domC \<Pi>)"
	     apply -
	     apply (simp add: succsExcept_def)
	     apply blast
	     done

	   from p'_B'_succsXpt succsXpt_domC Pi_def
	   have B'_xcpt_cond: "\<exists> As. B' = And (As@[xcpt_cond (P,An) NullPointer p])"
	     apply -
	     apply (rule_tac X="NullPointer" and L="[p]" and p'="p'" in succsXpt_xcpt_cond)
	     apply simp 
	     apply simp
	     apply simp
	     done

	   from p'_B'_succsXpt valid_B B_def B'_xcpt_cond 
	   have valid_xcpt_cond: "\<Pi>,s \<Turnstile> (xcpt_cond \<Pi> NullPointer p)"
	     apply -
	     apply (erule exE)+
	     apply (simp add: Pi_def del: succsXpt.simps)
	     apply (erule conjE)+
	     apply (simp add: evalEs_map)
	     done

	   from st_def s_def is_Ref_r valid_xcpt_cond cmd_p
	   have exec_instr_s: "exec_instr Throw P h st rg C M pc frs = 
             (Some (if r = Null then addr_of_sys_xcpt NullPointer else (the_Addr r)),h,(st,rg,(C,M,pc))#frs)"
	     apply (simp add: split_def xcpt_cond_def)
(*
	     apply (rule impI)
	     apply (case_tac "r::val")
	     apply simp
	     apply simp
	     apply simp
	     apply simp
	     apply simp
*)
	     done

	   from st_def s_def is_Ref_r valid_xcpt_cond cmd_p
	   have cname_r: "cname_of h ((if r = Null then addr_of_sys_xcpt NullPointer else (the_Addr r))) 
                          = NullPointer"
	     apply (simp add: xcpt_cond_def)
	     apply (case_tac "r::val")
	     apply simp+
	     apply (rule cname_sysxcpt)
	     apply (simp add: obj_ty_def)+
	     done

	   from s_def wf_Pi p'_B'_succsXpt valid_B B_def s_inv_Pos cname_r succsXpt_domC Pi_def p_def
	   obtain rg' frs'
	     where find_handler_s: "find_handler P (if r = Null then addr_of_sys_xcpt NullPointer else (the_Addr r)) h ((st, rg, p) # frs) = (None, h, ([Addr (if r = Null then (addr_of_sys_xcpt NullPointer) else (the_Addr r))], rg', p') # frs')"
	     apply -
	     apply (drule_tac xa="(if r = Null then (addr_of_sys_xcpt NullPointer) else (the_Addr r))" in succsXpt_findhandler)
	     apply assumption
	     apply assumption
	     apply simp
	     apply assumption
	     apply simp
	     apply assumption
	     apply (erule exE)+
	     by fastsimp
 
	   from Pi_def p_def instr_p has_method_p exec_instr_s find_handler_s cname_sysxcpt s_def
	   have s_effS: "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,([Addr (if r = Null then (addr_of_sys_xcpt NullPointer) else (the_Addr r))],rg',p')#frs'),
	                 e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>)) \<in> effS \<Pi>" 
	     apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Throw"  and loc'="rg'"
	       and h="h" and xa="if r = Null then (addr_of_sys_xcpt NullPointer) else (the_Addr r)"  and frs="frs" and frs'="frs'" and bla="(st, rg, C, M, pc) # frs" and h'="h" in effS.expt)
	     apply simp
	     
	     apply simp

	     apply simp
	     
	     apply simp
		     
	     apply simp

	     apply simp

	     apply simp

	     apply simp

	     apply simp
	     done

	   from s_effS s_def 
	   show ?thesis
	     by fastsimp
	 qed
       
       next

       assume norm_case:

          "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` (\<Union>a\<in>set (extractTy (A,St 0)). set (case a of Class X \<Rightarrow> succsXpt (\<Pi>, X, [p]) | _ \<Rightarrow> []))"
   
      from valid_B cmd_p wf_Throw norm_case xcpt succsExcept_exp succsExcept_domC 
      obtain XA where succsXpt_XA:
       "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsXpt (\<Pi>, XA, [p]))" and XA_extractTy:"Class XA \<in> set (extractTy (A,St 0))"
	 apply  -
	 apply (erule conjE)+
	 apply (erule imageE)
	 apply (simp add: succsExcept_def)
	 apply (erule bexE)
	 apply (case_tac "a")
	 apply simp+
	 apply fastsimp
	done

        from succsXpt_XA obtain B'
	  where p'_B'_succsXpt: "(p',B') \<in> set (succsXpt (\<Pi>,XA,[p]))"
	  and B_def: "B = And [Pos p,B']"
	     apply -
	     apply (erule imageE)
	     apply (simp add: split_def)
	     by fastsimp

	   from wf_Throw XA_extractTy
	   obtain tys1 tys2 
	     where tys_def: "tys = tys1@(Class XA)#tys2"
	     apply -
	     apply (erule conjE)+
	     apply (simp add: in_set_conv_decomp)
	     apply fastsimp
	     done 

	   from wf_Throw
	   have extractTy_A: "extractTy (A, St 0) = tys"
	     by simp

	   from xcpt succsExcept_domC cmd_p p'_B'_succsXpt B_def tys_def anF_p extractTy_A
	   have succsXpt_domC: "fst ` (set (succsXpt (\<Pi>,XA,[p]))) \<subset> set (domC \<Pi>)"
	     apply -
	     apply (simp add: succsExcept_def split del: option.split_asm)
	     apply (erule conjE | erule exE | erule imageE)+
	     apply blast
	     done

	   from p'_B'_succsXpt succsXpt_domC Pi_def
	   have B'_xcpt_cond: "\<exists> As. B' = And (As@[xcpt_cond (P,An) XA p])"
	     apply -
	     apply (rule_tac X="XA" and L="[p]" and p'="p'" in succsXpt_xcpt_cond)
	     apply simp 
	     apply simp
	     apply simp
	     done

	   from p'_B'_succsXpt valid_B B_def B'_xcpt_cond 
	   have valid_xcpt_cond: "\<Pi>,s \<Turnstile> (xcpt_cond \<Pi> XA p)"
	     apply -
	     apply (erule exE)+
	     apply (simp add: Pi_def del: succsXpt.simps)
	     apply (erule conjE)+
	     apply (simp add: evalEs_map)
	     done

	   from st_def s_def is_Ref_r valid_xcpt_cond cmd_p
	   have exec_instr_s: "exec_instr Throw P h st rg C M pc frs = 
           (Some (if r = Null then addr_of_sys_xcpt NullPointer else the_Addr r),h,(st,rg,(C,M,pc))#frs)"
	     apply (simp add: split_def xcpt_cond_def)
	     done

	   from st_def s_def is_Ref_r valid_xcpt_cond cmd_p
	   have cname_r: "cname_of h (if r=Null then addr_of_sys_xcpt NullPointer else the_Addr r) = XA"
	     apply simp
	     apply (case_tac "r::val")
	     apply (simp add: is_Ref'_def)+
	     apply (simp add: xcpt_cond_def)
	     apply (case_tac "XA = NullPointer")
	     apply simp
	     apply (rule cname_sysxcpt)
	     apply simp
	     apply (simp add: is_Ref'_def)+
	     apply (erule exE)+
	     apply (simp add: xcpt_cond_def obj_ty_def)
	     apply (case_tac "XA = NullPointer")
	     apply simp
	     apply simp
	     done

	   from s_def wf_Pi p'_B'_succsXpt valid_B B_def s_inv_Pos cname_r succsXpt_domC Pi_def p_def
	   obtain rg' frs'
	     where find_handler_s: "find_handler P (if r = Null then addr_of_sys_xcpt NullPointer else the_Addr r) h 
             ((st, rg, p) # frs) = (None, h, ([Addr (if r = Null then addr_of_sys_xcpt NullPointer else the_Addr r)], rg', p') # frs')"
	     apply -
	     apply (drule_tac xa="(if r = Null then addr_of_sys_xcpt NullPointer else the_Addr r)" in succsXpt_findhandler)
	     apply assumption
	     apply assumption
	     apply simp
	     apply assumption
	     apply simp
	     apply simp
	     apply (erule exE)+
	     by fastsimp
 

	   from Pi_def p_def instr_p has_method_p exec_instr_s find_handler_s cname_sysxcpt s_def
	   have s_effS: "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,
           ([Addr (if r = Null then addr_of_sys_xcpt NullPointer else the_Addr r)],rg',p')#frs'),
	                 e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>)) \<in> effS \<Pi>" 
	     apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Throw"  and loc'="rg'"
	       and h="h" and xa="if r = Null then addr_of_sys_xcpt NullPointer else (the_Addr r)"  and frs="frs" and frs'="frs'" and bla="(st, rg, C, M, pc) # frs" and h'="h" in effS.expt)
	     apply simp
	     
	     apply simp

	     apply simp
	     
	     apply simp
		     
	     apply simp

	     apply simp

	     apply simp

	     apply simp

	     apply simp
	     done

	   from s_effS s_def 
	   show ?thesis
	     by fastsimp
	 qed
       qed
     qed

	  
lemma succsF_progress_Invoke:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
 (* assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (Invoke Mn n)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B  cmd_p
  
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
    by (simp add: addPos_def succsF_def)
  
  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = Invoke Mn n"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done

  from check_s s_def p_def instr_p i_def obtain args r rst 
   where st_def:"st = args@r#rst" 
   and length_args:"length args = n" 
   and is_Ref_r:"is_Ref' h r"
   apply atomize
   apply (simp add: neq_Nil_conv check_def split_def)
   apply (erule conjE | erule exE)+
   apply (drule_tac n="n" in list_length_split)
   apply (erule conjE | erule exE)+
   apply (erule_tac x="ls" in allE)
   apply (erule_tac x="l" in allE)
   apply (subgoal_tac "is_Ref' h l")
    prefer 2
    apply (simp add: is_Ref'_def nth_append)
    apply (case_tac "l = Null")
    apply simp

    apply (simp add: is_Ref'_def)
    done

  from is_Ref_r obtain adr obj 
   where r_def: "r = Null \<or> (r = Addr adr \<and> h adr = Some obj)"
   by (simp only: is_Ref'_def, case_tac "r::val",simp,simp,simp,simp,simp add: not_None_eq,blast)

  from r_def st_def length_args is_Ref_r check_s p_def i_def Pi_def obtain cn cn' 
   where classnames_obj: "(r \<noteq> Null) \<longrightarrow> classnames P = cn@[fst obj]@cn'"
   apply (subgoal_tac "(r \<noteq> Null) \<longrightarrow> (\<exists> cn cn'. classnames P = cn@[fst obj]@cn')")
    prefer 2
    apply (rule impI)
    apply (simp add: nth_append)
    apply (simp only: TypeRel.has_method_def)
    apply (erule exE)+
    apply (drule sees_method_is_class)
    apply (simp add: is_class_def class_def classnames_def)
    apply (erule exE)+
    apply (drule map_of_SomeD)
    apply (simp add: in_set_conv_decomp)
    apply (erule exE)+
    apply (simp add: map_append)
    apply (rule_tac x=" map fst ys" in exI)
    apply (rule_tac x="map fst zs" in exI)
    apply simp

    apply (case_tac "r = Null")
    apply simp

    apply atomize
    apply simp
    done

  from s_inv_ExTys s_def have cname_sysxcpt: "(cname_of h (addr_of_sys_xcpt NullPointer)) = NullPointer"
    apply (simp add: inv_ExTys_def obj_ty_def)
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"

    from cmd_p nrml valid_B s_def wf_Pi have
      p'_B_def': "\<exists> A. anF \<Pi> p = Some A \<and> (\<exists> tp \<in> (set (extractTy (A,St n))). (\<exists> X. tp = Class X \<and> p' = (X,Mn,0) \<and>
                  B = And [Pos p,  And [Neg (St n \<doteq> Cn Null), Ty (St n) (Class X)]] \<and> JBC_Semantics.has_method (fst \<Pi>) X Mn))"
      apply -
      apply (simp add: JBC_VCG.wf_def checkPos_split domC_p split_if[of "\<lambda> x. x" _ _ "False"])
      apply (erule conjE)+
      apply (case_tac "anF \<Pi> p")
      apply simp
      
      apply (rule_tac x="a" in exI)
      apply simp
      
      apply (case_tac "p = ipc \<Pi>")
      apply simp

      apply simp

      apply (subgoal_tac "\<forall> tp \<in> set (extractTy (a,St n)). (\<exists> X. tp = Class X \<and> JBC_Semantics.has_method (fst \<Pi>) X Mn) \<or> tp = NT")
       prefer 2
       apply (case_tac "extractTy (a, St n)")
       apply simp
       
       apply (simp only: list.cases)
       apply (drule_tac t="aa # list" in sym)
       apply (simp only: list_all_iff)
       apply (rule ballI)
       apply (erule conjE)+
       apply (erule_tac x="tp" in ballE)
        prefer 2
	apply simp
       apply (case_tac "tp::ty")
       apply simp
       apply simp
       apply simp
       --{* tp = NT *}
       apply simp
       --{* tp = Class lista *}
       apply simp
       
      apply (simp add: succsNormal_def st_def length_args nth_append)
      apply (erule imageE)
      apply simp
      apply (erule bexE)
      apply (case_tac "aa::ty")
      apply simp
      apply simp
      apply simp
      apply simp
      --{* aa = Class list *}
      apply (simp add: xcpt_cond_def)
      apply (erule_tac x="Class list" in ballE)
      prefer 2
      apply simp

      apply (erule conjE)+
      apply simp

      apply (subgoal_tac "\<exists>Ts T m. method P list Mn = (list, Ts, T, m)")
       prefer 2
       apply (rule_tac An="An" in has_method_class)
       apply (cut_tac wf_Pi)
       apply (simp add: Pi_def)
       apply (cut_tac Pi_def)
       apply simp
      apply (erule exE)+
      apply (cut_tac Pi_def)
      apply simp
      done

   from p'_B_def' obtain A X where  
   p'_B_def:"p' = (X,Mn,0) \<and> 
      B = And [Pos p,  And [Neg (St n \<doteq> Cn Null), Ty (St n) (Class X)]] \<and> Class X \<in> (set (extractTy (A,St n))) \<and> has_method (fst \<Pi>) X Mn"
     apply -
     apply atomize
     apply (erule exE | erule conjE)+
     apply (erule bexE)
     apply (erule exE)
     apply (erule_tac x="X" in allE)
     apply (erule_tac x="A" in allE)
     apply simp
     done

   from st_def length_args p'_B_def valid_B s_def r_def wf_Pi
   have exec_instr_s: "exec_instr (Invoke Mn n) P h st rg C M pc frs = (None,h,([],Addr adr # rev args @ replicate (fst (snd (snd (snd (snd (method P (fst obj) Mn)))))) arbitrary,(X,Mn,0))#(st,rg,(C,M,pc))#frs)"
    apply (simp add: split_def nth_append obj_ty_def)
    apply (erule conjE )+
    apply (simp add: Pi_def has_method_def mem_iff)
    apply (frule methodnames_P)
    apply (subgoal_tac "method  P (fst obj) Mn = method' P (fst obj) Mn")
     prefer 2
     apply (rule_tac wf_md="wf_md_Ty" in  method_method')
     apply (drule wf_wfprog)
     apply simp
     apply assumption
    apply (erule conjE | erule exE)+
    apply (simp add: method'_def)
    done

    from Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def st_def r_def s_def i_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,([],Addr adr # rev args @ replicate (fst (snd (snd (snd (snd (method P (fst obj) Mn)))))) arbitrary,(X,Mn,0))#(st,rg,(C,M,pc))#frs),e\<lparr>cs:=h#(cs e)\<rparr>)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Invoke Mn n"
                    and fr'="([],Addr adr # rev args @ replicate (fst (snd (snd (snd (snd (method P (fst obj) Mn)))))) arbitrary,(X,Mn,0))"
		    and h="h" and h'="h" and frs="frs" and frs'="(st,rg,(C,M,pc))#frs" in effS.nrml)
    apply simp
    apply simp
    apply simp
    apply simp
    apply simp
    apply simp
    apply simp
    apply simp
    apply simp
    done

    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next

    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
    proof -
      
    from xcpt cmd_p obtain B'
    where p'_B'_succsXpt: "(p',B') \<in> set (succsXpt (\<Pi>,NullPointer,[p]))"
      and B_def: "B = And [Pos p,B']"
      apply -
      apply (simp add: succsExcept_def)
      apply (erule imageE)
      apply (simp add: split_def)
      by fastsimp

    from wf_Pi domC_p have succsExcept_domC:
      "fst ` (set (succsExcept \<Pi> p)) \<subset> set (domC \<Pi>)"
      by (simp add: wf_def JBC_VCG.wf_def checkPos_split split_if[of "\<lambda> x. x" _ _ "False"] )
    
    from xcpt succsExcept_domC cmd_p
    have succsXpt_domC: "fst ` (set (succsXpt (\<Pi>,NullPointer,[p]))) \<subset> set (domC \<Pi>)"
      apply -
      apply (simp add: succsExcept_def)
      done

    from p'_B'_succsXpt succsXpt_domC Pi_def
    have B'_xcpt_cond: "\<exists> As. B' = And (As@[xcpt_cond (P,An) NullPointer p])"
      apply -
      apply (rule_tac X="NullPointer" and L="[p]" and p'="p'" in succsXpt_xcpt_cond)
      apply simp 
      apply simp
      apply simp
      done

    from p'_B'_succsXpt valid_B B_def B'_xcpt_cond 
    have valid_xcpt_cond: "\<Pi>,s \<Turnstile> (xcpt_cond \<Pi> NullPointer p)"
      apply -
      apply (erule exE)+
      apply (simp add: Pi_def del: succsXpt.simps)
      apply (erule conjE)+
      apply (simp add: evalEs_map)
      done

    from st_def s_def is_Ref_r valid_xcpt_cond cmd_p i_def length_args
    obtain bla
    where exec_instr_s: "exec_instr i P h st rg C M pc frs = 
        (\<lfloor>addr_of_sys_xcpt NullPointer\<rfloor>, h,bla)"
      apply (simp add: split_def xcpt_cond_def)
      done

    from s_def s_inv_ExTys
    have cname_r: "cname_of h (addr_of_sys_xcpt NullPointer) = NullPointer"
      by (simp add: inv_ExTys_def obj_ty_def)


    from s_def wf_Pi p'_B'_succsXpt valid_B B_def s_inv_Pos cname_r succsXpt_domC Pi_def p_def
    obtain rg' frs'
      where find_handler_s: "find_handler P (addr_of_sys_xcpt NullPointer) h ((st, rg, p) # frs) = 
      (None, h, ([Addr (addr_of_sys_xcpt NullPointer)], rg', p') # frs')"
      apply -
      apply (drule_tac xa="addr_of_sys_xcpt NullPointer" in succsXpt_findhandler)
      apply assumption
      apply assumption
      apply simp
      apply assumption
      apply simp
      apply assumption
      apply (erule exE)+
      by fastsimp
 

    from Pi_def p_def instr_p has_method_p exec_instr_s find_handler_s cname_sysxcpt s_def i_def
    have s_effS: "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,([Addr (addr_of_sys_xcpt NullPointer)],rg',p')#frs'),
	                 e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>)) \<in> effS \<Pi>" 
      apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="i"  and loc'="rg'"
	       and h="h" and xa="(addr_of_sys_xcpt NullPointer)"  and frs="frs" and frs'="frs'" and 
               bla="bla" and h'="h" in effS.expt)
      apply simp
	     
      apply simp

      apply simp
      
      apply simp
		     
      apply simp

      apply simp

      apply simp

      apply simp

      apply simp
      done

    from s_effS s_def
    show ?thesis
      by fastsimp
  qed
qed
qed
(*>*)


lemma succsF_progress_New:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
 (* assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (New Cl)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B  cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)
  
 from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

   obtain i where i_def: "i = New Cl"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done

  from s_inv_ExTys s_def have cname_sysxcpt: "(cname_of h (addr_of_sys_xcpt OutOfMemory)) = OutOfMemory"
    apply (simp add: inv_ExTys_def obj_ty_def)
    done

  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p,  Neg (NewA 0 \<doteq> Cn Null)]"
      by (simp add: succsNormal_def xcpt_cond_def)
    from p'_B_def valid_B s_def
    have exec_instr_s: "exec_instr (New Cl) P h st rg C M pc frs = (None,h((the (new_Addr h)) \<mapsto> blank P Cl),(Addr (the (new_Addr h))#st,rg,(C,M,Suc pc))#frs)"
    by (simp add: split_def)

    from Pi_def p_def instr_p i_def exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h((the (new_Addr h)) \<mapsto> blank P Cl),(Addr (the (new_Addr h))#st,rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="New Cl"
                    and fr'="(Addr (the (new_Addr h))#st,rg,(C,M,Suc pc))"
		    and h="h" and h'="h((the (new_Addr h)) \<mapsto> blank P Cl)" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
 
    from xcpt cmd_p obtain B'
      where p'_B'_succsXpt: "(p',B') \<in> set (succsXpt (\<Pi>,OutOfMemory,[p]))"
      and B_def: "B = And [Pos p,B']"
      apply -
      apply (simp add: succsExcept_def)
      apply (erule imageE)
      apply (simp add: split_def)
      by fastsimp

    from wf_Pi domC_p have succsExcept_domC:
      "fst ` (set (succsExcept \<Pi> p)) \<subset> set (domC \<Pi>)"
      by (simp add: wf_def JBC_VCG.wf_def checkPos_split split_if[of "\<lambda> x. x" _ _ "False"] )
    
    from xcpt succsExcept_domC cmd_p
    have succsXpt_domC: "fst ` (set (succsXpt (\<Pi>,OutOfMemory,[p]))) \<subset> set (domC \<Pi>)"
      apply -
      apply (simp add: succsExcept_def)
      done

    from p'_B'_succsXpt succsXpt_domC Pi_def
    have B'_xcpt_cond: "\<exists> As. B' = And (As@[xcpt_cond (P,An) OutOfMemory p])"
      apply -
      apply (rule_tac X="OutOfMemory" and L="[p]" and p'="p'" in succsXpt_xcpt_cond)
      apply simp 
      apply simp
      apply simp
      done

    from p'_B'_succsXpt valid_B B_def B'_xcpt_cond 
    have valid_xcpt_cond: "\<Pi>,s \<Turnstile> (xcpt_cond \<Pi> OutOfMemory p)"
      apply -
      apply (erule exE)+
      apply (simp add: Pi_def del: succsXpt.simps)
      apply (erule conjE)+
      apply (simp add: evalEs_map)
      done

    from  s_def valid_xcpt_cond cmd_p i_def
    obtain bla
    where exec_instr_s: "exec_instr i P h st rg C M pc frs = 
        (\<lfloor>addr_of_sys_xcpt OutOfMemory\<rfloor>, h,bla)"
      apply (simp add: split_def xcpt_cond_def)
      done

    from s_def wf_Pi p'_B'_succsXpt valid_B B_def s_inv_Pos cname_sysxcpt succsXpt_domC Pi_def p_def
    obtain rg' frs'
      where find_handler_s: "find_handler P (addr_of_sys_xcpt OutOfMemory) h ((st, rg, p) # frs) = 
      (None, h, ([Addr (addr_of_sys_xcpt OutOfMemory)], rg', p') # frs')"
      apply -
      apply (drule_tac xa="addr_of_sys_xcpt OutOfMemory" in succsXpt_findhandler)
      apply assumption
      apply assumption
      apply simp
      apply assumption
      apply simp
      apply assumption
      apply (erule exE)+
      by fastsimp
 
    from Pi_def p_def instr_p has_method_p exec_instr_s find_handler_s cname_sysxcpt s_def i_def
    have s_effS: "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,([Addr (addr_of_sys_xcpt OutOfMemory)],rg',p')#frs'),
	                 e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>)) \<in> effS \<Pi>" 
      apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="i"  and loc'="rg'"
	       and h="h" and xa="(addr_of_sys_xcpt OutOfMemory)"  and frs="frs" and frs'="frs'" and 
               bla="bla" and h'="h" in effS.expt)
      apply simp
	     
      apply simp

      apply simp
      
      apply simp
		     
      apply simp

      apply simp

      apply simp

      apply simp

      apply simp
      done

    from s_effS s_def
    show ?thesis
      by fastsimp
  qed
qed
(*>*)


lemma succsF_progress_Getfield:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
 (* assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (Getfield F Cl)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B  cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)
  
  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

   obtain i where i_def: "i = Getfield F Cl"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done

  from check_s s_def  p_def instr_p i_def obtain r rst  
   where st_def:"st = r#rst" 
   and is_Ref_r:"is_Ref' h r"
   apply (simp add: neq_Nil_conv check_def split_def)
   apply (erule conjE | erule exE)+
   apply atomize
   apply simp
   done
  
  from is_Ref_r obtain adr obj 
   where r_def: "r = Null \<or> (r = Addr adr \<and> h adr = Some obj)"
   by (simp only: is_Ref'_def, case_tac "r::val",simp,simp,simp,simp,simp add: not_None_eq,blast)

  from s_inv_ExTys s_def have cname_sysxcpt: "(cname_of h (addr_of_sys_xcpt NullPointer)) = NullPointer"
    apply (simp add: inv_ExTys_def obj_ty_def)
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p,  Neg (St 0 \<doteq> Cn Null)]"
      by (simp add: succsNormal_def xcpt_cond_def)
    from st_def p'_B_def valid_B s_def r_def
    have exec_instr_s: "exec_instr (Getfield F Cl) P h (r#rst) rg C M pc frs = (None,h,(the (snd obj (F, Cl))#rst,rg,(C,M,Suc pc))#frs)"
    by (simp add: split_def)

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def st_def r_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(the (snd obj (F, Cl))#rst,rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Getfield F Cl"
                    and fr'="(the (snd obj (F, Cl))#rst,rg,(C,M,Suc pc))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
    proof -

      from xcpt cmd_p obtain B'
      where p'_B'_succsXpt: "(p',B') \<in> set (succsXpt (\<Pi>,NullPointer,[p]))"
      and B_def: "B = And [Pos p,B']"
      apply -
      apply (simp add: succsExcept_def)
      apply (erule imageE)
      apply (simp add: split_def)
      by fastsimp

    from wf_Pi domC_p have succsExcept_domC:
      "fst ` (set (succsExcept \<Pi> p)) \<subset> set (domC \<Pi>)"
      by (simp add: wf_def JBC_VCG.wf_def checkPos_split split_if[of "\<lambda> x. x" _ _ "False"] )
    
    from xcpt succsExcept_domC cmd_p
    have succsXpt_domC: "fst ` (set (succsXpt (\<Pi>,NullPointer,[p]))) \<subset> set (domC \<Pi>)"
      apply -
      apply (simp add: succsExcept_def)
      done

    from p'_B'_succsXpt succsXpt_domC Pi_def
    have B'_xcpt_cond: "\<exists> As. B' = And (As@[xcpt_cond (P,An) NullPointer p])"
      apply -
      apply (rule_tac X="NullPointer" and L="[p]" and p'="p'" in succsXpt_xcpt_cond)
      apply simp 
      apply simp
      apply simp
      done

    from p'_B'_succsXpt valid_B B_def B'_xcpt_cond 
    have valid_xcpt_cond: "\<Pi>,s \<Turnstile> (xcpt_cond \<Pi> NullPointer p)"
      apply -
      apply (erule exE)+
      apply (simp add: Pi_def del: succsXpt.simps)
      apply (erule conjE)+
      apply (simp add: evalEs_map)
      done

    from  st_def s_def valid_xcpt_cond cmd_p i_def
    obtain bla
    where exec_instr_s: "exec_instr i P h st rg C M pc frs = 
        (\<lfloor>addr_of_sys_xcpt NullPointer\<rfloor>, h,bla)"
      apply (simp add: split_def xcpt_cond_def)
      done

    from s_def wf_Pi p'_B'_succsXpt valid_B B_def s_inv_Pos cname_sysxcpt succsXpt_domC Pi_def p_def
    obtain rg' frs'
      where find_handler_s: "find_handler P (addr_of_sys_xcpt NullPointer) h ((st, rg, p) # frs) = 
      (None, h, ([Addr (addr_of_sys_xcpt NullPointer)], rg', p') # frs')"
      apply -
      apply (drule_tac xa="addr_of_sys_xcpt NullPointer" in succsXpt_findhandler)
      apply assumption
      apply assumption
      apply simp
      apply assumption
      apply simp
      apply assumption
      apply (erule exE)+
      by fastsimp
 
    from Pi_def p_def instr_p has_method_p exec_instr_s find_handler_s cname_sysxcpt s_def i_def
    have s_effS: "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,([Addr (addr_of_sys_xcpt NullPointer)],rg',p')#frs'),
	                 e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>)) \<in> effS \<Pi>" 
      apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="i"  and loc'="rg'"
	       and h="h" and xa="(addr_of_sys_xcpt NullPointer)"  and frs="frs" and frs'="frs'" and 
               bla="bla" and h'="h" in effS.expt)
      apply simp
	     
      apply simp

      apply simp
      
      apply simp
		     
      apply simp

      apply simp

      apply simp

      apply simp

      apply simp
      done

    from s_effS s_def
    show ?thesis
      by fastsimp
  qed
qed
qed
(*>*)


lemma succsF_progress_Putfield:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (Putfield F Cl)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B  cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)
  
 from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done
 
    obtain i where i_def: "i = Putfield F Cl"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done

  from i_def check_s s_def  p_def instr_p obtain v r rst 
   where st_def:"st = v#r#rst" 
   and is_Ref_r:"is_Ref' h r"
   apply atomize
   apply (simp add: neq_Nil_conv check_def split_def)
   apply (case_tac "st")
   apply simp
   apply (case_tac "list")
   apply simp
   apply simp
   done
  
  from is_Ref_r obtain adr obj 
   where r_def: "r = Null \<or> (r = Addr adr \<and> h adr = Some obj)"
   by (simp only: is_Ref'_def, case_tac "r::val",simp,simp,simp,simp,simp add: not_None_eq,blast)

  from s_inv_ExTys s_def have cname_sysxcpt: "(cname_of h (addr_of_sys_xcpt NullPointer)) = NullPointer"
    apply (simp add: inv_ExTys_def obj_ty_def)
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p,  Neg (St (Suc 0) \<doteq> Cn Null)]"
      by (simp add: succsNormal_def xcpt_cond_def)
    from st_def p'_B_def valid_B s_def r_def
    have exec_instr_s: "exec_instr (Getfield F Cl) P h (r#rst) rg C M pc frs = (None,h,(the (snd obj (F, Cl))#rst,rg,(C,M,Suc pc))#frs)"
    by (simp add: split_def)

    from p'_B_def st_def r_def valid_B s_def have r_not_Null: "r \<noteq> Null"
      by (simp add: check_def)

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def st_def r_def r_not_Null s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h(adr \<mapsto> (fst obj, snd obj((F, Cl) \<mapsto> v))) ,(rst,rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Putfield F Cl"
                    and fr'="(rst,rg,(C,M,Suc pc))"
		    and h="h" and h'="h(adr \<mapsto> (fst obj, snd obj((F, Cl) \<mapsto> v)))" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def split_def)+
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -

    from xcpt cmd_p obtain B'
      where p'_B'_succsXpt: "(p',B') \<in> set (succsXpt (\<Pi>,NullPointer,[p]))"
      and B_def: "B = And [Pos p,B']"
      apply -
      apply (simp add: succsExcept_def)
      apply (erule imageE)
      apply (simp add: split_def)
      by fastsimp

    from wf_Pi domC_p have succsExcept_domC:
      "fst ` (set (succsExcept \<Pi> p)) \<subset> set (domC \<Pi>)"
      by (simp add: wf_def JBC_VCG.wf_def checkPos_split split_if[of "\<lambda> x. x" _ _ "False"] )
    
    from xcpt succsExcept_domC cmd_p
    have succsXpt_domC: "fst ` (set (succsXpt (\<Pi>,NullPointer,[p]))) \<subset> set (domC \<Pi>)"
      apply -
      apply (simp add: succsExcept_def)
      done

    from p'_B'_succsXpt succsXpt_domC Pi_def
    have B'_xcpt_cond: "\<exists> As. B' = And (As@[xcpt_cond (P,An) NullPointer p])"
      apply -
      apply (rule_tac X="NullPointer" and L="[p]" and p'="p'" in succsXpt_xcpt_cond)
      apply simp 
      apply simp
      apply simp
      done

    from p'_B'_succsXpt valid_B B_def B'_xcpt_cond 
    have valid_xcpt_cond: "\<Pi>,s \<Turnstile> (xcpt_cond \<Pi> NullPointer p)"
      apply -
      apply (erule exE)+
      apply (simp add: Pi_def del: succsXpt.simps)
      apply (erule conjE)+
      apply (simp add: evalEs_map)
      done

    from  st_def s_def valid_xcpt_cond cmd_p i_def
    obtain bla h'
    where exec_instr_s: "exec_instr i P h st rg C M pc frs = 
        (\<lfloor>addr_of_sys_xcpt NullPointer\<rfloor>, h',bla)"
      apply (simp add: split_def xcpt_cond_def)
      apply fastsimp
      done

    from s_def wf_Pi p'_B'_succsXpt valid_B B_def s_inv_Pos cname_sysxcpt succsXpt_domC Pi_def p_def
    obtain rg' frs'
      where find_handler_s: "find_handler P (addr_of_sys_xcpt NullPointer) h ((st, rg, p) # frs) = 
      (None, h, ([Addr (addr_of_sys_xcpt NullPointer)], rg', p') # frs')"
      apply -
      apply (drule_tac xa="addr_of_sys_xcpt NullPointer" in succsXpt_findhandler)
      apply assumption
      apply assumption
      apply simp
      apply assumption
      apply simp
      apply assumption
      apply (erule exE)+
      by fastsimp
 
    from Pi_def p_def instr_p has_method_p exec_instr_s find_handler_s cname_sysxcpt s_def i_def
    have s_effS: "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,([Addr (addr_of_sys_xcpt NullPointer)],rg',p')#frs'),
	                 e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>)) \<in> effS \<Pi>" 
      apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="i"  and loc'="rg'"
	       and h="h" and xa="(addr_of_sys_xcpt NullPointer)"  and frs="frs" and frs'="frs'" and 
               bla="bla" and h'="h'" in effS.expt)
      apply simp
	     
      apply simp

      apply simp
      
      apply simp
		     
      apply simp

      apply simp

      apply simp

      apply simp

      apply simp
      done

    from s_effS s_def
    show ?thesis
      by fastsimp
  qed
qed
qed
(*>*)



lemma succsF_progress_Checkcast:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (Checkcast Cl)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)
 
  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

     obtain i where i_def: "i = Checkcast Cl"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
  
  from check_s s_def i_def p_def instr_p Pi_def obtain r rst 
   where st_def:"st = r#rst" 
   and class_Cl:"is_class P Cl" 
   and is_Ref_r:"is_Ref' h r"
    apply -
    apply atomize
    apply (simp add: neq_Nil_conv check_def split_def)
    apply (erule exE | erule conjE)+
    apply simp
    done

  from is_Ref_r obtain adr obj 
   where r_def: "r = Null \<or> (r = Addr adr \<and> h adr = Some obj)"
   by (simp only: is_Ref'_def, case_tac "r::val",simp,simp,simp,simp,simp add: not_None_eq,blast)

  from s_inv_ExTys s_def have cname_sysxcpt: "(cname_of h (addr_of_sys_xcpt ClassCast)) = ClassCast"
    apply (simp add: inv_ExTys_def obj_ty_def)
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p, Neg (And (Neg (St 0 \<doteq> Cn Null) # map (\<lambda>Cn. Neg (Ty (St 0) (Class Cn))) [Cn\<in>classnames (fst \<Pi>) . fst \<Pi> \<turnstile> Cn \<preceq>\<^sup>* Cl]))]"
      by (simp add: succsNormal_def xcpt_cond_def)
    from st_def valid_B p'_B_def s_def r_def class_Cl 
    have cast_ok_s:"cast_ok P Cl h r"
      apply (simp add: cast_ok_def)
      apply (case_tac "r = Null")
      apply simp

      apply (simp add: list_all_iff evalEs_map)
      apply (erule exE | erule conjE)+
      apply (simp add: obj_ty_def Pi_def)
      done

    from cast_ok_s st_def
    have exec_instr_s: "exec_instr (Checkcast Cl) P h st rg C M pc frs = (None,h,(st,rg,(C,M,Suc pc))#frs)"
      by simp

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(st,rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Checkcast Cl"
                    and fr'="(st,rg,(C,M,Suc pc))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -

    from xcpt cmd_p obtain B'
      where p'_B'_succsXpt: "(p',B') \<in> set (succsXpt (\<Pi>,ClassCast,[p]))"
      and B_def: "B = And [Pos p,B']"
      apply -
      apply (simp add: succsExcept_def)
      apply (erule imageE)
      apply (simp add: split_def)
      by fastsimp

    from wf_Pi domC_p have succsExcept_domC:
      "fst ` (set (succsExcept \<Pi> p)) \<subset> set (domC \<Pi>)"
      by (simp add: wf_def JBC_VCG.wf_def checkPos_split split_if[of "\<lambda> x. x" _ _ "False"] )
    
    from xcpt succsExcept_domC cmd_p
    have succsXpt_domC: "fst ` (set (succsXpt (\<Pi>,ClassCast,[p]))) \<subset> set (domC \<Pi>)"
      apply -
      apply (simp add: succsExcept_def)
      done

    from p'_B'_succsXpt succsXpt_domC Pi_def
    have B'_xcpt_cond: "\<exists> As. B' = And (As@[xcpt_cond (P,An) ClassCast p])"
      apply -
      apply (rule_tac X="ClassCast" and L="[p]" and p'="p'" in succsXpt_xcpt_cond)
      apply simp 
      apply simp
      apply simp
      done

    from p'_B'_succsXpt valid_B B_def B'_xcpt_cond 
    have valid_xcpt_cond: "\<Pi>,s \<Turnstile> (xcpt_cond \<Pi> ClassCast p)"
      apply -
      apply (erule exE)+
      apply (simp add: Pi_def del: succsXpt.simps)
      apply (erule conjE)+
      apply (simp add: evalEs_map)
      done

    from valid_xcpt_cond cmd_p Pi_def
    have xcpt_cond_s: "(P,An),s \<Turnstile> (And (Neg (St 0 \<doteq> Cn Null) # map (\<lambda>Cn. Neg (Ty (St 0) (Class Cn))) [Cn\<in>classnames P . P \<turnstile> Cn \<preceq>\<^sup>* Cl]))"
    by (simp add: xcpt_cond_def)
    
  from st_def xcpt_cond_s s_def r_def class_Cl 
  have not_cast_ok: "\<not> cast_ok P Cl h r"
    apply (case_tac "P \<turnstile> fst obj \<preceq>\<^sup>* Cl")
    apply (simp add: evalEs_map list_all_iff)
    apply (erule_tac x="fst obj" in allE)
    apply (simp add: obj_ty_def)
    apply (erule converse_rtranclE)
    apply (simp add: is_class_def classnames_def class_def)
    apply (erule exE)+
    apply (drule map_of_SomeD)
    apply (simp add: in_set_conv_decomp)
    apply (erule exE)+
    apply simp

    apply (drule subcls1D)
    apply (erule exE | erule conjE)+
    apply (simp add: classnames_def class_def)
    apply (drule map_of_SomeD)
    apply (simp add: in_set_conv_decomp)
    apply(erule exE)+
    apply simp

    apply (simp add: cast_ok_def)
    done

  from st_def xcpt_cond_s s_def r_def not_cast_ok 
  obtain bla
  where exec_instr_s: "exec_instr (Checkcast Cl) P h st rg C M pc frs = (Some (addr_of_sys_xcpt ClassCast),h,bla)"
    by simp

  from s_def wf_Pi p'_B'_succsXpt valid_B B_def s_inv_Pos cname_sysxcpt succsXpt_domC Pi_def p_def
  obtain rg' frs'
    where find_handler_s: "find_handler P (addr_of_sys_xcpt ClassCast) h ((st, rg, p) # frs) = 
    (None, h, ([Addr (addr_of_sys_xcpt ClassCast)], rg', p') # frs')"
    apply -
    apply (drule_tac xa="addr_of_sys_xcpt ClassCast" in succsXpt_findhandler)
    apply assumption
    apply assumption
    apply simp
    apply assumption
    apply simp
    apply assumption
    apply (erule exE)+
    by fastsimp
 
  from Pi_def p_def instr_p has_method_p exec_instr_s find_handler_s cname_sysxcpt s_def i_def
  have s_effS: "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,([Addr (addr_of_sys_xcpt ClassCast)],rg',p')#frs'),
                e\<lparr>cs := drop (length frs - length frs') (cs e)\<rparr>)) \<in> effS \<Pi>" 
      apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="i"  and loc'="rg'"
	       and h="h" and xa="(addr_of_sys_xcpt ClassCast)"  and frs="frs" and frs'="frs'" and 
               bla="bla" and h'="h" in effS.expt)
      apply simp
	     
      apply simp

      apply simp
      
      apply simp
		     
      apply simp

      apply simp

      apply simp

      apply simp

      apply simp
      done

    from s_effS s_def
    show ?thesis
      by fastsimp
  qed
qed
qed
(*>*)


lemma succsF_progress_Load:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (Load n)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = Load n"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p, TT]"
      by (simp add: succsNormal_def xcpt_cond_def)
    have exec_instr_s: "exec_instr (Load n) P h st rg C M pc frs = (None,h,( rg ! n # st,rg,(C,M,Suc pc))#frs)"
      by simp

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(rg ! n # st,rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Load n"
                    and fr'="(rg ! n # st,rg,(C,M,Suc pc))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_Store:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (Store n)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done
  
  obtain i where i_def: "i = Store n"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p, TT]"
      by (simp add: succsNormal_def xcpt_cond_def)
    have exec_instr_s: "exec_instr (Store n) P h st rg C M pc frs = (None,h,( tl st, rg[n := hd st],(C,M,Suc pc))#frs)"
      by simp

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(tl st,rg[n := hd st],(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Store n"
                    and fr'="(tl st,rg[n := hd st],(C,M,Suc pc))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_Push:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (Push v)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

   obtain i where i_def: "i = Push v"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p, TT]"
      by (simp add: succsNormal_def xcpt_cond_def)
    have exec_instr_s: "exec_instr (Push v) P h st rg C M pc frs = (None,h,( v # st,rg,(C,M,Suc pc))#frs)"
      by simp

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(v # st,rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Push v"
                    and fr'="(v # st,rg,(C,M,Suc pc))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_Pop:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some Pop"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = Pop"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p, TT]"
      by (simp add: succsNormal_def xcpt_cond_def)
    have exec_instr_s: "exec_instr Pop P h st rg C M pc frs = (None,h,( tl st,rg,(C,M,Suc pc))#frs)"
      by simp

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(tl st,rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Pop"
                    and fr'="(tl st,rg,(C,M,Suc pc))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_IBin:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
 (* assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (IBin no)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = (IBin no)"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
   
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p, TT]"
      by (simp add: succsNormal_def xcpt_cond_def)
    have exec_instr_s: "exec_instr (IBin no) P h st rg C M pc frs = (None,h,(Intg (numop no (the_Intg (hd (tl st))) (the_Intg (hd st))) # tl (tl st),rg,(C,M,Suc pc))#frs)"
      by simp

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(Intg (numop no (the_Intg (hd (tl st))) (the_Intg (hd st))) # tl (tl st),rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="IBin no"
                    and fr'="(Intg (numop no (the_Intg (hd (tl st))) (the_Intg (hd st))) # tl (tl st),rg,(C,M,Suc pc))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_Goto:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (Goto t)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = Goto t"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
  
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = (C,M,nat ((int pc)+t)) \<and> 
      B = And [Pos p, TT]"
      by (simp add: p_def succsNormal_def xcpt_cond_def split_def)
    have exec_instr_s: "exec_instr (Goto t) P h st rg C M pc frs = (None,h,(st,rg,(C,M,nat (int pc + t)))#frs)"
      by simp

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(st,rg,(C,M,nat (int pc + t)))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Goto t"
                    and fr'="(st,rg,(C,M,nat (int pc + t)))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_CmpEq:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
 (*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some CmpEq"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = CmpEq"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done

  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"p' = incA p \<and> 
      B = And [Pos p, TT]"
      by (simp add: succsNormal_def xcpt_cond_def)
    have exec_instr_s: "exec_instr CmpEq P h st rg C M pc frs = (None,h,(Bool (hd (tl st) = hd st)#(tl (tl st)),rg,(C,M,Suc pc))#frs)"
      by simp

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(Bool (hd (tl st) = hd st)#(tl (tl st)),rg,(C,M,Suc pc))#frs),e)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="CmpEq"
                    and fr'="(Bool (hd (tl st) = hd st)#(tl (tl st)),rg,(C,M,Suc pc))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
    by (simp add:incA_def)+
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_IfIntCmp:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (IfIntCmp ro t)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = (IfIntCmp ro t)"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"(p' = (C,M,nat ((int pc)+t)) \<and> 
      B = And [Pos p,  Rel (St 1) ro (St 0)]) \<or> 
      (p' = incA p \<and> 
      B = And [Pos p,  Neg (Rel (St 1) ro (St 0))])"
      apply (simp add: p_def succsNormal_def xcpt_cond_def split_def)
      done
    from p'_B_def show ?thesis
      proof
      assume p'_St0_Leq_St1:
      "p' = (C, M, nat (int pc + t)) \<and> B = And [Pos p, Rel (St 1) ro (St 0)]"
      show ?thesis
	proof -
	from i_def p'_St0_Leq_St1 valid_B s_def Pi_def p_def check_s instr_p
	have exec_instr_s: "exec_instr (IfIntCmp ro t) P h st rg C M pc frs = (None,h,(tl (tl st),rg,(C,M,nat (int pc + t)))#frs)"
	  apply (simp add: check_def split_def)
	  apply (case_tac "st")
	  apply simp
	  apply (case_tac "list")
	  apply simp

	  apply (case_tac "hd st")
	  apply simp+
	  apply (case_tac "aa")
	  apply simp+
	  done
	 from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_St0_Leq_St1 s_def
	 have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(tl (tl st),rg,(C,M,nat (int pc + t)))#frs),e)) \<in> effS \<Pi>" 
	   apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="IfIntCmp ro t"
                    and fr'="(tl (tl st),rg,(C,M,nat (int pc + t)))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
	   by (simp add:incA_def)+
	 from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
	 qed
	 
	 
       next

	 assume p'_Neg_St0_Leq_St1:
	 "p' = incA p \<and> B = And [Pos p, Neg (Rel (St 1) ro (St 0))]"
	 show ?thesis
	 proof -
	   from i_def p'_Neg_St0_Leq_St1 valid_B s_def Pi_def p_def check_s instr_p
	   have exec_instr_s: "exec_instr (IfIntCmp ro t) P h st rg C M pc frs = (None,h,(tl (tl st),rg,incA p)#frs)"
	     apply (simp add: check_def split_def)
	     apply (case_tac "st")
	     apply simp
	     apply (case_tac "list")
	     apply simp  
	     apply (case_tac "hd st")
	     apply (simp add: incA_def)+
	     apply (case_tac "hd (tl st)")
	     apply (simp add: relop_def)+
	     done

	   from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_Neg_St0_Leq_St1 s_def
	   have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(tl (tl st),rg,incA p)#frs),e)) \<in> effS \<Pi>" 
	     apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="IfIntCmp ro t"
               and fr'="(tl (tl st),rg,incA p)"
	       and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
	     by (simp add:incA_def)+
	   from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
	 qed
	 qed
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_IfFalse:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some (IfFalse t)"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)

  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = (IfFalse t)"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
 
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    have p'_B_def:"(p' = (C,M,nat ((int pc)+t)) \<and> 
      B = And [Pos p,  St 0 \<doteq> FF]) \<or> 
      (p' = incA p \<and> 
      B = And [Pos p,  Neg (St 0 \<doteq> FF)])"
      apply (simp add: p_def succsNormal_def xcpt_cond_def split_def)
      done
    from p'_B_def show ?thesis
      proof
      assume p'_St0_FF:
      "p' = (C, M, nat (int pc + t)) \<and> B = And [Pos p, St 0 \<doteq> FF]"
      show ?thesis
	proof -
	from i_def p'_St0_FF valid_B s_def Pi_def p_def check_s instr_p
	have exec_instr_s: "exec_instr (IfFalse t) P h st rg C M pc frs = (None,h,(tl st,rg,(C,M,nat (int pc + t)))#frs)"
	  apply (simp add: check_def split_def)
	  apply (case_tac "st")
	  apply simp

	  apply (case_tac "hd st")
	  apply simp+
	  done
	 from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_St0_FF s_def
	 have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(tl st,rg,(C,M,nat (int pc + t)))#frs),e)) \<in> effS \<Pi>" 
	   apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="IfFalse t"
                    and fr'="(tl st,rg,(C,M,nat (int pc + t)))"
		    and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
	   by (simp add:incA_def)+
	 from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
	 qed
	 
	 
       next

	 assume p'_St0_Neg_FF:
	 "p' = incA p \<and> B = And [Pos p, Neg (St 0 \<doteq> FF)]"
	 show ?thesis
	 proof -
	   from i_def p'_St0_Neg_FF valid_B s_def Pi_def p_def check_s instr_p
	   have exec_instr_s: "exec_instr (IfFalse t) P h st rg C M pc frs = (None,h,(tl st,rg,incA p)#frs)"
	     apply (simp add: check_def split_def)
	     apply (case_tac "st")
	     apply simp
	     
	     apply (case_tac "hd st")
	     apply (simp add: incA_def)+
	     done

	   from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_St0_Neg_FF s_def
	   have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(tl st,rg,incA p)#frs),e)) \<in> effS \<Pi>" 
	     apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="IfFalse t"
               and fr'="(tl st,rg,incA p)"
	       and h="h" and h'="h" and frs="frs" and frs'="frs" in effS.nrml)
	     by (simp add:incA_def)+
	   from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
	 qed
	 qed
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)


lemma succsF_progress_Return:
  assumes Pi_def:"\<Pi> = (P,An)"
  assumes p_def:"p = (C,M,pc)"
  assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
  assumes wf_Pi:"wf \<Pi>"
(*  assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *)
  assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
  assumes valid_B:"\<Pi>,s \<Turnstile> B"
  assumes cmd_p:"cmd \<Pi> p = Some Return"
  assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
  assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
  assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
  assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
  shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
  note GA = Pi_def p_def s_def wf_Pi p'_B_succsF valid_B cmd_p
  from GA have p'_B_nrml_expt: 
  "(p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsNormal \<Pi> p) \<or>
   (p', B) \<in> (\<lambda>(p', B). (p', And [Pos p, B])) ` set (succsExcept \<Pi> p)" (is "?nrml \<or> ?xcpt")
  by (simp add: addPos_def succsF_def)
  
  from Pi_def wf_Pi have wfK: "wf_jvm_prog\<^isub>k P"
    apply -
    apply (drule wf_TypeSafe)
    apply (simp add: jvm_kildall_correct wf_jvm_prog_def)
    apply fastsimp
    done

  obtain i where i_def: "i = Return"
    by fastsimp
  
  from cmd_p Pi_def wf_Pi p_def i_def
  have instr_p:"instrs_of P C M ! pc = i"
   apply -
   apply (drule_tac \<Pi>="\<Pi>" and C="C" and M="M" and pc="pc" in domC_cmd_instr_of)
   apply (rule cmd_domC)
   apply simp

   apply simp
   done

  from cmd_p obtain dm dm' where domC_p:"domC \<Pi> = dm@[p]@dm'"
   by (fastsimp dest: cmd_domC simp add: in_set_conv_decomp)

  from cmd_p have has_method_p: "has_method P C M" 
    apply -
    apply (drule cmd_domC)
    apply (simp add: p_def Pi_def has_method_def mem_iff)
    apply (rule_tac pc="pc" and An="An" in domC_methodnames, assumption)
    done

  from wf_Pi Pi_def s_def p_def s_inv_Ty  cmd_p i_def
  have check_s: "check_instr' i (fst \<Pi>) h st rg C M pc frs"
    apply -
    apply (rule wf_invTys_check')
    apply simp+
    done
 
 
  from p'_B_nrml_expt show ?thesis
  proof
    assume nrml: "?nrml"
    from cmd_p nrml 
    obtain cp
    where p'_B_def:" cp \<in> set (callers \<Pi> p) \<and>p' = incA cp \<and> 
      B = And [Pos p, Call (And [aF \<Pi> cp,Pos cp])]"
      apply (simp add: p_def succsNormal_def xcpt_cond_def split_def)
      apply (erule imageE)
      apply (erule imageE)
      apply (atomize)
      apply (erule_tac x="p'a" in allE)
      apply simp
      done


    from s_inv_Pos have s_callers_sysinv: "callers_sysinv (\<Pi>,s)"
      apply -
      apply (rule callers_sysinv_Pos)
      apply (simp add: inv_Pos_def)
      done 

    from wf_Pi p_def Pi_def s_def s_def s_callers_sysinv p'_B_def obtain fr frss 
      where frs_cons: "frs = fr#frss"
      apply -
      apply atomize
      apply (simp only: callers_sysinv_trans)
      apply (subgoal_tac "\<exists> fr frss. frs = fr#frss")
      prefer 2
      apply (case_tac "frs = []")
      apply (erule_tac x="0" in allE)
      apply simp
      apply (drule_tac C="C" and pc="pc" in wf_no_main_call)
      apply simp

      apply (simp only: neq_Nil_conv)
     
      apply (erule exE)+
      apply (erule_tac x="fr" in allE)
      apply (erule_tac x="frss" in allE)
      apply simp
      done

    obtain cst crg cp' 
    where fr_def: "fr = (cst,crg,cp')"
      apply -
      apply atomize
      apply (erule_tac x="fst fr" in allE)
      apply (erule_tac x="fst (snd fr)" in allE)
      apply (erule_tac x="snd (snd fr)" in allE)
      apply simp
      done

    from i_def check_s s_def Pi_def instr_p frs_cons fr_def
    have exec_instr_s: "exec_instr Return P h st rg C M pc frs = 
         (None,h,(hd st # drop (Suc (length (fst (snd (method P C M))))) cst, crg, incA cp') # frss)"
      by (simp add: check_def split_def incA_def)

    from i_def Pi_def p_def instr_p  exec_instr_s check_s has_method_p p'_B_def frs_cons fr_def s_def
    have "((p,(None,h,(st,rg,p)#frs),e),(p',(None,h,(hd st # drop (Suc (length (fst (snd (method P C M))))) cst, crg, incA cp') # frss),e\<lparr>cs := tl (cs e)\<rparr>)) \<in> effS \<Pi>" 
    apply (rule_tac P="P" and M="M" and C="C" and pc="pc" and stk="st" and loc="rg" and i="Return"
                    and fr'="(hd st # drop (Suc (length (fst (snd (method P C M))))) cst, crg, incA cp')"
		    and h="h" and h'="h" and frs="frs" and frs'="frss" in effS.nrml)
    apply simp
    apply simp
    apply simp
    apply simp
    apply simp
    apply simp
    apply simp
    --{* incA cp = incA cp' *}
    apply (cut_tac valid_B)
    apply (cut_tac s_def)
    apply simp

    apply simp
    done
  
    from this s_def show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>" by fastsimp
    
  next
   
    assume xcpt: "?xcpt"
    show "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
      proof -
	from xcpt cmd_p show ?thesis
	  by (simp add: succsExcept_def)
      qed
    qed
qed
(*>*)

theorem succsF_progress:
assumes Pi_def:"\<Pi> = (P,An)"
assumes p_def:"p = (C,M,pc)"
assumes s_def:"s = (p, (None, h, (st, rg, p) # frs), e)"
assumes wf_Pi:"wf \<Pi>"
(* assumes valid_An: "\<forall> A. anF \<Pi> p = Some A \<longrightarrow> \<Pi>,s \<Turnstile> A" *) 
assumes p'_B_succsF:"(p',B) \<in> set (succsF \<Pi> p)"
assumes valid_B:"\<Pi>,s \<Turnstile> B"
assumes cmd_p:"cmd \<Pi> p = Some i"
assumes s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> (fst s)"
assumes s_inv_Ty:"\<Pi>,s \<Turnstile> inv_Ty \<Pi> (fst s)"
assumes s_inv_FrNr:"\<Pi>,s \<Turnstile> inv_FrNr \<Pi> (fst s)"
assumes s_inv_ExTys:"\<Pi>,s \<Turnstile> inv_ExTys \<Pi> (fst s)"  
shows goal: "\<exists>st' rg' frs' e'. (s, (p', (st', rg', frs'), e')) \<in> effS \<Pi>"
(*<*)
proof -
note reqs = Pi_def p_def s_def wf_Pi  p'_B_succsF valid_B cmd_p
     s_inv_Pos s_inv_Ty s_inv_FrNr s_inv_ExTys
show ?thesis
proof (cases i)

case (Load n)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Load)
  apply (simp only:)+
  done

next

case (Store n)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Store)
  apply (simp only:)+
  done

next

case (Push v)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Push)
  apply (simp only:)+
  done

next

case (New Cl)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_New)
  apply (simp only:)+
  done

next

case (Getfield F C)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Getfield)
  apply (simp only:)+
  done

next

case (Putfield F C)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Putfield)
  apply (simp only:)+
  done

next

case (Checkcast Cl)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Checkcast)
  apply (simp only:)+
  done

next

case (Invoke Mn n)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Invoke)
  apply (simp only:)+
  done

next
case Return
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Return)
  apply (simp only:)+
  done

next

case Pop
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Pop)
  apply (simp only:)+
  done

next

case (IBin no)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_IBin)
  apply (simp only:)+
  done

next

case (Goto t)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Goto)
  apply (simp only:)+
  done

next 

case CmpEq

from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_CmpEq)
  apply (simp only:)+
  done

next

case (IfIntCmp ro t)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_IfIntCmp)
  apply (simp only:)+
  done

next

case (IfFalse t)
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_IfFalse)
  apply (simp only:)+
  done

next

case Throw 
from this reqs
show ?thesis
  apply -
  apply (rule succsF_progress_Throw)
  apply (simp only:)+
  done

qed

qed
(*>*)


end