Up to index of Isabelle/HOL/SafeImp
theory dem_POPCONT(*
Title: Lemmas for the translation SVM to JVM. POPCONT
Author: Javier de Dios and Ricardo Pe~na
Copyright: January 2009, Universidad Complutense de Madrid
*)
theory dem_POPCONT
imports "../JVMSAFE/JVMExec" SVM2JVM SVMSemantics CertifSVM2JVM
begin
no_translations "Norm s" == "(None,s)"
no_translations "ex_table_of m" == "snd (snd (snd m))"
declare trInstr.simps [simp del]
declare equivS.simps [simp del]
(* Axioms *)
axioms maxPush_POPCONT:
"2 + n < int m"
(* Lemmas for equivS *)
lemma equivS_POPCONT:
"equivS (v1 # Cont (k1, l1) # S ) S' n ctm d g ==> n >= 2"
apply (induct S)
apply (case_tac v1,simp_all)
apply (unfold equivS.simps)
apply (case_tac "(nat n)", simp, simp)
apply (case_tac "nata", simp, simp)
apply (case_tac x,simp)
apply (simp add: equivS.simps)
apply (case_tac v1,simp_all)
apply (simp add: equivS.simps)
apply (simp add: equivS.simps)
apply (case_tac x)
by (simp add: equivS.simps)
lemma equivS2_POPCONT:
"[| 2 < length vs; equivS (Val v1 # Cont (k1, l1) # S') S'a n ctm d g|]
==> equivS (Val v1 # S') (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0)) (n - 2) ctm d g"
apply (simp add: equivS.simps, clarsimp)
apply (drule equivS_ge_n)
apply (erule_tac x="1" in allE,simp)
by (subgoal_tac "-2 + n= n - 2",simp,simp)
lemma equivS_k1:
"[| equivS (Val v1 # Cont (k1, l1) # S') S'a n ctm d g|]
==> k1 = nat (the_Intg (the (S'a (nat (n - 1)))))"
by (simp add: equivS.simps)
(* Lemmas for activeCells *)
declare equivH.simps [simp del]
lemma activeCells_POPCONT:
"[| la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))|]
==> activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) =
activeCells regS (h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> the (S'a (nat n)))))) (nat (the_Intg (the (sha (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_POPCONT:
"[| 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 m (S'a(nat (n - 2) \<mapsto> the (S'a (nat n)))))) l'
(the ((h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> the (S'a (nat 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_POPCONT:
"[|((hm, k), k0, (l, i), v1 # Cont (k1, l1) # S') = ((H, ka), k0a, PC, S);
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 m S'a); sha (stackC, topf) = Some (Intg n);
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''} = {}; 2 < length vs|]
==> equivH (hm, k) (h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))))
(nat (the_Intg
(the ((sha((stackC, topf) \<mapsto> Intg (n - 2), (heapC, k0f) \<mapsto>
vs[Suc 0 := the (S'a (nat n)), 2 := the (S'a (nat (n - 1)))] ! 2))
(heapC, kf)))))
com regS d g"
apply (simp add: heapC_def add: stackC_def)
apply (simp add: kf_def add: k0f_def)
apply (fold heapC_def, fold kf_def)
apply (unfold equivH.simps, elim conjE)
apply (rule conjI, assumption)
apply (rule conjI, frule activeCells_POPCONT,simp)
apply (rule conjI, assumption)
by (rule domH_POPCONT,assumption+)
declare extractBytecode_def [simp del]
declare initConsTable_def [simp del]
declare equivS.simps [simp del]
axioms Tableswitch_POPCONT:
"drop pcc (extractBytecode P') =
[Tableswitch 1 (int (length ps)) ps] @ bytecode' ∧ ctm (nat (ps!i)) = Some i"
axioms equivpc_POPCONT:
"if' (the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3) < 1 ∨
int (length ps) < the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3))
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop)) + nat (ps ! nat (int (length ps))))
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop)) +
nat (ps ! nat (the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3) - 1))) =
the (cdm (l1, 0))"
constdefs if' :: "[bool, 'a, 'a] => 'a"
"if' c a b ≡ if c then a else b"
declare if'_def [simp del]
lemma execSVMInstr_POPCONT :
"[| (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) = POPCONT;
execSVMInst POPCONT (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 POPCONT @ 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 "∃ v1 k1 l1 S'. S=Val v1#Cont (k1,l1)#S'",clarsimp)
(* We now prove the subgoal *)
prefer 2
apply (case_tac S)
apply simp
apply (insert RightNotUndefined)
apply (erule_tac x= "S2" in allE, force)
apply simp
apply (case_tac a)
apply simp
apply (case_tac list)
apply simp
apply simp
apply (case_tac aa)
apply simp
apply (erule_tac x= "S2" in allE,force)
apply simp
apply simp
apply simp
apply simp
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 - 2),
(heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)), 2 := the (S'a (nat (n - 1)))] ! 2)" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0)))" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="[([],
vs[Suc 0 := the (S'a (nat n)), 2 := the (S'a (nat (n - 1))), 3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
if' (((the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3) < 1) ∨
(int (length ps) < the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3))))
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop)) +
nat (ps ! nat (int (length ps))))
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop)) +
nat (ps ! nat (the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3) - 1))),
ref)]" in exI)
(* Now, we prove that the JVM sequence leads to the arrival state *)
apply (subgoal_tac "∃ vs pc . fms=([],vs,safeP,sigSafeMain,pc,ref)#[]")
prefer 2 apply simp
apply (erule exE)+
apply (unfold exec_all_def)
apply (rule conjI)
apply (subgoal_tac "PC = (l,i)") prefer 2 apply simp
apply simp apply (elim conjE) apply clarsimp
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,[([], vs, safeP, sigSafeMain, the (cdm (l,i)), aa,ba)]) -jvm->
(None,sha,h,inih,[([the (sha (stackC,Sf))], vs, safeP, sigSafeMain, the (cdm (l,i)) + 1, aa,ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
(* We prove the first step of the SVM *)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (unfold extractBytecode_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
the (cdm (l, i))) = Getstatic Sf stackC",simp)
apply (unfold trInstr.simps, erule nth_via_drop_append)
(* Getstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha, h, inih,
[([the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! Suc (the (cdm (l, i)))) =
Getstatic topf stackC",simp)
apply (erule nth_via_drop_append)
(* Dup2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! (Suc (Suc (the (cdm (l, i)))))) =
Dup2",simp)
apply (erule nth_via_drop_append)
(* Dup2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) ! (Suc (Suc (Suc (the (cdm (l, i))))))) =
Dup2",simp)
apply (erule nth_via_drop_append)
(* Dup2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (the (cdm (l, i)))))))) =
Dup2",simp)
apply (erule nth_via_drop_append)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (S'a (nat n)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))) =
ArrLoad",simp)
(* Equivalencia de entornos *)
apply (frule equivS_POPCONT, simp)
apply (simp add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)
(* Store (Suc 0) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (S'a (nat n)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs, safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))) =
Store 1",simp)
apply (erule nth_via_drop_append)
(* LitPush (Intg 1) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([Intg 1,
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))) =
LitPush (Intg 1)",simp)
apply (erule nth_via_drop_append)
(* BinOp Substract *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg 1,
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf)))- 1),
the (sha (stackC, Sf)),the (sha (stackC,topf)),
the (sha (stackC, Sf)),the (sha (stackC,topf)),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))) =
BinOp Substract",simp)
apply (erule nth_via_drop_append)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf))) - 1),
the (sha (stackC, Sf)),the (sha (stackC,topf)),
the (sha (stackC, Sf)),the (sha (stackC,topf)),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (S'a (nat (n - 1))),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))) =
ArrLoad",simp)
(* Equivalencia de entornos *)
apply (frule equivS_POPCONT, 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,sha,h,inih,
[([the (S'a (nat (n - 1))),
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))) =
Store 2",simp)
apply (erule nth_via_drop_append)
(* LitPush (Intg 2) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([Intg 2,
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))) =
LitPush (Intg 2)",simp)
apply (erule nth_via_drop_append)
(* BinOp Substract *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg 2,
the (sha (stackC,topf)),the (sha (stackC, Sf)),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf))) - 2),
the (sha (stackC, Sf)),the (sha (stackC,topf)),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))) =
BinOp Substract",simp)
apply (erule nth_via_drop_append)
(* ArrLoad *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (the_Intg (the (sha (stackC, topf))) - 2),
the (sha (stackC, Sf)),the (sha (stackC,topf)),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (S'a (nat (n - 2))),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))) =
ArrLoad",simp)
(* Equivalencia de entornos *)
apply (frule equivS_POPCONT, simp)
apply (simp add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)
(* Store 3 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (S'a (nat (n - 2))),
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))) =
Store 3",simp)
apply (erule nth_via_drop_append)
(* LitPush (Intg 2) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([Intg 2,
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))) =
LitPush (Intg 2)",simp)
apply (erule nth_via_drop_append)
(* BinOp Substract *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg 2,
the (sha (stackC,topf)),the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([Intg (n - 2),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))) =
BinOp Substract",simp)
apply (erule nth_via_drop_append)
(* Dup *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (n - 2),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain, the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None,sha,h,inih,
[([Intg (n - 2),
Intg (n - 2),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))) =
Dup",simp)
apply (erule nth_via_drop_append)
(* Putstatic topf stackC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None,sha,h,inih,
[([Intg (n - 2),
Intg (n - 2),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n - 2)),h,inih,
[([Intg (n - 2),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))) =
Putstatic topf stackC",simp)
apply (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 - 2)),h,inih,
[([Intg (n - 2),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n - 2)),h,inih,
[([vs[Suc 0 := the (S'a (nat n))]! Suc 0,
Intg (n - 2),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))) =
Load 1",simp)
apply (erule nth_via_drop_append)
(* ArrStore *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha((stackC, topf) \<mapsto> Intg (n - 2)),h,inih,
[([vs[Suc 0 := the (S'a (nat n))]! Suc 0,
Intg (n - 2),
the (sha (stackC,Sf))],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n - 2)),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))))) =
ArrStore",simp)
(* Equivalencia de entornos *)
apply (frule equivS_POPCONT, simp)
apply (simp add: raise_system_xcpt_def)
apply (erule nth_via_drop_append)
(* Load 2 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha((stackC, topf) \<mapsto> Intg (n - 2)),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1, aa, ba)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n - 2)),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))]!2],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1+1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))))) =
Load 2",simp)
apply (erule nth_via_drop_append)
(* Putstatic kOf heapC *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha((stackC, topf) \<mapsto> Intg (n - 2)),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))]!2],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1+1, aa, ba)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n - 2), (heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))))))) =
Putstatic k0f heapC",simp)
apply (erule nth_via_drop_append)
(* Load 3 *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha((stackC, topf) \<mapsto> Intg (n - 2), (heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1 + 1 + 1, aa, ba)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n - 2), (heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))]!3],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1 + 1 + 1 + 1, aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i))))))))))))))))))))))))))) =
Load 3",simp)
apply (erule nth_via_drop_append)
(* Goto (trAddr pcc (pc + incPop)) *)
apply (drule drop_Suc_append)
apply (subgoal_tac "P'\<turnstile> (None, sha((stackC, topf) \<mapsto> Intg (n - 2), (heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))]!3],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
the (cdm (l, i)) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +1 + 1 + 1 + 1, aa, ba)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n - 2), (heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))]!3],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
nat (24 + int (the (cdm (l, i))) +
trAddr pcc (the (cdm (l, i)) + incPop)), aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain)))))) !
(Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (the (cdm (l, i)))))))))))))))))))))))))))) =
Goto (trAddr pcc (the (cdm (l, i)) + incPop))",simp)
apply (erule nth_via_drop_append)
(* Tableswitch nts mts ps *)
apply (subgoal_tac "drop pcc (extractBytecode P') =
[Tableswitch 1 (int (length ps)) ps] @ bytecode' ∧ ctm (nat (ps!i)) = Some i")
apply (elim conjE)
prefer 2 apply (rule Tableswitch_POPCONT)
apply (subgoal_tac "P'\<turnstile> (None, sha((stackC, topf) \<mapsto> Intg (n - 2), (heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))]!3],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
nat (24 + int (the (cdm (l, i))) +
trAddr pcc (the (cdm (l, i)) + incPop)), aa, ba)])
-jvm->
(None, sha((stackC, topf) \<mapsto> Intg (n - 2), (heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2),
h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))),inih,
[([],
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))],
safeP, sigSafeMain,
if' (((the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3) < 1) ∨
(int (length ps) < the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3))))
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop)) +
nat (ps ! nat (int (length ps))))
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop)) +
nat (ps ! nat (the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3) - 1))),
aa, ba)])")
apply (unfold exec_all_def)
apply (erule rtrancl_trans)
prefer 2
apply (rule r_into_rtrancl)
apply (clarify)
apply (unfold extractBytecode_def)
apply (unfold JVMExec.exec.simps)
apply (unfold Let_def)
apply (subgoal_tac "(fst (snd (snd (snd (snd (the (method' (P', safeP) sigSafeMain))))))) !
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop))) =
Tableswitch 1 (int (length ps)) ps",simp)
apply (simp add: if'_def)
apply (subgoal_tac
"pcc = nat (24 + int (the (cdm (l, i))) + (int pcc - int (the (cdm (l, i)) + incPop)))")
prefer 2 apply (simp add: incPop_def)
apply (simp add: trAddr_def)
apply (erule nth_via_drop)
apply simp
apply (rule_tac x="hm" in exI)
apply (rule_tac x="k" in exI)
apply (rule_tac x="k1" in exI)
apply (rule_tac x="(l1,0)" in exI)
apply (rule_tac x="Val v1 # S'" in exI)
apply (rule_tac x="sha((stackC, topf) \<mapsto> Intg (n - 2),
(heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)), 2 := the (S'a (nat (n - 1)))] ! 2)" in exI)
apply (rule_tac x="h(la \<mapsto> Arr ty m (S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0)))" in exI)
apply (rule_tac x=inih in exI)
apply (rule_tac x="vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))]" in exI)
apply (rule_tac x="if' (((the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3) < 1) ∨
(int (length ps) < the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3))))
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop)) +
nat (ps ! nat (int (length ps))))
(nat (24 + int (the (cdm (l, i))) + trAddr pcc (the (cdm (l, i)) + incPop)) +
nat (ps ! nat (the_Intg (vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1))),
3 := the (S'a (nat (n - 2)))] ! 3) - 1)))" in exI)
apply (rule_tac x="ref" in exI)
apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n - 2),
(heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2)) (heapC, kf))))" in exI)
apply (rule_tac x="nat (the_Intg (the ((sha((stackC, topf) \<mapsto> Intg (n - 2),
(heapC, k0f) \<mapsto> vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] ! 2)) (heapC, k0f))))" in exI)
apply (rule_tac x="la" in exI)
apply (rule_tac x="ty" in exI)
apply (rule_tac x="m" in exI)
apply (rule_tac x="S'a(nat (n - 2) \<mapsto> vs[Suc 0 := the (S'a (nat n))] ! Suc 0)" in exI)
apply (rule_tac x=" n - 2" 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, rule refl)
apply (rule conjI) apply (unfold trAddr_def)
apply (rule refl)
apply (rule conjI, rule refl)
apply (rule conjI, rule refl)
apply (rule conjI) apply clarsimp
apply (simp add: Sf_def add: topf_def)
apply (simp add: stackC_def add: heapC_def)
apply (rule conjI, assumption)
apply (rule conjI) apply clarsimp
apply (simp add: stackC_def add: heapC_def)
apply (simp add: kf_def add: k0f_def)
apply (rule conjI) apply (erule activeCells)
apply (rule conjI) apply (erule activeCells_2,assumption)
apply (erule activeCells_2,assumption)
apply (rule conjI, simp)
apply (rule conjI) apply (subgoal_tac "length vs = 10")
apply (simp add: stackC_def add: heapC_def)
apply (rule length_vs)
apply (rule conjI) apply clarsimp
apply (simp add: stackC_def add: heapC_def)
apply (simp add: regionsf_def add: k0f_def)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (simp add: dirCellC_def add: stackC_def)
apply (simp add: heapC_def add: safeDirf_def)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (rule conjI) apply (subgoal_tac "length vs = 10")
apply (rule equivH_POPCONT,assumption+)
apply simp
apply (rule length_vs)
apply (rule conjI) apply clarsimp
apply (rule conjI) apply clarsimp
apply (subgoal_tac "length vs = 10")
apply (rule equivS2_POPCONT,simp,assumption+)
apply (rule length_vs)
apply (rule conjI) apply (subgoal_tac "length vs = 10")
apply clarsimp
apply (rule equivS_k1,assumption+)
apply (rule length_vs)
by (rule equivpc_POPCONT)
end
lemma equivS_POPCONT:
equivS (v1.0 # Cont (k1.0, l1.0) # S) S' n ctm d g ==> 2 ≤ n
lemma equivS2_POPCONT:
[| 2 < length vs; equivS (Val v1.0 # Cont (k1.0, l1.0) # S') S'a n ctm d g |]
==> equivS (Val v1.0 # S')
(S'a(nat (n - 2) |-> vs[Suc 0 := the (S'a (nat n))] ! Suc 0)) (n - 2) ctm d
g
lemma equivS_k1:
equivS (Val v1.0 # Cont (k1.0, l1.0) # S') S'a n ctm d g
==> k1.0 = nat (the_Intg (the (S'a (nat (n - 1)))))
lemma activeCells_POPCONT:
la ∉ activeCells regS h (nat (the_Intg (the (sha (heapC, kf)))))
==> activeCells regS h (nat (the_Intg (the (sha (heapC, kf))))) =
activeCells regS
(h(la |-> Arr ty m (S'a(nat (n - 2) |-> the (S'a (nat n))))))
(nat (the_Intg (the (sha (heapC, kf)))))
lemma domH_POPCONT:
[| 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 |-> Arr ty m (S'a(nat (n - 2) |-> the (S'a (nat n)))))) l'
(the ((h(la |-> Arr ty m (S'a(nat (n - 2) |-> the (S'a (nat n))))))
l'))
(nat (the_Intg (the (sha (heapC, kf))))) com regS d g
lemma equivH_POPCONT:
[| ((hm, k), k0.0, (l, i), v1.0 # Cont (k1.0, l1.0) # S') =
((H, ka), k0a, PC, S);
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 m S'a); sha (stackC, topf) = Some (Intg n);
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''} = {}; 2 < length vs |]
==> equivH (hm, k)
(h(la |->
Arr ty m (S'a(nat (n - 2) |-> vs[Suc 0 := the (S'a (nat n))] ! Suc 0))))
(nat (the_Intg
(the ((sha((stackC, topf) |-> Intg (n - 2), (heapC, k0f) |->
vs[Suc 0 := the (S'a (nat n)),
2 := the (S'a (nat (n - 1)))] !
2))
(heapC, kf)))))
com regS d g
lemma execSVMInstr_POPCONT:
[| (P', cdm, ctm, com) = trSVM2JVM ((svms, ctmap), ini, ct, ah, ai, bc);
cdm , ctm, com \<turnstile> ((hm, k), k0.0, (l, i), S) \<triangleq> S1';
fst (the (map_of svms l)) ! i = POPCONT;
execSVMInst POPCONT (map_of ct) (hm, k) k0.0 (l, i) S = Either.Right S2.0;
drop (the (cdm (l, i))) (extractBytecode P') =
trInstr (the (cdm (l, i))) cdm' ctm' com pcc POPCONT @ bytecode' |]
==> ∃v' sh' dh' ih' fms'.
P' |- S1' -jvm-> (v', sh', dh', ih', fms') ∧
cdm , ctm, com \<turnstile> S2.0 \<triangleq> (v', sh', dh', ih', fms')