src/HOL/TLA/Memory/RPC.thy
changeset 62145 5b946c81dfbf
parent 60592 c9bd1d902f04
child 62146 324bc1ffba12
     1.1 --- a/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -12,63 +12,64 @@
     1.4  type_synonym rpcRcvChType = "memChType"
     1.5  type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun"
     1.6  
     1.7 -consts
     1.8 -  (* state predicates *)
     1.9 -  RPCInit      :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
    1.10 +
    1.11 +(* state predicates *)
    1.12  
    1.13 -  (* actions *)
    1.14 -  RPCFwd     :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.15 -  RPCReject  :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.16 -  RPCFail    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.17 -  RPCReply   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.18 -  RPCNext    :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.19 +definition RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
    1.20 +  where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
    1.21 +
    1.22 +
    1.23 +(* actions *)
    1.24  
    1.25 -  (* temporal *)
    1.26 -  RPCIPSpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
    1.27 -  RPCISpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
    1.28 -
    1.29 -defs
    1.30 -  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
    1.31 +definition RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.32 +  where "RPCFwd send rcv rst p == ACT
    1.33 +      $(Calling send p)
    1.34 +    \<and> $(rst!p) = # rpcA
    1.35 +    \<and> IsLegalRcvArg<arg<$(send!p)>>
    1.36 +    \<and> Call rcv p RPCRelayArg<arg<send!p>>
    1.37 +    \<and> (rst!p)$ = # rpcB
    1.38 +    \<and> unchanged (rtrner send!p)"
    1.39  
    1.40 -  RPCFwd_def:        "RPCFwd send rcv rst p == ACT
    1.41 -                         $(Calling send p)
    1.42 -                         \<and> $(rst!p) = # rpcA
    1.43 -                         \<and> IsLegalRcvArg<arg<$(send!p)>>
    1.44 -                         \<and> Call rcv p RPCRelayArg<arg<send!p>>
    1.45 -                         \<and> (rst!p)$ = # rpcB
    1.46 -                         \<and> unchanged (rtrner send!p)"
    1.47 +definition RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.48 +  where "RPCReject send rcv rst p == ACT
    1.49 +      $(rst!p) = # rpcA
    1.50 +    \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
    1.51 +    \<and> Return send p #BadCall
    1.52 +    \<and> unchanged ((rst!p), (caller rcv!p))"
    1.53  
    1.54 -  RPCReject_def:     "RPCReject send rcv rst p == ACT
    1.55 -                           $(rst!p) = # rpcA
    1.56 -                         \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
    1.57 -                         \<and> Return send p #BadCall
    1.58 -                         \<and> unchanged ((rst!p), (caller rcv!p))"
    1.59 +definition RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.60 +  where "RPCFail send rcv rst p == ACT
    1.61 +      \<not>$(Calling rcv p)
    1.62 +    \<and> Return send p #RPCFailure
    1.63 +    \<and> (rst!p)$ = #rpcA
    1.64 +    \<and> unchanged (caller rcv!p)"
    1.65  
    1.66 -  RPCFail_def:       "RPCFail send rcv rst p == ACT
    1.67 -                           \<not>$(Calling rcv p)
    1.68 -                         \<and> Return send p #RPCFailure
    1.69 -                         \<and> (rst!p)$ = #rpcA
    1.70 -                         \<and> unchanged (caller rcv!p)"
    1.71 +definition RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.72 +  where "RPCReply send rcv rst p == ACT
    1.73 +      \<not>$(Calling rcv p)
    1.74 +    \<and> $(rst!p) = #rpcB
    1.75 +    \<and> Return send p res<rcv!p>
    1.76 +    \<and> (rst!p)$ = #rpcA
    1.77 +    \<and> unchanged (caller rcv!p)"
    1.78  
    1.79 -  RPCReply_def:      "RPCReply send rcv rst p == ACT
    1.80 -                           \<not>$(Calling rcv p)
    1.81 -                         \<and> $(rst!p) = #rpcB
    1.82 -                         \<and> Return send p res<rcv!p>
    1.83 -                         \<and> (rst!p)$ = #rpcA
    1.84 -                         \<and> unchanged (caller rcv!p)"
    1.85 +definition RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
    1.86 +  where "RPCNext send rcv rst p == ACT
    1.87 +    (  RPCFwd send rcv rst p
    1.88 +     \<or> RPCReject send rcv rst p
    1.89 +     \<or> RPCFail send rcv rst p
    1.90 +     \<or> RPCReply send rcv rst p)"
    1.91 +
    1.92  
    1.93 -  RPCNext_def:       "RPCNext send rcv rst p == ACT
    1.94 -                        (  RPCFwd send rcv rst p
    1.95 -                         \<or> RPCReject send rcv rst p
    1.96 -                         \<or> RPCFail send rcv rst p
    1.97 -                         \<or> RPCReply send rcv rst p)"
    1.98 +(* temporal *)
    1.99  
   1.100 -  RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
   1.101 -                           Init RPCInit rcv rst p
   1.102 -                         \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
   1.103 -                         \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
   1.104 +definition RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
   1.105 +  where "RPCIPSpec send rcv rst p == TEMP
   1.106 +     Init RPCInit rcv rst p
   1.107 +   \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
   1.108 +   \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
   1.109  
   1.110 -  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
   1.111 +definition RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
   1.112 +  where "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
   1.113  
   1.114  
   1.115  lemmas RPC_action_defs =