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