14 val mem_css = (claset(), simpset()); |
14 val mem_css = (claset(), simpset()); |
15 |
15 |
16 (* The Clerk engages in an action for process p only if there is an outstanding, |
16 (* The Clerk engages in an action for process p only if there is an outstanding, |
17 unanswered call for that process. |
17 unanswered call for that process. |
18 *) |
18 *) |
|
19 Goal "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p"; |
|
20 by (auto_tac (mem_css addsimps2 (Return_def::MC_action_defs))); |
|
21 qed "MClkidle"; |
19 |
22 |
20 qed_goal "MClkidle" MemClerk.thy |
23 Goal "|- $Calling rcv p --> ~MClkNext send rcv cst p"; |
21 "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p" |
24 by (auto_tac (mem_css addsimps2 (Call_def::MC_action_defs))); |
22 (fn _ => [ auto_tac (mem_css addsimps2 (Return_def::MC_action_defs)) ]); |
25 qed "MClkbusy"; |
23 |
|
24 qed_goal "MClkbusy" MemClerk.thy |
|
25 "|- $Calling rcv p --> ~MClkNext send rcv cst p" |
|
26 (fn _ => [ auto_tac (mem_css addsimps2 (MC_action_defs @ [Call_def])) ]); |
|
27 |
26 |
28 (* Enabledness of actions *) |
27 (* Enabledness of actions *) |
29 |
28 |
30 qed_goal "MClkFwd_enabled" MemClerk.thy |
29 Goal "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \ |
31 "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \ |
30 \ |- Calling send p & ~Calling rcv p & cst!p = #clkA \ |
32 \ |- Calling send p & ~Calling rcv p & cst!p = #clkA \ |
31 \ --> Enabled (MClkFwd send rcv cst p)"; |
33 \ --> Enabled (MClkFwd send rcv cst p)" |
32 by (action_simp_tac (simpset() addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def]) |
34 (fn _ => [action_simp_tac (simpset() addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def]) |
33 [exI] [base_enabled,Pair_inject] 1); |
35 [exI] [base_enabled,Pair_inject] 1]); |
34 qed "MClkFwd_enabled"; |
36 |
35 |
37 qed_goal "MClkFwd_ch_enabled" MemClerk.thy |
36 Goal "|- Enabled (MClkFwd send rcv cst p) --> \ |
38 "|- Enabled (MClkFwd send rcv cst p) --> \ |
37 \ Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"; |
39 \ Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
38 by (auto_tac (mem_css addSEs2 [enabled_mono] addsimps2 [angle_def,MClkFwd_def])); |
40 (fn _ => [auto_tac (mem_css addSEs2 [enabled_mono] |
39 qed "MClkFwd_ch_enabled"; |
41 addsimps2 [angle_def,MClkFwd_def]) |
|
42 ]); |
|
43 |
40 |
44 qed_goal "MClkReply_change" MemClerk.thy |
41 Goal "|- MClkReply send rcv cst p --> \ |
45 "|- MClkReply send rcv cst p --> <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)" |
42 \ <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"; |
46 (fn _ => [auto_tac (mem_css addsimps2 [angle_def,MClkReply_def] |
43 by (auto_tac (mem_css addsimps2 [angle_def,MClkReply_def] |
47 addEs2 [Return_changed]) |
44 addEs2 [Return_changed])); |
48 ]); |
45 qed "MClkReply_change"; |
49 |
46 |
50 qed_goal "MClkReply_enabled" MemClerk.thy |
47 Goal "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \ |
51 "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \ |
48 \ |- Calling send p & ~Calling rcv p & cst!p = #clkB \ |
52 \ |- Calling send p & ~Calling rcv p & cst!p = #clkB \ |
49 \ --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"; |
53 \ --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
50 by (action_simp_tac (simpset()) [MClkReply_change RSN (2,enabled_mono)] [] 1); |
54 (fn _ => [action_simp_tac (simpset()) [MClkReply_change RSN (2,enabled_mono)] [] 1, |
51 by (action_simp_tac (simpset() addsimps [MClkReply_def,Return_def,caller_def,rtrner_def]) |
55 action_simp_tac (simpset() addsimps [MClkReply_def,Return_def,caller_def,rtrner_def]) |
52 [exI] [base_enabled,Pair_inject] 1); |
56 [exI] [base_enabled,Pair_inject] 1 |
53 qed "MClkReply_enabled"; |
57 ]); |
|
58 |
54 |
59 qed_goal "MClkReplyNotRetry" MemClerk.thy |
55 Goal "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"; |
60 "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p" |
56 by (auto_tac (mem_css addsimps2 [MClkReply_def,MClkRetry_def])); |
61 (fn _ => [ auto_tac (mem_css addsimps2 [MClkReply_def,MClkRetry_def]) ]); |
57 qed "MClkReplyNotRetry"; |
62 |
|