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     dirGraphTheory;
8
9val set_ss = list_ss ++ PRED_SET_ss;
10val dnf_ss = bool_ss ++ boolSimps.DNF_ss ++ rewrites [AND_IMP_INTRO];
11
12val _ = numLib.prefer_num();
13
14val _ = new_theory "dft";
15
16(*---------------------------------------------------------------------------*)
17(* DFT :('a -> 'a list) ->   (* graph *)                                     *)
18(*      ('a -> 'b -> 'b) ->  (* folding function *)                          *)
19(*      'a list ->           (* nodes seen *)                                *)
20(*      'a list ->           (* fringe to visit *)                           *)
21(*      'b ->                (* accumulator *)                               *)
22(*      'b                   (* final result *)                              *)
23(*                                                                           *)
24(* DFT checks that the given graph has finite Parents.  If the Parents set   *)
25(* is finite then the graph has only finitely many edges (because G produces *)
26(* a list of children, a node has only finitely many children) and DFT must  *)
27(* terminate.                                                                *)
28(*                                                                           *)
29(* Termination proof. In the first recursive call, the to_visit list is      *)
30(* shorter. In the second recursive call, the seen and to_visit argument can *)
31(* both increase, but in different circumstances.  In this call, visit_now   *)
32(* has not been seen.  If it is a parent in the graph, then adding it to     *)
33(* seen decreases the number of unseen parents in the graph. If it is not a  *)
34(* parent, then it has no children, and so the to_visit list shrinks.        *)
35(*---------------------------------------------------------------------------*)
36
37val Rel_def =   (* map arg. tuples into a pair of numbers for termination *)
38 Define
39   `Rel(G,f,seen,to_visit,acc) =
40        (CARD(Parents G DIFF (LIST_TO_SET seen)), LENGTH to_visit)`;
41
42val () = computeLib.auto_import_definitions := false
43
44val def = (* Define function and prove termination *)
45 tDefine
46  "DFT"
47  `DFT G f seen to_visit acc =
48    if FINITE (Parents G)
49      then case to_visit
50           of [] => acc
51           | visit_now :: visit_later =>
52              if MEM visit_now seen
53                then DFT G f seen visit_later acc
54                else DFT G f (visit_now :: seen)
55                             (G visit_now ++ visit_later)
56                             (f visit_now acc)
57      else ARB`
58 (WF_REL_TAC `inv_image ($< LEX $<) Rel`
59   THEN RW_TAC set_ss [Rel_def, DECIDE ``(0 < p - q) = q < p ``]
60   THEN Cases_on `visit_now IN Parents G` THENL
61   [DISJ1_TAC, DISJ2_TAC] THEN RW_TAC set_ss [] THENL
62   [MATCH_MP_TAC (DECIDE ``y <= x /\ y < z ==> x < z + (x - y)``) THEN
63     CONJ_TAC THENL
64      [METIS_TAC [CARD_INTER_LESS_EQ],
65       MATCH_MP_TAC (SIMP_RULE dnf_ss [] CARD_PSUBSET)
66         THEN RW_TAC set_ss [INTER_DEF,PSUBSET_DEF,SUBSET_DEF,EXTENSION]
67         THEN METIS_TAC[]],
68    MATCH_MP_TAC (SIMP_RULE dnf_ss [] CARD_PSUBSET)
69       THEN RW_TAC set_ss [INTER_DEF,PSUBSET_DEF,SUBSET_DEF,EXTENSION]
70       THEN METIS_TAC[],
71    MATCH_MP_TAC (DECIDE ``(p=q) ==> (x-p = x-q)``)
72      THEN MATCH_MP_TAC (METIS_PROVE [] ``(s1=s2) ==> (CARD s1 = CARD s2)``)
73      THEN RW_TAC set_ss [INTER_DEF,EXTENSION] THEN METIS_TAC [],
74    FULL_SIMP_TAC set_ss [Parents_def]]);
75
76
77(*---------------------------------------------------------------------------*)
78(* Desired recursion equations, constrained by finiteness of graph.          *)
79(*---------------------------------------------------------------------------*)
80
81val DFT_def = Q.store_thm
82("DFT_def",
83 `FINITE (Parents G) ==>
84  (DFT G f seen [] acc = acc) /\
85  (DFT G f seen (visit_now :: visit_later) acc =
86    if MEM visit_now seen
87       then DFT G f seen visit_later acc
88       else DFT G f (visit_now :: seen)
89                    (G visit_now ++ visit_later)
90                    (f visit_now acc))`,
91 RW_TAC std_ss [] THENL
92 [RW_TAC list_ss [def],
93  GEN_REWRITE_TAC LHS_CONV empty_rewrites [def] THEN RW_TAC list_ss [],
94  RW_TAC list_ss [def],
95  GEN_REWRITE_TAC LHS_CONV empty_rewrites [def] THEN RW_TAC list_ss []]);
96
97
98(*---------------------------------------------------------------------------*)
99(* Desired induction theorem for DFT.                                        *)
100(*---------------------------------------------------------------------------*)
101
102val DFT_ind = Q.store_thm
103("DFT_ind",
104 `!P.
105    (!G f seen visit_now visit_later acc.
106       P G f seen [] acc /\
107       ((FINITE (Parents G) /\ ~MEM visit_now seen ==>
108            P G f (visit_now :: seen)
109                  (G visit_now ++ visit_later)
110                  (f visit_now acc)) /\
111        (FINITE (Parents G) /\ MEM visit_now seen ==>
112            P G f seen visit_later acc)
113         ==> P G f seen (visit_now :: visit_later) acc))
114   ==>
115   !v v1 v2 v3 v4. P v v1 v2 v3 v4`,
116 NTAC 2 STRIP_TAC
117 THEN HO_MATCH_MP_TAC (fetch "-" "DFT_ind")
118 THEN REPEAT GEN_TAC THEN Cases_on `to_visit`
119 THEN RW_TAC list_ss []);
120
121(*---------------------------------------------------------------------------*)
122(* Basic lemmas about DFT                                                    *)
123(*---------------------------------------------------------------------------*)
124
125val DFT_CONS = Q.store_thm
126("DFT_CONS",
127 `!G f seen to_visit acc a b.
128    FINITE (Parents G) /\ (f = CONS) /\ (acc = APPEND a b)
129      ==>
130    (DFT G f seen to_visit acc = DFT G f seen to_visit a ++ b)`,
131 recInduct DFT_ind
132  THEN RW_TAC list_ss [DFT_def] THEN METIS_TAC [APPEND]);
133
134val FOLDR_UNROLL = Q.prove
135(`!f x b l. FOLDR f (f x b) l = FOLDR f b (l ++ [x])`,
136 Induct_on `l` THEN RW_TAC list_ss []);
137
138val DFT_FOLD = Q.store_thm
139("DFT_FOLD",
140 `!G f seen to_visit acc.
141    FINITE (Parents G)
142       ==>
143   (DFT G f seen to_visit acc = FOLDR f acc (DFT G CONS seen to_visit []))`,
144 recInduct DFT_ind THEN
145 RW_TAC list_ss [DFT_def] THEN METIS_TAC [FOLDR_UNROLL,DFT_CONS,APPEND]);
146
147val DFT_ALL_DISTINCT_LEM = Q.prove
148(`!G f seen to_visit acc.
149    FINITE (Parents G) /\ (f = CONS) /\
150    ALL_DISTINCT acc /\ (!x. MEM x acc ==> MEM x seen)
151      ==>
152    ALL_DISTINCT (DFT G f seen to_visit acc)`,
153 recInduct DFT_ind THEN RW_TAC list_ss [DFT_def] THEN METIS_TAC []);
154
155val DFT_ALL_DISTINCT = Q.store_thm
156("DFT_ALL_DISTINCT",
157 `!G seen to_visit.
158    FINITE (Parents G) ==> ALL_DISTINCT (DFT G CONS seen to_visit [])`,
159 RW_TAC list_ss [DFT_ALL_DISTINCT_LEM]);
160
161(*---------------------------------------------------------------------------*)
162(* If DFT visits x, then x is reachable or is in the starting accumulator    *)
163(*---------------------------------------------------------------------------*)
164
165val DFT_REACH_1 = Q.store_thm
166("DFT_REACH_1",
167 `!G f seen to_visit acc.
168    FINITE (Parents G) /\ (f = CONS) ==>
169    !x. MEM x (DFT G f seen to_visit acc) ==>
170      x IN (REACH_LIST G to_visit) \/ MEM x acc`,
171 recInduct DFT_ind
172   THEN RW_TAC set_ss [DFT_def, REACH_LIST_def, REACH_def, IN_DEF]
173   THENL[METIS_TAC [], ALL_TAC]
174   THEN POP_ASSUM MP_TAC THEN RW_TAC set_ss []
175   THEN POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN RW_TAC set_ss [] THENL
176   [IMP_RES_TAC RTC_RULES THEN METIS_TAC[],
177    METIS_TAC[], METIS_TAC[RTC_RULES], METIS_TAC[]]);
178
179(*---------------------------------------------------------------------------*)
180(* If x is reachable from to_visit on a path that does not include the nodes *)
181(* in seen, then DFT visits x.                                               *)
182(*---------------------------------------------------------------------------*)
183
184val DFT_REACH_2 = Q.store_thm
185("DFT_REACH_2",
186 `!G f seen to_visit acc x.
187    FINITE (Parents G) /\ (f = CONS) /\
188    x IN (REACH_LIST (EXCLUDE G (LIST_TO_SET seen)) to_visit) /\
189    ~MEM x seen
190     ==>
191      MEM x (DFT G f seen to_visit acc)`,
192 recInduct DFT_ind THEN RW_TAC set_ss [DFT_def] THENL
193 [(* Base Case *)
194  FULL_SIMP_TAC list_ss [IN_DEF, EXCLUDE_def, REACH_LIST_def],
195  (* The head of to_visit is in seen *)
196  FULL_SIMP_TAC dnf_ss [SPECIFICATION, REACH_LIST_def]
197  THEN RW_TAC list_ss [] THEN
198  POP_ASSUM MP_TAC THEN RW_TAC list_ss [] THEN POP_ASSUM MATCH_MP_TAC THEN
199  FULL_SIMP_TAC set_ss [SPECIFICATION, REACH_LIST_def] THENL
200  [FULL_SIMP_TAC set_ss [REACH_EXCLUDE,Once RTC_CASES1,SPECIFICATION],ALL_TAC]
201   THEN METIS_TAC [],
202  (* The head of to_visit is not in seen *)
203  POP_ASSUM MP_TAC THEN RW_TAC set_ss [] THEN
204    POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN RW_TAC list_ss [] THEN
205    Cases_on `x = visit_now` THEN FULL_SIMP_TAC set_ss [] THEN
206    RW_TAC set_ss [] THENL
207    [RW_TAC list_ss [Q.SPECL [`G`, `CONS`, `h::seen`,
208                              `G visit_now ++ visit_later`, `visit_now::acc`,
209                              `[]`, `visit_now::acc`] DFT_CONS],
210     FIRST_ASSUM MATCH_MP_TAC THEN RW_TAC set_ss [] THEN
211       Cases_on `x IN REACH (EXCLUDE G (LIST_TO_SET seen)) visit_now` THENL
212       [POP_ASSUM MP_TAC THEN RW_TAC set_ss [REACH_LEM1] THEN
213         FULL_SIMP_TAC set_ss [SPECIFICATION,REACH_LIST_def,LIST_TO_SET_THM]
214         THEN METIS_TAC [],
215        FULL_SIMP_TAC set_ss [SPECIFICATION, REACH_LIST_def,LIST_TO_SET_THM]
216        THENL [METIS_TAC [], METIS_TAC [REACH_LEM2, EXCLUDE_LEM]]]]]);
217
218(*---------------------------------------------------------------------------*)
219(* x is reachable iff DFT finds it.                                          *)
220(*---------------------------------------------------------------------------*)
221
222val DFT_REACH_THM = Q.store_thm
223("DFT_REACH_THM",
224 `!G to_visit.
225    FINITE (Parents G)
226      ==>
227    !x. x IN REACH_LIST G to_visit = MEM x (DFT G CONS [] to_visit [])`,
228 RW_TAC bool_ss [EQ_IMP_THM] THENL
229 [MATCH_MP_TAC DFT_REACH_2,IMP_RES_TAC DFT_REACH_1] THEN
230 FULL_SIMP_TAC set_ss [REACH_def,REACH_EXCLUDE,SPECIFICATION,REACH_LIST_def] THEN
231 METIS_TAC[LIST_TO_SET_DEF]);
232
233val _ = export_theory();
234