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