author  blanchet 
Tue, 03 May 2011 00:10:22 +0200  
changeset 42646  4781fcd53572 
parent 42641  2cd4e6463842 
child 42671  390de893659a 
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 = 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41158
diff
changeset

13 
{allow_ext : bool, 
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

14 
local_const_multiplier : real, 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41158
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

32 

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

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

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

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

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

37 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

38 
val trace : bool Config.T 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

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

40 
val fact_from_ref : 
38996  41 
Proof.context > unit Symtab.table > thm list 
42 
> Facts.ref * Attrib.src list > ((string * locality) * thm) list 

41767
44b2a0385001
export useful function (needed in a Sledgehammerrelated experiment)
blanchet
parents:
41491
diff
changeset

43 
val all_facts : 
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

44 
Proof.context > 'a Symtab.table > bool > thm list > thm list 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

45 
> (((unit > string) * locality) * (bool * thm)) list 
41768
dd2125fb75f9
export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents:
41767
diff
changeset

46 
val const_names_in_fact : 
dd2125fb75f9
export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents:
41767
diff
changeset

47 
theory > (string * typ > term list > bool * term list) > term 
dd2125fb75f9
export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents:
41767
diff
changeset

48 
> string list 
42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

49 
val is_dangerous_term : term > bool 
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

50 
val relevant_facts : 
42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

51 
Proof.context > real * real > int 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

52 
> (string * typ > term list > bool * term list) > relevance_fudge 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

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

54 
> ((string * locality) * thm) list 
15347  55 
end; 
56 

38988  57 
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = 
15347  58 
struct 
59 

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

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

61 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

62 
val trace = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

63 
Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false) 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

64 
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () 
35826  65 

41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset

66 
(* experimental features *) 
38997  67 
val respect_no_atp = true 
41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset

68 
val instantiate_inducts = false 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

69 

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

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

71 

42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

72 
(* (quasi)underapproximation of the truth *) 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

73 
fun is_global_locality Local = false 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

74 
 is_global_locality Assum = false 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

75 
 is_global_locality Chained = false 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

76 
 is_global_locality _ = true 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

77 

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

78 
type relevance_fudge = 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41158
diff
changeset

79 
{allow_ext : bool, 
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

80 
local_const_multiplier : real, 
41159
1e12d6495423
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
blanchet
parents:
41158
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

98 

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

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

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

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

102 
only : bool} 
21070  103 

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

104 
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

105 
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

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

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

108 

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

109 
fun needs_quoting reserved s = 
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

110 
Symtab.defined reserved s orelse 
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
41999
diff
changeset

111 
exists (not o Lexicon.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

112 

40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

113 
fun make_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

114 
(name > needs_quoting reserved name ? quote) ^ 
41491  115 
(if multi then "(" ^ string_of_int j ^ ")" else "") 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38743
diff
changeset

116 

40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

117 
fun explode_interval _ (Facts.FromTo (i, j)) = i upto j 
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

118 
 explode_interval max (Facts.From i) = i upto i + max  1 
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

119 
 explode_interval _ (Facts.Single i) = [i] 
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

120 

41279  121 
val backquote = 
122 
raw_explode #> map (fn "`" => "\\`"  s => s) #> implode #> enclose "`" "`" 

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

123 
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

124 
let 
38996  125 
val ths = Attrib.eval_thms ctxt [xthm] 
126 
val bracket = 

41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41989
diff
changeset

127 
map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args 
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41989
diff
changeset

128 
> implode 
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

129 
fun nth_name j = 
38996  130 
case xref of 
41279  131 
Facts.Fact s => backquote s ^ bracket 
38996  132 
 Facts.Named (("", _), _) => "[" ^ bracket ^ "]" 
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

133 
 Facts.Named ((name, _), NONE) => 
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

134 
make_name reserved (length ths > 1) (j + 1) name ^ bracket 
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

135 
 Facts.Named ((name, _), SOME intervals) => 
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

136 
make_name reserved true 
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

137 
(nth (maps (explode_interval (length ths)) intervals) j) name ^ 
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

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

139 
in 
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

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

141 
> fold (fn th => fn (j, rest) => 
40375
db690d38e4b9
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet
parents:
40373
diff
changeset

142 
(j + 1, ((nth_name j, 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

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

144 
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

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

147 

41199  148 
(* This is a terrible hack. Free variables are sometimes code as "M__" when they 
149 
are displayed as "M" and we want to avoid clashes with these. But sometimes 

150 
it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all 

151 
free variables. In the worse case scenario, where the fact won't be resolved 

152 
correctly, the user can fix it manually, e.g., by naming the fact in 

153 
question. Ideally we would need nothing of it, but backticks just don't work 

154 
with schematic variables. *) 

155 
fun all_prefixes_of s = 

156 
map (fn i => String.extract (s, 0, SOME i)) (1 upto size s  1) 

157 
fun close_form t = 

158 
(t, [] > Term.add_free_names t > maps all_prefixes_of) 

159 
> fold (fn ((s, i), T) => fn (t', taken) => 

160 
let val s' = Name.variant taken s in 

161 
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const 

162 
else Term.all) T 

163 
$ Abs (s', T, abstract_over (Var ((s, i), T), t')), 

164 
s' :: taken) 

165 
end) 

166 
(Term.add_vars t [] > sort_wrt (fst o fst)) 

167 
> fst 

168 

169 
fun string_for_term ctxt t = 

170 
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) 

171 
(print_mode_value ())) (Syntax.string_of_term ctxt) t 

172 
> String.translate (fn c => if Char.isPrint c then str c else "") 

173 
> simplify_spaces 

174 

175 
(** Structural induction rules **) 

176 

41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

177 
fun struct_induct_rule_on th = 
41199  178 
case Logic.strip_horn (prop_of th) of 
179 
(prems, @{const Trueprop} 

180 
$ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => 

181 
if not (is_TVar ind_T) andalso length prems > 1 andalso 

182 
exists (exists_subterm (curry (op aconv) p)) prems andalso 

183 
not (exists (exists_subterm (curry (op aconv) a)) prems) then 

184 
SOME (p_name, ind_T) 

185 
else 

186 
NONE 

187 
 _ => NONE 

188 

41207  189 
fun instantiate_induct_rule ctxt concl_prop p_name ((name, loc), (multi, th)) 
41199  190 
ind_x = 
191 
let 

192 
fun varify_noninducts (t as Free (s, T)) = 

193 
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) 

194 
 varify_noninducts t = t 

195 
val p_inst = 

196 
concl_prop > map_aterms varify_noninducts > close_form 

197 
> lambda (Free ind_x) 

198 
> string_for_term ctxt 

199 
in 

41207  200 
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", loc), 
41199  201 
(multi, th > read_instantiate ctxt [((p_name, 0), p_inst)])) 
202 
end 

203 

204 
fun type_match thy (T1, T2) = 

205 
(Sign.typ_match thy (T2, T1) Vartab.empty; true) 

206 
handle Type.TYPE_MATCH => false 

207 

208 
fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, (_, th))) = 

41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

209 
case struct_induct_rule_on th of 
41199  210 
SOME (p_name, ind_T) => 
42361  211 
let val thy = Proof_Context.theory_of ctxt in 
41199  212 
stmt_xs > filter (fn (_, T) => type_match thy (T, ind_T)) 
213 
> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax)) 

214 
end 

215 
 NONE => [ax] 

216 

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

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

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

219 
(***************************************************************) 
19194  220 

24287  221 
(*** constants with types ***) 
222 

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

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

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

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

228 
 order_of_type _ = 0 

229 

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

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

231 
datatype pattern = PVar  PApp of string * pattern list 
38939  232 
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

233 

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

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

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

236 
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

237 
and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" 
38939  238 
fun string_for_ptype (PType (_, ps)) = string_for_patterns ps 
24287  239 

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

38824  241 
fun match_pattern (PVar, _) = true 
242 
 match_pattern (PApp _, PVar) = false 

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

244 
s = t andalso match_patterns (ps, qs) 

245 
and match_patterns (_, []) = true 

246 
 match_patterns ([], _) = false 

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

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

38939  249 
fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs) 
24287  250 

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

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

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

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

255 
fun pconst_hyper_mem f const_tab (s, ps) = 
38939  256 
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

257 

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

260 
 pattern_for_type (TVar _) = PVar 

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

261 

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

262 
(* Pairs a constant with the list of its type instantiations. *) 
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

263 
fun ptype thy const x = 
38939  264 
(if const then map pattern_for_type (these (try (Sign.const_typargs thy) x)) 
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

265 
else []) 
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

266 
fun rich_ptype thy const (s, T) = 
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

267 
PType (order_of_type T, ptype thy const (s, T)) 
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

268 
fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T)) 
24287  269 

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

24287  272 

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

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

274 
connective, which we ignore.*) 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

275 
fun add_pconst_to_table also_skolem (s, p) = 
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

276 
if (not also_skolem andalso String.isPrefix skolem_prefix s) then I 
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

277 
else Symtab.map_default (s, [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

278 

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

279 
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

280 
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

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

282 
(* We include free variables, as well as constants, to handle locales. For 
41205  283 
each quantifiers that must necessarily be skolemized by the automatic 
284 
prover, we introduce a fresh constant to simulate the effect of 

285 
Skolemization. *) 

40373  286 
fun do_const const x ts = 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

287 
let val (built_in, ts) = is_built_in_const x ts in 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

288 
(not built_in 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

289 
? add_pconst_to_table also_skolems (rich_pconst thy const x)) 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

290 
#> fold do_term ts 
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

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

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

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

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

295 
 (Free x, ts) => do_const false x ts 
38939  296 
 (Abs (_, T, t'), ts) => 
297 
(null ts 

41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

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

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

300 
 (_, ts) => fold do_term ts 
38939  301 
fun do_quantifier will_surely_be_skolemized abs_T body_t = 
37537  302 
do_formula pos body_t 
38747  303 
#> (if also_skolems andalso will_surely_be_skolemized then 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

304 
add_pconst_to_table true 
41207  305 
(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

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

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

308 
and do_term_or_formula T = 
41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset

309 
if T = HOLogic.boolT then do_formula NONE else do_term 
37537  310 
and do_formula pos t = 
311 
case t of 

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

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

316 
 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

317 
fold (do_term_or_formula T) [t1, t2] 
37537  318 
 @{const Trueprop} $ t1 => do_formula pos t1 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

319 
 @{const False} => I 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

320 
 @{const True} => I 
37537  321 
 @{const Not} $ t1 => do_formula (flip pos) t1 
38939  322 
 Const (@{const_name All}, _) $ Abs (_, T, t') => 
323 
do_quantifier (pos = SOME false) T t' 

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

325 
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

326 
 @{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

327 
 @{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

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

330 
 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

331 
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

332 
 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

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

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

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

338 
do_quantifier (pos = SOME false) T 

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

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

341 
do_quantifier (pos = SOME true) T 

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

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

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

346 
in Symtab.empty > fold (do_formula pos) ts end 
24287  347 

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

349 
takes the given theory into account.*) 

41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

350 
fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...} 
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

351 
: relevance_fudge) thy_name t = 
40070
bdb890782d4a
replaced references with proper record that's threaded through
blanchet
parents:
39958
diff
changeset

352 
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

353 
theory_const_irrel_weight] then 
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

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

355 
else 
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

356 
t 
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

357 

6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

358 
fun theory_const_prop_of fudge th = 
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

359 
theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

360 

24287  361 
(**** Constant / Type Frequencies ****) 
362 

38743  363 
(* A twodimensional symbol table counts frequencies of constants. It's keyed 
364 
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

365 
latter, we need a linear ordering on "pattern list". *) 
24287  366 

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

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

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

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

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

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

373 
prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) 
38939  374 
fun ptype_ord (PType p, PType q) = 
375 
prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q) 

24287  376 

38939  377 
structure PType_Tab = Table(type key = ptype val ord = ptype_ord) 
24287  378 

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

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

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

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

382 
(* Twodimensional table update. Constant maps to types maps to count. *) 
41204
bd57cf5944cb
get rid of experimental feature of term patterns in relevance filter  doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
blanchet
parents:
41202
diff
changeset

383 
PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1) 
38939  384 
> Symtab.map_default (s, PType_Tab.empty) 
38827
cf01645cbbce
extended relevance filter with firstorder term matching
blanchet
parents:
38825
diff
changeset

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

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

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

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

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

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

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

392 
in do_term o theory_const_prop_of fudge o snd end 
24287  393 

394 

395 
(**** Actual Filtering Code ****) 

396 

39367  397 
fun pow_int _ 0 = 1.0 
38939  398 
 pow_int x 1 = x 
399 
 pow_int x n = if n > 0 then x * pow_int x (n  1) else pow_int x (n + 1) / x 

400 

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

38686  405 

24287  406 

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

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

408 
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

409 

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

410 
(* "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

411 
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

412 
rare ones. *) 
39367  413 
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

414 

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

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

416 
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

417 
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

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

419 
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

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

421 
let val (k, x) = worse_irrel_freq > `Real.ceil in 
38939  422 
(if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x 
423 
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

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

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

426 

41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

427 
fun multiplier_for_const_name local_const_multiplier s = 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

428 
if String.isSubstring "." s then 1.0 else local_const_multiplier 
38821  429 

41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

430 
(* Computes a constant's weight, as determined by its frequency. *) 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

431 
fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

432 
theory_const_weight weight_for f const_tab 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

433 
(c as (s, PType (m, _))) = 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

434 
if s = abs_name then 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

435 
abs_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

436 
else if String.isPrefix skolem_prefix s then 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

437 
skolem_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

438 
else if String.isSuffix theory_const_suffix s then 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

439 
theory_const_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

440 
else 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

441 
multiplier_for_const_name local_const_multiplier s 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

442 
* weight_for m (pconst_freq (match_ptype o f) const_tab c) 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

443 

56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

444 
fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight, 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

445 
theory_const_rel_weight, ...} : relevance_fudge) 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

446 
const_tab = 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

447 
generic_pconst_weight local_const_multiplier abs_rel_weight 0.0 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

448 
theory_const_rel_weight rel_weight_for I const_tab 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

449 
fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight, 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

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

451 
theory_const_irrel_weight, ...}) const_tab = 
41790
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

452 
generic_pconst_weight local_const_multiplier abs_irrel_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

453 
skolem_irrel_weight theory_const_irrel_weight 
56dcd46ddf7a
give more weight to Frees than to Consts in relevance filter
blanchet
parents:
41768
diff
changeset

454 
(irrel_weight_for fudge) swap const_tab 
24287  455 

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

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

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

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

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

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

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

462 
 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

463 

40418  464 
fun is_odd_const_name s = 
465 
s = abs_name orelse String.isPrefix skolem_prefix s orelse 

466 
String.isSuffix theory_const_suffix s 

467 

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

468 
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

469 
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

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

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

472 
 (rel, irrel) => 
40418  473 
if forall (forall (is_odd_const_name o fst)) [rel, irrel] then 
40371  474 
0.0 
475 
else 

476 
let 

477 
val irrel = irrel > filter_out (pconst_mem swap rel) 

478 
val rel_weight = 

479 
0.0 > fold (curry (op +) o rel_pconst_weight fudge const_tab) rel 

480 
val irrel_weight = 

481 
~ (locality_bonus fudge loc) 

482 
> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel 

483 
val res = rel_weight / (rel_weight + irrel_weight) 

484 
in if Real.isFinite res then res else 0.0 end 

38747  485 

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

486 
fun pconsts_in_fact thy is_built_in_const t = 
38825  487 
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

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

489 
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

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

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

492 
[] => 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

493 
 consts => SOME ((fact, consts), NONE) 
24287  494 

41768
dd2125fb75f9
export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents:
41767
diff
changeset

495 
val const_names_in_fact = map fst ooo pconsts_in_fact 
dd2125fb75f9
export more functionality of Sledgehammer to applications (for experiments)
blanchet
parents:
41767
diff
changeset

496 

38699  497 
type annotated_thm = 
38939  498 
(((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

499 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

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

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

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

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

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

507 
/ Real.fromInt max_relevant, max_imperfect_exp))) 
38747  508 
val (perfect, imperfect) = 
38889  509 
candidates > sort (Real.compare o swap o pairself snd) 
510 
> take_prefix (fn (_, w) => w > 0.99999) 

38747  511 
val ((accepts, more_rejects), rejects) = 
512 
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

513 
in 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

514 
trace_msg ctxt (fn () => 
41491  515 
"Actually passed (" ^ string_of_int (length accepts) ^ " of " ^ 
516 
string_of_int (length candidates) ^ "): " ^ 

38889  517 
(accepts > map (fn ((((name, _), _), _), weight) => 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38751
diff
changeset

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

519 
> commas)); 
38747  520 
(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

521 
end 
24287  522 

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

523 
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

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

525 
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

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

527 
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

528 
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

529 
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

530 

41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

531 
fun add_arities is_built_in_const th = 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

532 
let 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

533 
fun aux _ _ NONE = NONE 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

534 
 aux t args (SOME tab) = 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

535 
case t of 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

536 
t1 $ t2 => SOME tab > aux t1 (t2 :: args) > aux t2 [] 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

537 
 Const (x as (s, _)) => 
41336
0ea5b9c7d233
proper handling of the arguments of SMT builtins  for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
blanchet
parents:
41279
diff
changeset

538 
(if is_built_in_const x args > fst then 
41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

539 
SOME tab 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

540 
else case Symtab.lookup tab s of 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

541 
NONE => SOME (Symtab.update (s, length args) tab) 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

542 
 SOME n => if n = length args then SOME tab else NONE) 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

543 
 _ => SOME tab 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

544 
in aux (prop_of th) [] end 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

545 

8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

546 
fun needs_ext is_built_in_const facts = 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

547 
fold (add_arities is_built_in_const o snd) facts (SOME Symtab.empty) 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

548 
> is_none 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

549 

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

550 
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

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

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

553 
let 
42361  554 
val thy = Proof_Context.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

555 
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

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

557 
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

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

559 
[Chained, Assum, Local] 
39012  560 
val add_ths = Attrib.eval_thms ctxt add 
561 
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

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

564 
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

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

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

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

571 
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

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

574 
let 
38747  575 
val (accepts, more_rejects) = 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

576 
take_most_relevant ctxt max_relevant remaining_max fudge 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

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

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

579 
rel_const_tab 
41066
3890ef4e02f9
pass constant arguments to the builtin check function, cf. d2b1fc1b8e19
blanchet
parents:
40418
diff
changeset

580 
> fold (add_pconst_to_table false) (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

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

582 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

598 
in 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

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

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

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

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

603 
map (fst o fst) accepts @ 
38747  604 
(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

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

606 
else 
38747  607 
iter (j + 1) remaining_max threshold rel_const_tab' 
608 
hopeless_rejects hopeful_rejects) 

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

609 
end 
38889  610 
 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

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

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

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

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

616 
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

617 
 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

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

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

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

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

625 
in 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

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

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

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

629 
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

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

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

633 
end 
41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

634 
fun add_facts ths accepts = 
41167
b05014180288
move facts supplied with "add:" to the front, so that they get a better weight (SMT)
blanchet
parents:
41159
diff
changeset

635 
(facts > filter (member Thm.eq_thm ths o snd)) @ 
b05014180288
move facts supplied with "add:" to the front, so that they get a better weight (SMT)
blanchet
parents:
41159
diff
changeset

636 
(accepts > filter_out (member Thm.eq_thm ths o snd)) 
40408  637 
> take max_relevant 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

639 
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

640 
> iter 0 max_relevant threshold0 goal_const_tab [] 
41158
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

641 
> not (null add_ths) ? add_facts add_ths 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

642 
> (fn accepts => 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

643 
accepts > needs_ext is_built_in_const accepts 
8c9c31a757f5
make Sledgehammer's relevance filter include the "ext" rule when appropriate
blanchet
parents:
41140
diff
changeset

644 
? add_facts @{thms ext}) 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

645 
> tap (fn accepts => trace_msg ctxt (fn () => 
41491  646 
"Total relevant: " ^ string_of_int (length accepts))) 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

647 
end 
24287  648 

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

649 

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

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

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

653 

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

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

655 

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

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

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

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

659 
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

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

661 
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

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

663 

42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

664 
fun mk_fact_table g f xs = 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

665 
fold (Termtab.update o `(g o prop_of o f)) xs Termtab.empty 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

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

667 

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

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

669 
val multi_base_blacklist = 
41199  670 
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", 
671 
"cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", 

672 
"weak_case_cong"] 

41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset

673 
> not instantiate_inducts ? append ["induct", "inducts"] 
38682  674 
> map (prefix ".") 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

675 

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

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

677 

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

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

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

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

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

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

683 

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

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

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

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

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

688 
 formula_has_too_many_lambdas Ts t = 
41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset

689 
if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

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

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

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

693 

38692  694 
(* 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

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

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

697 

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

698 
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

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

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

701 

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

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

703 
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

704 

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

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

708 

38904  709 
(* FIXME: make more reliable *) 
710 
val exists_low_level_class_const = 

711 
exists_Const (fn (s, _) => 

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

713 

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

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

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

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

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

719 

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

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

723 
 _ => false) (prop_of th) 

724 

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

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

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

727 

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

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

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

730 

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

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

732 
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

733 
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

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

735 

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

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

737 
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

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

739 
let 
38629  740 
fun is_bad_equal (Var z) t = 
741 
not (exists_subterm (fn Var z' => z = z'  _ => false) t) 

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

743 
 is_bad_equal _ _ = false 

744 
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

745 
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

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

747 
(_, @{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

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

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

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

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

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

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

754 
 (_, @{const "==>"} $ t1 $ t2) => 
38629  755 
do_formula (not pos) t1 andalso 
756 
(t2 = @{prop False} orelse do_formula pos t2) 

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

757 
 (_, @{const HOL.implies} $ t1 $ t2) => 
38629  758 
do_formula (not pos) t1 andalso 
759 
(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

760 
 (_, @{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

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

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

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

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

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

766 
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

767 

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

768 
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

769 
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

770 
 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

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

772 

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

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

774 
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

775 
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

776 
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

777 
for higherorder problems. *) 
42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

778 
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

779 

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

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

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

782 
are omitted. *) 
42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

783 
val is_dangerous_term = 
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

784 
transform_elim_term 
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

785 
#> has_bound_or_var_of_type dangerous_types orf is_exhaustive_finite 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

786 

42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

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

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

789 
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse 
42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

790 
exists_sledgehammer_const t orelse exists_low_level_class_const t orelse 
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

791 
is_metastrange_theorem thm orelse is_that_fact thm 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

793 

42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

794 
fun meta_equify (@{const Trueprop} 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

795 
$ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) = 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

796 
Const (@{const_name "=="}, T > T > @{typ prop}) $ t1 $ t2 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

797 
 meta_equify t = t 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

798 

2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

799 
val normalize_simp_prop = 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

800 
meta_equify 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

801 
#> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T)  t => t) 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

802 
#> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S))) 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

803 

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

804 
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

805 
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

806 
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

807 
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

808 
val elims = map Classical.classical_rule (safeEs @ hazEs) 
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

809 
val simps = ctxt > simpset_of > dest_ss > #simps 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

810 
in 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

811 
(mk_fact_table I I intros, 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

812 
mk_fact_table I I elims, 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

813 
mk_fact_table normalize_simp_prop snd simps) 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

814 
end 
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

815 

42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

816 
fun all_facts ctxt reserved really_all add_ths chained_ths = 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

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

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

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

823 
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

824 
val is_chained = member Thm.eq_thm chained_ths 
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

825 
val (intros, elims, simps) = clasimpset_rules_of ctxt 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

826 
fun locality_of_theorem global th = 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

827 
if is_chained th then 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

828 
Chained 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

829 
else if global then 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

830 
let val t = prop_of th in 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

831 
if Termtab.defined intros t then Intro 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

832 
else if Termtab.defined elims t then Elim 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

833 
else if Termtab.defined simps (normalize_simp_prop t) then Simp 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

834 
else General 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

835 
end 
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

836 
else 
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

837 
if is_assum th then Assum else Local 
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

838 
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

839 
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

840 
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

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

842 
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

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

844 
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

845 
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

846 
fun add_facts global foldx facts = 
38699  847 
foldx (fn (name0, ths) => 
41989
c1d560db15ec
add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)
blanchet
parents:
41790
diff
changeset

848 
if not really_all andalso name0 <> "" andalso 
39012  849 
forall (not o member Thm.eq_thm add_ths) ths andalso 
38699  850 
(Facts.is_concealed facts name0 orelse 
851 
(respect_no_atp andalso is_package_def name0) orelse 

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

853 
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

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

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

856 
let 
38699  857 
val multi = length ths > 1 
41279  858 
val backquote_thm = 
859 
backquote o string_for_term ctxt o close_form o prop_of 

38699  860 
fun check_thms a = 
42361  861 
case try (Proof_Context.get_thms ctxt) a of 
38699  862 
NONE => false 
863 
 SOME ths' => Thm.eq_thms (ths, ths') 

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

864 
in 
38699  865 
pair 1 
866 
#> fold (fn th => fn (j, rest) => 

42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

867 
(j + 1, 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

868 
if is_theorem_bad_for_atps th andalso 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

869 
not (member Thm.eq_thm add_ths th) then 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

870 
rest 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

871 
else 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

872 
(((fn () => 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

873 
if name0 = "" then 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

874 
th > backquote_thm 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

875 
else 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

876 
[Facts.extern ctxt facts name0, 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

877 
Name_Space.extern ctxt full_space name0, 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

878 
name0] 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

879 
> find_first check_thms 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

880 
> (fn SOME name => 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

881 
make_name reserved multi j name 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

882 
 NONE => "")), 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

883 
locality_of_theorem global th), 
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

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

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

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

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

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

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

891 

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

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

893 
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

894 
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

895 
List.partition (fst o snd) #> op @ #> map (apsnd snd) 
38699  896 
#> 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

897 

41199  898 
fun external_frees t = 
899 
[] > Term.add_frees t > filter_out (can Name.dest_internal o fst) 

900 

42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

901 
fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const 
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

902 
fudge (override as {add, only, ...}) chained_ths hyp_ts 
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42589
diff
changeset

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

904 
let 
42361  905 
val thy = Proof_Context.theory_of ctxt 
38822
aa0101e618e2
fix threshold computation + remove "op =" from relevant constants
blanchet
parents:
38821
diff
changeset

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

907 
1.0 / Real.fromInt (max_relevant + 1)) 
39012  908 
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

909 
val reserved = reserved_isar_keyword_table () 
41199  910 
val ind_stmt = 
911 
Logic.list_implies (hyp_ts > filter_out (null o external_frees), concl_t) 

41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41207
diff
changeset

912 
> Object_Logic.atomize_term thy 
41199  913 
val ind_stmt_xs = external_frees ind_stmt 
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

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

916 
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

917 
o fact_from_ref ctxt reserved chained_ths) add 
38699  918 
else 
42641
2cd4e6463842
recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
blanchet
parents:
42638
diff
changeset

919 
all_facts ctxt reserved false add_ths chained_ths) 
41273
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset

920 
> instantiate_inducts 
35ce17cd7967
made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
blanchet
parents:
41211
diff
changeset

921 
? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

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

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

924 
in 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

925 
trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^ 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42641
diff
changeset

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

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

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

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

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

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

932 
else 
41200
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

933 
((concl_t > theory_constify fudge (Context.theory_name thy)) :: hyp_ts) 
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

934 
> relevance_filter ctxt threshold0 decay max_relevant is_built_in_const 
6cc9b6fd7f6f
add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
blanchet
parents:
41199
diff
changeset

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

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

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

938 

15347  939 
end; 