Various little changes like cmethd -> method and cfield -> field.
authornipkow
Fri Nov 26 08:46:59 1999 +0100 (1999-11-26)
changeset 80346fc37b5c5e98
parent 8033 325b8e754523
child 8035 84c5ce912b43
Various little changes like cmethd -> method and cfield -> field.
src/HOL/MicroJava/BV/BVSpec.ML
src/HOL/MicroJava/BV/BVSpec.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/JTypeSafe.ML
src/HOL/MicroJava/J/TypeRel.ML
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellForm.ML
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.ML
src/HOL/MicroJava/J/WellType.thy
src/HOL/MicroJava/JVM/JVMExec.thy
src/HOL/MicroJava/JVM/JVMState.thy
src/HOL/MicroJava/JVM/Method.thy
src/HOL/MicroJava/JVM/Object.thy
src/HOL/MicroJava/JVM/Store.thy
     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 -		in
   13.10 -		(None,hp,(stk',loc',cn,ml,pc')#frs))
   13.11 -
   13.12 -    | CO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_co ins G hp stk pc
   13.13 +   Some (case snd(snd(snd(the(method (G,cn) ml)))) ! pc of
   13.14 +      LS ins \\<Rightarrow> let (stk',loc',pc') = exec_las ins stk loc pc
   13.15  		in
   13.16 -		(xp',hp',(stk',loc,cn,ml,pc')#frs))	    
   13.17 +		(None,hp,(stk',loc',cn,ml,pc')#frs)
   13.18  
   13.19 -    | MO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_mo ins hp stk pc
   13.20 +    | CO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_co ins G hp stk pc
   13.21  		in
   13.22 -		(xp',hp',(stk',loc,cn,ml,pc')#frs))	
   13.23 +		(xp',hp',(stk',loc,cn,ml,pc')#frs)	    
   13.24  
   13.25 -    | CH ins \\<Rightarrow> (let (xp',stk',pc') = exec_ch ins G hp stk pc
   13.26 +    | MO ins \\<Rightarrow> let (xp',hp',stk',pc') = exec_mo ins hp stk pc
   13.27  		in
   13.28 -		(xp',hp,(stk',loc,cn,ml,pc')#frs))
   13.29 +		(xp',hp',(stk',loc,cn,ml,pc')#frs)
   13.30  
   13.31 -    | MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc 
   13.32 +    | CH ins \\<Rightarrow> let (xp',stk',pc') = exec_ch ins G hp stk pc
   13.33  		in
   13.34 -		(xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
   13.35 +		(xp',hp,(stk',loc,cn,ml,pc')#frs)
   13.36  
   13.37 -    | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
   13.38 -		(None,hp,frs'))
   13.39 +    | MI ins \\<Rightarrow> let (xp',frs',stk',pc') = exec_mi ins G hp stk pc 
   13.40 +		in
   13.41 +		(xp',hp,frs'@(stk',loc,cn,ml,pc')#frs)
   13.42 +
   13.43 +    | MR ins \\<Rightarrow> let frs' = exec_mr ins stk frs in (None,hp,frs')
   13.44  
   13.45 -    | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
   13.46 +    | OS ins \\<Rightarrow> let (stk',pc') = exec_os ins stk pc
   13.47  		in
   13.48 -		(None,hp,(stk',loc,cn,ml,pc')#frs))
   13.49 +		(None,hp,(stk',loc,cn,ml,pc')#frs)
   13.50  
   13.51 -    | BR ins \\<Rightarrow> (let (stk',pc') = exec_br ins stk pc
   13.52 +    | BR ins \\<Rightarrow> let (stk',pc') = exec_br ins stk pc
   13.53  		in
   13.54 -		(None,hp,(stk',loc,cn,ml,pc')#frs)))"
   13.55 +		(None,hp,(stk',loc,cn,ml,pc')#frs))"
   13.56  
   13.57 - "exec (G, Some xp, hp, f#frs) = Some (Some xp, hp, [])"
   13.58 + "exec (G, Some xp, hp, f#frs) = None"
   13.59  
   13.60  
   13.61  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"