author | wenzelm |
Thu, 03 Aug 2000 19:29:03 +0200 | |
changeset 9517 | f58863b1406a |
parent 7570 | a9391550eea1 |
child 10231 | 178a272bceeb |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: MemoryImplementation.ML |
|
3 |
Author: Stephan Merz |
|
4 |
Copyright: 1997 University of Munich |
|
5 |
||
6 |
RPC-Memory example: Memory implementation (ML file) |
|
7 |
||
8 |
The main theorem is theorem "Implementation" at the end of this file, |
|
9 |
which shows that the composition of a reliable memory, an RPC component, and |
|
10 |
a memory clerk implements an unreliable memory. The files "MIsafe.ML" and |
|
11 |
"MIlive.ML" contain lower-level lemmas for the safety and liveness parts. |
|
12 |
||
13 |
Steps are (roughly) numbered as in the hand proof. |
|
14 |
*) |
|
15 |
||
6255 | 16 |
(* --------------------------- automatic prover --------------------------- *) |
3807 | 17 |
|
6919 | 18 |
Delcongs [if_weak_cong]; |
19 |
||
6255 | 20 |
val MI_css = (claset(), simpset()); |
3807 | 21 |
|
22 |
(* A more aggressive variant that tries to solve subgoals by assumption |
|
23 |
or contradiction during the simplification. |
|
24 |
THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!! |
|
6255 | 25 |
(but it can be a lot faster than MI_css) |
3807 | 26 |
*) |
27 |
val MI_fast_css = |
|
28 |
let |
|
29 |
val (cs,ss) = MI_css |
|
30 |
in |
|
7570 | 31 |
(cs addSEs [squareE], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE)))) |
3807 | 32 |
end; |
33 |
||
6255 | 34 |
val temp_elim = make_elim o temp_use; |
3807 | 35 |
|
36 |
(****************************** The history variable ******************************) |
|
37 |
section "History variable"; |
|
38 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
39 |
Goal "|- Init(ALL p. ImpInit p) & [](ALL p. ImpNext p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
40 |
\ --> (EEX rmhist. Init(ALL p. HInit rmhist p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
41 |
\ & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
42 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
43 |
by (rtac historyI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
44 |
by (TRYALL atac); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
45 |
by (rtac MI_base 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
46 |
by (action_simp_tac (simpset() addsimps [HInit_def]) [] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
47 |
by (etac fun_cong 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
48 |
by (action_simp_tac (simpset() addsimps [HNext_def]) [busy_squareI] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
49 |
by (etac fun_cong 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
50 |
qed "HistoryLemma"; |
3807 | 51 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
52 |
Goal "|- Implementation --> (EEX rmhist. Hist rmhist)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
53 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
54 |
by (rtac ((temp_use HistoryLemma) RS eex_mono) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
55 |
by (force_tac (MI_css |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
56 |
addsimps2 [Hist_def,HistP_def,Init_def,all_box,split_box_conj]) 3); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
57 |
by (auto_tac (MI_css |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
58 |
addsimps2 [Implementation_def,MClkISpec_def,RPCISpec_def,IRSpec_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
59 |
MClkIPSpec_def,RPCIPSpec_def,RPSpec_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
60 |
ImpInit_def,Init_def,ImpNext_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
61 |
c_def,r_def,m_def,all_box,split_box_conj])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
62 |
qed "History"; |
3807 | 63 |
|
64 |
(******************************** The safety part *********************************) |
|
65 |
||
66 |
section "The safety part"; |
|
67 |
||
68 |
(* ------------------------- Include lower-level lemmas ------------------------- *) |
|
69 |
use "MIsafe.ML"; |
|
70 |
||
71 |
section "Correctness of predicate-action diagram"; |
|
72 |
||
6255 | 73 |
|
3807 | 74 |
(* ========== Step 1.1 ================================================= *) |
75 |
(* The implementation's initial condition implies the state predicate S1 *) |
|
76 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
77 |
Goal "|- ImpInit p & HInit rmhist p --> S1 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
78 |
by (auto_tac (MI_fast_css |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
79 |
addsimps2 [MVNROKBA_def,MClkInit_def,RPCInit_def,PInit_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
80 |
HInit_def,ImpInit_def,S_def,S1_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
81 |
qed "Step1_1"; |
3807 | 82 |
|
83 |
(* ========== Step 1.2 ================================================== *) |
|
84 |
(* Figure 16 is a predicate-action diagram for the implementation. *) |
|
85 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
86 |
Goal "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
87 |
\ & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
88 |
\ --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
89 |
by (action_simp_tac (simpset() addsimps [ImpNext_def]) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
90 |
(map temp_elim [S1ClerkUnch,S1RPCUnch,S1MemUnch,S1Hist]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
91 |
by (auto_tac (MI_fast_css addSIs2 [S1Env])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
92 |
qed "Step1_2_1"; |
3807 | 93 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
94 |
Goal "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
95 |
\ & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
96 |
\ --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
97 |
\ & unchanged (e p, r p, m p, rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
98 |
by (action_simp_tac (simpset() addsimps [ImpNext_def]) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
99 |
(map temp_elim [S2EnvUnch,S2RPCUnch,S2MemUnch,S2Hist]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
100 |
by (auto_tac (MI_fast_css addSIs2 [S2Clerk,S2Forward])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
101 |
qed "Step1_2_2"; |
3807 | 102 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
103 |
Goal "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
104 |
\ & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
105 |
\ --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
106 |
\ | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
107 |
by (action_simp_tac (simpset() addsimps [ImpNext_def]) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
108 |
(map temp_elim [S3EnvUnch,S3ClerkUnch,S3MemUnch]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
109 |
by (action_simp_tac (simpset()) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
110 |
(squareE::map temp_elim [S3RPC,S3Forward,S3Fail]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
111 |
by (auto_tac (MI_css addDs2 [S3Hist])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
112 |
qed "Step1_2_3"; |
3807 | 113 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
114 |
Goal "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p \ |
6255 | 115 |
\ & ~unchanged (e p, c p, r p, m p, rmhist!p) \ |
116 |
\ & $S4 rmhist p & (!l. $(MemInv mm l)) \ |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
117 |
\ --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
118 |
\ | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
119 |
\ | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
120 |
by (action_simp_tac (simpset() addsimps [ImpNext_def]) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
121 |
(map temp_elim [S4EnvUnch,S4ClerkUnch,S4RPCUnch]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
122 |
by (action_simp_tac (simpset() addsimps [RNext_def]) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
123 |
(squareE::map temp_elim [S4Read,S4Write,S4Return]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
124 |
by (auto_tac (MI_css addDs2 [S4Hist])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
125 |
qed "Step1_2_4"; |
3807 | 126 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
127 |
Goal "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p \ |
6255 | 128 |
\ & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p \ |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
129 |
\ --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
130 |
\ | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
131 |
by (action_simp_tac (simpset() addsimps [ImpNext_def]) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
132 |
(map temp_elim [S5EnvUnch,S5ClerkUnch,S5MemUnch,S5Hist]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
133 |
by (action_simp_tac (simpset()) [] [squareE, temp_elim S5RPC] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
134 |
by (auto_tac (MI_fast_css addSDs2 [S5Reply,S5Fail])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
135 |
qed "Step1_2_5"; |
3807 | 136 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
137 |
Goal "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p \ |
6255 | 138 |
\ & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p \ |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
139 |
\ --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
140 |
\ | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
141 |
by (action_simp_tac (simpset() addsimps [ImpNext_def]) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
142 |
(map temp_elim [S6EnvUnch,S6RPCUnch,S6MemUnch]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
143 |
by (action_simp_tac (simpset()) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
144 |
(squareE::map temp_elim [S6Clerk,S6Retry,S6Reply]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
145 |
by (auto_tac (MI_css addDs2 [S6Hist])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
146 |
qed "Step1_2_6"; |
3807 | 147 |
|
148 |
(* -------------------------------------------------------------------------- |
|
149 |
Step 1.3: S1 implies the barred initial condition. |
|
150 |
*) |
|
151 |
||
152 |
section "Initialization (Step 1.3)"; |
|
153 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
154 |
Goal "|- S1 rmhist p --> PInit (resbar rmhist) p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
155 |
by (action_simp_tac (simpset() addsimps [resbar_def,PInit_def,S_def,S1_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
156 |
[] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
157 |
qed "Step1_3"; |
3807 | 158 |
|
159 |
(* ---------------------------------------------------------------------- |
|
160 |
Step 1.4: Implementation's next-state relation simulates specification's |
|
161 |
next-state relation (with appropriate substitutions) |
|
162 |
*) |
|
163 |
||
164 |
section "Step simulation (Step 1.4)"; |
|
165 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
166 |
Goal "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
167 |
\ --> unchanged (rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
168 |
by (auto_tac (MI_fast_css addsimps2 [c_def,r_def,m_def,resbar_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
169 |
qed "Step1_4_1"; |
3807 | 170 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
171 |
Goal "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$ \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
172 |
\ & unchanged (e p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
173 |
\ --> unchanged (rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
174 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
175 |
(simpset() addsimps [MClkFwd_def, e_def, r_def, m_def, resbar_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
176 |
S_def, S2_def, S3_def]) [] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
177 |
qed "Step1_4_2"; |
3807 | 178 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
179 |
Goal "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$ \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
180 |
\ & unchanged (e p, c p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
181 |
\ --> unchanged (rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
182 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
183 |
by (REPEAT (dresolve_tac (map temp_use [S3_excl,S4_excl]) 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
184 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
185 |
(simpset() addsimps [e_def,c_def,m_def,resbar_def,S_def, S3_def]) [] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
186 |
qed "Step1_4_3a"; |
3807 | 187 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
188 |
Goal "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
189 |
\ & unchanged (e p, c p, m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
190 |
\ --> MemFail memCh (resbar rmhist) p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
191 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
192 |
by (dtac (temp_use S6_excl) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
193 |
by (auto_tac (MI_css addsimps2 [RPCFail_def,MemFail_def,e_def,c_def,m_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
194 |
resbar_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
195 |
by (force_tac (MI_css addsimps2 [S3_def,S_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
196 |
by (auto_tac (MI_css addsimps2 [Return_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
197 |
qed "Step1_4_3b"; |
3807 | 198 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
199 |
Goal "|- $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
200 |
\ & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
201 |
\ --> ReadInner memCh mm (resbar rmhist) p l"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
202 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
203 |
by (REPEAT (dtac (temp_use S4_excl) 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
204 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
205 |
(simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,e_def,c_def,m_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
206 |
[] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
207 |
by (auto_tac (MI_css addsimps2 [resbar_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
208 |
by (ALLGOALS (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
209 |
(simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
210 |
S_def,S4_def,RdRequest_def,MemInv_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
211 |
[] [impE,MemValNotAResultE])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
212 |
qed "Step1_4_4a1"; |
3807 | 213 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
214 |
Goal "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$ \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
215 |
\ & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
216 |
\ --> Read memCh mm (resbar rmhist) p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
217 |
by (force_tac (MI_css addsimps2 [Read_def] addSEs2 [Step1_4_4a1]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
218 |
qed "Step1_4_4a"; |
3807 | 219 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
220 |
Goal "|- $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
221 |
\ & unchanged (e p, c p, r p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
222 |
\ --> WriteInner memCh mm (resbar rmhist) p l v"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
223 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
224 |
by (REPEAT (dtac (temp_use S4_excl) 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
225 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
226 |
(simpset() addsimps [WriteInner_def, GoodWrite_def, BadWrite_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
227 |
e_def, c_def, m_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
228 |
[] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
229 |
by (auto_tac (MI_css addsimps2 [resbar_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
230 |
by (ALLGOALS (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
231 |
(simpset() addsimps [RPCRelayArg_def,MClkRelayArg_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
232 |
S_def,S4_def,WrRequest_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
233 |
[] [])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
234 |
qed "Step1_4_4b1"; |
3807 | 235 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
236 |
Goal "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$ \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
237 |
\ & unchanged (e p, c p, r p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
238 |
\ --> Write memCh mm (resbar rmhist) p l"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
239 |
by (force_tac (MI_css addsimps2 [Write_def] addSEs2 [Step1_4_4b1]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
240 |
qed "Step1_4_4b"; |
3807 | 241 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
242 |
Goal "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
243 |
\ & unchanged (e p, c p, r p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
244 |
\ --> unchanged (rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
245 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
246 |
(simpset() addsimps [e_def,c_def,r_def,resbar_def]) [] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
247 |
by (REPEAT (dresolve_tac [temp_use S4_excl, temp_use S5_excl] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
248 |
by (auto_tac (MI_fast_css addsimps2 [MemReturn_def,Return_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
249 |
qed "Step1_4_4c"; |
3807 | 250 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
251 |
Goal "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
252 |
\ & unchanged (e p, c p, m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
253 |
\ --> unchanged (rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
254 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
255 |
by (REPEAT (dresolve_tac [temp_use S5_excl, temp_use S6_excl] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
256 |
by (auto_tac (MI_css addsimps2 [e_def,c_def,m_def, resbar_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
257 |
by (auto_tac (MI_css addsimps2 [RPCReply_def,Return_def,S5_def,S_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
258 |
addSDs2 [MVOKBAnotRF])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
259 |
qed "Step1_4_5a"; |
3807 | 260 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
261 |
Goal "|- RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
262 |
\ & unchanged (e p, c p, m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
263 |
\ --> MemFail memCh (resbar rmhist) p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
264 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
265 |
by (dtac (temp_use S6_excl) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
266 |
by (auto_tac (MI_css addsimps2 [e_def, c_def, m_def, RPCFail_def, Return_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
267 |
MemFail_def, resbar_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
268 |
by (auto_tac (MI_css addsimps2 [S5_def,S_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
269 |
qed "Step1_4_5b"; |
3807 | 270 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
271 |
Goal "|- MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
272 |
\ & unchanged (e p, r p, m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
273 |
\ --> MemReturn memCh (resbar rmhist) p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
274 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
275 |
by (dtac (temp_use S6_excl) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
276 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
277 |
(simpset() addsimps [e_def,r_def,m_def,MClkReply_def,MemReturn_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
278 |
Return_def,resbar_def]) [] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
279 |
by (ALLGOALS Asm_full_simp_tac); (* simplify if-then-else *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
280 |
by (ALLGOALS (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
281 |
(simpset() addsimps [MClkReplyVal_def,S6_def,S_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
282 |
[] [MVOKBARFnotNR])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
283 |
qed "Step1_4_6a"; |
3807 | 284 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
285 |
Goal "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$ \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
286 |
\ & unchanged (e p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
287 |
\ --> MemFail memCh (resbar rmhist) p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
288 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
289 |
by (dtac (temp_use S3_excl) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
290 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
291 |
(simpset() addsimps [e_def, r_def, m_def, MClkRetry_def, MemFail_def, resbar_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
292 |
[] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
293 |
by (auto_tac (MI_css addsimps2 [S6_def,S_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
294 |
qed "Step1_4_6b"; |
3807 | 295 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
296 |
Goal "|- unchanged (e p, c p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
297 |
\ --> unchanged (S rmhist ec cc rc cs rs hs1 hs2 p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
298 |
by (auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,caller_def,rtrner_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
299 |
S_def,Calling_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
300 |
qed "S_lemma"; |
3807 | 301 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
302 |
Goal "|- unchanged (e p, c p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
303 |
\ --> unchanged (rtrner memCh!p, S1 rmhist p, S2 rmhist p, S3 rmhist p, \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
304 |
\ S4 rmhist p, S5 rmhist p, S6 rmhist p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
305 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
306 |
by (rtac conjI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
307 |
by (force_tac (MI_css addsimps2 [c_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
308 |
by (force_tac (MI_css addsimps2 [S1_def,S2_def,S3_def,S4_def,S5_def,S6_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
309 |
addSIs2 [S_lemma]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
310 |
qed "Step1_4_7H"; |
3807 | 311 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
312 |
Goal "|- unchanged (e p, c p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
313 |
\ --> unchanged (rtrner memCh!p, resbar rmhist!p, S1 rmhist p, S2 rmhist p, \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
314 |
\ S3 rmhist p, S4 rmhist p, S5 rmhist p, S6 rmhist p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
315 |
by (rtac actionI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
316 |
by (rewrite_goals_tac action_rews); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
317 |
by (rtac impI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
318 |
by (forward_tac [temp_use Step1_4_7H] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
319 |
by (auto_tac (MI_css addsimps2 [e_def,c_def,r_def,m_def,rtrner_def,resbar_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
320 |
qed "Step1_4_7"; |
3807 | 321 |
|
322 |
(* Frequently needed abbreviation: distinguish between idling and non-idling |
|
323 |
steps of the implementation, and try to solve the idling case by simplification |
|
324 |
*) |
|
325 |
fun split_idle_tac simps i = |
|
6255 | 326 |
EVERY [TRY (rtac actionI i), |
327 |
case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i, |
|
3807 | 328 |
rewrite_goals_tac action_rews, |
6255 | 329 |
forward_tac [temp_use Step1_4_7] i, |
4089 | 330 |
asm_full_simp_tac (simpset() addsimps simps) i |
3807 | 331 |
]; |
332 |
||
333 |
(* ---------------------------------------------------------------------- |
|
334 |
Combine steps 1.2 and 1.4 to prove that the implementation satisfies |
|
335 |
the specification's next-state relation. |
|
336 |
*) |
|
337 |
||
338 |
(* Steps that leave all variables unchanged are safe, so I may assume |
|
339 |
that some variable changes in the proof that a step is safe. *) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
340 |
Goal "|- (~unchanged (e p, c p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
341 |
\ --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
342 |
\ --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
343 |
by (split_idle_tac [square_def] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
344 |
by (Force_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
345 |
qed "unchanged_safe"; |
3807 | 346 |
(* turn into (unsafe, looping!) introduction rule *) |
6255 | 347 |
bind_thm("unchanged_safeI", impI RS (action_use unchanged_safe)); |
3807 | 348 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
349 |
Goal "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
350 |
\ --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
351 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
352 |
by (rtac unchanged_safeI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
353 |
by (rtac idle_squareI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
354 |
by (auto_tac (MI_css addSDs2 [Step1_2_1,Step1_4_1])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
355 |
qed "S1safe"; |
3807 | 356 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
357 |
Goal "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
358 |
\ --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
359 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
360 |
by (rtac unchanged_safeI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
361 |
by (rtac idle_squareI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
362 |
by (auto_tac (MI_css addSDs2 [Step1_2_2,Step1_4_2])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
363 |
qed "S2safe"; |
3807 | 364 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
365 |
Goal "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
366 |
\ --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
367 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
368 |
by (rtac unchanged_safeI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
369 |
by (auto_tac (MI_css addSDs2 [Step1_2_3])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
370 |
by (auto_tac (MI_css addsimps2 [square_def,UNext_def] addSDs2 [Step1_4_3a,Step1_4_3b])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
371 |
qed "S3safe"; |
3807 | 372 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
373 |
Goal "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
374 |
\ & (!l. $(MemInv mm l)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
375 |
\ --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
376 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
377 |
by (rtac unchanged_safeI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
378 |
by (auto_tac (MI_css addSDs2 [Step1_2_4])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
379 |
by (auto_tac (MI_css addsimps2 [square_def,UNext_def,RNext_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
380 |
addSDs2 [Step1_4_4a,Step1_4_4b,Step1_4_4c])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
381 |
qed "S4safe"; |
3807 | 382 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
383 |
Goal "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
384 |
\ --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
385 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
386 |
by (rtac unchanged_safeI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
387 |
by (auto_tac (MI_css addSDs2 [Step1_2_5])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
388 |
by (auto_tac (MI_css addsimps2 [square_def,UNext_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
389 |
addSDs2 [Step1_4_5a,Step1_4_5b])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
390 |
qed "S5safe"; |
3807 | 391 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
392 |
Goal "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
393 |
\ --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
394 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
395 |
by (rtac unchanged_safeI 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
396 |
by (auto_tac (MI_css addSDs2 [Step1_2_6])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
397 |
by (auto_tac (MI_css addsimps2 [square_def,UNext_def,RNext_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
398 |
addSDs2 [Step1_4_6a,Step1_4_6b])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
399 |
qed "S6safe"; |
3807 | 400 |
|
401 |
(* ---------------------------------------------------------------------- |
|
402 |
Step 1.5: Temporal refinement proof, based on previous steps. |
|
403 |
*) |
|
404 |
||
405 |
section "The liveness part"; |
|
406 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
407 |
(* Liveness assertions for the different implementation states, based on the |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
408 |
fairness conditions. Prove subgoals of WF1 / SF1 rules as separate lemmas |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
409 |
for readability. Reuse action proofs from safety part. |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
410 |
*) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
411 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
412 |
(* ------------------------------ State S1 ------------------------------ *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
413 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
414 |
Goal "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
415 |
\ --> (S1 rmhist p)$ | (S2 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
416 |
by (split_idle_tac [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
417 |
by (auto_tac (MI_css addSDs2 [Step1_2_1])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
418 |
qed "S1_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
419 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
420 |
(* Show that the implementation can satisfy the high-level fairness requirements |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
421 |
by entering the state S1 infinitely often. |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
422 |
*) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
423 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
424 |
Goal "|- S1 rmhist p --> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
425 |
\ ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
426 |
by (action_simp_tac (simpset() addsimps [angle_def,S_def,S1_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
427 |
[notI] [enabledE,temp_elim Memoryidle] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
428 |
by (Force_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
429 |
qed "S1_RNextdisabled"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
430 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
431 |
Goal "|- S1 rmhist p --> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
432 |
\ ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
433 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
434 |
(simpset() addsimps [angle_def,MemReturn_def,Return_def,S_def,S1_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
435 |
[notI] [enabledE] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
436 |
qed "S1_Returndisabled"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
437 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
438 |
Goal "|- []<>S1 rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
439 |
\ --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
440 |
by (auto_tac (MI_css addsimps2 [WF_alt] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
441 |
addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
442 |
qed "RNext_fair"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
443 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
444 |
Goal "|- []<>S1 rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
445 |
\ --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
446 |
by (auto_tac (MI_css addsimps2 [WF_alt] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
447 |
addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
448 |
qed "Return_fair"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
449 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
450 |
(* ------------------------------ State S2 ------------------------------ *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
451 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
452 |
Goal "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
453 |
\ --> (S2 rmhist p)$ | (S3 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
454 |
by (split_idle_tac [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
455 |
by (auto_tac (MI_css addSDs2 [Step1_2_2])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
456 |
qed "S2_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
457 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
458 |
Goal "|- ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
459 |
\ & <MClkFwd memCh crCh cst p>_(c p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
460 |
\ --> (S3 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
461 |
by (auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_2])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
462 |
qed "S2MClkFwd_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
463 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
464 |
Goal "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
465 |
\ --> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
466 |
by (auto_tac (MI_css addsimps2 [c_def] addSIs2 [MClkFwd_ch_enabled,MClkFwd_enabled])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
467 |
by (cut_facts_tac [MI_base] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
468 |
by (blast_tac (claset() addDs [base_pair]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
469 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S2_def]))); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
470 |
qed "S2MClkFwd_enabled"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
471 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
472 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
473 |
\ & WF(MClkFwd memCh crCh cst p)_(c p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
474 |
\ --> (S2 rmhist p ~> S3 rmhist p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
475 |
by (REPEAT (resolve_tac [WF1,S2_successors, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
476 |
S2MClkFwd_successors,S2MClkFwd_enabled] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
477 |
qed "S2_live"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
478 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
479 |
(* ------------------------------ State S3 ------------------------------ *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
480 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
481 |
Goal "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
482 |
\ --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
483 |
by (split_idle_tac [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
484 |
by (auto_tac (MI_css addSDs2 [Step1_2_3])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
485 |
qed "S3_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
486 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
487 |
Goal "|- ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
488 |
\ & <RPCNext crCh rmCh rst p>_(r p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
489 |
\ --> (S4 rmhist p | S6 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
490 |
by (auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_3])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
491 |
qed "S3RPC_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
492 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
493 |
Goal "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
494 |
\ --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
495 |
by (auto_tac (MI_css addsimps2 [r_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
496 |
addSIs2 [RPCFail_Next_enabled,RPCFail_enabled])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
497 |
by (cut_facts_tac [MI_base] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
498 |
by (blast_tac (claset() addDs [base_pair]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
499 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S3_def]))); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
500 |
qed "S3RPC_enabled"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
501 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
502 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
503 |
\ & WF(RPCNext crCh rmCh rst p)_(r p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
504 |
\ --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
505 |
by (REPEAT (resolve_tac [WF1,S3_successors,S3RPC_successors,S3RPC_enabled] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
506 |
qed "S3_live"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
507 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
508 |
(* ------------- State S4 -------------------------------------------------- *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
509 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
510 |
Goal"|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
511 |
\ & (ALL l. $MemInv mm l) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
512 |
\ --> (S4 rmhist p)$ | (S5 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
513 |
by (split_idle_tac [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
514 |
by (auto_tac (MI_css addSDs2 [Step1_2_4])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
515 |
qed "S4_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
516 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
517 |
(* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
518 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
519 |
Goal "|- $(S4 rmhist p & ires!p = #NotAResult) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
520 |
\ & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
521 |
\ --> (S4 rmhist p & ires!p = #NotAResult)$ \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
522 |
\ | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
523 |
by (split_idle_tac [m_def] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
524 |
by (auto_tac (MI_css addSDs2 [Step1_2_4])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
525 |
qed "S4a_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
526 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
527 |
Goal "|- ($(S4 rmhist p & ires!p = #NotAResult) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
528 |
\ & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l))\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
529 |
\ & <RNext rmCh mm ires p>_(m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
530 |
\ --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
531 |
by (auto_tac (MI_css addsimps2 [angle_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
532 |
addSDs2 [Step1_2_4, ReadResult, WriteResult])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
533 |
qed "S4aRNext_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
534 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
535 |
Goal "|- $(S4 rmhist p & ires!p = #NotAResult) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
536 |
\ & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
537 |
\ --> $Enabled (<RNext rmCh mm ires p>_(m p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
538 |
by (auto_tac (MI_css addsimps2 [m_def] addSIs2 [RNext_enabled])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
539 |
by (cut_facts_tac [MI_base] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
540 |
by (blast_tac (claset() addDs [base_pair]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
541 |
by (asm_full_simp_tac (simpset() addsimps [S_def,S4_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
542 |
qed "S4aRNext_enabled"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
543 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
544 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
545 |
\ & (ALL l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
546 |
\ --> (S4 rmhist p & ires!p = #NotAResult \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
547 |
\ ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
548 |
by (REPEAT (resolve_tac [WF1, S4a_successors, S4aRNext_successors, S4aRNext_enabled] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
549 |
qed "S4a_live"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
550 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
551 |
(* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
552 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
553 |
Goal "|- $(S4 rmhist p & ires!p ~= #NotAResult) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
554 |
\ & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
555 |
\ --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
556 |
by (split_idle_tac [m_def] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
557 |
by (auto_tac (MI_css addSDs2 [WriteResult,Step1_2_4,ReadResult])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
558 |
qed "S4b_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
559 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
560 |
Goal "|- ($(S4 rmhist p & ires!p ~= #NotAResult) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
561 |
\ & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
562 |
\ & (ALL l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
563 |
\ --> (S5 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
564 |
by (force_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_4] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
565 |
addDs2 [ReturnNotReadWrite]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
566 |
qed "S4bReturn_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
567 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
568 |
Goal "|- $(S4 rmhist p & ires!p ~= #NotAResult) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
569 |
\ & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
570 |
\ & (ALL l. $MemInv mm l) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
571 |
\ --> $Enabled (<MemReturn rmCh ires p>_(m p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
572 |
by (auto_tac (MI_css addsimps2 [m_def] addSIs2 [MemReturn_enabled])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
573 |
by (cut_facts_tac [MI_base] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
574 |
by (blast_tac (claset() addDs [base_pair]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
575 |
by (asm_full_simp_tac (simpset() addsimps [S_def,S4_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
576 |
qed "S4bReturn_enabled"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
577 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
578 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
579 |
\ & WF(MemReturn rmCh ires p)_(m p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
580 |
\ --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
581 |
by (REPEAT (resolve_tac [WF1, S4b_successors,S4bReturn_successors, S4bReturn_enabled] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
582 |
qed "S4b_live"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
583 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
584 |
(* ------------------------------ State S5 ------------------------------ *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
585 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
586 |
Goal "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
587 |
\ --> (S5 rmhist p)$ | (S6 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
588 |
by (split_idle_tac [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
589 |
by (auto_tac (MI_css addSDs2 [Step1_2_5])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
590 |
qed "S5_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
591 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
592 |
Goal "|- ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
593 |
\ & <RPCNext crCh rmCh rst p>_(r p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
594 |
\ --> (S6 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
595 |
by (auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_5])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
596 |
qed "S5RPC_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
597 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
598 |
Goal "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
599 |
\ --> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
600 |
by (auto_tac (MI_css addsimps2 [r_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
601 |
addSIs2 [RPCFail_Next_enabled, RPCFail_enabled])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
602 |
by (cut_facts_tac [MI_base] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
603 |
by (blast_tac (claset() addDs [base_pair]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
604 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [S_def,S5_def]))); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
605 |
qed "S5RPC_enabled"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
606 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
607 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
608 |
\ & WF(RPCNext crCh rmCh rst p)_(r p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
609 |
\ --> (S5 rmhist p ~> S6 rmhist p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
610 |
by (REPEAT (resolve_tac [WF1,S5_successors,S5RPC_successors,S5RPC_enabled] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
611 |
qed "S5_live"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
612 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
613 |
(* ------------------------------ State S6 ------------------------------ *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
614 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
615 |
Goal "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
616 |
\ --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
617 |
by (split_idle_tac [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
618 |
by (auto_tac (MI_css addSDs2 [Step1_2_6])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
619 |
qed "S6_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
620 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
621 |
Goal "|- ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
622 |
\ & <MClkReply memCh crCh cst p>_(c p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
623 |
\ --> (S1 rmhist p)$"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
624 |
by (auto_tac (MI_css addsimps2 [angle_def] addSDs2 [Step1_2_6, MClkReplyNotRetry])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
625 |
qed "S6MClkReply_successors"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
626 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
627 |
Goal "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
628 |
by (action_simp_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
629 |
(simpset() addsimps [angle_def,MClkReply_def,Return_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
630 |
ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
631 |
[] [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
632 |
qed "MClkReplyS6"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
633 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
634 |
Goal "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
635 |
by (auto_tac (MI_css addsimps2 [c_def] addSIs2 [MClkReply_enabled])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
636 |
by (cut_facts_tac [MI_base] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
637 |
by (blast_tac (claset() addDs [base_pair]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
638 |
by (ALLGOALS (action_simp_tac (simpset() addsimps [S_def,S6_def]) [] [])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
639 |
qed "S6MClkReply_enabled"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
640 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
641 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
642 |
\ & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
643 |
\ --> []<>(S1 rmhist p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
644 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
645 |
by (subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
646 |
by (etac InfiniteEnsures 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
647 |
by (atac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
648 |
by (action_simp_tac (simpset()) [] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
649 |
(map temp_elim [MClkReplyS6,S6MClkReply_successors]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
650 |
by (auto_tac (MI_css addsimps2 [SF_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
651 |
by (etac swap 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
652 |
by (auto_tac (MI_css addSIs2 [S6MClkReply_enabled] addSEs2 [STL4E, DmdImplE])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
653 |
qed "S6_live"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
654 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
655 |
(* --------------- aggregate leadsto properties----------------------------- *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
656 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
657 |
Goal "sigma |= S5 rmhist p ~> S6 rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
658 |
\ ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
659 |
by (auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro, LatticeReflexivity])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
660 |
qed "S5S6LeadstoS6"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
661 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
662 |
Goal "[| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
663 |
\ sigma |= S5 rmhist p ~> S6 rmhist p |] \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
664 |
\ ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
665 |
\ ~> S6 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
666 |
by (auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,S5S6LeadstoS6] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
667 |
addIs2 [LatticeTransitivity])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
668 |
qed "S4bS5S6LeadstoS6"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
669 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
670 |
Goal "[| sigma |= S4 rmhist p & ires!p = #NotAResult \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
671 |
\ ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
672 |
\ sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
673 |
\ sigma |= S5 rmhist p ~> S6 rmhist p |] \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
674 |
\ ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
675 |
by (subgoal_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
676 |
"sigma |= (S4 rmhist p & ires!p = #NotAResult)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
677 |
\ | (S4 rmhist p & ires!p ~= #NotAResult)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
678 |
\ | S5 rmhist p | S6 rmhist p ~> S6 rmhist p" 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
679 |
by (eres_inst_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
680 |
[("G", "PRED ((S4 rmhist p & ires!p = #NotAResult)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
681 |
\ | (S4 rmhist p & ires!p ~= #NotAResult)\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
682 |
\ | S5 rmhist p | S6 rmhist p)")] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
683 |
(temp_use LatticeTransitivity) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
684 |
by (force_tac (MI_css addsimps2 Init_defs addSIs2 [ImplLeadsto_gen, necT]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
685 |
by (rtac (temp_use LatticeDisjunctionIntro) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
686 |
by (etac (temp_use LatticeTransitivity) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
687 |
by (etac (temp_use LatticeTriangle2) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
688 |
by (atac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
689 |
by (auto_tac (MI_css addSIs2 [S4bS5S6LeadstoS6])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
690 |
qed "S4S5S6LeadstoS6"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
691 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
692 |
Goal "[| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
693 |
\ sigma |= S4 rmhist p & ires!p = #NotAResult \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
694 |
\ ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
695 |
\ sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
696 |
\ sigma |= S5 rmhist p ~> S6 rmhist p |] \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
697 |
\ ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
698 |
by (rtac (temp_use LatticeDisjunctionIntro) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
699 |
by (etac (temp_use LatticeTriangle2) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
700 |
by (rtac (S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
701 |
by (auto_tac (MI_css addSIs2 [S4S5S6LeadstoS6,necT] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
702 |
addIs2 [ImplLeadsto_gen] addsimps2 Init_defs)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
703 |
qed "S3S4S5S6LeadstoS6"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
704 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
705 |
Goal "[| sigma |= S2 rmhist p ~> S3 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
706 |
\ sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
707 |
\ sigma |= S4 rmhist p & ires!p = #NotAResult \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
708 |
\ ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
709 |
\ sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
710 |
\ sigma |= S5 rmhist p ~> S6 rmhist p |] \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
711 |
\ ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
712 |
\ ~> S6 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
713 |
by (rtac (temp_use LatticeDisjunctionIntro) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
714 |
by (rtac (temp_use LatticeTransitivity) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
715 |
by (atac 2); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
716 |
by (rtac (S3S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
717 |
by (auto_tac (MI_css addSIs2 [S3S4S5S6LeadstoS6,necT] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
718 |
addIs2 [ImplLeadsto_gen] addsimps2 Init_defs)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
719 |
qed "S2S3S4S5S6LeadstoS6"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
720 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
721 |
Goal "[| sigma |= []ImpInv rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
722 |
\ sigma |= S2 rmhist p ~> S3 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
723 |
\ sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
724 |
\ sigma |= S4 rmhist p & ires!p = #NotAResult \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
725 |
\ ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
726 |
\ sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
727 |
\ sigma |= S5 rmhist p ~> S6 rmhist p |] \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
728 |
\ ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
729 |
by (rtac (S2S3S4S5S6LeadstoS6 RS (temp_use LatticeTransitivity)) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
730 |
by (TRYALL atac); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
731 |
by (etac (temp_use INV_leadsto) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
732 |
by (rtac (temp_use ImplLeadsto_gen) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
733 |
by (rtac (temp_use necT) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
734 |
by (auto_tac (MI_css addsimps2 ImpInv_def::Init_defs addSIs2 [necT])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
735 |
qed "NotS1LeadstoS6"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
736 |
|
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
737 |
Goal "[| sigma |= ~S1 rmhist p ~> S6 rmhist p; \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
738 |
\ sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |] \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
739 |
\ ==> sigma |= []<>S1 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
740 |
by (rtac classical 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
741 |
by (asm_full_simp_tac (simpset() addsimps [temp_use NotBox, NotDmd]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
742 |
by (auto_tac (MI_css addSEs2 [mp,leadsto_infinite] addSDs2 [DBImplBD])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
743 |
qed "S1Infinite"; |
3807 | 744 |
|
745 |
section "Refinement proof (step 1.5)"; |
|
746 |
||
747 |
(* Prove invariants of the implementation: |
|
748 |
a. memory invariant |
|
749 |
b. "implementation invariant": always in states S1,...,S6 |
|
750 |
*) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
751 |
Goal "|- IPImp p --> (ALL l. []$MemInv mm l)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
752 |
by (auto_tac (MI_css addsimps2 [IPImp_def,box_stp_act] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
753 |
addSIs2 [MemoryInvariantAll])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
754 |
qed "Step1_5_1a"; |
3807 | 755 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
756 |
Goal "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
757 |
\ & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
758 |
\ --> []ImpInv rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
759 |
by (inv_tac MI_css 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
760 |
by (auto_tac (MI_css addsimps2 [Init_def, ImpInv_def, box_stp_act] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
761 |
addSDs2 [Step1_1] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
762 |
addDs2 [S1_successors,S2_successors,S3_successors, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
763 |
S4_successors,S5_successors,S6_successors])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
764 |
qed "Step1_5_1b"; |
3807 | 765 |
|
766 |
(*** Initialization ***) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
767 |
Goal "|- Init(ImpInit p & HInit rmhist p) --> Init(PInit (resbar rmhist) p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
768 |
by (auto_tac (MI_css addsimps2 [Init_def] addSIs2 [Step1_1,Step1_3])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
769 |
qed "Step1_5_2a"; |
3807 | 770 |
|
771 |
(*** step simulation ***) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
772 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
773 |
\ & $ImpInv rmhist p & (!l. $MemInv mm l)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
774 |
\ --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
775 |
by (auto_tac (MI_css addsimps2 [ImpInv_def] addSEs2 [STL4E] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
776 |
addSDs2 [S1safe,S2safe,S3safe,S4safe,S5safe,S6safe])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
777 |
qed "Step1_5_2b"; |
3807 | 778 |
|
779 |
(*** Liveness ***) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
780 |
Goal "|- IPImp p & HistP rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
781 |
\ --> Init(ImpInit p & HInit rmhist p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
782 |
\ & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
783 |
\ & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
784 |
\ & ImpLive p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
785 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
786 |
by (subgoal_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
787 |
"sigma |= Init(ImpInit p & HInit rmhist p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
788 |
\ & [](ImpNext p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
789 |
\ & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
790 |
\ & [](ALL l. $MemInv mm l)" 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
791 |
by (auto_tac (MI_css addsimps2 [split_box_conj,box_stp_act] addSDs2 [Step1_5_1b])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
792 |
by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
793 |
ImpLive_def,c_def,r_def,m_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
794 |
by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
795 |
HistP_def,Init_def,ImpInit_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
796 |
by (force_tac (MI_css addsimps2 [IPImp_def,MClkIPSpec_def,RPCIPSpec_def,RPSpec_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
797 |
ImpNext_def,c_def,r_def,m_def,split_box_conj]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
798 |
by (force_tac (MI_css addsimps2 [HistP_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
799 |
by (force_tac (MI_css addsimps2 [temp_use allT] addSDs2 [Step1_5_1a]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
800 |
qed "GoodImpl"; |
3807 | 801 |
|
6255 | 802 |
(* The implementation is infinitely often in state S1... *) |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
803 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
804 |
\ & [](ALL l. $MemInv mm l) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
805 |
\ & []($ImpInv rmhist p) & ImpLive p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
806 |
\ --> []<>S1 rmhist p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
807 |
by (clarsimp_tac (MI_css addsimps2 [ImpLive_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
808 |
by (rtac S1Infinite 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
809 |
by (force_tac |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
810 |
(MI_css addsimps2 [split_box_conj,box_stp_act] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
811 |
addSIs2 [NotS1LeadstoS6,S2_live,S3_live,S4a_live,S4b_live,S5_live]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
812 |
by (auto_tac (MI_css addsimps2 [split_box_conj] addSIs2 [S6_live])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
813 |
qed "Step1_5_3a"; |
3807 | 814 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
815 |
(* ... and therefore satisfies the fairness requirements of the specification *) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
816 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
817 |
\ & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
818 |
\ --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
819 |
by (auto_tac (MI_css addSIs2 [RNext_fair,Step1_5_3a])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
820 |
qed "Step1_5_3b"; |
3807 | 821 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
822 |
Goal "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
823 |
\ & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
824 |
\ --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
825 |
by (auto_tac (MI_css addSIs2 [Return_fair,Step1_5_3a])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
826 |
qed "Step1_5_3c"; |
3807 | 827 |
|
828 |
(* QED step of step 1 *) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
829 |
Goal "|- IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
830 |
by (auto_tac (MI_css addsimps2 [UPSpec_def,split_box_conj] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
831 |
addSDs2 [GoodImpl] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
832 |
addSIs2 [Step1_5_2a,Step1_5_2b,Step1_5_3b,Step1_5_3c])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
833 |
qed "Step1"; |
3807 | 834 |
|
835 |
(* ------------------------------ Step 2 ------------------------------ *) |
|
836 |
section "Step 2"; |
|
837 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
838 |
Goal "|- Write rmCh mm ires p l & ImpNext p\ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
839 |
\ & [HNext rmhist p]_(c p, r p, m p, rmhist!p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
840 |
\ & $ImpInv rmhist p \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
841 |
\ --> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
842 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
843 |
by (dtac (action_use WriteS4) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
844 |
by (atac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
845 |
by (split_idle_tac [] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
846 |
by (auto_tac (MI_css addsimps2 [ImpNext_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
847 |
addSDs2 [S4EnvUnch,S4ClerkUnch,S4RPCUnch])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
848 |
by (auto_tac (MI_css addsimps2 [square_def] addDs2 [S4Write])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
849 |
qed "Step2_2a"; |
3807 | 850 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
851 |
Goal "|- (ALL p. ImpNext p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
852 |
\ & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
853 |
\ & (ALL p. $ImpInv rmhist p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
854 |
\ & [EX q. Write rmCh mm ires q l]_(mm!l) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
855 |
\ --> [EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
856 |
by (auto_tac (MI_css addSIs2 [squareCI] addSEs2 [squareE])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
857 |
by (REPEAT (ares_tac [exI, action_use Step1_4_4b] 1)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
858 |
by (force_tac (MI_css addSIs2 [WriteS4]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
859 |
by (auto_tac (MI_css addSDs2 [Step2_2a])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
860 |
qed "Step2_2"; |
3807 | 861 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
862 |
Goal "|- []( (ALL p. ImpNext p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
863 |
\ & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
864 |
\ & (ALL p. $ImpInv rmhist p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
865 |
\ & [EX q. Write rmCh mm ires q l]_(mm!l)) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
866 |
\ --> [][EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
867 |
by (force_tac (MI_css addSEs2 [STL4E] addSDs2 [Step2_2]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
868 |
qed "Step2_lemma"; |
3807 | 869 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
870 |
Goal "|- #l : #MemLoc & (ALL p. IPImp p & HistP rmhist p) \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
871 |
\ --> MSpec memCh mm (resbar rmhist) l"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
872 |
by (auto_tac (MI_css addsimps2 [MSpec_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
873 |
by (force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
874 |
by (auto_tac (MI_css addSIs2 [Step2_lemma] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
875 |
addsimps2 [split_box_conj,all_box])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
876 |
by (force_tac (MI_css addsimps2 [IPImp_def,MSpec_def]) 4); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
877 |
by (auto_tac (MI_css addsimps2 [split_box_conj] addSEs2 [allE] addSDs2 [GoodImpl])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
878 |
qed "Step2"; |
3807 | 879 |
|
880 |
(* ----------------------------- Main theorem --------------------------------- *) |
|
881 |
section "Memory implementation"; |
|
882 |
||
883 |
(* The combination of a legal caller, the memory clerk, the RPC component, |
|
884 |
and a reliable memory implement the unreliable memory. |
|
885 |
*) |
|
886 |
||
887 |
(* Implementation of internal specification by combination of implementation |
|
888 |
and history variable with explicit refinement mapping |
|
889 |
*) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
890 |
Goal "|- Implementation & Hist rmhist --> IUSpec memCh mm (resbar rmhist)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
891 |
by (auto_tac (MI_css addsimps2 [IUSpec_def,Implementation_def,IPImp_def, |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
892 |
MClkISpec_def,RPCISpec_def,IRSpec_def,Hist_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
893 |
addSIs2 [Step1,Step2])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
894 |
qed "Impl_IUSpec"; |
3807 | 895 |
|
896 |
(* The main theorem: introduce hiding and eliminate history variable. *) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
897 |
Goal "|- Implementation --> USpec memCh"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
898 |
by (Clarsimp_tac 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
899 |
by (forward_tac [temp_use History] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
900 |
by (auto_tac (MI_css addsimps2 [USpec_def] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
901 |
addIs2 [eexI, Impl_IUSpec, MI_base] |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
902 |
addSEs2 [eexE])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7570
diff
changeset
|
903 |
qed "Implementation"; |