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