--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 25 12:01:28 1999 +0100
@@ -10,7 +10,7 @@
Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
"\\<lbrakk> wt_jvm_prog G phi; \
\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
-\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
by (Asm_full_simp_tac 1);
by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1);
@@ -28,8 +28,8 @@
\ ins!pc = LS(Load idx); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
@@ -42,8 +42,8 @@
\ ins!pc = LS(Store idx); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]
addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1);
@@ -60,8 +60,8 @@
\ ins!pc = LS(Bipush i); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
qed "Bipush_correct";
@@ -84,8 +84,8 @@
\ ins!pc = LS Aconst_null; \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
qed "Aconst_null_correct";
@@ -96,8 +96,8 @@
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = LS ls_com; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
@@ -131,8 +131,8 @@
\ ins!pc = CH (Checkcast D); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,
xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
@@ -146,8 +146,8 @@
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = CH ch_com; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
@@ -164,8 +164,8 @@
\ ins!pc = MO (Getfield F D); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
@@ -203,8 +203,8 @@
\ ins!pc = MO (Putfield F D); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
@@ -231,8 +231,8 @@
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = MO mo_com; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
@@ -250,12 +250,12 @@
Goal
"\\<lbrakk> wf_prog wt G; \
-\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
+\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = CO(New cl_idx); \
-\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
+\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
@@ -271,8 +271,8 @@
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = CO co_com; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
@@ -287,11 +287,11 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
-\ ins ! pc = MI(Invokevirtual mn pTs); \
+\ ins ! pc = MI(Invoke mn pTs); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_progD] 1);
by(etac exE 1);
by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1
@@ -361,20 +361,20 @@
by (fast_tac (claset()
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1);
-qed "Invokevirtual_correct";
+qed "Invoke_correct";
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = MI mi_com; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
by (exhaust_tac "mi_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Invokevirtual_correct])));
+by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
qed "MI_correct";
(****** MR ******)
@@ -395,11 +395,11 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
-\ ins ! pc = MR; \
+\ ins ! pc = MR Return; \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (asm_full_simp_tac (simpset() addsimps defs1) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps defs1) 1);
@@ -424,13 +424,14 @@
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
-\ ins!pc = MR; \
+\ ins!pc = MR mr; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
+by (exhaust_tac "mr" 1);
by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
qed "MR_correct";
@@ -441,8 +442,8 @@
\ ins ! pc = BR(Goto branch); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
addss (simpset() addsimps defs1)) 1);
qed "Goto_correct";
@@ -454,8 +455,8 @@
\ ins!pc = BR(Ifcmpeq branch); \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
qed "Ifiacmpeq_correct";
@@ -466,8 +467,8 @@
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = BR br_com; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
@@ -485,8 +486,8 @@
\ ins ! pc = OS Pop; \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
qed "Pop_correct";
@@ -498,8 +499,8 @@
\ ins ! pc = OS Dup; \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
@@ -512,8 +513,8 @@
\ ins ! pc = OS Dup_x1; \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
@@ -525,8 +526,8 @@
\ ins ! pc = OS Dup_x2; \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
@@ -538,8 +539,8 @@
\ ins ! pc = OS Swap; \
\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
@@ -550,8 +551,8 @@
\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
\ ins!pc = OS os_com; \
\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
-\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
-\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
+\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
+\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
@@ -563,15 +564,15 @@
(** Main **)
Goalw [correct_state_def,Let_def]
- "correct_state G phi (None,hp,(stk,loc,C,sig,pc)#fs) \
-\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) sig = Some(C,meth)";
+ "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \
+\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) ml = Some(C,meth)";
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
qed "correct_state_impl_Some_cmethd";
Goal
-"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; correct_state G phi state\\<rbrakk> \
-\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> correct_state G phi state'";
+"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \
+\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
by(split_all_tac 1);
by(rename_tac "xp hp frs" 1);
by (exhaust_tac "xp" 1);
@@ -596,9 +597,8 @@
qed_spec_mp "exec_lemma";
Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ correct_state G phi (xp,hp,frs); xp=None; frs\\<noteq>[] \\<rbrakk> \
-\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs') \\<and> correct_state G phi (xp',hp',frs')";
+"\\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[] \\<rbrakk> \
+\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec(G,xp,hp,frs) = Some(xp',hp',frs') \\<and> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
by (dres_inst_tac [("G","G"),("hp","hp")] exec_lemma 1);
ba 1;
by (fast_tac (claset() addIs [BV_correct_1]) 1);
@@ -606,8 +606,7 @@
(*******)
Goalw [exec_all_def]
-"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \
-\ \\<Longrightarrow> correct_state G phi s \\<longrightarrow> correct_state G phi t";
+"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \\<Longrightarrow> G,phi \\<turnstile>JVM s\\<surd> \\<longrightarrow> G,phi \\<turnstile>JVM t\\<surd>";
be rtrancl_induct 1;
by (Simp_tac 1);
by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1);
@@ -615,7 +614,7 @@
Goal
-"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,cn,ml,pc)#frs); correct_state G phi s0 \\<rbrakk> \
+"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,cn,ml,pc)#frs); G,phi \\<turnstile>JVM s0 \\<surd>\\<rbrakk> \
\ \\<Longrightarrow> approx_stk G hp stk (fst (((phi cn) ml) ! pc)) \\<and> approx_loc G hp loc (snd (((phi cn) ml) ! pc)) ";
bd BV_correct 1;
ba 1;