--- a/src/HOL/MicroJava/BV/Correct.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Tue Jun 12 14:11:00 2001 +0200
@@ -56,7 +56,7 @@
constdefs
correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
- ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
+ ("_,_ |-JVM _ [ok]" [51,51] 50)
"correct_state G phi == \<lambda>(xp,hp,frs).
case xp of
None => (case frs of
@@ -73,9 +73,9 @@
| Some x => True"
-syntax (HTML)
+syntax (xsymbols)
correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
- ("_,_ |-JVM _ [ok]" [51,51] 50)
+ ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
lemma sup_ty_opt_OK:
--- a/src/HOL/MicroJava/BV/JVMType.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy Tue Jun 12 14:11:00 2001 +0200
@@ -43,31 +43,31 @@
constdefs
sup_ty_opt :: "['code prog,ty err,ty err] => bool"
- ("_ \<turnstile> _ <=o _" [71,71] 70)
+ ("_ |- _ <=o _" [71,71] 70)
"sup_ty_opt G == Err.le (subtype G)"
sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
- ("_ \<turnstile> _ <=l _" [71,71] 70)
+ ("_ |- _ <=l _" [71,71] 70)
"sup_loc G == Listn.le (sup_ty_opt G)"
sup_state :: "['code prog,state_type,state_type] => bool"
- ("_ \<turnstile> _ <=s _" [71,71] 70)
+ ("_ |- _ <=s _" [71,71] 70)
"sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
- ("_ \<turnstile> _ <=' _" [71,71] 70)
+ ("_ |- _ <=' _" [71,71] 70)
"sup_state_opt G == Opt.le (sup_state G)"
-syntax (HTML)
+syntax (xsymbols)
sup_ty_opt :: "['code prog,ty err,ty err] => bool"
- ("_ |- _ <=o _")
+ ("_ \<turnstile> _ <=o _" [71,71] 70)
sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
- ("_ |- _ <=l _" [71,71] 70)
+ ("_ \<turnstile> _ <=l _" [71,71] 70)
sup_state :: "['code prog,state_type,state_type] => bool"
- ("_ |- _ <=s _" [71,71] 70)
+ ("_ \<turnstile> _ <=s _" [71,71] 70)
sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
- ("_ |- _ <=' _" [71,71] 70)
+ ("_ \<turnstile> _ <=' _" [71,71] 70)
lemma JVM_states_unfold:
--- 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"
--- a/src/HOL/MicroJava/J/Decl.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy Tue Jun 12 14:11:00 2001 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/MicroJava/J/Decl.thy
ID: $Id$
Author: David von Oheimb
- Copyright 1997 Technische Universitaet Muenchen
+ Copyright 1999 Technische Universitaet Muenchen
*)
header "Class Declarations and whole Programs"
--- a/src/HOL/MicroJava/J/Eval.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Tue Jun 12 14:11:00 2001 +0200
@@ -13,7 +13,7 @@
evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
exec :: "java_mb prog => (xstate \<times> stmt \<times> xstate) set"
-syntax
+syntax (xsymbols)
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
evals:: "[java_mb prog,xstate,expr list,
@@ -22,7 +22,7 @@
exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
-syntax (HTML)
+syntax
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
("_ |- _ -_>_-> _" [51,82,60,82,82] 81)
evals:: "[java_mb prog,xstate,expr list,
--- a/src/HOL/MicroJava/J/Example.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Tue Jun 12 14:11:00 2001 +0200
@@ -1,7 +1,7 @@
(* Title: isabelle/Bali/Example.thy
ID: $Id$
Author: David von Oheimb
- Copyright 1997 Technische Universitaet Muenchen
+ Copyright 1999 Technische Universitaet Muenchen
*)
header "Example MicroJava Program"
--- a/src/HOL/MicroJava/J/State.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/State.thy Tue Jun 12 14:11:00 2001 +0200
@@ -25,7 +25,7 @@
| ClassCast
| OutOfMemory
-types aheap = "loc \<leadsto> obj" (* "heap" used in a translation below *)
+types aheap = "loc \<leadsto> obj" (** "heap" used in a translation below **)
locals = "vname \<leadsto> val"
state (* simple state, i.e. variable contents *)
--- a/src/HOL/MicroJava/J/TypeRel.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Jun 12 14:11:00 2001 +0200
@@ -13,17 +13,17 @@
widen :: "'c prog => (ty \<times> ty ) set" (* widening *)
cast :: "'c prog => (cname \<times> cname) set" (* casting *)
-syntax
+syntax (xsymbols)
subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
- subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
- widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
- cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
+ subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
+ widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
+ cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
-syntax (HTML)
+syntax
subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
- subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
- widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70)
- cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
+ subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
+ widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70)
+ cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
translations
"G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
--- a/src/HOL/MicroJava/J/WellType.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Tue Jun 12 14:11:00 2001 +0200
@@ -103,12 +103,12 @@
ty_exprs:: "java_mb env => (expr list \<times> ty list) set"
wt_stmt :: "java_mb env => stmt set"
-syntax
+syntax (xsymbols)
ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ \<turnstile> _ :: _" [51,51,51]50)
ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
wt_stmt :: "java_mb env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51,51 ]50)
-syntax (HTML)
+syntax
ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ |- _ :: _" [51,51,51]50)
ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
wt_stmt :: "java_mb env => stmt => bool" ("_ |- _ [ok]" [51,51 ]50)
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Tue Jun 12 14:11:00 2001 +0200
@@ -28,12 +28,12 @@
constdefs
exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
- "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
+ ("_ |- _ -jvm-> _" [61,61,61]60)
+ "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
-syntax (HTML)
+syntax (xsymbols)
exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ |- _ -jvm-> _" [61,61,61]60)
+ ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
end