author  blanchet 
Tue, 29 Jun 2010 10:25:53 +0200  
changeset 37626  1146291fe718 
parent 37616  c8d2d84d6011 
child 37995  06f02b15ef8a 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML 
33309  2 
Author: Jia Meng, Cambridge University Computer Laboratory, 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 
33309  4 
*) 
15452  5 

35826  6 
signature SLEDGEHAMMER_FACT_FILTER = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

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

8 
type relevance_override = 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

9 
{add: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

10 
del: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

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

12 

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

13 
val trace : bool Unsynchronized.ref 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

14 
val chained_prefix : string 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

15 
val name_thms_pair_from_ref : 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

16 
Proof.context > thm list > Facts.ref > string * thm list 
37347
635425a442e8
show more respect for userspecified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
blanchet
parents:
37345
diff
changeset

17 
val relevant_facts : 
37580
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

18 
bool > real > real > bool > int > bool > relevance_override 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

19 
> Proof.context * (thm list * 'a) > thm list > (string * thm) list 
15347  20 
end; 
21 

35826  22 
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = 
15347  23 
struct 
24 

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

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

26 
fun trace_msg msg = if !trace then tracing (msg ()) else () 
35826  27 

37580
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

28 
val respect_no_atp = true 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

29 

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

30 
type relevance_override = 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

31 
{add: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

32 
del: Facts.ref list, 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

33 
only: bool} 
21070  34 

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

35 
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

36 
(* Used to label theorems chained into the goal. *) 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

37 
val chained_prefix = sledgehammer_prefix ^ "chained_" 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

38 

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

39 
fun name_thms_pair_from_ref ctxt chained_ths xref = 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

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

41 
val ths = ProofContext.get_fact ctxt xref 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

42 
val name = Facts.string_of_ref xref 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

43 
> forall (member Thm.eq_thm chained_ths) ths 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

44 
? prefix chained_prefix 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

45 
in (name, ths) end 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

46 

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

47 

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

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

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

50 
(***************************************************************) 
19194  51 

35865  52 
fun strip_Trueprop (@{const Trueprop} $ t) = t 
24958  53 
 strip_Trueprop t = t; 
19194  54 

24287  55 
(*** constants with types ***) 
56 

57 
(*An abstraction of Isabelle types*) 

58 
datatype const_typ = CTVar  CType of string * const_typ list 

59 

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

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

61 
fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
24287  62 
con1=con2 andalso match_types args1 args2 
63 
 match_type CTVar _ = true 

64 
 match_type _ CTVar = false 

65 
and match_types [] [] = true 

66 
 match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2; 

67 

68 
(*Is there a unifiable constant?*) 

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

69 
fun uni_mem goal_const_tab (c, c_typ) = 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

70 
exists (match_types c_typ) (these (Symtab.lookup goal_const_tab c)) 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

71 

24287  72 
(*Maps a "real" type to a const_typ*) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

73 
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
24287  74 
 const_typ_of (TFree _) = CTVar 
75 
 const_typ_of (TVar _) = CTVar 

76 

77 
(*Pairs a constant with the list of its type instantiations (using const_typ)*) 

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

78 
fun const_with_typ thy (c,typ) = 
24287  79 
let val tvars = Sign.const_typargs thy (c,typ) 
80 
in (c, map const_typ_of tvars) end 

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

81 
handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) 
24287  82 

83 
(*Add a const/type pair to the table, but a [] entry means a standard connective, 

84 
which we ignore.*) 

37502  85 
fun add_const_type_to_table (c, ctyps) = 
86 
Symtab.map_default (c, [ctyps]) 

87 
(fn [] => []  ctypss => insert (op =) ctyps ctypss) 

24287  88 

37551
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

89 
val fresh_prefix = "Sledgehammer.Fresh." 
37537  90 

91 
val flip = Option.map not 

24287  92 

37551
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

93 
val boring_natural_consts = [@{const_name If}] 
37537  94 
(* Including equality in this list might be expected to stop rules like 
95 
subset_antisym from being chosen, but for some reason filtering works better 

96 
with them listed. The logical signs All, Ex, &, and > are omitted for CNF 

97 
because any remaining occurrences must be within comprehensions. *) 

98 
val boring_cnf_consts = 

99 
[@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, 

100 
@{const_name "=="}, @{const_name "op "}, @{const_name Not}, 

101 
@{const_name "op ="}] 

102 

103 
fun get_consts_typs thy pos ts = 

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

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

105 
(* Free variables are included, as well as constants, to handle locales. 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

106 
"skolem_id" is included to increase the complexity of theorems containing 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

107 
Skolem functions. In nonCNF form, "Ex" is included but each occurrence 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

108 
is considered fresh, to simulate the effect of Skolemization. *) 
37537  109 
fun do_term t = 
110 
case t of 

111 
Const x => add_const_type_to_table (const_with_typ thy x) 

112 
 Free x => add_const_type_to_table (const_with_typ thy x) 

113 
 (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t 

114 
 t1 $ t2 => do_term t1 #> do_term t2 

37551
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

115 
 Abs (_, _, t) => 
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

116 
(* Abstractions lead to combinators, so we add a penalty for them. *) 
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

117 
add_const_type_to_table (gensym fresh_prefix, []) 
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

118 
#> do_term t 
37537  119 
 _ => I 
120 
fun do_quantifier sweet_pos pos body_t = 

121 
do_formula pos body_t 

122 
#> (if pos = SOME sweet_pos then I 

37551
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

123 
else add_const_type_to_table (gensym fresh_prefix, [])) 
37537  124 
and do_equality T t1 t2 = 
125 
fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE 

126 
else do_term) [t1, t2] 

127 
and do_formula pos t = 

128 
case t of 

129 
Const (@{const_name all}, _) $ Abs (_, _, body_t) => 

130 
do_quantifier false pos body_t 

131 
 @{const "==>"} $ t1 $ t2 => 

132 
do_formula (flip pos) t1 #> do_formula pos t2 

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

134 
do_equality T t1 t2 

135 
 @{const Trueprop} $ t1 => do_formula pos t1 

136 
 @{const Not} $ t1 => do_formula (flip pos) t1 

137 
 Const (@{const_name All}, _) $ Abs (_, _, body_t) => 

138 
do_quantifier false pos body_t 

139 
 Const (@{const_name Ex}, _) $ Abs (_, _, body_t) => 

140 
do_quantifier true pos body_t 

141 
 @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 

142 
 @{const "op "} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 

143 
 @{const "op >"} $ t1 $ t2 => 

144 
do_formula (flip pos) t1 #> do_formula pos t2 

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

146 
do_equality T t1 t2 

147 
 (t0 as Const (_, @{typ bool})) $ t1 => 

148 
do_term t0 #> do_formula pos t1 (* theory constant *) 

149 
 _ => do_term t 

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

150 
in 
37537  151 
Symtab.empty 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

152 
> fold (Symtab.update o rpair []) boring_natural_consts 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

153 
> fold (do_formula pos) ts 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

154 
end 
24287  155 

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

157 
takes the given theory into account.*) 

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

158 
fun theory_const_prop_of theory_relevant th = 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

159 
if theory_relevant then 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

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

161 
val name = Context.theory_name (theory_of_thm th) 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

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

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

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

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

166 

24287  167 
(**** Constant / Type Frequencies ****) 
168 

169 
(*A twodimensional symbol table counts frequencies of constants. It's keyed first by 

170 
constant name and second by its list of type instantiations. For the latter, we need 

171 
a linear ordering on type const_typ list.*) 

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

172 

24287  173 
local 
174 

175 
fun cons_nr CTVar = 0 

176 
 cons_nr (CType _) = 1; 

177 

178 
in 

179 

180 
fun const_typ_ord TU = 

181 
case TU of 

182 
(CType (a, Ts), CType (b, Us)) => 

183 
(case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us)  ord => ord) 

184 
 (T, U) => int_ord (cons_nr T, cons_nr U); 

185 

186 
end; 

187 

31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31910
diff
changeset

188 
structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord); 
24287  189 

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

190 
fun count_axiom_consts theory_relevant thy (_, th) = 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

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

192 
fun do_const (a, T) = 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

193 
let val (c, cts) = const_with_typ thy (a,T) in 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

194 
(* Twodimensional table update. Constant maps to types maps to 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

195 
count. *) 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

196 
CTtab.map_default (cts, 0) (Integer.add 1) 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

197 
> Symtab.map_default (c, CTtab.empty) 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

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

199 
fun do_term (Const x) = do_const x 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

200 
 do_term (Free x) = do_const x 
37515
ef3742657bc6
fix bug with "skolem_id" + sort facts for increased readability
blanchet
parents:
37509
diff
changeset

201 
 do_term (Const (x as (@{const_name skolem_id}, _)) $ _) = do_const x 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

202 
 do_term (t $ u) = do_term t #> do_term u 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

203 
 do_term (Abs (_, _, t)) = do_term t 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

204 
 do_term _ = I 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

205 
in th > theory_const_prop_of theory_relevant > do_term end 
24287  206 

207 

208 
(**** Actual Filtering Code ****) 

209 

210 
(*The frequency of a constant is the sum of those of all instances of its type.*) 

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

211 
fun const_frequency const_tab (c, cts) = 
36185
0ee736f08ed0
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
blanchet
parents:
36182
diff
changeset

212 
CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

213 
(the (Symtab.lookup const_tab c) 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

214 
handle Option.Option => raise Fail ("Const: " ^ c)) 0 
24287  215 

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

216 
(*A surprising number of theorems contain only a few significant constants. 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

217 
These include all induction rules, and other general theorems. Filtering 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

218 
theorems in clause form reveals these complexities in the form of Skolem 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

219 
functions. If we were instead to filter theorems in their natural form, 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

220 
some other method of measuring theorem complexity would become necessary.*) 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

221 

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

222 
(* "log" seems best in practice. A constant function of one ignores the constant 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

223 
frequencies. *) 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

224 
fun log_weight2 (x:real) = 1.0 + 2.0 / Math.ln (x + 1.0) 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

225 

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

226 
(* Computes a constant's weight, as determined by its frequency. *) 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

227 
val ct_weight = log_weight2 o real oo const_frequency 
24287  228 

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

229 
(*Relevant constants are weighted according to frequency, 
24287  230 
but irrelevant constants are simply counted. Otherwise, Skolem functions, 
231 
which are rare, would harm a clause's chances of being picked.*) 

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

232 
fun clause_weight const_tab gctyps consts_typs = 
24287  233 
let val rel = filter (uni_mem gctyps) consts_typs 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

234 
val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0 
24287  235 
in 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

236 
rel_weight / (rel_weight + real (length consts_typs  length rel)) 
24287  237 
end; 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

238 

24287  239 
(*Multiplies out to a list of pairs: 'a * 'b list > ('a * 'b) list > ('a * 'b) list*) 
30190  240 
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys; 
24287  241 

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

242 
fun consts_typs_of_term thy t = 
37537  243 
Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) [] 
24287  244 

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

245 
fun pair_consts_typs_axiom theory_relevant thy axiom = 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

246 
(axiom, axiom > snd > theory_const_prop_of theory_relevant 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

247 
> consts_typs_of_term thy) 
24287  248 

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

249 
exception CONST_OR_FREE of unit 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

250 

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

251 
fun dest_Const_or_Free (Const x) = x 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

252 
 dest_Const_or_Free (Free x) = x 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

253 
 dest_Const_or_Free _ = raise CONST_OR_FREE () 
24287  254 

255 
(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) 

32994  256 
fun defines thy thm gctypes = 
24287  257 
let val tm = prop_of thm 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

258 
fun defs lhs rhs = 
24287  259 
let val (rator,args) = strip_comb lhs 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

260 
val ct = const_with_typ thy (dest_Const_or_Free rator) 
33037
b22e44496dc2
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
haftmann
parents:
32994
diff
changeset

261 
in 
b22e44496dc2
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
haftmann
parents:
32994
diff
changeset

262 
forall is_Var args andalso uni_mem gctypes ct andalso 
33038  263 
subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) 
24287  264 
end 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

265 
handle CONST_OR_FREE () => false 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

266 
in 
35963  267 
case tm of 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

268 
@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

269 
defs lhs rhs 
35963  270 
 _ => false 
24287  271 
end; 
272 

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

273 
type annotated_cnf_thm = (string * thm) * (string * const_typ list) list 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

274 

24287  275 
(*For a reverse sort, putting the largest values first.*) 
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

276 
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) 
24287  277 

278 
(*Limit the number of new clauses, to prevent runaway acceptance.*) 

37568  279 
fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) = 
24287  280 
let val nnew = length newpairs 
281 
in 

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

282 
if nnew <= max_new then (map #1 newpairs, []) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

283 
else 
24287  284 
let val cls = sort compare_pairs newpairs 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28065
diff
changeset

285 
val accepted = List.take (cls, max_new) 
24287  286 
in 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

287 
trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

288 
", exceeds the limit of " ^ Int.toString (max_new))); 
35865  289 
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); 
290 
trace_msg (fn () => "Actually passed: " ^ 

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

291 
space_implode ", " (map (fst o fst o fst) accepted)); 
24287  292 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

293 
(map #1 accepted, map #1 (List.drop (cls, max_new))) 
24287  294 
end 
295 
end; 

296 

36922  297 
fun relevant_clauses ctxt relevance_convergence defs_relevant max_new 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

298 
({add, del, ...} : relevance_override) const_tab = 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

299 
let 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

300 
val thy = ProofContext.theory_of ctxt 
37501
b5440c78ed3f
leverage new data structure for handling "add:" and "del:"
blanchet
parents:
37500
diff
changeset

301 
val add_thms = maps (ProofContext.get_fact ctxt) add 
b5440c78ed3f
leverage new data structure for handling "add:" and "del:"
blanchet
parents:
37500
diff
changeset

302 
val del_thms = maps (ProofContext.get_fact ctxt) del 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

303 
fun iter threshold rel_const_tab = 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

304 
let 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

305 
fun relevant ([], _) [] = [] (* Nothing added this iteration *) 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

306 
 relevant (newpairs, rejects) [] = 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

307 
let 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

308 
val (newrels, more_rejects) = take_best max_new newpairs 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

309 
val new_consts = maps #2 newrels 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

310 
val rel_const_tab = 
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

311 
rel_const_tab > fold add_const_type_to_table new_consts 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

312 
val threshold = 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

313 
threshold + (1.0  threshold) / relevance_convergence 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

314 
in 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

315 
trace_msg (fn () => "relevant this iteration: " ^ 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

316 
Int.toString (length newrels)); 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

317 
map #1 newrels @ iter threshold rel_const_tab 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

318 
(more_rejects @ rejects) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

319 
end 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

320 
 relevant (newrels, rejects) 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

321 
((ax as (clsthm as (name, th), consts_typs)) :: axs) = 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

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

323 
val weight = 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

324 
if member Thm.eq_thm add_thms th then 1.0 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

325 
else if member Thm.eq_thm del_thms th then 0.0 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

326 
else clause_weight const_tab rel_const_tab consts_typs 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

327 
in 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

328 
if weight >= threshold orelse 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

329 
(defs_relevant andalso defines thy th rel_const_tab) then 
37537  330 
(trace_msg (fn () => 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

331 
name ^ " passes: " ^ Real.toString weight 
37537  332 
(* ^ " consts: " ^ commas (map fst consts_typs) *)); 
333 
relevant ((ax, weight) :: newrels, rejects) axs) 

36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

334 
else 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

335 
relevant (newrels, ax :: rejects) axs 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

336 
end 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

337 
in 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

338 
trace_msg (fn () => "relevant_clauses, current threshold: " ^ 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

339 
Real.toString threshold); 
36182
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

340 
relevant ([], []) 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

341 
end 
b136019c5d61
reorganize Sledgehammer's relevance filter slightly
blanchet
parents:
36061
diff
changeset

342 
in iter end 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

343 

36922  344 
fun relevance_filter ctxt relevance_threshold relevance_convergence 
345 
defs_relevant max_new theory_relevant relevance_override 

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

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

347 
if relevance_threshold > 1.0 then 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

348 
[] 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

349 
else if relevance_threshold < 0.0 then 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

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

351 
else 
35963  352 
let 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

353 
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

354 
Symtab.empty 
37537  355 
val goal_const_tab = get_consts_typs thy (SOME true) goals 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

356 
val relevance_threshold = 0.9 * relevance_threshold (* FIXME *) 
35963  357 
val _ = 
358 
trace_msg (fn () => "Initial constants: " ^ 

37551
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

359 
commas (goal_const_tab 
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

360 
> Symtab.dest 
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

361 
> filter (curry (op <>) [] o snd) 
2dc53a9f69c9
improve the natural formula relevance filter code, so that it behaves more like the CNF one
blanchet
parents:
37543
diff
changeset

362 
> map fst)) 
35963  363 
val relevant = 
36922  364 
relevant_clauses ctxt relevance_convergence defs_relevant max_new 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

365 
relevance_override const_tab relevance_threshold 
36922  366 
goal_const_tab 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

367 
(map (pair_consts_typs_axiom theory_relevant thy) 
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36185
diff
changeset

368 
axioms) 
35963  369 
in 
370 
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); 

371 
relevant 

372 
end 

24287  373 

374 
(***************************************************************) 

19768
9afd9b9c47d0
ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents:
19746
diff
changeset

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

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

377 

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

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

379 

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

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

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

382 
fun is_package_def a = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30291
diff
changeset

383 
let val names = Long_Name.explode a 
21690
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

384 
in 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

385 
length names > 2 andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

386 
not (hd names = "local") andalso 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

387 
String.isSuffix "_def" a orelse String.isSuffix "_defs" a 
552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires.
paulson
parents:
21588
diff
changeset

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

389 

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

390 
fun make_clause_table xs = 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

391 
fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

392 

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

393 
fun make_unique xs = 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

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

395 

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

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

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

398 
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

399 
"split_asm", "cases", "ext_cases"] 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

400 

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

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

402 

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

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

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

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

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

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

408 

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

409 
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

410 

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

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

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

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

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

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

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

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

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

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

420 

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

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

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

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

424 

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

425 
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

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

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

428 

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

429 
fun is_formula_too_complex t = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

430 
apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

431 
formula_has_too_many_lambdas [] t 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

432 

37543  433 
val exists_sledgehammer_const = 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

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

435 

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

436 
fun is_strange_thm th = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

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

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

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

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

441 

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

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

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

444 

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

445 
fun is_theorem_bad_for_atps thm = 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

446 
let val t = prop_of thm in 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

447 
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

448 
exists_sledgehammer_const t orelse is_strange_thm thm 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

449 
end 
37543  450 

37580
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

451 
fun all_name_thms_pairs ctxt chained_ths = 
22382
dbf09db0a40d
New code to store theorem names in a concise form rather than as fullyqualified.
paulson
parents:
22217
diff
changeset

452 
let 
26675  453 
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); 
26278  454 
val local_facts = ProofContext.facts_of ctxt; 
33641
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

455 
val full_space = 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

456 
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

457 

af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

458 
fun valid_facts facts = 
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

459 
(facts, []) > Facts.fold_static (fn (name, ths0) => 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

460 
if Facts.is_concealed facts name orelse 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

461 
(respect_no_atp andalso is_package_def name) orelse 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

462 
member (op =) multi_base_blacklist (Long_Name.base_name name) then 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

463 
I 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

464 
else 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

465 
let 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

466 
fun check_thms a = 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

467 
(case try (ProofContext.get_thms ctxt) a of 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

468 
NONE => false 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

469 
 SOME ths1 => Thm.eq_thms (ths0, ths1)); 
33641
af07d9cd86ce
all_valid_thms: more sophisticated check against global + local name space;
wenzelm
parents:
33316
diff
changeset

470 

37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

471 
val name1 = Facts.extern facts name; 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

472 
val name2 = Name_Space.extern full_space name; 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37616
diff
changeset

473 
val ths = filter_out is_theorem_bad_for_atps ths0 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

474 
in 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

475 
case find_first check_thms [name1, name2, name] of 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

476 
NONE => I 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

477 
 SOME name' => 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

478 
cons (name' > forall (member Thm.eq_thm chained_ths) ths 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

479 
? prefix chained_prefix, ths) 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

480 
end) 
26675  481 
in valid_facts global_facts @ valid_facts local_facts end; 
21224  482 

33309  483 
fun multi_name a th (n, pairs) = 
484 
(n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); 

21224  485 

37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

486 
fun add_names (_, []) pairs = pairs 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

487 
 add_names (a, [th]) pairs = (a, th) :: pairs 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

488 
 add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)) 
21224  489 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

490 
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

491 

36550
f8da913b6c3a
make sure short theorem names are preferred to composite ones in Sledgehammer;
blanchet
parents:
36473
diff
changeset

492 
(* The singlename theorems go after the multiplename ones, so that single 
f8da913b6c3a
make sure short theorem names are preferred to composite ones in Sledgehammer;
blanchet
parents:
36473
diff
changeset

493 
names are preferred when both are available. *) 
37580
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

494 
fun name_thm_pairs ctxt respect_no_atp name_thms_pairs = 
33309  495 
let 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

496 
val (mults, singles) = List.partition is_multi name_thms_pairs 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37359
diff
changeset

497 
val ps = [] > fold add_names singles > fold add_names mults 
36060
4d27652ffb40
reintroduce efficient set structure to collect "no_atp" theorems
blanchet
parents:
36059
diff
changeset

498 
in ps > respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; 
21224  499 

37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

500 
fun is_named ("", th) = 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

501 
(warning ("No name for theorem " ^ 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

502 
Display.string_of_thm_without_context th); false) 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

503 
 is_named _ = true 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

504 
fun checked_name_thm_pairs respect_no_atp ctxt = 
37580
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

505 
name_thm_pairs ctxt respect_no_atp 
37344
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

506 
#> tap (fn ps => trace_msg 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

507 
(fn () => ("Considering " ^ Int.toString (length ps) ^ 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

508 
" theorems"))) 
40f379944c1e
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
blanchet
parents:
37171
diff
changeset

509 
#> filter is_named 
19894  510 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21243
diff
changeset

511 
(***************************************************************) 
19194  512 
(* ATP invocation methods setup *) 
513 
(***************************************************************) 

514 

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

515 
(**** Predicates to detect unwanted clauses (prolific or likely to cause 
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

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

517 

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

518 
(** Too general means, positive equality literal with a variable X as one operand, 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

519 
when X does not occur properly in the other operand. This rules out clearly 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

520 
inconsistent clauses such as V=aV=b, though it by no means guarantees soundness. **) 
21588  521 

37348  522 
fun var_occurs_in_term ix = 
523 
let 

524 
fun aux (Var (jx, _)) = (ix = jx) 

525 
 aux (t1 $ t2) = aux t1 orelse aux t2 

526 
 aux (Abs (_, _, t)) = aux t 

527 
 aux _ = false 

528 
in aux end 

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

529 

37348  530 
fun is_record_type T = not (null (Record.dest_recTs T)) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

531 

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

532 
(*Unwanted equalities include 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

533 
(1) those between a variable that does not properly occur in the second operand, 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

534 
(2) those between a variable and a record, since these seem to be prolific "cases" thms 
21588  535 
*) 
37348  536 
fun too_general_eqterms (Var (ix,T), t) = 
537 
not (var_occurs_in_term ix t) orelse is_record_type T 

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

538 
 too_general_eqterms _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

539 

35865  540 
fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) = 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

541 
too_general_eqterms (x,y) orelse too_general_eqterms(y,x) 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

542 
 too_general_equality _ = false; 
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

543 

29267  544 
fun has_typed_var tycons = exists_subterm 
545 
(fn Var (_, Type (a, _)) => member (op =) tycons a  _ => false); 

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

546 

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

547 
(* Clauses are forbidden to contain variables of these types. The typical reason 
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

548 
is that they lead to unsoundness. Note that "unit" satisfies numerous 
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

549 
equations like "?x = ()". The resulting clause will have no type constraint, 
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

550 
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

551 
for higherorder problems. *) 
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

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

553 

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

554 
(* Clauses containing variables of type "unit" or "bool" or of the form 
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

555 
"?x = A  ?x = B  ?x = C" are likely to lead to unsound proofs if types are 
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

556 
omitted. *) 
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

557 
fun is_dangerous_term _ @{prop True} = true 
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

558 
 is_dangerous_term full_types t = 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

559 
not full_types andalso 
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

560 
(has_typed_var dangerous_types t orelse 
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

561 
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t))) 
21470
7c1b59ddcd56
Consolidation of code to "blacklist" unhelpful theorems, including record
paulson
parents:
21431
diff
changeset

562 

37580
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

563 
fun relevant_facts full_types relevance_threshold relevance_convergence 
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

564 
defs_relevant max_new theory_relevant 
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

565 
(relevance_override as {add, del, 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

566 
(ctxt, (chained_ths, _)) goal_cls = 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

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

568 
val thy = ProofContext.theory_of ctxt 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

569 
val add_thms = maps (ProofContext.get_fact ctxt) add 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

570 
val has_override = not (null add) orelse not (null del) 
37566
9ca40dff25bd
move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
blanchet
parents:
37552
diff
changeset

571 
val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

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

573 
checked_name_thm_pairs (respect_no_atp andalso not only) ctxt 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

574 
(map (name_thms_pair_from_ref ctxt chained_ths) add @ 
37580
c2c1caff5dea
got rid of "respect_no_atp" option, which even I don't use
blanchet
parents:
37578
diff
changeset

575 
(if only then [] else all_name_thms_pairs ctxt chained_ths)) 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

576 
> not has_override ? make_unique 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

577 
> filter (fn (_, th) => 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

578 
member Thm.eq_thm add_thms th orelse 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

579 
((* ### FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*) 
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

580 
not (is_dangerous_term full_types (prop_of th)))) 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

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

582 
relevance_filter ctxt relevance_threshold relevance_convergence 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

583 
defs_relevant max_new theory_relevant relevance_override 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

584 
thy axioms (map prop_of goal_cls) 
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

585 
> has_override ? make_unique 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

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

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

588 

15347  589 
end; 