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