modernized specifications;
authorwenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018878f33040280
parent 42017 0d4bedb25fc9
child 42032 143f37194911
modernized specifications;
src/HOL/TLA/Action.thy
src/HOL/TLA/Init.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Memory/MemClerk.thy
src/HOL/TLA/Memory/MemClerkParameters.thy
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/Memory/RPC.thy
src/HOL/TLA/Memory/RPCMemoryParams.thy
src/HOL/TLA/Stfun.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Sun Mar 20 22:48:08 2011 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Sun Mar 20 23:07:06 2011 +0100
     1.3 @@ -12,9 +12,8 @@
     1.4  
     1.5  (** abstract syntax **)
     1.6  
     1.7 -types
     1.8 -  'a trfun = "(state * state) => 'a"
     1.9 -  action   = "bool trfun"
    1.10 +type_synonym 'a trfun = "(state * state) => 'a"
    1.11 +type_synonym action   = "bool trfun"
    1.12  
    1.13  arities prod :: (world, world) world
    1.14  
     2.1 --- a/src/HOL/TLA/Init.thy	Sun Mar 20 22:48:08 2011 +0100
     2.2 +++ b/src/HOL/TLA/Init.thy	Sun Mar 20 23:07:06 2011 +0100
     2.3 @@ -14,8 +14,7 @@
     2.4  typedecl behavior
     2.5  arities behavior :: world
     2.6  
     2.7 -types
     2.8 -  temporal = "behavior form"
     2.9 +type_synonym temporal = "behavior form"
    2.10  
    2.11  
    2.12  consts
     3.1 --- a/src/HOL/TLA/Intensional.thy	Sun Mar 20 22:48:08 2011 +0100
     3.2 +++ b/src/HOL/TLA/Intensional.thy	Sun Mar 20 23:07:06 2011 +0100
     3.3 @@ -15,9 +15,8 @@
     3.4  
     3.5  (** abstract syntax **)
     3.6  
     3.7 -types
     3.8 -  ('w,'a) expr = "'w => 'a"               (* intention: 'w::world, 'a::type *)
     3.9 -  'w form = "('w, bool) expr"
    3.10 +type_synonym ('w,'a) expr = "'w => 'a"   (* intention: 'w::world, 'a::type *)
    3.11 +type_synonym 'w form = "('w, bool) expr"
    3.12  
    3.13  consts
    3.14    Valid    :: "('w::world) form => bool"
     4.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Sun Mar 20 22:48:08 2011 +0100
     4.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Sun Mar 20 23:07:06 2011 +0100
     4.3 @@ -8,11 +8,10 @@
     4.4  imports Memory RPC MemClerkParameters
     4.5  begin
     4.6  
     4.7 -types
     4.8 -  (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
     4.9 -  mClkSndChType = "memChType"
    4.10 -  mClkRcvChType = "rpcSndChType"
    4.11 -  mClkStType    = "(PrIds => mClkState) stfun"
    4.12 +(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
    4.13 +type_synonym mClkSndChType = "memChType"
    4.14 +type_synonym mClkRcvChType = "rpcSndChType"
    4.15 +type_synonym mClkStType = "(PrIds => mClkState) stfun"
    4.16  
    4.17  definition
    4.18    (* state predicates *)
     5.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Mar 20 22:48:08 2011 +0100
     5.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Mar 20 23:07:06 2011 +0100
     5.3 @@ -10,11 +10,10 @@
     5.4  
     5.5  datatype mClkState = clkA | clkB
     5.6  
     5.7 -types
     5.8 -  (* types sent on the clerk's send and receive channels are argument types
     5.9 -     of the memory and the RPC, respectively *)
    5.10 -  mClkSndArgType   = "memOp"
    5.11 -  mClkRcvArgType   = "rpcOp"
    5.12 +(* types sent on the clerk's send and receive channels are argument types
    5.13 +   of the memory and the RPC, respectively *)
    5.14 +type_synonym mClkSndArgType = "memOp"
    5.15 +type_synonym mClkRcvArgType = "rpcOp"
    5.16  
    5.17  definition
    5.18    (* translate a memory call to an RPC call *)
     6.1 --- a/src/HOL/TLA/Memory/Memory.thy	Sun Mar 20 22:48:08 2011 +0100
     6.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Sun Mar 20 23:07:06 2011 +0100
     6.3 @@ -8,10 +8,9 @@
     6.4  imports MemoryParameters ProcedureInterface
     6.5  begin
     6.6  
     6.7 -types
     6.8 -  memChType  = "(memOp, Vals) channel"
     6.9 -  memType = "(Locs => Vals) stfun"      (* intention: MemLocs => MemVals *)
    6.10 -  resType = "(PrIds => Vals) stfun"
    6.11 +type_synonym memChType = "(memOp, Vals) channel"
    6.12 +type_synonym memType = "(Locs => Vals) stfun"  (* intention: MemLocs => MemVals *)
    6.13 +type_synonym resType = "(PrIds => Vals) stfun"
    6.14  
    6.15  consts
    6.16    (* state predicates *)
     7.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Mar 20 22:48:08 2011 +0100
     7.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Mar 20 23:07:06 2011 +0100
     7.3 @@ -10,8 +10,7 @@
     7.4  
     7.5  datatype histState = histA | histB
     7.6  
     7.7 -types
     7.8 -  histType  = "(PrIds => histState) stfun"     (* the type of the history variable *)
     7.9 +type_synonym histType = "(PrIds => histState) stfun"  (* the type of the history variable *)
    7.10  
    7.11  consts
    7.12    (* the specification *)
     8.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Mar 20 22:48:08 2011 +0100
     8.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Sun Mar 20 23:07:06 2011 +0100
     8.3 @@ -8,15 +8,13 @@
     8.4  imports "../TLA" RPCMemoryParams
     8.5  begin
     8.6  
     8.7 -typedecl
     8.8 +typedecl ('a,'r) chan
     8.9    (* type of channels with argument type 'a and return type 'r.
    8.10       we model a channel as an array of variables (of type chan)
    8.11       rather than a single array-valued variable because the
    8.12       notation gets a little simpler.
    8.13    *)
    8.14 -  ('a,'r) chan
    8.15 -types
    8.16 -  ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
    8.17 +type_synonym ('a,'r) channel =" (PrIds => ('a,'r) chan) stfun"
    8.18  
    8.19  consts
    8.20    (* data-level functions *)
     9.1 --- a/src/HOL/TLA/Memory/RPC.thy	Sun Mar 20 22:48:08 2011 +0100
     9.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Sun Mar 20 23:07:06 2011 +0100
     9.3 @@ -8,10 +8,9 @@
     9.4  imports RPCParameters ProcedureInterface Memory
     9.5  begin
     9.6  
     9.7 -types
     9.8 -  rpcSndChType  = "(rpcOp,Vals) channel"
     9.9 -  rpcRcvChType  = "memChType"
    9.10 -  rpcStType     = "(PrIds => rpcState) stfun"
    9.11 +type_synonym rpcSndChType = "(rpcOp,Vals) channel"
    9.12 +type_synonym rpcRcvChType = "memChType"
    9.13 +type_synonym rpcStType = "(PrIds => rpcState) stfun"
    9.14  
    9.15  consts
    9.16    (* state predicates *)
    10.1 --- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Mar 20 22:48:08 2011 +0100
    10.2 +++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Sun Mar 20 23:07:06 2011 +0100
    10.3 @@ -8,10 +8,10 @@
    10.4  imports Main
    10.5  begin
    10.6  
    10.7 -types
    10.8 -  bit = "bool"   (* Signal wires for the procedure interface.
    10.9 -                    Defined as bool for simplicity. All I should really need is
   10.10 -                    the existence of two distinct values. *)
   10.11 +type_synonym bit = "bool"
   10.12 + (* Signal wires for the procedure interface.
   10.13 +    Defined as bool for simplicity. All I should really need is
   10.14 +    the existence of two distinct values. *)
   10.15  
   10.16  (* all of these are simple (HOL) types *)
   10.17  typedecl Locs    (* "syntactic" value type *)
    11.1 --- a/src/HOL/TLA/Stfun.thy	Sun Mar 20 22:48:08 2011 +0100
    11.2 +++ b/src/HOL/TLA/Stfun.thy	Sun Mar 20 23:07:06 2011 +0100
    11.3 @@ -13,9 +13,8 @@
    11.4  
    11.5  arities state :: world
    11.6  
    11.7 -types
    11.8 -  'a stfun = "state => 'a"
    11.9 -  stpred  = "bool stfun"
   11.10 +type_synonym 'a stfun = "state => 'a"
   11.11 +type_synonym stpred  = "bool stfun"
   11.12  
   11.13  
   11.14  consts