src/HOL/TLA/Memory/RPC.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/RPC.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 header {* RPC-Memory example: RPC specification *}
     6 
     7 theory RPC
     8 imports RPCParameters ProcedureInterface Memory
     9 begin
    10 
    11 type_synonym rpcSndChType = "(rpcOp,Vals) channel"
    12 type_synonym rpcRcvChType = "memChType"
    13 type_synonym rpcStType = "(PrIds => rpcState) stfun"
    14 
    15 consts
    16   (* state predicates *)
    17   RPCInit      :: "rpcRcvChType => rpcStType => PrIds => stpred"
    18 
    19   (* actions *)
    20   RPCFwd     :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
    21   RPCReject  :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
    22   RPCFail    :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
    23   RPCReply   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
    24   RPCNext    :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
    25 
    26   (* temporal *)
    27   RPCIPSpec   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal"
    28   RPCISpec   :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
    29 
    30 defs
    31   RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
    32 
    33   RPCFwd_def:        "RPCFwd send rcv rst p == ACT
    34                          $(Calling send p)
    35                          & $(rst!p) = # rpcA
    36                          & IsLegalRcvArg<arg<$(send!p)>>
    37                          & Call rcv p RPCRelayArg<arg<send!p>>
    38                          & (rst!p)$ = # rpcB
    39                          & unchanged (rtrner send!p)"
    40 
    41   RPCReject_def:     "RPCReject send rcv rst p == ACT
    42                            $(rst!p) = # rpcA
    43                          & ~IsLegalRcvArg<arg<$(send!p)>>
    44                          & Return send p #BadCall
    45                          & unchanged ((rst!p), (caller rcv!p))"
    46 
    47   RPCFail_def:       "RPCFail send rcv rst p == ACT
    48                            ~$(Calling rcv p)
    49                          & Return send p #RPCFailure
    50                          & (rst!p)$ = #rpcA
    51                          & unchanged (caller rcv!p)"
    52 
    53   RPCReply_def:      "RPCReply send rcv rst p == ACT
    54                            ~$(Calling rcv p)
    55                          & $(rst!p) = #rpcB
    56                          & Return send p res<rcv!p>
    57                          & (rst!p)$ = #rpcA
    58                          & unchanged (caller rcv!p)"
    59 
    60   RPCNext_def:       "RPCNext send rcv rst p == ACT
    61                         (  RPCFwd send rcv rst p
    62                          | RPCReject send rcv rst p
    63                          | RPCFail send rcv rst p
    64                          | RPCReply send rcv rst p)"
    65 
    66   RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
    67                            Init RPCInit rcv rst p
    68                          & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
    69                          & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
    70 
    71   RPCISpec_def:      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
    72 
    73 
    74 lemmas RPC_action_defs =
    75   RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def
    76 
    77 lemmas RPC_temp_defs = RPCIPSpec_def RPCISpec_def
    78 
    79 
    80 (* The RPC component engages in an action for process p only if there is an outstanding,
    81    unanswered call for that process.
    82 *)
    83 
    84 lemma RPCidle: "|- ~$(Calling send p) --> ~RPCNext send rcv rst p"
    85   by (auto simp: Return_def RPC_action_defs)
    86 
    87 lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p"
    88   by (auto simp: RPC_action_defs)
    89 
    90 (* RPC failure actions are visible. *)
    91 lemma RPCFail_vis: "|- RPCFail send rcv rst p -->  
    92     <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"
    93   by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def)
    94 
    95 lemma RPCFail_Next_enabled: "|- Enabled (RPCFail send rcv rst p) -->  
    96     Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"
    97   by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
    98 
    99 (* Enabledness of some actions *)
   100 lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
   101     |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
   102   by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def},
   103     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
   104     [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   105 
   106 lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
   107       |- ~Calling rcv p & Calling send p & rst!p = #rpcB  
   108          --> Enabled (RPCReply send rcv rst p)"
   109   by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def},
   110     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
   111     [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   112 
   113 end