modernized specifications;
authorwenzelm
Fri Feb 18 16:36:42 2011 +0100 (2011-02-18)
changeset 417785f79a9e42507
parent 41777 1f7cbe39d425
child 41779 a68f503805ed
modernized specifications;
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Conform.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/Value.thy
src/HOL/Bali/WellType.thy
     1.1 --- a/src/HOL/Bali/AxSem.thy	Fri Feb 18 16:22:27 2011 +0100
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Fri Feb 18 16:36:42 2011 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4  \end{itemize}
     1.5  *}
     1.6  
     1.7 -types  res = vals --{* result entry *}
     1.8 +type_synonym  res = vals --{* result entry *}
     1.9  
    1.10  abbreviation (input)
    1.11    Val where "Val x == In1 x"
    1.12 @@ -58,7 +58,7 @@
    1.13    "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> CONST the_In3"
    1.14  
    1.15    --{* relation on result values, state and auxiliary variables *}
    1.16 -types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
    1.17 +type_synonym 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
    1.18  translations
    1.19    (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
    1.20  
    1.21 @@ -381,7 +381,7 @@
    1.22  datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
    1.23  something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
    1.24                                          ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
    1.25 -types    'a triples = "'a triple set"
    1.26 +type_synonym 'a triples = "'a triple set"
    1.27  
    1.28  abbreviation
    1.29    var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
     2.1 --- a/src/HOL/Bali/Conform.thy	Fri Feb 18 16:22:27 2011 +0100
     2.2 +++ b/src/HOL/Bali/Conform.thy	Fri Feb 18 16:36:42 2011 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4  \end{itemize}
     2.5  *}
     2.6  
     2.7 -types env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
     2.8 +type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
     2.9  
    2.10  
    2.11  section "extension of global store"
     3.1 --- a/src/HOL/Bali/Decl.thy	Fri Feb 18 16:22:27 2011 +0100
     3.2 +++ b/src/HOL/Bali/Decl.thy	Fri Feb 18 16:36:42 2011 +0100
     3.3 @@ -136,7 +136,7 @@
     3.4  
     3.5  
     3.6  subsubsection {* Static Modifier *}
     3.7 -types stat_modi = bool (* modifier: static *)
     3.8 +type_synonym stat_modi = bool (* modifier: static *)
     3.9  
    3.10  subsection {* Declaration (base "class" for member,interface and class
    3.11   declarations *}
    3.12 @@ -164,8 +164,7 @@
    3.13    (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
    3.14    (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
    3.15  
    3.16 -types     
    3.17 -        fdecl           (* field declaration, cf. 8.3 *)
    3.18 +type_synonym fdecl          (* field declaration, cf. 8.3 *)
    3.19          = "vname \<times> field"
    3.20  
    3.21  
    3.22 @@ -185,7 +184,7 @@
    3.23  record methd = mhead + (* method in a class *)
    3.24          mbody::mbody
    3.25  
    3.26 -types mdecl = "sig \<times> methd"  (* method declaration in a class *)
    3.27 +type_synonym mdecl = "sig \<times> methd"  (* method declaration in a class *)
    3.28  
    3.29  
    3.30  translations
    3.31 @@ -300,7 +299,7 @@
    3.32  
    3.33  record  iface = ibody + --{* interface *}
    3.34           isuperIfs:: "qtname list" --{* superinterface list *}
    3.35 -types
    3.36 +type_synonym
    3.37          idecl           --{* interface declaration, cf. 9.1 *}
    3.38          = "qtname \<times> iface"
    3.39  
    3.40 @@ -332,7 +331,7 @@
    3.41  record "class" = cbody +           --{* class *}
    3.42          super   :: "qtname"      --{* superclass *}
    3.43          superIfs:: "qtname list" --{* implemented interfaces *}
    3.44 -types
    3.45 +type_synonym
    3.46          cdecl           --{* class declaration, cf. 8.1 *}
    3.47          = "qtname \<times> class"
    3.48  
     4.1 --- a/src/HOL/Bali/DeclConcepts.thy	Fri Feb 18 16:22:27 2011 +0100
     4.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Fri Feb 18 16:36:42 2011 +0100
     4.3 @@ -1401,7 +1401,7 @@
     4.4  section "fields and methods"
     4.5  
     4.6  
     4.7 -types
     4.8 +type_synonym
     4.9    fspec = "vname \<times> qtname"
    4.10  
    4.11  translations 
     5.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Fri Feb 18 16:22:27 2011 +0100
     5.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Fri Feb 18 16:36:42 2011 +0100
     5.3 @@ -498,7 +498,7 @@
     5.4  section "The rules of definite assignment"
     5.5  
     5.6   
     5.7 -types breakass = "(label, lname) tables" 
     5.8 +type_synonym breakass = "(label, lname) tables" 
     5.9  --{* Mapping from a break label, to the set of variables that will be assigned 
    5.10       if the evaluation terminates with this break *}
    5.11      
     6.1 --- a/src/HOL/Bali/Eval.thy	Fri Feb 18 16:22:27 2011 +0100
     6.2 +++ b/src/HOL/Bali/Eval.thy	Fri Feb 18 16:36:42 2011 +0100
     6.3 @@ -96,8 +96,8 @@
     6.4  *}
     6.5  
     6.6  
     6.7 -types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
     6.8 -      vals  =        "(val, vvar, val list) sum3"
     6.9 +type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
    6.10 +type_synonym vals = "(val, vvar, val list) sum3"
    6.11  translations
    6.12    (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
    6.13    (type) "vals" <= (type) "(val, vvar, val list) sum3" 
     7.1 --- a/src/HOL/Bali/State.thy	Fri Feb 18 16:22:27 2011 +0100
     7.2 +++ b/src/HOL/Bali/State.thy	Fri Feb 18 16:36:42 2011 +0100
     7.3 @@ -27,7 +27,7 @@
     7.4                             since its type is given already by the reference to 
     7.5                             it (see below) *}
     7.6  
     7.7 -types   vn   = "fspec + int"                    --{* variable name      *}
     7.8 +type_synonym vn = "fspec + int"                 --{* variable name      *}
     7.9  record  obj  = 
    7.10            tag :: "obj_tag"                      --{* generalized object *}
    7.11            "values" :: "(vn, val) table"      
    7.12 @@ -130,7 +130,7 @@
    7.13  
    7.14  section "object references"
    7.15  
    7.16 -types oref = "loc + qtname"         --{* generalized object reference *}
    7.17 +type_synonym oref = "loc + qtname"         --{* generalized object reference *}
    7.18  syntax
    7.19    Heap  :: "loc   \<Rightarrow> oref"
    7.20    Stat  :: "qtname \<Rightarrow> oref"
    7.21 @@ -213,11 +213,11 @@
    7.22  
    7.23  section "stores"
    7.24  
    7.25 -types   globs               --{* global variables: heap and static variables *}
    7.26 +type_synonym globs               --{* global variables: heap and static variables *}
    7.27          = "(oref , obj) table"
    7.28 -        heap
    7.29 +type_synonym heap
    7.30          = "(loc  , obj) table"
    7.31 -(*      locals                   
    7.32 +(* type_synonym locals                   
    7.33          = "(lname, val) table" *) (* defined in Value.thy local variables *)
    7.34  
    7.35  translations
    7.36 @@ -579,7 +579,7 @@
    7.37  
    7.38  section "full program state"
    7.39  
    7.40 -types
    7.41 +type_synonym
    7.42    state = "abopt \<times> st"          --{* state including abruption information *}
    7.43  
    7.44  translations
     8.1 --- a/src/HOL/Bali/Table.thy	Fri Feb 18 16:22:27 2011 +0100
     8.2 +++ b/src/HOL/Bali/Table.thy	Fri Feb 18 16:36:42 2011 +0100
     8.3 @@ -29,9 +29,9 @@
     8.4  \end{itemize}
     8.5  *}
     8.6  
     8.7 -types ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
     8.8 +type_synonym ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
     8.9        = "'a \<rightharpoonup> 'b"
    8.10 -      ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
    8.11 +type_synonym ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
    8.12        = "'a \<Rightarrow> 'b set"
    8.13  
    8.14  
     9.1 --- a/src/HOL/Bali/Term.thy	Fri Feb 18 16:22:27 2011 +0100
     9.2 +++ b/src/HOL/Bali/Term.thy	Fri Feb 18 16:36:42 2011 +0100
     9.3 @@ -57,7 +57,7 @@
     9.4  
     9.5  
     9.6  
     9.7 -types locals = "(lname, val) table"  --{* local variables *}
     9.8 +type_synonym locals = "(lname, val) table"  --{* local variables *}
     9.9  
    9.10  
    9.11  datatype jump
    9.12 @@ -78,7 +78,7 @@
    9.13          | Jump jump   --{* break, continue, return *}
    9.14          | Error error -- {* runtime errors, we wan't to detect and proof absent
    9.15                              in welltyped programms *}
    9.16 -types
    9.17 +type_synonym
    9.18    abopt  = "abrupt option"
    9.19  
    9.20  text {* Local variable store and exception. 
    9.21 @@ -235,7 +235,7 @@
    9.22  intermediate steps of class-initialisation.
    9.23  *}
    9.24   
    9.25 -types "term" = "(expr+stmt,var,expr list) sum3"
    9.26 +type_synonym "term" = "(expr+stmt,var,expr list) sum3"
    9.27  translations
    9.28    (type) "sig"   <= (type) "mname \<times> ty list"
    9.29    (type) "term"  <= (type) "(expr+stmt,var,expr list) sum3"
    10.1 --- a/src/HOL/Bali/Value.thy	Fri Feb 18 16:22:27 2011 +0100
    10.2 +++ b/src/HOL/Bali/Value.thy	Fri Feb 18 16:36:42 2011 +0100
    10.3 @@ -26,7 +26,7 @@
    10.4  primrec the_Addr :: "val \<Rightarrow> loc"
    10.5    where "the_Addr (Addr a) = a"
    10.6  
    10.7 -types   dyn_ty      = "loc \<Rightarrow> ty option"
    10.8 +type_synonym dyn_ty = "loc \<Rightarrow> ty option"
    10.9  
   10.10  primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
   10.11  where
    11.1 --- a/src/HOL/Bali/WellType.thy	Fri Feb 18 16:22:27 2011 +0100
    11.2 +++ b/src/HOL/Bali/WellType.thy	Fri Feb 18 16:36:42 2011 +0100
    11.3 @@ -28,7 +28,7 @@
    11.4  \end{itemize}
    11.5  *}
    11.6  
    11.7 -types lenv
    11.8 +type_synonym lenv
    11.9          = "(lname, ty) table"  --{* local variables, including This and Result*}
   11.10  
   11.11  record env = 
   11.12 @@ -49,7 +49,7 @@
   11.13  
   11.14  section "Static overloading: maximally specific methods "
   11.15  
   11.16 -types
   11.17 +type_synonym
   11.18    emhead = "ref_ty \<times> mhead"
   11.19  
   11.20  --{* Some mnemotic selectors for emhead *}
   11.21 @@ -244,7 +244,7 @@
   11.22  
   11.23  section "Typing for terms"
   11.24  
   11.25 -types tys  = "ty + ty list"
   11.26 +type_synonym tys  = "ty + ty list"
   11.27  translations
   11.28    (type) "tys" <= (type) "ty + ty list"
   11.29