--- a/src/HOL/MicroJava/J/Conform.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Tue Jun 12 14:11:00 2001 +0200
@@ -12,44 +12,45 @@
constdefs
- hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50)
- "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
+ hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50)
+ "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
- conf :: "'c prog => aheap => val => ty => bool" ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
- "G,h\<turnstile>v::\<preceq>T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
+ conf :: "'c prog => aheap => val => ty => bool"
+ ("_,_ |- _ ::<= _" [51,51,51,51] 50)
+ "G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
- ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
- "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)"
+ ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
+ "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)"
- oconf :: "'c prog => aheap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
- "G,h\<turnstile>obj\<surd> == G,h\<turnstile>snd obj[::\<preceq>]map_of (fields (G,fst obj))"
+ oconf :: "'c prog => aheap => obj => bool" ("_,_ |- _ [ok]" [51,51,51] 50)
+ "G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))"
- hconf :: "'c prog => aheap => bool" ("_ \<turnstile>h _ \<surd>" [51,51] 50)
- "G\<turnstile>h h\<surd> == \<forall>a obj. h a = Some obj --> G,h\<turnstile>obj\<surd>"
+ hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50)
+ "G|-h h [ok] == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
- conforms :: "state => java_mb env_ => bool" ("_ ::\<preceq> _" [51,51] 50)
- "s::\<preceq>E == prg E\<turnstile>h heap s\<surd> \<and> prg E,heap s\<turnstile>locals s[::\<preceq>]localT E"
+ conforms :: "state => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
+ "s::<=E == prg E|-h heap s [ok] \<and> prg E,heap s|-locals s[::<=]localT E"
-syntax (HTML)
+syntax (xsymbols)
hext :: "aheap => aheap => bool"
- ("_ <=| _" [51,51] 50)
+ ("_ \<le>| _" [51,51] 50)
conf :: "'c prog => aheap => val => ty => bool"
- ("_,_ |- _ ::<= _" [51,51,51,51] 50)
+ ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
- ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
+ ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
oconf :: "'c prog => aheap => obj => bool"
- ("_,_ |- _ [ok]" [51,51,51] 50)
+ ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
hconf :: "'c prog => aheap => bool"
- ("_ |-h _ [ok]" [51,51] 50)
+ ("_ \<turnstile>h _ \<surd>" [51,51] 50)
conforms :: "state => java_mb env_ => bool"
- ("_ ::<= _" [51,51] 50)
+ ("_ ::\<preceq> _" [51,51] 50)
section "hext"