Theory dem_SLIDE

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

theory dem_SLIDE
imports "../JVMSAFE/JVMExec" "../JVMSAFE/State" 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]

constdefs
 slideArray :: "[entries_ ,int,nat,nat] => entries_"
 "slideArray S ntop m n ≡ (
       let bs = map ( % i . the (S (nat(ntop)-m+i+1))) [0..<m]
       in S ( [nat(ntop)-m-n+1..<nat(ntop)-n+1] [\<mapsto>] bs))"

axioms slide_method:
 "[| s = (None, shp, hp, ihp, 
            ([Intg (int n),Intg (int m)],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');
  Invoke_static stackC slide [PrimT Integer,PrimT Integer] = 
                     fst(snd(snd(snd(snd(the(method' (P',safeP) sigSafeMain)))))) ! pc
  |] ==> 
  P' |- s -jvm-> (None, shp ((stackC,topf)\<mapsto> Intg (ntop-int n)), 
                            hp(l \<mapsto> Arr ty ma (slideArray S' ntop m n)), 
                            ihp, ([],loc,safeP,sigSafeMain,pc+1,z1,z2)#[])"

(* Lemmas for activeCells *)

declare equivH.simps [simp del]

lemma activeCells_SLIDE:
  "[| la ∉ activeCells regS h (nat (the_Intg (the (sh (heapC, kf)))))|] 
   ==> activeCells regS h (nat (the_Intg (the (sh (heapC, kf))))) =
       activeCells regS (h(la \<mapsto> Arr ty ma (slideArray S' na m n))) 
       (nat (the_Intg (the (sh (heapC, kf)))))"
apply (frule l_not_in_cellReg)
apply (unfold activeCells_def,auto)
 apply (unfold region_def, simp add: Let_def, elim conjE)
 apply (rule_tac x="j" in exI,simp) 
 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 (simp add: Let_def, elim conjE)
apply (rule_tac x="j" in exI, simp)
apply (rule cellReg_step) 
 apply (rule cellReg_basic)
 apply (erule_tac x="j" in allE) 
apply (erule cellsReg_monotone_2,assumption+)
by (erule l_not_in_regs)

(* Lemmas for domH *)


lemma domH_SLIDE:
  "[| la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))));
     ∀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.
          ∃l'. l' = the (g l) ∧
               equivC (the (H l)) (h(la \<mapsto> Arr ty ma (slideArray S' na m n))) l' 
               (the ((h(la \<mapsto> Arr ty ma (slideArray S' na m n))) l')) 
               (nat (the_Intg (the (sha (heapC, kf))))) com regS d g"
apply (frule l_not_in_cellReg)
apply (rule ballI)
apply (erule_tac x="l" in ballE) 
 prefer 2 apply simp
apply (erule exE)
apply (rule_tac x="l'" in exI) apply (elim conjE)
 apply (rule conjI, assumption)
apply clarsimp
apply (rule conjI, rule impI)
apply (simp add: region_def)
apply (rule impI)
apply (rule_tac x="Obj" in exI)
apply (rule_tac x="flds" in exI) apply simp
apply (simp add: region_def)
apply clarsimp
apply (rule cellReg_step) 
 apply (rule cellReg_basic)
 apply (erule_tac x="j" in allE)
 apply (rule cellsReg_monotone_1,assumption+)
by (erule l_not_in_regs)


lemma equivH_SLIDE:
  "[| ((hm, k), k0, (l, i), S) = ((H, ka), k0a, PC, Sa);
    k' = nat (the_Intg (the (sha (heapC, kf)))); 
    k0' = nat (the_Intg (the (sha (heapC, k0f)))); 
    sha (stackC, Sf) = Some (Addr la);
    distinct [la,l',l''];  h la = Some (Arr ty ma S'); 
    sha (stackC, topf) = Some (Intg na);
    sha (heapC, regionsf) = Some (Addr l'); 
    h l' = Some (Arr ty m' regS); 
    sha (dirCellC, safeDirf) = Some (Addr l'');
    h l'' = Some (Arr ty m'' d); inj_on g (dom H); 
    equivH (H, ka) h k' com regS d g;  k0a = k0';
    activeCells regS h k' ∩ {la, l', l''} = {}|]
    ==> equivH (hm, k) (h(la \<mapsto> Arr ty ma (slideArray S' na m n)))
        (nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (na - int n))) (heapC, kf))))) com regS d g"
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, frule activeCells_SLIDE,simp)
apply (rule conjI, assumption)
by (rule domH_SLIDE,assumption+)

axioms equivS_concat:
  "[| equivS (S1@S2) S' ntop ctm d g;
     n = length S1;
     ∀ i < n . ∀ z . S!i ≠ Cont z;
     ∀ i < n . S' (nat ntop - i) = S'' (nat ntop - i);
     equivS S3 S'' (ntop - int n) ctm d g  
   |] ==> equivS (S1@S3) S'' ntop ctm d g"

axioms equivS_concat2:
  "[| equivS (S1@S2) S' ntop ctm d g;
     n = length S1;
     ∀ i < n . ∀ z . S!i ≠ Cont z
   |] ==> equivS S2 S' (ntop - int n) ctm d g"

axioms equivS_same_subarray:
    "equivS (drop (m + n) S)
            (S'([nat ntop - m - n + 1..<nat ntop - n + 1] [\<mapsto>]
            map (λi. the (S' (nat ntop - m + i + 1))) [0..<m]))
            (ntop - int n - int m) ctm d g
       ==> equivS (drop (Suc m + n) S)
           (S'([nat ntop - Suc m - n + 1..<nat ntop - n + 1] [\<mapsto>]
            map (λi. the (S' (nat ntop - Suc m + i + 1))) [0..<Suc m]))
           (ntop - int n - int m - 1) ctm d g"

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

axioms equivS_nth_reg:
  "[| equivS S S' ntop ctm d g;
    n ≤  length S;
    ∀ i < n . ∀ z . S!i ≠ Cont z;
    i < n;
    S!i = Reg reg|] ==> reg =  nat (the_Intg (the (S' (nat ntop - i))))"

lemma equivS_SLIDE [rule_format]:
  "equivS S S' ntop ctm d g --> 
   length S ≥ m + n --> 
   (∀ i < m+n . ∀ z . S!i ≠ Cont z) --> 
   equivS (take m S @ drop (m + n) S) 
          (slideArray S' ntop m n) (ntop - int n) ctm d g"
apply (unfold slideArray_def)
apply (unfold Let_def)
apply (induct m)

(* base case m=0. By induction on n *)
apply simp
apply (induct_tac n)
 apply simp
apply (rule impI)+
apply (drule mp,simp)+
apply (subgoal_tac "drop n S = S!n # drop (Suc n) S")
apply clarsimp
apply (thin_tac "equivS ?x ?y ?z ?u ?v ?w")

(* we distinguish  according to the top of the stack *)
apply (case_tac "S!n")
 apply (simp add: equivS.simps)
 apply (elim conjE)
 apply (subgoal_tac "ntop - int n - 1=ntop - (1 + int n)",simp,simp)
 apply (simp add: equivS.simps)
 apply (elim conjE)
 apply (subgoal_tac "ntop - int n - 1=ntop - (1 + int n)",simp,simp)
 apply (erule_tac x=n in allE)
 apply (drule mp,simp,force)
apply (rule drop_nth3,simp)

(* inductive case m>0 *)
apply (rule impI)+
apply (drule mp,simp)+
apply (subgoal_tac "take m S @ (S!m # drop (Suc m + n) S) =
                    take (Suc m) S @ drop (Suc m + n) S")
apply (erule_tac s="take m S @ (S!m # drop (Suc m + n) S)" in subst)
 prefer 2
 apply (subgoal_tac "(take m S @ [S ! m]) @ drop (Suc m + n) S =
                    take m S @ S ! m # drop (Suc m + n) S")
 prefer 2 apply (rule sym,rule concat1)  
 apply (erule subst)
 apply (rule concat2)
 apply (rule sym,rule take_append3,simp)

(* we apply  a lemma to get rid of the first part of the stack *)
apply (subgoal_tac "ntop = int (length S) - 1")
 prefer 2 apply (erule equivS_length)
apply (rule equivS_concat)
 apply (simp del: upt_Suc)
 apply (subgoal_tac "m=length (take m S)")
  prefer 2 apply (rule take_length,simp) 
 apply simp
 apply (rule allI,rule impI,erule_tac x=i in allE,drule mp,simp,simp)
 defer

(* we make case distinction on the stack's top *)
apply (case_tac "S!m")

(* the top element is a value *)
apply (simp only: equivS.simps)
 apply (rule conjI,simp)
 apply (rule conjI) defer
apply (subgoal_tac "equivS (drop (m + n) S) 
          (S'([nat ntop - m - n + 1..<nat ntop - n + 1] [\<mapsto>]
          map (λi. the (S' (nat ntop - m + i + 1))) [0..<m]))
          ((ntop - int n)- int m) ctm d g")
 prefer 2 apply (rule equivS_concat2) apply simp
 apply (rule take_length,simp)
 apply (rule allI,rule impI,erule_tac x=i in allE,drule mp,simp,simp)
apply clarify
apply (erule equivS_same_subarray)

(* the top element is a region *)
apply (simp only: equivS.simps)
 apply (rule conjI,simp)
 apply (rule conjI) defer
apply (subgoal_tac "equivS (drop (m + n) S) 
          (S'([nat ntop - m - n + 1..<nat ntop - n + 1] [\<mapsto>]
          map (λi. the (S' (nat ntop - m + i + 1))) [0..<m]))
          ((ntop - int n)- int m) ctm d g")
 prefer 2  apply clarify apply (erule equivS_concat2) 
 apply (rule take_length,simp)
 apply (rule allI,rule impI,erule_tac x=i in allE,drule mp,simp,simp)
apply clarify
apply (erule equivS_same_subarray)

(* the top element cannot be a continuation *)
apply (erule_tac x=m in allE)
apply (drule mp,simp)
apply (erule_tac x="x" in allE)
apply force

(* we prove the three deferred objectives *)
(* the first m positions of both arrays coincide *)
apply (rule allI,rule impI)
apply (subgoal_tac "(Suc (nat ntop - (m + n))) + ((m-i)- 1) = nat (ntop - int n) - i")
apply (erule_tac s="Suc (nat ntop - (m + n)) + ((m-i)- 1)" in subst)
apply (subgoal_tac "(S'([Suc (nat ntop - (m + n))..<Suc (nat ntop - n)] [\<mapsto>]
              map (λi. the (S' (Suc (nat ntop - m + i)))) [0..<m]))
              (Suc (nat ntop - (m + n)) + ((m - i)- 1))=
              Some ((map (λi. the (S' (Suc (nat ntop - m + i)))) [0..<m])!((m - i)- 1))")
 prefer 2 apply (rule map_upds_nth)
 apply simp
apply clarify
apply (rule_tac s="Some (map (λi. the (S' (Suc (nat (int (length S) - 1) - m + i)))) [0..<m] 
                  ! (m - i - 1))" in subst)
prefer 2 apply simp
apply (thin_tac "?x=?y")
apply (subgoal_tac "(nat (int (length S) - 1) - Suc m - n + 1)+(m-i)=
                    Suc (nat (int (length S) - 1) - (m + n)) + (m - i - 1)")
apply (erule_tac s="nat (int (length S) - 1) - Suc m - n + 1 + (m - i)" in subst)
apply (subgoal_tac "(S'([nat (int (length S) - 1) - Suc m - n + 1..<nat (int (length S) - 1) - n + 1] 
              [\<mapsto>] map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m]))
              (nat (int (length S) - 1) - Suc m - n + 1 + (m - i))=
              Some ((map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m])
              ! (m-i))")
 prefer 2 apply (rule map_upds_nth)
 apply (erule additions1,simp)
apply (rule_tac s="Some (map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] !
                 (m - i))" and 
       t="(S'([nat (int (length S) - 1) - Suc m - n + 1..<nat (int (length S) - 1) - n + 1] [\<mapsto>]
           map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m]))
          (nat (int (length S) - 1) - Suc m - n + 1 + (m - i))" in subst)
apply (rule sym,assumption)
apply (thin_tac "?x=?y")
apply (simp only: nth_map_upt)
apply (subgoal_tac "Suc (nat (int (length S) - 1) - m + (0 + (m - i - 1)))=
                  nat (int (length S) - 1) - Suc m + (0 + (m - i)) + 1")
apply (erule_tac s="Suc (nat (int (length S) - 1) - m + (0 + (m - i - 1)))" in subst,rule refl)

(* we discharge some arithmetic identities *)
apply (simp (no_asm))
apply (erule additions2,simp) 
apply (simp (no_asm))
apply (erule additions3,simp) 
apply (simp (no_asm))

(* the value at S!m is equivalent to S'[ntop-m-n] *)
apply (subgoal_tac "(nat (int (length S) - 1) - Suc m - n + 1) + 0
       = nat (int (length S) - 1 - int n - int m)")
apply (erule_tac s="(nat (int (length S) - 1) - Suc m - n + 1) + 0" in subst)
apply (subgoal_tac 
      "(S'([nat (int (length S) - 1) - Suc m - n + 1..<nat (int (length S) - 1) - n + 1] [\<mapsto>]
       map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m]))
       (nat (int (length S) - 1) - Suc m - n + 1 + 0)=
       Some (map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] ! 0)")
 prefer 2 apply (rule map_upds_nth) apply simp
 defer
apply (rule_tac t="(S'([nat (int (length S) - 1) - Suc m - n + 1..<nat (int (length S) - 1) - n + 1] [\<mapsto>]
      map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m]))
      (nat (int (length S) - 1) - Suc m - n + 1 + 0)" and 
      s="Some (map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] ! 0)" 
      in subst) apply (rule sym,assumption)
apply (thin_tac "?x=Some ?y")
apply (subgoal_tac 
      "map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] ! 0
       =(λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) (0+0)")
 prefer 2 apply (rule nth_map_upt, simp (no_asm))
apply (rule_tac s="the (S' (nat (int (length S) - 1) - Suc m + (0 + 0) + 1))" 
       and t="map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] ! 0" 
       in subst,rule sym,assumption)
apply (rule_tac s="nat ntop - m" and t="nat (int (length S) - 1) - Suc m + (0 + 0) + 1" in subst)
apply (simp (no_asm)) apply clarify
apply (erule additions4) 
apply (simp (no_asm),clarify)
apply (erule_tac n="Suc m + n" in equivS_nth)
 apply (assumption,rule allI,rule impI,force,simp,assumption)
apply (simp (no_asm))
apply (erule additions5)
 prefer 2 apply (rule additions6,simp)

(* the region number at S!m is equivalent to S'[ntop-m-n] *)
apply (subgoal_tac "(nat (int (length S) - 1) - Suc m - n + 1) + 0
       = nat (int (length S) - 1 - int n - int m)")
apply (erule_tac s="(nat (int (length S) - 1) - Suc m - n + 1) + 0" in subst)
apply (subgoal_tac 
      "(S'([nat (int (length S) - 1) - Suc m - n + 1..<nat (int (length S) - 1) - n + 1] [\<mapsto>]
       map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m]))
       (nat (int (length S) - 1) - Suc m - n + 1 + 0)=
       Some (map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] ! 0)")
 prefer 2 apply (rule map_upds_nth) apply simp
 defer
apply (rule_tac t="(S'([nat (int (length S) - 1) - Suc m - n + 1..<nat (int (length S) - 1) - n + 1] [\<mapsto>]
      map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m]))
      (nat (int (length S) - 1) - Suc m - n + 1 + 0)" and 
      s="Some (map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] ! 0)" 
      in subst) apply (rule sym,assumption)
apply (thin_tac "?x=Some ?y")
apply (subgoal_tac 
      "map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] ! 0
       =(λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) (0+0)")
 prefer 2 apply (rule nth_map_upt, simp (no_asm))
apply (rule_tac s="the (S' (nat (int (length S) - 1) - Suc m + (0 + 0) + 1))" 
       and t="map (λi. the (S' (nat (int (length S) - 1) - Suc m + i + 1))) [0..<Suc m] ! 0" 
       in subst,rule sym,assumption)
apply (rule_tac s="nat ntop - m" and t="nat (int (length S) - 1) - Suc m + (0 + 0) + 1" in subst)
apply (simp (no_asm)) apply clarify
apply (erule additions4) 
apply (simp (no_asm),clarify)
apply (erule_tac n="Suc m + n" in equivS_nth_reg)
 apply (assumption,rule allI,rule impI,force,simp,assumption)
apply (simp (no_asm))
apply (erule additions5)
apply (rule additions6,simp)
done

axioms good_stack_SLIDE:
   "[| (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) = SLIDE m n   
    |] ==> length S ≥ m + n ∧ (∀ i < m+n . ∀ z . S!i ≠ Cont z)"
 
lemma execSVMInstr_SLIDE :
   "[| (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) = SLIDE m n;
       execSVMInst (SLIDE m n) (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 (SLIDE m n) @ 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') ∧
      cdm , ctm, com  \<turnstile>  S2  \<triangleq> (v',sh',dh',ih', fms')"

(* we incorporate some additional premises *)
apply (subgoal_tac "length S ≥ m + n ∧ (∀ i < m+n . ∀ z . S!i ≠ Cont z)")
 prefer 2 apply (rule good_stack_SLIDE,assumption+)
apply (elim conjE)

(* 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)

(* We unfold the equivalence relation definition *)
apply (unfold equivState_def)
apply (elim exE,elim conjE)

(* We instantiate the arrival JVM state*)
apply (rule_tac x="None" in exI)
apply (rule_tac x="sha((stackC, topf) \<mapsto> Intg (na - int(n)))" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty ma (slideArray S' na m n))" in exI)
apply (rule_tac x=ih in exI)
apply (rule_tac x="[([], vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, ref)]" in exI)
apply (rule conjI)
apply (unfold extractBytecode_def)
apply (clarify)

(* Now, we prove that the JVM sequence leads to the arrival state *)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,[([], vs, safeP, sigSafeMain, the (cdm (l,i)), ag,bd)]) 
   -jvm-> (None,sha,h,inih,[([Intg (int m)], vs, safeP, sigSafeMain, the (cdm (l,i)) + 1, ag,bd)])")
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 (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! 
                      the (cdm (l, i))) = LitPush (Intg (int m))",simp)

(* We prove that the executed instruction corresponds with the translation *)  
 apply (unfold trInstr.simps) 
 apply (erule nth_via_drop_append) 

(*  LitPush (Intg (int n)) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,[([Intg (int m)], 
                      vs, safeP, sigSafeMain, the (cdm (l,i))+1, ag,bd)]) 
   -jvm-> (None,sha,h,inih,[([Intg (int n), Intg (int m)], 
                      vs, safeP, sigSafeMain, (the (cdm (l,i)) + 1)+1, ag,bd)])")
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)))) = LitPush (Intg (int n))") apply (simp)
 apply (erule nth_via_drop_append) 

(* Invoke_static stackC slide [PrimT Integer,PrimT Integer]] *)
apply (drule drop_Suc_append)
apply (fold exec_all_def)
apply (rule slide_method)
 apply (simp,assumption,simp,simp)

apply (rule sym)
apply (rule_tac ys="[]" in nth_via_drop_append)
apply simp

(* Now we prove the equivalence relation *)

apply (frule nonJumping_Suc_pc)
apply (erule_tac sym [where t="SLIDE m n"])
apply (simp add: nonJumping.simps)
apply (simp add: trInstr.simps)

apply (rule_tac x="hm" 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="take m S @ drop (m + n) S" in exI)

apply (rule_tac x="sha((stackC, topf) \<mapsto> Intg (na - int n))" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty ma (slideArray S' na m n))" in exI)
apply (rule_tac x="ih" in exI)
apply (rule_tac x="vs" in exI)
apply (rule_tac x="the (cdm (l, i)) + 1 + 1 + 1" in exI)
apply (rule_tac x="ref" in exI)

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

apply (rule_tac x="la" in exI)
apply (rule_tac x="ty" in exI)
apply (rule_tac x="ma" in exI)
apply (rule_tac x="(slideArray S' na m n)" in exI)

apply (rule_tac x="(na - int 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" 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: heapC_def add: stackC_def)
apply (rule conjI) apply (rule activeCells,assumption)
apply (rule conjI) apply (rule activeCells_2,assumption+)
                   apply (rule activeCells_2,assumption+)
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 clarsimp
apply (rule conjI) apply (rule equivH_SLIDE, assumption+) 
apply (rule conjI) apply simp 
apply (rule conjI) apply (rule equivS_SLIDE)
  apply (simp,assumption,erule_tac x=ia in allE,drule mp,assumption,case_tac z,force)
apply (rule conjI) apply simp
                   apply (simp add: heapC_def add: stackC_def)
by simp

end