Theory dem_REUSE

(* 
   Title: Lemmas for the translation SVM to JVM. REUSE
   Author: Javier de Dios and Ricardo Pe~na
   Copyright: January 2009, Universidad Complutense de Madrid
*)


theory dem_REUSE
imports "../JVMSAFE/JVMExec" SVM2JVM SVMSemantics CertifSVM2JVM 
                             dem_translation
begin

no_translations "Norm s" == "(None,s)"


no_translations "ex_table_of m" == "snd (snd (snd m))"

declare trInstr.simps [simp del]
declare equivS.simps [simp del]


(* Axioms *)

axioms equivS_ge_n_distinct_g:
  "equivS S S' n ctm d g ==> (∀  p > 0. equivS S (S'(nat (p + n)  \<mapsto> A)) n ctm d g')"

(* Lemmas for equivS *)

lemma S2_REUSE:
  "execSVMInst (REUSE) (map_of ct) (hm, k) k0 (l, i) S = Either.Right S2
   ==>∃ b S'. ((hm(b := None)(getFresh hm \<mapsto> the (hm b)), k), k0, incrPC (l, i), Val (Val.Loc (getFresh hm)) # S') = S2 ∧
      S = Val (Val.Loc b) # S'"
apply (unfold execSVMInst.simps)
apply (case_tac "S",simp_all)
 apply (insert RightNotUndefined)
 apply (erule_tac x= "S2" in allE, force)
apply (case_tac a,simp_all)
  apply (case_tac Vala,simp_all)
   apply (erule_tac x= "S2" in allE, force)
  apply simp
 apply simp
by simp



lemma equivS_Val_Loc:
  "equivS (Val (Val.Loc b) # S) S' n ctm d g
   ==> (∃i. the (S' (nat n)) = Intg i ∧ (∃l'. d (nat i) = Some (Addr l') ∧ g b = Some l'))"
by (simp add: equivS.simps)

lemma equivS2_REUSE:
 "[| equivS (Val (Val.Loc b) # S) S' n ctm d g; d (nat ii) = Some (Addr l'); g b' = Some l'|] 
  ==> equivS (Val (Val.Loc (getFresh hm)) # S) (S'(nat n \<mapsto> Intg ii)) n ctm d (g(b:=None)(getFresh hm \<mapsto> l'))"
apply (frule equivS_Val_Loc)
apply (erule exE, elim conjE)
apply (erule exE, elim conjE)
apply (simp add: equivS.simps)
apply (elim conjE)
apply (frule equivS_ge_n_distinct_g)
apply (erule_tac x="1" in allE) 
by simp

(* Lemmas for inj_on *)

axioms getFresh_notin_dom_h:
 "getFresh hm ∉ dom hm"


lemma inj_on_REUSE:
  "[| inj_on g (dom hm); g b = Some l; dom g = dom hm;
     getFresh hm ∉ dom g; getFresh hm ∉ dom hm|] 
   ==> inj_on (g(b := None)(getFresh hm \<mapsto> l)) (dom (hm(b := None)(getFresh hm \<mapsto> the (hm b))))"
apply simp
apply (rule conjI)
 apply (simp add: inj_on_def)
apply (simp add: inj_on_def,clarsimp)
apply (split split_if_asm,simp) 
apply (split split_if_asm,simp,simp)
apply (erule_tac x="b" in ballE)
 apply (erule_tac x="x" in ballE)
  apply simp 
 apply (simp add: dom_def)
apply (subgoal_tac "b ∈ dom hm",simp)
apply (subgoal_tac "g b = Some l")
 apply (subgoal_tac "b ∈ dom g")
  apply (simp add: dom_def)
 apply (rule domI,assumption)
by simp


(* Lemmas for activeCells *)

lemma x_ran_update:
  " [| g b = Some l'a; x ∈ ran (g(b := None)(getFresh hm \<mapsto> l'a))|]
   ==> x ∈ ran g"
apply (simp add: ran_def,clarsimp)
apply (split split_if_asm,simp)
 apply (rule_tac x="b" in exI,simp)
apply (simp,split split_if_asm,simp) 
by (rule_tac x="a" in exI,simp)


lemma x_ran_update_2:
  " [| g b = Some l'a; x ∈ ran g; getFresh hm ∉ dom g; inj_on g (dom h)|]
   ==> x ∈ ran (g(b := None)(getFresh hm \<mapsto> l'a))"
apply (case_tac "x= l'a")
 apply (simp add: ran_def,force)
apply (simp add: ran_def)
apply (elim exE)
apply (rule_tac x="a" in exI,simp)
apply (rule conjI)
 apply (simp add: inj_on_def)
 apply (clarsimp, rule impI)
by clarsimp


lemma activeCells_REUSE:
  "[| la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
     ran g = activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))); 
     g b = Some l'a;
     getFresh hm ∉ dom g;
     inj_on g (dom hm) |] 
   ==> ran (g(b := None)(getFresh hm \<mapsto> l'a)) =
        activeCells regS (h(la \<mapsto> Arr ty m (S'a(nat n \<mapsto> vb')))) (nat (the_Intg (the (sha (heapC, kf)))))"
apply (frule l_not_in_cellReg)
apply (rule equalityI)
 apply (rule subsetI)
 apply (subgoal_tac "x ∈ ran g",simp)
  apply (simp add: activeCells_def) 
  apply (elim exE, elim conjE)
  apply (rule_tac x="j" in exI,simp)
  apply (simp add: region_def) 
  apply (elim conjE) 
  apply (rule cellReg_step) 
   apply (rule cellReg_basic)
  apply (erule_tac x="j" in allE) 
  apply (rule cellsReg_monotone_1,assumption+)
  apply (erule l_not_in_regs)
 apply (rule x_ran_update,assumption+)
apply (rule subsetI)
apply (subgoal_tac "x ∈ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))")
 apply (subgoal_tac "x ∈ ran g")
  prefer 2 apply simp
 apply (rule x_ran_update_2,assumption+)
apply (simp add: activeCells_def) 
apply (elim exE, elim conjE)
apply (rule_tac x="j" in exI,simp)
apply (simp add: region_def) 
apply (elim conjE) 
apply (rule cellReg_step) 
 apply (rule cellReg_basic)
apply (erule_tac x="j" in allE) 
apply (rule cellsReg_monotone_2,assumption+)
by (erule l_not_in_regs)


declare equivH.simps [simp del]


(* Lemmas for domH *)

axioms l_not_getFresh:
  "l ≠ getFresh hm"

lemma same_region_REUSE:
  "la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))
   ==> region regS h j = region regS (h(la \<mapsto> Arr ty m (S'a(nat n \<mapsto> vb')))) j"
apply (frule l_not_in_cellReg)
apply (simp add: region_def)
apply (rule equalityI)
 apply (rule subsetI)
 apply clarsimp
 apply (rule cellReg_step) 
  apply (rule cellReg_basic)
 apply (erule_tac x="j" in allE) 
 apply (rule cellsReg_monotone_1,assumption+)
 apply (erule l_not_in_regs)
apply (rule subsetI)
apply clarsimp
apply (rule cellReg_step) 
 apply (rule cellReg_basic)
apply (erule_tac x="j" in allE) 
apply (rule cellsReg_monotone_2,assumption+)
by (erule l_not_in_regs)

lemma equivV_REUSE:
  "[| i < length vs;
     ∀ i < length vs. ∀ l''. vs!i = Val.Loc l'' --> l'' ≠ b ∧ l'' ∈ dom hm;
     getFresh hm ∉ dom g;
     b ≠ getFresh hm;
    equivV (vs ! i) (argCell flds i) d g |] 
  ==> equivV (vs ! i) (argCell flds i) d (g(b := None)(getFresh hm \<mapsto> l'a))"
apply (case_tac "vs!i")
apply clarsimp
apply simp
by simp

axioms vs_i_good:
 "∀ i < length vs. ∀ l''. vs!i = Val.Loc l'' --> l'' ≠ b ∧ l'' ∈ dom hm"


lemma domH_REUSE:
  "[| la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))); dom g = dom hm;
     ∀l∈dom hm. ∃l'. l' = the (g l) ∧ equivC (the (hm l)) h l' (the (h l')) (nat (the_Intg (the (sha (heapC, kf))))) com regS d g;
    g b = Some l'a |] 
   ==> ∀l∈dom (hm(b := None)(getFresh hm \<mapsto> the (hm b))).
          ∃l'. l' = the ((g(b := None)(getFresh hm \<mapsto> l'a)) l) ∧
               equivC (the ((hm(b := None)(getFresh hm \<mapsto> the (hm b))) l)) (h(la \<mapsto> Arr ty m (S'a(nat n \<mapsto> vb')))) l'
                (the ((h(la \<mapsto> Arr ty m (S'a(nat n \<mapsto> vb')))) l')) (nat (the_Intg (the (sha (heapC, kf))))) com regS d
                (g(b := None)(getFresh hm \<mapsto> l'a))"
apply (rule ballI)
apply (erule_tac x="l" in ballE)
 prefer 2 apply (subgoal_tac "l ≠ getFresh hm")
  prefer 2 apply (rule l_not_getFresh)
 apply simp
apply (elim exE)
apply (rule_tac x="l'" in exI)
apply (rule conjI)
 apply (subgoal_tac "l ≠ getFresh hm")
  prefer 2 apply (rule l_not_getFresh)
 apply simp apply (elim conjE)
apply (unfold equivC.simps)
apply (elim exE) apply (elim conjE)
apply (rule_tac x="j" in exI)
apply (rule_tac x="C" in exI)
apply (rule_tac x="vs" in exI)
apply (rule_tac x="Obj" in exI)
apply (rule_tac x="cname" in exI)
apply (rule_tac x="flds" in exI)
apply (rule_tac x="tag" in exI)
apply (rule_tac x="na" in exI)
apply (rule_tac x="reg_j" in exI)
apply (rule_tac x="tag'" in exI)

apply (rule conjI)
 apply (subgoal_tac "l ≠ getFresh hm",simp)
 apply (rule l_not_getFresh)
apply (rule conjI, assumption)
apply (rule conjI) 
 apply (subgoal_tac "l' ≠ la",simp)
 apply (simp add: activeCells_def) 
 apply (erule_tac x="j" in allE,clarsimp)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, clarsimp)
 apply (rule same_region_REUSE, assumption+)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply (rule conjI, assumption)
apply simp
apply (rule allI, rule impI)
apply (erule_tac x="i" in allE,simp)
apply clarsimp
apply (subgoal_tac "∀ i < length vs. ∀ l''. vs!i = Val.Loc l'' --> l'' ≠ b ∧ l'' ∈ dom hm")
prefer 2 apply (rule vs_i_good)
apply (subgoal_tac "getFresh hm ∉ dom g")
 prefer 2 apply (subgoal_tac "getFresh hm ∉ dom hm",simp)
 apply (rule getFresh_notin_dom_h)
by (rule equivV_REUSE,assumption+,blast,assumption) 


(* Lemmas for equivH *)


lemma equivH_REUSE:
  "[| la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
     dom g = dom hm; g b = Some l'a; getFresh hm ∉ dom g; inj_on g (dom hm);
     equivH (hm, k) h (nat (the_Intg (the (sha (heapC, kf))))) com regS d g |] 
   ==> equivH (hm(b := None)(getFresh hm \<mapsto> the (hm b)), k) (h(la \<mapsto> Arr ty m (S'a(nat n \<mapsto> vb'))))
              (nat (the_Intg (the (sha (heapC, kf))))) com regS d (g(b := None)(getFresh hm \<mapsto> l'a))"
apply (unfold equivH.simps, elim conjE)
apply (rule conjI, clarsimp) 
apply (rule conjI)
apply (rule activeCells_REUSE, assumption+)
apply (rule conjI, clarsimp)
by (rule domH_REUSE,assumption+)


declare extractBytecode_def [simp del]
declare initConsTable_def   [simp del]
declare equivS.simps        [simp del]

axioms vs_length:
  "length vs = 10"

(* Axioms for RTS *)

axioms copyCell_method_jvm:
 "[| s = (None, shp, hp, ihp, [([vb],loc,safeP, sigSafeMain,pc,z1,z2)]);
  shp (stackC,Sf) = Some (Addr l);
  shp (StackC,topf) = Some (Intg ntop);
  hp l = Some  (Arr ty ma S');
  vb = Intg i;
  d (nat i) = Somde (Addr l');
  Invoke_static heapC copyCell [PrimT Integer] = 
                     fst(snd(snd(snd(snd(the(method' (P',safeP) sigSafeMain)))))) ! pc
  |] ==> 
  P' |- s -jvm-> (None, shp, hp, ihp, [([Intg ii],loc,safeP,sigSafeMain,pc+1,z1,z2)])"


axioms copyCell_method_equivState:
 "[| s = (None, shp, hp, ihp, 
            ([vb],loc,safeP, sigSafeMain,pc,z1,z2)#[]);
  shp (stackC,Sf) = Some (Addr l);
  shp (StackC,topf) = Some (Intg ntop);
  hp l = Some  (Arr ty ma S');
  vb = Intg i;
  d (nat i) = Somde (Addr l');
  Invoke_static heapC copyCell [PrimT Integer] = 
                     fst(snd(snd(snd(snd(the(method' (P',safeP) sigSafeMain)))))) ! pc
  |] ==> 
  P' |- s -jvm-> (None, shp, 
                        hp, 
                        ihp, ([vb'],loc,safeP,sigSafeMain,pc+1,z1,z2)#[]) ∧
  vb' = Intg ii ∧ 
  d (nat i) = None ∧
  d (nat ii) = Some (Addr l')"


declare execSVMInst.simps [simp del]

lemma execSVMInstr_REUSE :
  "[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
   cdm , ctm, com \<turnstile> ((hm, k), k0, (l, i), S) \<triangleq> S1'; 
   (fst (the (map_of svms l)) ! i) = REUSE;
   execSVMInst REUSE (map_of ct) (hm, k) k0 (l, i) S = Either.Right S2;
   drop (the (cdm (l, i))) (extractBytecode P') =
   trInstr (the (cdm (l, i))) cdm' ctm' com pcc REUSE @ bytecode'
   |] ==>   ∃ v' sh' dh' ih' fms' . 
      P' \<turnstile>  S1' -jvm-> (v',sh',dh',ih', fms') ∧
      cdm , ctm, com  \<turnstile>  S2  \<triangleq> (v',sh',dh',ih', fms')"

(* First, we make the tuples explicit *)
apply (case_tac S1')
apply (rename_tac v tup)
apply (case_tac tup)
apply (rename_tac sh tup)
apply (case_tac tup)
apply (rename_tac dh tup)
apply (case_tac tup)
apply (rename_tac ih fms)
apply (simp)

apply (subgoal_tac 
  "∃ b S'. ((hm(b := None)(getFresh hm \<mapsto> the (hm b)), k), k0, incrPC (l, i), Val (Val.Loc (getFresh hm)) # S') = S2 ∧
      S = Val (Val.Loc b) # S'")
prefer 2 apply (rule S2_REUSE,assumption)
apply (elim exE)

apply (unfold equivState_def) 
apply (elim exE,elim conjE)


apply (subgoal_tac "equivS (Val (Val.Loc b) # S') S'a n ctm d g")
prefer 2 apply clarsimp
apply (frule equivS_Val_Loc)
apply (elim exE, elim conjE)
apply (elim exE, elim conjE)

(* we go on with the main goal. We instantiate the arrival JVM state*)
apply (subgoal_tac "length vs = 10")
prefer 2 apply (rule vs_length)

apply (rule_tac x="None" in exI)
apply (rule_tac x="sha" in exI)
apply (rule_tac x=" h(la \<mapsto> Arr ty m (S'a(nat n \<mapsto> Intg ia)))" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="[([], 
                     vs[Suc 0 := Intg ia], 
                     safeP, sigSafeMain,
                     the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
                     ref)]" in exI)

(* Now, we prove that the JVM sequence leads to the arrival state *)
apply (subgoal_tac "∃ vs pc . fms=([],vs,safeP,sigSafeMain,pc,ref)#[]")
 prefer 2 apply simp
apply (erule exE)+
apply (unfold exec_all_def)
apply (rule conjI)


apply (subgoal_tac "PC = (l,i)") prefer 2 apply simp 
apply simp apply (elim conjE) apply clarsimp
apply (subgoal_tac 
  "P'\<turnstile> 
  (None,sha,h,inih,[([], vs, safeP, sigSafeMain, the (cdm (l,i)), ag,be)]) 
  -jvm-> 
  (None,sha,h,inih,[([the (sha (stackC,Sf))], vs, safeP, sigSafeMain, the (cdm (l,i)) + 1, ag,be)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)

(* We prove the first step of the SVM *)
prefer 2 
 apply (rule r_into_rtrancl)
 apply (clarify) 
 apply (unfold JVMExec.exec.simps) 
 apply (unfold Let_def)
 apply (unfold extractBytecode_def)
 apply (subgoal_tac 
   "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! 
    the (cdm (l, i))) = Getstatic Sf stackC",simp)
 apply (unfold trInstr.simps, erule nth_via_drop_append) 

(*  Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
     (None, sha, h, inih, 
     [([the (sha (stackC, Sf))], 
     vs, safeP, sigSafeMain, the (cdm (l, i)) + 1, ag, be)]) 
  -jvm->
     (None,sha,h,inih,
     [([the (sha (stackC,topf)),
        the (sha (stackC,Sf))], 
     vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, be)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2 
 apply (rule r_into_rtrancl)
 apply (clarify) 
 apply (unfold JVMExec.exec.simps) 
 apply (unfold Let_def)
 apply (subgoal_tac 
   "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! Suc (the (cdm (l, i)))) = 
    Getstatic topf stackC",simp)
 apply (erule nth_via_drop_append) 

(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
     (None,sha,h,inih,
     [([the (sha (stackC,topf)),
        the (sha (stackC, Sf))], 
     vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, ag, be)])
  -jvm->
     (None,sha,h,inih,
     [([the (S'a (nat n))], 
     vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, be)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2 
 apply (rule r_into_rtrancl)
 apply (clarify) 
 apply (unfold JVMExec.exec.simps) 
 apply (unfold Let_def)
 apply (subgoal_tac 
   "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! (Suc (Suc (the (cdm (l, i)))))) = 
    ArrLoad",simp)
 apply (simp add: raise_system_xcpt_def)
 apply (subgoal_tac "n >= 0",simp)
 apply (simp add: equivS.simps)
apply (erule nth_via_drop_append)

(* Invoke_static heapC copyCell [PrimT Integer] *)
apply (drule drop_Suc_append)
 apply (frule equivS_Val_Loc)
apply (elim exE, elim conjE)
apply (elim exE, elim conjE)
apply (subgoal_tac
  "P'\<turnstile> 
     (None,sha,h,inih,
     [([the (S'a (nat n))], 
     vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ag, be)])
  -jvm->
     (None,sha,h,inih,
     [([Intg ia], 
     vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, be)])")
prefer 2
 apply (rule_tac vb="the (S'a (nat n))" in copyCell_method_jvm)
apply (simp, assumption+)
apply (rule sym)
apply (simp, erule nth_via_drop) 
apply (unfold exec_all_def)
apply (erule rtrancl_trans)


(* Store 1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
  "P'\<turnstile> 
     (None,sha,h,inih,
     [([Intg ia], 
     vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, ag, be)])
  -jvm->
     (None,sha,h,inih,
     [([], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, ag, be)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2 
 apply (rule r_into_rtrancl)
 apply (clarify) 
 apply (unfold JVMExec.exec.simps) 
 apply (unfold Let_def)
 apply (subgoal_tac 
   "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))  = 
    Store 1",simp)
apply (erule nth_via_drop_append)


(* Getstatic Sf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac
  "P'\<turnstile> 
     (None,sha,h,inih,
     [([], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, ag, be)])
  -jvm->
     (None,sha,h,inih,
     [([the (sha (stackC, Sf))], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, ag, be)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2 
 apply (rule r_into_rtrancl)
 apply (clarify) 
 apply (unfold JVMExec.exec.simps) 
 apply (unfold Let_def)
 apply (subgoal_tac 
   "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! 
    (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))) = 
    Getstatic Sf stackC",simp)
apply (erule nth_via_drop_append)

(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac
  "P'\<turnstile> 
     (None,sha,h,inih,
     [([the (sha (stackC, Sf))], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, ag, be)])
  -jvm->
     (None,sha,h,inih,
     [([the (sha (stackC,topf)),
        the (sha (stackC, Sf))], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, be)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2 
 apply (rule r_into_rtrancl)
 apply (clarify) 
 apply (unfold JVMExec.exec.simps) 
 apply (unfold Let_def)
 apply (subgoal_tac 
   "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! 
    (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))) = 
    Getstatic topf stackC",simp) 
apply (erule nth_via_drop_append)

(* Load 1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac
  "P'\<turnstile> 
     (None,sha,h,inih,
     [([the (sha (stackC,topf)),
        the (sha (stackC, Sf))], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, be)])
  -jvm->
     (None,sha,h,inih,
     [([Intg ia,
        the (sha (stackC,topf)),
        the (sha (stackC, Sf))], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, be)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2 
 apply (rule r_into_rtrancl)
 apply (clarify) 
 apply (unfold JVMExec.exec.simps) 
 apply (unfold Let_def)
 apply (subgoal_tac 
   "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! 
    (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) = 
     Load 1 ",simp)
apply (erule nth_via_drop_append)



(* ArrStore *)
apply (drule drop_Suc_append)
apply (subgoal_tac
  "P'\<turnstile> 
     (None,sha,h,inih,
     [([Intg ia,
        the (sha (stackC,topf)),
        the (sha (stackC, Sf))], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, be)])
  -jvm->
     (None,sha,
     h(la \<mapsto> Arr ty m (S'a(nat n \<mapsto> Intg ia))),
     inih,
     [([], 
     vs[Suc 0 := Intg ia], 
     safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ag, be)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2 
 apply (rule r_into_rtrancl)
 apply (clarify) 
 apply (unfold JVMExec.exec.simps) 
 apply (unfold Let_def)
 apply (subgoal_tac 
   "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! 
    (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))) = 
     ArrStore",simp)
 apply (simp add: raise_system_xcpt_def)
 apply (subgoal_tac "n ≥ 0",simp)
 apply (simp add: equivS.simps)
 apply (erule nth_via_drop_append)
apply simp


(* Now we prove the equivalence relation *)
apply (frule nonJumping_Suc_pc)
apply (erule_tac sym [where t="REUSE"])
apply (simp add: nonJumping.simps)
apply (simp add: trInstr.simps)

apply (rule_tac x="hm(b := None)(getFresh hm \<mapsto> the (hm b))" in exI)
apply (rule_tac x="k" in exI)
apply (rule_tac x="k0" in exI)
apply (rule_tac x="(l,Suc i)" in exI)
apply (rule_tac x="Val (Val.Loc (getFresh hm)) # S'" in exI)

apply (rule_tac x="sha" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty m (S'a(nat n \<mapsto> Intg ia)))" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="vs[Suc 0 := Intg ia]" in exI)
apply (rule_tac x="the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1" in exI)
apply (rule_tac x="ref" in exI)

apply (rule_tac x="nat (the_Intg (the (sha (heapC, kf))))" in exI)
apply (rule_tac x="nat (the_Intg (the (sha (heapC, k0f))))" in exI)

apply (rule_tac x="la" in exI)
apply (rule_tac x="ty" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="(S'a(nat n \<mapsto> Intg ia))" in exI)

apply (rule_tac x="n" in exI)
apply (rule_tac x="l'" in exI) 
apply (rule_tac x="regS" in exI)
apply (rule_tac x="l''" in exI) 
apply (rule_tac x="m'" in exI) 
apply (rule_tac x="m''" in exI)  
apply (rule_tac x="d" in exI) 
apply (rule_tac x="g(b := None)(getFresh hm \<mapsto> l'a)" in exI)


apply (rule conjI, clarsimp)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI) apply clarsimp
apply (rule conjI, assumption)
apply (rule conjI) apply clarsimp
                   apply (simp add: stackC_def add: heapC_def)
                   apply (simp add: kf_def add: k0f_def) 
apply (rule conjI) apply (erule activeCells)
apply (rule conjI) apply (erule activeCells_2,assumption)
                   apply (erule activeCells_2,assumption)
apply (rule conjI, simp)
apply (rule conjI) apply (simp add: stackC_def add: heapC_def) 
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply (subgoal_tac "getFresh hm ∉ dom hm") 
                   prefer 2 apply (rule getFresh_notin_dom_h)
                   apply (subgoal_tac "getFresh hm ∉ dom g") 
                   prefer 2 apply simp 
                   apply (rule inj_on_REUSE,simp,assumption,simp,simp,assumption+)
apply (rule conjI) apply clarsimp 
                   apply (subgoal_tac "getFresh hm ∉ dom hm") 
                   prefer 2 apply (rule getFresh_notin_dom_h)
                   apply (subgoal_tac "getFresh hm ∉ dom g") 
                   prefer 2 apply simp
                   apply (rule equivH_REUSE,assumption+)
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply clarsimp 
                   apply (frule_tac hm="hm" in equivS2_REUSE,assumption+)
apply (rule conjI) apply clarsimp
by simp

end