3807
|
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 |
]);
|