# HG changeset patch
# User wenzelm
# Date 1376426278 -7200
# Node ID e0968e1f6fe93a599af681520380afc75c00fa88
# Parent  f127e949389f173abc8699af55bccaf4c5a7a5e2
more symbolic notation;

diff -r f127e949389f -r e0968e1f6fe9 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Aug 13 22:25:24 2013 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Aug 13 22:37:58 2013 +0200
@@ -397,8 +397,8 @@
   one (after arbitrarily many steps).
 *}
 theorem welltyped_aggressive_imp_defensive:
-  "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t 
-  \<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)"
+  "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t 
+  \<Longrightarrow> G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)"
   apply (unfold exec_all_def) 
   apply (erule rtrancl_induct)
    apply (simp add: exec_all_d_def)
@@ -417,7 +417,7 @@
 
 theorem no_type_errors:
   "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd>
-  \<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> t \<Longrightarrow> t \<noteq> TypeError"
+  \<Longrightarrow> G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t \<Longrightarrow> t \<noteq> TypeError"
   apply (unfold exec_all_d_def)   
   apply (erule rtrancl_induct)
    apply simp
@@ -433,7 +433,7 @@
     and m: "m \<noteq> init"
   defines start: "s \<equiv> start_state \<Gamma> C m"
 
-  assumes s: "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> t" 
+  assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t" 
   shows "t \<noteq> TypeError"
 proof -
   from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
@@ -449,7 +449,7 @@
 corollary welltyped_commutes:
   fixes G ("\<Gamma>") and Phi ("\<Phi>")
   assumes wt: "wt_jvm_prog \<Gamma> \<Phi>" and *: "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" 
-  shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
+  shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
   apply rule
    apply (erule defensive_imp_aggressive, rule welltyped_aggressive_imp_defensive)
     apply (rule wt)
@@ -464,7 +464,7 @@
     and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     and m: "m \<noteq> init"
   defines start: "s \<equiv> start_state \<Gamma> C m"
-  shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
+  shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
 proof -
   from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
     unfolding start by (rule BV_correct_initial)
diff -r f127e949389f -r e0968e1f6fe9 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Aug 13 22:25:24 2013 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Aug 13 22:37:58 2013 +0200
@@ -1304,7 +1304,7 @@
 done
 
 theorem BV_correct [rule_format]:
-"\<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>"
+"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s \<midarrow>jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
 apply (unfold exec_all_def)
 apply (erule rtrancl_induct)
  apply simp
@@ -1314,7 +1314,7 @@
 
 theorem BV_correct_implies_approx:
 "\<lbrakk> wt_jvm_prog G phi; 
-    G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
+    G \<turnstile> s0 \<midarrow>jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
 \<Longrightarrow> 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)
@@ -1356,12 +1356,12 @@
   assumes welltyped:   "wt_jvm_prog \<Gamma> \<Phi>" and
           main_method: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)"  
   shows typesafe:
-  "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s  \<Longrightarrow>  \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+  "G \<turnstile> start_state \<Gamma> C m \<midarrow>jvm\<rightarrow> s  \<Longrightarrow>  \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
 proof -
   from welltyped main_method
   have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>" by (rule BV_correct_initial)
   moreover
-  assume "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s"
+  assume "G \<turnstile> start_state \<Gamma> C m \<midarrow>jvm\<rightarrow> s"
   ultimately  
   show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" using welltyped by - (rule BV_correct)
 qed
diff -r f127e949389f -r e0968e1f6fe9 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Aug 13 22:25:24 2013 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Aug 13 22:37:58 2013 +0200
@@ -59,7 +59,7 @@
 theorem exec_instr_in_exec_all:
   "\<lbrakk> exec_instr i G hp stk lvars C S pc frs =  (None, hp', frs');
              gis (gmb G C S) ! pc = i\<rbrakk>  \<Longrightarrow>
-       G \<turnstile> (None, hp, (stk, lvars, C, S, pc) # frs) -jvm\<rightarrow> (None, hp', frs')"
+       G \<turnstile> (None, hp, (stk, lvars, C, S, pc) # frs) \<midarrow>jvm\<rightarrow> (None, hp', frs')"
 apply (simp only: exec_all_def)
 apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
 apply (simp add: gis_def gmb_def)
@@ -71,7 +71,7 @@
   (exec_instr i G hp0 stk0 lvars0 C S pc0 frs) = 
   (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs) \<rbrakk>
   \<Longrightarrow> 
-  G \<turnstile> (None, hp0, (stk0,lvars0,C,S, pc0)#frs) -jvm\<rightarrow> 
+  G \<turnstile> (None, hp0, (stk0,lvars0,C,S, pc0)#frs) \<midarrow>jvm\<rightarrow> 
   (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs)"
 apply (unfold exec_all_def)
 apply (rule r_into_rtrancl)
@@ -90,7 +90,7 @@
   "{G,C,S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1} ==
   \<forall> pre post frs.
   (gis (gmb G C S) = pre @ instrs @ post) \<longrightarrow>
-   G \<turnstile> (None,hp0,(os0,lvars0,C,S,length pre)#frs) -jvm\<rightarrow>
+   G \<turnstile> (None,hp0,(os0,lvars0,C,S,length pre)#frs) \<midarrow>jvm\<rightarrow>
        (None,hp1,(os1,lvars1,C,S,(length pre) + (length instrs))#frs)"
 
 
diff -r f127e949389f -r e0968e1f6fe9 src/HOL/MicroJava/JVM/JVMDefensive.thy
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Tue Aug 13 22:25:24 2013 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Tue Aug 13 22:37:58 2013 +0200
@@ -119,14 +119,11 @@
 
 definition
   exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
-                   ("_ |- _ -jvmd-> _" [61,61,61]60) where
-  "G |- s -jvmd-> t \<longleftrightarrow>
+                   ("_ \<turnstile> _ \<midarrow>jvmd\<rightarrow> _" [61,61,61]60) where
+  "G \<turnstile> s \<midarrow>jvmd\<rightarrow> t \<longleftrightarrow>
          (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
                   {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
 
-notation (xsymbols)
-  exec_all_d  ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
-
 
 declare split_paired_All [simp del]
 declare split_paired_Ex [simp del]
@@ -146,9 +143,9 @@
 
 
 lemma defensive_imp_aggressive:
-  "G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t"
+  "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t"
 proof -
-  have "\<And>x y. G \<turnstile> x -jvmd\<rightarrow> y \<Longrightarrow> \<forall>s t. x = Normal s \<longrightarrow> y = Normal t \<longrightarrow>  G \<turnstile> s -jvm\<rightarrow> t"
+  have "\<And>x y. G \<turnstile> x \<midarrow>jvmd\<rightarrow> y \<Longrightarrow> \<forall>s t. x = Normal s \<longrightarrow> y = Normal t \<longrightarrow>  G \<turnstile> s \<midarrow>jvm\<rightarrow> t"
     apply (unfold exec_all_d_def)
     apply (erule rtrancl_induct)
      apply (simp add: exec_all_def)
@@ -163,9 +160,9 @@
     apply blast
     done
   moreover
-  assume "G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)" 
+  assume "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)" 
   ultimately
-  show "G \<turnstile> s -jvm\<rightarrow> t" by blast
+  show "G \<turnstile> s \<midarrow>jvm\<rightarrow> t" by blast
 qed
 
 end
\ No newline at end of file
diff -r f127e949389f -r e0968e1f6fe9 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Aug 13 22:25:24 2013 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Aug 13 22:37:58 2013 +0200
@@ -24,13 +24,10 @@
 
 
 definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
-              ("_ |- _ -jvm-> _" [61,61,61]60) where
-  "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
+              ("_ \<turnstile> _ \<midarrow>jvm\<rightarrow> _" [61,61,61]60) where
+  "G \<turnstile> s \<midarrow>jvm\<rightarrow> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
 
 
-notation (xsymbols)
-  exec_all  ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
-
 text {*
   The start configuration of the JVM: in the start heap, we call a 
   method @{text m} of class @{text C} in program @{text G}. The