1(*===========================================================================*) 2(* Unfold and it application to breadth-first search. Prompted by reading *) 3(* "The Underappreciated Unfold", by Gibbons and Jones, ICFP 1998. *) 4(* *) 5(* Konrad Slind and Scott Owens, *) 6(* School of Computing, University of Utah *) 7(* October 20, 2004 *) 8(*===========================================================================*) 9 10quietdec := true; open listTheory; quietdec := false; 11 12(*---------------------------------------------------------------------------*) 13(* Syntax fiddling so that some identifiers in the HOL theory of lists, *) 14(* which are upper-case, are spelt the same as their ML counterparts. *) 15(*---------------------------------------------------------------------------*) 16 17val _ = 18 let open listSyntax 19 in map overload_on [("null", null_tm), ("map", map_tm), 20 ("filter",filter_tm), ("flat",flat_tm)] 21 end; 22 23(*---------------------------------------------------------------------------*) 24(* Trivial lemmas, should be in listTheory already *) 25(*---------------------------------------------------------------------------*) 26 27val NULL_ELIM = Q.prove 28(`!l. null l = (l=[])`, Cases THEN RW_TAC list_ss []); 29 30val FLAT_CONS_APPEND = Q.prove 31(`!L1 L2. flat (L1 :: L2) = L1 ++ flat L2`, 32 Induct THEN RW_TAC list_ss []); 33 34val FLAT_APPEND_DISTRIB = Q.prove 35(`!L1 L2. flat (L1 ++ L2) = flat L1 ++ flat L2`, 36 Induct THEN RW_TAC list_ss []); 37 38(*---------------------------------------------------------------------------*) 39(* The underappreciated unfold, defined as a recursion schema. *) 40(*---------------------------------------------------------------------------*) 41 42val unfold_def = 43 TotalDefn.DefineSchema 44 `unfold (x:'a) = if d(x) then [] else f(x)::unfold (g x)`; 45 46(*---------------------------------------------------------------------------*) 47(* Join the schema with its induction theorem. *) 48(* *) 49(* |- WF R /\ (!x. ~d x ==> R (g x) x) ==> *) 50(* (unfold d f g x = (if d x then [] else f x::unfold d f g (g x))) /\ *) 51(* !P. (!x. (~d x ==> P (g x)) ==> P x) ==> !v. P v *) 52(*---------------------------------------------------------------------------*) 53 54val unfold_facts = REWRITE_RULE [AND_IMP_INTRO] 55 (DISCH_ALL (CONJ (SPEC_ALL unfold_def) 56 (fetch "-" "unfold_ind"))); 57 58(*---------------------------------------------------------------------------*) 59(* Type of n-ary tree to be searched. In ML the type would be defined *) 60(* *) 61(* datatype 'a tree = Node of 'a * 'a tree list *) 62(* *) 63(*---------------------------------------------------------------------------*) 64 65Hol_datatype `tree = Node of 'a => tree list`; 66 67(*---------------------------------------------------------------------------*) 68(* Destructors for trees *) 69(*---------------------------------------------------------------------------*) 70 71val root_def = Define `root (Node a tlist) = a`; 72val subtrees_def = Define `subtrees (Node a tlist) = tlist`; 73 74(*---------------------------------------------------------------------------*) 75(* Breadth-first search defined as an unfold from a list of trees. *) 76(* *) 77(* bfs : ('a -> bool) -> 'a tree list -> 'a list list *) 78(* *) 79(*---------------------------------------------------------------------------*) 80 81val bfs_def = 82 Define 83 `bfs (P:'a -> bool) x = unfold null (filter P o map root) 84 (flat o map subtrees) x`; 85 86(*---------------------------------------------------------------------------*) 87(* Instantiate unfold facts with bfs parameters *) 88(*---------------------------------------------------------------------------*) 89 90val unfold_as_bfs = 91 PART_MATCH (lhs o snd o strip_forall o fst o dest_conj o snd o dest_imp) 92 unfold_facts 93 (rhs(snd(strip_forall(concl bfs_def)))); 94 95(*---------------------------------------------------------------------------*) 96(* Derive the bfs recursion equations and induction theorem from the unfold. *) 97(* Amounts to showing that the bfs parameters cause the unfold to terminate. *) 98(* *) 99(* bfs_eqn = *) 100(* |- bfs P x = if null x then [] *) 101(* else (filter P o map root) x::bfs P ((flat o map subtrees) x) *) 102(* *) 103(* bfs_ind = *) 104(* |- !P. (!x.(~null x ==> P ((flat o map subtrees) x)) ==> P x) ==> !v. P v *) 105(*---------------------------------------------------------------------------*) 106 107val tsize_def = (* Need a bespoke termination measure *) 108 Define 109 `(tsize (Node x tlist) = 1 + ltsize tlist) /\ 110 (ltsize [] = 0) /\ 111 (ltsize (h::t) = tsize h + ltsize t)`; 112 113val subtrees_smaller = Q.prove 114(`!t. ltsize (subtrees t) < tsize t`, 115 Cases THEN RW_TAC list_ss [subtrees_def, tsize_def]); 116 117val ltsize_append = Q.prove 118(`!L1 L2. ltsize (L1 ++ L2) = ltsize L1 + ltsize L2`, 119 Induct THEN RW_TAC list_ss [tsize_def]); 120 121(*---------------------------------------------------------------------------*) 122(* Unfold-based bfs and its induction theorem (see above). *) 123(*---------------------------------------------------------------------------*) 124 125val [bfs_eqn, bfs_ind] = CONJUNCTS 126 (REWRITE_RULE [GSYM bfs_def] 127 (prove (snd(dest_imp(concl unfold_as_bfs)), 128 MATCH_MP_TAC (GEN_ALL unfold_as_bfs) 129 THEN WF_REL_TAC `measure ltsize` 130 THEN Induct THEN RW_TAC list_ss [tsize_def,ltsize_append] 131 THEN Cases_on `null x` THEN FULL_SIMP_TAC list_ss [NULL_ELIM] 132 THEN METIS_TAC [DECIDE ``a<b /\ c<d ==> a+c < b+d``, subtrees_smaller]))); 133 134(*---------------------------------------------------------------------------*) 135(* Queue-based breadth-first search *) 136(*---------------------------------------------------------------------------*) 137 138val bfsq_eqn = 139 tDefine 140 "bfsq" 141 `(bfsq [] = []) /\ 142 (bfsq (Node (x:'a) tlist::rst) = 143 if P x then x::bfsq (rst ++ tlist) 144 else bfsq (rst ++ tlist))` 145 (WF_REL_TAC `measure ltsize` THEN 146 RW_TAC list_ss [tsize_def, ltsize_append]); 147 148val bfsq_ind = fetch "-" "bfsq_ind"; 149 150(*---------------------------------------------------------------------------*) 151(* Technical lemma *) 152(*---------------------------------------------------------------------------*) 153 154val lem = Q.prove 155(`!L1 L2. 156 bfsq P (L1 ++ flat (map subtrees L2)) 157 = 158 filter P (map root L1) ++ bfsq P (flat (map subtrees L2 ++ map subtrees L1))`, 159 Induct THEN RW_TAC list_ss [] 160 THEN Q.PAT_ASSUM `$!M` (ASSUME_TAC o Q.SPEC `L2 ++ [h]`) 161 THEN FULL_SIMP_TAC list_ss [] 162 THEN RULE_ASSUM_TAC (REWRITE_RULE [GSYM APPEND_ASSOC,APPEND]) 163 THEN POP_ASSUM (SUBST_ALL_TAC o SYM) 164 THEN Cases_on `h` 165 THEN FULL_SIMP_TAC list_ss 166 [Once bfsq_eqn, root_def, subtrees_def, FLAT_APPEND_DISTRIB]); 167 168(*---------------------------------------------------------------------------*) 169(* Main inductive property of bfsq *) 170(*---------------------------------------------------------------------------*) 171 172val bfsq_lem = Q.prove 173(`!l. (filter P o map root) l ++ bfsq P ((flat o map subtrees) l) = bfsq P l`, 174 recInduct bfsq_ind 175 THEN RW_TAC list_ss [root_def,subtrees_def] 176 THENL [RW_TAC list_ss [Once bfsq_eqn],RW_TAC list_ss [Once bfsq_eqn]] 177 THEN METIS_TAC [FILTER_APPEND_DISTRIB, APPEND_ASSOC, APPEND_11,lem]); 178 179(*---------------------------------------------------------------------------*) 180(* Desired equality between the two versions of BFS. *) 181(*---------------------------------------------------------------------------*) 182 183val bfs_eq_bfsq = Q.prove 184(`!tlist:'a tree list. flat (bfs P tlist) = bfsq P tlist`, 185 recInduct bfs_ind THEN Cases THENL 186 [RW_TAC list_ss [Once bfsq_eqn, Once bfs_eqn], 187 METIS_TAC [NULL_DEF, bfs_eqn, FLAT_CONS_APPEND, bfsq_lem]]); 188