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