
diff -r f6335d319e9f -r db63752140c7 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Feb 08 13:02:42 1999 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Feb 08 13:02:56 1999 +0100
@@ -9,7 +9,9 @@
     RPC-Memory example: Memory implementation
 *)
 
-MemoryImplementation = Memory + RPC + MemClerk + MIParameters +
+MemoryImplementation = Memory + RPC + MemClerk + Datatype +
+
+datatype  histState  =  histA | histB
 
 types
   histType  = "(PrIds => histState) stfun"     (* the type of the history variable *)
@@ -19,8 +21,7 @@
      (* channel (external) *)
   memCh         :: "memChType"
      (* internal variables *)
-  mem           :: "memType"
-  resbar        :: "histType => resType"        (* defined by refinement mapping *)
+  mm            :: "memType"
   
   (* the state variables of the implementation *)
      (* channels *)
@@ -28,7 +29,7 @@
   crCh          :: "rpcSndChType"
   rmCh          :: "rpcRcvChType"
      (* internal variables *)
-  (* identity refinement mapping for mem -- simply reused *)
+  (* identity refinement mapping for mm -- simply reused *)
   rst           :: "rpcStType"
   cst           :: "mClkStType"
   ires          :: "resType"
@@ -36,153 +37,145 @@
   rmhist        :: "histType"
 *)
 
+constdefs
+  (* auxiliary predicates *)
+  MVOKBARF      :: "Vals => bool"
+     "MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
+  MVOKBA        :: "Vals => bool"
+     "MVOKBA v   == (v : MemVal) | (v = OK) | (v = BadArg)"
+  MVNROKBA      :: "Vals => bool"
+     "MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
+
+  (* tuples of state functions changed by the various components *)
+  e             :: "PrIds => (bit * memOp) stfun"
+     "e p == PRED (caller memCh!p)"
+  c             :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
+     "c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)"
+  r             :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun"
+     "r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
+  m             :: "PrIds => ((bit * Vals) * Vals) stfun"
+     "m p == PRED (rtrner rmCh!p, ires!p)"
+
   (* the environment action *)
   ENext         :: "PrIds => action"
+     "ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
+
 
   (* specification of the history variable *)
   HInit         :: "histType => PrIds => stpred"
+     "HInit rmhist p == PRED rmhist!p = #histA"
+
   HNext         :: "histType => PrIds => action"
+     "HNext rmhist p == ACT (rmhist!p)$ =
+                     (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
+                      then #histB
+                      else if (MClkReply memCh crCh cst p)
+                           then #histA
+                           else $(rmhist!p))"
+
   HistP         :: "histType => PrIds => temporal"
+     "HistP rmhist p == TEMP Init HInit rmhist p
+                           & [][HNext rmhist p]_(c p,r p,m p, rmhist!p)"
+
   Hist          :: "histType => temporal"
+      "Hist rmhist == TEMP (!p. HistP rmhist p)"
 
   (* the implementation *)
+  IPImp          :: "PrIds => temporal"
+     "IPImp p == TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
+	               & MClkIPSpec memCh crCh cst p
+  	               & RPCIPSpec crCh rmCh rst p
+	               & RPSpec rmCh mm ires p
+		       & (! l. #l : #MemLoc --> MSpec rmCh mm ires l))"
+
   ImpInit        :: "PrIds => stpred"
+      "ImpInit p == PRED (  ~Calling memCh p
+                          & MClkInit crCh cst p
+	                  & RPCInit rmCh rst p
+	                  & PInit ires p)"
+
   ImpNext        :: "PrIds => action"
+      "ImpNext p == ACT  [ENext p]_(e p) 
+                       & [MClkNext memCh crCh cst p]_(c p)
+                       & [RPCNext crCh rmCh rst p]_(r p) 
+                       & [RNext rmCh mm ires p]_(m p)"
+
   ImpLive        :: "PrIds => temporal"
-  IPImp          :: "PrIds => temporal"
+      "ImpLive p == TEMP  WF(MClkFwd memCh crCh cst p)_(c p) 
+			& SF(MClkReply memCh crCh cst p)_(c p)
+			& WF(RPCNext crCh rmCh rst p)_(r p) 
+			& WF(RNext rmCh mm ires p)_(m p)
+			& WF(MemReturn rmCh ires p)_(m p)"
+
   Implementation :: "temporal"
-  ImpInv         :: "histType => PrIds => stpred"
-
-  (* tuples of state functions changed by the various components *)
-  e             :: "PrIds => (bit * memArgType) stfun"
-  c             :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcArgType)) stfun"
-  r             :: "PrIds => (rpcState * (bit * Vals) * (bit * memArgType)) stfun"
-  m             :: "PrIds => ((bit * Vals) * Vals) stfun"
+      "Implementation == TEMP ( (!p. Init (~Calling memCh p) & [][ENext p]_(e p))
+                               & MClkISpec memCh crCh cst
+                               & RPCISpec crCh rmCh rst
+                               & IRSpec rmCh mm ires)"
 
   (* the predicate S describes the states of the implementation.
-     slight simplification: two "histState" parameters instead of a (one- or
-     two-element) set. *)
-  S             :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
+     slight simplification: two "histState" parameters instead of a
+     (one- or two-element) set.
+     NB: The second conjunct of the definition in the paper is taken care of by
+     the type definitions. The last conjunct is asserted separately as the memory
+     invariant MemInv, proved in Memory.ML. *)
+  S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
+      "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
+                Calling memCh p = #ecalling
+              & Calling crCh p  = #ccalling
+              & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
+              & (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
+              & Calling rmCh p  = #rcalling
+              & (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
+              & (~ #rcalling --> ires!p = #NotAResult)
+              & (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
+              & cst!p = #cs
+              & rst!p = #rs
+              & (rmhist!p = #hs1 | rmhist!p = #hs2)
+              & MVNROKBA<ires!p>"
 
   (* predicates S1 -- S6 define special instances of S *)
   S1            :: "histType => PrIds => stpred"
+      "S1 rmhist p == S rmhist False False False clkA rpcA histA histA p"
   S2            :: "histType => PrIds => stpred"
+      "S2 rmhist p == S rmhist True False False clkA rpcA histA histA p"
   S3            :: "histType => PrIds => stpred"
+      "S3 rmhist p == S rmhist True True False clkB rpcA histA histB p"
   S4            :: "histType => PrIds => stpred"
+      "S4 rmhist p == S rmhist True True True clkB rpcB histA histB p"
   S5            :: "histType => PrIds => stpred"
+      "S5 rmhist p == S rmhist True True False clkB rpcB histB histB p"
   S6            :: "histType => PrIds => stpred"
+      "S6 rmhist p == S rmhist True False False clkB rpcA histB histB p"
 
-  (* auxiliary predicates *)
-  MVOKBARF      :: "Vals => bool"
-  MVOKBA        :: "Vals => bool"
-  MVNROKBA      :: "Vals => bool"
+  (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
+  ImpInv         :: "histType => PrIds => stpred"
+      "ImpInv rmhist p == PRED (  S1 rmhist p | S2 rmhist p | S3 rmhist p
+				| S4 rmhist p | S5 rmhist p | S6 rmhist p)"
+
+  resbar        :: "histType => resType"        (* refinement mapping *)
+      "resbar rmhist s p == 
+                  (if (S1 rmhist p s | S2 rmhist p s)
+                   then ires s p
+                   else if S3 rmhist p s
+                   then if rmhist s p = histA 
+                        then ires s p else MemFailure
+                   else if S4 rmhist p s
+                   then if (rmhist s p = histB & ires s p = NotAResult)
+                        then MemFailure else ires s p
+                   else if S5 rmhist p s
+                   then res (rmCh s p)
+                   else if S6 rmhist p s
+                   then if res (crCh s p) = RPCFailure
+                        then MemFailure else res (crCh s p)
+                   else NotAResult)" (* dummy value *)
 
 rules
-  MVOKBARF_def  "MVOKBARF v == (MemVal v) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
-  MVOKBA_def    "MVOKBA v   == (MemVal v) | (v = OK) | (v = BadArg)"
-  MVNROKBA_def  "MVNROKBA v == (MemVal v) | (v = NotAResult) | (v = OK) | (v = BadArg)"
-
   (* the "base" variables: everything except resbar and hist (for any index) *)
-  MI_base       "base_var <caller memCh @ p, rtrner memCh @ p, 
-                           caller crCh @ p, rtrner crCh @ p,
-                           caller rmCh @ p, rtrner rmCh @ p,
-                           rst@p, cst@p, mem@l, ires@p>"
-
-  (* Environment's next-state relation *)
-  ENext_def     "ENext p == REX l. #(MemLoc l) .& Call memCh p (#(Inl (read,l)))"
-
-  (* Specification of the history variable used in the proof *)
-  HInit_def     "$(HInit rmhist p) .= ($(rmhist@p) .= #histA)"
-  HNext_def     "HNext rmhist p == 
-                   (rmhist@p)$ .=
-                     (.if (MemReturn rmCh ires p .| RPCFail crCh rmCh rst p)
-                      .then #histB
-                      .else .if (MClkReply memCh crCh cst p)
-                            .then #histA
-                            .else $(rmhist@p))"
-  HistP_def     "HistP rmhist p == 
-                    Init($(HInit rmhist p))
-                    .& [][HNext rmhist p]_<c p,r p,m p, rmhist@p>"
-  Hist_def      "Hist rmhist == RALL p. HistP rmhist p"
-
-  (* definitions of e,c,r,m *)
-  e_def         "e p == caller memCh @ p"
-  c_def         "c p == <cst@p, rtrner memCh @ p, caller crCh @ p>"
-  r_def         "r p == <rst@p, rtrner crCh @ p, caller rmCh @ p>"
-  m_def         "m p == <rtrner rmCh @ p, ires@p>"
-
-  (* definition of the implementation (without the history variable) *)
-  IPImp_def     "IPImp p ==    Init(.~ $(Calling memCh p)) .& [][ENext p]_(e p)
-			           .& MClkIPSpec memCh crCh cst p
-			           .& RPCIPSpec crCh rmCh rst p
-			           .& RPSpec rmCh mem ires p 
-			           .& (RALL l. #(MemLoc l) .-> MSpec rmCh mem ires l)"
-
-  ImpInit_def   "$(ImpInit p) .= (   .~ $(Calling memCh p)    \
-\		                  .& $(MClkInit crCh cst p)   \
-\		                  .& $(RPCInit rmCh rst p)   \
-\		                  .& $(PInit ires p))"
-
-  ImpNext_def   "ImpNext p ==   [ENext p]_(e p) 
-                             .& [MClkNext memCh crCh cst p]_(c p)
-                             .& [RPCNext crCh rmCh rst p]_(r p) 
-                             .& [RNext rmCh mem ires p]_(m p)"
-
-  ImpLive_def  "ImpLive p ==   WF(MClkFwd memCh crCh cst p)_(c p) 
-			    .& SF(MClkReply memCh crCh cst p)_(c p)
-			    .& WF(RPCNext crCh rmCh rst p)_(r p) 
-			    .& WF(RNext rmCh mem ires p)_(m p)
-			    .& WF(MemReturn rmCh ires p)_(m p)"
-
-  Impl_def   "Implementation ==    (RALL p. Init(.~ $(Calling memCh p)) .& [][ENext p]_(e p))
-                                .& MClkISpec memCh crCh cst
-                                .& RPCISpec crCh rmCh rst
-                                .& IRSpec rmCh mem ires"
-
-  ImpInv_def "$(ImpInv rmhist p) .= ($(S1 rmhist p) .| $(S2 rmhist p) .| $(S3 rmhist p) .| 
-                                     $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p))"
-
-  (* Definition of predicate S.
-     NB: The second conjunct of the definition in the paper is taken care of by
-     the type definitions. The last conjunct is asserted separately as the memory
-     invariant MemInv, proved in Memory.ML. *)
-  S_def    "$(S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p) .=
-              (  ($(Calling memCh p) .= # ecalling)
-              .& ($(Calling crCh p) .= # ccalling)
-              .& (# ccalling .-> (arg[ $(crCh@p)] .= MClkRelayArg[ arg[$(memCh@p)] ]))
-              .& ((.~ # ccalling .& ($(cst@p) .= # clkB)) .-> MVOKBARF[ res[$(crCh@p)] ])
-              .& ($(Calling rmCh p) .= # rcalling)
-              .& (# rcalling .-> (arg[ $(rmCh@p)] .= RPCRelayArg[ arg[$(crCh@p)] ]))
-              .& (.~ # rcalling .-> ($(ires@p) .= # NotAResult))
-              .& ((.~ # rcalling .& ($(rst@p) .= # rpcB)) .-> MVOKBA[ res[$(rmCh@p)] ])
-              .& ($(cst@p) .= # cs)
-              .& ($(rst@p) .= # rs)
-              .& (($(rmhist@p) .= #hs1) .| ($(rmhist@p) .= #hs2))
-              .& (MVNROKBA[ $(ires@p)]))"
-
-  S1_def   "$(S1 rmhist p) .= $(S rmhist False False False clkA rpcA histA histA p)"
-  S2_def   "$(S2 rmhist p) .= $(S rmhist True False False clkA rpcA histA histA p)"
-  S3_def   "$(S3 rmhist p) .= $(S rmhist True True False clkB rpcA histA histB p)"
-  S4_def   "$(S4 rmhist p) .= $(S rmhist True True True clkB rpcB histA histB p)"
-  S5_def   "$(S5 rmhist p) .= $(S rmhist True True False clkB rpcB histB histB p)"
-  S6_def   "$(S6 rmhist p) .= $(S rmhist True False False clkB rpcA histB histB p)"
-
-  (* Definition of the refinement mapping resbar for result *)
-  resbar_def   "$((resbar rmhist) @ p) .=
-                  (.if ($(S1 rmhist p) .| $(S2 rmhist p))
-                   .then $(ires@p)
-                   .else .if $(S3 rmhist p)
-                   .then .if $(rmhist@p) .= #histA 
-                         .then $(ires@p) .else # MemFailure
-                   .else .if $(S4 rmhist p)
-                   .then .if ($(rmhist@p) .= #histB) .& ($(ires@p) .= # NotAResult)
-                         .then #MemFailure .else $(ires@p)
-                   .else .if $(S5 rmhist p)
-                   .then res[$(rmCh@p)]
-                   .else .if $(S6 rmhist p)
-                   .then .if res[$(crCh@p)] .= #RPCFailure
-                         .then #MemFailure .else res[$(crCh@p)]
-                   .else #NotAResult)" (* dummy value *)
+  MI_base       "basevars (caller memCh!p,
+			   (rtrner memCh!p, caller crCh!p, cst!p),
+			   (rtrner crCh!p, caller rmCh!p, rst!p),
+			   (mm!l, rtrner rmCh!p, ires!p))"
 
 end
 




