--- 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)
--- 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
--- 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)"
--- 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
--- 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