added HTML syntax; added spaces in normal syntax for better documents
authorkleing
Fri Sep 22 16:28:53 2000 +0200 (2000-09-22)
changeset 10061fe82134773dc
parent 10060 4522e59b7d84
child 10062 3b819da9c71a
added HTML syntax; added spaces in normal syntax for better documents
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/Term.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.thy
     1.1 --- a/src/HOL/MicroJava/J/Conform.thy	Fri Sep 22 16:28:04 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Fri Sep 22 16:28:53 2000 +0200
     1.3 @@ -12,23 +12,43 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -  hext :: "aheap => aheap => bool"		 (     "_\\<le>|_"  [51,51] 50)
     1.8 +  hext :: "aheap => aheap => bool" ("_ \\<le>| _" [51,51] 50)
     1.9   "h\\<le>|h' == \\<forall>a C fs. h a = Some(C,fs) --> (\\<exists>fs'. h' a = Some(C,fs'))"
    1.10  
    1.11 -  conf :: "'c prog => aheap => val => ty => bool"	 ( "_,_\\<turnstile>_::\\<preceq>_"  [51,51,51,51] 50)
    1.12 +  conf :: "'c prog => aheap => val => ty => bool"	("_,_ \\<turnstile> _ ::\\<preceq> _" [51,51,51,51] 50)
    1.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"
    1.14  
    1.15    lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
    1.16 -                                                 ("_,_\\<turnstile>_[::\\<preceq>]_" [51,51,51,51] 50)
    1.17 +                                                ("_,_ \\<turnstile> _ [::\\<preceq>] _" [51,51,51,51] 50)
    1.18   "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)"
    1.19  
    1.20 -  oconf :: "'c prog => aheap => obj => bool"      ("_,_\\<turnstile>_\\<surd>"     [51,51,51]    50)
    1.21 +  oconf :: "'c prog => aheap => obj => bool" ("_,_ \\<turnstile> _ \\<surd>" [51,51,51] 50)
    1.22   "G,h\\<turnstile>obj\\<surd> == G,h\\<turnstile>snd obj[::\\<preceq>]map_of (fields (G,fst obj))"
    1.23  
    1.24 -  hconf :: "'c prog => aheap => bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
    1.25 +  hconf :: "'c prog => aheap => bool" ("_ \\<turnstile>h _ \\<surd>" [51,51] 50)
    1.26   "G\\<turnstile>h h\\<surd>    == \\<forall>a obj. h a = Some obj --> G,h\\<turnstile>obj\\<surd>"
    1.27  
    1.28 -  conforms :: "state => java_mb env_ => bool"	 ("_::\\<preceq>_"       [51,51]       50)
    1.29 +  conforms :: "state => java_mb env_ => bool"	("_ ::\\<preceq> _" [51,51] 50)
    1.30   "s::\\<preceq>E == prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[::\\<preceq>]localT E"
    1.31  
    1.32 +
    1.33 +syntax (HTML)
    1.34 +  hext     :: "aheap => aheap => bool"
    1.35 +              ("_ <=| _" [51,51] 50)
    1.36 +
    1.37 +  conf     :: "'c prog => aheap => val => ty => bool"
    1.38 +              ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
    1.39 +
    1.40 +  lconf    :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
    1.41 +              ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
    1.42 +
    1.43 +  oconf    :: "'c prog => aheap => obj => bool"
    1.44 +              ("_,_ |- _ [ok]" [51,51,51] 50)
    1.45 +
    1.46 +  hconf    :: "'c prog => aheap => bool"
    1.47 +              ("_ |-h _ [ok]" [51,51] 50)
    1.48 +
    1.49 +  conforms :: "state => java_mb env_ => bool"
    1.50 +              ("_ ::<= _" [51,51] 50)
    1.51 +
    1.52  end
     2.1 --- a/src/HOL/MicroJava/J/Eval.thy	Fri Sep 22 16:28:04 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Fri Sep 22 16:28:53 2000 +0200
     2.3 @@ -16,12 +16,22 @@
     2.4  
     2.5  syntax
     2.6    eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
     2.7 -          ("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
     2.8 +          ("_ \\<turnstile> _ -_\\<succ>_-> _" [51,82,82,82,82] 81)
     2.9    evals:: "[java_mb prog,xstate,expr list,
    2.10                          val list,xstate] => bool "
    2.11 -          ("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
    2.12 +          ("_ \\<turnstile> _ -_[\\<succ>]_-> _" [51,82,51,51,82] 81)
    2.13    exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
    2.14 -          ("_\\<turnstile>_ -_-> _"  [51,82,82,   82]81)
    2.15 +          ("_ \\<turnstile> _ -_-> _" [51,82,82,82] 81)
    2.16 +
    2.17 +syntax (HTML)
    2.18 +  eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
    2.19 +          ("_ |- _ -_>_-> _" [51,82,82,82,82] 81)
    2.20 +  evals:: "[java_mb prog,xstate,expr list,
    2.21 +                        val list,xstate] => bool "
    2.22 +          ("_ |- _ -_[>]_-> _" [51,82,51,51,82] 81)
    2.23 +  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
    2.24 +          ("_ |- _ -_-> _" [51,82,82,82] 81)
    2.25 +
    2.26  
    2.27  translations
    2.28    "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval  G"
     3.1 --- a/src/HOL/MicroJava/J/State.thy	Fri Sep 22 16:28:04 2000 +0200
     3.2 +++ b/src/HOL/MicroJava/J/State.thy	Fri Sep 22 16:28:53 2000 +0200
     3.3 @@ -14,7 +14,6 @@
     3.4          obj = "cname \\<times> fields_"	(* class instance with class name and fields *)
     3.5  
     3.6  constdefs
     3.7 -
     3.8    obj_ty	:: "obj => ty"
     3.9   "obj_ty obj  == Class (fst obj)"
    3.10  
    3.11 @@ -42,9 +41,9 @@
    3.12    Norm		:: "state => xstate"
    3.13  
    3.14  translations
    3.15 -  "heap"	=> "fst"
    3.16 -  "locals"	=> "snd"
    3.17 -  "Norm s"      == "(None,s)"  
    3.18 +  "heap"   => "fst"
    3.19 +  "locals" => "snd"
    3.20 +  "Norm s" == "(None,s)"  
    3.21  
    3.22  constdefs
    3.23  
     4.1 --- a/src/HOL/MicroJava/J/Term.thy	Fri Sep 22 16:28:04 2000 +0200
     4.2 +++ b/src/HOL/MicroJava/J/Term.thy	Fri Sep 22 16:28:53 2000 +0200
     4.3 @@ -11,21 +11,23 @@
     4.4  datatype binop = Eq | Add	   (* function codes for binary operation *)
     4.5  
     4.6  datatype expr
     4.7 -	= NewC	cname		   (* class instance creation *)
     4.8 -	| Cast	cname expr	   (* type cast *)
     4.9 -	| Lit	val		   (* literal value, also references *)
    4.10 -        | BinOp binop  expr expr   (* binary operation *)
    4.11 -	| LAcc vname		   (* local (incl. parameter) access *)
    4.12 -	| LAss vname expr          (* local assign *) ("_::=_"  [      90,90]90)
    4.13 -	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)
    4.14 +	= NewC	cname              (* class instance creation *)
    4.15 +	| Cast	cname expr         (* type cast *)
    4.16 +	| Lit	val                  (* literal value, also references *)
    4.17 +  | BinOp binop  expr expr   (* binary operation *)
    4.18 +	| LAcc vname               (* local (incl. parameter) access *)
    4.19 +	| LAss vname expr          (* local assign *) ("_::=_"   [      90,90]90)
    4.20 +	| FAcc cname expr vname    (* field access *) ("{_}_.._" [10,90,99   ]90)
    4.21  	| FAss cname expr vname 
    4.22 -	                  expr     (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
    4.23 -	| Call expr mname (ty list) (expr list)(* method call*)
    4.24 -                                    ("_.._'({_}_')" [90,99,10,10] 90)
    4.25 +                    expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
    4.26 +	| Call expr mname 
    4.27 +    (ty list) (expr list)    (* method call*) ("_.._'({_}_')" [90,99,10,10] 90)
    4.28 +
    4.29  and stmt
    4.30 -	= Skip			   (* empty      statement *)
    4.31 -	| Expr expr		   (* expression statement *)
    4.32 -	| Comp stmt stmt	   ("_;; _"			[      61,60]60)
    4.33 -	| Cond expr stmt stmt      ("If'(_') _ Else _"		[   80,79,79]70)
    4.34 -	| Loop expr stmt	   ("While'(_') _"		[      80,79]70)
    4.35 +	= Skip                     (* empty statement *)
    4.36 +  | Expr expr                (* expression statement *)
    4.37 +  | Comp stmt stmt       ("_;; _"             [61,60]60)
    4.38 +  | Cond expr stmt stmt  ("If '(_') _ Else _" [80,79,79]70)
    4.39 +  | Loop expr stmt       ("While '(_') _"     [80,79]70)
    4.40 +
    4.41  end
     5.1 --- a/src/HOL/MicroJava/J/Type.thy	Fri Sep 22 16:28:04 2000 +0200
     5.2 +++ b/src/HOL/MicroJava/J/Type.thy	Fri Sep 22 16:28:53 2000 +0200
     5.3 @@ -8,32 +8,35 @@
     5.4  
     5.5  Type = JBasis +
     5.6  
     5.7 -types	cname		(* class name *)
     5.8 -        vnam		(* variable or field name *)
     5.9 -	mname		(* method name *)
    5.10 +types cname   (* class name *)
    5.11 +      vnam    (* variable or field name *)
    5.12 +      mname   (* method name *)
    5.13 +
    5.14  arities cname, vnam, mname :: term
    5.15  
    5.16  datatype vname		(* names for This pointer and local/field variables *)
    5.17 -	= This
    5.18 -	| VName   vnam
    5.19 +  = This
    5.20 +  | VName vnam
    5.21  
    5.22 -datatype prim_ty       	(* primitive type, cf. 4.2 *)
    5.23 -	= Void    	(* 'result type' of void methods *)
    5.24 -	| Boolean
    5.25 -	| Integer
    5.26 +datatype prim_ty  (* primitive type, cf. 4.2 *)
    5.27 +  = Void          (* 'result type' of void methods *)
    5.28 +  | Boolean
    5.29 +  | Integer
    5.30  
    5.31  datatype ref_ty		(* reference type, cf. 4.3 *)
    5.32 -	= NullT		(* null type, cf. 4.1 *)
    5.33 -	| ClassT cname	(* class type *)
    5.34 -datatype ty    		(* any type, cf. 4.1 *)
    5.35 -	= PrimT prim_ty	(* primitive type *)
    5.36 -	| RefT  ref_ty	(* reference type *)
    5.37 +  = NullT		      (* null type, cf. 4.1 *)
    5.38 +  | ClassT cname  (* class type *)
    5.39 +
    5.40 +datatype ty       (* any type, cf. 4.1 *)
    5.41 +  = PrimT prim_ty (* primitive type *)
    5.42 +  | RefT  ref_ty  (* reference type *)
    5.43  
    5.44  syntax
    5.45 -         NT     :: "          ty"
    5.46 -	 Class	:: "cname  => ty"
    5.47 +  NT    :: "          ty"
    5.48 +	Class	:: "cname  => ty"
    5.49 +
    5.50  translations
    5.51 -	"NT"      == "RefT   NullT"
    5.52 +	"NT"      == "RefT NullT"
    5.53  	"Class C" == "RefT (ClassT C)"
    5.54  
    5.55  end
     6.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Sep 22 16:28:04 2000 +0200
     6.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Sep 22 16:28:53 2000 +0200
     6.3 @@ -9,21 +9,27 @@
     6.4  TypeRel = Decl +
     6.5  
     6.6  consts
     6.7 -  subcls1	:: "'c prog => (cname \\<times> cname) set"  (* subclass *)
     6.8 -  widen 	:: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
     6.9 -  cast		:: "'c prog => (cname \\<times> cname) set"  (* casting *)
    6.10 +  subcls1 :: "'c prog => (cname \\<times> cname) set"  (* subclass *)
    6.11 +  widen   :: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
    6.12 +  cast    :: "'c prog => (cname \\<times> cname) set"  (* casting *)
    6.13  
    6.14  syntax
    6.15 -  subcls1	:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
    6.16 -  subcls	:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
    6.17 -  widen		:: "'c prog => [ty   , ty   ] => bool" ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
    6.18 -  cast		:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
    6.19 +  subcls1 :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<prec>C1 _" [71,71,71] 70)
    6.20 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>C _" [71,71,71] 70)
    6.21 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \\<turnstile> _ \\<preceq> _" [71,71,71] 70)
    6.22 +  cast    :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>? _" [71,71,71] 70)
    6.23 +
    6.24 +syntax (HTML)
    6.25 +  subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
    6.26 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
    6.27 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _" [71,71,71] 70)
    6.28 +  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
    6.29  
    6.30  translations
    6.31 -  	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    6.32 -	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    6.33 -	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    6.34 -	"G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
    6.35 +  "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    6.36 +  "G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    6.37 +  "G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    6.38 +  "G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
    6.39  
    6.40  defs
    6.41  
     7.1 --- a/src/HOL/MicroJava/J/Value.thy	Fri Sep 22 16:28:04 2000 +0200
     7.2 +++ b/src/HOL/MicroJava/J/Value.thy	Fri Sep 22 16:28:53 2000 +0200
     7.3 @@ -8,44 +8,45 @@
     7.4  
     7.5  Value = Type +
     7.6  
     7.7 -types   loc		(* locations, i.e. abstract references on objects *)
     7.8 +types   loc     (* locations, i.e. abstract references on objects *)
     7.9  arities loc :: term
    7.10  
    7.11 -datatype val_		(* name non 'val' because of clash with ML token *)
    7.12 -	= Unit		(* dummy result value of void methods *)
    7.13 -	| Null		(* null reference *)
    7.14 -	| Bool bool	(* Boolean value *)
    7.15 -	| Intg int	(* integer value *) (* Name Intg instead of Int because
    7.16 -					       of clash with HOL/Set.thy *)
    7.17 -	| Addr loc	(* addresses, i.e. locations of objects *)
    7.18 +datatype val_   (* name non 'val' because of clash with ML token *)
    7.19 +  = Unit        (* dummy result value of void methods *)
    7.20 +  | Null        (* null reference *)
    7.21 +  | Bool bool   (* Boolean value *)
    7.22 +  | Intg int    (* integer value, name Intg instead of Int because
    7.23 +                   of clash with HOL/Set.thy *)
    7.24 +  | Addr loc    (* addresses, i.e. locations of objects *)
    7.25 +
    7.26  types	val = val_
    7.27  translations "val" <= (type) "val_"
    7.28  
    7.29  consts
    7.30 -  the_Bool	:: "val => bool"
    7.31 -  the_Intg	:: "val => int"
    7.32 -  the_Addr	:: "val => loc"
    7.33 +  the_Bool :: "val => bool"
    7.34 +  the_Intg :: "val => int"
    7.35 +  the_Addr :: "val => loc"
    7.36  
    7.37  primrec
    7.38 - "the_Bool (Bool b) = b"
    7.39 +  "the_Bool (Bool b) = b"
    7.40  
    7.41  primrec
    7.42 - "the_Intg (Intg i) = i"
    7.43 +  "the_Intg (Intg i) = i"
    7.44  
    7.45  primrec
    7.46 - "the_Addr (Addr a) = a"
    7.47 +  "the_Addr (Addr a) = a"
    7.48  
    7.49  consts
    7.50 -  defpval	:: "prim_ty => val"	(* default value for primitive types *)
    7.51 -  default_val	:: "ty => val"		(* default value for all types *)
    7.52 +  defpval :: "prim_ty => val"  (* default value for primitive types *)
    7.53 +  default_val :: "ty => val"   (* default value for all types *)
    7.54  
    7.55  primrec
    7.56 -	"defpval Void    = Unit"
    7.57 -	"defpval Boolean = Bool False"
    7.58 -	"defpval Integer = Intg (#0)"
    7.59 +  "defpval Void    = Unit"
    7.60 +  "defpval Boolean = Bool False"
    7.61 +  "defpval Integer = Intg (#0)"
    7.62  
    7.63  primrec
    7.64 -	"default_val (PrimT pt) = defpval pt"
    7.65 -	"default_val (RefT  r ) = Null"
    7.66 +  "default_val (PrimT pt) = defpval pt"
    7.67 +  "default_val (RefT  r ) = Null"
    7.68  
    7.69  end
     8.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Fri Sep 22 16:28:04 2000 +0200
     8.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Fri Sep 22 16:28:53 2000 +0200
     8.3 @@ -19,17 +19,16 @@
     8.4  types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
     8.5  
     8.6  constdefs
     8.7 -
     8.8 - wf_fdecl	:: "'c prog =>          fdecl => bool"
     8.9 + wf_fdecl	:: "'c prog => fdecl => bool"
    8.10  "wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
    8.11  
    8.12 - wf_mhead	:: "'c prog => sig   => ty => bool"
    8.13 + wf_mhead	:: "'c prog => sig => ty => bool"
    8.14  "wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
    8.15  
    8.16 - wf_mdecl	:: "'c wf_mb => 'c wf_mb"
    8.17 + wf_mdecl :: "'c wf_mb => 'c wf_mb"
    8.18  "wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
    8.19  
    8.20 -  wf_cdecl	:: "'c wf_mb => 'c prog => 'c cdecl => bool"
    8.21 + wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
    8.22  "wf_cdecl wf_mb G ==
    8.23     \\<lambda>(C,(sc,fs,ms)).
    8.24  	(\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
    8.25 @@ -40,7 +39,7 @@
    8.26               (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
    8.27                   method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
    8.28  
    8.29 - wf_prog	:: "'c wf_mb => 'c prog => bool"
    8.30 + wf_prog :: "'c wf_mb => 'c prog => bool"
    8.31  "wf_prog wf_mb G ==
    8.32     let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
    8.33  
     9.1 --- a/src/HOL/MicroJava/J/WellType.thy	Fri Sep 22 16:28:04 2000 +0200
     9.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Fri Sep 22 16:28:53 2000 +0200
     9.3 @@ -23,26 +23,22 @@
     9.4  	= "'c prog \\<times> lenv"
     9.5  
     9.6  syntax
     9.7 -
     9.8 -  prg		:: "'c env => 'c prog"
     9.9 -  localT	:: "'c env => (vname \\<leadsto> ty)"
    9.10 +  prg    :: "'c env => 'c prog"
    9.11 +  localT :: "'c env => (vname \\<leadsto> ty)"
    9.12  
    9.13  translations	
    9.14 -
    9.15 -  "prg"		=> "fst"
    9.16 -  "localT"	=> "snd"
    9.17 +  "prg"    => "fst"
    9.18 +  "localT" => "snd"
    9.19  
    9.20  consts
    9.21 -
    9.22 -  more_spec	:: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
    9.23 -		               (ty \\<times> 'x) \\<times> ty list => bool"
    9.24 -  appl_methds	:: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
    9.25 -  max_spec	:: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
    9.26 +  more_spec :: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
    9.27 +                (ty \\<times> 'x) \\<times> ty list => bool"
    9.28 +  appl_methds :: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
    9.29 +  max_spec :: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
    9.30  
    9.31  defs
    9.32 -
    9.33 -  more_spec_def	  "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
    9.34 -		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
    9.35 +  more_spec_def "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
    9.36 +		                            list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
    9.37    
    9.38    (* applicable methods, cf. 15.11.2.1 *)
    9.39    appl_methds_def "appl_methds G C == \\<lambda>(mn, pTs).
    9.40 @@ -51,11 +47,11 @@
    9.41  		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
    9.42  
    9.43    (* maximally specific methods, cf. 15.11.2.2 *)
    9.44 -   max_spec_def	  "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and> 
    9.45 -				          (\\<forall>m'\\<in>appl_methds G C sig.
    9.46 -				                   more_spec G m' m --> m' = m)}"
    9.47 +  max_spec_def "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and> 
    9.48 +                                      (\\<forall>m'\\<in>appl_methds G C sig.
    9.49 +                                        more_spec G m' m --> m' = m)}"
    9.50 +
    9.51  consts
    9.52 -
    9.53    typeof :: "(loc => ty option) => val => ty option"
    9.54  
    9.55  primrec
    9.56 @@ -70,16 +66,20 @@
    9.57  	(* method body with parameter names, local variables, block, result expression *)
    9.58  
    9.59  consts
    9.60 -
    9.61    ty_expr :: "java_mb env => (expr      \\<times> ty     ) set"
    9.62    ty_exprs:: "java_mb env => (expr list \\<times> ty list) set"
    9.63    wt_stmt :: "java_mb env =>  stmt                 set"
    9.64  
    9.65  syntax
    9.66 +  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \\<turnstile> _ :: _"   [51,51,51]50)
    9.67 +  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \\<turnstile> _ [::] _" [51,51,51]50)
    9.68 +  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ \\<turnstile> _ \\<surd>"      [51,51   ]50)
    9.69  
    9.70 -ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_\\<turnstile>_::_"  [51,51,51]50)
    9.71 -ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_\\<turnstile>_[::]_"[51,51,51]50)
    9.72 -wt_stmt :: "java_mb env =>  stmt                => bool" ("_\\<turnstile>_ \\<surd>" [51,51   ]50)
    9.73 +syntax (HTML)
    9.74 +  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
    9.75 +  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
    9.76 +  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
    9.77 +
    9.78  
    9.79  translations
    9.80  	"E\\<turnstile>e :: T" == "(e,T) \\<in> ty_expr  E"
    9.81 @@ -91,84 +91,84 @@
    9.82  (* well-typed expressions *)
    9.83  
    9.84    (* cf. 15.8 *)
    9.85 -  NewC	"[|is_class (prg E) C|] ==>
    9.86 -						 E\\<turnstile>NewC C::Class C"
    9.87 +  NewC	"[| is_class (prg E) C |] ==>
    9.88 +         E\\<turnstile>NewC C::Class C"
    9.89  
    9.90    (* cf. 15.15 *)
    9.91 -  Cast	"[|E\\<turnstile>e::Class C;
    9.92 -	  prg E\\<turnstile>C\\<preceq>? D|] ==>
    9.93 -						 E\\<turnstile>Cast D e::Class D"
    9.94 +  Cast  "[| E\\<turnstile>e::Class C;
    9.95 +            prg E\\<turnstile>C\\<preceq>? D |] ==>
    9.96 +         E\\<turnstile>Cast D e::Class D"
    9.97  
    9.98    (* cf. 15.7.1 *)
    9.99 -  Lit	"[|typeof (\\<lambda>v. None) x = Some T|] ==>
   9.100 -						 E\\<turnstile>Lit x::T"
   9.101 +  Lit	  "[| typeof (\\<lambda>v. None) x = Some T |] ==>
   9.102 +         E\\<turnstile>Lit x::T"
   9.103  
   9.104    
   9.105    (* cf. 15.13.1 *)
   9.106 -  LAcc	"[|localT E v = Some T; is_type (prg E) T|] ==>
   9.107 -						 E\\<turnstile>LAcc v::T"
   9.108 +  LAcc  "[| localT E v = Some T; is_type (prg E) T |] ==>
   9.109 +         E\\<turnstile>LAcc v::T"
   9.110  
   9.111 -  BinOp "[|E\\<turnstile>e1::T;
   9.112 -	  E\\<turnstile>e2::T;
   9.113 -	  if bop = Eq then T' = PrimT Boolean
   9.114 -	              else T' = T \\<and> T = PrimT Integer|] ==>
   9.115 -						 E\\<turnstile>BinOp bop e1 e2::T'"
   9.116 +  BinOp "[| E\\<turnstile>e1::T;
   9.117 +            E\\<turnstile>e2::T;
   9.118 +            if bop = Eq then T' = PrimT Boolean
   9.119 +                        else T' = T \\<and> T = PrimT Integer|] ==>
   9.120 +         E\\<turnstile>BinOp bop e1 e2::T'"
   9.121  
   9.122    (* cf. 15.25, 15.25.1 *)
   9.123 -  LAss  "[|E\\<turnstile>LAcc v::T;
   9.124 -	  E\\<turnstile>e::T';
   9.125 -	  prg E\\<turnstile>T'\\<preceq>T|] ==>
   9.126 -						 E\\<turnstile>v::=e::T'"
   9.127 +  LAss  "[| E\\<turnstile>LAcc v::T;
   9.128 +	          E\\<turnstile>e::T';
   9.129 +            prg E\\<turnstile>T'\\<preceq>T |] ==>
   9.130 +         E\\<turnstile>v::=e::T'"
   9.131  
   9.132    (* cf. 15.10.1 *)
   9.133 -  FAcc	"[|E\\<turnstile>a::Class C; 
   9.134 -	  field (prg E,C) fn = Some (fd,fT)|] ==>
   9.135 -						 E\\<turnstile>{fd}a..fn::fT"
   9.136 +  FAcc  "[| E\\<turnstile>a::Class C; 
   9.137 +            field (prg E,C) fn = Some (fd,fT) |] ==>
   9.138 +         E\\<turnstile>{fd}a..fn::fT"
   9.139  
   9.140    (* cf. 15.25, 15.25.1 *)
   9.141 -  FAss  "[|E\\<turnstile>{fd}a..fn::T;
   9.142 -	  E\\<turnstile>v       ::T';
   9.143 -	  prg E\\<turnstile>T'\\<preceq>T|] ==>
   9.144 -					 	 E\\<turnstile>{fd}a..fn:=v::T'"
   9.145 +  FAss  "[| E\\<turnstile>{fd}a..fn::T;
   9.146 +            E\\<turnstile>v        ::T';
   9.147 +            prg E\\<turnstile>T'\\<preceq>T |] ==>
   9.148 +         E\\<turnstile>{fd}a..fn:=v::T'"
   9.149  
   9.150  
   9.151    (* cf. 15.11.1, 15.11.2, 15.11.3 *)
   9.152 -  Call	"[|E\\<turnstile>a::Class C;
   9.153 -	  E\\<turnstile>ps[::]pTs;
   9.154 -	  max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}|] ==>
   9.155 -						 E\\<turnstile>a..mn({pTs'}ps)::rT"
   9.156 +  Call  "[| E\\<turnstile>a::Class C;
   9.157 +            E\\<turnstile>ps[::]pTs;
   9.158 +            max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
   9.159 +         E\\<turnstile>a..mn({pTs'}ps)::rT"
   9.160  
   9.161  (* well-typed expression lists *)
   9.162  
   9.163    (* cf. 15.11.??? *)
   9.164 -  Nil						"E\\<turnstile>[][::][]"
   9.165 +  Nil  "E\\<turnstile>[][::][]"
   9.166  
   9.167    (* cf. 15.11.??? *)
   9.168 -  Cons	"[|E\\<turnstile>e::T;
   9.169 -	   E\\<turnstile>es[::]Ts|] ==>
   9.170 -						 E\\<turnstile>e#es[::]T#Ts"
   9.171 +  Cons "[| E\\<turnstile>e::T;
   9.172 +           E\\<turnstile>es[::]Ts |] ==>
   9.173 +        E\\<turnstile>e#es[::]T#Ts"
   9.174  
   9.175  (* well-typed statements *)
   9.176  
   9.177 -  Skip					"E\\<turnstile>Skip\\<surd>"
   9.178 +  Skip "E\\<turnstile>Skip\\<surd>"
   9.179  
   9.180 -  Expr	"[|E\\<turnstile>e::T|] ==>
   9.181 -					 E\\<turnstile>Expr e\\<surd>"
   9.182 +  Expr "[| E\\<turnstile>e::T |] ==>
   9.183 +        E\\<turnstile>Expr e\\<surd>"
   9.184  
   9.185 -  Comp	"[|E\\<turnstile>s1\\<surd>; 
   9.186 -	  E\\<turnstile>s2\\<surd>|] ==>
   9.187 -					 E\\<turnstile>s1;; s2\\<surd>"
   9.188 +  Comp "[| E\\<turnstile>s1\\<surd>; 
   9.189 +           E\\<turnstile>s2\\<surd> |] ==>
   9.190 +        E\\<turnstile>s1;; s2\\<surd>"
   9.191  
   9.192    (* cf. 14.8 *)
   9.193 -  Cond	"[|E\\<turnstile>e::PrimT Boolean;
   9.194 -	  E\\<turnstile>s1\\<surd>;
   9.195 -	  E\\<turnstile>s2\\<surd>|] ==>
   9.196 -					 E\\<turnstile>If(e) s1 Else s2\\<surd>"
   9.197 +  Cond "[| E\\<turnstile>e::PrimT Boolean;
   9.198 +           E\\<turnstile>s1\\<surd>;
   9.199 +           E\\<turnstile>s2\\<surd> |] ==>
   9.200 +         E\\<turnstile>If(e) s1 Else s2\\<surd>"
   9.201  
   9.202    (* cf. 14.10 *)
   9.203 -  Loop "[|E\\<turnstile>e::PrimT Boolean;
   9.204 -	 E\\<turnstile>s\\<surd>|] ==>
   9.205 -					 E\\<turnstile>While(e) s\\<surd>"
   9.206 +  Loop "[| E\\<turnstile>e::PrimT Boolean;
   9.207 +           E\\<turnstile>s\\<surd> |] ==>
   9.208 +        E\\<turnstile>While(e) s\\<surd>"
   9.209  
   9.210  constdefs
   9.211