Theory dem_translation

(* 
   Title: Lemmas on the static properties of the translation SVM to JVM
   Author: Ricardo Pe~na and Javier de Dios
   Copyright: January 2009, Universidad Complutense de Madrid
*)

header {* Lemmas on the static properties of the translation SVM to JVM *}

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

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

lemma fun_trInstr1_aux [rule_format]:
   "(∀ pc i cdm pc' i' cdm' insts . 
   (∀ j ≥ i . (p,j) ∉ dom cdm) -->
   ((pc',i',cdm'),insts) = mapAccumL (trInstrAux p ctm com pcc) (pc,i,cdm) svms
   --> cdm ⊆m cdm'∧ (∀ j ≥ i'. (p,j) ∉ dom cdm'))"

(* we make induction on the list of instructions *)
apply (induct svms)
(* empty list *)
apply simp
(* non-empty list *)
apply (rule allI)+
apply (rename_tac inst svms pc1 i1 cdm1 pc2 i2 cdm2 insts2)
apply (unfold mapAccumL.simps)
apply (case_tac "trInstrAux p ctm com pcc (pc1, i1, cdm1) inst")
apply (rename_tac state bc)
apply (case_tac state, rename_tac pc3 rest)
apply (case_tac rest, rename_tac i3 cdm3, simp) 
apply (case_tac "mapAccumL (trInstrAux p ctm com pcc) (pc3, i3, cdm3) svms")
apply (rename_tac state4 insts4)
apply (case_tac state4,rename_tac pc4 rest4)
apply (case_tac rest4, rename_tac i4 cdm4,clarsimp)
apply (subgoal_tac "((pc4, i4, cdm4), insts4)
      = mapAccumL (trInstrAux p ctm com pcc) (pc3, i3, cdm3) svms")
 prefer 2 apply simp

(* we instantiate the universal vars of the induction hypothesis *)
apply (erule_tac x="pc3" in allE)
apply (rotate_tac -1)
apply (erule_tac x="i3" in allE)
apply (rotate_tac -1)
apply (erule_tac x="cdm3" in allE)

(* we  eliminate the implication in the premises *)
apply (erule impE)
prefer 2
 apply (rotate_tac -1)
 apply (erule_tac x="pc4" in allE)
 apply (rotate_tac -1)
 apply (erule_tac x="i4" in allE)
 apply (rotate_tac -1)
 apply (erule_tac x="cdm4" in allE)
 apply (erule impE)
 apply (rule_tac x=insts4 in exI,assumption)

(* we unfold the definition of trInstrAux *)
 apply (elim conjE)
 apply (rule conjI)
 apply (unfold trInstrAux_def)  apply (simp)
 apply (elim conjE)
 apply (subgoal_tac "cdm1 ⊆m cdm1((p, i1) \<mapsto> pc1)")
 apply (erule map_le_trans,simp)

(* we prove that (p,i1) was not in the domain of cdm1 *)
apply (erule_tac x=i1 in allE)
apply (erule impE,simp)
apply (unfold map_le_def) apply(force)
apply assumption
apply simp
apply (elim conjE) 
apply clarify
apply (erule_tac x=j in allE)
apply (drule mp)
by auto

lemma fun_trInstr1 [rule_format]:
   "(∀ pc i cdm pc' i' cdm' insts . 
   (∀ j ≥ i . (p,j) ∉ dom cdm) -->
   ((pc',i',cdm'),insts) = mapAccumL (trInstrAux p ctm com pcc) (pc,i,cdm) svms
   --> cdm ⊆m cdm')"
apply (rule allI)+
apply (rule impI)+
thm fun_trInstr1_aux
apply (subgoal_tac "cdm ⊆m cdm'∧ (∀ j ≥ i'. (p,j) ∉ dom cdm')")
 prefer 2 apply (rule fun_trInstr1_aux)
 apply (erule_tac x=j in allE) apply (drule mp)
by auto

lemma fun_trInstrAux:
   "((pc',cdm'),bc') = trSeq ctm com pcc (pc,cdm) (p,svms,fn) -->
   svms = is # iss -->
   (∀ j≥0 . (p,j) ∉ dom cdm) -->
   drop pc bc = bc' @ rest -->
   (∀ i . i < length svms -->
      (∃ pc'' cdm'' bc'' rest' insts1.
      ((pc''+length bc'',i+1,cdm''((p,i)\<mapsto> pc'')),bc'') = 
          trInstrAux p ctm com pcc (pc'',i,cdm'') (svms!i)
      ∧ drop (pc''-pc) bc' = bc'' @ rest'
      ∧ ((pc'',i,cdm''),insts1)= 
          mapAccumL (trInstrAux p ctm com pcc) (pc,0,cdm) (take i svms)
      ∧ cdm''((p,i)\<mapsto> pc'') ⊆m cdm'))"

apply (rule impI)+
apply (rule allI)

(* we make induction on the position i of the svm instruction *)
apply (induct_tac i)

(* i= 0 *)
apply (rule impI)
apply (unfold trSeq_def)
apply clarify
apply (case_tac "(pc,cdm)")
apply (case_tac "(p, is # iss, fn)")
apply (rename_tac pc2 cdm2 p2 rest2)
apply (case_tac "rest2")
apply (rename_tac instr ff)
apply (simp del: mapAccumL.simps) 
apply (case_tac "mapAccumL (trInstrAux p2 ctm com pcc) (pc2, 0, cdm2) instr")
apply (rename_tac result instss2)
apply (case_tac result)
apply (rename_tac pc3 rest2)
apply (case_tac rest2)
apply (simp del: mapAccumL.simps)
apply clarify

(* we apply the lemma mapAccumL_non_empty *)
apply (rename_tac nn bca)
apply (subgoal_tac "(∃ s' y ys'.
      (s',y) = trInstrAux p ctm com pcc (pc, 0, cdm) is
      ∧ ((pc',nn,cdm'),ys')=mapAccumL (trInstrAux p ctm com pcc) s' iss
      ∧ instss2 = y # ys')")
 prefer 2
 apply (subgoal_tac "((pc', nn, cdm'), instss2)=
       mapAccumL (trInstrAux p ctm com pcc) (pc, 0, cdm) (is # iss)")
  prefer 2 apply simp
 apply (erule mapAccumL_non_empty2,simp)
apply (elim exE,elim conjE)
apply clarify
apply (rename_tac pc4 nn4 cdm4 bc0 ys')

(* we instantiate the existential vars: pc and cdm are the inital ones *)
apply (rule_tac x=pc in exI)
apply (rule_tac x=cdm in exI)
apply (rule_tac x=bc0 in exI)

apply (subgoal_tac "(pc4, nn4, cdm4)=
 (pc + length bc0, Suc 0, λ a. if a = (p, 0) then Some pc else cdm a)")
apply (rule conjI)
apply simp
 apply (rule conjI)
  apply (rule_tac x="concat ys'" in exI)
  apply force
 apply (rule conjI)
 apply (rule_tac x="[]" in exI,simp) 
 apply (simp del: mapAccumL.simps add: trInstrAux_def)
 apply (fold fun_upd_apply)
 apply (elim conjE)
 apply clarify
 thm fun_trInstr1
 apply (rule_tac i="Suc 0" and p="p" in fun_trInstr1)
 apply (erule_tac x=j in allE)
 apply force
apply simp
apply (simp del: mapAccumL.simps add: trInstrAux_def)
apply (fold fun_upd_apply)
apply force

(* inductive step i > 0 *)
apply clarify
apply (case_tac "(pc,cdm)")
apply (case_tac "(p, is # iss, fn)")
apply (rename_tac pc2 cdm2 p2 rest2)
apply (case_tac "rest2")
apply (rename_tac instr ff)
apply (simp del: mapAccumL.simps) 
apply (case_tac "mapAccumL (trInstrAux p2 ctm com pcc) (pc2, 0, cdm2) instr")
apply (rename_tac result instss)
apply (case_tac result)
apply (rename_tac pc3 rest3)
apply (case_tac rest3)
apply (rename_tac n3 cdm3)
apply (simp del: mapAccumL.simps)
apply clarify

(* we split the input list into the n first ones and the rest *)
apply (subgoal_tac "(take n (is#iss)) @ (drop n (is#iss))=is#iss")
 prefer 2
 apply (rule append_take_drop_id)
apply (subgoal_tac "∃ s1 insts1 insts2 . (s1,insts1) = 
       mapAccumL (trInstrAux p ctm com pcc) (pc, 0, cdm) (take n (is # iss))
  ∧ ((pc', n3, cdm'), insts2)= 
       mapAccumL (trInstrAux p ctm com pcc) s1 (drop n (is # iss))
  ∧ instss= insts1 @ insts2")
 prefer 2
 apply (rule mapAccumL_split [where xs="is # iss"]) apply(simp,simp)
apply (elim exE, elim conjE)
apply (case_tac s1)
apply (rename_tac pc1 rest1)
apply (case_tac rest1)
apply (rename_tac nn1 cdm1)
apply clarify
apply (subgoal_tac " ((pc'', n, cdm''), insts1)=((pc1, nn1, cdm1), insts1a)")
prefer 2
 apply simp
apply clarify
apply (thin_tac "?x=mapAccumL ?f (pc,0,cdm) ?xs")

(* we execute one mapAccumL step *)
(* non empty list after dropping nn1 instructions *)
apply (subgoal_tac "nn1 < length (is#iss)")
apply (subgoal_tac "(∃ is2 iss2 . drop nn1 (is # iss) = is2#iss2
                    ∧ (is # iss) ! nn1 = is2)")
 prefer 2
 apply (erule drop_nth)
 prefer 2
 apply simp
apply (elim exE)
apply clarify

(* now, instruction nn1 is the first one of the remaining list *) 
apply (subgoal_tac "(∃ s' y ys'.
      (s',y) = trInstrAux p ctm com pcc (pc1, nn1, cdm1) ((is # iss) ! nn1)
      ∧ ((pc', n3, cdm'),ys') = mapAccumL (trInstrAux p ctm com pcc) s' iss2
      ∧ insts2 = y # ys')")
 prefer 2
 apply (erule mapAccumL_non_empty2,simp) 
apply (elim exE)
apply (elim conjE)
apply (simp del: mapAccumL.simps drop_append)
apply (rename_tac s' bc2 ys')
apply (case_tac s')
apply (rename_tac pc2 rest2)
apply (case_tac rest2, rename_tac nn2 cdm2,clarify)
apply (subgoal_tac "((pc1 + length bc'', Suc nn1,  
      % a. if a = (p, nn1) then Some pc1 else cdm1 a), bc'')
      =((pc2, nn2, cdm2), bc2)")
 prefer 2
 apply simp
apply (clarify, thin_tac "?x=trInstrAux p ctm com pcc ?y ?z")

(* we execute two steps of mapAccumL *)
apply (subgoal_tac "∃ iss3. iss2=(iss ! nn1)#iss3")
apply (elim exE,clarify)
apply (subgoal_tac "(∃  s1 s2 y1 y2 ys3 . 
   (s1,y1)=trInstrAux p ctm com pcc (pc1, nn1, cdm1) ((is # iss) ! nn1)
   ∧ (s2,y2)=trInstrAux p ctm com pcc s1 (iss!nn1)
   ∧ ((pc', n3, cdm'), ys3)=mapAccumL (trInstrAux p ctm com pcc) s2 iss3
   ∧ bc2#ys'=y1#y2#ys3)")
 prefer 2
 apply (erule mapAccumL_two_elements)
 apply simp
apply (elim exE)
apply (case_tac s1, rename_tac pc3 rest3,clarify)
apply (rename_tac nn3 cdm3) 
apply (subgoal_tac "((pc3, nn3, cdm3), y1)=
      ((pc1 + length y1, Suc nn1, 
      % a. if a = (p, nn1) then Some pc1 else cdm1 a), y1)")
 prefer 2
 apply simp
apply (clarify,thin_tac "?x=trInstrAux p ctm com pcc ?y ?z")
apply (rename_tac pc4 nn4 cdm4 y1 y2 ys3 pc3 nn3 cdm3)

 prefer 2
 apply (rule_tac x="tl iss2" in exI)
  apply (subgoal_tac "drop (Suc nn1) (is#iss) = iss2") 
  prefer 2
  apply (subgoal_tac "drop (Suc nn1) (is # iss)=drop nn1 (tl (is#iss))")
  prefer 2
  apply (rule drop_Suc)
 apply (subgoal_tac "is # iss=take nn1 (is # iss) @ (is # iss) ! nn1 # iss2")
  prefer 2
  apply simp
 apply (erule drop_take_Suc)
 apply (rule drop_nth2,assumption,simp)

(* finally we instantiate the existential vars *)
apply (rule_tac x="pc1 + length y1" in exI)
apply (rule_tac x=" % a. if a = (p, nn1) then Some pc1 else cdm1 a" in exI)
apply (rule_tac x="y2" in exI)
apply (rule conjI)

(* first conclusion *)
apply (thin_tac "mapAccumL ?x ?y ?z = ?w")
apply (thin_tac "?w=mapAccumL ?x ?y ?z")
apply (thin_tac "?w=mapAccumL ?x ?y ?z")
apply (thin_tac "?x=trInstrAux ?x1 ?x2 ?x3 ?x4 ?x5 ?x6")
apply (simp add: trInstrAux_def)
apply clarify
apply (fold fun_upd_apply)
apply force

(* second conclusion *)
apply (rule conjI)
apply (rule_tac x="concat ys3" in exI)
apply (simp only: concat.simps)
apply (rule drop_append2,simp,simp)
 
(* third conclusion *)
apply (rule conjI)
apply (rule_tac x="insts1a @ [y1]" in exI)
apply (subgoal_tac "is # take nn1 iss=(take nn1 (is # iss)) @ [(is # iss) ! nn1]")
apply (erule_tac t="is # take nn1 iss" in ssubst)
 prefer 2
 apply (erule take_append2)
apply (rule mapAccumL_one_more,simp,assumption)

(* fourth conclusion *)
apply (thin_tac "drop ?n ?x = ?y")
apply (thin_tac "drop ?n ?x = ?y")
apply (thin_tac "drop ?n ?x = ?y")
apply (thin_tac "(take ?n ?x)@?z = ?y")
apply (thin_tac "?x < ?y")
apply (subgoal_tac "cdm4 = cdm1((p, nn1) \<mapsto> pc1, 
                                (p, Suc nn1) \<mapsto>  pc1 + length y1)")
 prefer 2 apply (unfold trInstrAux_def)
 apply force
apply (simp del:mapAccumL.simps trInstr.simps)
apply (fold fun_upd_apply)
apply (elim conjE)
apply (thin_tac "mapAccumL ?f ?s ?x = ?y")

apply (subgoal_tac "cdm1 ((p, nn1) \<mapsto> pc1, (p, Suc nn1) \<mapsto> pc1 + length 
     (trInstr pc1 (cdm1((p, nn1) \<mapsto> pc1)) ctm com pcc ((is # iss) ! nn1))) 
    ⊆m cdm' ∧ (∀ j≥ n3.(p,j)∉ dom cdm')")
 prefer 2
 apply (rule fun_trInstr1_aux)
  prefer 2 apply simp
 prefer 2 apply (elim conjE,assumption)

apply (subgoal_tac "cdm ⊆m cdm1 ∧ (∀ j≥ nn1.(p,j)∉ dom cdm1)")
 prefer 2
 apply (rule fun_trInstr1_aux)
  prefer 2 apply simp
 apply (erule_tac x=ja in allE,assumption)
apply (thin_tac "?y = mapAccumL ?f ?s ?x")
apply (thin_tac "?y = mapAccumL ?f ?s ?x")
apply (thin_tac "?y = mapAccumL ?f ?s ?x")
apply (thin_tac "?mapAccumL ?f ?s ?x = ?y")
apply (elim conjE)
apply clarify
apply (unfold fun_upd_apply)
apply (rotate_tac 1)
apply (erule_tac x=j in allE)
apply (drule mp,simp)
apply force
done

lemma fun_trInstr :
   "[| ((pc',cdm'),bc') = trSeq ctm com pcc (pc,cdm) (p,svms,fn);
      svms = is1 # iss;
      (∀ j≥0 . (p,j) ∉ dom cdm);
      drop pc bc = bc' @ rest;
      svm = svms ! i;
      i < length svms
      |] ==> (∃ pc'' cdm'' bc'' rest .
            bc'' = trInstr pc'' cdm'' ctm com pcc svm 
            ∧ drop pc'' bc = bc'' @ rest
            ∧ cdm'' (p,i) = Some pc''
            ∧ cdm'' ⊆m cdm')"

(* this is a more or less direct consequence of lemma fun_trInstrAux *)
apply (insert fun_trInstrAux [of pc' cdm' bc' ctm com pcc pc cdm 
                                 p svms fn is1 iss bc rest])
apply (drule mp,assumption)+
apply (rotate_tac -1)
apply (erule_tac x=i in allE)
apply (drule mp,assumption)
apply (elim exE, elim conjE)

(* the pc, an bc are the same than those of trInstrAux, but 
   rest is the appending of the two rests and
   the cdm is the one returned by trInstrAux *)
apply (rule_tac x="pc''" in exI)
apply (rule_tac x="cdm''((p, i) \<mapsto> pc'')" in exI)
apply (rule_tac x="bc''" in exI)
apply (rule_tac x="rest' @ rest" in exI)

(* first conclusion *)
apply (rule conjI)
apply (unfold trInstrAux_def)
apply simp

(* second and third conclusions *)
apply (rule conjI)
apply clarsimp
apply (erule drop_append3,assumption)
apply (rule conjI,simp) 

(* fourth conclusion *)
by assumption

axioms fun_trSeq1:
  "(∃ pc2 cdm2 bc2 . ((pc2,cdm2),bc2)  = trSeq ctm com pcc (pc1,cdm1) svm
   ∧ pc2-pc1=length bc2)"

axioms fun_trSeq2:
  "((pc2,cdm2),bc2)  = trSeq ctm com pcc (pc1,cdm1) seq
   ==> cdm1 ⊆m cdm2"

lemma fun_trSeq3 [rule_format]:
  "(∀ pc1 cdm1 pc2 cdm2 bcs . 
   ((pc2,cdm2),bcs) = mapAccumL (trSeq ctm com pcc) (pc1,cdm1) svms -->
   cdm1 ⊆m cdm2)"
(* we make induction on the list of sequences *)
apply (induct svms)
(* empty list *)
apply simp
(* non-empty list *)
apply (rule allI)+
apply (rename_tac seq svms pc1 cdm1 pc2 cdm2 bcs)
apply (unfold mapAccumL.simps)
apply (case_tac "trSeq ctm com pcc (pc1, cdm1) seq")
apply (rename_tac state bc)
apply (case_tac state, rename_tac pc3 cdm3,simp) 
apply (case_tac "mapAccumL (trSeq ctm com pcc) (pc3, cdm3) svms",rename_tac state4 bcs4)
apply (case_tac state4,rename_tac pc4 cdm4,clarsimp)
apply (subgoal_tac "((pc4, cdm4), bcs4)
      = mapAccumL (trSeq ctm com pcc) (pc3, cdm3) svms")
 prefer 2 apply simp
apply (erule_tac x="pc3" in allE)
apply (erule_tac x="cdm3" in allE)
apply (erule_tac x="pc4" in allE)
apply (erule_tac x="cdm4" in allE)
apply (erule impE)
apply (rule_tac x=bcs4 in exI,assumption)
apply (subgoal_tac "cdm1 ⊆m cdm3")
 prefer 2 apply (rule fun_trSeq2,rule sym,simp)
by (erule map_le_trans,assumption)

lemma fun_trSeq_aux :
 "((pc,cdm),bcs) = mapAccumL (trSeq ctm com pcc) (pcini,cdini) svms -->
  drop pcini bc = concat bcs -->
  (∀ i . i < length svms -->
  (∃ pc1 cdm1 pc2 cdm2 bcs1 bcs2 bc2 .
  ((pc1,cdm1),bcs1) = mapAccumL (trSeq ctm com pcc) (pcini,cdini) (take i svms)
  ∧ ((pc2,cdm2),bc2)  = trSeq ctm com pcc (pc1,cdm1) (svms ! i)
  ∧ ((pc,cdm),bcs2)   = mapAccumL (trSeq ctm com pcc) (pc1,cdm1) (drop i svms)
  ∧ bcs = bcs1 @ bcs2
  ∧ (pc1-pcini) = length (concat bcs1)
  ∧ cdm2 ⊆m cdm))"

apply (rule impI)+
apply (rule allI)

(* we make induction on the position i of the sequence *)
apply (induct_tac i)

(* i= 0 *)
apply (rule impI)
apply (rule_tac x="pcini" in exI)
apply (rule_tac x="cdini" in exI)
apply (subgoal_tac "(∃ pc2 cdm2 bc2 . 
      ((pc2,cdm2),bc2)  = trSeq ctm com pcc (pcini,cdini) (svms ! 0)
      ∧ pc2-pcini=length bc2)")
 prefer 2
 apply (rule fun_trSeq1)
apply (elim exE, elim conjE)
apply (rule_tac x="pc2" in exI)
apply (rule_tac x="cdm2" in exI)
apply (rule_tac x="[]" in exI)
apply (rule_tac x="bcs" in exI)
apply (rule_tac x="bc2" in exI)
apply (rule conjI,simp)
apply (rule conjI,assumption)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (subgoal_tac "∃ s' y ys'.
      (s',y) = trSeq ctm com pcc (pcini, cdini) (svms!0)
      ∧ ((pc, cdm),ys') = mapAccumL (trSeq ctm com pcc) s' (tl svms)")
 prefer 2 apply (erule mapAccumL_non_empty3,assumption)
apply (elim exE,elim conjE)
apply clarify apply (rename_tac pc2' cdm2' bc2' bcs')
apply (subgoal_tac "((pc2', cdm2'), bc2')=((pc2, cdm2), bc2)")
 prefer 2 apply simp
apply clarify
apply (erule fun_trSeq3)
 
(* i > 0*)
apply (rule impI, drule mp, simp)
apply (elim exE,elim conjE)

(* we unfold the second occurrence of mapAccumL *)
apply (subgoal_tac "drop n svms = (svms ! n) # drop (Suc n) svms")
apply clarify
 prefer 2 apply (rule drop_nth3, simp)
apply (subgoal_tac "∃ s' y ys'.
      (s',y) = trSeq ctm com pcc (pc1, cdm1) (svms ! n)
      ∧ ((pc, cdm),ys') = mapAccumL (trSeq ctm com pcc) s' (drop (Suc n) svms)
      ∧ bcs2 = y # ys'")
 prefer 2
 apply (rule mapAccumL_non_empty2 [where f="trSeq ctm com pcc"]) 
 apply (blast,simp)
apply (elim exE,elim conjE)
apply (case_tac s')
apply clarify
apply (rename_tac bc2' bcs3 pc2' cdm2')
apply (subgoal_tac "((pc2', cdm2'), bc2')=((pc2, cdm2), bc2)")
 prefer 2 apply simp
apply clarify
apply (thin_tac "?x=trSeq ?x1 ?x2 ?x3 ?x4 ?x5")

(* we instantiate the initial pc and cdm of svms ! Suc n *) 
apply (rule_tac x="pc2" in exI)
apply (rule_tac x="cdm2" in exI)
apply (subgoal_tac "∃ pc2a cdm2a bc2a .
      ((pc2a, cdm2a), bc2a) = trSeq ctm com pcc (pc2, cdm2) (svms ! Suc n)
      ∧ pc2a - pc2 = length bc2a")
 prefer 2 apply (rule fun_trSeq1)
apply (elim exE,elim conjE)

(* we instantiate the rest of existential vars *)
apply (rule_tac x="pc2a" in exI)
apply (rule_tac x="cdm2a" in exI)
apply (rule_tac x="bcs1 @ [bc2]" in exI)
apply (rule_tac x="bcs3" in exI)
apply (rule_tac x="bc2a" in exI)

(* first conclusion *)
apply (rule conjI)
apply (subgoal_tac "take (Suc n) svms=(take n svms)@[svms ! n]")
 prefer 2 
 apply (rule take_append3,simp)
apply (erule_tac t="take (Suc n) svms" in ssubst)
apply (erule mapAccumL_one_more,assumption)

(* second conclusion *)
apply (rule conjI,assumption)

(* third conclusion *)
apply (rule conjI,assumption)

(* fourth conclusion *)
apply (rule conjI, simp)

(* fifth conclusion *)
apply (subgoal_tac "∃ pc2b cdm2b bc2b .
      ((pc2b, cdm2b), bc2b) = trSeq ctm com pcc (pc1, cdm1) (svms ! n)
      ∧ pc2b - pc1 = length bc2b")
 prefer 2
 apply (rule fun_trSeq1)
 apply (elim exE,elim conjE)
apply (subgoal_tac "((pc2, cdm2), bc2)=((pc2b, cdm2b), bc2b)")
 prefer 2 apply simp
apply clarify
apply simp
apply (subgoal_tac "(pc1 - pcini)+(pc2b - pc1)=
      (length (concat bcs1))+(length bc2b)")
 prefer 2 
 apply (erule sum_nat,assumption)
apply (rule conjI)
apply (rule sym)
apply (subgoal_tac "length (concat bcs1) + length bc2b
      = pc1 - pcini + (pc2b - pc1)")
 prefer 2 apply simp
apply (erule_tac t="length (concat bcs1) + length bc2b" in ssubst)
apply (rule sum_substract)
apply (rename_tac cdm3 bc3 pc2 cdm2 bc2)

(* sixth conclusion *)
apply (subgoal_tac "∃ s' y ys'.
      (s',y) = trSeq ctm com pcc (pc2, cdm2) ((drop (Suc n) svms)!0)
      ∧ ((pc, cdm),ys') = 
        mapAccumL (trSeq ctm com pcc) s' (tl (drop (Suc n) svms))")
 prefer 2 apply (erule mapAccumL_non_empty3)
 apply force
apply (elim exE,elim conjE)
apply clarify apply (rename_tac pc2' cdm3' bc3' bcs')
apply (subgoal_tac "((pc2', cdm3'), bc3')=((pc2a, cdm3), bc3)")
 prefer 2 apply simp
apply clarify
apply (erule fun_trSeq3)
done

lemma fun_trSeq :
  "[| ((pc,cdm),bcs) = mapAccumL (trSeq ctm com pcc) (pcini,cdini) svms;
    drop pcini bc = concat bcs;
    l < length svms;
    seq = svms ! l 
   |] ==> (∃ pc' cdm' pc'' cdm'' bc' rest .
          ((pc'',cdm''),bc') = trSeq ctm com pcc (pc',cdm') seq
          ∧ drop pc' bc = bc' @ rest
          ∧ cdm'' ⊆m cdm)"
 
(* this is a consequence of lemma fun_trSeq_aux *)
apply (insert fun_trSeq_aux [of pc cdm bcs ctm com pcc pcini cdini svms bc])
apply (drule mp,assumption)+
apply (erule_tac x=l in allE)
apply (drule mp,assumption)
apply (elim exE, elim conjE)

(* we instantiate the existential vars *)
apply (rule_tac x="pc1" in exI)
apply (rule_tac x="cdm1" in exI)
apply (rule_tac x="pc2" in exI)
apply (rule_tac x="cdm2" in exI)
apply (rule_tac x="bc2" in exI)
apply (rule_tac x="drop (pc2-pc1) (concat bcs2)" in exI)

(* first conclusion *)
apply (rule conjI, simp)

(* second and third conclusions *)
apply (rule conjI)
apply (thin_tac "?x=mapAccumL ?y ?z ?u")
apply (thin_tac "?x=mapAccumL ?y ?z ?u")
apply (subgoal_tac "drop l svms=(svms!l) # drop (Suc l) svms")
 prefer 2
 apply (erule drop_nth3, clarify)
apply (case_tac "trSeq ctm com pcc (pc1, cdm1) (svms ! l)", clarsimp)
apply (rename_tac pc2 cdm2 bc2)
apply (case_tac "mapAccumL (trSeq ctm com pcc) (pc2,cdm2) (drop (Suc l) svms)",clarsimp)
apply (rename_tac bcs3)
apply (subgoal_tac "∃ pc2' cdm2' bc2' .
      ((pc2',cdm2'),bc2') = trSeq ctm com pcc (pc1, cdm1) (svms ! l)
      ∧ pc2'-pc1 = length bc2'")
 prefer 2 apply (rule fun_trSeq1, clarify)
apply (subgoal_tac "((pc2', cdm2'), bc2')=((pc2, cdm2), bc2)")
 prefer 2 apply simp
apply clarify
apply auto
apply (subgoal_tac "drop pc1 bc = [] @ [] @ (bc2 @ concat bcs3)")
 prefer 2 apply (rule drop_append3)
apply (simp,simp,simp add: drop_append)
done

lemma fun_trCodeStore:
   "(P',cdm,ctm,com) = trSVM2JVM ((svms, ctmap), ini, ct, st) -->
    bc = extractBytecode P' -->
      (∃ cdm' ctm' pcc pcini cdini pc bcs .
      ((pc,cdm),bcs) = mapAccumL (trSeq ctm' com pcc) (pcini,cdini) svms
      ∧ drop pcini bc = concat bcs)"

(* First we unfold some definitions and tuples *)
apply (rule impI)+
apply (unfold trSVM2JVM_def)
apply clarsimp
apply (case_tac "trCodeStore ini (length (initConsTable ct) + 
      length (initSizeTable st)) ctmap (trConsTable ct) svms")
apply (rename_tac instrs1 rest)
apply (case_tac rest)
apply (rename_tac cdm1 ctm1)
apply clarsimp
apply (subgoal_tac "extractBytecode
      ((safeP, objectC, [], [(sigSafeMain, PrimT Void, 10, 10, 
      initConsTable ct @ initSizeTable st @ instrs1, [])]) # Prog_RTS) = 
      initConsTable ct @ initSizeTable st @ instrs1")
apply simp
apply (thin_tac "extractBytecode ?x=?y")
 prefer 2 
 apply (unfold extractBytecode_def)
 apply (unfold method'_def)
 apply simp
 apply (subgoal_tac "class ((safeP,objectC,[],[(sigSafeMain,PrimT Void, 
       10,10,initConsTable ct@initSizeTable st@instrs1,[])]) # Prog_RTS) 
       safeP = Some (objectC, [], [(sigSafeMain, PrimT Void, 10, 10, 
       initConsTable ct @ initSizeTable st @ instrs1, [])])")
 apply simp 
 apply (unfold Prog_RTS_def)
 apply (simp add:class_def)

(* we unfold the definition of trCodeStore *)
apply (unfold trCodeStore_def)
apply (case_tac "unzip3 ctmap",rename_tac fs1 rest,
      case_tac rest,rename_tac ps1 contss1)
apply clarify apply (simp del: mapAccumL.simps trConsTable_def zip.simps upt_Suc)
apply (case_tac "mapAccumL (trSeq (map_of (zip (concat contss1) 
 [Suc 0..<Suc (length (concat contss1))])) (trConsTable ct)
 (Suc (length (initConsTable ct) + length (initSizeTable st) + length fs1)))
 (Suc (Suc (length (initConsTable ct) + length (initSizeTable st) 
 + length fs1)), map_of (zip (zip ps1 (replicate (length fs1) 0))
  [Suc (length (initConsTable ct) + length (initSizeTable st))..<
  Suc (length (initConsTable ct) + length (initSizeTable st) + 
  length fs1)])) svms")
apply (rename_tac rest iss1,case_tac rest, rename_tac pc1 cdm1) 
apply (clarify) apply (simp del: mapAccumL.simps trConsTable_def zip.simps upt_Suc)
apply (elim conjE,clarify)

(* we instantiate the existential vars *)
apply (rule_tac x="map_of (zip (concat contss1) 
      [Suc 0..<Suc (length (concat contss1))])" in exI)
apply (rule_tac x="Suc (length (initConsTable ct) + length (initSizeTable st)
      + length fs1)" in exI)
apply (rule_tac x="Suc (Suc (length (initConsTable ct) 
      + length (initSizeTable st) + length fs1))" in exI)
apply (rule_tac x=" map_of (zip (zip ps1 (replicate (length fs1) 0))
      [Suc (length (initConsTable ct) + length (initSizeTable st))..<
       Suc (length (initConsTable ct) + length (initSizeTable st) 
       + length fs1)])" in exI)
apply (rule_tac x="pc1" in exI)
apply (rule_tac x="iss1" in exI)

(* first conclusion *)
apply (rule conjI)
apply simp

(* second conclusion *)
apply (subgoal_tac "length fs1 =length ps1")
 prefer 2 apply (rule unzip3_length,simp)
apply (subgoal_tac "length (map Goto
      (zipWith (% p n. int (the (cdm (p, 0))) - int n) ps1
      [Suc (length (initConsTable ct) + length (initSizeTable st))..<
      Suc (length (initConsTable ct) + length (initSizeTable st) + length fs1)]))
      = length fs1")
 prefer 2
 apply (subgoal_tac  "length [Suc (length (initConsTable ct) + 
       length (initSizeTable st))..<
       Suc (length (initConsTable ct) + length (initSizeTable st)) 
       + length fs1] = 
       (Suc (length (initConsTable ct) + length (initSizeTable st))
       + length fs1) -
       (Suc (length (initConsTable ct) + length (initSizeTable st)))")
  prefer 2 apply(rule upt_length,simp)
 apply (subgoal_tac "length (zipWith ( % p n. int (the (cdm (p, 0))) 
       - int n) ps1
       [Suc (length (initConsTable ct) + length (initSizeTable st))..<
        Suc (length (initConsTable ct) + length (initSizeTable st) 
        + length fs1)]) =
        min (length ps1) (length [Suc (length (initConsTable ct) + 
        length (initSizeTable st))..<
        Suc (length (initConsTable ct) + length (initSizeTable st) 
        + length fs1)])")
  prefer 2 apply (rule zipWith_length)
  apply simp
apply (simp add: drop_append)
done


axioms fun_SVM2JVM_aux:
 "[| l < length svms; svms ! l = (p, seq, fn);
   ((pc, cdm), bcs) = mapAccumL (trSeq ctm' com pcc) (pcini, cdini) svms;
   ((pc2, cdm2), bcSeq) = trSeq ctm' com pcc (pcSeq, cdmSeq) (svms ! l)
  |] ==>  (∀ j≥0. (p, j) ∉ dom cdmSeq)"
 


lemma fun_SVM2JVM [rule_format]:
     "(P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, st) -->
     l < length svms -->
     svms ! l = (p,seq,fn) -->
     i < length seq -->
     svm = fst (the (map_of svms p)) ! i -->
     pc = the (cdm (p,i)) -->
     bytecode = extractBytecode P' -->
     (∃ cdm' ctm' pcc inss bytecode' .
                inss = trInstr pc cdm' ctm' com pcc svm ∧
                drop pc bytecode = inss @ bytecode' ∧
                cdm' ⊆m cdm)"

apply (rule impI)+

(* we apply lemma on the translation of the whole code store *)
apply (insert fun_trCodeStore [of P' cdm ctm com svms ctmap ini ct st bytecode])
apply (drule mp, assumption)+
apply (erule exE)+
apply(elim conjE)

(* we apply lemma on the translation of a single sequence *)
apply (subgoal_tac "(∃ pc' cdm' pc'' cdm'' bc' rest .
          ((pc'',cdm''),bc') = trSeq ctm' com pcc (pc',cdm') (svms ! l)
          ∧ drop pc' bytecode = bc' @ rest
          ∧ cdm'' ⊆m cdm)")
 prefer 2 apply (rule fun_trSeq) apply(simp,assumption,simp,simp)
apply (elim exE, elim conjE)
apply clarify
apply (rename_tac pcSeq cdmSeq pc2 cdm2 bcSeq restSeq)

(* we apply the lemma on the translation of a single SVM instruction *)
apply (subgoal_tac "∃ is iss . seq = is#iss")
 prefer 2 apply (rule list_non_empty,force)
 apply (elim exE)
apply (subgoal_tac "seq=fst (the (map_of svms p))")
 prefer 2 apply (subgoal_tac "map_of svms p= Some (seq,fn)")
  prefer 2 apply (rule map_of_distinct)
  apply (rule svms_good,simp,simp)
 apply simp
apply (insert svms_good [of svms])
apply (subgoal_tac " (∃ pc'' cdm'' bc'' rest .
      bc'' = trInstr pc'' cdm'' ctm' com pcc (seq ! i)
      ∧ drop pc'' (extractBytecode P') = bc'' @ rest
      ∧ cdm'' (p,i) = Some pc''
      ∧ cdm'' ⊆m cdm2)")
 prefer 2 apply (rule fun_trInstr)
 apply (simp) 
 apply (rule sym)
 apply force
 apply (erule fun_SVM2JVM_aux [of l svms p seq fn],assumption,simp,simp)
 apply simp
 apply simp
 apply simp
apply (elim exE, elim conjE)

(* we instantiate the existential vars *)
apply (rule_tac x="cdm''" in exI)
apply (rule_tac x="ctm'" in exI)
apply (rule_tac x="pcc" in exI)
apply (rule_tac x="bc''" in exI)
apply (rule_tac x="rest" in exI)
apply (subgoal_tac "cdm'' ⊆m cdm")
 prefer 2 apply (erule map_le_trans,assumption)
apply (subgoal_tac "the (cdm (p,i))=pc''")
 prefer 2 apply (unfold map_le_def)
 apply force
apply clarify
apply simp
done

consts
  nonJumping :: "SafeInstr => bool"
primrec
  "nonJumping  DECREGION        = True"
  "nonJumping (SLIDE m n)       = True"
  "nonJumping (PRIMOP oper)     = True"
  "nonJumping  REUSE            = True"
  "nonJumping  COPY             = True"
  "nonJumping (PUSHCONT p)      = True"
  "nonJumping (BUILDENV its)    = True"
  "nonJumping (BUILDCLS c is i) = True"
  "nonJumping (CALL p)          = False"
  "nonJumping  POPCONT          = False"
  "nonJumping (MATCHN l v m ps) = False"
  "nonJumping (MATCH l ps)      = False"
  "nonJumping (MATCHD l ps)     = False"

axioms nonJumping_Suc_pc :
  "[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, st);
   svm = fst (the (map_of svms l)) ! i;
   nonJumping svm;
   iss = trInstr (the (cdm (l, i))) cdm' ctm' com pcc svm
   |] ==> the (cdm (l,i+1)) = the (cdm (l,i)) + length iss"

end