author | blanchet |
Wed, 23 Jun 2010 10:20:33 +0200 | |
changeset 37512 | ff72d3ddc898 |
parent 37511 | 26afa11a1fb2 |
child 37518 | efb0923cc098 |
permissions | -rw-r--r-- |
35826 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML |
33311 | 2 |
Author: Jia Meng, Cambridge University Computer Laboratory |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36228
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
15347 | 4 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
5 |
Transformation of axiom rules (elim/intro/etc) into CNF forms. |
15347 | 6 |
*) |
7 |
||
35826 | 8 |
signature SLEDGEHAMMER_FACT_PREPROCESSOR = |
21505 | 9 |
sig |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
10 |
type cnf_thm = thm * ((string * int) * thm) |
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
blanchet
parents:
36945
diff
changeset
|
11 |
val chained_prefix: string |
32955 | 12 |
val trace: bool Unsynchronized.ref |
13 |
val trace_msg: (unit -> string) -> unit |
|
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
14 |
val skolem_theory_name: string |
35865 | 15 |
val skolem_prefix: string |
36492
60532b9bcd1c
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet
parents:
36478
diff
changeset
|
16 |
val skolem_infix: string |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
17 |
val is_skolem_const_name: string -> bool |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
18 |
val cnf_axiom: theory -> thm -> thm list |
27184 | 19 |
val multi_base_blacklist: string list |
37348 | 20 |
val is_theorem_bad_for_atps: thm -> bool |
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
33832
diff
changeset
|
21 |
val type_has_topsort: typ -> bool |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
22 |
val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list |
37496
9ae78e12e126
reintroduce new Sledgehammer polymorphic handling code;
blanchet
parents:
37488
diff
changeset
|
23 |
val saturate_skolem_cache: theory -> theory option |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
24 |
val auto_saturate_skolem_cache: bool Unsynchronized.ref |
36398
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset
|
25 |
val neg_clausify: thm -> thm list |
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset
|
26 |
val neg_conjecture_clauses: |
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset
|
27 |
Proof.context -> thm -> int -> thm list list * (string * typ) list |
24669 | 28 |
val setup: theory -> theory |
21505 | 29 |
end; |
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
30 |
|
35826 | 31 |
structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR = |
15997 | 32 |
struct |
15347 | 33 |
|
35865 | 34 |
open Sledgehammer_FOL_Clause |
35 |
||
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
36 |
type cnf_thm = thm * ((string * int) * thm) |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
37 |
|
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
blanchet
parents:
36945
diff
changeset
|
38 |
(* Used to label theorems chained into the goal. *) |
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
blanchet
parents:
36945
diff
changeset
|
39 |
val chained_prefix = "Sledgehammer.chained_" |
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
blanchet
parents:
36945
diff
changeset
|
40 |
|
32955 | 41 |
val trace = Unsynchronized.ref false; |
35865 | 42 |
fun trace_msg msg = if !trace then tracing (msg ()) else (); |
43 |
||
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
44 |
val skolem_theory_name = "Sledgehammer.Sko" |
35865 | 45 |
val skolem_prefix = "sko_" |
36492
60532b9bcd1c
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet
parents:
36478
diff
changeset
|
46 |
val skolem_infix = "$" |
32955 | 47 |
|
33832 | 48 |
fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th); |
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
49 |
|
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
33832
diff
changeset
|
50 |
val type_has_topsort = Term.exists_subtype |
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
33832
diff
changeset
|
51 |
(fn TFree (_, []) => true |
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
33832
diff
changeset
|
52 |
| TVar (_, []) => true |
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
33832
diff
changeset
|
53 |
| _ => false); |
27184 | 54 |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
55 |
|
15997 | 56 |
(**** Transformation of Elimination Rules into First-Order Formulas****) |
15347 | 57 |
|
29064 | 58 |
val cfalse = cterm_of @{theory HOL} HOLogic.false_const; |
59 |
val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const); |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
60 |
|
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
61 |
(*Converts an elim-rule into an equivalent theorem that does not have the |
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
62 |
predicate variable. Leaves other theorems unchanged. We simply instantiate the |
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
63 |
conclusion variable to False.*) |
16009 | 64 |
fun transform_elim th = |
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
65 |
case concl_of th of (*conclusion variable*) |
35963 | 66 |
@{const Trueprop} $ (v as Var (_, @{typ bool})) => |
29064 | 67 |
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th |
35963 | 68 |
| v as Var(_, @{typ prop}) => |
29064 | 69 |
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th |
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
70 |
| _ => th; |
15997 | 71 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
72 |
(*To enforce single-threading*) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
73 |
exception Clausify_failure of theory; |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
74 |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
75 |
|
16009 | 76 |
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) |
77 |
||
36492
60532b9bcd1c
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet
parents:
36478
diff
changeset
|
78 |
(*Keep the full complexity of the original name*) |
60532b9bcd1c
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet
parents:
36478
diff
changeset
|
79 |
fun flatten_name s = space_implode "_X" (Long_Name.explode s); |
60532b9bcd1c
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet
parents:
36478
diff
changeset
|
80 |
|
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
81 |
fun skolem_name thm_name j var_name = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
82 |
skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^ |
36492
60532b9bcd1c
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet
parents:
36478
diff
changeset
|
83 |
skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name) |
60532b9bcd1c
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet
parents:
36478
diff
changeset
|
84 |
|
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
85 |
(* Hack: Could return false positives (e.g., a user happens to declare a |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
86 |
constant called "SomeTheory.sko_means_shoe_in_$wedish". *) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
87 |
val is_skolem_const_name = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
88 |
Long_Name.base_name |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
89 |
#> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
90 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
91 |
fun rhs_extra_types lhsT rhs = |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
92 |
let val lhs_vars = Term.add_tfreesT lhsT [] |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
93 |
fun add_new_TFrees (TFree v) = |
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
94 |
if member (op =) lhs_vars v then I else insert (op =) (TFree v) |
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
95 |
| add_new_TFrees _ = I |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
96 |
val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs [] |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
97 |
in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end; |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
98 |
|
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
99 |
fun skolem_type_and_args bound_T body = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
100 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
101 |
val args1 = OldTerm.term_frees body |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
102 |
val Ts1 = map type_of args1 |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
103 |
val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
104 |
val args2 = map (fn T => Free (gensym "vsk", T)) Ts2 |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
105 |
in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
106 |
|
37348 | 107 |
(* Traverse a theorem, declaring Skolem function definitions. String "s" is the |
108 |
suggested prefix for the Skolem constants. *) |
|
37349 | 109 |
fun declare_skolem_funs s th thy = |
27174
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset
|
110 |
let |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
111 |
val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
112 |
fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
113 |
(axs, thy) = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
114 |
(*Existential: declare a Skolem function, then insert into body and continue*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
115 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
116 |
val id = skolem_name s (Unsynchronized.inc skolem_count) s' |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
117 |
val (cT, args) = skolem_type_and_args T body |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
118 |
val rhs = list_abs_free (map dest_Free args, |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
119 |
HOLogic.choice_const T $ body) |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
120 |
(*Forms a lambda-abstraction over the formal parameters*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
121 |
val (c, thy) = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
122 |
Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
123 |
val cdef = id ^ "_def" |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
124 |
val ((_, ax), thy) = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
125 |
Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
126 |
val ax' = Drule.export_without_context ax |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
127 |
in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end |
35963 | 128 |
| dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
129 |
(*Universal quant: insert a free variable into body and continue*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
130 |
let val fname = Name.variant (OldTerm.add_term_names (p, [])) a |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
131 |
in dec_sko (subst_bound (Free (fname, T), p)) thx end |
35963 | 132 |
| dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx) |
133 |
| dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx) |
|
134 |
| dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
135 |
| dec_sko _ thx = thx |
37349 | 136 |
in dec_sko (prop_of th) ([], thy) end |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
137 |
|
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
138 |
fun mk_skolem_id t = |
37436 | 139 |
let val T = fastype_of t in |
37496
9ae78e12e126
reintroduce new Sledgehammer polymorphic handling code;
blanchet
parents:
37488
diff
changeset
|
140 |
Const (@{const_name skolem_id}, T --> T) $ t |
37436 | 141 |
end |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
142 |
|
37512
ff72d3ddc898
this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents:
37511
diff
changeset
|
143 |
fun quasi_beta_eta_contract (Abs (s, T, t')) = |
ff72d3ddc898
this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents:
37511
diff
changeset
|
144 |
Abs (s, T, quasi_beta_eta_contract t') |
ff72d3ddc898
this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents:
37511
diff
changeset
|
145 |
| quasi_beta_eta_contract t = Envir.beta_eta_contract t |
ff72d3ddc898
this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents:
37511
diff
changeset
|
146 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
147 |
(*Traverse a theorem, accumulating Skolem function definitions.*) |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
148 |
fun assume_skolem_funs inline s th = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
149 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
150 |
val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
151 |
fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
152 |
(*Existential: declare a Skolem function, then insert into body and continue*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
153 |
let |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
154 |
val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
155 |
val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
156 |
val Ts = map type_of args |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
157 |
val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
158 |
val id = skolem_name s (Unsynchronized.inc skolem_count) s' |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
159 |
val c = Free (id, cT) |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
160 |
(* Forms a lambda-abstraction over the formal parameters *) |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
161 |
val rhs = |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
162 |
list_abs_free (map dest_Free args, |
37512
ff72d3ddc898
this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents:
37511
diff
changeset
|
163 |
HOLogic.choice_const T |
ff72d3ddc898
this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents:
37511
diff
changeset
|
164 |
$ quasi_beta_eta_contract body) |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
165 |
|> inline ? mk_skolem_id |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
166 |
val def = Logic.mk_equals (c, rhs) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
167 |
val comb = list_comb (if inline then rhs else c, args) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
168 |
in dec_sko (subst_bound (comb, p)) (def :: defs) end |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
169 |
| dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
170 |
(*Universal quant: insert a free variable into body and continue*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
171 |
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
172 |
in dec_sko (subst_bound (Free(fname,T), p)) defs end |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
173 |
| dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
174 |
| dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
175 |
| dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
176 |
| dec_sko _ defs = defs |
20419 | 177 |
in dec_sko (prop_of th) [] end; |
178 |
||
179 |
||
24827 | 180 |
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) |
20419 | 181 |
|
182 |
(*Returns the vars of a theorem*) |
|
183 |
fun vars_of_thm th = |
|
22691 | 184 |
map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
20419 | 185 |
|
186 |
(*Make a version of fun_cong with a given variable name*) |
|
187 |
local |
|
188 |
val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) |
|
189 |
val cx = hd (vars_of_thm fun_cong'); |
|
190 |
val ty = typ_of (ctyp_of_term cx); |
|
20445 | 191 |
val thy = theory_of_thm fun_cong; |
20419 | 192 |
fun mkvar a = cterm_of thy (Var((a,0),ty)); |
193 |
in |
|
194 |
fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong' |
|
195 |
end; |
|
196 |
||
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
197 |
(*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n, |
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
198 |
serves as an upper bound on how many to remove.*) |
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
199 |
fun strip_lambdas 0 th = th |
24669 | 200 |
| strip_lambdas n th = |
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
201 |
case prop_of th of |
35963 | 202 |
_ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) => |
24669 | 203 |
strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x)) |
204 |
| _ => th; |
|
20419 | 205 |
|
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
206 |
fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
207 |
| is_quasi_lambda_free (t1 $ t2) = |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
208 |
is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
209 |
| is_quasi_lambda_free (Abs _) = false |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
210 |
| is_quasi_lambda_free _ = true |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
211 |
|
32010 | 212 |
val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); |
213 |
val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); |
|
214 |
val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); |
|
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
215 |
|
24827 | 216 |
(*FIXME: requires more use of cterm constructors*) |
217 |
fun abstract ct = |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
218 |
let |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
219 |
val thy = theory_of_cterm ct |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
220 |
val Abs(x,_,body) = term_of ct |
35963 | 221 |
val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) |
24827 | 222 |
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT |
27184 | 223 |
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} |
24827 | 224 |
in |
225 |
case body of |
|
226 |
Const _ => makeK() |
|
227 |
| Free _ => makeK() |
|
228 |
| Var _ => makeK() (*though Var isn't expected*) |
|
27184 | 229 |
| Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) |
24827 | 230 |
| rator$rand => |
27184 | 231 |
if loose_bvar1 (rator,0) then (*C or S*) |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
232 |
if loose_bvar1 (rand,0) then (*S*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
233 |
let val crator = cterm_of thy (Abs(x,xT,rator)) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
234 |
val crand = cterm_of thy (Abs(x,xT,rand)) |
27184 | 235 |
val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} |
236 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_S') |
|
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
237 |
in |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
238 |
Thm.transitive abs_S' (Conv.binop_conv abstract rhs) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
239 |
end |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
240 |
else (*C*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
241 |
let val crator = cterm_of thy (Abs(x,xT,rator)) |
27184 | 242 |
val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} |
243 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_C') |
|
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
244 |
in |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
245 |
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
246 |
end |
27184 | 247 |
else if loose_bvar1 (rand,0) then (*B or eta*) |
36945 | 248 |
if rand = Bound 0 then Thm.eta_conversion ct |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
249 |
else (*B*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
250 |
let val crand = cterm_of thy (Abs(x,xT,rand)) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
251 |
val crator = cterm_of thy rator |
27184 | 252 |
val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} |
253 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_B') |
|
37349 | 254 |
in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
255 |
else makeK() |
37349 | 256 |
| _ => raise Fail "abstract: Bad term" |
24827 | 257 |
end; |
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
258 |
|
37349 | 259 |
(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) |
260 |
fun do_introduce_combinators ct = |
|
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
261 |
if is_quasi_lambda_free (term_of ct) then |
37349 | 262 |
Thm.reflexive ct |
263 |
else case term_of ct of |
|
264 |
Abs _ => |
|
265 |
let |
|
266 |
val (cv, cta) = Thm.dest_abs NONE ct |
|
267 |
val (v, _) = dest_Free (term_of cv) |
|
268 |
val u_th = do_introduce_combinators cta |
|
269 |
val cu = Thm.rhs_of u_th |
|
270 |
val comb_eq = abstract (Thm.cabs cv cu) |
|
271 |
in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end |
|
272 |
| _ $ _ => |
|
273 |
let val (ct1, ct2) = Thm.dest_comb ct in |
|
274 |
Thm.combination (do_introduce_combinators ct1) |
|
275 |
(do_introduce_combinators ct2) |
|
276 |
end |
|
277 |
||
278 |
fun introduce_combinators th = |
|
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
279 |
if is_quasi_lambda_free (prop_of th) then |
37349 | 280 |
th |
24827 | 281 |
else |
37349 | 282 |
let |
283 |
val th = Drule.eta_contraction_rule th |
|
284 |
val eqth = do_introduce_combinators (cprop_of th) |
|
285 |
in Thm.equal_elim eqth th end |
|
286 |
handle THM (msg, _, _) => |
|
287 |
(warning ("Error in the combinator translation of " ^ |
|
288 |
Display.string_of_thm_without_context th ^ |
|
289 |
"\nException message: " ^ msg ^ "."); |
|
290 |
(* A type variable of sort "{}" will make abstraction fail. *) |
|
291 |
TrueI) |
|
16009 | 292 |
|
293 |
(*cterms are used throughout for efficiency*) |
|
29064 | 294 |
val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop; |
16009 | 295 |
|
296 |
(*cterm version of mk_cTrueprop*) |
|
297 |
fun c_mkTrueprop A = Thm.capply cTrueprop A; |
|
298 |
||
299 |
(*Given an abstraction over n variables, replace the bound variables by free |
|
300 |
ones. Return the body, along with the list of free variables.*) |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
301 |
fun c_variant_abs_multi (ct0, vars) = |
16009 | 302 |
let val (cv,ct) = Thm.dest_abs NONE ct0 |
303 |
in c_variant_abs_multi (ct, cv::vars) end |
|
304 |
handle CTERM _ => (ct0, rev vars); |
|
305 |
||
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
306 |
(*Given the definition of a Skolem function, return a theorem to replace |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
307 |
an existential formula by a use of that function. |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
308 |
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
309 |
fun skolem_theorem_of_def inline def = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
310 |
let |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
311 |
val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def)) |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
312 |
val rhs' = rhs |> inline ? (snd o Thm.dest_comb) |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
313 |
val (ch, frees) = c_variant_abs_multi (rhs', []) |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
314 |
val (chilbert, cabs) = ch |> Thm.dest_comb |
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26618
diff
changeset
|
315 |
val thy = Thm.theory_of_cterm chilbert |
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26618
diff
changeset
|
316 |
val t = Thm.term_of chilbert |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
317 |
val T = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
318 |
case t of |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
319 |
Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
320 |
| _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t]) |
22596 | 321 |
val cex = Thm.cterm_of thy (HOLogic.exists_const T) |
16009 | 322 |
val ex_tm = c_mkTrueprop (Thm.capply cex cabs) |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
323 |
and conc = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
324 |
Drule.list_comb (if inline then rhs else c, frees) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
325 |
|> Drule.beta_conv cabs |> c_mkTrueprop |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
326 |
fun tacf [prem] = |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
327 |
(if inline then rewrite_goals_tac @{thms skolem_id_def_raw} |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
328 |
else rewrite_goals_tac [def]) |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
329 |
THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw}) |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
330 |
RS @{thm someI_ex}) 1 |
23352 | 331 |
in Goal.prove_internal [ex_tm] conc tacf |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
332 |
|> forall_intr_list frees |
26653 | 333 |
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35828
diff
changeset
|
334 |
|> Thm.varifyT_global |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
335 |
end; |
16009 | 336 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
337 |
|
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
338 |
(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
339 |
fun to_nnf th ctxt0 = |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
340 |
let val th1 = th |> transform_elim |> zero_var_indexes |
32262 | 341 |
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 |
342 |
val th3 = th2 |
|
35625 | 343 |
|> Conv.fconv_rule Object_Logic.atomize |
32262 | 344 |
|> Meson.make_nnf ctxt |> strip_lambdas ~1 |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
345 |
in (th3, ctxt) end; |
16009 | 346 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
347 |
(*Generate Skolem functions for a theorem supplied in nnf*) |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
348 |
fun skolem_theorems_of_assume inline s th = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
349 |
map (skolem_theorem_of_def inline o Thm.assume o cterm_of (theory_of_thm th)) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
350 |
(assume_skolem_funs inline s th) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
351 |
|
25007 | 352 |
|
37349 | 353 |
(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***) |
25007 | 354 |
|
37348 | 355 |
val max_lambda_nesting = 3 |
27184 | 356 |
|
37348 | 357 |
fun term_has_too_many_lambdas max (t1 $ t2) = |
358 |
exists (term_has_too_many_lambdas max) [t1, t2] |
|
359 |
| term_has_too_many_lambdas max (Abs (_, _, t)) = |
|
360 |
max = 0 orelse term_has_too_many_lambdas (max - 1) t |
|
361 |
| term_has_too_many_lambdas _ _ = false |
|
25007 | 362 |
|
37348 | 363 |
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) |
25007 | 364 |
|
37348 | 365 |
(* Don't count nested lambdas at the level of formulas, since they are |
366 |
quantifiers. *) |
|
367 |
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = |
|
368 |
formula_has_too_many_lambdas (T :: Ts) t |
|
369 |
| formula_has_too_many_lambdas Ts t = |
|
370 |
if is_formula_type (fastype_of1 (Ts, t)) then |
|
371 |
exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) |
|
372 |
else |
|
373 |
term_has_too_many_lambdas max_lambda_nesting t |
|
25007 | 374 |
|
37348 | 375 |
(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007) |
376 |
was 11. *) |
|
377 |
val max_apply_depth = 15 |
|
27184 | 378 |
|
37348 | 379 |
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) |
380 |
| apply_depth (Abs (_, _, t)) = apply_depth t |
|
381 |
| apply_depth _ = 0 |
|
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
382 |
|
37348 | 383 |
fun is_formula_too_complex t = |
384 |
apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse |
|
385 |
formula_has_too_many_lambdas [] t |
|
27184 | 386 |
|
25243 | 387 |
fun is_strange_thm th = |
388 |
case head_of (concl_of th) of |
|
35963 | 389 |
Const (a, _) => (a <> @{const_name Trueprop} andalso |
390 |
a <> @{const_name "=="}) |
|
25243 | 391 |
| _ => false; |
392 |
||
37348 | 393 |
fun is_theorem_bad_for_atps thm = |
394 |
let val t = prop_of thm in |
|
395 |
is_formula_too_complex t orelse exists_type type_has_topsort t orelse |
|
396 |
is_strange_thm thm |
|
397 |
end |
|
25243 | 398 |
|
35963 | 399 |
(* FIXME: put other record thms here, or declare as "no_atp" *) |
25007 | 400 |
val multi_base_blacklist = |
35963 | 401 |
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", |
402 |
"split_asm", "cases", "ext_cases"]; |
|
25007 | 403 |
|
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
404 |
fun fake_name th = |
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27809
diff
changeset
|
405 |
if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th) |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
406 |
else gensym "unknown_thm_"; |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
407 |
|
27184 | 408 |
(*Skolemize a named theorem, with Skolem functions as additional premises.*) |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
409 |
fun skolemize_theorem s th = |
37345
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37332
diff
changeset
|
410 |
if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse |
37348 | 411 |
is_theorem_bad_for_atps th then |
37345
4402a2bfa204
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
blanchet
parents:
37332
diff
changeset
|
412 |
[] |
27184 | 413 |
else |
414 |
let |
|
36603
d5d6111761a6
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
wenzelm
parents:
36492
diff
changeset
|
415 |
val ctxt0 = Variable.global_thm_context th |
37349 | 416 |
val (nnfth, ctxt) = to_nnf th ctxt0 |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
417 |
val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
418 |
val defs = skolem_theorems_of_assume inline s nnfth |
37349 | 419 |
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt |
420 |
in |
|
421 |
cnfs |> map introduce_combinators |
|
422 |
|> Variable.export ctxt ctxt0 |
|
423 |
|> Meson.finish_cnf |
|
424 |
end |
|
425 |
handle THM _ => [] |
|
27184 | 426 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
427 |
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
428 |
Skolem functions.*) |
33522 | 429 |
structure ThmCache = Theory_Data |
22846 | 430 |
( |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
431 |
type T = thm list Thmtab.table * unit Symtab.table; |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
432 |
val empty = (Thmtab.empty, Symtab.empty); |
26618 | 433 |
val extend = I; |
33522 | 434 |
fun merge ((cache1, seen1), (cache2, seen2)) : T = |
27184 | 435 |
(Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2)); |
22846 | 436 |
); |
22516 | 437 |
|
27184 | 438 |
val lookup_cache = Thmtab.lookup o #1 o ThmCache.get; |
439 |
val already_seen = Symtab.defined o #2 o ThmCache.get; |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
440 |
|
27184 | 441 |
val update_cache = ThmCache.map o apfst o Thmtab.update; |
442 |
fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ()))); |
|
25007 | 443 |
|
36228
df47dc6c0e03
got rid of somewhat pointless "pairname" function in Sledgehammer
blanchet
parents:
36106
diff
changeset
|
444 |
(* Convert Isabelle theorems into axiom clauses. *) |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
445 |
fun cnf_axiom thy th0 = |
27184 | 446 |
let val th = Thm.transfer thy th0 in |
447 |
case lookup_cache thy th of |
|
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
448 |
SOME cls => cls |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
449 |
| NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th) |
22516 | 450 |
end; |
15347 | 451 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
452 |
|
22471 | 453 |
(**** Translate a set of theorems into CNF ****) |
15347 | 454 |
|
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset
|
455 |
(*The combination of rev and tail recursion preserves the original order*) |
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
456 |
fun cnf_rules_pairs thy = |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
457 |
let |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
458 |
fun do_one _ [] = [] |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
459 |
| do_one ((name, k), th) (cls :: clss) = |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
460 |
(cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
461 |
fun do_all pairs [] = pairs |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
462 |
| do_all pairs ((name, th) :: ths) = |
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
463 |
let |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
464 |
val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th) |
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
465 |
handle THM _ => [] | |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
466 |
CLAUSE _ => [] |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
467 |
in do_all (new_pairs @ pairs) ths end |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
468 |
in do_all [] o rev end |
19353 | 469 |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
470 |
|
35865 | 471 |
(**** Convert all facts of the theory into FOL or HOL clauses ****) |
15347 | 472 |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
473 |
local |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
474 |
|
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
475 |
fun skolem_def (name, th) thy = |
36603
d5d6111761a6
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
wenzelm
parents:
36492
diff
changeset
|
476 |
let val ctxt0 = Variable.global_thm_context th in |
37348 | 477 |
case try (to_nnf th) ctxt0 of |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
478 |
NONE => (NONE, thy) |
37349 | 479 |
| SOME (nnfth, ctxt) => |
37348 | 480 |
let val (defs, thy') = declare_skolem_funs (flatten_name name) nnfth thy |
37349 | 481 |
in (SOME (th, ctxt0, ctxt, nnfth, defs), thy') end |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
482 |
end; |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
483 |
|
37349 | 484 |
fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) = |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
485 |
let |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
486 |
val (cnfs, ctxt) = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
487 |
Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
488 |
val cnfs' = cnfs |
37349 | 489 |
|> map introduce_combinators |
490 |
|> Variable.export ctxt ctxt0 |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
491 |
|> Meson.finish_cnf |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
492 |
|> map Thm.close_derivation; |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
493 |
in (th, cnfs') end; |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
494 |
|
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
495 |
in |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
496 |
|
27184 | 497 |
fun saturate_skolem_cache thy = |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
498 |
let |
33306
4138ba02b681
replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space;
wenzelm
parents:
33222
diff
changeset
|
499 |
val facts = PureThy.facts_of thy; |
4138ba02b681
replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space;
wenzelm
parents:
33222
diff
changeset
|
500 |
val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) => |
4138ba02b681
replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space;
wenzelm
parents:
33222
diff
changeset
|
501 |
if Facts.is_concealed facts name orelse already_seen thy name then I |
4138ba02b681
replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space;
wenzelm
parents:
33222
diff
changeset
|
502 |
else cons (name, ths)); |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
503 |
val new_thms = (new_facts, []) |-> fold (fn (name, ths) => |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
504 |
if member (op =) multi_base_blacklist (Long_Name.base_name name) then |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
505 |
I |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
506 |
else |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
507 |
fold_index (fn (i, th) => |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
508 |
if is_theorem_bad_for_atps th orelse |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
509 |
is_some (lookup_cache thy th) then |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
510 |
I |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
511 |
else |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
512 |
cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths) |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
513 |
in |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
514 |
if null new_facts then |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
515 |
NONE |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
516 |
else |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
517 |
let |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
518 |
val (defs, thy') = thy |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
519 |
|> fold (mark_seen o #1) new_facts |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
520 |
|> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms) |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
521 |
|>> map_filter I; |
29368 | 522 |
val cache_entries = Par_List.map skolem_cnfs defs; |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
523 |
in SOME (fold update_cache cache_entries thy') end |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
524 |
end; |
27184 | 525 |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
526 |
end; |
24854 | 527 |
|
37511 | 528 |
(* For emergency use where the Skolem cache causes problems. *) |
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
529 |
val auto_saturate_skolem_cache = Unsynchronized.ref true |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
530 |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
531 |
fun conditionally_saturate_skolem_cache thy = |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
532 |
if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
533 |
|
36398
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset
|
534 |
|
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
535 |
(*** Converting a subgoal into negated conjecture clauses. ***) |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
536 |
|
32262 | 537 |
fun neg_skolemize_tac ctxt = |
37332
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
538 |
EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt] |
36398
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset
|
539 |
|
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35865
diff
changeset
|
540 |
val neg_clausify = |
37349 | 541 |
single |
542 |
#> Meson.make_clauses_unsorted |
|
543 |
#> map introduce_combinators |
|
544 |
#> Meson.finish_cnf |
|
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
545 |
|
32257
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32231
diff
changeset
|
546 |
fun neg_conjecture_clauses ctxt st0 n = |
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32231
diff
changeset
|
547 |
let |
37332
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
548 |
(* "Option" is thrown if the assumptions contain schematic variables. *) |
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
549 |
val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0 |
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
550 |
val ({params, prems, ...}, _) = |
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
551 |
Subgoal.focus (Variable.set_body false ctxt) n st |
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
552 |
in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end |
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
553 |
|
27184 | 554 |
|
555 |
(** setup **) |
|
556 |
||
557 |
val setup = |
|
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
558 |
perhaps conditionally_saturate_skolem_cache |
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37496
diff
changeset
|
559 |
#> Theory.at_end conditionally_saturate_skolem_cache |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
560 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
561 |
end; |