dftScript.sml
1(*---------------------------------------------------------------------------*)
2(* Depth first traversal of directed graphs that can contain cycles. *)
3(*---------------------------------------------------------------------------*)
4Theory dft
5Ancestors
6 pred_set relation list dirGraph
7Libs
8 pred_setLib
9
10
11val set_ss = list_ss ++ PRED_SET_ss;
12val dnf_ss = bool_ss ++ boolSimps.DNF_ss ++ rewrites [AND_IMP_INTRO];
13
14val _ = numLib.temp_prefer_num();
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
37Definition Rel_def:
38 (* map arg. tuples into a pair of numbers for termination *)
39 Rel(G,f,seen,to_visit,acc) =
40 (CARD(Parents G DIFF (LIST_TO_SET seen)), LENGTH to_visit)
41End
42
43Definition def[nocompute,induction=DFT_ind0]:
44 DFT G f seen to_visit acc =
45 if FINITE (Parents G)
46 then case to_visit
47 of [] => acc
48 | visit_now :: visit_later =>
49 if MEM visit_now seen
50 then DFT G f seen visit_later acc
51 else DFT G f (visit_now :: seen)
52 (G visit_now ++ visit_later)
53 (f visit_now acc)
54 else ARB
55Termination
56 WF_REL_TAC `inv_image ($< LEX $<) Rel`
57 THEN RW_TAC set_ss [Rel_def, DECIDE ``(0 < p - q) <=> q < p ``]
58 THEN Cases_on `visit_now IN Parents G` THENL
59 [DISJ1_TAC, DISJ2_TAC] THEN RW_TAC set_ss [] THENL
60 [MATCH_MP_TAC (DECIDE ``y <= x /\ y < z ==> x < z + (x - y)``) THEN
61 CONJ_TAC THENL
62 [METIS_TAC [CARD_INTER_LESS_EQ],
63 MATCH_MP_TAC (SIMP_RULE dnf_ss [] CARD_PSUBSET)
64 THEN RW_TAC set_ss [INTER_DEF,PSUBSET_DEF,SUBSET_DEF,EXTENSION]
65 THEN METIS_TAC[]],
66 MATCH_MP_TAC (SIMP_RULE dnf_ss [] CARD_PSUBSET)
67 THEN RW_TAC set_ss [INTER_DEF,PSUBSET_DEF,SUBSET_DEF,EXTENSION]
68 THEN METIS_TAC[],
69 MATCH_MP_TAC (DECIDE ``(p=q) ==> (x-p = x-q)``)
70 THEN MATCH_MP_TAC (METIS_PROVE [] ``(s1=s2) ==> (CARD s1 = CARD s2)``)
71 THEN RW_TAC set_ss [INTER_DEF,EXTENSION] THEN METIS_TAC [],
72 FULL_SIMP_TAC set_ss [Parents_def]]
73End
74
75
76(*---------------------------------------------------------------------------*)
77(* Desired recursion equations, constrained by finiteness of graph. *)
78(*---------------------------------------------------------------------------*)
79
80Theorem DFT_def:
81 FINITE (Parents G) ==>
82 (DFT G f seen [] acc = acc) /\
83 (DFT G f seen (visit_now :: visit_later) acc =
84 if MEM visit_now seen
85 then DFT G f seen visit_later acc
86 else DFT G f (visit_now :: seen)
87 (G visit_now ++ visit_later)
88 (f visit_now acc))
89Proof
90 RW_TAC std_ss [] THENL
91 [RW_TAC list_ss [def],
92 GEN_REWRITE_TAC LHS_CONV empty_rewrites [def] THEN RW_TAC list_ss [],
93 RW_TAC list_ss [def],
94 GEN_REWRITE_TAC LHS_CONV empty_rewrites [def] THEN RW_TAC list_ss []]
95QED
96
97
98(*---------------------------------------------------------------------------*)
99(* Desired induction theorem for DFT. *)
100(*---------------------------------------------------------------------------*)
101
102Theorem DFT_ind:
103 !P.
104 (!G f seen visit_now visit_later acc.
105 P G f seen [] acc /\
106 ((FINITE (Parents G) /\ ~MEM visit_now seen ==>
107 P G f (visit_now :: seen)
108 (G visit_now ++ visit_later)
109 (f visit_now acc)) /\
110 (FINITE (Parents G) /\ MEM visit_now seen ==>
111 P G f seen visit_later acc)
112 ==> P G f seen (visit_now :: visit_later) acc))
113 ==>
114 !v v1 v2 v3 v4. P v v1 v2 v3 v4
115Proof
116 NTAC 2 STRIP_TAC
117 THEN HO_MATCH_MP_TAC DFT_ind0
118 THEN REPEAT GEN_TAC THEN Cases_on `to_visit`
119 THEN RW_TAC list_ss []
120QED
121
122(*---------------------------------------------------------------------------*)
123(* Basic lemmas about DFT *)
124(*---------------------------------------------------------------------------*)
125
126Theorem 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)
131Proof
132 recInduct DFT_ind
133 THEN RW_TAC list_ss [DFT_def] THEN METIS_TAC [APPEND]
134QED
135
136Theorem FOLDR_UNROLL[local]:
137 !f x b l. FOLDR f (f x b) l = FOLDR f b (l ++ [x])
138Proof
139 Induct_on `l` THEN RW_TAC list_ss []
140QED
141
142Theorem DFT_FOLD:
143 !G f seen to_visit acc.
144 FINITE (Parents G)
145 ==>
146 (DFT G f seen to_visit acc = FOLDR f acc (DFT G CONS seen to_visit []))
147Proof
148 recInduct DFT_ind THEN
149 RW_TAC list_ss [DFT_def] THEN METIS_TAC [FOLDR_UNROLL,DFT_CONS,APPEND]
150QED
151
152Theorem DFT_ALL_DISTINCT_LEM[local]:
153 !G f seen to_visit acc.
154 FINITE (Parents G) /\ (f = CONS) /\
155 ALL_DISTINCT acc /\ (!x. MEM x acc ==> MEM x seen)
156 ==>
157 ALL_DISTINCT (DFT G f seen to_visit acc)
158Proof
159 recInduct DFT_ind THEN RW_TAC list_ss [DFT_def] THEN METIS_TAC []
160QED
161
162Theorem DFT_ALL_DISTINCT:
163 !G seen to_visit.
164 FINITE (Parents G) ==> ALL_DISTINCT (DFT G CONS seen to_visit [])
165Proof
166 RW_TAC list_ss [DFT_ALL_DISTINCT_LEM]
167QED
168
169(*---------------------------------------------------------------------------*)
170(* If DFT visits x, then x is reachable or is in the starting accumulator *)
171(*---------------------------------------------------------------------------*)
172
173Theorem DFT_REACH_1:
174 !G f seen to_visit acc.
175 FINITE (Parents G) /\ (f = CONS) ==>
176 !x. MEM x (DFT G f seen to_visit acc) ==>
177 x IN (REACH_LIST G to_visit) \/ MEM x acc
178Proof
179 recInduct DFT_ind
180 THEN RW_TAC set_ss [DFT_def, REACH_LIST_def, REACH_def, IN_DEF]
181 THENL[METIS_TAC [], ALL_TAC]
182 THEN POP_ASSUM MP_TAC THEN RW_TAC set_ss []
183 THEN POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN RW_TAC set_ss [] THENL
184 [IMP_RES_TAC RTC_RULES THEN METIS_TAC[],
185 METIS_TAC[], METIS_TAC[RTC_RULES], METIS_TAC[]]
186QED
187
188(*---------------------------------------------------------------------------*)
189(* If x is reachable from to_visit on a path that does not include the nodes *)
190(* in seen, then DFT visits x. *)
191(*---------------------------------------------------------------------------*)
192
193Theorem DFT_REACH_2:
194 !G f seen to_visit acc x.
195 FINITE (Parents G) /\ (f = CONS) /\
196 x IN (REACH_LIST (EXCLUDE G (LIST_TO_SET seen)) to_visit) /\
197 ~MEM x seen
198 ==>
199 MEM x (DFT G f seen to_visit acc)
200Proof
201 recInduct DFT_ind THEN RW_TAC set_ss [DFT_def] THENL
202 [(* Base Case *)
203 FULL_SIMP_TAC list_ss [IN_DEF, EXCLUDE_def, REACH_LIST_def],
204 (* The head of to_visit is in seen *)
205 FULL_SIMP_TAC dnf_ss [SPECIFICATION, REACH_LIST_def]
206 THEN RW_TAC list_ss [] THEN
207 POP_ASSUM MP_TAC THEN RW_TAC list_ss [] THEN POP_ASSUM MATCH_MP_TAC THEN
208 FULL_SIMP_TAC set_ss [SPECIFICATION, REACH_LIST_def] THENL
209 [FULL_SIMP_TAC set_ss [REACH_EXCLUDE,Once RTC_CASES1,SPECIFICATION],ALL_TAC]
210 THEN METIS_TAC [],
211 (* The head of to_visit is not in seen *)
212 POP_ASSUM MP_TAC THEN RW_TAC set_ss [] THEN
213 POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN RW_TAC list_ss [] THEN
214 Cases_on `x = visit_now` THEN FULL_SIMP_TAC set_ss [] THEN
215 RW_TAC set_ss [] THENL
216 [RW_TAC list_ss [Q.SPECL [`G`, `CONS`, `h::seen`,
217 `G visit_now ++ visit_later`, `visit_now::acc`,
218 `[]`, `visit_now::acc`] DFT_CONS],
219 FIRST_ASSUM MATCH_MP_TAC THEN RW_TAC set_ss [] THEN
220 Cases_on `x IN REACH (EXCLUDE G (LIST_TO_SET seen)) visit_now` THENL
221 [POP_ASSUM MP_TAC THEN RW_TAC set_ss [REACH_LEM1] THEN
222 FULL_SIMP_TAC set_ss [SPECIFICATION,REACH_LIST_def,LIST_TO_SET_THM]
223 THEN METIS_TAC [],
224 FULL_SIMP_TAC set_ss [SPECIFICATION, REACH_LIST_def,LIST_TO_SET_THM]
225 THENL [METIS_TAC [], METIS_TAC [REACH_LEM2, EXCLUDE_LEM]]]]]
226QED
227
228(*---------------------------------------------------------------------------*)
229(* x is reachable iff DFT finds it. *)
230(*---------------------------------------------------------------------------*)
231
232Theorem DFT_REACH_THM:
233 !G to_visit.
234 FINITE (Parents G)
235 ==>
236 !x. x IN REACH_LIST G to_visit <=> MEM x (DFT G CONS [] to_visit [])
237Proof
238 RW_TAC bool_ss [EQ_IMP_THM] THENL [
239 MATCH_MP_TAC DFT_REACH_2,
240 IMP_RES_TAC DFT_REACH_1] >>
241 FULL_SIMP_TAC set_ss [REACH_def,REACH_EXCLUDE,SPECIFICATION,REACH_LIST_def] >>
242 METIS_TAC[LIST_TO_SET_DEF]
243QED