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