--- a/src/HOL/MicroJava/BV/JVMType.thy Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Dec 30 20:30:42 2015 +0100
@@ -38,29 +38,22 @@
"sup S maxs maxr == snd(snd(sl S maxs maxr))"
definition sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool"
- ("_ |- _ <=o _" [71,71] 70) where
+ ("_ \<turnstile> _ <=o _" [71,71] 70) where
"sup_ty_opt G == Err.le (subtype G)"
definition sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
- ("_ |- _ <=l _" [71,71] 70) where
+ ("_ \<turnstile> _ <=l _" [71,71] 70) where
"sup_loc G == Listn.le (sup_ty_opt G)"
definition sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
- ("_ |- _ <=s _" [71,71] 70) where
+ ("_ \<turnstile> _ <=s _" [71,71] 70) where
"sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
definition sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
- ("_ |- _ <=' _" [71,71] 70) where
+ ("_ \<turnstile> _ <=' _" [71,71] 70) where
"sup_state_opt G == Opt.le (sup_state G)"
-notation (xsymbols)
- sup_ty_opt ("_ \<turnstile> _ <=o _" [71,71] 70) and
- sup_loc ("_ \<turnstile> _ <=l _" [71,71] 70) and
- sup_state ("_ \<turnstile> _ <=s _" [71,71] 70) and
- sup_state_opt ("_ \<turnstile> _ <=' _" [71,71] 70)
-
-
lemma JVM_states_unfold:
"states S maxs maxr == err(opt((\<Union>{list n (types S) |n. n <= maxs}) \<times>
list maxr (err(types S))))"
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Wed Dec 30 20:30:42 2015 +0100
@@ -182,7 +182,7 @@
by (induct n, auto)
lemma lesubstep_type_simple:
- "a <=[Product.le (op =) r] b \<Longrightarrow> a <=|r| b"
+ "a <=[Product.le (op =) r] b \<Longrightarrow> a \<le>|r| b"
apply (unfold lesubstep_type_def)
apply clarify
apply (simp add: set_conv_nth)
@@ -202,7 +202,7 @@
lemma eff_mono:
"\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\<rbrakk>
- \<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
+ \<Longrightarrow> eff (bs!p) G p et s \<le>|sup_state_opt G| eff (bs!p) G p et t"
apply (unfold eff_def)
apply (rule lesubstep_type_simple)
apply (rule le_list_appendI)
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Dec 30 20:30:42 2015 +0100
@@ -69,7 +69,7 @@
lemma (in lbv) merge_mono:
- assumes less: "ss2 <=|r| ss1"
+ assumes less: "ss2 \<le>|r| ss1"
assumes x: "x \<in> A"
assumes ss1: "snd`set ss1 \<subseteq> A"
assumes ss2: "snd`set ss2 \<subseteq> A"
@@ -131,7 +131,7 @@
assumes s2: "s2 \<in> A"
shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'")
proof -
- from mono pc s2 less have "step pc s2 <=|r| step pc s1" by (rule monoD)
+ from mono pc s2 less have "step pc s2 \<le>|r| step pc s1" by (rule monoD)
moreover
from cert B_A pc have "c!Suc pc \<in> A" by (rule cert_okD3)
moreover
--- a/src/HOL/MicroJava/DFA/Semilat.thy Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Wed Dec 30 20:30:42 2015 +0100
@@ -20,12 +20,12 @@
"lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
"plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
(*<*)
-notation
+notation (ASCII)
"lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and
"lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and
"plussub" ("(_ /+'__ _)" [65, 1000, 66] 65)
(*>*)
-notation (xsymbols)
+notation
"lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy Wed Dec 30 20:30:42 2015 +0100
@@ -10,8 +10,8 @@
begin
definition lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
- ("(_ /<=|_| _)" [50, 0, 51] 50) where
- "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
+ ("(_ /\<le>|_| _)" [50, 0, 51] 50) where
+ "x \<le>|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
primrec plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65) where
"[] ++_f y = y"
@@ -25,14 +25,14 @@
definition mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" where
"mono r step n A ==
- \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s \<le>|r| step p t"
lemma pres_typeD:
"\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
by (unfold pres_type_def, blast)
lemma monoD:
- "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
+ "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s \<le>|r| step p t"
by (unfold mono_def, blast)
lemma boundedD:
@@ -40,11 +40,11 @@
by (unfold bounded_def, blast)
lemma lesubstep_type_refl [simp, intro]:
- "(\<And>x. x <=_r x) \<Longrightarrow> x <=|r| x"
+ "(\<And>x. x <=_r x) \<Longrightarrow> x \<le>|r| x"
by (unfold lesubstep_type_def) auto
lemma lesub_step_typeD:
- "a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
+ "a \<le>|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
by (unfold lesubstep_type_def) blast
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Wed Dec 30 20:30:42 2015 +0100
@@ -86,7 +86,7 @@
lemma map_snd_lessI:
- "x <=|r| y \<Longrightarrow> map_snd OK x <=|Err.le r| map_snd OK y"
+ "x \<le>|r| y \<Longrightarrow> map_snd OK x \<le>|Err.le r| map_snd OK y"
apply (induct x)
apply (unfold lesubstep_type_def map_snd_def)
apply auto
@@ -95,7 +95,7 @@
lemma mono_lift:
"order r \<Longrightarrow> app_mono r app n A \<Longrightarrow> bounded (err_step n app step) n \<Longrightarrow>
- \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s <=|r| step p t \<Longrightarrow>
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> app p t \<longrightarrow> step p s \<le>|r| step p t \<Longrightarrow>
mono (Err.le r) (err_step n app step) n (err A)"
apply (unfold app_mono_def mono_def err_step_def)
apply clarify
--- a/src/HOL/MicroJava/J/Conform.thy Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Wed Dec 30 20:30:42 2015 +0100
@@ -9,41 +9,32 @@
type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}"
-definition hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) where
- "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
+definition hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50) where
+ "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
definition conf :: "'c prog => aheap => val => ty => bool"
- ("_,_ |- _ ::<= _" [51,51,51,51] 50) where
- "G,h|-v::<=T == \<exists>T'. typeof (map_option obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
+ ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) where
+ "G,h\<turnstile>v::\<preceq>T == \<exists>T'. typeof (map_option obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
definition lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
- ("_,_ |- _ [::<=] _" [51,51,51,51] 50) where
- "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)"
+ ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) where
+ "G,h\<turnstile>vs[::\<preceq>]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h\<turnstile>v::\<preceq>T)"
-definition oconf :: "'c prog => aheap => obj => bool" ("_,_ |- _ [ok]" [51,51,51] 50) where
- "G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))"
+definition oconf :: "'c prog => aheap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) where
+ "G,h\<turnstile>obj \<surd> == G,h\<turnstile>snd obj[::\<preceq>]map_of (fields (G,fst obj))"
-definition hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50) where
- "G|-h h [ok] == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
+definition hconf :: "'c prog => aheap => bool" ("_ \<turnstile>h _ \<surd>" [51,51] 50) where
+ "G\<turnstile>h h \<surd> == \<forall>a obj. h a = Some obj --> G,h\<turnstile>obj \<surd>"
definition xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool" where
"xconf hp vo == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))"
-definition conforms :: "xstate => java_mb env' => bool" ("_ ::<= _" [51,51] 50) where
- "s::<=E == prg E|-h heap (store s) [ok] \<and>
- prg E,heap (store s)|-locals (store s)[::<=]localT E \<and>
+definition conforms :: "xstate => java_mb env' => bool" ("_ ::\<preceq> _" [51,51] 50) where
+ "s::\<preceq>E == prg E\<turnstile>h heap (store s) \<surd> \<and>
+ prg E,heap (store s)\<turnstile>locals (store s)[::\<preceq>]localT E \<and>
xconf (heap (store s)) (abrupt s)"
-notation (xsymbols)
- hext ("_ \<le>| _" [51,51] 50) and
- conf ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and
- lconf ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and
- oconf ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and
- hconf ("_ \<turnstile>h _ \<surd>" [51,51] 50) and
- conforms ("_ ::\<preceq> _" [51,51] 50)
-
-
subsection "hext"
lemma hextI: