|
1 (* Title: HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML |
|
2 Author: Nik Sultana, Cambridge University Computer Laboratory |
|
3 Collection of general functions used in the reconstruction module. |
|
4 *) |
|
5 |
|
6 signature TPTP_RECONSTRUCT_LIBRARY = |
|
7 sig |
|
8 exception BREAK_LIST |
|
9 val break_list : 'a list -> 'a * 'a list |
|
10 val break_seq : 'a Seq.seq -> 'a * 'a Seq.seq |
|
11 exception MULTI_ELEMENT_LIST |
|
12 val cascaded_filter_single : bool -> ('a list -> 'a list) list -> 'a list -> 'a option |
|
13 val concat_between : 'a list list -> ('a option * 'a option) -> 'a list |
|
14 exception DIFF_TYPE of typ * typ |
|
15 exception DIFF of term * term |
|
16 val diff : |
|
17 theory -> |
|
18 term * term -> (term * term) list * (typ * typ) list |
|
19 exception DISPLACE_KV |
|
20 val displace_kv : ''a -> (''a * 'b) list -> (''a * 'b) list |
|
21 val enumerate : int -> 'a list -> (int * 'a) list |
|
22 val fold_options : 'a option list -> 'a list |
|
23 val find_and_remove : ('a -> bool) -> 'a list -> 'a * 'a list |
|
24 val lift_option : ('a -> 'b) -> 'a option -> 'b option |
|
25 val list_diff : ''a list -> ''a list -> ''a list |
|
26 val list_prod : 'a list list -> 'a list -> 'a list -> 'a list list |
|
27 val permute : ''a list -> ''a list list |
|
28 val prefix_intersection_list : |
|
29 ''a list -> ''a list -> ''a list |
|
30 val repeat_until_fixpoint : (''a -> ''a) -> ''a -> ''a |
|
31 val switch : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c |
|
32 val zip_amap : |
|
33 'a list -> |
|
34 'b list -> |
|
35 ('a * 'b) list -> ('a * 'b) list * ('a list * 'b list) |
|
36 |
|
37 val consts_in : term -> term list |
|
38 val head_quantified_variable : |
|
39 int -> thm -> (string * typ) option |
|
40 val push_allvar_in : string -> term -> term |
|
41 val strip_top_All_var : term -> (string * typ) * term |
|
42 val strip_top_All_vars : term -> (string * typ) list * term |
|
43 val strip_top_all_vars : |
|
44 (string * typ) list -> term -> (string * typ) list * term |
|
45 val trace_tac' : |
|
46 string -> |
|
47 ('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq |
|
48 val try_dest_Trueprop : term -> term |
|
49 |
|
50 val type_devar : ((indexname * sort) * typ) list -> term -> term |
|
51 val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm |
|
52 |
|
53 val batter : int -> tactic |
|
54 val break_hypotheses : int -> tactic |
|
55 val clause_breaker : int -> tactic |
|
56 (* val dist_all_and_tac : Proof.context -> int -> tactic *)(*FIXME unused*) |
|
57 val reassociate_conjs_tac : Proof.context -> int -> tactic |
|
58 |
|
59 val ASAP : (int -> tactic) -> (int -> tactic) -> int -> tactic |
|
60 val COND' : |
|
61 ('a -> thm -> bool) -> |
|
62 ('a -> tactic) -> ('a -> tactic) -> 'a -> tactic |
|
63 |
|
64 val TERMFUN : |
|
65 (term list * term -> 'a) -> int option -> thm -> 'a list |
|
66 val TERMPRED : |
|
67 (term -> bool) -> |
|
68 (term -> bool) -> int option -> thm -> bool |
|
69 |
|
70 val guided_abstract : |
|
71 bool -> term -> term -> ((string * typ) * term) * term list |
|
72 val abstract : |
|
73 term list -> term -> ((string * typ) * term) list * term |
|
74 end |
|
75 |
|
76 structure TPTP_Reconstruct_Library : TPTP_RECONSTRUCT_LIBRARY = |
|
77 struct |
|
78 |
|
79 (*zip as much as possible*) |
|
80 fun zip_amap [] ys acc = (acc, ([], ys)) |
|
81 | zip_amap xs [] acc = (acc, (xs, [])) |
|
82 | zip_amap (x :: xs) (y :: ys) acc = |
|
83 zip_amap xs ys ((x, y) :: acc); |
|
84 |
|
85 (*Pair a list up with the position number of each element, |
|
86 starting from n*) |
|
87 fun enumerate n ls = |
|
88 let |
|
89 fun enumerate' [] _ acc = acc |
|
90 | enumerate' (x :: xs) n acc = enumerate' xs (n + 1) ((n, x) :: acc) |
|
91 in |
|
92 enumerate' ls n [] |
|
93 |> rev |
|
94 end |
|
95 |
|
96 (* |
|
97 enumerate 0 []; |
|
98 enumerate 0 ["a", "b", "c"]; |
|
99 *) |
|
100 |
|
101 (*List subtraction*) |
|
102 fun list_diff l1 l2 = |
|
103 List.filter (fn x => List.all (fn y => x <> y) l2) l1 |
|
104 |
|
105 val _ = @{assert} |
|
106 (list_diff [1,2,3] [2,4] = [1, 3]) |
|
107 |
|
108 (* [a,b] times_list [c,d] gives [[a,c,d], [b,c,d]] *) |
|
109 fun list_prod acc [] _ = rev acc |
|
110 | list_prod acc (x :: xs) ys = list_prod ((x :: ys) :: acc) xs ys |
|
111 |
|
112 fun repeat_until_fixpoint f x = |
|
113 let |
|
114 val x' = f x |
|
115 in |
|
116 if x = x' then x else repeat_until_fixpoint f x' |
|
117 end |
|
118 |
|
119 (*compute all permutations of a list*) |
|
120 fun permute l = |
|
121 let |
|
122 fun permute' (l, []) = [(l, [])] |
|
123 | permute' (l, xs) = |
|
124 map (fn x => (x :: l, filter (fn y => y <> x) xs)) xs |
|
125 |> map permute' |
|
126 |> List.concat |
|
127 in |
|
128 permute' ([], l) |
|
129 |> map fst |
|
130 end |
|
131 (* |
|
132 permute [1,2,3]; |
|
133 permute ["A", "B"] |
|
134 *) |
|
135 |
|
136 (*this exception is raised when the pair we wish to displace |
|
137 isn't found in the association list*) |
|
138 exception DISPLACE_KV; |
|
139 (*move a key-value pair, determined by the k, to the beginning of |
|
140 an association list. it moves the first occurrence of a pair |
|
141 keyed by "k"*) |
|
142 local |
|
143 fun fold_fun k (kv as (k', v)) (l, buff) = |
|
144 if is_some buff then (kv :: l, buff) |
|
145 else |
|
146 if k = k' then |
|
147 (l, SOME kv) |
|
148 else |
|
149 (kv :: l, buff) |
|
150 in |
|
151 (*"k" is the key value of the pair we wish to displace*) |
|
152 fun displace_kv k alist = |
|
153 let |
|
154 val (pre_alist, kv) = fold (fold_fun k) alist ([], NONE) |
|
155 in |
|
156 if is_some kv then |
|
157 the kv :: rev pre_alist |
|
158 else raise DISPLACE_KV |
|
159 end |
|
160 end |
|
161 |
|
162 (*Given two lists, it generates a new list where |
|
163 the intersection of the lists forms the prefix |
|
164 of the new list.*) |
|
165 local |
|
166 fun prefix_intersection_list' (acc_pre, acc_pro) l1 l2 = |
|
167 if null l1 then |
|
168 List.rev acc_pre @ List.rev acc_pro |
|
169 else if null l2 then |
|
170 List.rev acc_pre @ l1 @ List.rev acc_pro |
|
171 else |
|
172 let val l1_hd = hd l1 |
|
173 in |
|
174 prefix_intersection_list' |
|
175 (if member (op =) l2 l1_hd then |
|
176 (l1_hd :: acc_pre, acc_pro) |
|
177 else |
|
178 (acc_pre, l1_hd :: acc_pro)) |
|
179 (tl l1) l2 |
|
180 end |
|
181 in |
|
182 fun prefix_intersection_list l1 l2 = prefix_intersection_list' ([], []) l1 l2 |
|
183 end; |
|
184 |
|
185 val _ = @{assert} |
|
186 (prefix_intersection_list [1,2,3,4,5] [1,3,5] = [1, 3, 5, 2, 4]); |
|
187 |
|
188 val _ = @{assert} |
|
189 (prefix_intersection_list [1,2,3,4,5] [] = [1,2,3,4,5]); |
|
190 |
|
191 val _ = @{assert} |
|
192 (prefix_intersection_list [] [1,3,5] = []) |
|
193 |
|
194 fun switch f y x = f x y |
|
195 |
|
196 (*Given a value of type "'a option list", produce |
|
197 a value of type "'a list" by dropping the NONE elements |
|
198 and projecting the SOME elements.*) |
|
199 fun fold_options opt_list = |
|
200 fold |
|
201 (fn x => fn l => if is_some x then the x :: l else l) |
|
202 opt_list |
|
203 []; |
|
204 |
|
205 val _ = @{assert} |
|
206 ([2,0,1] = |
|
207 fold_options [NONE, SOME 1, NONE, SOME 0, NONE, NONE, SOME 2]); |
|
208 |
|
209 fun lift_option (f : 'a -> 'b) (x_opt : 'a option) : 'b option = |
|
210 case x_opt of |
|
211 NONE => NONE |
|
212 | SOME x => SOME (f x) |
|
213 |
|
214 fun break_seq x = (Seq.hd x, Seq.tl x) |
|
215 |
|
216 exception BREAK_LIST |
|
217 fun break_list (x :: xs) = (x, xs) |
|
218 | break_list _ = raise BREAK_LIST |
|
219 |
|
220 exception MULTI_ELEMENT_LIST |
|
221 (*Try a number of predicates, in order, to find a single element. |
|
222 Predicates are expected to either return an empty list or a |
|
223 singleton list. If strict=true and list has more than one element, |
|
224 then raise an exception. Otherwise try a new predicate.*) |
|
225 fun cascaded_filter_single strict preds l = |
|
226 case preds of |
|
227 [] => NONE |
|
228 | (p :: ps) => |
|
229 case p l of |
|
230 [] => cascaded_filter_single strict ps l |
|
231 | [x] => SOME x |
|
232 | l => |
|
233 if strict then raise MULTI_ELEMENT_LIST |
|
234 else cascaded_filter_single strict ps l |
|
235 |
|
236 (*concat but with optional before-and-after delimiters*) |
|
237 fun concat_between [] _ = [] |
|
238 | concat_between [l] _ = l |
|
239 | concat_between (l :: ls) (seps as (bef, aft)) = |
|
240 let |
|
241 val pre = if is_some bef then the bef :: l else l |
|
242 val mid = if is_some aft then [the aft] else [] |
|
243 val post = concat_between ls seps |
|
244 in |
|
245 pre @ mid @ post |
|
246 end |
|
247 |
|
248 (*Given a list, find an element satisfying pred, and return |
|
249 a pair consisting of that element and the list minus the element.*) |
|
250 fun find_and_remove pred l = |
|
251 find_index pred l |
|
252 |> switch chop l |
|
253 |> apsnd break_list |
|
254 |> (fn (xs, (y, ys)) => (y, xs @ ys)) |
|
255 |
|
256 val _ = @{assert} (find_and_remove (curry (op =) 3) [0,1,2,3,4,5] = (3, [0,1,2,4,5])) |
|
257 |
|
258 |
|
259 (** Functions on terms **) |
|
260 |
|
261 (*Extract the forall-prefix of a term, and return a pair consisting of the prefix |
|
262 and the body*) |
|
263 local |
|
264 (*Strip off HOL's All combinator if it's at the toplevel*) |
|
265 fun try_dest_All (Const (@{const_name HOL.All}, _) $ t) = t |
|
266 | try_dest_All (Const (@{const_name HOL.Trueprop}, _) $ t) = try_dest_All t |
|
267 | try_dest_All t = t |
|
268 |
|
269 val _ = @{assert} |
|
270 ((@{term "! x. (! y. P) = True"} |
|
271 |> try_dest_All |
|
272 |> Term.strip_abs_vars) |
|
273 = [("x", @{typ "'a"})]) |
|
274 |
|
275 val _ = @{assert} |
|
276 ((@{prop "! x. (! y. P) = True"} |
|
277 |> try_dest_All |
|
278 |> Term.strip_abs_vars) |
|
279 = [("x", @{typ "'a"})]) |
|
280 |
|
281 fun strip_top_All_vars' once acc t = |
|
282 let |
|
283 val t' = try_dest_All t |
|
284 val var = |
|
285 try (Term.strip_abs_vars #> hd) t' |
|
286 |
|
287 fun strip v t = |
|
288 (v, subst_bounds ([Free v], Term.strip_abs_body t)) |
|
289 in |
|
290 if t' = t orelse is_none var then (acc, t) |
|
291 else |
|
292 let |
|
293 val (v, t) = strip (the var) t' |
|
294 val acc' = v :: acc |
|
295 in |
|
296 if once then (acc', t) |
|
297 else strip_top_All_vars' once acc' t |
|
298 end |
|
299 end |
|
300 in |
|
301 fun strip_top_All_vars t = strip_top_All_vars' false [] t |
|
302 |
|
303 val _ = |
|
304 let |
|
305 val answer = |
|
306 ([("x", @{typ "'a"})], |
|
307 HOLogic.all_const @{typ "'a"} $ |
|
308 (HOLogic.eq_const @{typ "'a"} $ |
|
309 Free ("x", @{typ "'a"}))) |
|
310 in |
|
311 @{assert} |
|
312 ((@{term "! x. All (op = x)"} |
|
313 |> strip_top_All_vars) |
|
314 = answer) |
|
315 end |
|
316 |
|
317 (*like strip_top_All_vars, but peels a single variable off, instead of all of them*) |
|
318 fun strip_top_All_var t = |
|
319 strip_top_All_vars' true [] t |
|
320 |> apfst the_single |
|
321 end |
|
322 |
|
323 (*like strip_top_All_vars but for "all" instead of "All"*) |
|
324 fun strip_top_all_vars acc t = |
|
325 if Logic.is_all t then |
|
326 let |
|
327 val (v, t') = Logic.dest_all t |
|
328 (*bound instances in t' are replaced with free vars*) |
|
329 in |
|
330 strip_top_all_vars (v :: acc) t' |
|
331 end |
|
332 else (acc, (*variables are returned in FILO order*) |
|
333 t) |
|
334 |
|
335 (*given a term "t" |
|
336 ! X Y Z. t' |
|
337 then then "push_allvar_in "X" t" will give |
|
338 ! Y Z X. t' |
|
339 *) |
|
340 fun push_allvar_in v t = |
|
341 let |
|
342 val (vs, t') = strip_top_All_vars t |
|
343 val vs' = displace_kv v vs |
|
344 in |
|
345 fold (fn (v, ty) => fn t => |
|
346 HOLogic.mk_all (v, ty, t)) vs' t' |
|
347 end |
|
348 |
|
349 (*Lists all consts in a term, uniquely*) |
|
350 fun consts_in (Const c) = [Const c] |
|
351 | consts_in (Free _) = [] |
|
352 | consts_in (Var _) = [] |
|
353 | consts_in (Bound _) = [] |
|
354 | consts_in (Abs (_, _, t)) = consts_in t |
|
355 | consts_in (t1 $ t2) = union (op =) (consts_in t1) (consts_in t2); |
|
356 |
|
357 exception DIFF of term * term |
|
358 exception DIFF_TYPE of typ * typ |
|
359 (*This carries out naive form of matching. It "diffs" two formulas, |
|
360 to create a function which maps (schematic or non-schematic) |
|
361 variables to terms. The first argument is the more "general" term. |
|
362 The second argument is used to find the "image" for the variables in |
|
363 the first argument which don't appear in the second argument. |
|
364 |
|
365 Note that the list that is returned might have duplicate entries. |
|
366 It's not checked to see if the same variable maps to different |
|
367 values -- that should be regarded as an error.*) |
|
368 fun diff thy (initial as (t_gen, t)) = |
|
369 let |
|
370 fun diff_ty acc [] = acc |
|
371 | diff_ty acc ((pair as (ty_gen, ty)) :: ts) = |
|
372 case pair of |
|
373 (Type (s1, ty_gens1), Type (s2, ty_gens2)) => |
|
374 if s1 <> s2 orelse |
|
375 length ty_gens1 <> length ty_gens2 then |
|
376 raise (DIFF (t_gen, t)) |
|
377 else |
|
378 diff_ty acc |
|
379 (ts @ ListPair.zip (ty_gens1, ty_gens2)) |
|
380 | (TFree (s1, so1), TFree (s2, so2)) => |
|
381 if s1 <> s2 orelse |
|
382 not (Sign.subsort thy (so2, so1)) then |
|
383 raise (DIFF (t_gen, t)) |
|
384 else |
|
385 diff_ty acc ts |
|
386 | (TVar (idx1, so1), TVar (idx2, so2)) => |
|
387 if idx1 <> idx2 orelse |
|
388 not (Sign.subsort thy (so2, so1)) then |
|
389 raise (DIFF (t_gen, t)) |
|
390 else |
|
391 diff_ty acc ts |
|
392 | (TFree _, _) => diff_ty (pair :: acc) ts |
|
393 | (TVar _, _) => diff_ty (pair :: acc) ts |
|
394 | _ => raise (DIFF_TYPE pair) |
|
395 |
|
396 fun diff' (acc as (acc_t, acc_ty)) (pair as (t_gen, t)) ts = |
|
397 case pair of |
|
398 (Const (s1, ty1), Const (s2, ty2)) => |
|
399 if s1 <> s2 orelse |
|
400 not (Sign.typ_instance thy (ty2, ty1)) then |
|
401 raise (DIFF (t_gen, t)) |
|
402 else |
|
403 diff_probs acc ts |
|
404 | (Free (s1, ty1), Free (s2, ty2)) => |
|
405 if s1 <> s2 orelse |
|
406 not (Sign.typ_instance thy (ty2, ty1)) then |
|
407 raise (DIFF (t_gen, t)) |
|
408 else |
|
409 diff_probs acc ts |
|
410 | (Var (idx1, ty1), Var (idx2, ty2)) => |
|
411 if idx1 <> idx2 orelse |
|
412 not (Sign.typ_instance thy (ty2, ty1)) then |
|
413 raise (DIFF (t_gen, t)) |
|
414 else |
|
415 diff_probs acc ts |
|
416 | (Bound i1, Bound i2) => |
|
417 if i1 <> i2 then |
|
418 raise (DIFF (t_gen, t)) |
|
419 else |
|
420 diff_probs acc ts |
|
421 | (Abs (s1, ty1, t1), Abs (s2, ty2, t2)) => |
|
422 if s1 <> s2 orelse |
|
423 not (Sign.typ_instance thy (ty2, ty1)) then |
|
424 raise (DIFF (t_gen, t)) |
|
425 else |
|
426 diff' acc (t1, t2) ts |
|
427 | (ta1 $ ta2, tb1 $ tb2) => |
|
428 diff_probs acc ((ta1, tb1) :: (ta2, tb2) :: ts) |
|
429 |
|
430 (*the particularly important bit*) |
|
431 | (Free (_, ty), _) => |
|
432 diff_probs |
|
433 (pair :: acc_t, |
|
434 diff_ty acc_ty [(ty, Term.fastype_of t)]) |
|
435 ts |
|
436 | (Var (_, ty), _) => |
|
437 diff_probs |
|
438 (pair :: acc_t, |
|
439 diff_ty acc_ty [(ty, Term.fastype_of t)]) |
|
440 ts |
|
441 |
|
442 (*everything else is problematic*) |
|
443 | _ => raise (DIFF (t_gen, t)) |
|
444 |
|
445 and diff_probs acc ts = |
|
446 case ts of |
|
447 [] => acc |
|
448 | (pair :: ts') => diff' acc pair ts' |
|
449 in |
|
450 diff_probs ([], []) [initial] |
|
451 end |
|
452 |
|
453 (*Abstracts occurrences of "t_sub" in "t", returning a list of |
|
454 abstractions of "t" with a Var at each occurrence of "t_sub". |
|
455 If "strong=true" then it uses strong abstraction (i.e., replaces |
|
456 all occurrnces of "t_sub"), otherwise it uses weak abstraction |
|
457 (i.e., replaces the occurrences one at a time). |
|
458 NOTE there are many more possibilities between strong and week. |
|
459 These can be enumerated by abstracting based on the powerset |
|
460 of occurrences (minus the null element, which would correspond |
|
461 to "t"). |
|
462 *) |
|
463 fun guided_abstract strong t_sub t = |
|
464 let |
|
465 val varnames = Term.add_frees t [] |> map #1 |
|
466 val prefixK = "v" |
|
467 val freshvar = |
|
468 let |
|
469 fun find_fresh i = |
|
470 let |
|
471 val varname = prefixK ^ Int.toString i |
|
472 in |
|
473 if member (op =) varnames varname then |
|
474 find_fresh (i + 1) |
|
475 else |
|
476 (varname, fastype_of t_sub) |
|
477 end |
|
478 in |
|
479 find_fresh 0 |
|
480 end |
|
481 |
|
482 fun guided_abstract' t = |
|
483 case t of |
|
484 Abs (s, ty, t') => |
|
485 if t = t_sub then [Free freshvar] |
|
486 else |
|
487 (map (fn t' => Abs (s, ty, t')) |
|
488 (guided_abstract' t')) |
|
489 | t1 $ t2 => |
|
490 if t = t_sub then [Free freshvar] |
|
491 else |
|
492 (map (fn t' => t' $ t2) |
|
493 (guided_abstract' t1)) @ |
|
494 (map (fn t' => t1 $ t') |
|
495 (guided_abstract' t2)) |
|
496 | _ => |
|
497 if t = t_sub then [Free freshvar] |
|
498 else [t] |
|
499 |
|
500 fun guided_abstract_strong' t = |
|
501 let |
|
502 fun continue t = guided_abstract_strong' t |
|
503 |> (fn x => if null x then t |
|
504 else the_single x) |
|
505 in |
|
506 case t of |
|
507 Abs (s, ty, t') => |
|
508 if t = t_sub then [Free freshvar] |
|
509 else |
|
510 [Abs (s, ty, continue t')] |
|
511 | t1 $ t2 => |
|
512 if t = t_sub then [Free freshvar] |
|
513 else |
|
514 [continue t1 $ continue t2] |
|
515 | _ => |
|
516 if t = t_sub then [Free freshvar] |
|
517 else [t] |
|
518 end |
|
519 |
|
520 in |
|
521 ((freshvar, t_sub), |
|
522 if strong then guided_abstract_strong' t |
|
523 else guided_abstract' t) |
|
524 end |
|
525 |
|
526 (*Carries out strong abstraction of a term guided by a list of |
|
527 other terms. |
|
528 In case some of the latter terms happen to be the same, it |
|
529 only abstracts them once. |
|
530 It returns the abstracted term, together with a map from |
|
531 the fresh names to the terms.*) |
|
532 fun abstract ts t = |
|
533 fold_map (apsnd the_single oo (guided_abstract true)) ts t |
|
534 |> (fn (v_and_ts, t') => |
|
535 let |
|
536 val (vs, ts) = ListPair.unzip v_and_ts |
|
537 val vs' = |
|
538 (* list_diff vs (list_diff (Term.add_frees t' []) vs) *) |
|
539 Term.add_frees t' [] |
|
540 |> list_diff vs |
|
541 |> list_diff vs |
|
542 val v'_and_ts = |
|
543 map (fn v => |
|
544 (v, AList.lookup (op =) v_and_ts v |> the)) |
|
545 vs' |
|
546 in |
|
547 (v'_and_ts, t') |
|
548 end) |
|
549 |
|
550 (*Instantiate type variables in a term, based on a type environment*) |
|
551 fun type_devar (tyenv : ((indexname * sort) * typ) list) (t : term) : term = |
|
552 case t of |
|
553 Const (s, ty) => Const (s, Term_Subst.instantiateT tyenv ty) |
|
554 | Free (s, ty) => Free (s, Term_Subst.instantiateT tyenv ty) |
|
555 | Var (idx, ty) => Var (idx, Term_Subst.instantiateT tyenv ty) |
|
556 | Bound _ => t |
|
557 | Abs (s, ty, t') => |
|
558 Abs (s, Term_Subst.instantiateT tyenv ty, type_devar tyenv t') |
|
559 | t1 $ t2 => type_devar tyenv t1 $ type_devar tyenv t2 |
|
560 |
|
561 (*Take a "diff" between an (abstract) thm's term, and another term |
|
562 (the latter is an instance of the form), then instantiate the |
|
563 abstract theorem. This is a way of turning the latter term into |
|
564 a theorem, but without exposing the proof-search functions to |
|
565 complex terms. |
|
566 In addition to the abstract thm ("scheme_thm"), this function is |
|
567 also supplied with the (sub)term of the abstract thm ("scheme_t") |
|
568 we want to use in the diff, in case only part of "scheme_t" |
|
569 might be needed (not the whole "prop_of scheme_thm")*) |
|
570 fun diff_and_instantiate ctxt scheme_thm scheme_t instance_t = |
|
571 let |
|
572 val thy = Proof_Context.theory_of ctxt |
|
573 |
|
574 val (term_pairing, type_pairing) = |
|
575 diff thy (scheme_t, instance_t) |
|
576 |
|
577 (*valuation of type variables*) |
|
578 val typeval = map (pairself (ctyp_of thy)) type_pairing |
|
579 |
|
580 val typeval_env = |
|
581 map (apfst dest_TVar) type_pairing |
|
582 (*valuation of term variables*) |
|
583 val termval = |
|
584 map (apfst (type_devar typeval_env)) term_pairing |
|
585 |> map (pairself (cterm_of thy)) |
|
586 in |
|
587 Thm.instantiate (typeval, termval) scheme_thm |
|
588 end |
|
589 |
|
590 (*FIXME this is bad form?*) |
|
591 val try_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop) |
|
592 |
|
593 |
|
594 (** Some tacticals **) |
|
595 |
|
596 (*Lift COND to be parametrised by subgoal number*) |
|
597 fun COND' sat' tac'1 tac'2 i = |
|
598 COND (sat' i) (tac'1 i) (tac'2 i) |
|
599 |
|
600 (*Apply simplification ("wittler") as few times as possible |
|
601 before being able to apply a tactic ("tac"). |
|
602 This is like a lazy version of REPEAT, since it attempts |
|
603 to REPEAT a tactic the smallest number times as possible, |
|
604 to make some other tactic succeed subsequently.*) |
|
605 fun ASAP wittler (tac : int -> tactic) (i : int) = fn st => |
|
606 let |
|
607 val tac_result = tac i st |
|
608 val pulled_tac_result = Seq.pull tac_result |
|
609 val tac_failed = |
|
610 is_none pulled_tac_result orelse |
|
611 not (has_fewer_prems 1 (fst (the pulled_tac_result))) |
|
612 in |
|
613 if tac_failed then (wittler THEN' ASAP wittler tac) i st |
|
614 else tac_result |
|
615 end |
|
616 |
|
617 |
|
618 (** Some tactics **) |
|
619 |
|
620 val break_hypotheses = |
|
621 ((REPEAT_DETERM o etac @{thm conjE}) |
|
622 THEN' (REPEAT_DETERM o etac @{thm disjE}) |
|
623 ) #> CHANGED |
|
624 |
|
625 (*Prove subgoals of form A ==> B1 | ... | A | ... | Bn*) |
|
626 val clause_breaker = |
|
627 (REPEAT o (resolve_tac [@{thm "disjI1"}, @{thm "disjI2"}, @{thm "conjI"}])) |
|
628 THEN' atac |
|
629 |
|
630 (* |
|
631 Refines a subgoal have the form: |
|
632 A1 ... An ==> B1 | ... | Aj | ... | Bi | ... | Ak | ... |
|
633 into multiple subgoals of the form: |
|
634 A'1 ==> B1 | ... | Aj | ... | Bi | ... | Ak | ... |
|
635 : |
|
636 A'm ==> B1 | ... | Aj | ... | Bi | ... | Ak | ... |
|
637 where {A'1 .. A'm} is disjoint from {B1, ..., Aj, ..., Bi, ..., Ak, ...} |
|
638 (and solves the subgoal completely if the first set is empty) |
|
639 *) |
|
640 val batter = |
|
641 break_hypotheses |
|
642 THEN' K (ALLGOALS (TRY o clause_breaker)) |
|
643 |
|
644 (*Same idiom as ex_expander_tac*) |
|
645 fun dist_all_and_tac ctxt i = |
|
646 let |
|
647 val simpset = |
|
648 empty_simpset ctxt |
|
649 |> Simplifier.add_simp |
|
650 @{lemma "! x. P x & Q x \<equiv> (! x. P x) & (! x. Q x)" |
|
651 by (rule eq_reflection, auto)} |
|
652 in |
|
653 CHANGED (asm_full_simp_tac simpset i) |
|
654 end |
|
655 |
|
656 fun reassociate_conjs_tac ctxt = |
|
657 asm_full_simp_tac |
|
658 (Simplifier.add_simp |
|
659 @{lemma "(A & B) & C == A & B & C" by auto} (*FIXME duplicates @{thm simp_meta(3)}*) |
|
660 (Raw_Simplifier.empty_simpset ctxt)) |
|
661 #> CHANGED |
|
662 #> REPEAT_DETERM |
|
663 |
|
664 |
|
665 (** Subgoal analysis **) |
|
666 |
|
667 (*Given an inference |
|
668 C |
|
669 ----- |
|
670 D |
|
671 This function returns "SOME X" if C = "! X. C'". |
|
672 If C has no quantification prefix, then returns NONE.*) |
|
673 fun head_quantified_variable i = fn st => |
|
674 let |
|
675 val thy = Thm.theory_of_thm st |
|
676 val ctxt = Proof_Context.init_global thy |
|
677 |
|
678 val gls = |
|
679 prop_of st |
|
680 |> Logic.strip_horn |
|
681 |> fst |
|
682 |
|
683 val hypos = |
|
684 if null gls then [] |
|
685 else |
|
686 rpair (i - 1) gls |
|
687 |> uncurry nth |
|
688 |> strip_top_all_vars [] |
|
689 |> snd |
|
690 |> Logic.strip_horn |
|
691 |> fst |
|
692 |
|
693 fun foralls_of_hd_hypos () = |
|
694 hd hypos |
|
695 |> try_dest_Trueprop |
|
696 |> strip_top_All_vars |
|
697 |> #1 |
|
698 |> rev |
|
699 |
|
700 val quantified_variables = foralls_of_hd_hypos () |
|
701 in |
|
702 if null hypos orelse null quantified_variables then NONE |
|
703 else SOME (hd quantified_variables) |
|
704 end |
|
705 |
|
706 |
|
707 (** Builders for goal analysers or transformers **) |
|
708 |
|
709 (*Lifts function over terms to apply it to subgoals. |
|
710 "fun_over_terms" has type (term list * term -> 'a), where |
|
711 (term list * term) will be the term representations of the |
|
712 hypotheses and conclusion. |
|
713 if i_opt=SOME i then applies fun_over_terms to that |
|
714 subgoal and returns singleton result. |
|
715 otherwise applies fun_over_terms to all subgoals and return |
|
716 list of results.*) |
|
717 fun TERMFUN |
|
718 (fun_over_terms : term list * term -> 'a) |
|
719 (i_opt : int option) : thm -> 'a list = fn st => |
|
720 let |
|
721 val t_raws = |
|
722 Thm.rep_thm st |
|
723 |> #prop |
|
724 |> strip_top_all_vars [] |
|
725 |> snd |
|
726 |> Logic.strip_horn |
|
727 |> fst |
|
728 in |
|
729 if null t_raws then [] |
|
730 else |
|
731 let |
|
732 val ts = |
|
733 let |
|
734 val stripper = |
|
735 strip_top_all_vars [] |
|
736 #> snd |
|
737 #> Logic.strip_horn |
|
738 #> apsnd try_dest_Trueprop |
|
739 #> apfst (map try_dest_Trueprop) |
|
740 in |
|
741 map stripper t_raws |
|
742 end |
|
743 in |
|
744 case i_opt of |
|
745 NONE => |
|
746 map fun_over_terms ts |
|
747 | SOME i => |
|
748 nth ts (i - 1) |
|
749 |> fun_over_terms |
|
750 |> single |
|
751 end |
|
752 end |
|
753 |
|
754 (*Applies a predicate to subgoal(s) conclusion(s)*) |
|
755 fun TERMPRED |
|
756 (hyp_pred_over_terms : term -> bool) |
|
757 (conc_pred_over_terms : term -> bool) |
|
758 (i_opt : int option) : thm -> bool = fn st => |
|
759 let |
|
760 val hyp_results = |
|
761 TERMFUN (fst (*discard hypotheses*) |
|
762 #> map hyp_pred_over_terms) i_opt st |
|
763 val conc_results = |
|
764 TERMFUN (snd (*discard hypotheses*) |
|
765 #> conc_pred_over_terms) i_opt st |
|
766 val _ = @{assert} (length hyp_results = length conc_results) |
|
767 in |
|
768 if null hyp_results then true |
|
769 else |
|
770 let |
|
771 val hyps_conjoined = |
|
772 fold (fn a => fn b => |
|
773 b andalso (List.all (fn x => x) a)) hyp_results true |
|
774 val concs_conjoined = |
|
775 fold (fn a => fn b => |
|
776 b andalso a) conc_results true |
|
777 in hyps_conjoined andalso concs_conjoined end |
|
778 end |
|
779 |
|
780 |
|
781 (** Tracing **) |
|
782 (*If "tac i st" succeeds then msg is printed to "trace" channel*) |
|
783 fun trace_tac' msg tac i st = |
|
784 let |
|
785 val thy = Thm.theory_of_thm st |
|
786 val ctxt = Proof_Context.init_global thy |
|
787 val result = tac i st |
|
788 in |
|
789 if Config.get ctxt tptp_trace_reconstruction andalso |
|
790 not (is_none (Seq.pull result)) then |
|
791 (tracing msg; result) |
|
792 else result |
|
793 end |
|
794 |
|
795 end |