# HG changeset patch
# User oheimb
# Date 978471677 -3600
# Node ID 08e1610c1dcb7220ad5e3ad9d3e3b82f4f3a49dd
# Parent  cd1a2bee55492d443742c18f681d5ecdf29fe8a8
added type annotation to Call

diff -r cd1a2bee5549 -r 08e1610c1dcb src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Jan 02 22:41:17 2001 +0100
@@ -18,7 +18,7 @@
 
 lemma wt_jvm_prog_impl_wt_instr_cor:
   "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); 
-      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+      G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
   ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
 apply (unfold correct_state_def Let_def correct_frame_def)
 apply simp
@@ -31,8 +31,8 @@
     ins!pc = Load idx; 
     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
-    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+    G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (rule approx_loc_imp_approx_val_sup)
@@ -47,8 +47,8 @@
   ins!pc = Store idx;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc;
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |]
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (blast intro: approx_stk_imp_approx_stk_sup)
@@ -58,7 +58,7 @@
 
 
 lemma conf_Intg_Integer [iff]:
-  "G,h \<turnstile> Intg i ::\<preceq> PrimT Integer"
+  "G,h \\<turnstile> Intg i ::\\<preceq> PrimT Integer"
 by (simp add: conf_def)
 
 
@@ -68,17 +68,17 @@
     ins!pc = Bipush i; 
     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
-    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+    G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |]
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
 apply (blast intro: approx_stk_imp_approx_stk_sup 
                     approx_loc_imp_approx_loc_sup)
 done
 
 lemma NT_subtype_conv:
-  "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
+  "G \\<turnstile> NT \\<preceq> T = (T=NT \\<or> (\\<exists>C. T = Class C))"
 proof -
-  have "!!T T'. G \<turnstile> T' \<preceq> T ==> T' = NT --> (T=NT | (\<exists>C. T = Class C))"
+  have "!!T T'. G \\<turnstile> T' \\<preceq> T ==> T' = NT --> (T=NT | (\\<exists>C. T = Class C))"
     apply (erule widen.induct)
     apply auto
     apply (case_tac R)
@@ -96,8 +96,8 @@
     ins!pc =  Aconst_null; 
     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
-    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+    G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (force simp add: approx_val_Null NT_subtype_conv)
@@ -107,9 +107,9 @@
 
 
 lemma Cast_conf2:
-  "[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
-      G\<turnstile>Class C\<preceq>T; is_class G C|] 
-  ==> G,h\<turnstile>v::\<preceq>T"
+  "[| wf_prog ok G; G,h\\<turnstile>v::\\<preceq>RefT rt; cast_ok G C h v; 
+      G\\<turnstile>Class C\\<preceq>T; is_class G C|] 
+  ==> G,h\\<turnstile>v::\\<preceq>T"
 apply (unfold cast_ok_def)
 apply (frule widen_Class)
 apply (elim exE disjE)
@@ -126,8 +126,8 @@
     ins!pc = Checkcast D; 
     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+    G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
 apply (blast intro: approx_stk_imp_approx_stk_sup 
                     approx_loc_imp_approx_loc_sup Cast_conf2)
@@ -140,8 +140,8 @@
   ins!pc = Getfield F D; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def
                 split: option.split)
 apply (frule conf_widen)
@@ -162,8 +162,8 @@
   ins!pc = Putfield F D; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
 apply (clarsimp simp add: approx_val_def)
 apply (frule conf_widen)
@@ -183,7 +183,7 @@
 done
 
 lemma collapse_paired_All:
-  "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
+  "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)"
   by fast
 
 lemma New_correct:
@@ -192,8 +192,8 @@
   ins!pc = New cl_idx; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def defs1
 		   fun_upd_apply map_eq_Cons raise_xcpt_def init_vars_def 
        split: option.split)
@@ -220,15 +220,15 @@
   ins ! pc = Invoke C' mn pTs; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>" 
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>" 
 proof -
   assume wtprog: "wt_jvm_prog G phi"
   assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)"
   assume ins:    "ins ! pc = Invoke C' mn pTs"
   assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
   assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
-  assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
+  assume approx: "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd>"
   
   from wtprog 
   obtain wfmb where
@@ -237,7 +237,7 @@
       
   from ins method approx
   obtain s where
-    heap_ok: "G\<turnstile>h hp\<surd>" and
+    heap_ok: "G\\<turnstile>h hp\\<surd>" and
     phi_pc:  "phi C sig!pc = Some s" and
     is_class_C: "is_class G C" and
     frame:   "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and
@@ -249,11 +249,11 @@
     s: "s = (rev apTs @ X # ST, LT)" and
     l: "length apTs = length pTs" and
     is_class: "is_class G C'" and
-    X: "G\<turnstile> X \<preceq> Class C'" and
-    w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
+    X: "G\\<turnstile> X \\<preceq> Class C'" and
+    w: "\\<forall>x\\<in>set (zip apTs pTs). x \\<in> widen G" and
     mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and
     pc:  "Suc pc < length ins" and
-    step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
+    step: "G \\<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
     by (simp add: wt_instr_def del: not_None_eq) (elim exE conjE, rule that)
 
   from step
@@ -284,13 +284,13 @@
     by - (drule approx_stk_append_lemma, simp, elim, simp)
 
   from oX 
-  have "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X"
+  have "\\<exists>T'. typeof (option_map obj_ty \\<circ> hp) oX = Some T' \\<and> G \\<turnstile> T' \\<preceq> X"
     by (clarsimp simp add: approx_val_def conf_def)
 
   with X_Ref
   obtain T' where
-    oX_Ref: "typeof (option_map obj_ty \<circ> hp) oX = Some (RefT T')"
-            "G \<turnstile> RefT T' \<preceq> X" 
+    oX_Ref: "typeof (option_map obj_ty \\<circ> hp) oX = Some (RefT T')"
+            "G \\<turnstile> RefT T' \\<preceq> X" 
     apply (elim, simp)
     apply (frule widen_RefT2)
     by (elim, simp)
@@ -317,7 +317,7 @@
       by (auto simp add: obj_ty_def)
 
     with X_Ref oX_Ref loc
-    obtain D: "G \<turnstile> Class D \<preceq> X"
+    obtain D: "G \\<turnstile> Class D \\<preceq> X"
       by simp
 
     with X_Ref
@@ -326,26 +326,26 @@
       by - (drule widen_Class, elim, rule that)
       
     with X
-    have X'_subcls: "G \<turnstile> X' \<preceq>C C'" 
+    have X'_subcls: "G \\<turnstile> X' \\<preceq>C C'" 
       by simp
 
     with mC' wfprog
     obtain D0 rT0 maxs0 maxl0 ins0 where
-      mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT"
+      mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\\<turnstile>rT0\\<preceq>rT"
       by (auto dest: subtype_widen_methd intro: that)
 
     from X' D
-    have D_subcls: "G \<turnstile> D \<preceq>C X'" 
+    have D_subcls: "G \\<turnstile> D \\<preceq>C X'" 
       by simp
 
     with wfprog mX
     obtain D'' rT' mxs' mxl' ins' where
       mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" 
-          "G \<turnstile> rT' \<preceq> rT0"
+          "G \\<turnstile> rT' \\<preceq> rT0"
       by (auto dest: subtype_widen_methd intro: that)
 
     from mX mD
-    have rT': "G \<turnstile> rT' \<preceq> rT"
+    have rT': "G \\<turnstile> rT' \\<preceq> rT"
       by - (rule widen_trans)
     
     from is_class X'_subcls D_subcls
@@ -371,7 +371,7 @@
       by (simp add: raise_xcpt_def)
     
     from wtprog mD''
-    have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []"
+    have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \\<and> ins' \\<noteq> []"
       by (auto dest: wt_jvm_prog_impl_wt_start)
     
     then
@@ -383,8 +383,8 @@
     proof -
       from start LT0
       have sup_loc: 
-        "G \<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0"
-        (is "G \<turnstile> ?LT <=l LT0")
+        "G \\<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0"
+        (is "G \\<turnstile> ?LT <=l LT0")
         by (simp add: wt_start_def sup_state_def)
 
       have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
@@ -392,14 +392,14 @@
                       list_all2_def set_replicate_conv_if)
 
       from wfprog mD is_class_D
-      have "G \<turnstile> Class D \<preceq> Class D''"
+      have "G \\<turnstile> Class D \\<preceq> Class D''"
         by (auto dest: method_wf_mdecl)
       with obj_ty loc
       have a: "approx_val G hp (Addr ref) (OK (Class D''))"
         by (simp add: approx_val_def conf_def)
 
       from w l
-      have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G"
+      have "\\<forall>x\\<in>set (zip (rev apTs) (rev pTs)). x \\<in> widen G"
         by (auto simp add: zip_rev)
       with wfprog l l_o opTs
       have "approx_loc G hp opTs (map OK (rev pTs))"
@@ -426,14 +426,14 @@
     have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'"
     proof -    
       from s s' mC' step l
-      have "G \<turnstile> LT <=l LT'"
+      have "G \\<turnstile> LT <=l LT'"
         by (simp add: step_def sup_state_def)
       with wfprog a_loc
       have a: "approx_loc G hp loc LT'"
         by (rule approx_loc_imp_approx_loc_sup)
       moreover
       from s s' mC' step l
-      have  "G \<turnstile> map OK ST <=l map OK (tl ST')"
+      have  "G \\<turnstile> map OK ST <=l map OK (tl ST')"
         by (auto simp add: step_def sup_state_def map_eq_Cons)
       with wfprog a_stk'
       have "approx_stk G hp stk' (tl ST')"
@@ -450,7 +450,7 @@
   }
   
   with Null_ok oX_Ref
-  show "G,phi \<turnstile>JVM state'\<surd>"
+  show "G,phi \\<turnstile>JVM state'\\<surd>"
     by - (cases oX, auto)
 qed
 
@@ -462,8 +462,8 @@
   ins ! pc = Return; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm iff del: not_None_eq)
 apply (frule wt_jvm_prog_impl_wt_instr)
 apply (assumption, assumption, erule Suc_lessD)
@@ -483,8 +483,8 @@
   ins ! pc = Goto branch; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup 
                    approx_stk_imp_approx_stk_sup)
@@ -497,8 +497,8 @@
   ins ! pc = Ifcmpeq branch; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup 
                    approx_stk_imp_approx_stk_sup)
@@ -510,8 +510,8 @@
   ins ! pc = Pop;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup 
                    approx_stk_imp_approx_stk_sup)
@@ -523,8 +523,8 @@
   ins ! pc = Dup;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup 
                     approx_val_imp_approx_val_sup 
@@ -538,8 +538,8 @@
   ins ! pc = Dup_x1;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup 
                     approx_val_imp_approx_val_sup 
@@ -553,8 +553,8 @@
   ins ! pc = Dup_x2;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup 
                     approx_val_imp_approx_val_sup 
@@ -568,8 +568,8 @@
   ins ! pc = Swap;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup 
                     approx_val_imp_approx_val_sup 
@@ -583,8 +583,8 @@
   ins ! pc = IAdd; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
 apply (blast intro: approx_stk_imp_approx_stk_sup 
                     approx_val_imp_approx_val_sup 
@@ -598,8 +598,8 @@
 "[| wt_jvm_prog G phi;
   method (G,C) sig = Some (C,rT,maxs,maxl,ins); 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] 
+==> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (frule wt_jvm_prog_impl_wt_instr_cor)
 apply assumption+
 apply (cases "ins!pc")
@@ -632,14 +632,14 @@
 (** Main **)
 
 lemma correct_state_impl_Some_method:
-  "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
-  ==> \<exists>meth. method (G,C) sig = Some(C,meth)"
+  "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> 
+  ==> \\<exists>meth. method (G,C) sig = Some(C,meth)"
 by (auto simp add: correct_state_def Let_def)
 
 
 lemma BV_correct_1 [rule_format]:
-"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|] 
- ==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>"
+"!!state. [| wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>|] 
+ ==> exec (G,state) = Some state' --> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (simp only: split_tupled_all)
 apply (rename_tac xp hp frs)
 apply (case_tac xp)
@@ -655,12 +655,12 @@
 
 
 lemma L0:
-  "[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
+  "[| xp=None; frs\\<noteq>[] |] ==> (\\<exists>state'. exec (G,xp,hp,frs) = Some state')"
 by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
 
 lemma L1:
-  "[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|] 
-  ==> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
+  "[|wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[]|] 
+  ==> \\<exists>state'. exec(G,xp,hp,frs) = Some state' \\<and> G,phi \\<turnstile>JVM state'\\<surd>"
 apply (drule L0)
 apply assumption
 apply (fast intro: BV_correct_1)
@@ -668,7 +668,7 @@
 
 
 theorem BV_correct [rule_format]:
-"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>"
+"[| wt_jvm_prog G phi; G \\<turnstile> s -jvm-> t |] ==> G,phi \\<turnstile>JVM s\\<surd> --> G,phi \\<turnstile>JVM t\\<surd>"
 apply (unfold exec_all_def)
 apply (erule rtrancl_induct)
  apply simp
@@ -678,8 +678,8 @@
 
 theorem BV_correct_initial:
 "[| wt_jvm_prog G phi; 
-    G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] 
-==> approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> 
+    G \\<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \\<turnstile>JVM s0 \\<surd>|] 
+==> approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \\<and> 
     approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
 apply (drule BV_correct)
 apply assumption+
diff -r cd1a2bee5549 -r 08e1610c1dcb src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Tue Jan 02 22:41:17 2001 +0100
@@ -94,7 +94,7 @@
             (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
             G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
             G\\<turnstile> s3 -res\\<succ>v -> (x4,s4) |] ==>
-         G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
+         G\\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
 
 
 (* evaluation of expression lists *)
diff -r cd1a2bee5549 -r 08e1610c1dcb src/HOL/MicroJava/J/Example.ML
--- a/src/HOL/MicroJava/J/Example.ML	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.ML	Tue Jan 02 22:41:17 2001 +0100
@@ -195,7 +195,7 @@
 
 fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
 Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\ 
-\ Expr(e::=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
+\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
 (* ?pTs' = [Class Base] *)
 by t;		(* ;; *)
 by  t;		(* Expr *)
diff -r cd1a2bee5549 -r 08e1610c1dcb src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Jan 02 22:41:17 2001 +0100
@@ -86,7 +86,7 @@
 			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
   test_def "test == Expr(e::=NewC Ext);; 
-                    Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
+                    Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
 
 
 syntax
diff -r cd1a2bee5549 -r 08e1610c1dcb src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/Term.thy	Tue Jan 02 22:41:17 2001 +0100
@@ -20,8 +20,9 @@
   | FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
   | FAss cname expr vname 
                     expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
-  | Call expr mname 
-    (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
+  | Call cname expr mname 
+    (ty list) (expr list)    (* method call*) ("{_}_.._'( {_}_')"
+                                                            [10,90,99,10,10] 90)
 
 datatype stmt
   = Skip                     (* empty statement *)
diff -r cd1a2bee5549 -r 08e1610c1dcb src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Tue Jan 02 12:04:33 2001 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Tue Jan 02 22:41:17 2001 +0100
@@ -136,7 +136,7 @@
   Call  "[| E\\<turnstile>a::Class C;
             E\\<turnstile>ps[::]pTs;
             max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
-         E\\<turnstile>a..mn({pTs'}ps)::rT"
+         E\\<turnstile>{C}a..mn({pTs'}ps)::rT"
 
 (* well-typed expression lists *)