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 8val set_ss = list_ss ++ PRED_SET_ss; 9 10val _ = numLib.prefer_num(); 11 12val _ = new_theory "dirGraph"; 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_def = 20 Define 21 `Parents G = {x | ~(G x = [])}`; 22 23(*---------------------------------------------------------------------------*) 24(* Definition of reachability in a directed graph represented as a function *) 25(* from nodes to a finite number of children, i.e., of type 'a -> 'a list *) 26(*---------------------------------------------------------------------------*) 27 28val REACH_def = 29 Define 30 `REACH G = RTC (\x y. MEM y (G x))`; 31 32val REACH_LIST_def = 33 Define 34 `REACH_LIST G nodes y = ?x. MEM x nodes /\ y IN REACH G x`; 35 36(*---------------------------------------------------------------------------*) 37(* Removing a set of nodes ex from G. *) 38(*---------------------------------------------------------------------------*) 39 40val EXCLUDE_def = 41 Define 42 `EXCLUDE G ex node = if node IN ex then [] else G node`; 43 44(*---------------------------------------------------------------------------*) 45(* Lemmas about reachability and restricted graphs. *) 46(*---------------------------------------------------------------------------*) 47 48val EXCLUDE_LEM = Q.store_thm 49("EXCLUDE_LEM", 50 `!G x l. EXCLUDE G (x INSERT l) = EXCLUDE (EXCLUDE G l) {x}`, 51 RW_TAC set_ss [FUN_EQ_THM,EXTENSION, EXCLUDE_def, IN_INSERT, NOT_IN_EMPTY] 52 THEN METIS_TAC[]); 53 54val REACH_EXCLUDE = Q.store_thm 55("REACH_EXCLUDE", 56`!G x. REACH (EXCLUDE G x) = RTC (\x' y. ~(x' IN x) /\ MEM y (G x'))`, 57 RW_TAC set_ss [REACH_def, EXCLUDE_def] THEN AP_TERM_TAC 58 THEN RW_TAC set_ss [FUN_EQ_THM] 59 THEN RW_TAC set_ss []); 60 61(*---------------------------------------------------------------------------*) 62(* A node is reachable from p iff it is reachable from a child of p on a *) 63(* path not containing p. *) 64(*---------------------------------------------------------------------------*) 65 66val REACH_LEM1 = Q.store_thm 67("REACH_LEM1", 68`!p G seen. 69 ~(p IN seen) ==> 70 (REACH (EXCLUDE G seen) p = 71 p INSERT (REACH_LIST (EXCLUDE G (p INSERT seen)) (G p)))`, 72 RW_TAC set_ss [EXTENSION,SPECIFICATION,REACH_EXCLUDE,REACH_LIST_def] 73 THEN Cases_on `p = x` 74 THEN RW_TAC list_ss [RTC_RULES] THEN EQ_TAC THEN RW_TAC bool_ss [] THENL 75 [Q.PAT_ASSUM `$~a` MP_TAC THEN POP_ASSUM MP_TAC 76 THEN Q.SPEC_TAC (`x`,`q`) THEN Q.ID_SPEC_TAC `p` 77 THEN HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN RW_TAC bool_ss [] 78 THEN Cases_on `p' = x'` THEN FULL_SIMP_TAC bool_ss [] THENL 79 [METIS_TAC [RTC_RULES], 80 Q.EXISTS_TAC `x''` THEN RW_TAC bool_ss [Once RTC_CASES2] THEN METIS_TAC[]], 81 `RTC (\x' y. ~seen x' /\ set (G x') y) x' x` 82 by (POP_ASSUM MP_TAC THEN MATCH_MP_TAC RTC_MONOTONE THEN METIS_TAC[]) 83 THEN RW_TAC bool_ss [Once RTC_CASES1] THEN METIS_TAC []]); 84 85(*---------------------------------------------------------------------------*) 86(* If y is reachable from x, but not z, then y is reachable from x on a path *) 87(* that does not include z. *) 88(*---------------------------------------------------------------------------*) 89 90val REACH_LEM2 = Q.store_thm 91("REACH_LEM2", 92 `!G x y. REACH G x y ==> !z. ~REACH G z y ==> REACH (EXCLUDE G {z}) x y`, 93 STRIP_TAC THEN REWRITE_TAC [REACH_EXCLUDE, REACH_def, IN_SING] THEN 94 HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN RW_TAC set_ss [RTC_RULES] THEN 95 POP_ASSUM MP_TAC THEN RW_TAC set_ss [Once RTC_CASES2] THEN 96 POP_ASSUM (MP_TAC o Q.SPEC `x'`) THEN RW_TAC set_ss [] THEN 97 RW_TAC set_ss [Once RTC_CASES2] THEN METIS_TAC [RTC_RULES]); 98 99val _ = export_theory();