src/HOL/TLA/Memory/MemClerk.thy
author wenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 51717 9e7d1c139569
permissions -rw-r--r--
modernized specifications;
     1 (*  Title:      HOL/TLA/Memory/MemClerk.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 header {* RPC-Memory example: specification of the memory clerk *}
     6 
     7 theory MemClerk
     8 imports Memory RPC MemClerkParameters
     9 begin
    10 
    11 (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
    12 type_synonym mClkSndChType = "memChType"
    13 type_synonym mClkRcvChType = "rpcSndChType"
    14 type_synonym mClkStType = "(PrIds => mClkState) stfun"
    15 
    16 definition
    17   (* state predicates *)
    18   MClkInit      :: "mClkRcvChType => mClkStType => PrIds => stpred"
    19   where "MClkInit rcv cst p = PRED (cst!p = #clkA  &  ~Calling rcv p)"
    20 
    21 definition
    22   (* actions *)
    23   MClkFwd       :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    24   where "MClkFwd send rcv cst p = ACT
    25                            $Calling send p
    26                          & $(cst!p) = #clkA
    27                          & Call rcv p MClkRelayArg<arg<send!p>>
    28                          & (cst!p)$ = #clkB
    29                          & unchanged (rtrner send!p)"
    30 
    31 definition
    32   MClkRetry     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    33   where "MClkRetry send rcv cst p = ACT
    34                            $(cst!p) = #clkB
    35                          & res<$(rcv!p)> = #RPCFailure
    36                          & Call rcv p MClkRelayArg<arg<send!p>>
    37                          & unchanged (cst!p, rtrner send!p)"
    38 
    39 definition
    40   MClkReply     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    41   where "MClkReply send rcv cst p = ACT
    42                            ~$Calling rcv p
    43                          & $(cst!p) = #clkB
    44                          & Return send p MClkReplyVal<res<rcv!p>>
    45                          & (cst!p)$ = #clkA
    46                          & unchanged (caller rcv!p)"
    47 
    48 definition
    49   MClkNext      :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    50   where "MClkNext send rcv cst p = ACT
    51                         (  MClkFwd send rcv cst p
    52                          | MClkRetry send rcv cst p
    53                          | MClkReply send rcv cst p)"
    54 
    55 definition
    56   (* temporal *)
    57   MClkIPSpec    :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal"
    58   where "MClkIPSpec send rcv cst p = TEMP
    59                            Init MClkInit rcv cst p
    60                          & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
    61                          & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
    62                          & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
    63 
    64 definition
    65   MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
    66   where "MClkISpec send rcv cst = TEMP (ALL p. MClkIPSpec send rcv cst p)"
    67 
    68 lemmas MC_action_defs =
    69   MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def
    70 
    71 lemmas MC_temp_defs = MClkIPSpec_def MClkISpec_def
    72 
    73 (* The Clerk engages in an action for process p only if there is an outstanding,
    74    unanswered call for that process.
    75 *)
    76 lemma MClkidle: "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p"
    77   by (auto simp: Return_def MC_action_defs)
    78 
    79 lemma MClkbusy: "|- $Calling rcv p --> ~MClkNext send rcv cst p"
    80   by (auto simp: Call_def MC_action_defs)
    81 
    82 
    83 (* Enabledness of actions *)
    84 
    85 lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
    86       |- Calling send p & ~Calling rcv p & cst!p = #clkA   
    87          --> Enabled (MClkFwd send rcv cst p)"
    88   by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
    89     @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
    90     [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
    91 
    92 lemma MClkFwd_ch_enabled: "|- Enabled (MClkFwd send rcv cst p)  -->   
    93          Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
    94   by (auto elim!: enabled_mono simp: angle_def MClkFwd_def)
    95 
    96 lemma MClkReply_change: "|- MClkReply send rcv cst p -->  
    97          <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"
    98   by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use])
    99 
   100 lemma MClkReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
   101       |- Calling send p & ~Calling rcv p & cst!p = #clkB   
   102          --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
   103   apply (tactic {* action_simp_tac @{simpset}
   104     [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
   105   apply (tactic {* action_simp_tac (@{simpset} addsimps
   106     [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
   107     [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   108   done
   109 
   110 lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"
   111   by (auto simp: MClkReply_def MClkRetry_def)
   112 
   113 end