author | blanchet |
Wed, 11 Jul 2012 21:43:19 +0200 | |
changeset 48248 | b6eb45a52c28 |
parent 48237 | d7ad89f60768 |
child 48250 | 1065c307fafe |
permissions | -rw-r--r-- |
38988 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter.ML |
38027 | 2 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36227
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
39958 | 4 |
|
48248 | 5 |
Sledgehammer's hybrid relevance filter. |
33309 | 6 |
*) |
15452 | 7 |
|
38988 | 8 |
signature SLEDGEHAMMER_FILTER = |
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset
|
9 |
sig |
46388 | 10 |
type status = ATP_Problem_Generate.status |
46340 | 11 |
type stature = ATP_Problem_Generate.stature |
48248 | 12 |
type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge |
13 |
type relevance_override = Sledgehammer_Filter_Iter.relevance_override |
|
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset
|
14 |
|
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44400
diff
changeset
|
15 |
val no_relevance_override : relevance_override |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
16 |
val fact_from_ref : |
46388 | 17 |
Proof.context -> unit Symtab.table -> thm list -> status Termtab.table |
46340 | 18 |
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list |
41767
44b2a0385001
export useful function (needed in a Sledgehammer-related experiment)
blanchet
parents:
41491
diff
changeset
|
19 |
val all_facts : |
46734 | 20 |
Proof.context -> bool -> 'a Symtab.table -> bool -> thm list |
47774 | 21 |
-> thm list -> status Termtab.table |
22 |
-> (((unit -> string) * stature) * thm) list |
|
48248 | 23 |
val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
48237 | 24 |
val maybe_instantiate_inducts : |
25 |
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
|
26 |
-> (((unit -> string) * 'a) * thm) list |
|
27 |
val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list |
|
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43324
diff
changeset
|
28 |
val nearly_all_facts : |
44585 | 29 |
Proof.context -> bool -> relevance_override -> thm list -> term list -> term |
46340 | 30 |
-> (((unit -> string) * stature) * thm) list |
37347
635425a442e8
show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset
|
31 |
val relevant_facts : |
44625 | 32 |
Proof.context -> real * real -> int |
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset
|
33 |
-> (string * typ -> term list -> bool * term list) -> relevance_fudge |
41066
3890ef4e02f9
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset
|
34 |
-> relevance_override -> thm list -> term list -> term |
46340 | 35 |
-> (((unit -> string) * stature) * thm) list |
36 |
-> ((string * stature) * thm) list |
|
15347 | 37 |
end; |
38 |
||
38988 | 39 |
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = |
15347 | 40 |
struct |
41 |
||
46320 | 42 |
open ATP_Problem_Generate |
44934 | 43 |
open Metis_Tactic |
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38644
diff
changeset
|
44 |
open Sledgehammer_Util |
48248 | 45 |
open Sledgehammer_Filter_Iter |
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44400
diff
changeset
|
46 |
|
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset
|
47 |
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator |
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset
|
48 |
|
48248 | 49 |
val no_relevance_override = {add = [], del = [], only = false} |
46388 | 50 |
|
40227
e31e3f0071d4
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset
|
51 |
fun needs_quoting reserved s = |
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
52 |
Symtab.defined reserved s orelse |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
41999
diff
changeset
|
53 |
exists (not o Lexicon.is_identifier) (Long_Name.explode s) |
40227
e31e3f0071d4
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset
|
54 |
|
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
55 |
fun make_name reserved multi j name = |
40227
e31e3f0071d4
support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset
|
56 |
(name |> needs_quoting reserved name ? quote) ^ |
41491 | 57 |
(if multi then "(" ^ string_of_int j ^ ")" else "") |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
58 |
|
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
59 |
fun explode_interval _ (Facts.FromTo (i, j)) = i upto j |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
60 |
| explode_interval max (Facts.From i) = i upto i + max - 1 |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
61 |
| explode_interval _ (Facts.Single i) = [i] |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
62 |
|
41279 | 63 |
val backquote = |
64 |
raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`" |
|
46388 | 65 |
|
48248 | 66 |
(* unfolding these can yield really huge terms *) |
67 |
val risky_defs = @{thms Bit0_def Bit1_def} |
|
68 |
||
69 |
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) |
|
70 |
fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t |
|
71 |
| is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2 |
|
72 |
| is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2 |
|
73 |
| is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2 |
|
74 |
| is_rec_def _ = false |
|
75 |
||
46388 | 76 |
fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms |
77 |
fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths |
|
78 |
||
79 |
fun scope_of_thm global assms chained_ths th = |
|
80 |
if is_chained chained_ths th then Chained |
|
81 |
else if global then Global |
|
82 |
else if is_assum assms th then Assum |
|
83 |
else Local |
|
84 |
||
47904
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47774
diff
changeset
|
85 |
val may_be_induction = |
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47774
diff
changeset
|
86 |
exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => |
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47774
diff
changeset
|
87 |
body_type T = @{typ bool} |
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47774
diff
changeset
|
88 |
| _ => false) |
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47774
diff
changeset
|
89 |
|
46388 | 90 |
fun status_of_thm css_table name th = |
91 |
(* FIXME: use structured name *) |
|
47904
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47774
diff
changeset
|
92 |
if (String.isSubstring ".induct" name orelse |
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47774
diff
changeset
|
93 |
String.isSubstring ".inducts" name) andalso |
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47774
diff
changeset
|
94 |
may_be_induction (prop_of th) then |
47148
7b5846065c1b
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
blanchet
parents:
47073
diff
changeset
|
95 |
Induction |
46388 | 96 |
else case Termtab.lookup css_table (prop_of th) of |
97 |
SOME status => status |
|
98 |
| NONE => General |
|
99 |
||
100 |
fun stature_of_thm global assms chained_ths css_table name th = |
|
101 |
(scope_of_thm global assms chained_ths th, status_of_thm css_table name th) |
|
102 |
||
103 |
fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) = |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
104 |
let |
38996 | 105 |
val ths = Attrib.eval_thms ctxt [xthm] |
106 |
val bracket = |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41989
diff
changeset
|
107 |
map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41989
diff
changeset
|
108 |
|> implode |
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
109 |
fun nth_name j = |
38996 | 110 |
case xref of |
41279 | 111 |
Facts.Fact s => backquote s ^ bracket |
38996 | 112 |
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]" |
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
113 |
| Facts.Named ((name, _), NONE) => |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
114 |
make_name reserved (length ths > 1) (j + 1) name ^ bracket |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
115 |
| Facts.Named ((name, _), SOME intervals) => |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
116 |
make_name reserved true |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
117 |
(nth (maps (explode_interval (length ths)) intervals) j) name ^ |
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
118 |
bracket |
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
119 |
in |
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset
|
120 |
(ths, (0, [])) |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset
|
121 |
|-> fold (fn th => fn (j, rest) => |
46388 | 122 |
let val name = nth_name j in |
123 |
(j + 1, ((name, stature_of_thm false [] chained_ths |
|
124 |
css_table name th), th) :: rest) |
|
125 |
end) |
|
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset
|
126 |
|> snd |
38699 | 127 |
end |
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset
|
128 |
|
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset
|
129 |
(*Reject theorems with names like "List.filter.filter_list_def" or |
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset
|
130 |
"Accessible_Part.acc.defs", as these are definitions arising from packages.*) |
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset
|
131 |
fun is_package_def a = |
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
132 |
let val names = Long_Name.explode a in |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
133 |
(length names > 2 andalso not (hd names = "local") andalso |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
134 |
String.isSuffix "_def" a) orelse String.isSuffix "_defs" a |
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset
|
135 |
end |
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset
|
136 |
|
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
137 |
(* FIXME: put other record thms here, or declare as "no_atp" *) |
44585 | 138 |
fun multi_base_blacklist ctxt ho_atp = |
41199 | 139 |
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", |
140 |
"cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", |
|
141 |
"weak_case_cong"] |
|
44585 | 142 |
|> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? |
143 |
append ["induct", "inducts"] |
|
38682 | 144 |
|> map (prefix ".") |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
145 |
|
44585 | 146 |
val max_lambda_nesting = 3 (*only applies if not ho_atp*) |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
147 |
|
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
148 |
fun term_has_too_many_lambdas max (t1 $ t2) = |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
149 |
exists (term_has_too_many_lambdas max) [t1, t2] |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
150 |
| term_has_too_many_lambdas max (Abs (_, _, t)) = |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
151 |
max = 0 orelse term_has_too_many_lambdas (max - 1) t |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
152 |
| term_has_too_many_lambdas _ _ = false |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
153 |
|
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
154 |
(* Don't count nested lambdas at the level of formulas, since they are |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
155 |
quantifiers. *) |
44585 | 156 |
fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*) |
157 |
| formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) = |
|
158 |
formula_has_too_many_lambdas false (T :: Ts) t |
|
159 |
| formula_has_too_many_lambdas _ Ts t = |
|
41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset
|
160 |
if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then |
44585 | 161 |
exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t)) |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
162 |
else |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
163 |
term_has_too_many_lambdas max_lambda_nesting t |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
164 |
|
38692 | 165 |
(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31) |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
166 |
was 11. *) |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
167 |
val max_apply_depth = 15 |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
168 |
|
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
169 |
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
170 |
| apply_depth (Abs (_, _, t)) = apply_depth t |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
171 |
| apply_depth _ = 0 |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
172 |
|
44585 | 173 |
fun is_formula_too_complex ho_atp t = |
174 |
apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t |
|
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
175 |
|
39946 | 176 |
(* FIXME: Extend to "Meson" and "Metis" *) |
37543 | 177 |
val exists_sledgehammer_const = |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
178 |
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) |
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
179 |
|
38904 | 180 |
(* FIXME: make more reliable *) |
181 |
val exists_low_level_class_const = |
|
182 |
exists_Const (fn (s, _) => |
|
47976 | 183 |
s = @{const_name equal_class.equal} orelse |
38904 | 184 |
String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) |
185 |
||
38821 | 186 |
fun is_metastrange_theorem th = |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
187 |
case head_of (concl_of th) of |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
188 |
Const (s, _) => (s <> @{const_name Trueprop} andalso |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
189 |
s <> @{const_name "=="}) |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
190 |
| _ => false |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset
|
191 |
|
38821 | 192 |
fun is_that_fact th = |
193 |
String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) |
|
194 |
andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN |
|
195 |
| _ => false) (prop_of th) |
|
196 |
||
44585 | 197 |
fun is_theorem_bad_for_atps ho_atp exporter thm = |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
198 |
is_metastrange_theorem thm orelse |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
199 |
(not exporter andalso |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
200 |
let val t = prop_of thm in |
44585 | 201 |
is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
202 |
exists_sledgehammer_const t orelse exists_low_level_class_const t orelse |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
203 |
is_that_fact thm |
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
204 |
end) |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
205 |
|
48248 | 206 |
fun string_for_term ctxt t = |
207 |
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
|
208 |
(print_mode_value ())) (Syntax.string_of_term ctxt) t |
|
209 |
|> String.translate (fn c => if Char.isPrint c then str c else "") |
|
210 |
|> simplify_spaces |
|
211 |
||
212 |
(* This is a terrible hack. Free variables are sometimes coded as "M__" when |
|
213 |
they are displayed as "M" and we want to avoid clashes with these. But |
|
214 |
sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all |
|
215 |
prefixes of all free variables. In the worse case scenario, where the fact |
|
216 |
won't be resolved correctly, the user can fix it manually, e.g., by naming |
|
217 |
the fact in question. Ideally we would need nothing of it, but backticks |
|
218 |
simply don't work with schematic variables. *) |
|
219 |
fun all_prefixes_of s = |
|
220 |
map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) |
|
221 |
||
222 |
fun close_form t = |
|
223 |
(t, [] |> Term.add_free_names t |> maps all_prefixes_of) |
|
224 |
|> fold (fn ((s, i), T) => fn (t', taken) => |
|
225 |
let val s' = singleton (Name.variant_list taken) s in |
|
226 |
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const |
|
227 |
else Logic.all_const) T |
|
228 |
$ Abs (s', T, abstract_over (Var ((s, i), T), t')), |
|
229 |
s' :: taken) |
|
230 |
end) |
|
231 |
(Term.add_vars t [] |> sort_wrt (fst o fst)) |
|
232 |
|> fst |
|
233 |
||
46734 | 234 |
fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table = |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
235 |
let |
42361 | 236 |
val thy = Proof_Context.theory_of ctxt |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39367
diff
changeset
|
237 |
val global_facts = Global_Theory.facts_of thy |
42361 | 238 |
val local_facts = Proof_Context.facts_of ctxt |
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents:
38629
diff
changeset
|
239 |
val named_locals = local_facts |> Facts.dest_static [] |
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset
|
240 |
val assms = Assumption.all_assms_of ctxt |
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents:
38699
diff
changeset
|
241 |
fun is_good_unnamed_local th = |
38820
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset
|
242 |
not (Thm.has_name_hint th) andalso |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
243 |
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals |
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents:
38629
diff
changeset
|
244 |
val unnamed_locals = |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
245 |
union Thm.eq_thm_prop (Facts.props local_facts) chained_ths |
38820
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset
|
246 |
|> filter is_good_unnamed_local |> map (pair "" o single) |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
247 |
val full_space = |
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
blanchet
parents:
38699
diff
changeset
|
248 |
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset
|
249 |
fun add_facts global foldx facts = |
38699 | 250 |
foldx (fn (name0, ths) => |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
251 |
if not exporter andalso name0 <> "" andalso |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
252 |
forall (not o member Thm.eq_thm_prop add_ths) ths andalso |
38699 | 253 |
(Facts.is_concealed facts name0 orelse |
42728
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
254 |
(not (Config.get ctxt ignore_no_atp) andalso |
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
255 |
is_package_def name0) orelse |
44cd74a419ce
added configuration options for experimental features
blanchet
parents:
42702
diff
changeset
|
256 |
exists (fn s => String.isSuffix s name0) |
46976
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46734
diff
changeset
|
257 |
(multi_base_blacklist ctxt ho_atp)) then |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
258 |
I |
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
259 |
else |
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
260 |
let |
38699 | 261 |
val multi = length ths > 1 |
41279 | 262 |
val backquote_thm = |
263 |
backquote o string_for_term ctxt o close_form o prop_of |
|
38699 | 264 |
fun check_thms a = |
42361 | 265 |
case try (Proof_Context.get_thms ctxt) a of |
38699 | 266 |
NONE => false |
42957
c693f9b7674a
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
blanchet
parents:
42952
diff
changeset
|
267 |
| SOME ths' => eq_list Thm.eq_thm_prop (ths, ths') |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
268 |
in |
38699 | 269 |
pair 1 |
43245 | 270 |
#> fold (fn th => fn (j, (multis, unis)) => |
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
271 |
(j + 1, |
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43492
diff
changeset
|
272 |
if not (member Thm.eq_thm_prop add_ths th) andalso |
44585 | 273 |
is_theorem_bad_for_atps ho_atp exporter th then |
43245 | 274 |
(multis, unis) |
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
275 |
else |
43245 | 276 |
let |
277 |
val new = |
|
278 |
(((fn () => |
|
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
279 |
if name0 = "" then |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
280 |
th |> backquote_thm |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
281 |
else |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
282 |
[Facts.extern ctxt facts name0, |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
283 |
Name_Space.extern ctxt full_space name0, |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
284 |
name0] |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
285 |
|> find_first check_thms |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
286 |
|> (fn SOME name => |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
287 |
make_name reserved multi j name |
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset
|
288 |
| NONE => "")), |
46388 | 289 |
stature_of_thm global assms chained_ths |
290 |
css_table name0 th), th) |
|
43245 | 291 |
in |
292 |
if multi then (new :: multis, unis) |
|
293 |
else (multis, new :: unis) |
|
294 |
end)) ths |
|
38699 | 295 |
#> snd |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
296 |
end) |
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents:
38629
diff
changeset
|
297 |
in |
43245 | 298 |
(* The single-name theorems go after the multiple-name ones, so that single |
299 |
names are preferred when both are available. *) |
|
300 |
([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) |
|
301 |
|> add_facts true Facts.fold_static global_facts global_facts |
|
302 |
|> op @ |
|
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
blanchet
parents:
38629
diff
changeset
|
303 |
end |
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset
|
304 |
|
48248 | 305 |
fun clasimpset_rule_table_of ctxt = |
306 |
let |
|
307 |
val thy = Proof_Context.theory_of ctxt |
|
308 |
val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy |
|
309 |
fun add stature normalizers get_th = |
|
310 |
fold (fn rule => |
|
311 |
let |
|
312 |
val th = rule |> get_th |
|
313 |
val t = |
|
314 |
th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of |
|
315 |
in |
|
316 |
fold (fn normalize => Termtab.update (normalize t, stature)) |
|
317 |
(I :: normalizers) |
|
318 |
end) |
|
319 |
val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = |
|
320 |
ctxt |> claset_of |> Classical.rep_cs |
|
321 |
val intros = Item_Net.content safeIs @ Item_Net.content hazIs |
|
322 |
(* Add once it is used: |
|
323 |
val elims = |
|
324 |
Item_Net.content safeEs @ Item_Net.content hazEs |
|
325 |
|> map Classical.classical_rule |
|
326 |
*) |
|
327 |
val simps = ctxt |> simpset_of |> dest_ss |> #simps |
|
328 |
val specs = ctxt |> Spec_Rules.get |
|
329 |
val (rec_defs, nonrec_defs) = |
|
330 |
specs |> filter (curry (op =) Spec_Rules.Equational o fst) |
|
331 |
|> maps (snd o snd) |
|
332 |
|> filter_out (member Thm.eq_thm_prop risky_defs) |
|
333 |
|> List.partition (is_rec_def o prop_of) |
|
334 |
val spec_intros = |
|
335 |
specs |> filter (member (op =) [Spec_Rules.Inductive, |
|
336 |
Spec_Rules.Co_Inductive] o fst) |
|
337 |
|> maps (snd o snd) |
|
338 |
in |
|
339 |
Termtab.empty |> add Simp [atomize] snd simps |
|
340 |
|> add Simp [] I rec_defs |
|
341 |
|> add Def [] I nonrec_defs |
|
342 |
(* Add once it is used: |
|
343 |
|> add Elim [] I elims |
|
344 |
*) |
|
345 |
|> add Intro [] I intros |
|
346 |
|> add Inductive [] I spec_intros |
|
347 |
end |
|
348 |
||
349 |
fun uniquify xs = |
|
350 |
Termtab.fold (cons o snd) |
|
351 |
(fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) [] |
|
352 |
||
353 |
fun struct_induct_rule_on th = |
|
354 |
case Logic.strip_horn (prop_of th) of |
|
355 |
(prems, @{const Trueprop} |
|
356 |
$ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => |
|
357 |
if not (is_TVar ind_T) andalso length prems > 1 andalso |
|
358 |
exists (exists_subterm (curry (op aconv) p)) prems andalso |
|
359 |
not (exists (exists_subterm (curry (op aconv) a)) prems) then |
|
360 |
SOME (p_name, ind_T) |
|
361 |
else |
|
362 |
NONE |
|
363 |
| _ => NONE |
|
364 |
||
365 |
fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x = |
|
366 |
let |
|
367 |
fun varify_noninducts (t as Free (s, T)) = |
|
368 |
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) |
|
369 |
| varify_noninducts t = t |
|
370 |
val p_inst = |
|
371 |
concl_prop |> map_aterms varify_noninducts |> close_form |
|
372 |
|> lambda (Free ind_x) |
|
373 |
|> string_for_term ctxt |
|
374 |
in |
|
375 |
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", |
|
376 |
stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)]) |
|
377 |
end |
|
378 |
||
379 |
fun type_match thy (T1, T2) = |
|
380 |
(Sign.typ_match thy (T2, T1) Vartab.empty; true) |
|
381 |
handle Type.TYPE_MATCH => false |
|
382 |
||
383 |
fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = |
|
384 |
case struct_induct_rule_on th of |
|
385 |
SOME (p_name, ind_T) => |
|
386 |
let val thy = Proof_Context.theory_of ctxt in |
|
387 |
stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) |
|
388 |
|> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax)) |
|
389 |
end |
|
390 |
| NONE => [ax] |
|
391 |
||
41199 | 392 |
fun external_frees t = |
393 |
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) |
|
394 |
||
48237 | 395 |
fun maybe_instantiate_inducts ctxt hyp_ts concl_t = |
396 |
if Config.get ctxt instantiate_inducts then |
|
397 |
let |
|
398 |
val thy = Proof_Context.theory_of ctxt |
|
399 |
val ind_stmt = |
|
400 |
(hyp_ts |> filter_out (null o external_frees), concl_t) |
|
401 |
|> Logic.list_implies |> Object_Logic.atomize_term thy |
|
402 |
val ind_stmt_xs = external_frees ind_stmt |
|
403 |
in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end |
|
404 |
else |
|
405 |
I |
|
406 |
||
407 |
fun maybe_filter_no_atps ctxt = |
|
408 |
not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) |
|
409 |
||
44585 | 410 |
fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) |
411 |
chained_ths hyp_ts concl_t = |
|
46734 | 412 |
if only andalso null add then |
413 |
[] |
|
414 |
else |
|
415 |
let |
|
416 |
val reserved = reserved_isar_keyword_table () |
|
417 |
val add_ths = Attrib.eval_thms ctxt add |
|
418 |
val css_table = clasimpset_rule_table_of ctxt |
|
419 |
in |
|
420 |
(if only then |
|
421 |
maps (map (fn ((name, stature), th) => ((K name, stature), th)) |
|
422 |
o fact_from_ref ctxt reserved chained_ths css_table) add |
|
423 |
else |
|
424 |
all_facts ctxt ho_atp reserved false add_ths chained_ths css_table) |
|
48237 | 425 |
|> maybe_instantiate_inducts ctxt hyp_ts concl_t |
426 |
|> not only ? maybe_filter_no_atps ctxt |
|
46734 | 427 |
|> uniquify |
428 |
end |
|
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43324
diff
changeset
|
429 |
|
48248 | 430 |
val relevant_facts = iterative_relevant_facts |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30364
diff
changeset
|
431 |
|
15347 | 432 |
end; |