1(*  Title:      HOL/UNITY/Simple/Reachability.thy
2    Author:     Tanja Vos, Cambridge University Computer Laboratory
3    Copyright   2000  University of Cambridge
4
5Reachability in Graphs.
6
7From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2
8and 11.3.
9*)
10
11theory Reachability imports "../Detects" Reach begin
12
13type_synonym edge = "vertex * vertex"
14
15record state =
16  reach :: "vertex => bool"
17  nmsg  :: "edge => nat"
18
19consts root :: "vertex"
20       E :: "edge set"
21       V :: "vertex set"
22
23inductive_set REACHABLE :: "edge set"
24  where
25    base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
26  | step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
27
28definition reachable :: "vertex => state set" where
29  "reachable p == {s. reach s p}"
30
31definition nmsg_eq :: "nat => edge  => state set" where
32  "nmsg_eq k == %e. {s. nmsg s e = k}"
33
34definition nmsg_gt :: "nat => edge  => state set" where
35  "nmsg_gt k  == %e. {s. k < nmsg s e}"
36
37definition nmsg_gte :: "nat => edge => state set" where
38  "nmsg_gte k == %e. {s. k \<le> nmsg s e}"
39
40definition nmsg_lte  :: "nat => edge => state set" where
41  "nmsg_lte k  == %e. {s. nmsg s e \<le> k}"
42
43definition final :: "state set" where
44  "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter> 
45            (INTER E (nmsg_eq 0))"
46
47axiomatization
48where
49    Graph1: "root \<in> V" and
50
51    Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)" and
52
53    MA1:  "F \<in> Always (reachable root)" and
54
55    MA2:  "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})" and
56
57    MA3:  "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))" and
58
59    MA4:  "(v,w) \<in> E ==> 
60           F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))" and
61
62    MA5:  "[|v \<in> V; w \<in> V|] 
63           ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))" and
64
65    MA6:  "[|v \<in> V|] ==> F \<in> Stable (reachable v)" and
66
67    MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))" and
68
69    MA7:  "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
70
71
72lemmas E_imp_in_V_L = Graph2 [THEN conjunct1]
73lemmas E_imp_in_V_R = Graph2 [THEN conjunct2]
74
75lemma lemma2:
76     "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v"
77apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L])
78apply (rule_tac [3] MA6)
79apply (auto simp add: E_imp_in_V_L E_imp_in_V_R)
80done
81
82lemma Induction_base: "(v,w) \<in> E ==> F \<in> reachable v LeadsTo reachable w"
83apply (rule MA4 [THEN Always_LeadsTo_weaken])
84apply (rule_tac [2] lemma2)
85apply (auto simp add: nmsg_eq_def nmsg_gt_def)
86done
87
88lemma REACHABLE_LeadsTo_reachable:
89     "(v,w) \<in> REACHABLE ==> F \<in> reachable v LeadsTo reachable w"
90apply (erule REACHABLE.induct)
91apply (rule subset_imp_LeadsTo, blast)
92apply (blast intro: LeadsTo_Trans Induction_base)
93done
94
95lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v"
96apply (rule single_LeadsTo_I)
97apply (simp split: if_split_asm)
98apply (rule MA1 [THEN Always_LeadsToI])
99apply (erule REACHABLE_LeadsTo_reachable [THEN LeadsTo_weaken_L], auto)
100done
101
102
103lemma Reachability_Detected: 
104     "v \<in> V ==> F \<in> (reachable v) Detects {s. (root,v) \<in> REACHABLE}"
105apply (unfold Detects_def, auto)
106 prefer 2 apply (blast intro: MA2 [THEN Always_weaken])
107apply (rule Detects_part1 [THEN LeadsTo_weaken_L], blast)
108done
109
110
111lemma LeadsTo_Reachability:
112     "v \<in> V ==> F \<in> UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE})"
113by (erule Reachability_Detected [THEN Detects_Imp_LeadstoEQ])
114
115
116(* ------------------------------------ *)
117
118(* Some lemmas about <==> *)
119
120lemma Eq_lemma1: 
121     "(reachable v <==> {s. (root,v) \<in> REACHABLE}) =  
122      {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
123by (unfold Equality_def, blast)
124
125
126lemma Eq_lemma2: 
127     "(reachable v <==> (if (root,v) \<in> REACHABLE then UNIV else {})) =  
128      {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
129by (unfold Equality_def, auto)
130
131(* ------------------------------------ *)
132
133
134(* Some lemmas about final (I don't need all of them!)  *)
135
136lemma final_lemma1: 
137     "(\<Inter>v \<in> V. \<Inter>w \<in> V. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE)) &  
138                              s \<in> nmsg_eq 0 (v,w)})  
139      \<subseteq> final"
140apply (unfold final_def Equality_def, auto)
141apply (frule E_imp_in_V_R)
142apply (frule E_imp_in_V_L, blast)
143done
144
145lemma final_lemma2: 
146 "E\<noteq>{}  
147  ==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}  
148                           \<inter> nmsg_eq 0 e)    \<subseteq>  final"
149apply (unfold final_def Equality_def)
150apply (auto split!: if_split)
151apply (frule E_imp_in_V_L, blast)
152done
153
154lemma final_lemma3:
155     "E\<noteq>{}  
156      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
157           (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)  
158          \<subseteq> final"
159apply (frule final_lemma2)
160apply (simp (no_asm_use) add: Eq_lemma2)
161done
162
163
164lemma final_lemma4:
165     "E\<noteq>{}  
166      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
167           {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))} \<inter> nmsg_eq 0 e)  
168          = final"
169apply (rule subset_antisym)
170apply (erule final_lemma2)
171apply (unfold final_def Equality_def, blast)
172done
173
174lemma final_lemma5:
175     "E\<noteq>{}  
176      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
177           ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)  
178          = final"
179apply (frule final_lemma4)
180apply (simp (no_asm_use) add: Eq_lemma2)
181done
182
183
184lemma final_lemma6:
185     "(\<Inter>v \<in> V. \<Inter>w \<in> V.  
186       (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 (v,w))  
187      \<subseteq> final"
188apply (simp (no_asm) add: Eq_lemma2 Int_def)
189apply (rule final_lemma1)
190done
191
192
193lemma final_lemma7: 
194     "final =  
195      (\<Inter>v \<in> V. \<Inter>w \<in> V.  
196       ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
197       (-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))"
198apply (unfold final_def)
199apply (rule subset_antisym, blast)
200apply (auto split: if_split_asm)
201apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+
202done
203
204(* ------------------------------------ *)
205
206
207(* ------------------------------------ *)
208
209(* Stability theorems *)
210lemma not_REACHABLE_imp_Stable_not_reachable:
211     "[| v \<in> V; (root,v) \<notin> REACHABLE |] ==> F \<in> Stable (- reachable v)"
212apply (drule MA2 [THEN AlwaysD], auto)
213done
214
215lemma Stable_reachable_EQ_R:
216     "v \<in> V ==> F \<in> Stable (reachable v <==> {s. (root,v) \<in> REACHABLE})"
217apply (simp (no_asm) add: Equality_def Eq_lemma2)
218apply (blast intro: MA6 not_REACHABLE_imp_Stable_not_reachable)
219done
220
221
222lemma lemma4: 
223     "((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter> 
224       (- nmsg_gt 0 (v,w) \<union> A))  
225      \<subseteq> A \<union> nmsg_eq 0 (v,w)"
226apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
227done
228
229
230lemma lemma5: 
231     "reachable v \<inter> nmsg_eq 0 (v,w) =  
232      ((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter> 
233       (reachable v \<inter> nmsg_lte 0 (v,w)))"
234by (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
235
236lemma lemma6: 
237     "- nmsg_gt 0 (v,w) \<union> reachable v \<subseteq> nmsg_eq 0 (v,w) \<union> reachable v"
238apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
239done
240
241lemma Always_reachable_OR_nmsg_0:
242     "[|v \<in> V; w \<in> V|] ==> F \<in> Always (reachable v \<union> nmsg_eq 0 (v,w))"
243apply (rule Always_Int_I [OF MA5 MA3, THEN Always_weaken])
244apply (rule_tac [5] lemma4, auto)
245done
246
247lemma Stable_reachable_AND_nmsg_0:
248     "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (reachable v \<inter> nmsg_eq 0 (v,w))"
249apply (subst lemma5)
250apply (blast intro: MA5 Always_imp_Stable [THEN Stable_Int] MA6b)
251done
252
253lemma Stable_nmsg_0_OR_reachable:
254     "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (nmsg_eq 0 (v,w) \<union> reachable v)"
255by (blast intro!: Always_weaken [THEN Always_imp_Stable] lemma6 MA3)
256
257lemma not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0:
258     "[| v \<in> V; w \<in> V; (root,v) \<notin> REACHABLE |]  
259      ==> F \<in> Stable (- reachable v \<inter> nmsg_eq 0 (v,w))"
260apply (rule Stable_Int [OF MA2 [THEN Always_imp_Stable] 
261                           Stable_nmsg_0_OR_reachable, 
262            THEN Stable_eq])
263   prefer 4 apply blast
264apply auto
265done
266
267lemma Stable_reachable_EQ_R_AND_nmsg_0:
268     "[| v \<in> V; w \<in> V |]  
269      ==> F \<in> Stable ((reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
270                      nmsg_eq 0 (v,w))"
271by (simp add: Equality_def Eq_lemma2  Stable_reachable_AND_nmsg_0
272              not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0)
273
274
275
276(* ------------------------------------ *)
277
278
279(* LeadsTo final predicate (Exercise 11.2 page 274) *)
280
281lemma UNIV_lemma: "UNIV \<subseteq> (\<Inter>v \<in> V. UNIV)"
282by blast
283
284lemmas UNIV_LeadsTo_completion = 
285    LeadsTo_weaken_L [OF Finite_stable_completion UNIV_lemma]
286
287lemma LeadsTo_final_E_empty: "E={} ==> F \<in> UNIV LeadsTo final"
288apply (unfold final_def, simp)
289apply (rule UNIV_LeadsTo_completion)
290  apply safe
291 apply (erule LeadsTo_Reachability [simplified])
292apply (drule Stable_reachable_EQ_R, simp)
293done
294
295
296lemma Leadsto_reachability_AND_nmsg_0:
297     "[| v \<in> V; w \<in> V |]  
298      ==> F \<in> UNIV LeadsTo  
299             ((reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 (v,w))"
300apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast)
301apply (subgoal_tac
302         "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
303              UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
304              nmsg_eq 0 (v,w) ")
305apply simp
306apply (rule PSP_Stable2)
307apply (rule MA7)
308apply (rule_tac [3] Stable_reachable_EQ_R, auto)
309done
310
311lemma LeadsTo_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> UNIV LeadsTo final"
312apply (rule LeadsTo_weaken_L [OF LeadsTo_weaken_R UNIV_lemma])
313apply (rule_tac [2] final_lemma6)
314apply (rule Finite_stable_completion)
315  apply blast
316 apply (rule UNIV_LeadsTo_completion)
317   apply (blast intro: Stable_INT Stable_reachable_EQ_R_AND_nmsg_0
318                    Leadsto_reachability_AND_nmsg_0)+
319done
320
321lemma LeadsTo_final: "F \<in> UNIV LeadsTo final"
322apply (cases "E={}")
323 apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
324apply (rule LeadsTo_final_E_empty, auto)
325done
326
327(* ------------------------------------ *)
328
329(* Stability of final (Exercise 11.2 page 274) *)
330
331lemma Stable_final_E_empty: "E={} ==> F \<in> Stable final"
332apply (unfold final_def, simp)
333apply (rule Stable_INT)
334apply (drule Stable_reachable_EQ_R, simp)
335done
336
337
338lemma Stable_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> Stable final"
339apply (subst final_lemma7)
340apply (rule Stable_INT)
341apply (rule Stable_INT)
342apply (simp (no_asm) add: Eq_lemma2)
343apply safe
344apply (rule Stable_eq)
345apply (subgoal_tac [2]
346     "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) = 
347      ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
348prefer 2 apply blast
349prefer 2 apply blast 
350apply (rule Stable_reachable_EQ_R_AND_nmsg_0
351            [simplified Eq_lemma2 Collect_const])
352apply (blast, blast)
353apply (rule Stable_eq)
354 apply (rule Stable_reachable_EQ_R [simplified Eq_lemma2 Collect_const])
355 apply simp
356apply (subgoal_tac 
357        "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) }) = 
358         ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter>
359              (- {} \<union> nmsg_eq 0 (v,w)))")
360apply blast+
361done
362
363lemma Stable_final: "F \<in> Stable final"
364apply (cases "E={}")
365 prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
366apply (blast intro: Stable_final_E_empty)
367done
368
369end
370
371