# HG changeset patch
# User wenzelm
# Date 1451503842 -3600
# Node ID 133a8a888ae89d72e1e91ec80bd7117aaf1ae823
# Parent  89206877f0ee1f3cc7121989aaf25431aa4a2a3d
clarified print modes;
more symbols;

diff -r 89206877f0ee -r 133a8a888ae8 src/HOL/MicroJava/BV/JVMType.thy
--- 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))))"
diff -r 89206877f0ee -r 133a8a888ae8 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- 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)
diff -r 89206877f0ee -r 133a8a888ae8 src/HOL/MicroJava/DFA/LBVComplete.thy
--- 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 
diff -r 89206877f0ee -r 133a8a888ae8 src/HOL/MicroJava/DFA/Semilat.thy
--- 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)
diff -r 89206877f0ee -r 133a8a888ae8 src/HOL/MicroJava/DFA/SemilatAlg.thy
--- 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
 
 
diff -r 89206877f0ee -r 133a8a888ae8 src/HOL/MicroJava/DFA/Typing_Framework_err.thy
--- 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
diff -r 89206877f0ee -r 133a8a888ae8 src/HOL/MicroJava/J/Conform.thy
--- 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: