Theory dem_BUILDCLS

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

theory dem_BUILDCLS
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]
declare extractBytecode_def [simp del]
declare initConsTable_def   [simp del]
declare exec_instr.simps [simp]

lemma drop_Suc_2:
  "drop n xs = (y # ys) ==> drop (Suc n) xs = ys"
apply (induct xs arbitrary: n, simp)
apply(simp add:drop_Cons nth_Cons split:nat.splits)
done

(* Axioms for RTS *)

axioms reserveCell_method:
  "[| s = (None, shp, hp, ihp, [([],loc,safeP, sigSafeMain,pc,ref)]);
     k' = nat (the_Intg (the (sha (heapC, kf))));
     shp (stackC,Sf) = Some (Addr l);
     shp (heapC,regionsf) = Some (Addr l');
     shp (dirCellC, safeDirf) = Some (Addr l''); hp l'' = Some (Arr ty m'' d);
     fst(snd(snd(snd(snd(the(method' (P',safeP) sigSafeMain)))))) ! pc = 
     Invoke_static dirCellC reserveCell []
   |] ==> 
   P' |- s -jvm-> (None, shp, hp', ihp, [([Intg ii], loc, safeP,sigSafeMain,pc+1,ref)]) ∧
   d (nat ii) = Some (Addr lobj) ∧ 
   hp' = hp( lobj \<mapsto> obj) ∧ 
   lobj ∉ activeCells regS h k' ∧
   lobj ∉ {l,l',l''} ∧
   the_obj obj = (cellC, empty) ∧
   ii < int m'' ∧ 0 < ii"

axioms insertCell_method_jvm:
  "[| s = (None, shp, hp(lobj \<mapsto> obj), ihp, [([ Intg iloc, Intg (int j)],vs,safeP, sigSafeMain,pc,ref)]);
     shp (heapC,regionsf) = Some (Addr l'); hp l' = Some (Arr ty m' regS);
     shp (dirCellC,safeDirf) = Some (Addr l''); hp l'' = Some (Arr ty m'' d);
     d (nat iloc) = Some (Addr lobj);
     fst(snd(snd(snd(snd(the(method' (P',safeP) sigSafeMain)))))) ! pc = 
     Invoke_static heapC insertCell [PrimT Integer, PrimT Integer]
   |] ==>  
   P' |- s -jvm-> (None, shp, hp(lobj \<mapsto> obj, l'  \<mapsto> Arr ty m' regS'), ihp, [([], vs, safeP,sigSafeMain,pc+1,ref)])"


axioms insertCell_method_equivState:
  "[| sh (stackC, Sf) = Some (Addr l); dh l = Some (Arr ty m S');
     sh (stackC, topf) = Some (Intg n);
     sh (heapC,regionsf) = Some (Addr l'); dh l' = Some (Arr ty m' regS);
     sh (dirCellC,safeDirf) = Some (Addr l''); dh l'' = Some (Arr ty m'' d);
     d (nat ii) = Some (Addr lobj);
     fst(snd(snd(snd(snd(the(method' (P',safeP) sigSafeMain)))))) ! pc = 
     Invoke_static heapC insertCell [PrimT Integer, PrimT Integer];
     P' |- 
        (None, sh, dh(lobj \<mapsto> obj), ih, [([ Intg ii, Intg (int j)],vs,safeP, sigSafeMain,pc,ref)])
     -jvm-> 
        (None, sh, dh(lobj \<mapsto> obj, l'  \<mapsto> Arr ty m' regS'), ih, [([], vs, safeP,sigSafeMain,pc+1,ref)])
   |] ==>  
   region regS' (dh(lobj \<mapsto> obj,
                     l' \<mapsto> Arr ty m' regS', 
                     l \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))) j = region regS dh j ∪ {lobj} ∧
   (∀ j''. j'' ≠ j -->  
           region regS' 
                  (dh(lobj \<mapsto> obj,
                     l' \<mapsto> Arr ty m' regS', 
                     l \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))) 
                  j'' = region regS dh j'')"



fun Item2val :: "entries_ => sheap => Item => val"
where
  "Item2val S sh (ItemConst v)    = (if (isBool v = True) 
                                    then (if (the_BoolT v)
                                          then Intg 1
                                          else Intg 0)
                                    else Intg (the_IntT v))"
| "Item2val S sh (ItemVar l)      = the (S (nat (the_Intg (the (sh (stackC, topf)))) -  l))"
| "Item2val S sh (ItemRegSelf)    = the (sh (heapC, kf))"


axioms fillAux_instrs:
" P'\<turnstile> (None, sha, h(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C)))]), 
        inih,  [([],
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := k_fresh],
       safeP,sigSafeMain, pc, ref)])
  -jvm->
     (None,sha,
       (let vitems = Intg (int (the (com C))) # map (Item2val S' sha) items;
            cnames = (tagGf, cellC) # map (λ i.  (VName (''arg''@ nat2Str i),cellC)) [0..<length items];
            objs   = Obj cellC (empty(cnames [\<mapsto>] vitems))
        in  h(lobj \<mapsto> objs )),
     inih,
     [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := k_fresh],
          safeP, sigSafeMain, pc + length (concat (map fillAux (zip items [1..<length items + 1]))), ref)])"


axioms regAux_instrs:
  "P'\<turnstile> 
    (None, sha, h, inih,
    [([], 
      vs[Suc 0 := Intg ii, 2 := Addr lobj], 
      safeP, sigSafeMain, pc, ref)])
 -jvm->
    (None, sha, h, inih,
    [([], 
     vs[Suc 0 := Intg ii, 2 := Addr lobj, 3 := Intg j], 
     safeP, sigSafeMain, pc + length (regAux item), ref)])"



axioms arrayIndex_S'_valid:
  "[| h l = Some (Arr ty m S'); 
    shp (stackC, topf) = Some (Intg n) |] 
   ==> n + 1 < int m ∧ 0 ≤ n + 1"


lemma S2_BUILDCLS:
  "execSVMInst (BUILDCLS C items item) (map_of ct) (hm, k) k0 
      (l, i) S = Either.Right S2
   ==> ∃ j'. 
      ((hm(getFresh hm \<mapsto> (j', C, map (item2Val S) items)), k), k0, 
       (l, Suc i), Val (Val.Loc (getFresh hm)) # S) = S2 ∧
       j' ≤ k"
apply (unfold execSVMInst.simps)
apply (case_tac "item2Stack (snd (hm, k)) S item",simp_all)
  apply (insert RightNotUndefined)
  apply (erule_tac x= "S2" in allE, force)
 apply (split split_if_asm,simp)
  apply (rename_tac j)
  apply (rule_tac x="j" in exI,simp)
 apply simp
by (erule_tac x= "S2" in allE, force)

lemma equivS_n_ge_minus_1:
  "equivS S S' n ctm d g ==> n >= -1"
apply (case_tac S)
 apply (simp add: equivS.simps)
apply (case_tac a)
  apply (simp add: equivS.simps)
 apply (simp add: equivS.simps)
apply (simp add: equivS.simps)
apply (case_tac x)
by (simp add: equivS.simps)

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')"

lemma equivS2_BUILDCLS:
  "[| equivS S S' n ctm d g;
     d (nat ii) = Some (Addr lobj) |] 
   ==> equivS (Val (Val.Loc (getFresh hm)) # S) (S'(nat (n + 1) \<mapsto> Intg ii)) (n + 1) 
              ctm d (g(getFresh hm \<mapsto> lobj))"
apply (frule equivS_n_ge_minus_1)
apply (simp add: equivS.simps)
apply (frule equivS_ge_n_distinct_g)
apply (erule_tac x="1" in allE) apply clarsimp
apply (subgoal_tac "nat (1 + n) = nat (n + 1)")
apply force
by arith


axioms maxPush_BUILDCLS:
 "n + 1 < int m"

axioms getFresh_notin_dom_h:
 "getFresh hm ∉ dom hm"

axioms lobj_notin_ran_g:
 "lobj ∉ ran g"


declare append.simps [simp del]

(** Lemmas for equivV_items **)

axioms S_good:
 "[| equivS S S' (the_Intg (the (sh (stackC, topf)))) ctm d g;
    execSVMInst (BUILDCLS C items item) (map_of ct) (H, k) 
                (nat (the_Intg (the (sh (heapC, k0f))))) (l, i) S = Either.Right S2 |] 
  ==> (∀ i < length items. ∀ v . items!i = ItemConst v --> (∀ v'. v ≠ Val.Loc v')) ∧
      (∀ i < length items. ∀ n . items!i = ItemVar n --> (∀ z . S!+n ≠ Cont z)) ∧
      (∀ i < length items. ∀ n . items!i = ItemVar n --> (∀ r . S!+n ≠ Reg r)) ∧
      (∀ i < length items. items!i ≠ ItemRegSelf) ∧
      (∀ n < length S. ∀ z . S!+n ≠ Cont z) ∧
      (∀ i < length items. ∀ n . items!i = ItemVar n --> n < nat (the_Intg (the (sh (stackC, topf)))) ∧ n < length S)"

axioms map_argCell:
 "argCell [(tagGf, cellC) \<mapsto> Intg (int (the (com C))), 
           map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] map (Item2val S' sha) items] i =
  argCell [(VName (''arg'' @ nat2Str i), cellC) \<mapsto> Item2val S' sha (items!i)] i"

axioms argCell_i:
 "argCell [(VName (''arg'' @ nat2Str i), cellC) \<mapsto> A] i = A"

declare equivV.simps [simp del]

axioms equivS_nth_2:
  "[| equivS S S' ntop ctm d g;
    ∀ i < length S . ∀ z . S!+i ≠ Cont z;
    i < length S;
    S!+i = Val v|] ==> equivV v (the (S' (nat ntop - i))) d g"

axioms equivV_distinct_g:
  "equivV v (the (S' (nat (the_Intg (the (sh (stackC, topf)))) - n))) d g
  ==> equivV v (the (S' (nat (the_Intg (the (sh (stackC, topf)))) - n))) d g'"

lemma equivV_items:
  "[| i < length items; 
     equivS S S' (the_Intg (the (sh (stackC, topf)))) ctm d g;
     ∀ i < length items. ∀ v . items!i = ItemConst v --> (∀ v'. v ≠ Val.Loc v');
     ∀ i < length items. ∀ n . items!i = ItemVar n --> (∀ z . S!+n ≠ Cont z);
     ∀ i < length items. ∀ n . items!i = ItemVar n --> (∀ r . S!+n ≠ Reg r);
     ∀ i < length items. items!i ≠ ItemRegSelf;
     ∀ n < length S. ∀ z . S!+n ≠ Cont z;  
     ∀ i < length items. ∀ n . items!i = ItemVar n --> n < nat (the_Intg (the (sh (stackC, topf)))) ∧ n < length S|] 
   ==>
   equivV (item2Val S (items ! i))
              (argCell
                [(tagGf, cellC) \<mapsto> Intg (int (the (com C))), map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                 map (Item2val S' sh) items]
                i)
              d
              (g(getFresh H \<mapsto> lobj))"
apply (case_tac "(items ! i)")
 (*  ItemConst Val *)
 apply simp
 apply (case_tac Val)
   (* Val.Loc *)
   apply force
   (* IntT *)
   apply (simp add: equivV.simps)
   apply (subst map_argCell,simp)
   apply (simp add: isBool_def)
   apply (subst argCell_i,simp)
   (* BoolT *)
   apply (simp add: equivV.simps)
   apply (subst map_argCell,simp)
   apply (simp add: isBool_def)
   apply (subst argCell_i,simp)
   apply (rule impI)
   apply (subst argCell_i,simp)
 (* ItemVar *)
 apply (rename_tac n)
 apply simp
 apply (case_tac "S !+ n")
  (* S !+ nat = Val Vala *)
  apply simp
  apply (rotate_tac 6)
  apply (erule_tac x="i" in allE) apply simp apply (elim conjE)
  apply (frule equivS_nth_2) 
  apply force
  apply assumption
  apply assumption
  apply (subst map_argCell)
  apply clarsimp
  apply (subst argCell_i)
  apply (erule equivV_distinct_g)
  (* S !+ n = Reg nata *)
  apply force
  (* S !+ n = Cont x *)
  apply force
 (* ItemRegSelf *)
 by force

declare equivV.simps [simp]

axioms com_C:
  " com C = Some (nat (the_Intg
                 (the ([(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                         map (Item2val S' sha) items]
                       (tagGf, cellC)))))"


lemma domH_BUILDCLS:
    "[| ran g = activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))); finite (dom H); dom g = dom H;
     j ≤ (nat (the_Intg (the (sha (heapC, kf)))));
     activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) ∩ {la, l', l''} = {};
     lobj ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) ∧ lobj ∉  {la,l',l''};
     equivS Sa S' (the_Intg (the (sha (stackC, topf)))) ctm d g;
     ∀ i < length items. ∀ v . items!i = ItemConst v --> (∀ v'. v ≠ Val.Loc v');
     ∀ i < length items. ∀ n . items!i = ItemVar n --> (∀ z . Sa!+n ≠ Cont z);
     ∀ i < length items. ∀ n . items!i = ItemVar n --> (∀ r . Sa!+n ≠ Reg r);
     ∀ i < length items. items!i ≠ ItemRegSelf;
     ∀ n < length Sa. ∀ z . Sa!+n ≠ Cont z;  
     ∀ i < length items. ∀ n . items!i = ItemVar n --> n < nat (the_Intg (the (sha (stackC, topf)))) ∧ n < length Sa;
     ∀ j''. j'' ≠ j -->  
           region regS' (h(lobj \<mapsto>  Obj cellC
                  [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                    map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                    map (Item2val S' sha) items],
         l' \<mapsto> Arr ty m' regS', la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))) j'' = region regS h j'';
     region regS' (h(lobj \<mapsto>  Obj cellC
                  [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                         map (Item2val S' sha) items],
         l' \<mapsto> Arr ty m' regS', la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))) j = region regS h j ∪ {lobj};
     ∀l∈dom H. ∃l'. l' = the (g l) ∧ equivC (the (H l)) h l' (the (h l')) (nat (the_Intg (the (sha (heapC, kf))))) com regS d g|]
    ==> ∀l∈dom (H(getFresh H \<mapsto> (j, C, map (item2Val Sa) items))).
          ∃l'a. l'a = the ((g(getFresh H \<mapsto> lobj)) l) ∧
                equivC (the ((H(getFresh H \<mapsto> (j, C, map (item2Val Sa) items))) l))
                 (h(lobj \<mapsto>
                  Obj cellC
                   [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                         map (Item2val S' sha) items],
                  l' \<mapsto> Arr ty m' regS', la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii))))
                 l'a (the ((h(lobj \<mapsto>
                            Obj cellC
                             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                               map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                               map (Item2val S' sha) items],
                            l' \<mapsto> Arr ty m' regS', la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii))))
                            l'a))
                 (nat (the_Intg (the (sha (heapC, kf))))) com regS' d (g(getFresh H \<mapsto> lobj))"
apply (rule ballI)
apply (erule_tac x="l" in ballE)
 apply (elim exE, elim conjE) 
  apply (case_tac "l ≠ getFresh H")
 apply (rule_tac x="l'a" in exI)
 apply (rule conjI)
  apply clarsimp
 apply simp
 apply (elim exE) apply (elim conjE)
 apply (elim exE) apply (elim conjE)
 apply (subgoal_tac "the (g l) ≠ lobj ∧ the (g l) ≠ l' ∧ the (g l) ≠ la",simp) 
 prefer 2 
 apply (simp add: activeCells_def)
 apply (erule_tac x="ja" in allE)+ apply simp
 apply blast 
 apply (rule_tac x="Obja" in exI)
 apply (rule_tac x="flds" in exI)
 apply (rule conjI, rule refl)
 apply (rule conjI, rule refl)
 apply (rule conjI)
 apply clarsimp
  apply (erule_tac x="ja" in allE) 
  apply (case_tac "ja ≠ j")
   apply clarsimp 
   apply clarsimp
 apply (rule allI)
 apply (erule_tac x="i" in allE)+
 apply (rule impI) apply simp
 apply (case_tac "(vs ! i)")
 apply simp
 apply (elim conjE)
 apply (subgoal_tac "nata ≠ getFresh H",simp)
 apply (subgoal_tac "getFresh H ∉ dom g") apply force
 apply (subgoal_tac "getFresh H ∉ dom H") apply simp
 apply (rule getFresh_notin_dom_h)
 apply simp
 apply simp

 (* l = getFresh H *)
 apply simp
 apply (rule_tac x="Obj" in exI)
 apply (rule_tac x="[(tagGf, cellC) \<mapsto> Intg (int (the (com C))), map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                        map (Item2val S' sha) items]" in exI)
 apply (rule conjI, rule refl)
 apply (rule conjI)
 apply clarsimp 

 apply (subgoal_tac " com C =
               Some (nat (the_Intg
                           (the ([(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                                  map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] map (Item2val S' sha) items]
                                  (tagGf, cellC)))))",simp)
 apply (rule com_C)
 apply (rule allI)
 apply (rule impI)
 apply (subgoal_tac "equivV (item2Val Sa (items ! i))
              (argCell
                [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                         map (Item2val S' sha) items]
                i)
              d (g(getFresh H \<mapsto> lobj))",simp)
apply (rule equivV_items) apply assumption+ apply clarsimp apply assumption+ apply clarsimp
apply simp
apply simp
apply (rule_tac x="Obj" in exI)
apply (rule_tac x="[(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                         map (Item2val S' sha) items]" in exI)
apply (rule conjI)
apply (rule refl)
apply (rule conjI)
apply (rule com_C)
apply (rule allI) apply (rule impI)
apply (rule equivV_items) apply assumption+ apply clarsimp apply assumption+ apply clarsimp
by simp






lemma ran_upd_getFresh:
  "[| lobj ∉ ran g; x ∈ ran g; getFresh H ∉ dom g|]
        ==> x ∈ ran (g(getFresh H \<mapsto> lobj))"
apply (simp add: ran_def)
apply (erule exE)
apply (erule_tac x="a" in allE,simp)
apply (rule_tac x="a" in exI)
apply (rule conjI)
 apply blast
by blast

lemma disjoint_getFresh:
  "[| x ∈ ran (g(getFresh H \<mapsto> lobj)); lobj ∉ ran g |] 
   ==> x∈ ran g ∨ x = lobj"
apply (simp add: ran_def)
apply (split split_if_asm,clarsimp)
by (rule_tac x="a" in exI, simp) 

lemma disjoint_getFresh_2:
  "[|  x∈ ran g ∨ x = lobj; lobj ∉ ran g; getFresh H ∉ dom g |] 
   ==> x ∈ ran (g(getFresh H \<mapsto> lobj))"
apply (erule disjE)
 apply (simp add: ran_def)
 apply (erule exE)
 apply (rule_tac x="a" in exI)
 apply (rule conjI,clarsimp) 
 apply clarsimp
by (simp add: ran_def)


axioms getFresh_notin_dom_g:
  "getFresh hm ∉ dom g"

lemma activeCells_BUILDCLS:
 "[| l' ∉ activeCells regS dh (nat (the_Intg (the (sha (heapC, kf)))));
    j ≤ (nat (the_Intg (the (sha (heapC, kf)))));
     ∀ j'. j'≠ j -->  region regS' (h(lobj \<mapsto>
         Obj cellC
          [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                         map (Item2val S' sha) items],
         l' \<mapsto> Arr ty m' regS', la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))) j' = region regS h j';
 ran g = activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
    region regS' (h(lobj \<mapsto>
         Obj cellC
          [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                         map (Item2val S' sha) items],
         l' \<mapsto> Arr ty m' regS', la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))) j = insert lobj (region regS h j) |] 
  ==> ran (g(getFresh hm \<mapsto> lobj)) =
       activeCells regS'
        (h(lobj \<mapsto>
         Obj cellC
          [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                         map (Item2val S' sha) items],
         l' \<mapsto> Arr ty m' regS', la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii))))
        (nat (the_Intg (the (sha (heapC, kf)))))"
apply (rule equalityI)
 apply (rule subsetI)
 apply (subgoal_tac "lobj ∉ ran g")
  prefer 2 apply (rule lobj_notin_ran_g)
 apply (subgoal_tac "x∈ ran g ∨ x = lobj",simp)
  prefer 2 apply (rule disjoint_getFresh,assumption+)
 apply (erule disjE)
  (* x ∈ ran g *)
  apply (simp add: activeCells_def)
  apply (elim exE)
  apply (rule_tac x="ja" in exI,simp,elim conjE)
  apply (erule_tac x="ja" in allE)+
  apply (case_tac "ja = j") apply simp
  apply simp
 apply simp
 (* x = lobj *)
 apply (simp add: activeCells_def)
 apply (rule_tac x="j" in exI)
 apply  (rule conjI)
 apply (erule_tac x="getFresh hm" in allE)
 apply assumption
 apply simp

apply (rule subsetI)
apply (subgoal_tac "lobj ∉ ran g")
 prefer 2 apply (rule lobj_notin_ran_g)
apply (subgoal_tac "getFresh hm ∉ dom g")
 prefer 2 apply (rule getFresh_notin_dom_g)
apply (simp add: activeCells_def)
apply (erule exE) apply (elim conjE)
apply (erule_tac x="ja" in allE)+
apply simp
apply (case_tac "ja = j") 
 apply simp
apply (erule disjE)
 apply simp defer (* x = lobj *)
 apply (subgoal_tac "lobj ∉ ran g")
  prefer 2 apply (rule lobj_notin_ran_g)
apply (subgoal_tac "x ∈ ran g")
apply (rule ran_upd_getFresh) apply assumption+
apply (subgoal_tac "x ∈ {p. ∃j≤nat (the_Intg (the (sha (heapC, kf)))). p ∈ region regS h j}")
apply simp
apply clarsimp
apply (subgoal_tac "x ∈ region regS h ja")
 prefer 2 apply simp
apply (subgoal_tac "x ∈ ran g")
apply (subgoal_tac "lobj ∉ ran g")
 prefer 2 apply (rule lobj_notin_ran_g)
apply (subgoal_tac "getFresh hm ∉ dom g")
 prefer 2 apply (rule getFresh_notin_dom_g)
apply (rule disjoint_getFresh_2) apply simp apply simp apply simp
apply (subgoal_tac "x ∈ {p. ∃j≤nat (the_Intg (the (sha (heapC, kf)))). p ∈ region regS h j}")
apply simp
apply simp
apply (rule_tac x="ja" in exI)
apply simp
apply (subgoal_tac "lobj ∉ ran g")
 prefer 2 apply (rule lobj_notin_ran_g)
apply (simp add: ran_def)
by force




lemma equivH_BUILDCLS:
  "[| equivH (H, ka) h (nat (the_Intg (the (sha (heapC, kf))))) com regS d g; j ≤ ka;
     dom g = dom H;
     activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) ∩ {la, l', l''} = {};
     lobj ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))); lobj ∉ {la, l', l''};
     equivS Sa S' (the_Intg (the (sha (stackC, topf)))) ctm d g;
     ∀ i < length items. ∀ v . items!i = ItemConst v --> (∀ v'. v ≠ Val.Loc v');
     ∀ i < length items. ∀ n . items!i = ItemVar n --> (∀ z . Sa!+n ≠ Cont z);
     ∀ i < length items. ∀ n . items!i = ItemVar n --> (∀ r . Sa!+n ≠ Reg r);
     ∀ i < length items. items!i ≠ ItemRegSelf;
     ∀ n < length Sa. ∀ z . Sa!+n ≠ Cont z;  
     ∀ i < length items. ∀ n . items!i = ItemVar n --> n < nat (the_Intg (the (sha (stackC, topf)))) ∧ n < length Sa;
     ∀ j''. j'' ≠ j -->  
           region regS' 
                  (h(lobj \<mapsto>  Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                                          map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                                          map (Item2val S' sha) items],
                     l' \<mapsto> Arr ty m' regS', 
                     la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))) 
                  j'' = region regS h j'';
     region regS' 
            (h(lobj \<mapsto>  Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                                    map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                                    map (Item2val S' sha) items],
               l' \<mapsto> Arr ty m' regS', 
               la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))) j = region regS h j ∪ {lobj}
    |] 
   ==> equivH ((H(getFresh H \<mapsto> (j, C, map (item2Val Sa) items))), ka)
           (h(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                                  map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                                  map (Item2val S' sha) items],
              l' \<mapsto> Arr ty m' regS', 
              la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii))))
           (nat (the_Intg (the (sha (heapC, kf)))))
           com regS' d (g(getFresh H \<mapsto> lobj))"
apply (simp add: heapC_def add: stackC_def)
apply (fold heapC_def)
apply (unfold equivH.simps, elim conjE)
apply (rule conjI, clarsimp) 
apply (rule conjI)
apply (rule activeCells_BUILDCLS,assumption+,simp,assumption+)
apply (rule conjI, simp)
apply (fold stackC_def)
apply (frule_tac la="la" and l'="l'" and l''="l''" and 
                 lobj="lobj" and C="C" and Sa="Sa" in domH_BUILDCLS) 
by (assumption+,simp+)



(* inj_on lemma *)

lemma notin_ran:
  "x ∉ ran g ==> ∀ y . g y ≠ Some x" 
by (clarsimp, simp add: ran_def)

lemma inj_on_BUILDCLS:
  "[| ((hm, k), k0, (l, i), S) = ((H, ka), k0a, PC, Sa);
       inj_on g (dom H) |] 
   ==> inj_on (g(getFresh hm \<mapsto> lobj)) (dom (hm(getFresh hm \<mapsto> (j', C, map (item2Val S) items))))"
apply (subgoal_tac "getFresh hm ∉ dom g") 
 prefer 2 apply (rule getFresh_notin_dom_g)
apply (subgoal_tac "getFresh hm ∉ dom hm") 
 prefer 2 apply (rule getFresh_notin_dom_h)
apply (subgoal_tac "lobj ∉ ran g") 
 prefer 2 apply (rule lobj_notin_ran_g)
apply clarsimp
apply (simp add: inj_on_def)
apply (split split_if_asm)
apply (simp add: getFresh_def add: fresh_def,auto)
 apply (split split_if_asm,auto)
apply (frule notin_ran)
apply (erule_tac x="x" in allE)
by simp

axioms activeCells_3:
  "[| l' ∉ activeCells regS h k; l ≠ l'; l ≠ l'' |] 
   ==> l' ∉ activeCells regS (h(l \<mapsto> A, l''\<mapsto> B)) k"

axioms activeCells_3_1:
  "[| l' ∉ activeCells regS h k |] 
   ==> l' ∉ activeCells regS (h(l' \<mapsto> A, l''\<mapsto> B)) k"

axioms activeCells_4:
  "la ∉ activeCells regS h k
   ==> la ∉ activeCells regS' h k'"

axioms activeCells_5:
  "la ∉ activeCells regS h k
   ==> la ∉ activeCells regS' h' k'"

axioms drop_append_length_2:
  "drop n xs = (ys @ zs) @ ms ==> drop (n + length ys) xs = zs @ ms"

declare List.upt.upt_Suc [simp del]
declare execSVMInst.simps [simp del]
declare equivH.simps [simp del]

(************** execSVMInstr_BUILDCLS_reserveCell **************)

thm drop_append_length

axioms drop_append_length_3:
  "drop n xs = ys @ zs @ ms ==> drop (n + length ys) xs = zs @ ms"

lemma execSVMInstr_BUILDCLS_reserveCell :
    "[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
       S1' = (None, sh, dh, ih, [([], vs, safeP, sigSafeMain, pc,ref)]);
       k' = nat (the_Intg (the (sha (heapC, kf))));
       (fst (the (map_of svms p)) ! i) = BUILDCLS C items item;
       execSVMInst (BUILDCLS C items item) (map_of ct) (hm, k) k0 (p, i) S = Either.Right S2;
       drop (the (cdm (p, i))) (extractBytecode P') =
       trInstr (the (cdm (p, i))) cdm' ctm' com pcc (BUILDCLS C items item) @ bytecode';
       sh (stackC, Sf) = Some (Addr l);
       distinct [l, l', l''];  
       sh (heapC, regionsf) = Some (Addr l'); dh l' = Some (Arr ty m' regS);
       sh (dirCellC, safeDirf) = Some (Addr l''); dh l'' = Some (Arr ty m'' d);
       pc = the (cdm (p,i))

     |] ==>
      P' \<turnstile> S1' -jvm-> 
            (None,sh,dh',ih, [([Intg ii], vs, safeP, sigSafeMain, pc + 1, ref)]) ∧ 
      d (nat ii) = Some (Addr lobj) ∧ 
      dh' = dh( lobj \<mapsto> obj) ∧ 
     lobj ∉ activeCells regS dh k' ∧
     lobj ∉ {l,l',l''} ∧
     the_obj obj = (cellC, empty) ∧
     ii < int m'' ∧ 0 < ii"

(* Now, we prove that the JVM sequence leads to the reserveCell arrival state *)
apply (subgoal_tac 
  "P' |- 
  (None,sh,dh,ih,[([], vs, safeP, sigSafeMain, the (cdm (p, i)), ref)])  
    -jvm->
  (None, sh, dh', ih, [([Intg ii], vs, safeP,sigSafeMain,the (cdm (p, i))+1,ref)]) ∧
  d (nat ii) = Some (Addr lobj) ∧ 
  dh' = dh(lobj \<mapsto> obj) ∧ 
  lobj ∉ activeCells regS dh k' ∧
  lobj ∉ {l, l',l''} ∧
  the_obj obj = (cellC, empty) ∧
  ii < int m'' ∧ 0 < ii")
prefer 2 apply (rule reserveCell_method) apply (simp,assumption+)
 apply (unfold extractBytecode_def)
 apply (unfold trInstr.simps)
 apply (unfold Let_def)
apply (simp,erule nth_via_drop_append)
by clarsimp

lemma execSVMInstr_BUILDCLS :
    "[| (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) = BUILDCLS C items item;
       execSVMInst (BUILDCLS C items item) (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 (BUILDCLS C items item) @ 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
   "∃ j. 
      ((hm(getFresh hm \<mapsto> (j, C, map (item2Val S) items)), k), k0, 
       (l, Suc i), Val (Val.Loc (getFresh hm)) # S) = S2 ∧ j ≤ k")
prefer 2 apply (erule S2_BUILDCLS) 
apply (elim exE, elim conjE)

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

(* we go on with the main goal. We instantiate the arrival JVM state*)
apply (rule_tac x="None" in exI)
apply (rule_tac x="sha((stackC, topf) \<mapsto> Intg (n + 1))" in exI)
apply (rule_tac x="h(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                                         map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>] 
                                         map (Item2val S' sha) items],
                     l' \<mapsto> Arr ty m' regS', 
                     la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))" in exI) 
apply (rule_tac x=inih in exI)
apply (rule_tac x="[([], 
                      vs[Suc 0 := Intg ii, 2 := Addr lobj, 3 := Intg (int j)], 
                      safeP, sigSafeMain,
                      Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
                      (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) + 
                      length (regAux item) + 
                      length (concat (map fillAux (zip items [Suc 0..<Suc (length items)]))))))))))))))))))))))), 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 (subgoal_tac "length vs = 10")
prefer 2 apply (rule length_vs)


apply (subgoal_tac "PC = (l,i)") 
 prefer 2 apply simp 

apply (drule_tac r="S1'" in trans,assumption)

apply (rule conjI)

(* Invoke_static dirCellC reserveCell [] *)
apply (frule_tac dh'="h'" and lobj="lobj" and obj="obj" and ii="ii" in execSVMInstr_BUILDCLS_reserveCell)
apply assumption+ apply simp
apply (elim conjE)

apply (unfold exec_all_def)
apply (erule rtrancl_trans)
 apply (unfold extractBytecode_def)
 apply (unfold trInstr.simps)
 apply (unfold Let_def) 

(* Store 1 *) 
apply (drule drop_Suc_append_2)
apply (subgoal_tac 
  "P'\<turnstile> (None,sh,h',ih,[([Intg ii], vs, safeP, sigSafeMain, pc + 1, ref)]) 
   -jvm->
       (None,sh,h',ih,[([], vs[Suc 0 := Intg ii], safeP, sigSafeMain, pc + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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)))) = 
     Store 1",simp)
 apply (simp, erule nth_via_drop_append) 

(* Getstatic safeDirf dirCellC *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> (None,sh,h',ih,[([], vs[Suc 0 := Intg ii], safeP, sigSafeMain, pc + 1 + 1, ref)])
   -jvm->
       (None,sh,h',ih,
       [([Addr l''], 
       vs[Suc 0 := Intg ii], 
       safeP, sigSafeMain, pc + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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)))))) = 
    Getstatic safeDirf dirCellC",simp)
apply (erule nth_via_drop_append)

(* Load 1 *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> (None,sh,h',ih,
        [([Addr l''], 
        vs[Suc 0 := Intg ii], 
        safeP, sigSafeMain, pc + 1 + 1 + 1, ref)])
  -jvm->
       (None,sh,h',ih,
       [([Intg ii, 
          Addr l''], 
       vs[Suc 0 := Intg ii], 
       safeP, sigSafeMain, pc + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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 (the (cdm (l, i)))))))  = 
     Load (Suc 0)",simp)
apply (erule nth_via_drop_append)

(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> (None,sh,h',ih,
        [([Intg ii, 
           Addr l''], 
        vs[Suc 0 := Intg ii], 
        safeP, sigSafeMain, pc + 1 + 1 + 1 + 1, ref)])
  -jvm->
       (None,sh,h',ih,
       [([Addr lobj], 
       vs[Suc 0 := Intg ii], 
       safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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))))))))  = 
     ArrLoad",simp)
apply (simp add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)

(* Store 2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> (None,sh,h',ih,
        [([Addr lobj], 
        vs[Suc 0 := Intg ii], 
        safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1, ref)])
  -jvm->
       (None,sh,h',ih,
       [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj], 
       safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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))))))))) = 
    Store 2",simp) 
apply (erule nth_via_drop_append)

(* Load 2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> (None,sh,h',ih,
       [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj], 
       safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1 + 1, ref)])
  -jvm->
       (None,sh,h',ih,
       [([Addr lobj], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj], 
       safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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)))))))))) = 
    Load 2",simp) 
apply (erule nth_via_drop_append) 

(* LitPush (Intg (int tagg)) *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> (None,sh,h',ih,
        [([Addr lobj], 
        vs[Suc 0 := Intg ii,
               2 := Addr lobj], 
        safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])
  -jvm->
       (None,sh,h',ih,
       [([Intg (int (the (com C))),
          Addr lobj], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj], 
       safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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))))))))))) = 
    LitPush (Intg (int (the (com C))))",simp) 
apply (erule nth_via_drop_append) 

(* Putfield tagGf cellC *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> (None,sh,h',ih,
        [([Intg (int (the (com C))),
           Addr lobj], 
        vs[Suc 0 := Intg ii,
               2 := Addr lobj], 
        safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])
  -jvm->
       (None,sh, h'(lobj \<mapsto> Obj cellC (empty((tagGf, cellC) \<mapsto> Intg (int (the (com C)))))),ih,
       [([], 
       vs[Suc 0 := Intg ii,
             2 := Addr lobj], 
       safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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)))))))))))) = 
    Putfield tagGf cellC",simp) 
apply (simp add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)  

(* regAux item *)
apply (drule drop_Suc_append)
apply (subgoal_tac
  "P'\<turnstile> 
    (None, sh, 
    h'(lobj \<mapsto> Obj cellC (empty((tagGf, cellC) \<mapsto> Intg (int (the (com C)))))), 
    ih,
    [([], 
      vs[Suc 0 := Intg ii, 2 := Addr lobj], 
      safeP, sigSafeMain, pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])
 -jvm->
    (None, sh, 
    h'(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C)))]), 
    ih,
    [([], 
     vs[Suc 0 := Intg ii, 2 := Addr lobj, 3 := Intg (int j)], 
     safeP, sigSafeMain, 
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item), ref)])")
prefer 2 apply (rule regAux_instrs)
apply (unfold exec_all_def)
apply (simp, erule rtrancl_trans)

(* concat (map pushAux (zip items [0..<length items])) *) 
apply (drule drop_append_length_3)
apply (subgoal_tac 
  "P'\<turnstile> (None, sh, 
        h'(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C)))]), 
        ih,  [([],
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
       safeP,sigSafeMain,
       pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item), ref)])
  -jvm->
     (None,sh,
       (let vitems = Intg (int (the (com C))) # map (Item2val S' sh) items;
            cnames = (tagGf, cellC) # map (λ i.  (VName (''arg''@ nat2Str i),cellC)) [0..<length items];
            objs   = Obj cellC (empty(cnames [\<mapsto>] vitems))
        in  h'(lobj \<mapsto> objs )),
     ih,
     [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
       safeP, sigSafeMain,
       pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))), ref)])")
prefer 2 apply (rule fillAux_instrs)
apply (unfold exec_all_def)
apply (simp,erule rtrancl_trans)

(* Load 3 *) 
apply (drule drop_append_length_3)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None,sh,
       (let vitems = Intg (int (the (com C))) # map (Item2val S' sh) items;
            cnames = (tagGf, cellC) # map (λ i.  (VName (''arg''@ nat2Str i),cellC)) [0..<length items];
            objs   = Obj cellC (empty(cnames [\<mapsto>] vitems))
        in  h'(lobj \<mapsto> objs )),
     ih,
     [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
       safeP, sigSafeMain,
       pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))), ref)])
 -jvm->
    (None,sh,
       (let vitems = Intg (int (the (com C))) # map (Item2val S' sh) items;
            cnames = (tagGf, cellC) # map (λ i.  (VName (''arg''@ nat2Str i),cellC)) [0..<length items];
            objs   = Obj cellC (empty(cnames [\<mapsto>] vitems))
        in  h'(lobj \<mapsto> objs )),
     ih,
     [([Intg (int j)], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
       safeP, sigSafeMain,
       pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))) + 1, ref)])")
apply (unfold exec_all_def)
apply (simp,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 (Suc (the (cdm (l, i))))))))))) + length (regAux item) +
    length (concat (map fillAux (zip items [1..<length items + 1])))) =  
    Load 3",simp)
apply (simp,erule nth_via_drop_append)

(* Load (Suc 0) *) 
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None,sh,
        h'(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sh) items]),
     ih,
     [([Intg (int j)], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
       safeP, sigSafeMain,
       pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))) + 1, ref)])
 -jvm->
    (None,sh,
        h'(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sh) items]),
     ih,
     [([Intg ii,
        Intg (int j)], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
       safeP, sigSafeMain,
       pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1, ref)])")
apply (unfold exec_all_def) 
apply (simp, 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 (Suc (Suc (the (cdm (l, i))))))))))) + length (regAux item) +
    length (concat (map fillAux (zip items [1..<length items + 1]))))) =
    Load 1",simp) 
apply (simp,erule nth_via_drop_append)

(* Invoke_static heapC insertCell [PrimT Integer, PrimT Integer] *)
apply (drule drop_Suc_append)
apply (subgoal_tac
  "P' |- 
  (None,sha,
        h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items]),
     inih,
     [([Intg ii,
        Intg (int j)], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
       safeP, sigSafeMain,
       the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1, ref)])
 -jvm-> 
     (None, sha, 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1, ref)])")
prefer 2 
apply (rule_tac obj="Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items]" and iloc="ii" in insertCell_method_jvm)
apply (simp, assumption+) 
apply (simp, erule nth_via_drop_append) 
apply (unfold exec_all_def)
apply (elim conjE)
apply (simp, erule rtrancl_trans)


(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None, sha, 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1, ref)])
 -jvm->
    (None, sha, 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg n], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp, 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 (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) + length (regAux item) +
    length (concat (map fillAux (zip items [1..<length items + 1]))))))) =
    Getstatic topf stackC",simp) 
apply (simp, erule nth_via_drop_append)

(* LitPush (Intg 1) *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None, sha, 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg n], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1, ref)])
 -jvm->
    (None, sha, 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg 1, 
        Intg n], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp, 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 (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) + length (regAux item) +
    length (concat (map fillAux (zip items [1..<length items + 1])))))))) =
    LitPush (Intg 1)",simp) 
apply (simp, erule nth_via_drop_append)

(* BinOp Add *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None, sha, 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg 1, 
        Intg n], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1, ref)])
 -jvm->
    (None, sha, 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg (n + 1)], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 +1, ref)])")
apply (unfold exec_all_def)
apply (simp, 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 (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) + 
    length (regAux item) + length (concat (map fillAux (zip items [1..<length items + 1]))))))))) =
    BinOp Add",simp) 
apply (simp, erule nth_via_drop_append)

(* Putstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None, sha, 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg (n + 1)], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1, ref)])
 -jvm->
    (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 +1, ref)])")
apply (unfold exec_all_def)
apply (simp, 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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) + 
    length (regAux item) + length (concat (map fillAux (zip items [1..<length items + 1])))))))))) =
    Putstatic topf stackC",simp) 
apply (simp, erule nth_via_drop_append)

(*  Getstatic Sf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])
 -jvm->
    (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Addr la], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1, ref)])")
apply (unfold exec_all_def)
apply (simp, 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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) + 
    length (regAux item) + length (concat (map fillAux (zip items [1..<length items + 1]))))))))))) =
    Getstatic Sf stackC",simp) 
apply (simp add: Sf_def add: topf_def)
apply (simp, erule nth_via_drop_append)

(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Addr la], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])
 -jvm->
    (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg (n + 1),
        Addr la], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp, 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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) + 
    length (regAux item) + length (concat (map fillAux (zip items [1..<length items + 1])))))))))))) =
    Getstatic topf stackC",simp) 
apply (simp, erule nth_via_drop_append)

(* Load (Suc 0) *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg (n + 1),
        Addr la], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])
 -jvm->
    (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg ii,
        Intg (n + 1),
        Addr la], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
apply (simp, 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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) + 
    length (regAux item) + length (concat (map fillAux (zip items [1..<length items + 1]))))))))))))) =
    Load (Suc 0)",simp) 
apply (simp, erule nth_via_drop_append)

(* ArrStore *)
apply (drule drop_Suc_append)
apply (subgoal_tac 
  "P'\<turnstile> 
  (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
     h(lobj \<mapsto>
            Obj cellC
             [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items], l'  \<mapsto> Arr ty m' regS'), 
     inih, 
     [([Intg ii,
        Intg (n + 1),
        Addr la], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])
 -jvm->
    (None,  sha((stackC, topf) \<mapsto> Intg (n + 1)), 
      h(lobj \<mapsto>
          Obj cellC
           [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items],
          l' \<mapsto> Arr ty m' regS', la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii))), 
     inih, 
     [([], 
       vs[Suc 0 := Intg ii,
              2 := Addr lobj,
              3 := Intg (int j)],
     safeP,sigSafeMain,
     pc + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
     length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, ref)])")
apply (unfold exec_all_def)
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 (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) + 
    length (regAux item) + length (concat (map fillAux (zip items [1..<length items + 1])))))))))))))) =
    ArrStore",simp) 
apply (simp add: raise_system_xcpt_def)
apply (frule arrayIndex_S'_valid,assumption+)
apply simp
apply (simp, erule nth_via_drop_append)
apply simp


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

apply (rule_tac x="hm(getFresh hm \<mapsto> (j, C, map (item2Val S) items))" in exI)
apply (rule_tac x="k" in exI)
apply (rule_tac x="nat (the_Intg (the (sha (heapC, k0f))))" 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((stackC, topf) \<mapsto> Intg (n + 1))" in exI)
apply (rule_tac x="h(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                              map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                              map (Item2val S' sha) items],
                     l' \<mapsto> Arr ty m' regS', 
                     la \<mapsto> Arr ty m (S'(nat (n + 1) \<mapsto> Intg ii)))" in exI)
apply (rule_tac x="inih" in exI)
apply (rule_tac x="vs[Suc 0 := Intg ii, 2 := Addr lobj, 3 := Intg (int j)]" in exI)
apply (rule_tac x="Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
                      (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)) + 
                      length (regAux item) + 
                      length (concat (map fillAux (zip items [Suc 0..<Suc (length items)])))))))))))))))))))))))" in exI)
apply (rule_tac x="ref" in exI)

apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n + 1))) (heapC, kf))))" in exI)

apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n + 1))) (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'(nat (n + 1) \<mapsto> Intg ii)" in exI)

apply (rule_tac x="(n + 1)" 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(getFresh hm \<mapsto> lobj))" in exI)

(* Postconditions: reserveCell_method *)
apply (fold extractBytecode_def)
apply (frule_tac dh'="h'" and lobj="lobj" and obj="obj" and ii="ii" 
       in execSVMInstr_BUILDCLS_reserveCell)
apply (assumption+, simp add: trInstr.simps, assumption+,simp)
apply (elim conjE)

apply (thin_tac "P' \<turnstile> ?s1 -jvm-> ?s2")

(* Postconditions: inserCell_method *) 
apply (subgoal_tac
  "P' |- 
   (None, sha, dh(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                      map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                      map (Item2val S' sh) items]), 
    ih, 
    [([ Intg ii, Intg (int j)],
    vs,safeP, sigSafeMain,
    the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1,ref)])
  -jvm-> 
   (None, sha, dh(lobj \<mapsto> Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
                      map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
                      map (Item2val S' sh) items], l'  \<mapsto> Arr ty m' regS'), 
    ih, 
    [([], vs, safeP,sigSafeMain,
    the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1 + 1,ref)])")
prefer 2 apply (rule_tac 
   obj="Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
        map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
        map (Item2val S' sh) items]" and 
        iloc="ii" and j="j" and m''="m''" and d="d" and
        pc="the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1"
         in insertCell_method_jvm)
apply (simp, assumption+, simp, simp, simp, assumption+) 
apply (drule drop_Suc_append_2)
apply (drule drop_Suc_append)+
apply (drule drop_append_length)
apply (drule drop_append_length_2)
apply (drule drop_Suc_append)
apply (drule drop_Suc_append)
apply (simp add: extractBytecode_def)
apply (rule_tac zs="bytecode'" in nth_via_drop_append, force)

apply (frule_tac 
  obj="Obj cellC [(tagGf, cellC) \<mapsto> Intg (int (the (com C))),
           map (λi. (VName (''arg'' @ nat2Str i), cellC)) [0..<length items] [\<mapsto>]
           map (Item2val S' sh) items]" and
  pc="the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + length (regAux item) + 
       length (concat (map fillAux (zip items [1..<length items + 1]))) + 1 + 1" and
  P'="P'" in  insertCell_method_equivState)
apply assumption+ 
apply (drule drop_Suc_append_2)
apply (drule drop_Suc_append)+
apply (drule drop_append_length)
apply (drule drop_append_length_2)
apply (drule drop_Suc_append)
apply (drule drop_Suc_append)
apply (simp add: extractBytecode_def)
apply (rule_tac zs="bytecode'" in nth_via_drop_append, force)
apply simp
apply (elim conjE)

apply (thin_tac "P' \<turnstile> ?s1 -jvm-> ?s2")


apply (rule conjI, simp)
apply (rule conjI, simp) 
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: heapC_def add: stackC_def) 
apply (rule conjI) apply (erule activeCells_5)
apply (rule conjI) apply (erule activeCells_5)
                   apply (erule activeCells_5)
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 clarsimp
apply (rule conjI) apply clarsimp 
apply (rule conjI) apply (rule inj_on_BUILDCLS,assumption+)
apply (rule conjI) apply simp 
                   apply (simp add: heapC_def add: stackC_def)
                   apply (fold heapC_def)
                   apply (subgoal_tac "equivS Sa S' (the_Intg (the (sh (stackC, topf)))) ctm d g")
                   apply (frule S_good) apply simp
                   apply (rule_tac l''="l''" in equivH_BUILDCLS)
                   apply (assumption+,simp,assumption+,simp,simp,simp,simp,simp)
                   apply (simp,simp,simp,assumption+,simp,simp,fold stackC_def,simp)
apply (rule conjI) apply clarsimp 
                   apply (rule maxPush_BUILDCLS)
apply (rule conjI) apply clarsimp 
                   apply (rule equivS2_BUILDCLS,assumption+) 
apply (rule conjI) apply (simp add: heapC_def add: stackC_def)
by simp






end