corrected xsymbol/HTML syntax
authoroheimb
Tue Jun 12 14:11:00 2001 +0200 (2001-06-12)
changeset 11372648795477bb5
parent 11371 1d5d181b7e28
child 11373 ef11fb6e6c58
corrected xsymbol/HTML syntax
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/MicroJava/JVM/JVMExec.thy
     1.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Mon Jun 11 19:21:13 2001 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Jun 12 14:11:00 2001 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  
     1.5  constdefs
     1.6   correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
     1.7 -                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
     1.8 +                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
     1.9  "correct_state G phi == \<lambda>(xp,hp,frs).
    1.10     case xp of
    1.11       None => (case frs of
    1.12 @@ -73,9 +73,9 @@
    1.13     | Some x => True" 
    1.14  
    1.15  
    1.16 -syntax (HTML)
    1.17 +syntax (xsymbols)
    1.18   correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
    1.19 -                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
    1.20 +                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
    1.21  
    1.22  
    1.23  lemma sup_ty_opt_OK:
     2.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Mon Jun 11 19:21:13 2001 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Tue Jun 12 14:11:00 2001 +0200
     2.3 @@ -43,31 +43,31 @@
     2.4  
     2.5  constdefs
     2.6    sup_ty_opt :: "['code prog,ty err,ty err] => bool" 
     2.7 -                 ("_ \<turnstile> _ <=o _" [71,71] 70)
     2.8 +                 ("_ |- _ <=o _" [71,71] 70)
     2.9    "sup_ty_opt G == Err.le (subtype G)"
    2.10  
    2.11    sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
    2.12 -              ("_ \<turnstile> _ <=l _"  [71,71] 70)
    2.13 +              ("_ |- _ <=l _"  [71,71] 70)
    2.14    "sup_loc G == Listn.le (sup_ty_opt G)"
    2.15  
    2.16    sup_state :: "['code prog,state_type,state_type] => bool"	  
    2.17 -               ("_ \<turnstile> _ <=s _"  [71,71] 70)
    2.18 +               ("_ |- _ <=s _"  [71,71] 70)
    2.19    "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
    2.20  
    2.21    sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
    2.22 -                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
    2.23 +                   ("_ |- _ <=' _"  [71,71] 70)
    2.24    "sup_state_opt G == Opt.le (sup_state G)"
    2.25  
    2.26  
    2.27 -syntax (HTML) 
    2.28 +syntax (xsymbols)
    2.29    sup_ty_opt    :: "['code prog,ty err,ty err] => bool" 
    2.30 -                   ("_ |- _ <=o _")
    2.31 +                   ("_ \<turnstile> _ <=o _" [71,71] 70)
    2.32    sup_loc       :: "['code prog,locvars_type,locvars_type] => bool" 
    2.33 -                   ("_ |- _ <=l _"  [71,71] 70)
    2.34 +                   ("_ \<turnstile> _ <=l _" [71,71] 70)
    2.35    sup_state     :: "['code prog,state_type,state_type] => bool"	
    2.36 -                   ("_ |- _ <=s _"  [71,71] 70)
    2.37 +                   ("_ \<turnstile> _ <=s _" [71,71] 70)
    2.38    sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
    2.39 -                   ("_ |- _ <=' _"  [71,71] 70)
    2.40 +                   ("_ \<turnstile> _ <=' _" [71,71] 70)
    2.41                     
    2.42  
    2.43  lemma JVM_states_unfold: 
     3.1 --- a/src/HOL/MicroJava/J/Conform.thy	Mon Jun 11 19:21:13 2001 +0200
     3.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Tue Jun 12 14:11:00 2001 +0200
     3.3 @@ -12,44 +12,45 @@
     3.4  
     3.5  constdefs
     3.6  
     3.7 -  hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50)
     3.8 - "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
     3.9 +  hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50)
    3.10 + "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
    3.11  
    3.12 -  conf :: "'c prog => aheap => val => ty => bool"	("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
    3.13 - "G,h\<turnstile>v::\<preceq>T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    3.14 +  conf :: "'c prog => aheap => val => ty => bool"	
    3.15 +                                   ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
    3.16 + "G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    3.17  
    3.18    lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
    3.19 -                                                ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
    3.20 - "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)"
    3.21 +                                   ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
    3.22 + "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)"
    3.23  
    3.24 -  oconf :: "'c prog => aheap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
    3.25 - "G,h\<turnstile>obj\<surd> == G,h\<turnstile>snd obj[::\<preceq>]map_of (fields (G,fst obj))"
    3.26 +  oconf :: "'c prog => aheap => obj => bool" ("_,_ |- _ [ok]" [51,51,51] 50)
    3.27 + "G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))"
    3.28  
    3.29 -  hconf :: "'c prog => aheap => bool" ("_ \<turnstile>h _ \<surd>" [51,51] 50)
    3.30 - "G\<turnstile>h h\<surd>    == \<forall>a obj. h a = Some obj --> G,h\<turnstile>obj\<surd>"
    3.31 +  hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50)
    3.32 + "G|-h h [ok]    == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
    3.33  
    3.34 -  conforms :: "state => java_mb env_ => bool"	("_ ::\<preceq> _" [51,51] 50)
    3.35 - "s::\<preceq>E == prg E\<turnstile>h heap s\<surd> \<and> prg E,heap s\<turnstile>locals s[::\<preceq>]localT E"
    3.36 +  conforms :: "state => java_mb env_ => bool"	("_ ::<= _" [51,51] 50)
    3.37 + "s::<=E == prg E|-h heap s [ok] \<and> prg E,heap s|-locals s[::<=]localT E"
    3.38  
    3.39  
    3.40 -syntax (HTML)
    3.41 +syntax (xsymbols)
    3.42    hext     :: "aheap => aheap => bool"
    3.43 -              ("_ <=| _" [51,51] 50)
    3.44 +              ("_ \<le>| _" [51,51] 50)
    3.45  
    3.46    conf     :: "'c prog => aheap => val => ty => bool"
    3.47 -              ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
    3.48 +              ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
    3.49  
    3.50    lconf    :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
    3.51 -              ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
    3.52 +              ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
    3.53  
    3.54    oconf    :: "'c prog => aheap => obj => bool"
    3.55 -              ("_,_ |- _ [ok]" [51,51,51] 50)
    3.56 +              ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
    3.57  
    3.58    hconf    :: "'c prog => aheap => bool"
    3.59 -              ("_ |-h _ [ok]" [51,51] 50)
    3.60 +              ("_ \<turnstile>h _ \<surd>" [51,51] 50)
    3.61  
    3.62    conforms :: "state => java_mb env_ => bool"
    3.63 -              ("_ ::<= _" [51,51] 50)
    3.64 +              ("_ ::\<preceq> _" [51,51] 50)
    3.65  
    3.66  
    3.67  section "hext"
     4.1 --- a/src/HOL/MicroJava/J/Decl.thy	Mon Jun 11 19:21:13 2001 +0200
     4.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Tue Jun 12 14:11:00 2001 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      HOL/MicroJava/J/Decl.thy
     4.5      ID:         $Id$
     4.6      Author:     David von Oheimb
     4.7 -    Copyright   1997 Technische Universitaet Muenchen
     4.8 +    Copyright   1999 Technische Universitaet Muenchen
     4.9  *)
    4.10  
    4.11  header "Class Declarations and whole Programs"
     5.1 --- a/src/HOL/MicroJava/J/Eval.thy	Mon Jun 11 19:21:13 2001 +0200
     5.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Tue Jun 12 14:11:00 2001 +0200
     5.3 @@ -13,7 +13,7 @@
     5.4    evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
     5.5    exec  :: "java_mb prog => (xstate \<times> stmt                 \<times> xstate) set"
     5.6  
     5.7 -syntax
     5.8 +syntax (xsymbols)
     5.9    eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
    5.10            ("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
    5.11    evals:: "[java_mb prog,xstate,expr list,
    5.12 @@ -22,7 +22,7 @@
    5.13    exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
    5.14            ("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
    5.15  
    5.16 -syntax (HTML)
    5.17 +syntax
    5.18    eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
    5.19            ("_ |- _ -_>_-> _" [51,82,60,82,82] 81)
    5.20    evals:: "[java_mb prog,xstate,expr list,
     6.1 --- a/src/HOL/MicroJava/J/Example.thy	Mon Jun 11 19:21:13 2001 +0200
     6.2 +++ b/src/HOL/MicroJava/J/Example.thy	Tue Jun 12 14:11:00 2001 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  (*  Title:      isabelle/Bali/Example.thy
     6.5      ID:         $Id$
     6.6      Author:     David von Oheimb
     6.7 -    Copyright   1997 Technische Universitaet Muenchen
     6.8 +    Copyright   1999 Technische Universitaet Muenchen
     6.9  *)
    6.10  
    6.11  header "Example MicroJava Program"
     7.1 --- a/src/HOL/MicroJava/J/State.thy	Mon Jun 11 19:21:13 2001 +0200
     7.2 +++ b/src/HOL/MicroJava/J/State.thy	Tue Jun 12 14:11:00 2001 +0200
     7.3 @@ -25,7 +25,7 @@
     7.4  	| ClassCast
     7.5  	| OutOfMemory
     7.6  
     7.7 -types	aheap  = "loc \<leadsto> obj" (* "heap" used in a translation below *)
     7.8 +types	aheap  = "loc \<leadsto> obj" (** "heap" used in a translation below **)
     7.9          locals = "vname \<leadsto> val"	
    7.10  
    7.11          state		(* simple state, i.e. variable contents *)
     8.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Jun 11 19:21:13 2001 +0200
     8.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Jun 12 14:11:00 2001 +0200
     8.3 @@ -13,17 +13,17 @@
     8.4    widen   :: "'c prog => (ty    \<times> ty   ) set"  (* widening *)
     8.5    cast    :: "'c prog => (cname \<times> cname) set"  (* casting *)
     8.6  
     8.7 -syntax
     8.8 +syntax (xsymbols)
     8.9    subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
    8.10 -  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
    8.11 -  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
    8.12 -  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
    8.13 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
    8.14 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
    8.15 +  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
    8.16  
    8.17 -syntax (HTML)
    8.18 +syntax
    8.19    subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
    8.20 -  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
    8.21 -  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _" [71,71,71] 70)
    8.22 -  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
    8.23 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _"  [71,71,71] 70)
    8.24 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _"   [71,71,71] 70)
    8.25 +  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
    8.26  
    8.27  translations
    8.28    "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
     9.1 --- a/src/HOL/MicroJava/J/WellType.thy	Mon Jun 11 19:21:13 2001 +0200
     9.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Tue Jun 12 14:11:00 2001 +0200
     9.3 @@ -103,12 +103,12 @@
     9.4    ty_exprs:: "java_mb env => (expr list \<times> ty list) set"
     9.5    wt_stmt :: "java_mb env =>  stmt                 set"
     9.6  
     9.7 -syntax
     9.8 +syntax (xsymbols)
     9.9    ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
    9.10    ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
    9.11    wt_stmt :: "java_mb env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
    9.12  
    9.13 -syntax (HTML)
    9.14 +syntax
    9.15    ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
    9.16    ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
    9.17    wt_stmt :: "java_mb env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
    10.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Mon Jun 11 19:21:13 2001 +0200
    10.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Jun 12 14:11:00 2001 +0200
    10.3 @@ -28,12 +28,12 @@
    10.4  
    10.5  constdefs
    10.6    exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
    10.7 -              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
    10.8 -  "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
    10.9 +              ("_ |- _ -jvm-> _" [61,61,61]60)
   10.10 +  "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
   10.11  
   10.12  
   10.13 -syntax (HTML)
   10.14 +syntax (xsymbols)
   10.15    exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
   10.16 -              ("_ |- _ -jvm-> _" [61,61,61]60)
   10.17 +              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
   10.18  
   10.19  end