Minor mods.
authornipkow
Thu Nov 25 12:01:28 1999 +0100 (1999-11-25)
changeset 80321eaae1a2f8ff
parent 8031 826c6222cca2
child 8033 325b8e754523
Minor mods.
src/HOL/MicroJava/BV/BVSpec.ML
src/HOL/MicroJava/BV/BVSpec.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
src/HOL/MicroJava/BV/Correct.ML
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/J/Conform.ML
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/MicroJava/JVM/JVMExec.thy
src/HOL/MicroJava/JVM/Method.ML
src/HOL/MicroJava/JVM/Method.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVSpec.ML	Wed Nov 24 13:36:14 1999 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVSpec.ML	Thu Nov 25 12:01:28 1999 +0100
     1.3 @@ -4,8 +4,6 @@
     1.4      Copyright   1999 Technische Universitaet Muenchen
     1.5  *)
     1.6  
     1.7 -Addsimps [wt_MR_def];
     1.8 -
     1.9  Goalw [wt_jvm_prog_def] "wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)";
    1.10  by(Blast_tac 1);
    1.11  qed "wt_jvm_progD";
     2.1 --- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Nov 24 13:36:14 1999 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Nov 25 12:01:28 1999 +0100
     2.3 @@ -148,7 +148,7 @@
     2.4  consts
     2.5   wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
     2.6  primrec
     2.7 -"wt_MI (Invokevirtual mn fpTs) G phi max_pc pc =
     2.8 +"wt_MI (Invoke mn fpTs) G phi max_pc pc =
     2.9  	(let (ST,LT) = phi ! pc
    2.10  	 in
    2.11           pc+1 < max_pc \\<and>
    2.12 @@ -158,9 +158,10 @@
    2.13           (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
    2.14           G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
    2.15  
    2.16 -constdefs
    2.17 - wt_MR	:: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
    2.18 -"wt_MR G rT phi pc \\<equiv>
    2.19 +consts
    2.20 + wt_MR	:: "[meth_ret,jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
    2.21 +primrec
    2.22 +  "wt_MR Return G rT phi pc =
    2.23  	(let (ST,LT) = phi ! pc
    2.24  	 in
    2.25  	 (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
    2.26 @@ -175,7 +176,7 @@
    2.27  	| MO  ins \\<Rightarrow> wt_MO ins G phi max_pc pc
    2.28  	| CH  ins \\<Rightarrow> wt_CH ins G phi max_pc pc
    2.29  	| MI  ins \\<Rightarrow> wt_MI ins G phi max_pc pc
    2.30 -	| MR      \\<Rightarrow> wt_MR     G rT phi pc
    2.31 +	| MR  ins \\<Rightarrow> wt_MR ins G rT phi pc
    2.32  	| OS  ins \\<Rightarrow> wt_OS ins G phi max_pc pc
    2.33  	| BR  ins \\<Rightarrow> wt_BR ins G phi max_pc pc"
    2.34  
     3.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Wed Nov 24 13:36:14 1999 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Thu Nov 25 12:01:28 1999 +0100
     3.3 @@ -10,7 +10,7 @@
     3.4  Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
     3.5  "\\<lbrakk> wt_jvm_prog G phi; \
     3.6  \   cmethd (G,C) sig = Some (C,rT,maxl,ins); \
     3.7 -\   correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
     3.8 +\   G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
     3.9  \\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
    3.10  by (Asm_full_simp_tac 1);
    3.11  by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1);
    3.12 @@ -28,8 +28,8 @@
    3.13  \  ins!pc = LS(Load idx); \
    3.14  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
    3.15  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
    3.16 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
    3.17 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
    3.18 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
    3.19 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
    3.20  by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
    3.21  	approx_loc_imp_approx_loc_sup] 
    3.22  	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
    3.23 @@ -42,8 +42,8 @@
    3.24  \  ins!pc = LS(Store idx); \
    3.25  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
    3.26  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
    3.27 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
    3.28 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
    3.29 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
    3.30 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
    3.31  by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
    3.32  	addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]
    3.33  	addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1);
    3.34 @@ -60,8 +60,8 @@
    3.35  \  ins!pc = LS(Bipush i); \
    3.36  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
    3.37  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
    3.38 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
    3.39 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
    3.40 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
    3.41 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
    3.42  by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
    3.43  	addss (simpset() addsimps [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
    3.44  qed "Bipush_correct";
    3.45 @@ -84,8 +84,8 @@
    3.46  \  ins!pc = LS Aconst_null; \
    3.47  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
    3.48  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
    3.49 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
    3.50 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
    3.51 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
    3.52 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
    3.53  by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
    3.54  	addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
    3.55  qed "Aconst_null_correct";
    3.56 @@ -96,8 +96,8 @@
    3.57  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
    3.58  \  ins!pc = LS ls_com; \
    3.59  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
    3.60 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
    3.61 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
    3.62 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
    3.63 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
    3.64  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
    3.65    ba 1;
    3.66   ba 1;
    3.67 @@ -131,8 +131,8 @@
    3.68  \  ins!pc = CH (Checkcast D); \
    3.69  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
    3.70  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
    3.71 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
    3.72 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
    3.73 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
    3.74 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
    3.75  by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,
    3.76  		xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
    3.77  by (fast_tac (claset() addDs [approx_stk_Cons_lemma] 
    3.78 @@ -146,8 +146,8 @@
    3.79  \  cmethd (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 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
    3.83 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
    3.84 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
    3.85 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
    3.86  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
    3.87    ba 1;
    3.88   ba 1;
    3.89 @@ -164,8 +164,8 @@
    3.90  \  ins!pc = MO (Getfield F D); \
    3.91  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
    3.92  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
    3.93 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
    3.94 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
    3.95 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
    3.96 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
    3.97  by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
    3.98  by (Clarify_tac 1);
    3.99  by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
   3.100 @@ -203,8 +203,8 @@
   3.101  \  ins!pc = MO (Putfield F D); \
   3.102  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.103  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
   3.104 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.105 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.106 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.107 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.108  by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
   3.109  by (Clarify_tac 1);
   3.110  by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
   3.111 @@ -231,8 +231,8 @@
   3.112  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.113  \  ins!pc = MO mo_com; \
   3.114  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.115 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.116 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.117 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.118 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.119  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   3.120    ba 1;
   3.121   ba 1;
   3.122 @@ -250,12 +250,12 @@
   3.123  
   3.124  Goal
   3.125  "\\<lbrakk> wf_prog wt G; \
   3.126 -\  cmethd (G,C) sig = Some (C,rT,maxl,ins); \
   3.127 +\  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.128  \  ins!pc = CO(New cl_idx); \
   3.129 -\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
   3.130 -\  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
   3.131 -\  correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
   3.132 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.133 +\  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.134 +\  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.135 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.136 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.137  by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
   3.138  		approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
   3.139  		approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
   3.140 @@ -271,8 +271,8 @@
   3.141  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.142  \  ins!pc = CO co_com; \
   3.143  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.144 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.145 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.146 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.147 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.148  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   3.149    ba 1;
   3.150   ba 1;
   3.151 @@ -287,11 +287,11 @@
   3.152  Goal
   3.153  "\\<lbrakk> wt_jvm_prog G phi; \
   3.154  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.155 -\  ins ! pc = MI(Invokevirtual mn pTs); \
   3.156 +\  ins ! pc = MI(Invoke mn pTs); \
   3.157  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.158  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.159 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.160 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.161 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.162 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.163  by(forward_tac [wt_jvm_progD] 1);
   3.164  by(etac exE 1);
   3.165  by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1 
   3.166 @@ -361,20 +361,20 @@
   3.167  by (fast_tac (claset()
   3.168         addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
   3.169         addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1);
   3.170 -qed "Invokevirtual_correct";
   3.171 +qed "Invoke_correct";
   3.172  
   3.173  Goal
   3.174  "\\<lbrakk> wt_jvm_prog G phi; \
   3.175  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.176  \  ins!pc = MI mi_com; \
   3.177  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.178 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.179 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.180 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.181 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.182  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   3.183    ba 1;
   3.184   ba 1;
   3.185  by (exhaust_tac "mi_com" 1);
   3.186 -by (ALLGOALS (fast_tac (claset() addIs [Invokevirtual_correct])));
   3.187 +by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
   3.188  qed "MI_correct";
   3.189  
   3.190  (****** MR ******)
   3.191 @@ -395,11 +395,11 @@
   3.192  Goal
   3.193  "\\<lbrakk> wt_jvm_prog G phi; \
   3.194  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.195 -\  ins ! pc = MR; \
   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 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.200 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.201 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.202 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.203  by (asm_full_simp_tac (simpset() addsimps defs1) 1);
   3.204  by (Clarify_tac 1);
   3.205  by (asm_full_simp_tac (simpset() addsimps defs1) 1);
   3.206 @@ -424,13 +424,14 @@
   3.207  Goal
   3.208  "\\<lbrakk> wt_jvm_prog G phi; \
   3.209  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.210 -\  ins!pc = MR; \
   3.211 +\  ins!pc = MR mr; \
   3.212  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.213 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.214 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.215 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.216 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.217  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   3.218    ba 1;
   3.219   ba 1;
   3.220 +by (exhaust_tac "mr" 1);
   3.221  by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
   3.222  qed "MR_correct";
   3.223  
   3.224 @@ -441,8 +442,8 @@
   3.225  \  ins ! pc = BR(Goto branch); \
   3.226  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.227  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.228 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.229 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.230 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.231 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.232  by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
   3.233  	addss (simpset() addsimps defs1)) 1);
   3.234  qed "Goto_correct";
   3.235 @@ -454,8 +455,8 @@
   3.236  \  ins!pc = BR(Ifcmpeq branch); \
   3.237  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.238  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.239 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.240 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.241 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.242 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.243  by (fast_tac (claset() addDs [approx_stk_Cons_lemma] 
   3.244  	addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
   3.245  qed "Ifiacmpeq_correct";
   3.246 @@ -466,8 +467,8 @@
   3.247  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.248  \  ins!pc = BR br_com; \
   3.249  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.250 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.251 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.252 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.253 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.254  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   3.255    ba 1;
   3.256   ba 1;
   3.257 @@ -485,8 +486,8 @@
   3.258  \  ins ! pc = OS Pop; \
   3.259  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.260  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
   3.261 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.262 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.263 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.264 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.265  by (fast_tac (claset() addDs [approx_stk_Cons_lemma] 
   3.266  	addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
   3.267  qed "Pop_correct";
   3.268 @@ -498,8 +499,8 @@
   3.269  \  ins ! pc = OS Dup; \
   3.270  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.271  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
   3.272 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.273 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.274 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.275 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.276  by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
   3.277  	addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
   3.278  	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
   3.279 @@ -512,8 +513,8 @@
   3.280  \  ins ! pc = OS Dup_x1; \
   3.281  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.282  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
   3.283 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.284 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.285 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.286 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.287  by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
   3.288  	addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
   3.289  	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
   3.290 @@ -525,8 +526,8 @@
   3.291  \  ins ! pc = OS Dup_x2; \
   3.292  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.293  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
   3.294 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.295 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.296 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.297 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.298  by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
   3.299  	addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
   3.300  	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
   3.301 @@ -538,8 +539,8 @@
   3.302  \  ins ! pc = OS Swap; \
   3.303  \  wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
   3.304  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
   3.305 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.306 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.307 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.308 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.309  by (fast_tac (claset() addDs [approx_stk_Cons_lemma] 
   3.310  	addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
   3.311  	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
   3.312 @@ -550,8 +551,8 @@
   3.313  \  cmethd (G,C) ml = Some (C,rT,maxl,ins); \
   3.314  \  ins!pc = OS os_com; \
   3.315  \  Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
   3.316 -\  correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
   3.317 -\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
   3.318 +\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \\<rbrakk> \
   3.319 +\\\<Longrightarrow> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.320  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   3.321    ba 1;
   3.322   ba 1;
   3.323 @@ -563,15 +564,15 @@
   3.324  (** Main **)
   3.325  
   3.326  Goalw [correct_state_def,Let_def]
   3.327 - "correct_state G phi (None,hp,(stk,loc,C,sig,pc)#fs) \
   3.328 -\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) sig = Some(C,meth)";
   3.329 + "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\<surd> \
   3.330 +\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) ml = Some(C,meth)";
   3.331  by(Asm_full_simp_tac 1);
   3.332  by(Blast_tac 1);
   3.333  qed "correct_state_impl_Some_cmethd";
   3.334  
   3.335  Goal
   3.336 -"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; correct_state G phi state\\<rbrakk> \
   3.337 -\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> correct_state G phi state'";
   3.338 +"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \
   3.339 +\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
   3.340  by(split_all_tac 1);
   3.341  by(rename_tac "xp hp frs" 1);
   3.342  by (exhaust_tac "xp" 1);
   3.343 @@ -596,9 +597,8 @@
   3.344  qed_spec_mp "exec_lemma";
   3.345  
   3.346  Goal
   3.347 -"\\<lbrakk> wt_jvm_prog G phi; \
   3.348 -\  correct_state G phi (xp,hp,frs); xp=None; frs\\<noteq>[] \\<rbrakk> \
   3.349 -\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs') \\<and> correct_state G phi (xp',hp',frs')";
   3.350 +"\\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[] \\<rbrakk> \
   3.351 +\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec(G,xp,hp,frs) = Some(xp',hp',frs') \\<and> G,phi \\<turnstile>JVM (xp',hp',frs')\\<surd>";
   3.352  by (dres_inst_tac [("G","G"),("hp","hp")]  exec_lemma 1);
   3.353  ba 1;
   3.354  by (fast_tac (claset() addIs [BV_correct_1]) 1);
   3.355 @@ -606,8 +606,7 @@
   3.356  (*******)
   3.357  
   3.358  Goalw [exec_all_def]
   3.359 -"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \
   3.360 -\ \\<Longrightarrow> correct_state G phi s \\<longrightarrow> correct_state G phi t";
   3.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>";
   3.362  be rtrancl_induct 1;
   3.363   by (Simp_tac 1);
   3.364  by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1);
   3.365 @@ -615,7 +614,7 @@
   3.366  
   3.367  
   3.368  Goal
   3.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> \
   3.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> \
   3.371  \ \\<Longrightarrow>  approx_stk G hp stk (fst (((phi  cn)  ml) ! pc)) \\<and> approx_loc G hp loc (snd (((phi  cn)  ml) ! pc)) ";
   3.372  bd BV_correct 1;
   3.373  ba 1;
     4.1 --- a/src/HOL/MicroJava/BV/Correct.ML	Wed Nov 24 13:36:14 1999 +0100
     4.2 +++ b/src/HOL/MicroJava/BV/Correct.ML	Thu Nov 25 12:01:28 1999 +0100
     4.3 @@ -233,7 +233,7 @@
     4.4  (** hconf **)
     4.5  
     4.6  
     4.7 -Goal "hp x = None \\<longrightarrow> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp(newref hp\\<mapsto>obj)\\<turnstile>\\<surd>";
     4.8 +Goal "hp x = None \\<longrightarrow> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G\\<turnstile>h hp(newref hp\\<mapsto>obj)\\<surd>";
     4.9  by (asm_full_simp_tac (simpset() addsplits [split_split] 
    4.10  				 addsimps [hconf_def]) 1);
    4.11   by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1);
    4.12 @@ -241,7 +241,7 @@
    4.13  
    4.14  
    4.15  Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \
    4.16 -\ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<turnstile>\\<surd>";
    4.17 +\ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G\\<turnstile>h hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<surd>";
    4.18  by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1);
    4.19  by (fast_tac (claset() addIs 
    4.20          [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update]
     5.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Wed Nov 24 13:36:14 1999 +0100
     5.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Nov 25 12:01:28 1999 +0100
     5.3 @@ -35,7 +35,7 @@
     5.4  	 in
     5.5           (\\<exists>rT maxl ins.
     5.6           cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
     5.7 -	 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invokevirtual mn pTs) \\<and>
     5.8 +	 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invoke mn pTs) \\<and>
     5.9           (mn,pTs) = ml0 \\<and> 
    5.10           (\\<exists>apTs D ST'.
    5.11           fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\<and>
    5.12 @@ -49,6 +49,7 @@
    5.13  
    5.14  constdefs
    5.15   correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool"
    5.16 +                  ("_,_\\<turnstile>JVM _\\<surd>"  [51,51] 50)
    5.17  "correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs).
    5.18     case xp of
    5.19       None \\<Rightarrow> (case frs of
    5.20 @@ -57,7 +58,7 @@
    5.21  		         in
    5.22                           \\<exists>rT maxl ins.
    5.23                           cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
    5.24 -		         G,hp\\<turnstile>\\<surd> \\<and> 
    5.25 +		         G\\<turnstile>h hp\\<surd> \\<and> 
    5.26  			 correct_frame G hp ((phi C ml) ! pc) maxl ins f \\<and> 
    5.27  		         correct_frames G hp phi rT C ml fs))
    5.28     | Some x \\<Rightarrow> True" 
     6.1 --- a/src/HOL/MicroJava/J/Conform.ML	Wed Nov 24 13:36:14 1999 +0100
     6.2 +++ b/src/HOL/MicroJava/J/Conform.ML	Thu Nov 25 12:01:28 1999 +0100
     6.3 @@ -210,11 +210,11 @@
     6.4  
     6.5  section "hconf";
     6.6  
     6.7 -Goalw [hconf_def] "\\<lbrakk>G,h\\<turnstile>\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
     6.8 +Goalw [hconf_def] "\\<lbrakk>G\\<turnstile>h h\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
     6.9  by (Fast_tac 1);
    6.10  qed "hconfD";
    6.11  
    6.12 -Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G,h\\<turnstile>\\<surd>";
    6.13 +Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G\\<turnstile>h h\\<surd>";
    6.14  by (Fast_tac 1);
    6.15  qed "hconfI";
    6.16  
    6.17 @@ -222,7 +222,7 @@
    6.18  section "conforms";
    6.19  
    6.20  val conforms_heapD = prove_goalw thy [conforms_def]
    6.21 -	"(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>\\<surd>"
    6.22 +	"(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G\\<turnstile>h h\\<surd>"
    6.23  	(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
    6.24  
    6.25  val conforms_localD = prove_goalw thy [conforms_def]
    6.26 @@ -230,12 +230,12 @@
    6.27  	cut_facts_tac prems 1, Asm_full_simp_tac 1]);
    6.28  
    6.29  val conformsI = prove_goalw thy [conforms_def] 
    6.30 -"\\<lbrakk>G,h\\<turnstile>\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
    6.31 +"\\<lbrakk>G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
    6.32  	cut_facts_tac prems 1,
    6.33  	Simp_tac 1,
    6.34  	Auto_tac]);
    6.35  
    6.36 -Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G,h'\\<turnstile>\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
    6.37 +Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
    6.38  by( fast_tac (HOL_cs addDs [conforms_localD] 
    6.39    addSEs [conformsI, lconf_hext]) 1);
    6.40  qed "conforms_hext";
     7.1 --- a/src/HOL/MicroJava/J/Conform.thy	Wed Nov 24 13:36:14 1999 +0100
     7.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Thu Nov 25 12:01:28 1999 +0100
     7.3 @@ -23,10 +23,10 @@
     7.4    oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool"      ("_,_\\<turnstile>_\\<surd>"     [51,51,51]    50)
     7.5   "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))"
     7.6  
     7.7 -  hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_,_\\<turnstile>\\<surd>"      [51,51]       50)
     7.8 - "G,h\\<turnstile>\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
     7.9 +  hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
    7.10 + "G\\<turnstile>h h\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
    7.11  
    7.12    conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
    7.13 - "s\\<Colon>\\<preceq>E \\<equiv> prg E,heap s\\<turnstile>\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
    7.14 + "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
    7.15  
    7.16  end
     8.1 --- a/src/HOL/MicroJava/J/Type.thy	Wed Nov 24 13:36:14 1999 +0100
     8.2 +++ b/src/HOL/MicroJava/J/Type.thy	Thu Nov 25 12:01:28 1999 +0100
     8.3 @@ -25,7 +25,7 @@
     8.4  datatype ref_ty		(* reference type, cf. 4.3 *)
     8.5  	= NullT		(* null type, cf. 4.1 *)
     8.6  	| ClassT cname	(* class type *)
     8.7 -and ty    		(* any type, cf. 4.1 *)
     8.8 +datatype ty    		(* any type, cf. 4.1 *)
     8.9  	= PrimT prim_ty	(* primitive type *)
    8.10  	| RefT  ref_ty	(* reference type *)
    8.11  
     9.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Nov 24 13:36:14 1999 +0100
     9.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Thu Nov 25 12:01:28 1999 +0100
     9.3 @@ -14,7 +14,7 @@
     9.4          | MO manipulate_object	
     9.5  	| CH check_object	
     9.6  	| MI meth_inv		
     9.7 -	| MR
     9.8 +	| MR meth_ret
     9.9  	| OS op_stack		
    9.10  	| BR branch
    9.11  
    9.12 @@ -51,7 +51,7 @@
    9.13  		in
    9.14  		(xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
    9.15  
    9.16 -    | MR     \\<Rightarrow> (let frs' = exec_mr stk frs in
    9.17 +    | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
    9.18  		(None,hp,frs'))
    9.19  
    9.20      | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
    10.1 --- a/src/HOL/MicroJava/JVM/Method.ML	Wed Nov 24 13:36:14 1999 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,7 +0,0 @@
    10.4 -(*  Title:      HOL/MicroJava/JVM/Method.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Cornelia Pusch
    10.7 -    Copyright   1999 Technische Universitaet Muenchen
    10.8 -*)
    10.9 -
   10.10 -Addsimps [exec_mr_def];
    11.1 --- a/src/HOL/MicroJava/JVM/Method.thy	Wed Nov 24 13:36:14 1999 +0100
    11.2 +++ b/src/HOL/MicroJava/JVM/Method.thy	Thu Nov 25 12:01:28 1999 +0100
    11.3 @@ -12,13 +12,13 @@
    11.4  
    11.5  datatype 
    11.6   meth_inv = 
    11.7 -   Invokevirtual   mname (ty list)      (** inv. instance meth of an object **)
    11.8 +   Invoke mname (ty list)      (** inv. instance meth of an object **)
    11.9   
   11.10  consts
   11.11   exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count] 
   11.12  		\\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)" 
   11.13  primrec
   11.14 - "exec_mi (Invokevirtual mn ps) G hp stk pc =
   11.15 + "exec_mi (Invoke mn ps) G hp stk pc =
   11.16  	(let n		= length ps;
   11.17  	     argsoref	= take (n+1) stk;
   11.18  	     oref	= last argsoref;
   11.19 @@ -30,11 +30,14 @@
   11.20  	 (xp' , frs' , drop (n+1) stk , pc+1))"
   11.21  
   11.22  
   11.23 -constdefs
   11.24 - exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
   11.25 -"exec_mr stk0 frs \\<equiv>
   11.26 -	 (let val			= hd stk0;
   11.27 -	      (stk,loc,cn,met,pc) = hd frs
   11.28 +datatype 
   11.29 + meth_ret = Return
   11.30 + 
   11.31 +consts
   11.32 + exec_mr :: "[meth_ret,opstack,frame list] \\<Rightarrow> frame list"
   11.33 +primrec
   11.34 +  "exec_mr Return stk0 frs =
   11.35 +	 (let val = hd stk0; (stk,loc,cn,met,pc) = hd frs
   11.36  	  in
   11.37  	  (val#stk,loc,cn,met,pc)#tl frs)"
   11.38