75 & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p) |
72 & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p) |
76 & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)" |
73 & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)" |
77 |
74 |
78 RPCISpec_def: "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)" |
75 RPCISpec_def: "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)" |
79 |
76 |
80 ML {* use_legacy_bindings (the_context ()) *} |
77 |
|
78 lemmas RPC_action_defs = |
|
79 RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def |
|
80 |
|
81 lemmas RPC_temp_defs = RPCIPSpec_def RPCISpec_def |
|
82 |
|
83 |
|
84 (* The RPC component engages in an action for process p only if there is an outstanding, |
|
85 unanswered call for that process. |
|
86 *) |
|
87 |
|
88 lemma RPCidle: "|- ~$(Calling send p) --> ~RPCNext send rcv rst p" |
|
89 by (auto simp: Return_def RPC_action_defs) |
|
90 |
|
91 lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p" |
|
92 by (auto simp: RPC_action_defs) |
|
93 |
|
94 (* RPC failure actions are visible. *) |
|
95 lemma RPCFail_vis: "|- RPCFail send rcv rst p --> |
|
96 <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)" |
|
97 by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def) |
|
98 |
|
99 lemma RPCFail_Next_enabled: "|- Enabled (RPCFail send rcv rst p) --> |
|
100 Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))" |
|
101 by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use]) |
|
102 |
|
103 (* Enabledness of some actions *) |
|
104 lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> |
|
105 |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)" |
|
106 by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFail_def", |
|
107 thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI] |
|
108 [thm "base_enabled", thm "Pair_inject"] 1 *}) |
|
109 |
|
110 lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> |
|
111 |- ~Calling rcv p & Calling send p & rst!p = #rpcB |
|
112 --> Enabled (RPCReply send rcv rst p)" |
|
113 by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCReply_def", |
|
114 thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI] |
|
115 [thm "base_enabled", thm "Pair_inject"] 1 *}) |
81 |
116 |
82 end |
117 end |