author | blanchet |
Mon, 28 Jun 2010 17:32:28 +0200 | |
changeset 37617 | f73cd4069f69 |
parent 37616 | c8d2d84d6011 |
child 37618 | fa57a87f92a0 |
permissions | -rw-r--r-- |
37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37572
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/clausifier.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 |
||
37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37572
diff
changeset
|
8 |
signature CLAUSIFIER = |
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) |
37543 | 11 |
|
32955 | 12 |
val trace: bool Unsynchronized.ref |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
13 |
val skolem_theory_name: string |
35865 | 14 |
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
|
15 |
val skolem_infix: string |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
16 |
val is_skolem_const_name: string -> bool |
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
17 |
val num_type_args: theory -> string -> int |
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 |
37584 | 23 |
val saturate_cache: theory -> theory option |
24 |
val auto_saturate_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 |
|
37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37572
diff
changeset
|
31 |
structure Clausifier : CLAUSIFIER = |
15997 | 32 |
struct |
15347 | 33 |
|
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
34 |
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
|
35 |
|
32955 | 36 |
val trace = Unsynchronized.ref false; |
35865 | 37 |
fun trace_msg msg = if !trace then tracing (msg ()) else (); |
38 |
||
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37584
diff
changeset
|
39 |
val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko" |
35865 | 40 |
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
|
41 |
val skolem_infix = "$" |
32955 | 42 |
|
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
33832
diff
changeset
|
43 |
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
|
44 |
(fn TFree (_, []) => true |
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
33832
diff
changeset
|
45 |
| TVar (_, []) => true |
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
33832
diff
changeset
|
46 |
| _ => false); |
27184 | 47 |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
48 |
|
15997 | 49 |
(**** Transformation of Elimination Rules into First-Order Formulas****) |
15347 | 50 |
|
29064 | 51 |
val cfalse = cterm_of @{theory HOL} HOLogic.false_const; |
52 |
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
|
53 |
|
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
54 |
(*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
|
55 |
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
|
56 |
conclusion variable to False.*) |
16009 | 57 |
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
|
58 |
case concl_of th of (*conclusion variable*) |
35963 | 59 |
@{const Trueprop} $ (v as Var (_, @{typ bool})) => |
29064 | 60 |
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th |
35963 | 61 |
| v as Var(_, @{typ prop}) => |
29064 | 62 |
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
|
63 |
| _ => th; |
15997 | 64 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
65 |
(*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
|
66 |
exception Clausify_failure of theory; |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
67 |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
68 |
|
16009 | 69 |
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) |
70 |
||
36492
60532b9bcd1c
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
blanchet
parents:
36478
diff
changeset
|
71 |
(*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
|
72 |
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
|
73 |
|
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
|
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
78 |
(* 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
|
79 |
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
|
80 |
val is_skolem_const_name = |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
81 |
Long_Name.base_name |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
82 |
#> 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
|
83 |
|
37572
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
84 |
(* The number of type arguments of a constant, zero if it's monomorphic. For |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
85 |
(instances of) Skolem pseudoconstants, this information is encoded in the |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
86 |
constant name. *) |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
87 |
fun num_type_args thy s = |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
88 |
if String.isPrefix skolem_theory_name s then |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
89 |
s |> unprefix skolem_theory_name |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
90 |
|> space_explode skolem_infix |> hd |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
91 |
|> space_explode "_" |> List.last |> Int.fromString |> the |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
92 |
else |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
93 |
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
a899f9506f39
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37571
diff
changeset
|
94 |
|
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
95 |
fun mk_skolem_id t = |
37436 | 96 |
let val T = fastype_of t in |
37496
9ae78e12e126
reintroduce new Sledgehammer polymorphic handling code;
blanchet
parents:
37488
diff
changeset
|
97 |
Const (@{const_name skolem_id}, T --> T) $ t |
37436 | 98 |
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
|
99 |
|
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
100 |
fun beta_eta_under_lambdas (Abs (s, T, t')) = |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
101 |
Abs (s, T, beta_eta_under_lambdas t') |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
102 |
| beta_eta_under_lambdas t = Envir.beta_eta_contract t |
37512
ff72d3ddc898
this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents:
37511
diff
changeset
|
103 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
104 |
(*Traverse a theorem, accumulating Skolem function definitions.*) |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
105 |
fun assume_skolem_funs th = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
106 |
let |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
107 |
fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) rhss = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
108 |
(*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
|
109 |
let |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
110 |
val args = OldTerm.term_frees body |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
111 |
val Ts = map type_of args |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
112 |
val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *) |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
113 |
(* 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
|
114 |
val rhs = |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
115 |
list_abs_free (map dest_Free args, |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
116 |
HOLogic.choice_const T $ beta_eta_under_lambdas body) |
37518
efb0923cc098
use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
blanchet
parents:
37512
diff
changeset
|
117 |
|> mk_skolem_id |
efb0923cc098
use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
blanchet
parents:
37512
diff
changeset
|
118 |
val comb = list_comb (rhs, args) |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
119 |
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
120 |
| dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
121 |
(*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
|
122 |
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
123 |
in dec_sko (subst_bound (Free(fname,T), p)) rhss end |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
124 |
| dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
125 |
| dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
126 |
| dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
127 |
| dec_sko _ rhss = rhss |
20419 | 128 |
in dec_sko (prop_of th) [] end; |
129 |
||
130 |
||
24827 | 131 |
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) |
20419 | 132 |
|
133 |
(*Returns the vars of a theorem*) |
|
134 |
fun vars_of_thm th = |
|
22691 | 135 |
map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
20419 | 136 |
|
37540
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
137 |
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} |
20419 | 138 |
|
37540
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
139 |
(* Removes the lambdas from an equation of the form t = (%x. u). *) |
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
140 |
fun extensionalize th = |
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
141 |
case prop_of th of |
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
142 |
_ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _])) |
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
143 |
$ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all) |
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
144 |
| _ => th |
20419 | 145 |
|
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
146 |
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
|
147 |
| is_quasi_lambda_free (t1 $ t2) = |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
148 |
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
|
149 |
| is_quasi_lambda_free (Abs _) = false |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
150 |
| is_quasi_lambda_free _ = true |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
151 |
|
32010 | 152 |
val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); |
153 |
val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); |
|
154 |
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
|
155 |
|
24827 | 156 |
(*FIXME: requires more use of cterm constructors*) |
157 |
fun abstract ct = |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
158 |
let |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
159 |
val thy = theory_of_cterm ct |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
160 |
val Abs(x,_,body) = term_of ct |
35963 | 161 |
val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) |
24827 | 162 |
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT |
27184 | 163 |
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} |
24827 | 164 |
in |
165 |
case body of |
|
166 |
Const _ => makeK() |
|
167 |
| Free _ => makeK() |
|
168 |
| Var _ => makeK() (*though Var isn't expected*) |
|
27184 | 169 |
| Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) |
24827 | 170 |
| rator$rand => |
27184 | 171 |
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
|
172 |
if loose_bvar1 (rand,0) then (*S*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
173 |
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
|
174 |
val crand = cterm_of thy (Abs(x,xT,rand)) |
27184 | 175 |
val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} |
176 |
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
|
177 |
in |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
178 |
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
|
179 |
end |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
180 |
else (*C*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
181 |
let val crator = cterm_of thy (Abs(x,xT,rator)) |
27184 | 182 |
val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} |
183 |
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
|
184 |
in |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
185 |
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
|
186 |
end |
27184 | 187 |
else if loose_bvar1 (rand,0) then (*B or eta*) |
36945 | 188 |
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
|
189 |
else (*B*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
190 |
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
|
191 |
val crator = cterm_of thy rator |
27184 | 192 |
val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} |
193 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_B') |
|
37349 | 194 |
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
|
195 |
else makeK() |
37349 | 196 |
| _ => raise Fail "abstract: Bad term" |
24827 | 197 |
end; |
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
198 |
|
37349 | 199 |
(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) |
200 |
fun do_introduce_combinators ct = |
|
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
201 |
if is_quasi_lambda_free (term_of ct) then |
37349 | 202 |
Thm.reflexive ct |
203 |
else case term_of ct of |
|
204 |
Abs _ => |
|
205 |
let |
|
206 |
val (cv, cta) = Thm.dest_abs NONE ct |
|
207 |
val (v, _) = dest_Free (term_of cv) |
|
208 |
val u_th = do_introduce_combinators cta |
|
209 |
val cu = Thm.rhs_of u_th |
|
210 |
val comb_eq = abstract (Thm.cabs cv cu) |
|
211 |
in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end |
|
212 |
| _ $ _ => |
|
213 |
let val (ct1, ct2) = Thm.dest_comb ct in |
|
214 |
Thm.combination (do_introduce_combinators ct1) |
|
215 |
(do_introduce_combinators ct2) |
|
216 |
end |
|
217 |
||
218 |
fun introduce_combinators th = |
|
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
219 |
if is_quasi_lambda_free (prop_of th) then |
37349 | 220 |
th |
24827 | 221 |
else |
37349 | 222 |
let |
223 |
val th = Drule.eta_contraction_rule th |
|
224 |
val eqth = do_introduce_combinators (cprop_of th) |
|
225 |
in Thm.equal_elim eqth th end |
|
226 |
handle THM (msg, _, _) => |
|
227 |
(warning ("Error in the combinator translation of " ^ |
|
228 |
Display.string_of_thm_without_context th ^ |
|
229 |
"\nException message: " ^ msg ^ "."); |
|
230 |
(* A type variable of sort "{}" will make abstraction fail. *) |
|
231 |
TrueI) |
|
16009 | 232 |
|
233 |
(*cterms are used throughout for efficiency*) |
|
29064 | 234 |
val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop; |
16009 | 235 |
|
236 |
(*Given an abstraction over n variables, replace the bound variables by free |
|
237 |
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
|
238 |
fun c_variant_abs_multi (ct0, vars) = |
16009 | 239 |
let val (cv,ct) = Thm.dest_abs NONE ct0 |
240 |
in c_variant_abs_multi (ct, cv::vars) end |
|
241 |
handle CTERM _ => (ct0, rev vars); |
|
242 |
||
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
243 |
val skolem_id_def_raw = @{thms skolem_id_def_raw} |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
244 |
|
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
245 |
(* Given the definition of a Skolem function, return a theorem to replace |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
246 |
an existential formula by a use of that function. |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
247 |
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
248 |
fun skolem_theorem_of_def thy rhs0 = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
249 |
let |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
250 |
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
251 |
val rhs' = rhs |> Thm.dest_comb |> snd |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
252 |
val (ch, frees) = c_variant_abs_multi (rhs', []) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
253 |
val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
254 |
val T = |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
255 |
case hilbert of |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
256 |
Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
257 |
| _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert]) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
258 |
val cex = Thm.cterm_of thy (HOLogic.exists_const T) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
259 |
val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
260 |
and conc = |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
261 |
Drule.list_comb (rhs, frees) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
262 |
|> Drule.beta_conv cabs |> Thm.capply cTrueprop |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
263 |
fun tacf [prem] = |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
264 |
rewrite_goals_tac skolem_id_def_raw |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
265 |
THEN rtac ((prem |> rewrite_rule skolem_id_def_raw) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
266 |
RS @{thm someI_ex}) 1 |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
267 |
in |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
268 |
Goal.prove_internal [ex_tm] conc tacf |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
269 |
|> forall_intr_list frees |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
270 |
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
271 |
|> Thm.varifyT_global |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
272 |
end |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
273 |
|
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
274 |
(*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
|
275 |
fun to_nnf th ctxt0 = |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
276 |
let val th1 = th |> transform_elim |> zero_var_indexes |
32262 | 277 |
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 |
37540
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
278 |
val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize |
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
279 |
|> extensionalize |
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
280 |
|> Meson.make_nnf ctxt |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
281 |
in (th3, ctxt) end; |
16009 | 282 |
|
37349 | 283 |
(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***) |
25007 | 284 |
|
37348 | 285 |
val max_lambda_nesting = 3 |
27184 | 286 |
|
37348 | 287 |
fun term_has_too_many_lambdas max (t1 $ t2) = |
288 |
exists (term_has_too_many_lambdas max) [t1, t2] |
|
289 |
| term_has_too_many_lambdas max (Abs (_, _, t)) = |
|
290 |
max = 0 orelse term_has_too_many_lambdas (max - 1) t |
|
291 |
| term_has_too_many_lambdas _ _ = false |
|
25007 | 292 |
|
37348 | 293 |
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) |
25007 | 294 |
|
37348 | 295 |
(* Don't count nested lambdas at the level of formulas, since they are |
296 |
quantifiers. *) |
|
297 |
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = |
|
298 |
formula_has_too_many_lambdas (T :: Ts) t |
|
299 |
| formula_has_too_many_lambdas Ts t = |
|
300 |
if is_formula_type (fastype_of1 (Ts, t)) then |
|
301 |
exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) |
|
302 |
else |
|
303 |
term_has_too_many_lambdas max_lambda_nesting t |
|
25007 | 304 |
|
37348 | 305 |
(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007) |
306 |
was 11. *) |
|
307 |
val max_apply_depth = 15 |
|
27184 | 308 |
|
37348 | 309 |
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) |
310 |
| apply_depth (Abs (_, _, t)) = apply_depth t |
|
311 |
| apply_depth _ = 0 |
|
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
312 |
|
37348 | 313 |
fun is_formula_too_complex t = |
314 |
apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse |
|
315 |
formula_has_too_many_lambdas [] t |
|
27184 | 316 |
|
25243 | 317 |
fun is_strange_thm th = |
318 |
case head_of (concl_of th) of |
|
35963 | 319 |
Const (a, _) => (a <> @{const_name Trueprop} andalso |
320 |
a <> @{const_name "=="}) |
|
25243 | 321 |
| _ => false; |
322 |
||
37348 | 323 |
fun is_theorem_bad_for_atps thm = |
324 |
let val t = prop_of thm in |
|
325 |
is_formula_too_complex t orelse exists_type type_has_topsort t orelse |
|
326 |
is_strange_thm thm |
|
327 |
end |
|
25243 | 328 |
|
35963 | 329 |
(* FIXME: put other record thms here, or declare as "no_atp" *) |
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37584
diff
changeset
|
330 |
(* FIXME: move to "Sledgehammer_Fact_Filter" *) |
25007 | 331 |
val multi_base_blacklist = |
35963 | 332 |
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", |
333 |
"split_asm", "cases", "ext_cases"]; |
|
25007 | 334 |
|
27184 | 335 |
(*Skolemize a named theorem, with Skolem functions as additional premises.*) |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
336 |
fun skolemize_theorem thy th = |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
337 |
if member (op =) multi_base_blacklist |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
338 |
(Long_Name.base_name (Thm.get_name_hint th)) orelse |
37348 | 339 |
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
|
340 |
[] |
27184 | 341 |
else |
342 |
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
|
343 |
val ctxt0 = Variable.global_thm_context th |
37349 | 344 |
val (nnfth, ctxt) = to_nnf th ctxt0 |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
345 |
val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
346 |
val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt |
37349 | 347 |
in |
348 |
cnfs |> map introduce_combinators |
|
349 |
|> Variable.export ctxt ctxt0 |
|
350 |
|> Meson.finish_cnf |
|
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
351 |
|> map Thm.close_derivation |
37349 | 352 |
end |
353 |
handle THM _ => [] |
|
27184 | 354 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
355 |
(*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
|
356 |
Skolem functions.*) |
33522 | 357 |
structure ThmCache = Theory_Data |
22846 | 358 |
( |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
359 |
type T = thm list Thmtab.table * unit Symtab.table; |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
360 |
val empty = (Thmtab.empty, Symtab.empty); |
26618 | 361 |
val extend = I; |
33522 | 362 |
fun merge ((cache1, seen1), (cache2, seen2)) : T = |
27184 | 363 |
(Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2)); |
22846 | 364 |
); |
22516 | 365 |
|
36228
df47dc6c0e03
got rid of somewhat pointless "pairname" function in Sledgehammer
blanchet
parents:
36106
diff
changeset
|
366 |
(* Convert Isabelle theorems into axiom clauses. *) |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
367 |
fun cnf_axiom thy th0 = |
27184 | 368 |
let val th = Thm.transfer thy th0 in |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
369 |
case Thmtab.lookup (#1 (ThmCache.get thy)) th of |
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
370 |
SOME cls => cls |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
371 |
| NONE => skolemize_theorem thy th |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
372 |
end |
15347 | 373 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
374 |
|
22471 | 375 |
(**** Translate a set of theorems into CNF ****) |
15347 | 376 |
|
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset
|
377 |
(*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
|
378 |
fun cnf_rules_pairs thy = |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
379 |
let |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
380 |
fun do_one _ [] = [] |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
381 |
| 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
|
382 |
(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
|
383 |
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
|
384 |
| do_all pairs ((name, th) :: ths) = |
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
385 |
let |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
386 |
val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th) |
37570 | 387 |
handle THM _ => [] |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
388 |
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
|
389 |
in do_all [] o rev end |
19353 | 390 |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
391 |
|
35865 | 392 |
(**** Convert all facts of the theory into FOL or HOL clauses ****) |
15347 | 393 |
|
37584 | 394 |
fun saturate_cache thy = |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
395 |
let |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
396 |
val (cache, seen) = ThmCache.get thy |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
397 |
val facts = PureThy.facts_of thy |
33306
4138ba02b681
replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space;
wenzelm
parents:
33222
diff
changeset
|
398 |
val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) => |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
399 |
if Facts.is_concealed facts name orelse Symtab.defined seen name then I |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
400 |
else cons (name, ths)) |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
401 |
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
|
402 |
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
|
403 |
I |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
404 |
else |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
405 |
fold_index (fn (i, th) => |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
406 |
if is_theorem_bad_for_atps th orelse Thmtab.defined cache th then |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
407 |
I |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
408 |
else |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
409 |
cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths) |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
410 |
val entries = |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
411 |
Par_List.map (fn (_, th) => (th, skolemize_theorem thy th)) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
412 |
(sort_distinct (Thm.thm_ord o pairself snd) new_thms) |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
413 |
in |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
414 |
if null entries then |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
415 |
NONE |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
416 |
else |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
417 |
thy |> ThmCache.map (fn p => p |>> fold Thmtab.update entries |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
418 |
||> fold Symtab.update |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
419 |
(map (rpair () o #1) new_facts)) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
420 |
|> SOME |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
421 |
end |
24854 | 422 |
|
37511 | 423 |
(* For emergency use where the Skolem cache causes problems. *) |
37584 | 424 |
val auto_saturate_cache = Unsynchronized.ref true |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
425 |
|
37584 | 426 |
fun conditionally_saturate_cache thy = |
427 |
if !auto_saturate_cache then saturate_cache thy else NONE |
|
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
428 |
|
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
|
429 |
|
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
430 |
(*** Converting a subgoal into negated conjecture clauses. ***) |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
431 |
|
32262 | 432 |
fun neg_skolemize_tac ctxt = |
37332
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
433 |
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
|
434 |
|
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35865
diff
changeset
|
435 |
val neg_clausify = |
37349 | 436 |
single |
437 |
#> Meson.make_clauses_unsorted |
|
438 |
#> map introduce_combinators |
|
439 |
#> Meson.finish_cnf |
|
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
440 |
|
32257
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32231
diff
changeset
|
441 |
fun neg_conjecture_clauses ctxt st0 n = |
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32231
diff
changeset
|
442 |
let |
37332
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
443 |
(* "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
|
444 |
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
|
445 |
val ({params, prems, ...}, _) = |
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset
|
446 |
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
|
447 |
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
|
448 |
|
27184 | 449 |
|
450 |
(** setup **) |
|
451 |
||
452 |
val setup = |
|
37584 | 453 |
perhaps conditionally_saturate_cache |
454 |
#> Theory.at_end conditionally_saturate_cache |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
455 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
456 |
end; |