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