author  blanchet 
Mon, 09 Aug 2010 14:08:30 +0200  
changeset 38290  581a402a80f0 
parent 38289  74dd8dd33512 
child 38395  2d6dc3f25686 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_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 
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 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

19 
> Proof.context * (thm list * 'a) > term list > term 
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

20 
> (string * thm) list 
15347  21 
end; 
22 

35826  23 
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = 
15347  24 
struct 
25 

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

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

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

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

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

30 

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

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

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

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

34 
only: bool} 
21070  35 

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

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

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

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

39 

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

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

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

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

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

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

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

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

47 

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

48 

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

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

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

51 
(***************************************************************) 
19194  52 

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

53 
fun strip_Trueprop_and_all (@{const Trueprop} $ t) = 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

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

55 
 strip_Trueprop_and_all (Const (@{const_name all}, _) $ Abs (_, _, t)) = 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

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

57 
 strip_Trueprop_and_all (Const (@{const_name All}, _) $ Abs (_, _, t)) = 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

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

59 
 strip_Trueprop_and_all t = t 
19194  60 

24287  61 
(*** constants with types ***) 
62 

63 
(*An abstraction of Isabelle types*) 

64 
datatype const_typ = CTVar  CType of string * const_typ list 

65 

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

67 
fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
24287  68 
con1=con2 andalso match_types args1 args2 
69 
 match_type CTVar _ = true 

70 
 match_type _ CTVar = false 

71 
and match_types [] [] = true 

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

73 

74 
(*Is there a unifiable constant?*) 

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

75 
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

76 
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

77 

24287  78 
(*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

79 
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
24287  80 
 const_typ_of (TFree _) = CTVar 
81 
 const_typ_of (TVar _) = CTVar 

82 

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

84 
fun const_with_typ thy (c,typ) = 
24287  85 
let val tvars = Sign.const_typargs thy (c,typ) 
86 
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

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

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

90 
which we ignore.*) 

37502  91 
fun add_const_type_to_table (c, ctyps) = 
92 
Symtab.map_default (c, [ctyps]) 

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

24287  94 

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

95 
val fresh_prefix = "Sledgehammer.Fresh." 
37537  96 
val flip = Option.map not 
38091  97 
(* These are typically simplified away by "Meson.presimplify". *) 
98 
val boring_consts = [@{const_name If}, @{const_name Let}] 

37537  99 

100 
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

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

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

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

104 
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

105 
is considered fresh, to simulate the effect of Skolemization. *) 
37537  106 
fun do_term t = 
107 
case t of 

108 
Const x => add_const_type_to_table (const_with_typ thy x) 

109 
 Free x => add_const_type_to_table (const_with_typ thy x) 

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

111 
 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

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

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

114 
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

115 
#> do_term t 
37537  116 
 _ => I 
117 
fun do_quantifier sweet_pos pos body_t = 

118 
do_formula pos body_t 

119 
#> (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

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

123 
else do_term) [t1, t2] 

124 
and do_formula pos t = 

125 
case t of 

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

127 
do_quantifier false pos body_t 

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

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

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

131 
do_equality T t1 t2 

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

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

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

135 
do_quantifier false pos body_t 

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

137 
do_quantifier true pos body_t 

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

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

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

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

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

143 
do_equality T t1 t2 

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

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

146 
 _ => do_term t 

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

147 
in 
38091  148 
Symtab.empty > fold (Symtab.update o rpair []) boring_consts 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

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

150 
end 
24287  151 

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

153 
takes the given theory into account.*) 

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

154 
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

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

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

157 
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

158 
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

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

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

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

162 

24287  163 
(**** Constant / Type Frequencies ****) 
164 

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

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

167 
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

168 

24287  169 
local 
170 

171 
fun cons_nr CTVar = 0 

172 
 cons_nr (CType _) = 1; 

173 

174 
in 

175 

176 
fun const_typ_ord TU = 

177 
case TU of 

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

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

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

181 

182 
end; 

183 

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

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

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

186 
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

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

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

189 
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

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

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

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

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

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

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

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

197 
 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

198 
 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

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

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

201 
in th > theory_const_prop_of theory_relevant > do_term end 
24287  202 

203 

204 
(**** Actual Filtering Code ****) 

205 

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

207 
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

208 
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

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

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

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

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

213 
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

214 

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

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

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

217 
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

218 

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

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

220 
val ct_weight = log_weight2 o real oo const_frequency 
24287  221 

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

222 
(*Relevant constants are weighted according to frequency, 
24287  223 
but irrelevant constants are simply counted. Otherwise, Skolem functions, 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

224 
which are rare, would harm a formula's chances of being picked.*) 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

225 
fun formula_weight const_tab gctyps consts_typs = 
38101
34b75b71235d
handle division by zero gracefully (used to raise Unordered later on)
blanchet
parents:
38095
diff
changeset

226 
let 
34b75b71235d
handle division by zero gracefully (used to raise Unordered later on)
blanchet
parents:
38095
diff
changeset

227 
val rel = filter (uni_mem gctyps) consts_typs 
34b75b71235d
handle division by zero gracefully (used to raise Unordered later on)
blanchet
parents:
38095
diff
changeset

228 
val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0 
34b75b71235d
handle division by zero gracefully (used to raise Unordered later on)
blanchet
parents:
38095
diff
changeset

229 
val res = rel_weight / (rel_weight + real (length consts_typs  length rel)) 
34b75b71235d
handle division by zero gracefully (used to raise Unordered later on)
blanchet
parents:
38095
diff
changeset

230 
in if Real.isFinite res then res else 0.0 end 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

231 

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

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

235 
fun consts_typs_of_term thy t = 
37537  236 
Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) [] 
24287  237 

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

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

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

240 
> consts_typs_of_term thy) 
24287  241 

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

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

243 

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

244 
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

245 
 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

246 
 dest_Const_or_Free _ = raise CONST_OR_FREE () 
24287  247 

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

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

251 
fun defs lhs rhs = 
24287  252 
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

253 
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

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

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

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

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

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

262 
defs lhs rhs 
35963  263 
 _ => false 
24287  264 
end; 
265 

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

266 
type annotated_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

267 

24287  268 
(*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

269 
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) 
24287  270 

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

271 
(* Limit the number of new facts, to prevent runaway acceptance. *) 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

272 
fun take_best max_new (newpairs : (annotated_thm * real) list) = 
24287  273 
let val nnew = length newpairs 
274 
in 

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

275 
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

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

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

280 
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

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

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

284 
space_implode ", " (map (fst o fst o fst) accepted)); 
24287  285 

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

286 
(map #1 accepted, map #1 (List.drop (cls, max_new))) 
24287  287 
end 
288 
end; 

289 

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

290 
fun relevant_facts ctxt relevance_convergence defs_relevant max_new 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

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

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

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

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

295 
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

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

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

298 
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

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

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

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

302 
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

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

304 
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

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

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

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

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

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

310 
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

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

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

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

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

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

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

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

318 
else if member Thm.eq_thm del_thms th then 0.0 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

319 
else formula_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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

336 

36922  337 
fun relevance_filter ctxt relevance_threshold relevance_convergence 
338 
defs_relevant max_new theory_relevant relevance_override 

37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

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

340 
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

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

342 
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

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

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

346 
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

347 
Symtab.empty 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

348 
val goal_const_tab = get_consts_typs thy (SOME true) goal_ts 
38090
fe51c098b0ab
fiddle with the fudge factors, to get similar results as before
blanchet
parents:
38085
diff
changeset

349 
val relevance_threshold = 0.8 * relevance_threshold (* FIXME *) 
35963  350 
val _ = 
351 
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

352 
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

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

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

355 
> map fst)) 
35963  356 
val relevant = 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

357 
relevant_facts ctxt relevance_convergence defs_relevant max_new 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

358 
relevance_override const_tab relevance_threshold 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

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

360 
(map (pair_consts_typs_axiom theory_relevant thy) 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

361 
axioms) 
35963  362 
in 
363 
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); 

364 
relevant 

365 
end 

24287  366 

367 
(***************************************************************) 

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

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

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

370 

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

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

372 

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

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

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

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

376 
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

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

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

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

380 
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

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

382 

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

383 
fun make_fact_table xs = 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

384 
fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

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

386 

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

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

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

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

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

391 

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

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

393 

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

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

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

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

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

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

399 

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

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

401 

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

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

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

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

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

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

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

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

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

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

411 

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

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

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

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

415 

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

416 
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

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

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

419 

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

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

421 
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

422 

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

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

425 

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

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

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

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

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

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

431 

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

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

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

434 

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

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

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

437 
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

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

439 
end 
37543  440 

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

441 
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

442 
let 
26675  443 
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); 
26278  444 
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

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

446 
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

447 

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

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

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

450 
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

451 
(respect_no_atp andalso is_package_def name) orelse 
38095  452 
member (op =) multi_base_blacklist (Long_Name.base_name name) orelse 
453 
String.isSuffix "_def_raw" (* FIXME: crude hack *) name then 

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

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

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

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

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

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

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

460 
 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

461 

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

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

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

464 
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

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

466 
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

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

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

469 
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

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

471 
end) 
26675  472 
in valid_facts global_facts @ valid_facts local_facts end; 
21224  473 

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

21224  476 

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

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

478 
 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

479 
 add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)) 
21224  480 

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

481 
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

482 

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

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

484 
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

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

487 
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

488 
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

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

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

491 
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

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

493 
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

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

495 
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

496 
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

497 
#> 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

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

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

500 
#> filter is_named 
19894  501 

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

502 
(***************************************************************) 
19194  503 
(* ATP invocation methods setup *) 
504 
(***************************************************************) 

505 

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

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

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

508 

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

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

510 
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

511 
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

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

513 

37348  514 
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

515 

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

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

517 
does not properly occur in the second operand. *) 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

518 
fun too_general_eqterms (Var z) t = 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

519 
not (exists_subterm (fn Var z' => z = z'  _ => false) t) 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

520 
 too_general_eqterms (Bound j) t = not (loose_bvar1 (t, j)) 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

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

522 

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

523 
fun too_general_equality (Const (@{const_name "op ="}, _) $ t1 $ t2) = 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

524 
too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1 
74dd8dd33512
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
blanchet
parents:
38279
diff
changeset

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

526 

29267  527 
fun has_typed_var tycons = exists_subterm 
528 
(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

529 

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

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

531 
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

532 
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

533 
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

534 
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

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

536 

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

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

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

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

540 
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

541 
 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

542 
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

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

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

545 

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

546 
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

547 
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

548 
(relevance_override as {add, del, only}) 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

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

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

551 
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

552 
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

553 
val has_override = not (null add) orelse not (null del) 
38279  554 
(* FIXME: 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

555 
val is_FO = forall Meson.is_fol_term thy (concl_t :: hyp_ts) 
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

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

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

558 
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

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

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

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

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

563 
member Thm.eq_thm add_thms th orelse 
38279  564 
((* FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*) 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37580
diff
changeset

565 
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

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

567 
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

568 
defs_relevant max_new theory_relevant relevance_override 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
diff
changeset

569 
thy axioms (concl_t :: hyp_ts) 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

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

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

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

573 

15347  574 
end; 