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 =
|
|
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
|