Minor mods.

--- a/src/HOL/MicroJava/BV/BVSpec.ML	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.ML	Thu Nov 25 12:01:28 1999 +0100
@@ -4,8 +4,6 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-Addsimps [wt_MR_def];
-
 Goalw [wt_jvm_prog_def] "wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)";
 by(Blast_tac 1);
 qed "wt_jvm_progD";

--- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Nov 25 12:01:28 1999 +0100
@@ -148,7 +148,7 @@
 consts
  wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
 primrec
-"wt_MI (Invokevirtual mn fpTs) G phi max_pc pc =
+"wt_MI (Invoke mn fpTs) G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
          pc+1 < max_pc \\<and>
@@ -158,9 +158,10 @@
          (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
          G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
 
-constdefs
- wt_MR	:: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
-"wt_MR G rT phi pc \\<equiv>
+consts
+ wt_MR	:: "[meth_ret,jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
+primrec
+  "wt_MR Return G rT phi pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
@@ -175,7 +176,7 @@
 	| MO  ins \\<Rightarrow> wt_MO ins G phi max_pc pc
 	| CH  ins \\<Rightarrow> wt_CH ins G phi max_pc pc
 	| MI  ins \\<Rightarrow> wt_MI ins G phi max_pc pc
-	| MR      \\<Rightarrow> wt_MR     G rT phi pc
+	| MR  ins \\<Rightarrow> wt_MR ins G rT phi pc
 	| OS  ins \\<Rightarrow> wt_OS ins G phi max_pc pc
 	| BR  ins \\<Rightarrow> wt_BR ins G phi max_pc pc"
 

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

--- a/src/HOL/MicroJava/BV/Correct.ML	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML	Thu Nov 25 12:01:28 1999 +0100
@@ -233,7 +233,7 @@
 (** hconf **)
 
 
-Goal "hp x = None \\<longrightarrow> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp(newref hp\\<mapsto>obj)\\<turnstile>\\<surd>";
+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>";
 by (asm_full_simp_tac (simpset() addsplits [split_split] 
 				 addsimps [hconf_def]) 1);
  by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1);
@@ -241,7 +241,7 @@
 
 
 Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \
-\ 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>";
+\ 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>";
 by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1);
 by (fast_tac (claset() addIs 
         [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update]

--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Nov 25 12:01:28 1999 +0100
@@ -35,7 +35,7 @@
 	 in
          (\\<exists>rT maxl ins.
          cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
-	 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invokevirtual mn pTs) \\<and>
+	 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invoke mn pTs) \\<and>
          (mn,pTs) = ml0 \\<and> 
          (\\<exists>apTs D ST'.
          fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\<and>
@@ -49,6 +49,7 @@
 
 constdefs
  correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool"
+                  ("_,_\\<turnstile>JVM _\\<surd>"  [51,51] 50)
 "correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs).
    case xp of
      None \\<Rightarrow> (case frs of
@@ -57,7 +58,7 @@
 		         in
                          \\<exists>rT maxl ins.
                          cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
-		         G,hp\\<turnstile>\\<surd> \\<and> 
+		         G\\<turnstile>h hp\\<surd> \\<and> 
 			 correct_frame G hp ((phi C ml) ! pc) maxl ins f \\<and> 
 		         correct_frames G hp phi rT C ml fs))
    | Some x \\<Rightarrow> True" 

--- a/src/HOL/MicroJava/J/Conform.ML	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/J/Conform.ML	Thu Nov 25 12:01:28 1999 +0100
@@ -210,11 +210,11 @@
 
 section "hconf";
 
-Goalw [hconf_def] "\\<lbrakk>G,h\\<turnstile>\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
+Goalw [hconf_def] "\\<lbrakk>G\\<turnstile>h h\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
 by (Fast_tac 1);
 qed "hconfD";
 
-Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G,h\\<turnstile>\\<surd>";
+Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G\\<turnstile>h h\\<surd>";
 by (Fast_tac 1);
 qed "hconfI";
 
@@ -222,7 +222,7 @@
 section "conforms";
 
 val conforms_heapD = prove_goalw thy [conforms_def]
-	"(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>\\<surd>"
+	"(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G\\<turnstile>h h\\<surd>"
 	(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
 
 val conforms_localD = prove_goalw thy [conforms_def]
@@ -230,12 +230,12 @@
 	cut_facts_tac prems 1, Asm_full_simp_tac 1]);
 
 val conformsI = prove_goalw thy [conforms_def] 
-"\\<lbrakk>G,h\\<turnstile>\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
+"\\<lbrakk>G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
 	cut_facts_tac prems 1,
 	Simp_tac 1,
 	Auto_tac]);
 
-Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G,h'\\<turnstile>\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
+Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
 by( fast_tac (HOL_cs addDs [conforms_localD] 
   addSEs [conformsI, lconf_hext]) 1);
 qed "conforms_hext";

--- a/src/HOL/MicroJava/J/Conform.thy	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Thu Nov 25 12:01:28 1999 +0100
@@ -23,10 +23,10 @@
   oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool"      ("_,_\\<turnstile>_\\<surd>"     [51,51,51]    50)
  "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))"
 
-  hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_,_\\<turnstile>\\<surd>"      [51,51]       50)
- "G,h\\<turnstile>\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
+  hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
+ "G\\<turnstile>h h\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
 
   conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
- "s\\<Colon>\\<preceq>E \\<equiv> prg E,heap s\\<turnstile>\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
+ "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
 
 end

--- a/src/HOL/MicroJava/J/Type.thy	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/J/Type.thy	Thu Nov 25 12:01:28 1999 +0100
@@ -25,7 +25,7 @@
 datatype ref_ty		(* reference type, cf. 4.3 *)
 	= NullT		(* null type, cf. 4.1 *)
 	| ClassT cname	(* class type *)
-and ty    		(* any type, cf. 4.1 *)
+datatype ty    		(* any type, cf. 4.1 *)
 	= PrimT prim_ty	(* primitive type *)
 	| RefT  ref_ty	(* reference type *)
 

--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Thu Nov 25 12:01:28 1999 +0100
@@ -14,7 +14,7 @@
         | MO manipulate_object	
 	| CH check_object	
 	| MI meth_inv		
-	| MR
+	| MR meth_ret
 	| OS op_stack		
 	| BR branch
 
@@ -51,7 +51,7 @@
 		in
 		(xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
 
-    | MR     \\<Rightarrow> (let frs' = exec_mr stk frs in
+    | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in
 		(None,hp,frs'))
 
     | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc

--- a/src/HOL/MicroJava/JVM/Method.ML	Wed Nov 24 13:36:14 1999 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      HOL/MicroJava/JVM/Method.ML
-    ID:         $Id$
-    Author:     Cornelia Pusch
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-Addsimps [exec_mr_def];

--- a/src/HOL/MicroJava/JVM/Method.thy	Wed Nov 24 13:36:14 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Method.thy	Thu Nov 25 12:01:28 1999 +0100
@@ -12,13 +12,13 @@
 
 datatype 
  meth_inv = 
-   Invokevirtual   mname (ty list)      (** inv. instance meth of an object **)
+   Invoke mname (ty list)      (** inv. instance meth of an object **)
  
 consts
  exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count] 
 		\\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)" 
 primrec
- "exec_mi (Invokevirtual mn ps) G hp stk pc =
+ "exec_mi (Invoke mn ps) G hp stk pc =
 	(let n		= length ps;
 	     argsoref	= take (n+1) stk;
 	     oref	= last argsoref;
@@ -30,11 +30,14 @@
 	 (xp' , frs' , drop (n+1) stk , pc+1))"
 
 
-constdefs
- exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
-"exec_mr stk0 frs \\<equiv>
-	 (let val			= hd stk0;
-	      (stk,loc,cn,met,pc) = hd frs
+datatype 
+ meth_ret = Return
+ 
+consts
+ exec_mr :: "[meth_ret,opstack,frame list] \\<Rightarrow> frame list"
+primrec
+  "exec_mr Return stk0 frs =
+	 (let val = hd stk0; (stk,loc,cn,met,pc) = hd frs
 	  in
 	  (val#stk,loc,cn,met,pc)#tl frs)"