1.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Wed Nov 24 13:36:14 1999 +0100
1.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 25 12:01:28 1999 +0100
1.3 @@ -10,7 +10,7 @@
1.4 Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
1.5 "\\<lbrakk> wt_jvm_prog G phi; \
1.6 \ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
1.7 -\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
1.8 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
1.9 \\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
1.10 by (Asm_full_simp_tac 1);
1.11 by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1);
1.12 @@ -28,8 +28,8 @@
1.13 \ ins!pc = LS(Load idx); \
1.14 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.15 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.16 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.17 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.18 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.19 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.20 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
1.21 approx_loc_imp_approx_loc_sup]
1.22 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
1.23 @@ -42,8 +42,8 @@
1.24 \ ins!pc = LS(Store idx); \
1.25 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.26 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.27 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.28 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.29 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.30 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.31 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
1.32 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]
1.33 addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1);
1.34 @@ -60,8 +60,8 @@
1.35 \ ins!pc = LS(Bipush i); \
1.36 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.37 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.38 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.39 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.40 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.41 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.42 by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
1.43 addss (simpset() addsimps [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
1.44 qed "Bipush_correct";
1.45 @@ -84,8 +84,8 @@
1.46 \ ins!pc = LS Aconst_null; \
1.47 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.48 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.49 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.50 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.51 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.52 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.53 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
1.54 addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
1.55 qed "Aconst_null_correct";
1.56 @@ -96,8 +96,8 @@
1.57 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.58 \ ins!pc = LS ls_com; \
1.59 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.60 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.61 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.62 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.63 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.64 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
1.65 ba 1;
1.66 ba 1;
1.67 @@ -131,8 +131,8 @@
1.68 \ ins!pc = CH (Checkcast D); \
1.69 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.70 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.71 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.72 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.73 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.74 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.75 by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,
1.76 xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
1.77 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
1.78 @@ -146,8 +146,8 @@
1.79 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.80 \ ins!pc = CH ch_com; \
1.81 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.82 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.83 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.84 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.85 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.86 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
1.87 ba 1;
1.88 ba 1;
1.89 @@ -164,8 +164,8 @@
1.90 \ ins!pc = MO (Getfield F D); \
1.91 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.92 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.93 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.94 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.95 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.96 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.97 by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
1.98 by (Clarify_tac 1);
1.99 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
1.100 @@ -203,8 +203,8 @@
1.101 \ ins!pc = MO (Putfield F D); \
1.102 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.103 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.104 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.105 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.106 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.107 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.108 by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
1.109 by (Clarify_tac 1);
1.110 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
1.111 @@ -231,8 +231,8 @@
1.112 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.113 \ ins!pc = MO mo_com; \
1.114 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.115 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.116 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.117 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.118 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.119 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
1.120 ba 1;
1.121 ba 1;
1.122 @@ -250,12 +250,12 @@
1.123
1.124 Goal
1.125 "\\<lbrakk> wf_prog wt G; \
1.126 -\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
1.127 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.128 \ ins!pc = CO(New cl_idx); \
1.129 -\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
1.130 -\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
1.131 -\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
1.132 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.133 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.134 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.135 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.136 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.137 by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
1.138 approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
1.139 approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
1.140 @@ -271,8 +271,8 @@
1.141 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.142 \ ins!pc = CO co_com; \
1.143 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.144 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.145 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.146 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.147 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.148 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
1.149 ba 1;
1.150 ba 1;
1.151 @@ -287,11 +287,11 @@
1.152 Goal
1.153 "\\<lbrakk> wt_jvm_prog G phi; \
1.154 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.155 -\ ins ! pc = MI(Invokevirtual mn pTs); \
1.156 +\ ins ! pc = MI(Invoke mn pTs); \
1.157 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.158 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.159 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.160 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.161 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.162 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.163 by(forward_tac [wt_jvm_progD] 1);
1.164 by(etac exE 1);
1.165 by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1
1.166 @@ -361,20 +361,20 @@
1.167 by (fast_tac (claset()
1.168 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
1.169 addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1);
1.170 -qed "Invokevirtual_correct";
1.171 +qed "Invoke_correct";
1.172
1.173 Goal
1.174 "\\<lbrakk> wt_jvm_prog G phi; \
1.175 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.176 \ ins!pc = MI mi_com; \
1.177 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.178 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.179 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.180 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.181 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.182 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
1.183 ba 1;
1.184 ba 1;
1.185 by (exhaust_tac "mi_com" 1);
1.186 -by (ALLGOALS (fast_tac (claset() addIs [Invokevirtual_correct])));
1.187 +by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
1.188 qed "MI_correct";
1.189
1.190 (****** MR ******)
1.191 @@ -395,11 +395,11 @@
1.192 Goal
1.193 "\\<lbrakk> wt_jvm_prog G phi; \
1.194 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.195 -\ ins ! pc = MR; \
1.196 +\ ins ! pc = MR Return; \
1.197 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.198 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.199 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.200 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.201 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.202 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.203 by (asm_full_simp_tac (simpset() addsimps defs1) 1);
1.204 by (Clarify_tac 1);
1.205 by (asm_full_simp_tac (simpset() addsimps defs1) 1);
1.206 @@ -424,13 +424,14 @@
1.207 Goal
1.208 "\\<lbrakk> wt_jvm_prog G phi; \
1.209 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.210 -\ ins!pc = MR; \
1.211 +\ ins!pc = MR mr; \
1.212 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.213 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.214 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.215 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.216 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.217 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
1.218 ba 1;
1.219 ba 1;
1.220 +by (exhaust_tac "mr" 1);
1.221 by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
1.222 qed "MR_correct";
1.223
1.224 @@ -441,8 +442,8 @@
1.225 \ ins ! pc = BR(Goto branch); \
1.226 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.227 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.228 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.229 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.230 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.231 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.232 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
1.233 addss (simpset() addsimps defs1)) 1);
1.234 qed "Goto_correct";
1.235 @@ -454,8 +455,8 @@
1.236 \ ins!pc = BR(Ifcmpeq branch); \
1.237 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.238 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.239 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.240 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.241 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.242 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.243 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
1.244 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
1.245 qed "Ifiacmpeq_correct";
1.246 @@ -466,8 +467,8 @@
1.247 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.248 \ ins!pc = BR br_com; \
1.249 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.250 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.251 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.252 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.253 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.254 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
1.255 ba 1;
1.256 ba 1;
1.257 @@ -485,8 +486,8 @@
1.258 \ ins ! pc = OS Pop; \
1.259 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.260 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.261 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.262 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.263 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.264 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.265 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
1.266 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
1.267 qed "Pop_correct";
1.268 @@ -498,8 +499,8 @@
1.269 \ ins ! pc = OS Dup; \
1.270 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.271 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.272 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.273 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.274 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.275 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.276 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
1.277 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
1.278 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
1.279 @@ -512,8 +513,8 @@
1.280 \ ins ! pc = OS Dup_x1; \
1.281 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.282 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.283 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.284 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.285 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.286 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.287 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
1.288 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
1.289 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
1.290 @@ -525,8 +526,8 @@
1.291 \ ins ! pc = OS Dup_x2; \
1.292 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.293 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.294 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.295 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.296 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.297 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.298 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
1.299 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
1.300 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
1.301 @@ -538,8 +539,8 @@
1.302 \ ins ! pc = OS Swap; \
1.303 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
1.304 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
1.305 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.306 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.307 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.308 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.309 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
1.310 addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
1.311 addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
1.312 @@ -550,8 +551,8 @@
1.313 \ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
1.314 \ ins!pc = OS os_com; \
1.315 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
1.316 -\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
1.317 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
1.318 +\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
1.319 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.320 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
1.321 ba 1;
1.322 ba 1;
1.323 @@ -563,15 +564,15 @@
1.324 (** Main **)
1.325
1.326 Goalw [correct_state_def,Let_def]
1.327 - "correct_state G phi (None,hp,(stk,loc,C,sig,pc)#fs) \
1.328 -\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) sig = Some(C,meth)";
1.329 + "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \
1.330 +\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) ml = Some(C,meth)";
1.331 by(Asm_full_simp_tac 1);
1.332 by(Blast_tac 1);
1.333 qed "correct_state_impl_Some_cmethd";
1.334
1.335 Goal
1.336 -"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; correct_state G phi state\\<rbrakk> \
1.337 -\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> correct_state G phi state'";
1.338 +"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \
1.339 +\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
1.340 by(split_all_tac 1);
1.341 by(rename_tac "xp hp frs" 1);
1.342 by (exhaust_tac "xp" 1);
1.343 @@ -596,9 +597,8 @@
1.344 qed_spec_mp "exec_lemma";
1.345
1.346 Goal
1.347 -"\\<lbrakk> wt_jvm_prog G phi; \
1.348 -\ correct_state G phi (xp,hp,frs); xp=None; frs\\<noteq>[] \\<rbrakk> \
1.349 -\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs') \\<and> correct_state G phi (xp',hp',frs')";
1.350 +"\\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[] \\<rbrakk> \
1.351 +\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec(G,xp,hp,frs) = Some(xp',hp',frs') \\<and> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
1.352 by (dres_inst_tac [("G","G"),("hp","hp")] exec_lemma 1);
1.353 ba 1;
1.354 by (fast_tac (claset() addIs [BV_correct_1]) 1);
1.355 @@ -606,8 +606,7 @@
1.356 (*******)
1.357
1.358 Goalw [exec_all_def]
1.359 -"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \
1.360 -\ \\<Longrightarrow> correct_state G phi s \\<longrightarrow> correct_state G phi t";
1.361 +"\\<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>";
1.362 be rtrancl_induct 1;
1.363 by (Simp_tac 1);
1.364 by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1);
1.365 @@ -615,7 +614,7 @@
1.366
1.367
1.368 Goal
1.369 -"\\<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> \
1.370 +"\\<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> \
1.371 \ \\<Longrightarrow> approx_stk G hp stk (fst (((phi cn) ml) ! pc)) \\<and> approx_loc G hp loc (snd (((phi cn) ml) ! pc)) ";
1.372 bd BV_correct 1;
1.373 ba 1;