8334
|
1 |
(* Title: HOL/UNITY/Reachability
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tanja Vos, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2000 University of Cambridge
|
|
5 |
|
|
6 |
Reachability in Graphs
|
|
7 |
|
|
8 |
From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
|
|
9 |
*)
|
|
10 |
|
|
11 |
bind_thm("E_imp_in_V_L", Graph2 RS conjunct1);
|
|
12 |
bind_thm("E_imp_in_V_R", Graph2 RS conjunct2);
|
|
13 |
|
|
14 |
Goal "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v";
|
|
15 |
by (rtac (MA7 RS PSP_Stable RS LeadsTo_weaken_L) 1);
|
|
16 |
by (rtac MA6 3);
|
|
17 |
by (auto_tac (claset(), simpset() addsimps [E_imp_in_V_L, E_imp_in_V_R]));
|
|
18 |
qed "lemma2";
|
|
19 |
|
|
20 |
Goal "(v,w) : E ==> F : reachable v LeadsTo reachable w";
|
|
21 |
by (rtac (MA4 RS Always_LeadsTo_weaken) 1);
|
|
22 |
by (rtac lemma2 2);
|
|
23 |
by (auto_tac (claset(), simpset() addsimps [nmsg_eq_def, nmsg_gt_def]));
|
|
24 |
qed "Induction_base";
|
|
25 |
|
|
26 |
Goal "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w";
|
|
27 |
by (etac REACHABLE.induct 1);
|
|
28 |
by (rtac subset_imp_LeadsTo 1);
|
|
29 |
by (Blast_tac 1);
|
|
30 |
by (blast_tac (claset() addIs [LeadsTo_Trans, Induction_base]) 1);
|
|
31 |
qed "REACHABLE_LeadsTo_reachable";
|
|
32 |
|
|
33 |
Goal "F : {s. (root,v) : REACHABLE} LeadsTo reachable v";
|
|
34 |
by (rtac single_LeadsTo_I 1);
|
|
35 |
by (full_simp_tac (simpset() addsplits [split_if_asm]) 1);
|
|
36 |
by (rtac (MA1 RS Always_LeadsToI) 1);
|
|
37 |
by (etac (REACHABLE_LeadsTo_reachable RS LeadsTo_weaken_L) 1);
|
|
38 |
by Auto_tac;
|
|
39 |
qed "Detects_part1";
|
|
40 |
|
|
41 |
|
|
42 |
Goalw [Detects_def]
|
|
43 |
"v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}";
|
|
44 |
by Auto_tac;
|
|
45 |
by (blast_tac (claset() addIs [MA2 RS Always_weaken]) 2);
|
|
46 |
by (rtac (Detects_part1 RS LeadsTo_weaken_L) 1);
|
|
47 |
by (Blast_tac 1);
|
|
48 |
qed "Reachability_Detected";
|
|
49 |
|
|
50 |
|
|
51 |
Goal "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})";
|
|
52 |
by (etac (Reachability_Detected RS Detects_Imp_LeadstoEQ) 1);
|
|
53 |
qed "LeadsTo_Reachability";
|
|
54 |
|
|
55 |
(* ------------------------------------ *)
|
|
56 |
|
|
57 |
(* Some lemmas about <==> *)
|
|
58 |
|
|
59 |
Goalw [Equality_def]
|
|
60 |
"(reachable v <==> {s. (root,v) : REACHABLE}) = \
|
|
61 |
\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
|
|
62 |
by (Blast_tac 1);
|
|
63 |
qed "Eq_lemma1";
|
|
64 |
|
|
65 |
|
|
66 |
Goalw [Equality_def]
|
|
67 |
"(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) = \
|
|
68 |
\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
|
|
69 |
by Auto_tac;
|
|
70 |
qed "Eq_lemma2";
|
|
71 |
|
|
72 |
(* ------------------------------------ *)
|
|
73 |
|
|
74 |
|
|
75 |
(* Some lemmas about final (I don't need all of them!) *)
|
|
76 |
|
|
77 |
Goalw [final_def, Equality_def]
|
|
78 |
"(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) & \
|
|
79 |
\ s : nmsg_eq 0 (v,w)}) \
|
|
80 |
\ <= final";
|
|
81 |
by Auto_tac;
|
|
82 |
by (ftac E_imp_in_V_R 1);
|
|
83 |
by (ftac E_imp_in_V_L 1);
|
|
84 |
by (Blast_tac 1);
|
|
85 |
qed "final_lemma1";
|
|
86 |
|
|
87 |
Goalw [final_def, Equality_def]
|
|
88 |
"E~={} \
|
|
89 |
\ ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))} \
|
|
90 |
\ Int nmsg_eq 0 e) <= final";
|
|
91 |
by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
|
|
92 |
by (ftac E_imp_in_V_L 1);
|
|
93 |
by (Blast_tac 1);
|
|
94 |
qed "final_lemma2";
|
|
95 |
|
|
96 |
Goal "E~={} \
|
|
97 |
\ ==> (INT v: V. INT e: E. \
|
|
98 |
\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
|
|
99 |
\ <= final";
|
|
100 |
by (ftac final_lemma2 1);
|
|
101 |
by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
|
|
102 |
qed "final_lemma3";
|
|
103 |
|
|
104 |
|
|
105 |
Goal "E~={} \
|
|
106 |
\ ==> (INT v: V. INT e: E. \
|
|
107 |
\ {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e) \
|
|
108 |
\ = final";
|
|
109 |
by (rtac subset_antisym 1);
|
|
110 |
by (etac final_lemma2 1);
|
|
111 |
by (rewrite_goals_tac [final_def,Equality_def]);
|
|
112 |
by (Blast_tac 1);
|
|
113 |
qed "final_lemma4";
|
|
114 |
|
|
115 |
Goal "E~={} \
|
|
116 |
\ ==> (INT v: V. INT e: E. \
|
|
117 |
\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
|
|
118 |
\ = final";
|
|
119 |
by (ftac final_lemma4 1);
|
|
120 |
by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
|
|
121 |
qed "final_lemma5";
|
|
122 |
|
|
123 |
|
|
124 |
Goal "(INT v: V. INT w: V. \
|
|
125 |
\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)) \
|
|
126 |
\ <= final";
|
|
127 |
by (simp_tac (simpset() addsimps [Eq_lemma2, Int_def]) 1);
|
|
128 |
by (rtac final_lemma1 1);
|
|
129 |
qed "final_lemma6";
|
|
130 |
|
|
131 |
|
|
132 |
Goalw [final_def]
|
|
133 |
"final = \
|
|
134 |
\ (INT v: V. INT w: V. \
|
|
135 |
\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int \
|
|
136 |
\ (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))";
|
|
137 |
by (rtac subset_antisym 1);
|
|
138 |
by (Blast_tac 1);
|
|
139 |
by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
|
|
140 |
by (ftac E_imp_in_V_R 1);
|
|
141 |
by (ftac E_imp_in_V_L 1);
|
|
142 |
by (Blast_tac 1);
|
|
143 |
qed "final_lemma7";
|
|
144 |
|
|
145 |
(* ------------------------------------ *)
|
|
146 |
|
|
147 |
|
|
148 |
(* ------------------------------------ *)
|
|
149 |
|
|
150 |
(* Stability theorems *)
|
|
151 |
|
|
152 |
|
|
153 |
Goal "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)";
|
|
154 |
by (dtac (MA2 RS AlwaysD) 1);
|
|
155 |
by Auto_tac;
|
|
156 |
qed "not_REACHABLE_imp_Stable_not_reachable";
|
|
157 |
|
|
158 |
Goal "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})";
|
|
159 |
by (simp_tac (simpset() addsimps [Equality_def, Eq_lemma2]) 1);
|
|
160 |
by (blast_tac (claset() addIs [MA6,not_REACHABLE_imp_Stable_not_reachable]) 1);
|
|
161 |
qed "Stable_reachable_EQ_R";
|
|
162 |
|
|
163 |
|
|
164 |
Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
|
|
165 |
"((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
|
|
166 |
\ <= A Un nmsg_eq 0 (v,w)";
|
|
167 |
by Auto_tac;
|
|
168 |
qed "lemma4";
|
|
169 |
|
|
170 |
|
|
171 |
Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
|
|
172 |
"reachable v Int nmsg_eq 0 (v,w) = \
|
|
173 |
\ ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
|
|
174 |
\ (reachable v Int nmsg_lte 0 (v,w)))";
|
|
175 |
by Auto_tac;
|
|
176 |
qed "lemma5";
|
|
177 |
|
|
178 |
Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
|
|
179 |
"- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v";
|
|
180 |
by Auto_tac;
|
|
181 |
qed "lemma6";
|
|
182 |
|
|
183 |
Goal "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))";
|
|
184 |
by (rtac ([MA5, MA3] MRS Always_Int_I RS Always_weaken) 1);
|
|
185 |
by (rtac lemma4 5);
|
|
186 |
by Auto_tac;
|
|
187 |
qed "Always_reachable_OR_nmsg_0";
|
|
188 |
|
|
189 |
Goal "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))";
|
|
190 |
by (stac lemma5 1);
|
|
191 |
by (blast_tac (claset() addIs [MA5, Always_imp_Stable RS Stable_Int, MA6b]) 1);
|
|
192 |
qed "Stable_reachable_AND_nmsg_0";
|
|
193 |
|
|
194 |
Goal "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)";
|
|
195 |
by (blast_tac (claset() addSIs [Always_weaken RS Always_imp_Stable,
|
|
196 |
lemma6, MA3]) 1);
|
|
197 |
qed "Stable_nmsg_0_OR_reachable";
|
|
198 |
|
|
199 |
Goal "[| v : V; w:V; (root,v) ~: REACHABLE |] \
|
|
200 |
\ ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))";
|
|
201 |
by (rtac ([MA2 RS Always_imp_Stable, Stable_nmsg_0_OR_reachable] MRS
|
|
202 |
Stable_Int RS Stable_eq) 1);
|
|
203 |
by (Blast_tac 4);
|
|
204 |
by Auto_tac;
|
|
205 |
qed "not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0";
|
|
206 |
|
|
207 |
Goal "[| v : V; w:V |] \
|
|
208 |
\ ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int \
|
|
209 |
\ nmsg_eq 0 (v,w))";
|
|
210 |
by (asm_simp_tac
|
|
211 |
(simpset() addsimps [Equality_def, Eq_lemma2,
|
|
212 |
not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0,
|
|
213 |
Stable_reachable_AND_nmsg_0]) 1);
|
|
214 |
qed "Stable_reachable_EQ_R_AND_nmsg_0";
|
|
215 |
|
|
216 |
|
|
217 |
(* ------------------------------------ *)
|
|
218 |
|
|
219 |
|
|
220 |
(* LeadsTo final predicate (Exercise 11.2 page 274) *)
|
|
221 |
|
|
222 |
Goal "UNIV <= (INT v: V. UNIV)";
|
|
223 |
by (Blast_tac 1);
|
|
224 |
val UNIV_lemma = result();
|
|
225 |
|
|
226 |
val UNIV_LeadsTo_completion =
|
|
227 |
[Finite_stable_completion, UNIV_lemma] MRS LeadsTo_weaken_L;
|
|
228 |
|
|
229 |
Goalw [final_def] "E={} ==> F : UNIV LeadsTo final";
|
|
230 |
by (Asm_full_simp_tac 1);
|
|
231 |
by (rtac UNIV_LeadsTo_completion 1);
|
|
232 |
by Safe_tac;
|
|
233 |
by (etac (simplify (simpset()) LeadsTo_Reachability) 1);
|
|
234 |
by (dtac Stable_reachable_EQ_R 1);
|
|
235 |
by (Asm_full_simp_tac 1);
|
|
236 |
qed "LeadsTo_final_E_empty";
|
|
237 |
|
|
238 |
|
|
239 |
Goal "[| v : V; w:V |] \
|
|
240 |
\ ==> F : UNIV LeadsTo \
|
|
241 |
\ ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))";
|
|
242 |
by (rtac (LeadsTo_Reachability RS LeadsTo_Trans) 1);
|
|
243 |
by (Blast_tac 1);
|
|
244 |
by (subgoal_tac "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)" 1);
|
|
245 |
by (Asm_full_simp_tac 1);
|
|
246 |
by (rtac PSP_Stable2 1);
|
|
247 |
by (rtac MA7 1);
|
|
248 |
by (rtac Stable_reachable_EQ_R 3);
|
|
249 |
by Auto_tac;
|
|
250 |
qed "Leadsto_reachability_AND_nmsg_0";
|
|
251 |
|
|
252 |
|
|
253 |
Goal "E~={} ==> F : UNIV LeadsTo final";
|
|
254 |
by (rtac ([LeadsTo_weaken_R, UNIV_lemma] MRS LeadsTo_weaken_L) 1);
|
|
255 |
by (rtac final_lemma6 2);
|
|
256 |
by (rtac Finite_stable_completion 1);
|
|
257 |
by (Blast_tac 1);
|
|
258 |
by (rtac UNIV_LeadsTo_completion 1);
|
|
259 |
by (REPEAT
|
|
260 |
(blast_tac (claset() addIs [Stable_INT,
|
|
261 |
Stable_reachable_EQ_R_AND_nmsg_0,
|
|
262 |
Leadsto_reachability_AND_nmsg_0]) 1));
|
|
263 |
qed "LeadsTo_final_E_NOT_empty";
|
|
264 |
|
|
265 |
|
|
266 |
Goal "F : UNIV LeadsTo final";
|
|
267 |
by (case_tac "E={}" 1);
|
|
268 |
by (rtac LeadsTo_final_E_NOT_empty 2);
|
|
269 |
by (rtac LeadsTo_final_E_empty 1);
|
|
270 |
by Auto_tac;
|
|
271 |
qed "LeadsTo_final";
|
|
272 |
|
|
273 |
(* ------------------------------------ *)
|
|
274 |
|
|
275 |
(* Stability of final (Exercise 11.2 page 274) *)
|
|
276 |
|
|
277 |
Goalw [final_def] "E={} ==> F : Stable final";
|
|
278 |
by (Asm_full_simp_tac 1);
|
|
279 |
by (rtac Stable_INT 1);
|
|
280 |
by (dtac Stable_reachable_EQ_R 1);
|
|
281 |
by (Asm_full_simp_tac 1);
|
|
282 |
qed "Stable_final_E_empty";
|
|
283 |
|
|
284 |
|
|
285 |
Goal "E~={} ==> F : Stable final";
|
|
286 |
by (stac final_lemma7 1);
|
|
287 |
by (rtac Stable_INT 1);
|
|
288 |
by (rtac Stable_INT 1);
|
|
289 |
by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
|
|
290 |
by Safe_tac;
|
|
291 |
by (rtac Stable_eq 1);
|
|
292 |
by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)} Int nmsg_eq 0 (v,w)) = \
|
|
293 |
\ ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- UNIV Un nmsg_eq 0 (v,w)))" 2);
|
|
294 |
by (Blast_tac 2); by (Blast_tac 2);
|
|
295 |
by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R_AND_nmsg_0) 1);
|
|
296 |
by (Blast_tac 1);by (Blast_tac 1);
|
|
297 |
by (rtac Stable_eq 1);
|
|
298 |
by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)}) = ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- {} Un nmsg_eq 0 (v,w)))" 2);
|
|
299 |
by (Blast_tac 2); by (Blast_tac 2);
|
|
300 |
by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R) 1);
|
|
301 |
by Auto_tac;
|
|
302 |
qed "Stable_final_E_NOT_empty";
|
|
303 |
|
|
304 |
Goal "F : Stable final";
|
|
305 |
by (case_tac "E={}" 1);
|
|
306 |
by (blast_tac (claset() addIs [Stable_final_E_NOT_empty]) 2);
|
|
307 |
by (blast_tac (claset() addIs [Stable_final_E_empty]) 1);
|
|
308 |
qed "Stable_final";
|