1(*---------------------------------------------------------------------------*)
2(* Depth first traversal of directed graphs that can contain cycles.         *)
3(*---------------------------------------------------------------------------*)
4 
5app load ["pred_setLib"];
6
7quietdec := true;
8open pred_setTheory pred_setLib relationTheory listTheory;
9quietdec := false;
10
11val set_ss = list_ss ++ PRED_SET_ss;
12val dnf_ss = bool_ss ++ boolSimps.DNF_ss ++ rewrites [AND_IMP_INTRO];
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 = Define `Parents G = {x | ~(G x = [])}`;
20
21(*---------------------------------------------------------------------------*)
22(* DFT :('a -> 'a list) ->   (* graph *)                                     *)
23(*      ('a -> 'b -> 'b) ->  (* folding function *)                          *)
24(*      'a list ->           (* nodes seen *)                                *)
25(*      'a list ->           (* fringe to visit *)                           *)
26(*      'b ->                (* accumulator *)                               *)
27(*      'b                   (* final result *)                              *)
28(*                                                                           *)
29(* DFT checks that the given graph has finite Parents.  If the Parents set   *)
30(* is finite then the graph has only finitely many edges (because G produces *)
31(* a list of children, a node has only finitely many children) and DFT must  *)
32(* terminate.                                                                *)
33(*                                                                           *)
34(* Termination proof. In the first recursive call, the to_visit list is      *)
35(* shorter. In the second recursive call, the seen and to_visit argument can *)
36(* both increase, but in different circumstances.  In this call, visit_now   *)
37(* has not been seen.  If it is a parent in the graph, then adding it to     *)
38(* seen decreases the number of unseen parents in the graph. If it is not a  *)
39(* parent, then it has no children, and so the to_visit list shrinks.        *)
40(*---------------------------------------------------------------------------*)
41
42val Rel_def =   (* map arg. tuples into a pair of numbers for termination *)
43 Define 
44   `Rel(G,f,seen,to_visit,acc) = 
45        (CARD(Parents G DIFF (LIST_TO_SET seen)), LENGTH to_visit)`;
46
47val def = (* Define function and prove termination *)
48 tDefine
49  "DFT" 
50  `DFT G f seen to_visit acc = 
51    if FINITE (Parents G)
52      then case to_visit
53           of [] -> acc 
54           || (visit_now :: visit_later) ->
55              if MEM visit_now seen 
56                then DFT G f seen visit_later acc 
57                else DFT G f (visit_now :: seen)
58                             (G visit_now ++ visit_later)
59                             (f visit_now acc)
60      else ARB`
61 (WF_REL_TAC `inv_image ($< LEX $<) Rel`
62   THEN RW_TAC set_ss [Rel_def, DECIDE ``(0 < p - q) = q < p ``]
63   THEN Cases_on `visit_now IN Parents G` THENL
64   [DISJ1_TAC, DISJ2_TAC] THEN RW_TAC set_ss [] THENL
65   [MATCH_MP_TAC (DECIDE ``y <= x /\ y < z ==> x < x - y + z``) THEN 
66      CONJ_TAC THENL
67      [METIS_TAC [CARD_INTER_LESS_EQ],
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 (SIMP_RULE dnf_ss [] CARD_PSUBSET) 
72       THEN RW_TAC set_ss [INTER_DEF,PSUBSET_DEF,SUBSET_DEF,EXTENSION] 
73       THEN METIS_TAC[],
74    MATCH_MP_TAC (DECIDE ``(p=q) ==> (x-p = x-q)``) 
75      THEN MATCH_MP_TAC (METIS_PROVE [] ``(s1=s2) ==> (CARD s1 = CARD s2)``) 
76      THEN RW_TAC set_ss [INTER_DEF,EXTENSION] THEN METIS_TAC [],
77    FULL_SIMP_TAC set_ss [Parents]]);
78
79
80(*---------------------------------------------------------------------------*)
81(* Desired recursion equations, constrained by finiteness of graph.          *)
82(*---------------------------------------------------------------------------*)
83
84val DFT_DEF = Q.prove
85(`FINITE (Parents G) ==> 
86  (DFT G f seen [] acc = acc) /\
87  (DFT G f seen (visit_now :: visit_later) acc =
88    if MEM visit_now seen 
89       then DFT G f seen visit_later acc
90       else DFT G f (visit_now :: seen)
91                    (G visit_now ++ visit_later)
92                    (f visit_now acc))`,
93 RW_TAC std_ss [] THENL
94 [RW_TAC list_ss [def],
95  GEN_REWRITE_TAC LHS_CONV empty_rewrites [def] THEN RW_TAC list_ss [],
96  RW_TAC list_ss [def],
97  GEN_REWRITE_TAC LHS_CONV empty_rewrites [def] THEN RW_TAC list_ss []]);
98
99
100(*---------------------------------------------------------------------------*)
101(* Desired induction theorem for DFT.                                        *)
102(*---------------------------------------------------------------------------*)
103
104val DFT_IND = Q.prove
105(`!P.
106    (!G f seen visit_now visit_later acc. 
107       P G f seen [] acc /\
108       ((FINITE (Parents G) /\ ~MEM visit_now seen ==>
109            P G f (visit_now :: seen)
110                  (G visit_now ++ visit_later)
111                  (f visit_now acc)) /\
112        (FINITE (Parents G) /\ MEM visit_now seen ==>
113            P G f seen visit_later acc)
114         ==> P G f seen (visit_now :: visit_later) acc))
115   ==>
116   !v v1 v2 v3 v4. P v v1 v2 v3 v4`,
117 NTAC 2 STRIP_TAC 
118 THEN HO_MATCH_MP_TAC (fetch "-" "DFT_ind")
119 THEN REPEAT GEN_TAC THEN Cases_on `to_visit`
120 THEN RW_TAC list_ss []);
121
122(*---------------------------------------------------------------------------*)
123(* Basic lemmas about DFT                                                    *)
124(*---------------------------------------------------------------------------*)
125
126val DFT_CONS = Q.prove
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.prove
139(`!G f seen to_visit acc. 
140    FINITE (Parents G) 
141       ==>
142   (DFT G f seen to_visit acc = FOLDR f acc (DFT G CONS seen to_visit []))`,
143 recInduct DFT_IND THEN 
144 RW_TAC list_ss [DFT_DEF] THEN METIS_TAC [FOLDR_UNROLL,DFT_CONS,APPEND]);
145
146val DFT_ALL_DISTINCT_LEM = Q.prove
147(`!G f seen to_visit acc. 
148    FINITE (Parents G) /\ (f = CONS) /\
149    ALL_DISTINCT acc /\ (!x. MEM x acc ==> MEM x seen)
150      ==>
151    ALL_DISTINCT (DFT G f seen to_visit acc)`,
152 recInduct DFT_IND THEN RW_TAC list_ss [DFT_DEF] THEN METIS_TAC []);
153
154val DFT_ALL_DISTINCT = Q.prove
155(`!G seen to_visit. 
156    FINITE (Parents G) ==> ALL_DISTINCT (DFT G CONS seen to_visit [])`,
157 RW_TAC list_ss [DFT_ALL_DISTINCT_LEM]);
158
159(*---------------------------------------------------------------------------*)
160(* Definition of reachability in a graph of the kind we are using here.      *)
161(*---------------------------------------------------------------------------*)
162
163val REACH_DEF = 
164 Define 
165   `REACH G = RTC (\x y. MEM y (G x))`;
166
167val REACH_LIST_DEF = 
168 Define
169   `REACH_LIST G nodes y = ?x. MEM x nodes /\ y IN REACH G x`;
170
171(*---------------------------------------------------------------------------*)
172(* Removing a set of nodes ex from G.                                        *)
173(*---------------------------------------------------------------------------*)
174
175val EXCLUDE_DEF = 
176 Define
177   `EXCLUDE G ex node = if node IN ex then [] else G node`;
178
179(*---------------------------------------------------------------------------*)
180(* Lemmas about reachability and restricted graphs.                          *)
181(*---------------------------------------------------------------------------*)
182
183val EXCLUDE_LEM = Q.prove (
184`!G x l. EXCLUDE G (x INSERT l) = EXCLUDE (EXCLUDE G l) {x}`,
185 RW_TAC set_ss [FUN_EQ_THM,EXTENSION, EXCLUDE_DEF, IN_INSERT, NOT_IN_EMPTY]
186  THEN METIS_TAC[]);
187
188val REACH_EXCLUDE = Q.prove (
189`!G x. REACH (EXCLUDE G x) = RTC (\x' y. ~(x' IN x) /\ MEM y (G x'))`,
190 RW_TAC set_ss [REACH_DEF, EXCLUDE_DEF] THEN AP_TERM_TAC 
191  THEN RW_TAC set_ss [FUN_EQ_THM] 
192  THEN RW_TAC set_ss []);
193
194(*---------------------------------------------------------------------------*)
195(* A node is reachable from p iff it is reachable from a child of p on a     *)
196(* path not containing p.                                                    *)
197(*---------------------------------------------------------------------------*)
198
199val REACH_LEM1 = Q.prove (
200`!p G seen. 
201    ~(p IN seen) ==>
202     (REACH (EXCLUDE G seen) p =
203      p INSERT (REACH_LIST (EXCLUDE G (p INSERT seen)) (G p)))`,
204 RW_TAC set_ss [EXTENSION,SPECIFICATION,REACH_EXCLUDE,REACH_LIST_DEF] 
205  THEN Cases_on `p = x` 
206  THEN RW_TAC list_ss [RTC_RULES] THEN EQ_TAC THEN RW_TAC bool_ss [] THENL
207 [Q.PAT_ASSUM `$~a` MP_TAC THEN POP_ASSUM MP_TAC 
208   THEN Q.SPEC_TAC (`x`,`q`) THEN Q.ID_SPEC_TAC `p` 
209   THEN HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN RW_TAC bool_ss [] 
210   THEN Cases_on `p' = x'` THEN FULL_SIMP_TAC bool_ss [] THENL
211   [METIS_TAC [RTC_RULES],
212    Q.EXISTS_TAC `x''` THEN RW_TAC bool_ss [Once RTC_CASES2] THEN METIS_TAC[]],
213  `RTC (\x' y. ~seen x' /\ MEM y (G x')) x' x` by
214    (MATCH_MP_TAC (SIMP_RULE dnf_ss [] RTC_MONOTONE) 
215      THEN Q.EXISTS_TAC `\x' y. (~(x' = p) /\ ~seen x') /\ MEM y (G x')` 
216      THEN RW_TAC list_ss []) THEN
217  RW_TAC bool_ss [Once RTC_CASES1] THEN METIS_TAC []]);
218
219(*---------------------------------------------------------------------------*)
220(* If y is reachable from x, but not z, then y is reachable from x on a path *)
221(* that does not include z.                                                  *) 
222(*---------------------------------------------------------------------------*)
223
224val REACH_LEM2 = Q.prove (
225`!G x y. REACH G x y ==> !z. ~REACH G z y ==> REACH (EXCLUDE G {z}) x y`,
226 STRIP_TAC THEN REWRITE_TAC [REACH_EXCLUDE, REACH_DEF, IN_SING] THEN
227 HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN RW_TAC set_ss [RTC_RULES] THEN
228 POP_ASSUM MP_TAC THEN RW_TAC set_ss [Once RTC_CASES2] THEN
229 POP_ASSUM (MP_TAC o Q.SPEC `x'`) THEN RW_TAC set_ss [] THEN
230 RW_TAC set_ss [Once RTC_CASES2] THEN METIS_TAC [RTC_RULES]);
231
232(*---------------------------------------------------------------------------*)
233(* If DFT visits x, then x is reachable or is in the starting accumulator    *)
234(*---------------------------------------------------------------------------*)
235
236val DFT_REACH_1 = Q.prove
237(`!G f seen to_visit acc. 
238    FINITE (Parents G) /\ (f = CONS) ==>
239    !x. MEM x (DFT G f seen to_visit acc) ==>
240      x IN (REACH_LIST G to_visit) \/ MEM x acc`,
241 recInduct DFT_IND 
242   THEN RW_TAC set_ss [DFT_DEF, REACH_LIST_DEF, REACH_DEF, IN_DEF] 
243   THENL[METIS_TAC [], ALL_TAC] 
244   THEN POP_ASSUM MP_TAC THEN RW_TAC set_ss [] 
245   THEN POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN RW_TAC set_ss [] THENL
246   [IMP_RES_TAC RTC_RULES THEN METIS_TAC[], 
247    METIS_TAC[], METIS_TAC[RTC_RULES], METIS_TAC[]]);
248
249(*---------------------------------------------------------------------------*)
250(* If x is reachable from to_visit on a path that does not include the nodes *)
251(* in seen, then DFT visits x.                                               *) 
252(*---------------------------------------------------------------------------*)
253
254val DFT_REACH_2 = Q.prove
255(`!G f seen to_visit acc x. 
256    FINITE (Parents G) /\ (f = CONS) /\
257    x IN (REACH_LIST (EXCLUDE G (LIST_TO_SET seen)) to_visit) /\ 
258    ~MEM x seen 
259     ==>
260      MEM x (DFT G f seen to_visit acc)`,
261 recInduct DFT_IND THEN RW_TAC set_ss [DFT_DEF] THENL
262 [(* Base Case *)
263  FULL_SIMP_TAC list_ss [IN_DEF, EXCLUDE_DEF, REACH_LIST_DEF],
264  (* The head of to_visit is in seen *)
265  FULL_SIMP_TAC dnf_ss [SPECIFICATION, REACH_LIST_DEF]
266  THEN RW_TAC list_ss [] THEN
267  POP_ASSUM MP_TAC THEN RW_TAC list_ss [] THEN POP_ASSUM MATCH_MP_TAC THEN
268  FULL_SIMP_TAC set_ss [SPECIFICATION, REACH_LIST_DEF] THENL
269  [FULL_SIMP_TAC set_ss [REACH_EXCLUDE,Once RTC_CASES1,SPECIFICATION],ALL_TAC]
270   THEN METIS_TAC [],
271  (* The head of to_visit is not in seen *)
272  POP_ASSUM MP_TAC THEN RW_TAC set_ss [] THEN
273    POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN RW_TAC list_ss [] THEN
274    Cases_on `x = visit_now` THEN FULL_SIMP_TAC set_ss [] THEN
275    RW_TAC set_ss [] THENL
276    [RW_TAC list_ss [Q.SPECL [`G`, `CONS`, `h::seen`,
277                              `G visit_now ++ visit_later`, `visit_now::acc`,
278                              `[]`, `visit_now::acc`] DFT_CONS],
279     FIRST_ASSUM MATCH_MP_TAC THEN RW_TAC set_ss [] THEN
280       Cases_on `x IN REACH (EXCLUDE G (LIST_TO_SET seen)) visit_now` THENL
281       [POP_ASSUM MP_TAC THEN RW_TAC set_ss [REACH_LEM1] THEN 
282         FULL_SIMP_TAC set_ss [SPECIFICATION,REACH_LIST_DEF,LIST_TO_SET_THM]
283         THEN METIS_TAC [],
284        FULL_SIMP_TAC set_ss [SPECIFICATION, REACH_LIST_DEF,LIST_TO_SET_THM] 
285        THENL [METIS_TAC [], METIS_TAC [REACH_LEM2, EXCLUDE_LEM]]]]]);
286
287(*---------------------------------------------------------------------------*)
288(* x is reachable iff DFT finds it.                                          *)
289(*---------------------------------------------------------------------------*)
290
291val DFT_REACH_THM = Q.prove 
292(`!G to_visit. 
293    FINITE (Parents G) 
294      ==> 
295    !x. x IN REACH_LIST G to_visit = MEM x (DFT G CONS [] to_visit [])`,
296 REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL
297 [MATCH_MP_TAC DFT_REACH_2, IMP_RES_TAC DFT_REACH_1] THEN 
298  FULL_SIMP_TAC set_ss [REACH_DEF,REACH_EXCLUDE,SPECIFICATION,REACH_LIST_DEF]
299  THEN METIS_TAC [MEM]);
300