author | nipkow |
Mon, 06 Aug 2001 13:43:24 +0200 | |
changeset 11464 | ddea204de5bc |
parent 9517 | f58863b1406a |
child 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: MemClerk.ML |
|
3 |
Author: Stephan Merz |
|
4 |
Copyright: 1997 University of Munich |
|
5 |
||
6255 | 6 |
RPC-Memory example: Memory clerk specification (theorems and proofs) |
3807 | 7 |
*) |
8 |
||
9 |
val MC_action_defs = |
|
6255 | 10 |
[MClkInit_def, MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def]; |
3807 | 11 |
|
12 |
val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def]; |
|
13 |
||
6255 | 14 |
val mem_css = (claset(), simpset()); |
15 |
||
3807 | 16 |
(* The Clerk engages in an action for process p only if there is an outstanding, |
17 |
unanswered call for that process. |
|
18 |
*) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
19 |
Goal "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
20 |
by (auto_tac (mem_css addsimps2 (Return_def::MC_action_defs))); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
21 |
qed "MClkidle"; |
3807 | 22 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
23 |
Goal "|- $Calling rcv p --> ~MClkNext send rcv cst p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
24 |
by (auto_tac (mem_css addsimps2 (Call_def::MC_action_defs))); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
25 |
qed "MClkbusy"; |
3807 | 26 |
|
27 |
(* Enabledness of actions *) |
|
28 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
29 |
Goal "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
30 |
\ |- Calling send p & ~Calling rcv p & cst!p = #clkA \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
31 |
\ --> Enabled (MClkFwd send rcv cst p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
32 |
by (action_simp_tac (simpset() addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
33 |
[exI] [base_enabled,Pair_inject] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
34 |
qed "MClkFwd_enabled"; |
3807 | 35 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
36 |
Goal "|- Enabled (MClkFwd send rcv cst p) --> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
37 |
\ Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
38 |
by (auto_tac (mem_css addSEs2 [enabled_mono] addsimps2 [angle_def,MClkFwd_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
39 |
qed "MClkFwd_ch_enabled"; |
3807 | 40 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
41 |
Goal "|- MClkReply send rcv cst p --> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
42 |
\ <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
43 |
by (auto_tac (mem_css addsimps2 [angle_def,MClkReply_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
44 |
addEs2 [Return_changed])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
45 |
qed "MClkReply_change"; |
3807 | 46 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
47 |
Goal "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
48 |
\ |- Calling send p & ~Calling rcv p & cst!p = #clkB \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
49 |
\ --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
50 |
by (action_simp_tac (simpset()) [MClkReply_change RSN (2,enabled_mono)] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
51 |
by (action_simp_tac (simpset() addsimps [MClkReply_def,Return_def,caller_def,rtrner_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
52 |
[exI] [base_enabled,Pair_inject] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
53 |
qed "MClkReply_enabled"; |
3807 | 54 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
55 |
Goal "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
56 |
by (auto_tac (mem_css addsimps2 [MClkReply_def,MClkRetry_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
57 |
qed "MClkReplyNotRetry"; |