src/HOL/TLA/Memory/RPC.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 60592 c9bd1d902f04
child 62146 324bc1ffba12
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/TLA/Memory/RPC.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 section \<open>RPC-Memory example: RPC specification\<close>
     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 \<Rightarrow> rpcState) stfun"
    14 
    15 
    16 (* state predicates *)
    17 
    18 definition RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
    19   where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
    20 
    21 
    22 (* actions *)
    23 
    24 definition RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    25   where "RPCFwd send rcv rst p == ACT
    26       $(Calling send p)
    27     \<and> $(rst!p) = # rpcA
    28     \<and> IsLegalRcvArg<arg<$(send!p)>>
    29     \<and> Call rcv p RPCRelayArg<arg<send!p>>
    30     \<and> (rst!p)$ = # rpcB
    31     \<and> unchanged (rtrner send!p)"
    32 
    33 definition RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    34   where "RPCReject send rcv rst p == ACT
    35       $(rst!p) = # rpcA
    36     \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
    37     \<and> Return send p #BadCall
    38     \<and> unchanged ((rst!p), (caller rcv!p))"
    39 
    40 definition RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    41   where "RPCFail send rcv rst p == ACT
    42       \<not>$(Calling rcv p)
    43     \<and> Return send p #RPCFailure
    44     \<and> (rst!p)$ = #rpcA
    45     \<and> unchanged (caller rcv!p)"
    46 
    47 definition RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    48   where "RPCReply send rcv rst p == ACT
    49       \<not>$(Calling rcv p)
    50     \<and> $(rst!p) = #rpcB
    51     \<and> Return send p res<rcv!p>
    52     \<and> (rst!p)$ = #rpcA
    53     \<and> unchanged (caller rcv!p)"
    54 
    55 definition RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    56   where "RPCNext send rcv rst p == ACT
    57     (  RPCFwd send rcv rst p
    58      \<or> RPCReject send rcv rst p
    59      \<or> RPCFail send rcv rst p
    60      \<or> RPCReply send rcv rst p)"
    61 
    62 
    63 (* temporal *)
    64 
    65 definition RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
    66   where "RPCIPSpec send rcv rst p == TEMP
    67      Init RPCInit rcv rst p
    68    \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
    69    \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
    70 
    71 definition RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
    72   where "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
    73 
    74 
    75 lemmas RPC_action_defs =
    76   RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def
    77 
    78 lemmas RPC_temp_defs = RPCIPSpec_def RPCISpec_def
    79 
    80 
    81 (* The RPC component engages in an action for process p only if there is an outstanding,
    82    unanswered call for that process.
    83 *)
    84 
    85 lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
    86   by (auto simp: Return_def RPC_action_defs)
    87 
    88 lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
    89   by (auto simp: RPC_action_defs)
    90 
    91 (* RPC failure actions are visible. *)
    92 lemma RPCFail_vis: "\<turnstile> RPCFail send rcv rst p \<longrightarrow>  
    93     <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"
    94   by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def)
    95 
    96 lemma RPCFail_Next_enabled: "\<turnstile> Enabled (RPCFail send rcv rst p) \<longrightarrow>  
    97     Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"
    98   by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
    99 
   100 (* Enabledness of some actions *)
   101 lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
   102     \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
   103   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
   104     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
   105     [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   106 
   107 lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
   108       \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB  
   109          \<longrightarrow> Enabled (RPCReply send rcv rst p)"
   110   by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
   111     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
   112     [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   113 
   114 end