equal
deleted
inserted
replaced
6 Reachability in Graphs |
6 Reachability in Graphs |
7 |
7 |
8 From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3 |
8 From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3 |
9 *) |
9 *) |
10 |
10 |
11 theory Reachability imports Detects Reach begin |
11 theory Reachability imports "../Detects" Reach begin |
12 |
12 |
13 types edge = "(vertex*vertex)" |
13 types edge = "(vertex*vertex)" |
14 |
14 |
15 record state = |
15 record state = |
16 reach :: "vertex => bool" |
16 reach :: "vertex => bool" |
344 apply safe |
344 apply safe |
345 apply (rule Stable_eq) |
345 apply (rule Stable_eq) |
346 apply (subgoal_tac [2] |
346 apply (subgoal_tac [2] |
347 "({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> nmsg_eq 0 (v,w)) = |
348 ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))") |
348 ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))") |
349 prefer 2 apply blast |
349 prefer 2 apply simp |
350 prefer 2 apply blast |
350 prefer 2 apply blast |
351 apply (rule Stable_reachable_EQ_R_AND_nmsg_0 |
351 apply (rule Stable_reachable_EQ_R_AND_nmsg_0 |
352 [simplified Eq_lemma2 Collect_const]) |
352 [simplified Eq_lemma2 Collect_const]) |
353 apply (blast, blast) |
353 apply (blast, blast) |
354 apply (rule Stable_eq) |
354 apply (rule Stable_eq) |