author  blanchet 
Thu, 04 Nov 2010 14:59:44 +0100  
changeset 40369  53dca3bd4250 
parent 40251  63405dd65b0d 
child 40371  8fe3c26c49af 
permissions  rwrr 
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 

5 
Sledgehammer's 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 
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

10 
datatype locality = General  Intro  Elim  Simp  Local  Assum  Chained 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

11 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

12 
type relevance_fudge = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

13 
{worse_irrel_freq : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

14 
higher_order_irrel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

15 
abs_rel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

16 
abs_irrel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

17 
skolem_irrel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

18 
theory_const_rel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

19 
theory_const_irrel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

20 
intro_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

21 
elim_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

22 
simp_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

23 
local_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

24 
assum_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

25 
chained_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

26 
max_imperfect : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

27 
max_imperfect_exp : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

28 
threshold_divisor : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

29 
ridiculous_threshold : real} 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

30 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

31 
type relevance_override = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

32 
{add : (Facts.ref * Attrib.src list) list, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

33 
del : (Facts.ref * Attrib.src list) list, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

34 
only : bool} 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

35 

37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

36 
val trace : bool Unsynchronized.ref 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

37 
val fact_from_ref : 
38996  38 
Proof.context > unit Symtab.table > thm list 
39 
> Facts.ref * Attrib.src list > ((string * locality) * thm) list 

37347
635425a442e8
show more respect for userspecified 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

40 
val relevant_facts : 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

41 
Proof.context > bool > real * real > int > (string * typ > bool) 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

42 
> relevance_fudge > relevance_override > thm list > term list > term 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

43 
> ((string * locality) * thm) list 
15347  44 
end; 
45 

38988  46 
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = 
15347  47 
struct 
48 

38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38644
diff
changeset

49 
open Sledgehammer_Util 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38644
diff
changeset

50 

37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

51 
val trace = Unsynchronized.ref false 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

52 
fun trace_msg msg = if !trace then tracing (msg ()) else () 
35826  53 

38997  54 
(* experimental features *) 
38889  55 
val term_patterns = false 
38997  56 
val respect_no_atp = true 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

57 

38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

58 
datatype locality = General  Intro  Elim  Simp  Local  Assum  Chained 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

59 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

60 
type relevance_fudge = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

61 
{worse_irrel_freq : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

62 
higher_order_irrel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

63 
abs_rel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

64 
abs_irrel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

65 
skolem_irrel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

66 
theory_const_rel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

67 
theory_const_irrel_weight : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

68 
intro_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

69 
elim_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

70 
simp_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

71 
local_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

72 
assum_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

73 
chained_bonus : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

74 
max_imperfect : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

75 
max_imperfect_exp : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

76 
threshold_divisor : real, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

77 
ridiculous_threshold : real} 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

78 

35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

79 
type relevance_override = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

80 
{add : (Facts.ref * Attrib.src list) list, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

81 
del : (Facts.ref * Attrib.src list) list, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

82 
only : bool} 
21070  83 

37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

84 
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator 
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39718
diff
changeset

85 
val abs_name = sledgehammer_prefix ^ "abs" 
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39718
diff
changeset

86 
val skolem_prefix = sledgehammer_prefix ^ "sko" 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

87 
val theory_const_suffix = Long_Name.separator ^ " 1" 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

88 

40227
e31e3f0071d4
support nonidentifierlike fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset

89 
fun needs_quoting reserved s = 
40251
63405dd65b0d
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
blanchet
parents:
40227
diff
changeset

90 
Symtab.defined reserved s (* FIXME: orelse 
63405dd65b0d
reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong
blanchet
parents:
40227
diff
changeset

91 
exists (not o Syntax.is_identifier) (Long_Name.explode s) *) 
40227
e31e3f0071d4
support nonidentifierlike fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset

92 

38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

93 
fun repair_name reserved multi j name = 
40227
e31e3f0071d4
support nonidentifierlike fact names in Sledgehammer (e.g., "my lemma") by quoting them
blanchet
parents:
40205
diff
changeset

94 
(name > needs_quoting reserved name ? quote) ^ 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

95 
(if multi then "(" ^ Int.toString j ^ ")" else "") 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

96 

40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

97 
fun fact_from_ref ctxt reserved chained_ths (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

98 
let 
38996  99 
val ths = Attrib.eval_thms ctxt [xthm] 
100 
val bracket = 

101 
implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg) 

102 
^ "]") args) 

103 
val name = 

104 
case xref of 

39264  105 
Facts.Fact s => "`" ^ s ^ "`" ^ bracket 
38996  106 
 Facts.Named (("", _), _) => "[" ^ bracket ^ "]" 
39264  107 
 _ => Facts.string_of_ref xref ^ bracket 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

108 
val multi = length ths > 1 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

109 
in 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

110 
(ths, (1, [])) 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

111 
> fold (fn th => fn (j, rest) => 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

112 
(j + 1, ((repair_name reserved multi j name, 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

113 
if member Thm.eq_thm chained_ths th then Chained 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

114 
else General), th) :: rest)) 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

115 
> snd 
38699  116 
end 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

117 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

118 
(***************************************************************) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

119 
(* Relevance Filtering *) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

120 
(***************************************************************) 
19194  121 

24287  122 
(*** constants with types ***) 
123 

38939  124 
fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) = 
125 
order_of_type T1 (* cheat: pretend sets are firstorder *) 

126 
 order_of_type (Type (@{type_name fun}, [T1, T2])) = 

127 
Int.max (order_of_type T1 + 1, order_of_type T2) 

128 
 order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0 

129 
 order_of_type _ = 0 

130 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

131 
(* An abstraction of Isabelle types and firstorder terms *) 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

132 
datatype pattern = PVar  PApp of string * pattern list 
38939  133 
datatype ptype = PType of int * pattern list 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

134 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

135 
fun string_for_pattern PVar = "_" 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

136 
 string_for_pattern (PApp (s, ps)) = 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

137 
if null ps then s else s ^ string_for_patterns ps 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

138 
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" 
38939  139 
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps 
24287  140 

141 
(*Is the second type an instance of the first one?*) 

38824  142 
fun match_pattern (PVar, _) = true 
143 
 match_pattern (PApp _, PVar) = false 

144 
 match_pattern (PApp (s, ps), PApp (t, qs)) = 

145 
s = t andalso match_patterns (ps, qs) 

146 
and match_patterns (_, []) = true 

147 
 match_patterns ([], _) = false 

148 
 match_patterns (p :: ps, q :: qs) = 

149 
match_pattern (p, q) andalso match_patterns (ps, qs) 

38939  150 
fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs) 
24287  151 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

152 
(* Is there a unifiable constant? *) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

153 
fun pconst_mem f consts (s, ps) = 
38939  154 
exists (curry (match_ptype o f) ps) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

155 
(map snd (filter (curry (op =) s o fst) consts)) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

156 
fun pconst_hyper_mem f const_tab (s, ps) = 
38939  157 
exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s)) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

158 

38939  159 
fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts) 
160 
 pattern_for_type (TFree (s, _)) = PApp (s, []) 

161 
 pattern_for_type (TVar _) = PVar 

38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

162 

cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

163 
fun pterm thy t = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

164 
case strip_comb t of 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

165 
(Const x, ts) => PApp (pconst thy true x ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

166 
 (Free x, ts) => PApp (pconst thy false x ts) 
39367  167 
 (Var _, []) => PVar 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

168 
 _ => PApp ("?", []) (* equivalence class of higherorder constructs *) 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

169 
(* Pairs a constant with the list of its type instantiations. *) 
38939  170 
and ptype thy const x ts = 
171 
(if const then map pattern_for_type (these (try (Sign.const_typargs thy) x)) 

38828
91ad85f962c4
turn off experimental feature per default + avoid exception on "theory constant"
blanchet
parents:
38827
diff
changeset

172 
else []) @ 
38889  173 
(if term_patterns then map (pterm thy) ts else []) 
38939  174 
and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts) 
175 
and rich_ptype thy const (s, T) ts = 

176 
PType (order_of_type T, ptype thy const (s, T) ts) 

177 
and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts) 

24287  178 

38939  179 
fun string_for_hyper_pconst (s, ps) = 
180 
s ^ "{" ^ commas (map string_for_ptype ps) ^ "}" 

24287  181 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

182 
(* Add a pconstant to the table, but a [] entry means a standard 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

183 
connective, which we ignore.*) 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

184 
fun add_pconst_to_table is_built_in_const also_skolem (c, p) = 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

185 
if is_built_in_const (c, dummyT)(*###*) orelse 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

186 
(not also_skolem andalso String.isPrefix skolem_prefix c) then 
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

187 
I 
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

188 
else 
38939  189 
Symtab.map_default (c, [p]) (insert (op =) p) 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

190 

71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

191 
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) 
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

192 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

193 
fun pconsts_in_terms thy is_built_in_const also_skolems pos ts = 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

194 
let 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

195 
val flip = Option.map not 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

196 
(* We include free variables, as well as constants, to handle locales. For 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

197 
each quantifiers that must necessarily be skolemized by the ATP, we 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

198 
introduce a fresh constant to simulate the effect of Skolemization. *) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

199 
fun do_const const (s, T) ts = 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

200 
add_pconst_to_table is_built_in_const also_skolems 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

201 
(rich_pconst thy const (s, T) ts) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

202 
#> fold do_term ts 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

203 
and do_term t = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

204 
case strip_comb t of 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

205 
(Const x, ts) => do_const true x ts 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

206 
 (Free x, ts) => do_const false x ts 
38939  207 
 (Abs (_, T, t'), ts) => 
208 
(null ts 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

209 
? add_pconst_to_table is_built_in_const true 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

210 
(abs_name, PType (order_of_type T + 1, []))) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

211 
#> fold do_term (t' :: ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

212 
 (_, ts) => fold do_term ts 
38939  213 
fun do_quantifier will_surely_be_skolemized abs_T body_t = 
37537  214 
do_formula pos body_t 
38747  215 
#> (if also_skolems andalso will_surely_be_skolemized then 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

216 
add_pconst_to_table is_built_in_const true 
38939  217 
(gensym skolem_prefix, PType (order_of_type abs_T, [])) 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

218 
else 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

219 
I) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

220 
and do_term_or_formula T = 
38692  221 
if is_formula_type T then do_formula NONE else do_term 
37537  222 
and do_formula pos t = 
223 
case t of 

38939  224 
Const (@{const_name all}, _) $ Abs (_, T, t') => 
225 
do_quantifier (pos = SOME false) T t' 

37537  226 
 @{const "==>"} $ t1 $ t2 => 
227 
do_formula (flip pos) t1 #> do_formula pos t2 

228 
 Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => 

38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

229 
fold (do_term_or_formula T) [t1, t2] 
37537  230 
 @{const Trueprop} $ t1 => do_formula pos t1 
231 
 @{const Not} $ t1 => do_formula (flip pos) t1 

38939  232 
 Const (@{const_name All}, _) $ Abs (_, T, t') => 
233 
do_quantifier (pos = SOME false) T t' 

234 
 Const (@{const_name Ex}, _) $ Abs (_, T, t') => 

235 
do_quantifier (pos = SOME true) T t' 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

236 
 @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

237 
 @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

238 
 @{const HOL.implies} $ t1 $ t2 => 
37537  239 
do_formula (flip pos) t1 #> do_formula pos t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

240 
 Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 => 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

241 
fold (do_term_or_formula T) [t1, t2] 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

242 
 Const (@{const_name If}, Type (_, [_, Type (_, [T, _])])) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

243 
$ t1 $ t2 $ t3 => 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

244 
do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3] 
38939  245 
 Const (@{const_name Ex1}, _) $ Abs (_, T, t') => 
246 
do_quantifier (is_some pos) T t' 

247 
 Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') => 

248 
do_quantifier (pos = SOME false) T 

249 
(HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t')) 

250 
 Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') => 

251 
do_quantifier (pos = SOME true) T 

252 
(HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t')) 

37537  253 
 (t0 as Const (_, @{typ bool})) $ t1 => 
254 
do_term t0 #> do_formula pos t1 (* theory constant *) 

255 
 _ => do_term t 

38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

256 
in Symtab.empty > fold (do_formula pos) ts end 
24287  257 

258 
(*Inserts a dummy "constant" referring to the theory name, so that relevance 

259 
takes the given theory into account.*) 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

260 
fun theory_const_prop_of ({theory_const_rel_weight, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

261 
theory_const_irrel_weight, ...} : relevance_fudge) 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

262 
th = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

263 
if exists (curry (op <) 0.0) [theory_const_rel_weight, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

264 
theory_const_irrel_weight] then 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

265 
let 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

266 
val name = Context.theory_name (theory_of_thm th) 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

267 
val t = Const (name ^ theory_const_suffix, @{typ bool}) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

268 
in t $ prop_of th end 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

269 
else 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

270 
prop_of th 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

271 

24287  272 
(**** Constant / Type Frequencies ****) 
273 

38743  274 
(* A twodimensional symbol table counts frequencies of constants. It's keyed 
275 
first by constant name and second by its list of type instantiations. For the 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

276 
latter, we need a linear ordering on "pattern list". *) 
24287  277 

38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

278 
fun pattern_ord p = 
38743  279 
case p of 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

280 
(PVar, PVar) => EQUAL 
38823
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

281 
 (PVar, PApp _) => LESS 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

282 
 (PApp _, PVar) => GREATER 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

283 
 (PApp q1, PApp q2) => 
828e68441a2f
renaming + treat "TFree" better in "pattern_for_type"
blanchet
parents:
38822
diff
changeset

284 
prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) 
38939  285 
fun ptype_ord (PType p, PType q) = 
286 
prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q) 

24287  287 

38939  288 
structure PType_Tab = Table(type key = ptype val ord = ptype_ord) 
24287  289 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

290 
fun count_fact_consts thy fudge = 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

291 
let 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

292 
fun do_const const (s, T) ts = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

293 
(* Twodimensional table update. Constant maps to types maps to count. *) 
38939  294 
PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1) 
295 
> Symtab.map_default (s, PType_Tab.empty) 

38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

296 
#> fold do_term ts 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

297 
and do_term t = 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

298 
case strip_comb t of 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

299 
(Const x, ts) => do_const true x ts 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

300 
 (Free x, ts) => do_const false x ts 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

301 
 (Abs (_, _, t'), ts) => fold do_term (t' :: ts) 
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

302 
 (_, ts) => fold do_term ts 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

303 
in do_term o theory_const_prop_of fudge o snd end 
24287  304 

305 

306 
(**** Actual Filtering Code ****) 

307 

39367  308 
fun pow_int _ 0 = 1.0 
38939  309 
 pow_int x 1 = x 
310 
 pow_int x n = if n > 0 then x * pow_int x (n  1) else pow_int x (n + 1) / x 

311 

24287  312 
(*The frequency of a constant is the sum of those of all instances of its type.*) 
38824  313 
fun pconst_freq match const_tab (c, ps) = 
38939  314 
PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m) 
315 
(the (Symtab.lookup const_tab c)) 0 

38686  316 

24287  317 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

318 
(* A surprising number of theorems contain only a few significant constants. 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

319 
These include all induction rules, and other general theorems. *) 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

320 

c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

321 
(* "log" seems best in practice. A constant function of one ignores the constant 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

322 
frequencies. Rare constants give more points if they are relevant than less 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

323 
rare ones. *) 
39367  324 
fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0) 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

325 

2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

326 
(* Irrelevant constants are treated differently. We associate lower penalties to 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

327 
very rare constants and very common ones  the former because they can't 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

328 
lead to the inclusion of too many new facts, and the latter because they are 
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

329 
so common as to be of little interest. *) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

330 
fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...} 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

331 
: relevance_fudge) order freq = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

332 
let val (k, x) = worse_irrel_freq > `Real.ceil in 
38939  333 
(if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x 
334 
else rel_weight_for order freq / rel_weight_for order k) 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

335 
* pow_int higher_order_irrel_weight (order  1) 
38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

336 
end 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

337 

c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

338 
(* Computes a constant's weight, as determined by its frequency. *) 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

339 
fun generic_pconst_weight abs_weight skolem_weight theory_const_weight 
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

340 
weight_for f const_tab (c as (s, PType (m, _))) = 
38816  341 
if s = abs_name then abs_weight 
342 
else if String.isPrefix skolem_prefix s then skolem_weight 

38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

343 
else if String.isSuffix theory_const_suffix s then theory_const_weight 
38939  344 
else weight_for m (pconst_freq (match_ptype o f) const_tab c) 
38821  345 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

346 
fun rel_pconst_weight ({abs_rel_weight, theory_const_rel_weight, ...} 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

347 
: relevance_fudge) const_tab = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

348 
generic_pconst_weight abs_rel_weight 0.0 theory_const_rel_weight 
38992
542474156c66
introduce fudge factors to deal with "theory const"
blanchet
parents:
38988
diff
changeset

349 
rel_weight_for I const_tab 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

350 
fun irrel_pconst_weight (fudge as {abs_irrel_weight, skolem_irrel_weight, 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

351 
theory_const_irrel_weight, ...}) const_tab = 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

352 
generic_pconst_weight abs_irrel_weight skolem_irrel_weight 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

353 
theory_const_irrel_weight (irrel_weight_for fudge) swap 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

354 
const_tab 
24287  355 

40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

356 
fun locality_bonus (_ : relevance_fudge) General = 0.0 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

357 
 locality_bonus {intro_bonus, ...} Intro = intro_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

358 
 locality_bonus {elim_bonus, ...} Elim = elim_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

359 
 locality_bonus {simp_bonus, ...} Simp = simp_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

360 
 locality_bonus {local_bonus, ...} Local = local_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

361 
 locality_bonus {assum_bonus, ...} Assum = assum_bonus 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

362 
 locality_bonus {chained_bonus, ...} Chained = chained_bonus 
38751
01c4d14b2a61
add a bonus for chained facts, since they are likely to be relevant;
blanchet
parents:
38749
diff
changeset

363 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

364 
fun fact_weight fudge loc const_tab relevant_consts fact_consts = 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

365 
case fact_consts > List.partition (pconst_hyper_mem I relevant_consts) 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

366 
> filter_out (pconst_hyper_mem swap relevant_consts) of 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

367 
([], _) => 0.0 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

368 
 (rel, irrel) => 
38889  369 
let 
370 
val irrel = irrel > filter_out (pconst_mem swap rel) 

38938
2b93dbc07778
improve weighting of irrelevant constants, based on Mirabelle experiments
blanchet
parents:
38937
diff
changeset

371 
val rel_weight = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

372 
0.0 > fold (curry (op +) o rel_pconst_weight fudge const_tab) rel 
38889  373 
val irrel_weight = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

374 
~ (locality_bonus fudge loc) 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

375 
> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel 
38889  376 
val res = rel_weight / (rel_weight + irrel_weight) 
377 
in if Real.isFinite res then res else 0.0 end 

38747  378 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

379 
fun pconsts_in_fact thy is_built_in_const t = 
38825  380 
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

381 
(pconsts_in_terms thy is_built_in_const true (SOME true) [t]) [] 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

382 
fun pair_consts_fact thy is_built_in_const fudge fact = 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

383 
case fact > snd > theory_const_prop_of fudge 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

384 
> pconsts_in_fact thy is_built_in_const of 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

385 
[] => NONE 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

386 
 consts => SOME ((fact, consts), NONE) 
24287  387 

38699  388 
type annotated_thm = 
38939  389 
(((unit > string) * locality) * thm) * (string * ptype) list 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

390 

38904  391 
fun take_most_relevant max_relevant remaining_max 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

392 
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) 
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

393 
(candidates : (annotated_thm * real) list) = 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

394 
let 
38747  395 
val max_imperfect = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

396 
Real.ceil (Math.pow (max_imperfect, 
38904  397 
Math.pow (Real.fromInt remaining_max 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

398 
/ Real.fromInt max_relevant, max_imperfect_exp))) 
38747  399 
val (perfect, imperfect) = 
38889  400 
candidates > sort (Real.compare o swap o pairself snd) 
401 
> take_prefix (fn (_, w) => w > 0.99999) 

38747  402 
val ((accepts, more_rejects), rejects) = 
403 
chop max_imperfect imperfect >> append perfect >> chop remaining_max 

38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

404 
in 
38889  405 
trace_msg (fn () => 
406 
"Actually passed (" ^ Int.toString (length accepts) ^ " of " ^ 

407 
Int.toString (length candidates) ^ "): " ^ 

408 
(accepts > map (fn ((((name, _), _), _), weight) => 

38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

409 
name () ^ " [" ^ Real.toString weight ^ "]") 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

410 
> commas)); 
38747  411 
(accepts, more_rejects @ rejects) 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

412 
end 
24287  413 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

414 
fun if_empty_replace_with_locality thy is_built_in_const facts loc tab = 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

415 
if Symtab.is_empty tab then 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

416 
pconsts_in_terms thy is_built_in_const false (SOME false) 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

417 
(map_filter (fn ((_, loc'), th) => 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

418 
if loc' = loc then SOME (prop_of th) else NONE) facts) 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

419 
else 
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

420 
tab 
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

421 

40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

422 
fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

423 
(fudge as {threshold_divisor, ridiculous_threshold, ...}) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

424 
({add, del, ...} : relevance_override) facts goal_ts = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

425 
let 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

426 
val thy = ProofContext.theory_of ctxt 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

427 
val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty 
38819
71c9f61516cd
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
blanchet
parents:
38818
diff
changeset

428 
val goal_const_tab = 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

429 
pconsts_in_terms thy is_built_in_const false (SOME false) goal_ts 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

430 
> fold (if_empty_replace_with_locality thy is_built_in_const facts) 
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

431 
[Chained, Assum, Local] 
39012  432 
val add_ths = Attrib.eval_thms ctxt add 
433 
val del_ths = Attrib.eval_thms ctxt del 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

434 
val facts = facts > filter_out (member Thm.eq_thm del_ths o snd) 
38747  435 
fun iter j remaining_max threshold rel_const_tab hopeless hopeful = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

436 
let 
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset

437 
fun relevant [] _ [] = 
38747  438 
(* Nothing has been added this iteration. *) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

439 
if j = 0 andalso threshold >= ridiculous_threshold then 
38747  440 
(* First iteration? Try again. *) 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

441 
iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab 
38747  442 
hopeless hopeful 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

443 
else 
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset

444 
[] 
38889  445 
 relevant candidates rejects [] = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

446 
let 
38747  447 
val (accepts, more_rejects) = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

448 
take_most_relevant max_relevant remaining_max fudge candidates 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

449 
val rel_const_tab' = 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

450 
rel_const_tab 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

451 
> fold (add_pconst_to_table is_built_in_const false) 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

452 
(maps (snd o fst) accepts) 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

453 
fun is_dirty (c, _) = 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

454 
Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

455 
val (hopeful_rejects, hopeless_rejects) = 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

456 
(rejects @ hopeless, ([], [])) 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

457 
> fold (fn (ax as (_, consts), old_weight) => 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

458 
if exists is_dirty consts then 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

459 
apfst (cons (ax, NONE)) 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

460 
else 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

461 
apsnd (cons (ax, old_weight))) 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

462 
>> append (more_rejects 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

463 
> map (fn (ax as (_, consts), old_weight) => 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

464 
(ax, if exists is_dirty consts then NONE 
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

465 
else SOME old_weight))) 
38747  466 
val threshold = 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

467 
1.0  (1.0  threshold) 
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

468 
* Math.pow (decay, Real.fromInt (length accepts)) 
38747  469 
val remaining_max = remaining_max  length accepts 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

470 
in 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

471 
trace_msg (fn () => "New or updated constants: " ^ 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

472 
commas (rel_const_tab' > Symtab.dest 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

473 
> subtract (op =) (rel_const_tab > Symtab.dest) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

474 
> map string_for_hyper_pconst)); 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

475 
map (fst o fst) accepts @ 
38747  476 
(if remaining_max = 0 then 
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset

477 
[] 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

478 
else 
38747  479 
iter (j + 1) remaining_max threshold rel_const_tab' 
480 
hopeless_rejects hopeful_rejects) 

38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

481 
end 
38889  482 
 relevant candidates rejects 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

483 
(((ax as (((_, loc), _), fact_consts)), cached_weight) 
38747  484 
:: hopeful) = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

485 
let 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

486 
val weight = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

487 
case cached_weight of 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

488 
SOME w => w 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

489 
 NONE => fact_weight fudge loc const_tab rel_const_tab 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

490 
fact_consts 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

491 
in 
38741  492 
if weight >= threshold then 
38889  493 
relevant ((ax, weight) :: candidates) rejects hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

494 
else 
38889  495 
relevant candidates ((ax, weight) :: rejects) hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

496 
end 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

497 
in 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

498 
trace_msg (fn () => 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

499 
"ITERATION " ^ string_of_int j ^ ": current threshold: " ^ 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

500 
Real.toString threshold ^ ", constants: " ^ 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

501 
commas (rel_const_tab > Symtab.dest 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

502 
> filter (curry (op <>) [] o snd) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

503 
> map string_for_hyper_pconst)); 
38889  504 
relevant [] [] hopeful 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

505 
end 
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset

506 
fun add_add_ths accepts = 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

507 
(facts > filter ((member Thm.eq_thm add_ths 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

508 
andf (not o member (Thm.eq_thm o apsnd snd) accepts)) 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

509 
o snd)) 
40191
257d2e06bfb8
put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away
blanchet
parents:
40071
diff
changeset

510 
@ accepts 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

511 
in 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

512 
facts > map_filter (pair_consts_fact thy is_built_in_const fudge) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

513 
> iter 0 max_relevant threshold0 goal_const_tab [] 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

514 
> not (null add_ths) ? add_add_ths 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

515 
> tap (fn res => trace_msg (fn () => 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

516 
"Total relevant: " ^ Int.toString (length res))) 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

517 
end 
24287  518 

38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

519 

24287  520 
(***************************************************************) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

521 
(* Retrieving and filtering lemmas *) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

522 
(***************************************************************) 
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

523 

33022
c95102496490
Removal of the unused atpset concept, the atp attribute and some related code.
paulson
parents:
32994
diff
changeset

524 
(*** retrieve lemmas and filter them ***) 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

525 

20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

526 
(*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

527 
"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

528 
fun is_package_def a = 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

529 
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

530 
(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

531 
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

532 
end 
20757
fe84fe0dfd30
Definitions produced by packages are now blacklisted.
paulson
parents:
20661
diff
changeset

533 

38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

534 
fun mk_fact_table f xs = 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

535 
fold (Termtab.update o `(prop_of o f)) xs Termtab.empty 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

536 
fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table snd xs) [] 
19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

537 

37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

538 
(* FIXME: put other record thms here, or declare as "no_atp" *) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

539 
val multi_base_blacklist = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

540 
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", 
38682  541 
"split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", 
542 
"case_cong", "weak_case_cong"] 

543 
> map (prefix ".") 

37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

544 

1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

545 
val max_lambda_nesting = 3 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

546 

1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

547 
fun term_has_too_many_lambdas max (t1 $ t2) = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

548 
exists (term_has_too_many_lambdas max) [t1, t2] 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

549 
 term_has_too_many_lambdas max (Abs (_, _, t)) = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

550 
max = 0 orelse term_has_too_many_lambdas (max  1) t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

551 
 term_has_too_many_lambdas _ _ = false 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

552 

1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

553 
(* 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

554 
quantifiers. *) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

555 
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

556 
formula_has_too_many_lambdas (T :: Ts) t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

557 
 formula_has_too_many_lambdas Ts t = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

558 
if is_formula_type (fastype_of1 (Ts, t)) then 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

559 
exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

560 
else 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

561 
term_has_too_many_lambdas max_lambda_nesting t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

562 

38692  563 
(* The max apply depth of any "metis" call in "Metis_Examples" (on 20071031) 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

564 
was 11. *) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

565 
val max_apply_depth = 15 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

566 

1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

567 
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

568 
 apply_depth (Abs (_, _, t)) = apply_depth t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

569 
 apply_depth _ = 0 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

570 

1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

571 
fun is_formula_too_complex t = 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

572 
apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

573 

39946  574 
(* FIXME: Extend to "Meson" and "Metis" *) 
37543  575 
val exists_sledgehammer_const = 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

576 
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

577 

38904  578 
(* FIXME: make more reliable *) 
579 
val exists_low_level_class_const = 

580 
exists_Const (fn (s, _) => 

581 
String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) 

582 

38821  583 
fun is_metastrange_theorem th = 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

584 
case head_of (concl_of th) of 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

585 
Const (a, _) => (a <> @{const_name Trueprop} andalso 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

586 
a <> @{const_name "=="}) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

587 
 _ => false 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

588 

38821  589 
fun is_that_fact th = 
590 
String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) 

591 
andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN 

592 
 _ => false) (prop_of th) 

593 

37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

594 
val type_has_top_sort = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

595 
exists_subtype (fn TFree (_, []) => true  TVar (_, []) => true  _ => false) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

596 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

597 
(**** Predicates to detect unwanted facts (prolific or likely to cause 
37347
635425a442e8
show more respect for userspecified 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

598 
unsoundness) ****) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

599 

38289
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

600 
(* Too general means, positive equality literal with a variable X as one 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

601 
operand, when X does not occur properly in the other operand. This rules out 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

602 
clearly inconsistent facts such as X = a  X = b, though it by no means 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

603 
guarantees soundness. *) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

604 

38289
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

605 
(* Unwanted equalities are those between a (bound or schematic) variable that 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

606 
does not properly occur in the second operand. *) 
38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

607 
val is_exhaustive_finite = 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

608 
let 
38629  609 
fun is_bad_equal (Var z) t = 
610 
not (exists_subterm (fn Var z' => z = z'  _ => false) t) 

611 
 is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) 

612 
 is_bad_equal _ _ = false 

613 
fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 

38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

614 
fun do_formula pos t = 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

615 
case (pos, t) of 
38615
4e1d828ee514
improve "x = A  x = B  x = C"style axiom detection
blanchet
parents:
38611
diff
changeset

616 
(_, @{const Trueprop} $ t1) => do_formula pos t1 
38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

617 
 (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

618 
do_formula pos t' 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

619 
 (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

620 
do_formula pos t' 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

621 
 (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

622 
do_formula pos t' 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

623 
 (_, @{const "==>"} $ t1 $ t2) => 
38629  624 
do_formula (not pos) t1 andalso 
625 
(t2 = @{prop False} orelse do_formula pos t2) 

38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

626 
 (_, @{const HOL.implies} $ t1 $ t2) => 
38629  627 
do_formula (not pos) t1 andalso 
628 
(t2 = @{const False} orelse do_formula pos t2) 

38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

629 
 (_, @{const Not} $ t1) => do_formula (not pos) t1 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

630 
 (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

631 
 (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

632 
 (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2 
38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

633 
 (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

634 
 _ => false 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

635 
in do_formula true end 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

636 

38592
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

637 
fun has_bound_or_var_of_type tycons = 
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

638 
exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s 
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

639 
 Abs (_, Type (s, _), _) => member (op =) tycons s 
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

640 
 _ => false) 
21431
ef9080e7dbbc
Outputs a minimal number of arity clauses. Tidying of blacklist, fixing the blacklisting of thm lists
paulson
parents:
21397
diff
changeset

641 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

642 
(* Facts are forbidden to contain variables of these types. The typical reason 
37347
635425a442e8
show more respect for userspecified 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

643 
is that they lead to unsoundness. Note that "unit" satisfies numerous 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

644 
equations like "?x = ()". The resulting clauses will have no type constraint, 
37347
635425a442e8
show more respect for userspecified 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

645 
yielding false proofs. Even "bool" leads to many unsound proofs, though only 
635425a442e8
show more respect for userspecified 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

646 
for higherorder problems. *) 
38592
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

647 
val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}]; 
22217
a5d983f7113f
Tidying; more debugging information. New reference unwanted_types.
paulson
parents:
22193
diff
changeset

648 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

649 
(* Facts containing variables of type "unit" or "bool" or of the form 
38290
581a402a80f0
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents:
38289
diff
changeset

650 
"ALL x. x = A  x = B  x = C" are likely to lead to unsound proofs if types 
581a402a80f0
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
blanchet
parents:
38289
diff
changeset

651 
are omitted. *) 
38593  652 
fun is_dangerous_term full_types t = 
38609  653 
not full_types andalso 
38679
2cfd0777580f
destroy elim rules before checking for finite exhaustive facts
blanchet
parents:
38652
diff
changeset

654 
let val t = transform_elim_term t in 
2cfd0777580f
destroy elim rules before checking for finite exhaustive facts
blanchet
parents:
38652
diff
changeset

655 
has_bound_or_var_of_type dangerous_types t orelse 
2cfd0777580f
destroy elim rules before checking for finite exhaustive facts
blanchet
parents:
38652
diff
changeset

656 
is_exhaustive_finite t 
2cfd0777580f
destroy elim rules before checking for finite exhaustive facts
blanchet
parents:
38652
diff
changeset

657 
end 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

658 

38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

659 
fun is_theorem_bad_for_atps full_types thm = 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

660 
let val t = prop_of thm in 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

661 
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

662 
is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse 
38904  663 
exists_low_level_class_const t orelse is_metastrange_theorem thm orelse 
664 
is_that_fact thm 

38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

665 
end 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

666 

38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

667 
fun clasimpset_rules_of ctxt = 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

668 
let 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

669 
val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt > claset_of > rep_cs 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

670 
val intros = safeIs @ hazIs 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

671 
val elims = map Classical.classical_rule (safeEs @ hazEs) 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

672 
val simps = ctxt > simpset_of > dest_ss > #simps > map snd 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

673 
in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

674 

39265
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

675 
fun all_prefixes_of s = 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

676 
map (fn i => String.extract (s, 0, SOME i)) (1 upto size s  1) 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

677 

c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

678 
(* This is a terrible hack. Free variables are sometimes code as "M__" when they 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

679 
are displayed as "M" and we want to avoid clashes with these. But sometimes 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

680 
it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

681 
free variables. In the worse case scenario, where the fact won't be resolved 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

682 
correctly, the user can fix it manually, e.g., by naming the fact in 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

683 
question. Ideally we would need nothing of it, but backticks just don't work 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

684 
with schematic variables. *) 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

685 
fun close_form t = 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

686 
(t, [] > Term.add_free_names t > maps all_prefixes_of) 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

687 
> fold (fn ((s, i), T) => fn (t', taken) => 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

688 
let val s' = Name.variant taken s in 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

689 
(Term.all T $ Abs (s', T, abstract_over (Var ((s, i), T), t')), 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

690 
s' :: taken) 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

691 
end) 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

692 
(Term.add_vars t [] > sort_wrt (fst o fst)) 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

693 
> fst 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

694 

40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

695 
fun all_facts ctxt reserved full_types 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

696 
({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

697 
add_ths chained_ths = 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

698 
let 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

699 
val thy = ProofContext.theory_of ctxt 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39367
diff
changeset

700 
val global_facts = Global_Theory.facts_of thy 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

701 
val local_facts = ProofContext.facts_of ctxt 
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

702 
val named_locals = local_facts > Facts.dest_static [] 
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

703 
val assms = Assumption.all_assms_of ctxt 
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

704 
fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

705 
val is_chained = member Thm.eq_thm chained_ths 
38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

706 
val (intros, elims, simps) = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

707 
if exists (curry (op <) 0.0) [intro_bonus, elim_bonus, simp_bonus] then 
38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

708 
clasimpset_rules_of ctxt 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

709 
else 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

710 
(Termtab.empty, Termtab.empty, Termtab.empty) 
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

711 
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

712 
not (Thm.has_name_hint th) andalso 
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

713 
forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

714 
val unnamed_locals = 
38820
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset

715 
union Thm.eq_thm (Facts.props local_facts) chained_ths 
d0f98bd81a85
add nameless chained facts to the pool of things known to Sledgehammer
blanchet
parents:
38819
diff
changeset

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

717 
val full_space = 
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

718 
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

719 
fun add_facts global foldx facts = 
38699  720 
foldx (fn (name0, ths) => 
721 
if name0 <> "" andalso 

39012  722 
forall (not o member Thm.eq_thm add_ths) ths andalso 
38699  723 
(Facts.is_concealed facts name0 orelse 
724 
(respect_no_atp andalso is_package_def name0) orelse 

725 
exists (fn s => String.isSuffix s name0) multi_base_blacklist orelse 

726 
String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then 

38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

727 
I 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

728 
else 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

729 
let 
38699  730 
val multi = length ths > 1 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

731 
fun backquotify th = 
39718  732 
"`" ^ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) 
39265
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

733 
(print_mode_value ())) 
c09c150f6af7
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
blanchet
parents:
39264
diff
changeset

734 
(Syntax.string_of_term ctxt) (close_form (prop_of th)) ^ "`" 
38738
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

735 
> String.translate (fn c => if Char.isPrint c then str c else "") 
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

736 
> simplify_spaces 
38699  737 
fun check_thms a = 
738 
case try (ProofContext.get_thms ctxt) a of 

739 
NONE => false 

740 
 SOME ths' => Thm.eq_thms (ths, ths') 

38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

741 
in 
38699  742 
pair 1 
743 
#> fold (fn th => fn (j, rest) => 

744 
(j + 1, 

745 
if is_theorem_bad_for_atps full_types th andalso 

39012  746 
not (member Thm.eq_thm add_ths th) then 
38699  747 
rest 
748 
else 

38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

749 
(((fn () => 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

750 
if name0 = "" then 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

751 
th > backquotify 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

752 
else 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

753 
let 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

754 
val name1 = Facts.extern facts name0 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

755 
val name2 = Name_Space.extern full_space name0 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

756 
in 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

757 
case find_first check_thms [name1, name2, name0] of 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

758 
SOME name => repair_name reserved multi j name 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

759 
 NONE => "" 
38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

760 
end), 
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

761 
let val t = prop_of th in 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

762 
if is_chained th then 
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

763 
Chained 
38993
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

764 
else if global then 
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

765 
if Termtab.defined intros t then Intro 
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

766 
else if Termtab.defined elims t then Elim 
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

767 
else if Termtab.defined simps t then Simp 
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

768 
else General 
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

769 
else 
504b9e1efd33
give priority to assumptions in structured proofs
blanchet
parents:
38992
diff
changeset

770 
if is_assum th then Assum else Local 
38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

771 
end), 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

772 
(multi, th)) :: rest)) ths 
38699  773 
#> snd 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

774 
end) 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

775 
in 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

776 
[] > add_facts false fold local_facts (unnamed_locals @ named_locals) 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

777 
> add_facts true Facts.fold_static global_facts global_facts 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

778 
end 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

779 

760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

780 
(* The singlename theorems go after the multiplename ones, so that single 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

781 
names are preferred when both are available. *) 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

782 
fun rearrange_facts ctxt respect_no_atp = 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

783 
List.partition (fst o snd) #> op @ #> map (apsnd snd) 
38699  784 
#> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

785 

760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

786 
(***************************************************************) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

787 
(* ATP invocation methods setup *) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

788 
(***************************************************************) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

789 

40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

790 
fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

791 
is_built_in_const fudge (override as {add, only, ...}) 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

792 
chained_ths hyp_ts concl_t = 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

793 
let 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

794 
val decay = Math.pow ((1.0  threshold1) / (1.0  threshold0), 
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

795 
1.0 / Real.fromInt (max_relevant + 1)) 
39012  796 
val add_ths = Attrib.eval_thms ctxt add 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

797 
val reserved = reserved_isar_keyword_table () 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

798 
val facts = 
38699  799 
(if only then 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

800 
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th))) 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

801 
o fact_from_ref ctxt reserved chained_ths) add 
38699  802 
else 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

803 
all_facts ctxt reserved full_types fudge add_ths chained_ths) 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

804 
> rearrange_facts ctxt (respect_no_atp andalso not only) 
38937
1b1a2f5ccd7d
take into consideration whether a fact is an "intro"/"elim"/"simp" rule as an additional factor influencing the relevance filter
blanchet
parents:
38907
diff
changeset

805 
> uniquify 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

806 
in 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

807 
trace_msg (fn () => "Considering " ^ Int.toString (length facts) ^ 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

808 
" facts"); 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset

809 
(if only orelse threshold1 < 0.0 then 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

810 
facts 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset

811 
else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse 
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39265
diff
changeset

812 
max_relevant = 0 then 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

813 
[] 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

814 
else 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40251
diff
changeset

815 
relevance_filter ctxt threshold0 decay max_relevant is_built_in_const 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40191
diff
changeset

816 
fudge override facts (concl_t :: hyp_ts)) 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

817 
> map (apfst (apfst (fn f => f ()))) 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

818 
end 
30536
07b4f050e4df
split relevancefilter and writing of problemfiles;
immler@in.tum.de
parents:
30364
diff
changeset

819 

15347  820 
end; 