1.1 --- a/src/HOL/MicroJava/BV/BVSpec.ML Thu Nov 25 12:30:57 1999 +0100
1.2 +++ b/src/HOL/MicroJava/BV/BVSpec.ML Fri Nov 26 08:46:59 1999 +0100
1.3 @@ -11,19 +11,19 @@
1.4
1.5 Goalw [wt_jvm_prog_def]
1.6 "\\<lbrakk> wt_jvm_prog G phi; \
1.7 -\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
1.8 +\ method (G,C) sig = Some (C,rT,maxl,ins); \
1.9 \ pc < length ins \\<rbrakk> \
1.10 \\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
1.11 -by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1);
1.12 +by(forward_tac [rotate_prems 2 method_wf_mdecl] 1);
1.13 by (Asm_full_simp_tac 1);
1.14 by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
1.15 qed "wt_jvm_prog_impl_wt_instr";
1.16
1.17 Goalw [wt_jvm_prog_def]
1.18 "\\<lbrakk> wt_jvm_prog G phi; \
1.19 -\ cmethd (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow> \
1.20 +\ method (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow> \
1.21 \ 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)";
1.22 -by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1);
1.23 +by(forward_tac [rotate_prems 2 method_wf_mdecl] 1);
1.24 by (Asm_full_simp_tac 1);
1.25 by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
1.26 qed "wt_jvm_prog_impl_wt_start";
2.1 --- a/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 25 12:30:57 1999 +0100
2.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Nov 26 08:46:59 1999 +0100
2.3 @@ -52,7 +52,7 @@
2.4 in
2.5 pc+1 < max_pc \\<and>
2.6 is_class G C \\<and>
2.7 - (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
2.8 + (\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and>
2.9 ST = oT # ST' \\<and>
2.10 G \\<turnstile> oT \\<preceq> (Class C) \\<and>
2.11 G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))"
2.12 @@ -63,7 +63,7 @@
2.13 pc+1 < max_pc \\<and>
2.14 is_class G C \\<and>
2.15 (\\<exists>T vT oT ST'.
2.16 - cfield (G,C) F = Some(C,T) \\<and>
2.17 + field (G,C) F = Some(C,T) \\<and>
2.18 ST = vT # oT # ST' \\<and>
2.19 G \\<turnstile> oT \\<preceq> (Class C) \\<and>
2.20 G \\<turnstile> vT \\<preceq> T \\<and>
2.21 @@ -155,7 +155,7 @@
2.22 (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
2.23 length apTs = length fpTs \\<and>
2.24 (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
2.25 - (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
2.26 + (\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
2.27 G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
2.28
2.29 consts
3.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 25 12:30:57 1999 +0100
3.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Fri Nov 26 08:46:59 1999 +0100
3.3 @@ -9,7 +9,7 @@
3.4
3.5 Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
3.6 "\\<lbrakk> wt_jvm_prog G phi; \
3.7 -\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
3.8 +\ method (G,C) sig = Some (C,rT,maxl,ins); \
3.9 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
3.10 \\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
3.11 by (Asm_full_simp_tac 1);
3.12 @@ -24,7 +24,7 @@
3.13
3.14 Goal
3.15 "\\<lbrakk> wf_prog wt G; \
3.16 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.17 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.18 \ ins!pc = LS(Load idx); \
3.19 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.20 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.21 @@ -38,7 +38,7 @@
3.22
3.23 Goal
3.24 "\\<lbrakk> wf_prog wt G; \
3.25 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.26 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.27 \ ins!pc = LS(Store idx); \
3.28 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.29 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.30 @@ -56,7 +56,7 @@
3.31
3.32 Goal
3.33 "\\<lbrakk> wf_prog wt G; \
3.34 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.35 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.36 \ ins!pc = LS(Bipush i); \
3.37 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.38 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.39 @@ -80,7 +80,7 @@
3.40
3.41 Goal
3.42 "\\<lbrakk> wf_prog wt G; \
3.43 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.44 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.45 \ ins!pc = LS Aconst_null; \
3.46 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.47 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.48 @@ -93,7 +93,7 @@
3.49
3.50 Goal
3.51 "\\<lbrakk> wt_jvm_prog G phi; \
3.52 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.53 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.54 \ ins!pc = LS ls_com; \
3.55 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.56 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.57 @@ -127,14 +127,14 @@
3.58
3.59 Goal
3.60 "\\<lbrakk> wf_prog wt G; \
3.61 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.62 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.63 \ ins!pc = CH (Checkcast D); \
3.64 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.65 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.66 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.67 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.68 by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,
3.69 - xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.70 + raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.71 by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.72 addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2]
3.73 addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,approx_val_def])) 1);
3.74 @@ -143,7 +143,7 @@
3.75
3.76 Goal
3.77 "\\<lbrakk> wt_jvm_prog G phi; \
3.78 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.79 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.80 \ ins!pc = CH ch_com; \
3.81 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.82 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.83 @@ -160,13 +160,13 @@
3.84 (******* MO *******)
3.85 Goal
3.86 "\\<lbrakk> wf_prog wt G; \
3.87 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.88 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.89 \ ins!pc = MO (Getfield F D); \
3.90 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.91 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.92 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.93 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.94 -by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.95 +by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.96 by (Clarify_tac 1);
3.97 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
3.98 by (Clarify_tac 1);
3.99 @@ -199,13 +199,13 @@
3.100
3.101 Goal
3.102 "\\<lbrakk> wf_prog wt G; \
3.103 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.104 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.105 \ ins!pc = MO (Putfield F D); \
3.106 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.107 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.108 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.109 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.110 -by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.111 +by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.112 by (Clarify_tac 1);
3.113 by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
3.114 by (Clarify_tac 1);
3.115 @@ -228,7 +228,7 @@
3.116
3.117 Goal
3.118 "\\<lbrakk> wt_jvm_prog G phi; \
3.119 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.120 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.121 \ ins!pc = MO mo_com; \
3.122 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.123 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.124 @@ -250,7 +250,7 @@
3.125
3.126 Goal
3.127 "\\<lbrakk> wf_prog wt G; \
3.128 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.129 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.130 \ ins!pc = CO(New cl_idx); \
3.131 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.132 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.133 @@ -262,13 +262,13 @@
3.134 hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref,
3.135 rewrite_rule [split_def] correct_init_obj]
3.136 addss (simpset() addsimps [NT_subtype_conv,approx_stk_Cons,approx_val_def,conf_def,
3.137 - fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,xcpt_update_def,raise_xcpt_def,init_vars_def]@defs1
3.138 + fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,raise_xcpt_def,init_vars_def]@defs1
3.139 addsplits [option.split])) 1);
3.140 qed "New_correct";
3.141
3.142 Goal
3.143 "\\<lbrakk> wt_jvm_prog G phi; \
3.144 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.145 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.146 \ ins!pc = CO co_com; \
3.147 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.148 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.149 @@ -286,7 +286,7 @@
3.150
3.151 Goal
3.152 "\\<lbrakk> wt_jvm_prog G phi; \
3.153 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.154 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.155 \ ins ! pc = MI(Invoke mn pTs); \
3.156 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.157 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.158 @@ -294,7 +294,7 @@
3.159 \\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
3.160 by(forward_tac [wt_jvm_progD] 1);
3.161 by(etac exE 1);
3.162 -by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1
3.163 +by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1
3.164 addsplits [option.split]) 1);
3.165 by (Clarify_tac 1);
3.166 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
3.167 @@ -315,11 +315,11 @@
3.168 by(rename_tac "oT'" 1);
3.169 by (Clarify_tac 1);
3.170 by(subgoal_tac "G \\<turnstile> Class oT \\<preceq> Class oT'" 1);
3.171 - by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 cmethd_wf_mdecl)) 2);
3.172 + by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 method_wf_mdecl)) 2);
3.173 ba 2;
3.174 by(Blast_tac 2);
3.175 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
3.176 -by(forward_tac [cmethd_in_md] 1);
3.177 +by(forward_tac [method_in_md] 1);
3.178 ba 1;
3.179 back();
3.180 back();
3.181 @@ -365,7 +365,7 @@
3.182
3.183 Goal
3.184 "\\<lbrakk> wt_jvm_prog G phi; \
3.185 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.186 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.187 \ ins!pc = MI mi_com; \
3.188 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.189 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.190 @@ -394,7 +394,7 @@
3.191 Delsimps [map_append];
3.192 Goal
3.193 "\\<lbrakk> wt_jvm_prog G phi; \
3.194 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.195 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.196 \ ins ! pc = MR Return; \
3.197 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.198 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.199 @@ -423,7 +423,7 @@
3.200
3.201 Goal
3.202 "\\<lbrakk> wt_jvm_prog G phi; \
3.203 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.204 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.205 \ ins!pc = MR mr; \
3.206 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.207 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.208 @@ -438,7 +438,7 @@
3.209 (****** BR ******)
3.210 Goal
3.211 "\\<lbrakk> wf_prog wt G; \
3.212 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.213 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.214 \ ins ! pc = BR(Goto branch); \
3.215 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.216 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.217 @@ -451,7 +451,7 @@
3.218
3.219 Goal
3.220 "\\<lbrakk> wf_prog wt G; \
3.221 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.222 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.223 \ ins!pc = BR(Ifcmpeq branch); \
3.224 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.225 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.226 @@ -464,7 +464,7 @@
3.227
3.228 Goal
3.229 "\\<lbrakk> wt_jvm_prog G phi; \
3.230 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.231 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.232 \ ins!pc = BR br_com; \
3.233 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.234 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.235 @@ -482,7 +482,7 @@
3.236
3.237 Goal
3.238 "\\<lbrakk> wf_prog wt G; \
3.239 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.240 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.241 \ ins ! pc = OS Pop; \
3.242 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.243 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.244 @@ -495,7 +495,7 @@
3.245
3.246 Goal
3.247 "\\<lbrakk> wf_prog wt G; \
3.248 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.249 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.250 \ ins ! pc = OS Dup; \
3.251 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.252 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.253 @@ -509,7 +509,7 @@
3.254
3.255 Goal
3.256 "\\<lbrakk> wf_prog wt G; \
3.257 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.258 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.259 \ ins ! pc = OS Dup_x1; \
3.260 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.261 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.262 @@ -522,7 +522,7 @@
3.263
3.264 Goal
3.265 "\\<lbrakk> wf_prog wt G; \
3.266 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.267 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.268 \ ins ! pc = OS Dup_x2; \
3.269 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.270 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.271 @@ -535,7 +535,7 @@
3.272
3.273 Goal
3.274 "\\<lbrakk> wf_prog wt G; \
3.275 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.276 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.277 \ ins ! pc = OS Swap; \
3.278 \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.279 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.280 @@ -548,7 +548,7 @@
3.281
3.282 Goal
3.283 "\\<lbrakk> wt_jvm_prog G phi; \
3.284 -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.285 +\ method (G,C) ml = Some (C,rT,maxl,ins); \
3.286 \ ins!pc = OS os_com; \
3.287 \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.288 \ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
3.289 @@ -565,10 +565,10 @@
3.290
3.291 Goalw [correct_state_def,Let_def]
3.292 "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \
3.293 -\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) ml = Some(C,meth)";
3.294 +\ \\<Longrightarrow> \\<exists>meth. method (G,C) ml = Some(C,meth)";
3.295 by(Asm_full_simp_tac 1);
3.296 by(Blast_tac 1);
3.297 -qed "correct_state_impl_Some_cmethd";
3.298 +qed "correct_state_impl_Some_method";
3.299
3.300 Goal
3.301 "\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \
3.302 @@ -580,7 +580,7 @@
3.303 by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
3.304 by(split_all_tac 1);
3.305 by(hyp_subst_tac 1);
3.306 - by(forward_tac [correct_state_impl_Some_cmethd] 1);
3.307 + by(forward_tac [correct_state_impl_Some_method] 1);
3.308 by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct,
3.309 BR_correct], simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1);
3.310 by (exhaust_tac "frs" 1);
4.1 --- a/src/HOL/MicroJava/BV/Correct.thy Thu Nov 25 12:30:57 1999 +0100
4.2 +++ b/src/HOL/MicroJava/BV/Correct.thy Fri Nov 26 08:46:59 1999 +0100
4.3 @@ -34,14 +34,14 @@
4.4 (ST,LT) = (phi C ml) ! pc
4.5 in
4.6 (\\<exists>rT maxl ins.
4.7 - cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
4.8 + method (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
4.9 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invoke mn pTs) \\<and>
4.10 (mn,pTs) = ml0 \\<and>
4.11 (\\<exists>apTs D ST'.
4.12 fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\<and>
4.13 length apTs = length pTs \\<and>
4.14 (\\<exists>D' rT' maxl' ins'.
4.15 - cmethd (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
4.16 + method (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
4.17 G \\<turnstile> rT0 \\<preceq> rT') \\<and>
4.18 correct_frame G hp (tl ST, LT) maxl ins f \\<and>
4.19 correct_frames G hp phi rT C ml frs))))"
4.20 @@ -57,7 +57,7 @@
4.21 | (f#fs) \\<Rightarrow> (let (stk,loc,C,ml,pc) = f
4.22 in
4.23 \\<exists>rT maxl ins.
4.24 - cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
4.25 + method (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
4.26 G\\<turnstile>h hp\\<surd> \\<and>
4.27 correct_frame G hp ((phi C ml) ! pc) maxl ins f \\<and>
4.28 correct_frames G hp phi rT C ml fs))
5.1 --- a/src/HOL/MicroJava/J/Eval.thy Thu Nov 25 12:30:57 1999 +0100
5.2 +++ b/src/HOL/MicroJava/J/Eval.thy Fri Nov 26 08:46:59 1999 +0100
5.3 @@ -72,7 +72,7 @@
5.4 (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
5.5 Call "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a';
5.6 G\\<turnstile>s1 -ps[\\<succ>]pvs\\<rightarrow> (x,(h,l)); dynT = fst (the (h a));
5.7 - (md,rT,pns,lvars,blk,res) = the (cmethd (G,dynT) (mn,pTs));
5.8 + (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
5.9 G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk\\<rightarrow> s3;
5.10 G\\<turnstile> s3 -res\\<succ>v \\<rightarrow> (x4,s4)\\<rbrakk> \\<Longrightarrow>
5.11 G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v\\<rightarrow> (x4,(heap s4,l))"
6.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML Thu Nov 25 12:30:57 1999 +0100
6.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML Fri Nov 26 08:46:59 1999 +0100
6.3 @@ -44,7 +44,7 @@
6.4 by Auto_tac;
6.5 qed "Cast_conf";
6.6
6.7 -Goal "\\<lbrakk> wf_prog wtm G; cfield (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
6.8 +Goal "\\<lbrakk> wf_prog wtm G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
6.9 \ x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
6.10 \ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
6.11 by( dtac np_NoneD 1);
6.12 @@ -66,7 +66,7 @@
6.13 "\\<lbrakk> wf_prog wtm G; a = the_Addr a'; (c, fs) = the (h a); \
6.14 \ (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
6.15 \ (G, lT)\\<turnstile>aa\\<Colon>Class C; \
6.16 -\ cfield (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
6.17 +\ field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
6.18 \ x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq>Class C; h'\\<le>|h; \
6.19 \ (h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>x\\<Colon>\\<preceq>T'; np a' x' = None\\<rbrakk> \\<Longrightarrow> \
6.20 \ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and> \
6.21 @@ -126,7 +126,7 @@
6.22 \ max_spec G T (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
6.23 \ list_all2 (conf G h) pvs pTsa;\
6.24 \ (md, rT, pns, lvars, blk, res) = \
6.25 -\ the (cmethd (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
6.26 +\ the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
6.27 \ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> \
6.28 \ (G, lT)\\<turnstile>blk\\<surd> \\<longrightarrow> h\\<le>|xi \\<and> (xi, xl)\\<Colon>\\<preceq>(G, lT); \
6.29 \ \\<forall>lT. (xi, xl)\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> (\\<forall>T. (G, lT)\\<turnstile>res\\<Colon>T \\<longrightarrow> \
6.30 @@ -146,7 +146,7 @@
6.31 by( Clarsimp_tac 1);
6.32 by( EVERY'[dtac Call_lemma, atac, atac] 1);
6.33 by( clarsimp_tac (claset(),simpset() addsimps [wt_java_mdecl_def])1);
6.34 -by( thin_tac "cmethd ?sig ?x = ?y" 1);
6.35 +by( thin_tac "method ?sig ?x = ?y" 1);
6.36 by( EVERY'[dtac spec, etac impE] 1);
6.37 by( mp_tac 2);
6.38 by( rtac conformsI 1);
6.39 @@ -326,7 +326,7 @@
6.40
6.41 Goal "\\<lbrakk>G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'\\<rightarrow> Norm s'; a' \\<noteq> Null;\
6.42 \ s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>RefT T; m_head G T sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
6.43 -\ cmethd (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
6.44 +\ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
6.45 by( dtac eval_type_sound 1);
6.46 by( atac 1);
6.47 by( atac 1);
7.1 --- a/src/HOL/MicroJava/J/TypeRel.ML Thu Nov 25 12:30:57 1999 +0100
7.2 +++ b/src/HOL/MicroJava/J/TypeRel.ML Fri Nov 26 08:46:59 1999 +0100
7.3 @@ -76,8 +76,8 @@
7.4 by(Force_tac 1);
7.5 val wf_subcls1_rel = result();
7.6
7.7 -val cmethd_TC = prove_goalw_cterm [subcls1_rel_def]
7.8 - (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (cmethd.tcs)))))
7.9 +val method_TC = prove_goalw_cterm [subcls1_rel_def]
7.10 + (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs)))))
7.11 (K [auto_tac (claset() addIs [subcls1I], simpset())]);
7.12
7.13 val fields_TC = prove_goalw_cterm [subcls1_rel_def]
8.1 --- a/src/HOL/MicroJava/J/TypeRel.thy Thu Nov 25 12:30:57 1999 +0100
8.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Nov 26 08:46:59 1999 +0100
8.3 @@ -32,8 +32,8 @@
8.4
8.5 consts
8.6
8.7 - cmethd :: "'c prog \\<times> cname \\<Rightarrow> ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
8.8 - cfield :: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
8.9 + method :: "'c prog \\<times> cname \\<Rightarrow> ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
8.10 + field :: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
8.11 fields :: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times> ty) list"
8.12
8.13 constdefs (* auxiliary relations for recursive definitions below *)
8.14 @@ -42,10 +42,10 @@
8.15 "subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}"
8.16
8.17 (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
8.18 -recdef cmethd "subcls1_rel"
8.19 - "cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
8.20 +recdef method "subcls1_rel"
8.21 + "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
8.22 | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow>
8.23 - if is_class G D then cmethd (G,D)
8.24 + if is_class G D then method (G,D)
8.25 else arbitrary) \\<oplus>
8.26 map_of (map (\\<lambda>(s, m ).
8.27 (s,(C,m))) ms))
8.28 @@ -61,7 +61,7 @@
8.29 else arbitrary)"
8.30 defs
8.31
8.32 - cfield_def "cfield \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
8.33 + field_def "field \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
8.34
8.35 inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
8.36 i.e. sort of syntactic subtyping *)
9.1 --- a/src/HOL/MicroJava/J/WellForm.ML Thu Nov 25 12:30:57 1999 +0100
9.2 +++ b/src/HOL/MicroJava/J/WellForm.ML Fri Nov 26 08:46:59 1999 +0100
9.3 @@ -111,11 +111,11 @@
9.4 by( etac subcls1I 1);
9.5 qed "subcls1_induct";
9.6
9.7 -Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) = \
9.8 +Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) = \
9.9 \ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
9.10 -\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> cmethd (G,D)) \\<oplus> \
9.11 +\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
9.12 \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
9.13 -by( stac (cmethd_TC RS (wf_subcls1_rel RS (hd cmethd.rules))) 1);
9.14 +by( stac (method_TC RS (wf_subcls1_rel RS (hd method.rules))) 1);
9.15 by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
9.16 addsplits [option.split]) 1);
9.17 by( case_tac "C = Object" 1);
9.18 @@ -125,7 +125,7 @@
9.19 by( dtac wf_cdecl_supD 1);
9.20 by( atac 1);
9.21 by( Asm_full_simp_tac 1);
9.22 -val cmethd_rec = result();
9.23 +val method_rec = result();
9.24
9.25 Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wtm G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
9.26 \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
9.27 @@ -144,14 +144,14 @@
9.28 by( Asm_full_simp_tac 1);
9.29 val fields_rec = result();
9.30
9.31 -val cmethd_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> cmethd (G,Object) = empty"
9.32 - (K [stac cmethd_rec 1,Auto_tac]);
9.33 +val method_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> method (G,Object) = empty"
9.34 + (K [stac method_rec 1,Auto_tac]);
9.35 val fields_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> fields (G,Object) = []"(K [
9.36 stac fields_rec 1,Auto_tac]);
9.37 -Addsimps [cmethd_Object, fields_Object];
9.38 -val cfield_Object = prove_goalw thy [cfield_def]
9.39 - "\\<And>X. wf_prog wtm G \\<Longrightarrow> cfield (G,Object) = empty" (K [Asm_simp_tac 1]);
9.40 -Addsimps [cfield_Object];
9.41 +Addsimps [method_Object, fields_Object];
9.42 +val field_Object = prove_goalw thy [field_def]
9.43 + "\\<And>X. wf_prog wtm G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
9.44 +Addsimps [field_Object];
9.45
9.46 val subcls_C_Object = prove_goal thy
9.47 "\\<And>X. \\<lbrakk>is_class G C; wf_prog wtm G \\<rbrakk> \\<Longrightarrow> C \\<noteq> Object \\<longrightarrow> G\\<turnstile>C\\<prec>C Object" (K [
9.48 @@ -264,24 +264,24 @@
9.49 val widen_fields_mono = result();
9.50
9.51
9.52 -val cfs_fields_lemma = prove_goalw thy [cfield_def]
9.53 -"\\<And>X. cfield (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
9.54 +val cfs_fields_lemma = prove_goalw thy [field_def]
9.55 +"\\<And>X. field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
9.56 (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
9.57
9.58 -val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>cfield (G,C) fn = Some (fd, fT);\
9.59 +val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
9.60 \ G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
9.61 fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
9.62
9.63 -Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) sig = Some (md,mh,m)\
9.64 +Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
9.65 \ \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wtm G md (sig,(mh,m))";
9.66 by( case_tac "is_class G C" 1);
9.67 -by( forw_inst_tac [("C","C")] cmethd_rec 2);
9.68 +by( forw_inst_tac [("C","C")] method_rec 2);
9.69 by( asm_full_simp_tac (simpset() addsimps [is_class_def]
9.70 delsimps [not_None_eq]) 2);
9.71 by( etac subcls1_induct 1);
9.72 by( atac 1);
9.73 by( Force_tac 1);
9.74 -by( forw_inst_tac [("C","C")] cmethd_rec 1);
9.75 +by( forw_inst_tac [("C","C")] method_rec 1);
9.76 by( strip_tac1 1);
9.77 by( rotate_tac ~1 1);
9.78 by( Asm_full_simp_tac 1);
9.79 @@ -300,11 +300,11 @@
9.80 by( Asm_full_simp_tac 1);
9.81 by( rewtac wf_cdecl_def);
9.82 by( Asm_full_simp_tac 1);
9.83 -val cmethd_wf_mdecl = result() RS mp;
9.84 +val method_wf_mdecl = result() RS mp;
9.85
9.86 Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wt G\\<rbrakk> \\<Longrightarrow> \
9.87 -\ \\<forall>D rT b. cmethd (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
9.88 -\ (\\<exists>D' rT' b'. cmethd (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
9.89 +\ \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
9.90 +\ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
9.91 by( etac trancl_trans_induct 1);
9.92 by( strip_tac1 2);
9.93 by( EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
9.94 @@ -312,7 +312,7 @@
9.95 by( strip_tac1 1);
9.96 by( dtac subcls1D 1);
9.97 by( strip_tac1 1);
9.98 -by( stac cmethd_rec 1);
9.99 +by( stac method_rec 1);
9.100 by( atac 1);
9.101 by( rewtac override_def);
9.102 by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
9.103 @@ -334,33 +334,33 @@
9.104
9.105 Goal
9.106 "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wt G; \
9.107 -\ cmethd (G,D) sig = Some (md, rT, b) \\<rbrakk> \
9.108 -\ \\<Longrightarrow> \\<exists>mD' rT' b'. cmethd (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
9.109 +\ method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
9.110 +\ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
9.111 by(auto_tac (claset() addSDs [widen_Class_Class]
9.112 - addDs [subcls_widen_methd,cmethd_wf_mdecl],
9.113 + addDs [subcls_widen_methd,method_wf_mdecl],
9.114 simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
9.115 qed "subtype_widen_methd";
9.116
9.117
9.118 -Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. cmethd (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> cmethd (G,D) sig = Some(D,mh,code)";
9.119 +Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
9.120 by( case_tac "is_class G C" 1);
9.121 -by( forw_inst_tac [("C","C")] cmethd_rec 2);
9.122 +by( forw_inst_tac [("C","C")] method_rec 2);
9.123 by( asm_full_simp_tac (simpset() addsimps [is_class_def]
9.124 delsimps [not_None_eq]) 2);
9.125 by (etac subcls1_induct 1);
9.126 ba 1;
9.127 by (Asm_full_simp_tac 1);
9.128 -by (stac cmethd_rec 1);
9.129 +by (stac method_rec 1);
9.130 ba 1;
9.131 by (Clarify_tac 1);
9.132 by (eres_inst_tac [("x","Da")] allE 1);
9.133 by (Clarsimp_tac 1);
9.134 by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
9.135 by (Clarify_tac 1);
9.136 - by (stac cmethd_rec 1);
9.137 + by (stac method_rec 1);
9.138 ba 1;
9.139 by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
9.140 -qed_spec_mp "cmethd_in_md";
9.141 +qed_spec_mp "method_in_md";
9.142
9.143 writeln"OK";
9.144
10.1 --- a/src/HOL/MicroJava/J/WellForm.thy Thu Nov 25 12:30:57 1999 +0100
10.2 +++ b/src/HOL/MicroJava/J/WellForm.thy Fri Nov 26 08:46:59 1999 +0100
10.3 @@ -38,7 +38,7 @@
10.4 | Some D \\<Rightarrow>
10.5 is_class G D \\<and> \\<not> G\\<turnstile>D\\<prec>C C \\<and>
10.6 (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
10.7 - cmethd(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
10.8 + method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
10.9
10.10 wf_prog :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
10.11 "wf_prog wtm G \\<equiv>
11.1 --- a/src/HOL/MicroJava/J/WellType.ML Thu Nov 25 12:30:57 1999 +0100
11.2 +++ b/src/HOL/MicroJava/J/WellType.ML Fri Nov 26 08:46:59 1999 +0100
11.3 @@ -6,7 +6,7 @@
11.4
11.5 Goalw [m_head_def]
11.6 "\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wtm G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
11.7 -\\\<exists>md' rT' b'. cmethd (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
11.8 +\\\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
11.9 by( forward_tac [widen_Class_RefT] 1);
11.10 by( etac exE 1);
11.11 by( hyp_subst_tac 1);
11.12 @@ -25,13 +25,13 @@
11.13
11.14 Goal
11.15 "\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
11.16 -\ \\<exists>T' rT' b. cmethd (G,T'') sig = Some (T',rT',b) \\<and> \
11.17 +\ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
11.18 \ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wtm G T' (sig,rT',b)";
11.19 by( dtac widen_methd 1);
11.20 by( atac 1);
11.21 by( atac 1);
11.22 by( Clarsimp_tac 1);
11.23 -by( dtac cmethd_wf_mdecl 1);
11.24 +by( dtac method_wf_mdecl 1);
11.25 by( atac 1);
11.26 by( rewtac wf_mdecl_def);
11.27 by Auto_tac;
12.1 --- a/src/HOL/MicroJava/J/WellType.thy Thu Nov 25 12:30:57 1999 +0100
12.2 +++ b/src/HOL/MicroJava/J/WellType.thy Fri Nov 26 08:46:59 1999 +0100
12.3 @@ -43,7 +43,7 @@
12.4 defs
12.5
12.6 m_head_def "m_head G t sig \\<equiv> case t of NullT \\<Rightarrow> None | ClassT C \\<Rightarrow>
12.7 - option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (cmethd (G,C) sig)"
12.8 + option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (method (G,C) sig)"
12.9
12.10 more_spec_def "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
12.11 list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
12.12 @@ -118,7 +118,7 @@
12.13
12.14 (* cf. 15.10.1 *)
12.15 FAcc "\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
12.16 - cfield (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
12.17 + field (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
12.18 E\\<turnstile>{fd}a..fn\\<Colon>fT"
12.19
12.20 (* cf. 15.25, 15.25.1 *)
13.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy Thu Nov 25 12:30:57 1999 +0100
13.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Fri Nov 26 08:46:59 1999 +0100
13.3 @@ -30,39 +30,38 @@
13.4 "exec (G, xp, hp, []) = None"
13.5
13.6 "exec (G, None, hp, (stk,loc,cn,ml,pc)#frs) =
13.7 - Some (case snd(snd(snd(the(cmethd (G,cn) ml)))) ! pc of
13.8 - LS ins \\<Rightarrow> (let (stk',loc',pc') = exec_las ins stk loc pc
13.9 + Some (case snd(snd(snd(the(method (G,cn) ml)))) ! pc of
13.10 + LS ins \\<Rightarrow> let (stk',loc',pc') = exec_las ins stk loc pc
13.11 in
13.12 - (None,hp,(stk',loc',cn,ml,pc')#frs))
13.13 + (None,hp,(stk',loc',cn,ml,pc')#frs)
13.14
13.15 - | CO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_co ins G hp stk pc
13.16 + | CO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_co ins G hp stk pc
13.17 in
13.18 - (xp',hp',(stk',loc,cn,ml,pc')#frs))
13.19 + (xp',hp',(stk',loc,cn,ml,pc')#frs)
13.20
13.21 - | MO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_mo ins hp stk pc
13.22 + | MO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_mo ins hp stk pc
13.23 in
13.24 - (xp',hp',(stk',loc,cn,ml,pc')#frs))
13.25 + (xp',hp',(stk',loc,cn,ml,pc')#frs)
13.26
13.27 - | CH ins \\<Rightarrow> (let (xp',stk',pc') = exec_ch ins G hp stk pc
13.28 + | CH ins \\<Rightarrow> let (xp',stk',pc') = exec_ch ins G hp stk pc
13.29 in
13.30 - (xp',hp,(stk',loc,cn,ml,pc')#frs))
13.31 + (xp',hp,(stk',loc,cn,ml,pc')#frs)
13.32
13.33 - | MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
13.34 + | MI ins \\<Rightarrow> let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
13.35 in
13.36 - (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
13.37 + (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs)
13.38
13.39 - | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
13.40 - (None,hp,frs'))
13.41 + | MR ins \\<Rightarrow> let frs' = exec_mr ins stk frs in (None,hp,frs')
13.42
13.43 - | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
13.44 + | OS ins \\<Rightarrow> let (stk',pc') = exec_os ins stk pc
13.45 in
13.46 - (None,hp,(stk',loc,cn,ml,pc')#frs))
13.47 + (None,hp,(stk',loc,cn,ml,pc')#frs)
13.48
13.49 - | BR ins \\<Rightarrow> (let (stk',pc') = exec_br ins stk pc
13.50 + | BR ins \\<Rightarrow> let (stk',pc') = exec_br ins stk pc
13.51 in
13.52 - (None,hp,(stk',loc,cn,ml,pc')#frs)))"
13.53 + (None,hp,(stk',loc,cn,ml,pc')#frs))"
13.54
13.55 - "exec (G, Some xp, hp, f#frs) = Some (Some xp, hp, [])"
13.56 + "exec (G, Some xp, hp, f#frs) = None"
13.57
13.58
13.59 constdefs
14.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy Thu Nov 25 12:30:57 1999 +0100
14.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy Fri Nov 26 08:46:59 1999 +0100
14.3 @@ -35,21 +35,10 @@
14.4 raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
14.5 "raise_xcpt c x \\<equiv> (if c then Some x else None)"
14.6
14.7 - heap_update :: "[xcpt option,aheap,aheap] \\<Rightarrow> aheap"
14.8 -"heap_update xp hp' hp \\<equiv> if xp=None then hp' else hp"
14.9 -
14.10 - stk_update :: "[xcpt option,opstack,opstack] \\<Rightarrow> opstack"
14.11 -"stk_update xp stk' stk \\<equiv> if xp=None then stk' else stk"
14.12 -
14.13 - xcpt_update :: "[xcpt option,'a,'a] \\<Rightarrow> 'a"
14.14 -"xcpt_update xp y' y \\<equiv> if xp=None then y' else y"
14.15 -
14.16 (** runtime state **)
14.17
14.18 types
14.19 - jvm_state = "xcpt option \\<times>
14.20 - aheap \\<times>
14.21 - frame list"
14.22 + jvm_state = "xcpt option \\<times> aheap \\<times> frame list"
14.23
14.24
14.25
14.26 @@ -57,5 +46,5 @@
14.27
14.28 constdefs
14.29 dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
14.30 -"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(cmethd(G,C) sig))"
14.31 +"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
14.32 end
15.1 --- a/src/HOL/MicroJava/JVM/Method.thy Thu Nov 25 12:30:57 1999 +0100
15.2 +++ b/src/HOL/MicroJava/JVM/Method.thy Fri Nov 26 08:46:59 1999 +0100
15.3 @@ -23,9 +23,11 @@
15.4 argsoref = take (n+1) stk;
15.5 oref = last argsoref;
15.6 xp' = raise_xcpt (oref=Null) NullPointer;
15.7 - dynT = fst(hp \\<And> (the_Addr oref));
15.8 - (dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps));
15.9 - frs' = xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] []
15.10 + dynT = fst(hp !! (the_Addr oref));
15.11 + (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
15.12 + frs' = if xp'=None
15.13 + then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
15.14 + else []
15.15 in
15.16 (xp' , frs' , drop (n+1) stk , pc+1))"
15.17
16.1 --- a/src/HOL/MicroJava/JVM/Object.thy Thu Nov 25 12:30:57 1999 +0100
16.2 +++ b/src/HOL/MicroJava/JVM/Object.thy Fri Nov 26 08:46:59 1999 +0100
16.3 @@ -21,8 +21,8 @@
16.4 (let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
16.5 oref = newref hp;
16.6 fs = init_vars (fields(G,C));
16.7 - hp' = xcpt_update xp' (hp(oref \\<mapsto> (C,fs))) hp;
16.8 - stk' = xcpt_update xp' ((Addr oref)#stk) stk
16.9 + hp' = if xp'=None then hp(oref \\<mapsto> (C,fs)) else hp;
16.10 + stk' = if xp'=None then (Addr oref)#stk else stk
16.11 in (xp' , hp' , stk' , pc+1))"
16.12
16.13
16.14 @@ -39,8 +39,8 @@
16.15 "exec_mo (Getfield F C) hp stk pc =
16.16 (let oref = hd stk;
16.17 xp' = raise_xcpt (oref=Null) NullPointer;
16.18 - (oc,fs) = hp \\<And> (the_Addr oref);
16.19 - stk' = xcpt_update xp' ((fs\\<And>(F,C))#(tl stk)) (tl stk)
16.20 + (oc,fs) = hp !! (the_Addr oref);
16.21 + stk' = if xp'=None then (fs!!(F,C))#(tl stk) else tl stk
16.22 in
16.23 (xp' , hp , stk' , pc+1))"
16.24
16.25 @@ -48,8 +48,8 @@
16.26 (let (fval,oref)= (hd stk, hd(tl stk));
16.27 xp' = raise_xcpt (oref=Null) NullPointer;
16.28 a = the_Addr oref;
16.29 - (oc,fs) = hp \\<And> a;
16.30 - hp' = xcpt_update xp' (hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval)))) hp
16.31 + (oc,fs) = hp !! a;
16.32 + hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp
16.33 in
16.34 (xp' , hp' , tl (tl stk), pc+1))"
16.35
16.36 @@ -66,7 +66,7 @@
16.37 "exec_ch (Checkcast C) G hp stk pc =
16.38 (let oref = hd stk;
16.39 xp' = raise_xcpt (\\<not> cast_ok G (Class C) hp oref) ClassCast;
16.40 - stk' = xcpt_update xp' stk (tl stk)
16.41 + stk' = if xp'=None then stk else tl stk
16.42 in
16.43 (xp' , stk' , pc+1))"
16.44
17.1 --- a/src/HOL/MicroJava/JVM/Store.thy Thu Nov 25 12:30:57 1999 +0100
17.2 +++ b/src/HOL/MicroJava/JVM/Store.thy Fri Nov 26 08:46:59 1999 +0100
17.3 @@ -12,9 +12,9 @@
17.4 Store = Conform +
17.5
17.6 syntax
17.7 - value :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ \\<And> _")
17.8 + map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ !! _")
17.9 translations
17.10 - "t \\<And> x" == "the (t x)"
17.11 + "t !! x" == "the (t x)"
17.12
17.13 constdefs
17.14 newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"