- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
3 Author: Lawrence C Paulson and Norbert Voelker
8 infix 1 THEN_MAYBE THEN_MAYBE';
12 val DEEPEN : int*int -> (int->int->tactic) -> int -> int -> tactic
14 val THEN_MAYBE : tactic * tactic -> tactic
15 val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
17 val trace_DEPTH_FIRST : bool ref
18 val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
19 val DEPTH_SOLVE : tactic -> tactic
20 val DEPTH_SOLVE_1 : tactic -> tactic
21 val ITER_DEEPEN : (thm->bool) -> (int->tactic) -> tactic
22 val THEN_ITER_DEEPEN : tactic -> (thm->bool) -> (int->tactic) -> tactic
24 val has_fewer_prems : int -> thm -> bool
25 val IF_UNSOLVED : tactic -> tactic
26 val SOLVE : tactic -> tactic
27 val DETERM_UNTIL_SOLVED: tactic -> tactic
28 val trace_BEST_FIRST : bool ref
29 val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
30 val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic
32 val trace_ASTAR : bool ref
33 val ASTAR : (thm -> bool) * (int->thm->int) -> tactic -> tactic
34 val THEN_ASTAR : tactic -> (thm->bool) * (int->thm->int) -> tactic
36 val BREADTH_FIRST : (thm -> bool) -> tactic -> tactic
37 val QUIET_BREADTH_FIRST : (thm -> bool) -> tactic -> tactic
41 (** Instantiation of heaps for best-first search **)
43 (*total ordering on theorems, allowing duplicates to be found*)
45 HeapFun (type elem = int * thm
46 val ord = Library.prod_ord Library.int_ord
47 (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
50 structure Search : SEARCH =
53 (**** Depth-first search ****)
55 val trace_DEPTH_FIRST = ref false;
57 (*Searches until "satp" reports proof tree as satisfied.
58 Suppresses duplicate solutions to minimize search space.*)
59 fun DEPTH_FIRST satp tac =
60 let val tac = tracify trace_DEPTH_FIRST tac
61 fun depth used [] = NONE
62 | depth used (q::qs) =
66 if satp st andalso not (gen_mem eq_thm (st, used))
67 then SOME(st, Seq.make
68 (fn()=> depth (st::used) (stq::qs)))
69 else depth used (tac st :: stq :: qs)
70 in traced_tac (fn st => depth [] ([Seq.single st])) end;
74 (*Predicate: Does the rule have fewer than n premises?*)
75 fun has_fewer_prems n rule = (nprems_of rule < n);
77 (*Apply a tactic if subgoals remain, else do nothing.*)
78 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
80 (*Force a tactic to solve its goal completely, otherwise fail *)
81 fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
83 (*Force repeated application of tactic until goal is solved completely *)
84 val DETERM_UNTIL_SOLVED = DETERM_UNTIL (has_fewer_prems 1);
86 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
87 as before. This ensures that tac2 is only applied to an outcome of tac1.*)
88 fun (tac1 THEN_MAYBE tac2) st =
89 (tac1 THEN COND (has_fewer_prems (nprems_of st)) all_tac tac2) st;
91 fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
93 (*Tactical to reduce the number of premises by 1.
94 If no subgoals then it must fail! *)
95 fun DEPTH_SOLVE_1 tac st = st |>
98 | n => DEPTH_FIRST (has_fewer_prems n) tac);
100 (*Uses depth-first search to solve ALL subgoals*)
101 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
105 (**** Iterative deepening with pruning ****)
107 fun has_vars (Var _) = true
108 | has_vars (Abs (_,_,t)) = has_vars t
109 | has_vars (f$t) = has_vars f orelse has_vars t
110 | has_vars _ = false;
112 (*Counting of primitive inferences is APPROXIMATE, as the step tactic
113 may perform >1 inference*)
115 (*Pruning of rigid ancestor to prevent backtracking*)
116 fun prune (new as (k', np':int, rgd', stq), qs) =
117 let fun prune_aux (qs, []) = new::qs
118 | prune_aux (qs, (k,np,rgd,q)::rqs) =
119 if np'+1 = np andalso rgd then
120 (if !trace_DEPTH_FIRST then
121 tracing ("Pruning " ^
122 string_of_int (1+length rqs) ^ " levels")
124 (*Use OLD k: zero-cost solution; see Stickel, p 365*)
125 (k, np', rgd', stq) :: qs)
126 else prune_aux ((k,np,rgd,q)::qs, rqs)
127 fun take ([], rqs) = ([], rqs)
128 | take (arg as ((k,np,rgd,stq)::qs, rqs)) =
129 if np' < np then take (qs, (k,np,rgd,stq)::rqs)
131 in prune_aux (take (qs, [])) end;
134 (*Depth-first iterative deepening search for a state that satisfies satp
135 tactic tac0 sets up the initial goal queue, while tac1 searches it.
136 The solution sequence is redundant: the cutoff heuristic makes it impossible
137 to suppress solutions arising from earlier searches, as the accumulated cost
139 fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
140 let val countr = ref 0
141 and tf = tracify trace_DEPTH_FIRST (tac1 1)
143 (*bnd = depth bound; inc = estimate of increment required next*)
144 fun depth (bnd,inc) [] =
145 (tracing (string_of_int (!countr) ^
146 " inferences so far. Searching to depth " ^
148 (*larger increments make it run slower for the hard problems*)
149 depth (bnd+inc, 10)) [(0, 1, false, qs0)]
150 | depth (bnd,inc) ((k,np,rgd,q)::qs) =
151 if k>=bnd then depth (bnd,inc) qs
153 case (countr := !countr+1;
154 if !trace_DEPTH_FIRST then
155 tracing (string_of_int np ^
156 implode (map (fn _ => "*") qs))
159 NONE => depth (bnd,inc) qs
161 if satp st (*solution!*)
162 then SOME(st, Seq.make
163 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
166 let val np' = nprems_of st
167 (*rgd' calculation assumes tactic operates on subgoal 1*)
168 val rgd' = not (has_vars (hd (prems_of st)))
169 val k' = k+np'-np+1 (*difference in # of subgoals, +1*)
171 then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
172 else if np' < np (*solved a subgoal; prune rigid ancestors*)
174 (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
175 else depth (bnd,inc) ((k', np', rgd', tf st) ::
176 (k,np,rgd,stq) :: qs)
178 in depth (0,5) [] end);
180 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
183 (*Simple iterative deepening tactical. It merely "deepens" any search tactic
184 using increment "inc" up to limit "lim". *)
185 fun DEEPEN (inc,lim) tacf m i =
187 st |> (if has_fewer_prems i st then no_tac
189 (warning "Search depth limit exceeded: giving up";
191 else (warning ("Search depth = " ^ string_of_int m);
192 tacf m i ORELSE dpn (m+inc)))
195 (*** Best-first search ***)
197 val trace_BEST_FIRST = ref false;
199 (*For creating output sequence*)
200 fun some_of_list [] = NONE
201 | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
203 (*Check for and delete duplicate proof states*)
204 fun deleteAllMin prf heap =
205 if ThmHeap.is_empty heap then heap
206 else if eq_thm (prf, #2 (ThmHeap.min heap))
207 then deleteAllMin prf (ThmHeap.delete_min heap)
210 (*Best-first search for a state that satisfies satp (incl initial state)
211 Function sizef estimates size of problem remaining (smaller means better).
212 tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
213 fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 =
214 let val tac = tracify trace_BEST_FIRST tac1
215 fun pairsize th = (sizef th, th);
216 fun bfs (news,nprf_heap) =
217 (case List.partition satp news of
218 ([],nonsats) => next(foldr ThmHeap.insert
219 nprf_heap (map pairsize nonsats))
220 | (sats,_) => some_of_list sats)
222 if ThmHeap.is_empty nprf_heap then NONE
224 let val (n,prf) = ThmHeap.min nprf_heap
225 in if !trace_BEST_FIRST
226 then tracing("state size = " ^ string_of_int n)
228 bfs (Seq.list_of (tac prf),
229 deleteAllMin prf (ThmHeap.delete_min nprf_heap))
231 fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty)
232 in traced_tac btac end;
234 (*Ordinary best-first search, with no initial tactic*)
235 val BEST_FIRST = THEN_BEST_FIRST all_tac;
237 (*Breadth-first search to satisfy satpred (including initial state)
238 SLOW -- SHOULD NOT USE APPEND!*)
239 fun gen_BREADTH_FIRST message satpred (tac:tactic) =
240 let val tacf = Seq.list_of o tac;
242 (case List.partition satpred prfs of
245 (message("breadth=" ^ string_of_int(length nonsats));
246 bfs (List.concat (map tacf nonsats)))
248 in (fn st => Seq.of_list (bfs [st])) end;
250 val BREADTH_FIRST = gen_BREADTH_FIRST tracing;
251 val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
254 (* Author: Norbert Voelker, FernUniversitaet Hagen
255 Remarks: Implementation of A*-like proof procedure by modification
256 of the existing code for BEST_FIRST and best_tac so that the
257 current level of search is taken into account.
260 (*Insertion into priority queue of states, marked with level *)
261 fun insert_with_level (lnth: int*int*thm, []) = [lnth]
262 | insert_with_level ((l,m,th), (l',n,th')::nths) =
263 if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
264 else if n=m andalso eq_thm(th,th')
265 then (l',n,th')::nths
266 else (l,m,th)::(l',n,th')::nths;
268 (*For creating output sequence*)
269 fun some_of_list [] = NONE
270 | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
272 val trace_ASTAR = ref false;
274 fun THEN_ASTAR tac0 (satp, costf) tac1 =
275 let val tf = tracify trace_ASTAR tac1;
276 fun bfs (news,nprfs,level) =
277 let fun cost thm = (level, costf level thm, thm)
278 in (case List.partition satp news of
280 => next (foldr insert_with_level nprfs (map cost nonsats))
281 | (sats,_) => some_of_list sats)
284 | next ((level,n,prf)::nprfs) =
286 then tracing("level = " ^ string_of_int level ^
287 " cost = " ^ string_of_int n ^
288 " queue length =" ^ string_of_int (length nprfs))
290 bfs (Seq.list_of (tf prf), nprfs,level+1))
291 fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
292 in traced_tac tf end;
294 (*Ordinary ASTAR, with no initial tactic*)
295 val ASTAR = THEN_ASTAR all_tac;