|
1 (* |
|
2 File: RPC.ML |
|
3 Author: Stephan Merz |
|
4 Copyright: 1997 University of Munich |
|
5 |
|
6 RPC-Memory example: RPC specification (ML file) |
|
7 *) |
|
8 |
|
9 val RPC_action_defs = |
|
10 [RPCInit_def RS inteq_reflection] |
|
11 @ [RPCFwd_def, RPCReject_def, RPCFail_def, RPCReply_def, RPCNext_def]; |
|
12 |
|
13 val RPC_temp_defs = [RPCIPSpec_def, RPCISpec_def]; |
|
14 |
|
15 (* The RPC component engages in an action for process p only if there is an outstanding, |
|
16 unanswered call for that process. |
|
17 *) |
|
18 |
|
19 qed_goal "RPCidle" RPC.thy |
|
20 ".~ $(Calling send p) .-> .~ RPCNext send rcv rst p" |
|
21 (fn _ => [ auto_tac (action_css addsimps2 (Return_def::RPC_action_defs)) ]); |
|
22 |
|
23 qed_goal "RPCbusy" RPC.thy |
|
24 "$(Calling rcv p) .& ($(rst@p) .= #rpcB) .-> .~ RPCNext send rcv rst p" |
|
25 (fn _ => [ auto_tac (action_css addsimps2 (RP_simps @ RPC_action_defs)) ]); |
|
26 |
|
27 (* unlifted versions as introduction rules *) |
|
28 |
|
29 bind_thm("RPCidleI", action_mp RPCidle); |
|
30 bind_thm("RPCbusyI", action_mp RPCbusy); |
|
31 |
|
32 (* RPC failure actions are visible. *) |
|
33 qed_goal "RPCFail_vis" RPC.thy |
|
34 "RPCFail send rcv rst p .-> <RPCNext send rcv rst p>_<rst@p, rtrner send @ p, caller rcv @ p>" |
|
35 (fn _ => [auto_tac (!claset addSEs [Return_changedE], |
|
36 !simpset addsimps [angle_def,RPCNext_def,RPCFail_def]) |
|
37 ]); |
|
38 |
|
39 qed_goal "RPCFail_Next_enabled" RPC.thy |
|
40 "Enabled (RPCFail send rcv rst p) s \ |
|
41 \ ==> Enabled (<RPCNext send rcv rst p>_<rst@p, rtrner send @ p, caller rcv @ p>) s" |
|
42 (fn [prem] => [REPEAT (resolve_tac [prem RS enabled_mono,RPCFail_vis] 1)]); |
|
43 |
|
44 (* Enabledness of some actions *) |
|
45 |
|
46 qed_goal "RPCFail_enabled" RPC.thy |
|
47 "!!p. base_var <rtrner send @ p, caller rcv @ p, rst@p> ==> \ |
|
48 \ .~ $(Calling rcv p) .& $(Calling send p) .-> $(Enabled (RPCFail send rcv rst p))" |
|
49 (fn _ => [action_simp_tac (!simpset addsimps [RPCFail_def,Return_def,caller_def,rtrner_def]) |
|
50 [] [base_enabled,Pair_inject] 1 |
|
51 ]); |
|
52 |
|
53 qed_goal "RPCReply_enabled" RPC.thy |
|
54 "!!p. base_var <rtrner send @ p, caller rcv @ p, rst@p> ==> \ |
|
55 \ .~ $(Calling rcv p) .& $(Calling send p) .& $(rst@p) .= #rpcB \ |
|
56 \ .-> $(Enabled (RPCReply send rcv rst p))" |
|
57 (fn _ => [action_simp_tac (!simpset addsimps [RPCReply_def,Return_def,caller_def,rtrner_def]) |
|
58 [] [base_enabled,Pair_inject] 1]); |
|
59 |