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