src/HOL/TLA/Memory/Memory.thy

 (*
     File:        Memory.thy
+    ID:          $Id$
     Author:      Stephan Merz
     Copyright:   1997 University of Munich
 
     Theory Name: Memory
     Logic Image: TLA
 
     RPC-Memory example: Memory specification
 *)
 
-Memory = MemoryParameters + ProcedureInterface +
+theory Memory
+imports MemoryParameters ProcedureInterface
+begin
 
 types
   memChType  = "(memOp, Vals) channel"
   memType = "(Locs => Vals) stfun"      (* intention: MemLocs => MemVals *)
   resType = "(PrIds => Vals) stfun"

 
   RSpec      :: "memChType => resType => temporal"
   USpec      :: "memChType => temporal"
 
   (* memory invariant: in the paper, the invariant is hidden in the definition of
-     the predicate S used in the implementation proof, but it is easier to verify 
+     the predicate S used in the implementation proof, but it is easier to verify
      at this level. *)
   MemInv    :: "memType => Locs => stpred"
 
-rules
-  MInit_def         "MInit mm l == PRED mm!l = #InitVal"
-  PInit_def         "PInit rs p == PRED rs!p = #NotAResult"
+defs
+  MInit_def:         "MInit mm l == PRED mm!l = #InitVal"
+  PInit_def:         "PInit rs p == PRED rs!p = #NotAResult"
 
-  RdRequest_def     "RdRequest ch p l == PRED
+  RdRequest_def:     "RdRequest ch p l == PRED
                          Calling ch p & (arg<ch!p> = #(read l))"
-  WrRequest_def     "WrRequest ch p l v == PRED
+  WrRequest_def:     "WrRequest ch p l v == PRED
                          Calling ch p & (arg<ch!p> = #(write l v))"
   (* a read that doesn't raise BadArg *)
-  GoodRead_def      "GoodRead mm rs p l == ACT
+  GoodRead_def:      "GoodRead mm rs p l == ACT
                         #l : #MemLoc & ((rs!p)$ = $(mm!l))"
   (* a read that raises BadArg *)
-  BadRead_def       "BadRead mm rs p l == ACT
+  BadRead_def:       "BadRead mm rs p l == ACT
                         #l ~: #MemLoc & ((rs!p)$ = #BadArg)"
   (* the read action with l visible *)
-  ReadInner_def     "ReadInner ch mm rs p l == ACT
+  ReadInner_def:     "ReadInner ch mm rs p l == ACT
                          $(RdRequest ch p l)
                          & (GoodRead mm rs p l  |  BadRead mm rs p l)
                          & unchanged (rtrner ch ! p)"
   (* the read action with l quantified *)
-  Read_def          "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
+  Read_def:          "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
 
   (* similar definitions for the write action *)
-  GoodWrite_def     "GoodWrite mm rs p l v == ACT
+  GoodWrite_def:     "GoodWrite mm rs p l v == ACT
                         #l : #MemLoc & #v : #MemVal
                         & ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
-  BadWrite_def      "BadWrite mm rs p l v == ACT
+  BadWrite_def:      "BadWrite mm rs p l v == ACT
                         ~ (#l : #MemLoc & #v : #MemVal)
                         & ((rs!p)$ = #BadArg) & unchanged (mm!l)"
-  WriteInner_def    "WriteInner ch mm rs p l v == ACT
+  WriteInner_def:    "WriteInner ch mm rs p l v == ACT
                         $(WrRequest ch p l v)
                         & (GoodWrite mm rs p l v  |  BadWrite mm rs p l v)
                         & unchanged (rtrner ch ! p)"
-  Write_def         "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
+  Write_def:         "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
 
   (* the return action *)
-  MemReturn_def     "MemReturn ch rs p == ACT
+  MemReturn_def:     "MemReturn ch rs p == ACT
                        (   ($(rs!p) ~= #NotAResult)
                         & ((rs!p)$ = #NotAResult)
                         & Return ch p (rs!p))"
 
   (* the failure action of the unreliable memory *)
-  MemFail_def       "MemFail ch rs p == ACT
+  MemFail_def:       "MemFail ch rs p == ACT
                         $(Calling ch p)
                         & ((rs!p)$ = #MemFailure)
                         & unchanged (rtrner ch ! p)"
   (* next-state relations for reliable / unreliable memory *)
-  RNext_def         "RNext ch mm rs p == ACT 
+  RNext_def:         "RNext ch mm rs p == ACT
                        (  Read ch mm rs p
                         | (EX l. Write ch mm rs p l)
                         | MemReturn ch rs p)"
-  UNext_def         "UNext ch mm rs p == ACT
+  UNext_def:         "UNext ch mm rs p == ACT
                         (RNext ch mm rs p | MemFail ch rs p)"
 
-  RPSpec_def        "RPSpec ch mm rs p == TEMP
+  RPSpec_def:        "RPSpec ch mm rs p == TEMP
                         Init(PInit rs p)
                         & [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
                         & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
                         & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
-  UPSpec_def        "UPSpec ch mm rs p == TEMP
+  UPSpec_def:        "UPSpec ch mm rs p == TEMP
                         Init(PInit rs p)
                         & [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
                         & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
                         & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
-  MSpec_def         "MSpec ch mm rs l == TEMP
+  MSpec_def:         "MSpec ch mm rs l == TEMP
                         Init(MInit mm l)
                         & [][ EX p. Write ch mm rs p l ]_(mm!l)"
-  IRSpec_def        "IRSpec ch mm rs == TEMP
+  IRSpec_def:        "IRSpec ch mm rs == TEMP
                         (ALL p. RPSpec ch mm rs p)
                         & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
-  IUSpec_def        "IUSpec ch mm rs == TEMP
+  IUSpec_def:        "IUSpec ch mm rs == TEMP
                         (ALL p. UPSpec ch mm rs p)
                         & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
 
-  RSpec_def         "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
-  USpec_def         "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
+  RSpec_def:         "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
+  USpec_def:         "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
 
-  MemInv_def        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
+  MemInv_def:        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
 end