src/HOL/MicroJava/J/Conform.thy

 
 theory Conform imports State WellType Exceptions begin
 
 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)"
-
-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 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]"
+                                   ("_,_ \<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" ("_,_ \<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" ("_ \<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: