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