|
1 (* |
|
2 File: MIlive.ML |
|
3 Author: Stephan Merz |
|
4 Copyright: 1997 University of Munich |
|
5 |
|
6 RPC-Memory example: Lower-level lemmas for the liveness proof |
|
7 *) |
|
8 |
|
9 (* Liveness assertions for the different implementation states, based on the |
|
10 fairness conditions. Prove subgoals of WF1 / SF1 rules as separate lemmas |
|
11 for readability. Reuse action proofs from safety part. |
|
12 *) |
|
13 |
|
14 (* ------------------------------ State S1 ------------------------------ *) |
|
15 |
|
16 qed_goal "S1_successors" MemoryImplementation.thy |
|
17 "$(S1 rmhist p) .& ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \ |
|
18 \ .-> $(S1 rmhist p)` .| $(S2 rmhist p)`" |
|
19 (fn _ => [split_idle_tac [] 1, |
|
20 auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_1]) |
|
21 ]); |
|
22 |
|
23 (* Show that the implementation can satisfy the high-level fairness requirements |
|
24 by entering the state S1 infinitely often. |
|
25 *) |
|
26 |
|
27 qed_goal "S1_RNextdisabled" MemoryImplementation.thy |
|
28 "$(S1 rmhist p) .-> \ |
|
29 \ .~$(Enabled (<RNext memCh mem (resbar rmhist) p>_<rtrner memCh @ p, resbar rmhist @ p>))" |
|
30 (fn _ => [action_simp_tac (!simpset addsimps [angle_def,S_def,S1_def]) |
|
31 [notI] [enabledE,MemoryidleE] 1, |
|
32 auto_tac MI_fast_css |
|
33 ]); |
|
34 |
|
35 qed_goal "S1_Returndisabled" MemoryImplementation.thy |
|
36 "$(S1 rmhist p) .-> \ |
|
37 \ .~$(Enabled (<MemReturn memCh (resbar rmhist) p>_<rtrner memCh @ p, resbar rmhist @ p>))" |
|
38 (fn _ => [action_simp_tac (!simpset addsimps [angle_def,MemReturn_def,Return_def,S_def,S1_def]) |
|
39 [notI] [enabledE] 1 |
|
40 ]); |
|
41 |
|
42 qed_goal "RNext_fair" MemoryImplementation.thy |
|
43 "!!sigma. (sigma |= []<>($(S1 rmhist p))) \ |
|
44 \ ==> (sigma |= WF(RNext memCh mem (resbar rmhist) p)_<rtrner memCh @ p, resbar rmhist @ p>)" |
|
45 (fn _ => [auto_tac (MI_css addsimps2 [temp_rewrite WF_alt] |
|
46 addSIs2 [S1_RNextdisabled] addSEs2 [STL4E,DmdImplE]) |
|
47 ]); |
|
48 |
|
49 qed_goal "Return_fair" MemoryImplementation.thy |
|
50 "!!sigma. (sigma |= []<>($(S1 rmhist p))) \ |
|
51 \ ==> (sigma |= WF(MemReturn memCh (resbar rmhist) p)_<rtrner memCh @ p, resbar rmhist @ p>)" |
|
52 (fn _ => [auto_tac (MI_css addsimps2 [temp_rewrite WF_alt] |
|
53 addSIs2 [S1_Returndisabled] addSEs2 [STL4E,DmdImplE]) |
|
54 ]); |
|
55 |
|
56 (* ------------------------------ State S2 ------------------------------ *) |
|
57 |
|
58 qed_goal "S2_successors" MemoryImplementation.thy |
|
59 "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
60 \ .-> $(S2 rmhist p)` .| $(S3 rmhist p)`" |
|
61 (fn _ => [split_idle_tac [] 1, |
|
62 auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_2]) |
|
63 ]); |
|
64 |
|
65 qed_goal "S2MClkFwd_successors" MemoryImplementation.thy |
|
66 "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
67 \ .& <MClkFwd memCh crCh cst p>_(c p) \ |
|
68 \ .-> $(S3 rmhist p)`" |
|
69 (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_2]) ]); |
|
70 |
|
71 qed_goal "S2MClkFwd_enabled" MemoryImplementation.thy |
|
72 "$(S2 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
73 \ .-> $(Enabled (<MClkFwd memCh crCh cst p>_(c p)))" |
|
74 (fn _ => [cut_facts_tac [MI_base] 1, |
|
75 auto_tac (MI_css addsimps2 [c_def,base_pair] |
|
76 addSIs2 [MClkFwd_ch_enabled,action_mp MClkFwd_enabled]), |
|
77 ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S2_def]) [] []) |
|
78 ]); |
|
79 |
|
80 qed_goal "S2_live" MemoryImplementation.thy |
|
81 "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) .& WF(MClkFwd memCh crCh cst p)_(c p) \ |
|
82 \ .-> ($(S2 rmhist p) ~> $(S3 rmhist p))" |
|
83 (fn _ => [REPEAT (resolve_tac [WF1,S2_successors, |
|
84 S2MClkFwd_successors,S2MClkFwd_enabled] 1) |
|
85 ]); |
|
86 |
|
87 |
|
88 (* ------------------------------ State S3 ------------------------------ *) |
|
89 |
|
90 qed_goal "S3_successors" MemoryImplementation.thy |
|
91 "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
92 \ .-> $(S3 rmhist p)` .| ($(S4 rmhist p) .| $(S6 rmhist p))`" |
|
93 (fn _ => [split_idle_tac [] 1, |
|
94 auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_3]) |
|
95 ]); |
|
96 |
|
97 qed_goal "S3RPC_successors" MemoryImplementation.thy |
|
98 "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
99 \ .& <RPCNext crCh rmCh rst p>_(r p) \ |
|
100 \ .-> ($(S4 rmhist p) .| $(S6 rmhist p))`" |
|
101 (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_3]) ]); |
|
102 |
|
103 qed_goal "S3RPC_enabled" MemoryImplementation.thy |
|
104 "$(S3 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
105 \ .-> $(Enabled (<RPCNext crCh rmCh rst p>_(r p)))" |
|
106 (fn _ => [cut_facts_tac [MI_base] 1, |
|
107 auto_tac (MI_css addsimps2 [r_def,base_pair] |
|
108 addSIs2 [RPCFail_Next_enabled,action_mp RPCFail_enabled]), |
|
109 ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S3_def]) [] []) |
|
110 ]); |
|
111 |
|
112 qed_goal "S3_live" MemoryImplementation.thy |
|
113 "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
114 \ .& WF(RPCNext crCh rmCh rst p)_(r p) \ |
|
115 \ .-> ($(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p)))" |
|
116 (fn _ => [REPEAT (resolve_tac [WF1,S3_successors,S3RPC_successors,S3RPC_enabled] 1)]); |
|
117 |
|
118 (* ------------- State S4 -------------------------------------------------- *) |
|
119 |
|
120 qed_goal "S4_successors" MemoryImplementation.thy |
|
121 "$(S4 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \ |
|
122 \ .& (RALL l. $(MemInv mem l))) \ |
|
123 \ .-> $(S4 rmhist p)` .| $(S5 rmhist p)`" |
|
124 (fn _ => [split_idle_tac [] 1, |
|
125 auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_4]) |
|
126 ]); |
|
127 |
|
128 (* ------------- State S4a: S4 /\ (ires p = NotAResult) ------------------------------ *) |
|
129 |
|
130 qed_goal "S4a_successors" MemoryImplementation.thy |
|
131 "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ |
|
132 \ .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \ |
|
133 \ .& (RALL l. $(MemInv mem l))) \ |
|
134 \ .-> ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult))` \ |
|
135 \ .| (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))`" |
|
136 (fn _ => [split_idle_tac [m_def] 1, |
|
137 auto_tac (MI_css addsimps2 [m_def] addSEs2 [action_conjimpE Step1_2_4]) |
|
138 ]); |
|
139 |
|
140 qed_goal "S4aRNext_successors" MemoryImplementation.thy |
|
141 "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ |
|
142 \ .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \ |
|
143 \ .& (RALL l. $(MemInv mem l))) \ |
|
144 \ .& <RNext rmCh mem ires p>_(m p) \ |
|
145 \ .-> (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))`" |
|
146 (fn _ => [auto_tac (MI_css addsimps2 [angle_def] |
|
147 addSEs2 [action_conjimpE Step1_2_4, |
|
148 action_conjimpE ReadResult, action_impE WriteResult]) |
|
149 ]); |
|
150 |
|
151 qed_goal "S4aRNext_enabled" MemoryImplementation.thy |
|
152 "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ |
|
153 \ .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \ |
|
154 \ .& (RALL l. $(MemInv mem l))) \ |
|
155 \ .-> $(Enabled (<RNext rmCh mem ires p>_(m p)))" |
|
156 (fn _ => [auto_tac (MI_css addsimps2 [m_def] addSIs2 [action_mp RNext_enabled]), |
|
157 ALLGOALS (cut_facts_tac [MI_base]), |
|
158 auto_tac (MI_css addsimps2 [base_pair]), |
|
159 (* it's faster to expand S4 only where necessary *) |
|
160 action_simp_tac (!simpset addsimps [S_def,S4_def]) [] [] 1 |
|
161 ]); |
|
162 |
|
163 qed_goal "S4a_live" MemoryImplementation.thy |
|
164 "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& (RALL l. $(MemInv mem l))) \ |
|
165 \ .& WF(RNext rmCh mem ires p)_(m p) \ |
|
166 \ .-> (($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ |
|
167 \ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p))" |
|
168 (fn _ => [rtac WF1 1, |
|
169 ALLGOALS (action_simp_tac (!simpset) |
|
170 (map ((rewrite_rule [slice_def]) o action_mp) |
|
171 [S4a_successors,S4aRNext_successors,S4aRNext_enabled]) |
|
172 []) |
|
173 ]); |
|
174 |
|
175 (* ------------- State S4b: S4 /\ (ires p # NotAResult) ------------------------------ *) |
|
176 |
|
177 qed_goal "S4b_successors" MemoryImplementation.thy |
|
178 "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) \ |
|
179 \ .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \ |
|
180 \ .& (RALL l. $(MemInv mem l))) \ |
|
181 \ .-> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult))` .| $(S5 rmhist p)`" |
|
182 (fn _ => [split_idle_tac [m_def] 1, |
|
183 auto_tac (MI_css addSEs2 (action_impE WriteResult |
|
184 :: map action_conjimpE [Step1_2_4,ReadResult])) |
|
185 ]); |
|
186 |
|
187 qed_goal "S4bReturn_successors" MemoryImplementation.thy |
|
188 "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) \ |
|
189 \ .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \ |
|
190 \ .& (RALL l. $(MemInv mem l))) \ |
|
191 \ .& <MemReturn rmCh ires p>_(m p) \ |
|
192 \ .-> ($(S5 rmhist p))`" |
|
193 (fn _ => [auto_tac (MI_css addsimps2 [angle_def] |
|
194 addSEs2 [action_conjimpE Step1_2_4] |
|
195 addEs2 [action_conjimpE ReturnNotReadWrite]) |
|
196 ]); |
|
197 |
|
198 qed_goal "S4bReturn_enabled" MemoryImplementation.thy |
|
199 "($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) \ |
|
200 \ .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> \ |
|
201 \ .& (RALL l. $(MemInv mem l))) \ |
|
202 \ .-> $(Enabled (<MemReturn rmCh ires p>_(m p)))" |
|
203 (fn _ => [cut_facts_tac [MI_base] 1, |
|
204 auto_tac (MI_css addsimps2 [m_def,base_pair] |
|
205 addSIs2 [action_mp MemReturn_enabled]), |
|
206 ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S4_def]) [] []) |
|
207 ]); |
|
208 |
|
209 qed_goal "S4b_live" MemoryImplementation.thy |
|
210 "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& (RALL l. $(MemInv mem l))) \ |
|
211 \ .& WF(MemReturn rmCh ires p)_(m p) \ |
|
212 \ .-> (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p))" |
|
213 (fn _ => [rtac WF1 1, |
|
214 ALLGOALS (action_simp_tac (!simpset) |
|
215 (map ((rewrite_rule [slice_def]) o action_mp) |
|
216 [S4b_successors,S4bReturn_successors,S4bReturn_enabled]) |
|
217 [allE]) |
|
218 ]); |
|
219 |
|
220 (* ------------------------------ State S5 ------------------------------ *) |
|
221 |
|
222 qed_goal "S5_successors" MemoryImplementation.thy |
|
223 "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
224 \ .-> $(S5 rmhist p)` .| $(S6 rmhist p)`" |
|
225 (fn _ => [split_idle_tac [] 1, |
|
226 auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_5]) |
|
227 ]); |
|
228 |
|
229 qed_goal "S5RPC_successors" MemoryImplementation.thy |
|
230 "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
231 \ .& <RPCNext crCh rmCh rst p>_(r p) \ |
|
232 \ .-> $(S6 rmhist p)`" |
|
233 (fn _ => [ auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_5]) ]); |
|
234 |
|
235 qed_goal "S5RPC_enabled" MemoryImplementation.thy |
|
236 "$(S5 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
237 \ .-> $(Enabled (<RPCNext crCh rmCh rst p>_(r p)))" |
|
238 (fn _ => [cut_facts_tac [MI_base] 1, |
|
239 auto_tac (MI_css addsimps2 [r_def,base_pair] |
|
240 addSIs2 [RPCFail_Next_enabled,action_mp RPCFail_enabled]), |
|
241 ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S5_def]) [] []) |
|
242 ]); |
|
243 |
|
244 qed_goal "S5_live" MemoryImplementation.thy |
|
245 "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
246 \ .& WF(RPCNext crCh rmCh rst p)_(r p) \ |
|
247 \ .-> ($(S5 rmhist p) ~> $(S6 rmhist p))" |
|
248 (fn _ => [REPEAT (resolve_tac [WF1,S5_successors,S5RPC_successors,S5RPC_enabled] 1)]); |
|
249 |
|
250 |
|
251 (* ------------------------------ State S6 ------------------------------ *) |
|
252 |
|
253 qed_goal "S6_successors" MemoryImplementation.thy |
|
254 "$(S6 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
255 \ .-> $(S1 rmhist p)` .| $(S3 rmhist p)` .| $(S6 rmhist p)`" |
|
256 (fn _ => [split_idle_tac [] 1, |
|
257 auto_tac (MI_css addSEs2 [action_conjimpE Step1_2_6]) |
|
258 ]); |
|
259 |
|
260 qed_goal "S6MClkReply_successors" MemoryImplementation.thy |
|
261 "$(S6 rmhist p) .& (ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p>) \ |
|
262 \ .& <MClkReply memCh crCh cst p>_(c p) \ |
|
263 \ .-> $(S1 rmhist p)`" |
|
264 (fn _ => [auto_tac (MI_css addsimps2 [angle_def] addSEs2 [action_conjimpE Step1_2_6, |
|
265 action_impE MClkReplyNotRetry]) |
|
266 ]); |
|
267 |
|
268 qed_goal "MClkReplyS6" MemoryImplementation.thy |
|
269 "$(ImpInv rmhist p) .& <MClkReply memCh crCh cst p>_(c p) .-> $(S6 rmhist p)" |
|
270 (fn _ => [action_simp_tac |
|
271 (!simpset addsimps |
|
272 [angle_def,MClkReply_def,Return_def, |
|
273 ImpInv_def,S_def,S1_def,S2_def,S3_def,S4_def,S5_def]) |
|
274 [] [] 1 |
|
275 ]); |
|
276 |
|
277 qed_goal "S6MClkReply_enabled" MemoryImplementation.thy |
|
278 "$(S6 rmhist p) .-> $(Enabled (<MClkReply memCh crCh cst p>_(c p)))" |
|
279 (fn _ => [cut_facts_tac [MI_base] 1, |
|
280 auto_tac (MI_css addsimps2 [c_def,base_pair] |
|
281 addSIs2 [action_mp MClkReply_enabled]), |
|
282 ALLGOALS (action_simp_tac (!simpset addsimps [S_def,S6_def]) [] []) |
|
283 ]); |
|
284 |
|
285 qed_goal "S6_live" MemoryImplementation.thy |
|
286 "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& $(ImpInv rmhist p)) \ |
|
287 \ .& SF(MClkReply memCh crCh cst p)_(c p) .& []<>($(S6 rmhist p)) \ |
|
288 \ .-> []<>($(S1 rmhist p))" |
|
289 (fn _ => [Auto_tac(), |
|
290 subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1, |
|
291 eres_inst_tac [("P","<MClkReply memCh crCh cst p>_(c p)")] |
|
292 EnsuresInfinite 1, atac 1, |
|
293 action_simp_tac (!simpset) [] |
|
294 (map action_conjimpE [MClkReplyS6,S6MClkReply_successors]) 1, |
|
295 auto_tac (MI_css addsimps2 [SF_def]), |
|
296 etac swap 1, |
|
297 auto_tac (MI_css addSIs2 [action_mp S6MClkReply_enabled] |
|
298 addSEs2 [STL4E,DmdImplE]) |
|
299 ]); |
|
300 |
|
301 (* ------------------------------ complex leadsto properties ------------------------------ *) |
|
302 |
|
303 qed_goal "S5S6LeadstoS6" MemoryImplementation.thy |
|
304 "!!sigma. (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) \ |
|
305 \ ==> (sigma |= ($(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" |
|
306 (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro, |
|
307 temp_unlift LatticeReflexivity]) |
|
308 ]); |
|
309 |
|
310 qed_goal "S4bS5S6LeadstoS6" MemoryImplementation.thy |
|
311 "!!sigma. [| (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ |
|
312 \ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ |
|
313 \ ==> (sigma |= (($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" |
|
314 (fn _ => [auto_tac (MI_css addSIs2 [LatticeDisjunctionIntro,S5S6LeadstoS6] |
|
315 addIs2 [LatticeTransitivity]) |
|
316 ]); |
|
317 |
|
318 qed_goal "S4S5S6LeadstoS6" MemoryImplementation.thy |
|
319 "!!sigma. [| (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ |
|
320 \ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \ |
|
321 \ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ |
|
322 \ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ |
|
323 \ ==> (sigma |= ($(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" |
|
324 (fn _ => [subgoal_tac "sigma |= (($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) .| ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p)" 1, |
|
325 eres_inst_tac [("G", "($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) .| ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p) .| $(S6 rmhist p)")] LatticeTransitivity 1, |
|
326 SELECT_GOAL (auto_tac (MI_css addSIs2 [ImplLeadsto, temp_unlift necT])) 1, |
|
327 rtac LatticeDisjunctionIntro 1, |
|
328 etac LatticeTransitivity 1, |
|
329 etac LatticeTriangle 1, atac 1, |
|
330 auto_tac (MI_css addSIs2 [S4bS5S6LeadstoS6]) |
|
331 ]); |
|
332 |
|
333 qed_goal "S3S4S5S6LeadstoS6" MemoryImplementation.thy |
|
334 "!!sigma. [| (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p))); \ |
|
335 \ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ |
|
336 \ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \ |
|
337 \ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ |
|
338 \ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ |
|
339 \ ==> (sigma |= ($(S3 rmhist p) .| $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" |
|
340 (fn _ => [rtac LatticeDisjunctionIntro 1, |
|
341 rtac LatticeTriangle 1, atac 2, |
|
342 rtac (S4S5S6LeadstoS6 RS LatticeTransitivity) 1, |
|
343 auto_tac (MI_css addSIs2 [S4S5S6LeadstoS6,temp_unlift necT] |
|
344 addIs2 [ImplLeadsto]) |
|
345 ]); |
|
346 |
|
347 qed_goal "S2S3S4S5S6LeadstoS6" MemoryImplementation.thy |
|
348 "!!sigma. [| (sigma |= $(S2 rmhist p) ~> $(S3 rmhist p)); \ |
|
349 \ (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p))); \ |
|
350 \ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ |
|
351 \ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \ |
|
352 \ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ |
|
353 \ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ |
|
354 \ ==> (sigma |= ($(S2 rmhist p) .| $(S3 rmhist p) .| $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p)) ~> $(S6 rmhist p))" |
|
355 (fn _ => [rtac LatticeDisjunctionIntro 1, |
|
356 rtac LatticeTransitivity 1, atac 2, |
|
357 rtac (S3S4S5S6LeadstoS6 RS LatticeTransitivity) 1, |
|
358 auto_tac (MI_css addSIs2 [S3S4S5S6LeadstoS6,temp_unlift necT] |
|
359 addIs2 [ImplLeadsto]) |
|
360 ]); |
|
361 |
|
362 qed_goal "NotS1LeadstoS6" MemoryImplementation.thy |
|
363 "!!sigma. [| (sigma |= []($(ImpInv rmhist p))); \ |
|
364 \ (sigma |= $(S2 rmhist p) ~> $(S3 rmhist p)); \ |
|
365 \ (sigma |= $(S3 rmhist p) ~> ($(S4 rmhist p) .| $(S6 rmhist p))); \ |
|
366 \ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .= #NotAResult)) \ |
|
367 \ ~> ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) .| $(S5 rmhist p)); \ |
|
368 \ (sigma |= ($(S4 rmhist p) .& ($(ires@p) .~= #NotAResult)) ~> $(S5 rmhist p)); \ |
|
369 \ (sigma |= $(S5 rmhist p) ~> $(S6 rmhist p)) |] \ |
|
370 \ ==> (sigma |= .~$(S1 rmhist p) ~> $(S6 rmhist p))" |
|
371 (fn _ => [rtac (S2S3S4S5S6LeadstoS6 RS LatticeTransitivity) 1, |
|
372 auto_tac (MI_css addsimps2 [ImpInv_def] addIs2 [ImplLeadsto] addSEs2 [STL4E]) |
|
373 ]); |
|
374 |
|
375 qed_goal "S1Infinite" MemoryImplementation.thy |
|
376 "!!sigma. [| (sigma |= .~$(S1 rmhist p) ~> $(S6 rmhist p)); \ |
|
377 \ (sigma |= []<>($(S6 rmhist p)) .-> []<>($(S1 rmhist p))) |] \ |
|
378 \ ==> (sigma |= []<>($(S1 rmhist p)))" |
|
379 (fn _ => [rtac classical 1, |
|
380 asm_full_simp_tac (!simpset addsimps [NotBox, temp_rewrite NotDmd]) 1, |
|
381 auto_tac (MI_css addSEs2 [mp,leadsto_infinite] addSDs2 [temp_mp DBImplBDAct]) |
|
382 ]); |