dirGraphScript.sml
1(*---------------------------------------------------------------------------*)
2(* Depth first traversal of directed graphs that can contain cycles. *)
3(*---------------------------------------------------------------------------*)
4Theory dirGraph
5Ancestors
6 pred_set relation list
7Libs
8 pred_setLib
9
10
11val set_ss = list_ss ++ PRED_SET_ss;
12
13(*---------------------------------------------------------------------------*)
14(* A graph G is a function of type 'a -> 'a list. *)
15(* A node of G is a parent iff it has children. *)
16(*---------------------------------------------------------------------------*)
17
18Definition Parents_def:
19 Parents G = {x | ~(G x = [])}
20End
21
22(*---------------------------------------------------------------------------*)
23(* Definition of reachability in a directed graph represented as a function *)
24(* from nodes to a finite number of children, i.e., of type 'a -> 'a list *)
25(*---------------------------------------------------------------------------*)
26
27Definition REACH_def:
28 REACH G = RTC (\x y. MEM y (G x))
29End
30
31Definition REACH_LIST_def:
32 REACH_LIST G nodes y = ?x. MEM x nodes /\ y IN REACH G x
33End
34
35(*---------------------------------------------------------------------------*)
36(* Removing a set of nodes ex from G. *)
37(*---------------------------------------------------------------------------*)
38
39Definition EXCLUDE_def:
40 EXCLUDE G ex node = if node IN ex then [] else G node
41End
42
43(*---------------------------------------------------------------------------*)
44(* Lemmas about reachability and restricted graphs. *)
45(*---------------------------------------------------------------------------*)
46
47Theorem EXCLUDE_LEM:
48 !G x l. EXCLUDE G (x INSERT l) = EXCLUDE (EXCLUDE G l) {x}
49Proof
50 RW_TAC set_ss [FUN_EQ_THM,EXTENSION, EXCLUDE_def, IN_INSERT, NOT_IN_EMPTY]
51 THEN METIS_TAC[]
52QED
53
54Theorem REACH_EXCLUDE:
55 !G x. REACH (EXCLUDE G x) = RTC (\x' y. ~(x' IN x) /\ MEM y (G x'))
56Proof
57 RW_TAC set_ss [REACH_def, EXCLUDE_def] THEN AP_TERM_TAC
58 THEN RW_TAC set_ss [FUN_EQ_THM]
59 THEN RW_TAC set_ss []
60QED
61
62(*---------------------------------------------------------------------------*)
63(* A node is reachable from p iff it is reachable from a child of p on a *)
64(* path not containing p. *)
65(*---------------------------------------------------------------------------*)
66
67Theorem REACH_LEM1:
68 !p G seen.
69 ~(p IN seen) ==>
70 (REACH (EXCLUDE G seen) p =
71 p INSERT (REACH_LIST (EXCLUDE G (p INSERT seen)) (G p)))
72Proof
73 RW_TAC set_ss [EXTENSION,SPECIFICATION,REACH_EXCLUDE,REACH_LIST_def]
74 THEN Cases_on `p = x`
75 THEN RW_TAC list_ss [RTC_RULES] THEN EQ_TAC THEN RW_TAC bool_ss [] THENL
76 [Q.PAT_ASSUM `$~a` MP_TAC THEN POP_ASSUM MP_TAC
77 THEN Q.SPEC_TAC (`x`,`q`) THEN Q.ID_SPEC_TAC `p`
78 THEN HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN RW_TAC bool_ss []
79 THEN Cases_on `p' = x'` THEN FULL_SIMP_TAC bool_ss [] THENL
80 [METIS_TAC [RTC_RULES],
81 Q.EXISTS_TAC `x''` THEN RW_TAC bool_ss [Once RTC_CASES2] THEN METIS_TAC[]],
82 `RTC (\x' y. ~seen x' /\ set (G x') y) x' x`
83 by (POP_ASSUM MP_TAC THEN MATCH_MP_TAC RTC_MONOTONE THEN METIS_TAC[])
84 THEN RW_TAC bool_ss [Once RTC_CASES1] THEN METIS_TAC []]
85QED
86
87(*---------------------------------------------------------------------------*)
88(* If y is reachable from x, but not z, then y is reachable from x on a path *)
89(* that does not include z. *)
90(*---------------------------------------------------------------------------*)
91
92Theorem REACH_LEM2:
93 !G x y. REACH G x y ==> !z. ~REACH G z y ==> REACH (EXCLUDE G {z}) x y
94Proof
95 STRIP_TAC THEN REWRITE_TAC [REACH_EXCLUDE, REACH_def, IN_SING] THEN
96 HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN RW_TAC set_ss [RTC_RULES] THEN
97 POP_ASSUM MP_TAC THEN RW_TAC set_ss [Once RTC_CASES2] THEN
98 POP_ASSUM (MP_TAC o Q.SPEC `x'`) THEN RW_TAC set_ss [] THEN
99 RW_TAC set_ss [Once RTC_CASES2] THEN METIS_TAC [RTC_RULES]
100QED
101