author  blanchet 
Fri, 20 Aug 2010 17:52:26 +0200  
changeset 38627  760a2d5cc671 
parent 38617  f7b32911340b 
child 38629  3387432c18af 
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 
38617  15 
val name_thms_pair_from_ref : 
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 

38617  40 
fun name_thms_pair_from_ref ctxt chained_ths xref = 
41 
let 

42 
val ths = ProofContext.get_fact ctxt xref 

43 
val name = Facts.string_of_ref xref 

44 
> forall (member Thm.eq_thm chained_ths) ths 

45 
? prefix chained_prefix 

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

46 
in (name, ths > map Clausifier.transform_elim_theorem) end 
38617  47 

37616
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 

24287  53 
(*** constants with types ***) 
54 

55 
(*An abstraction of Isabelle types*) 

56 
datatype const_typ = CTVar  CType of string * const_typ list 

57 

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

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

62 
 match_type _ CTVar = false 

63 
and match_types [] [] = true 

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

65 

66 
(*Is there a unifiable constant?*) 

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

67 
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

68 
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

69 

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

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

74 

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

76 
fun const_with_typ thy (c,typ) = 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38595
diff
changeset

77 
let val tvars = Sign.const_typargs thy (c,typ) in 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38595
diff
changeset

78 
(c, map const_typ_of tvars) end 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38595
diff
changeset

79 
handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*) 
24287  80 

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

82 
which we ignore.*) 

37502  83 
fun add_const_type_to_table (c, ctyps) = 
84 
Symtab.map_default (c, [ctyps]) 

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

24287  86 

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

87 
val fresh_prefix = "Sledgehammer.Fresh." 
37537  88 
val flip = Option.map not 
38091  89 
(* These are typically simplified away by "Meson.presimplify". *) 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38595
diff
changeset

90 
val boring_consts = 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38595
diff
changeset

91 
[@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)] 
37537  92 

93 
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

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

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

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

97 
introduce a fresh constant to simulate the effect of Skolemization. *) 
37537  98 
fun do_term t = 
99 
case t of 

38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38595
diff
changeset

100 
Const x => add_const_type_to_table (const_with_typ thy x) 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38595
diff
changeset

101 
 Free (s, _) => add_const_type_to_table (s, []) 
37537  102 
 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

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

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

105 
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

106 
#> do_term t 
37537  107 
 _ => I 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

108 
fun do_quantifier will_surely_be_skolemized body_t = 
37537  109 
do_formula pos body_t 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

110 
#> (if will_surely_be_skolemized then 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

111 
add_const_type_to_table (gensym fresh_prefix, []) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

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

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

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

115 
if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE 
ae6bb801e583
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
blanchet
parents:
38587
diff
changeset

116 
else do_term 
37537  117 
and do_formula pos t = 
118 
case t of 

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

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

120 
do_quantifier (pos = SOME false) body_t 
37537  121 
 @{const "==>"} $ t1 $ t2 => 
122 
do_formula (flip pos) t1 #> do_formula pos t2 

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

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

124 
fold (do_term_or_formula T) [t1, t2] 
37537  125 
 @{const Trueprop} $ t1 => do_formula pos t1 
126 
 @{const Not} $ t1 => do_formula (flip pos) t1 

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

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

128 
do_quantifier (pos = SOME false) body_t 
37537  129 
 Const (@{const_name Ex}, _) $ Abs (_, _, body_t) => 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

130 
do_quantifier (pos = SOME true) body_t 
37537  131 
 @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 
132 
 @{const "op "} $ t1 $ t2 => fold (do_formula pos) [t1, t2] 

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

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

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

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

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

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

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

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

140 
 Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) => 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

141 
do_quantifier (is_some pos) body_t 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

142 
 Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) => 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

143 
do_quantifier (pos = SOME false) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

144 
(HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t)) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

145 
 Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) => 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

146 
do_quantifier (pos = SOME true) 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

147 
(HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t)) 
37537  148 
 (t0 as Const (_, @{typ bool})) $ t1 => 
149 
do_term t0 #> do_formula pos t1 (* theory constant *) 

150 
 _ => do_term t 

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

151 
in 
38091  152 
Symtab.empty > fold (Symtab.update o rpair []) boring_consts 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37626
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) = 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38595
diff
changeset

193 
let val (c, cts) = const_with_typ thy (a, T) in 
37503
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 
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

201 
 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

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

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

204 
in th > theory_const_prop_of theory_relevant > do_term end 
24287  205 

206 

207 
(**** Actual Filtering Code ****) 

208 

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

210 
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

211 
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

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

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

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

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

216 
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

217 

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

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

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

220 
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

221 

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

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

223 
val ct_weight = log_weight2 o real oo const_frequency 
24287  224 

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

225 
(*Relevant constants are weighted according to frequency, 
24287  226 
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

227 
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

228 
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

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

230 
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

231 
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

232 
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

233 
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

234 

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

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

238 
fun consts_typs_of_term thy t = 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

239 
Symtab.fold add_expand_pairs (get_consts_typs thy (SOME true) [t]) [] 
24287  240 

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

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

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

243 
> consts_typs_of_term thy) 
24287  244 

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

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

246 

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

247 
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

248 
 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

249 
 dest_Const_or_Free _ = raise CONST_OR_FREE () 
24287  250 

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

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

254 
fun defs lhs rhs = 
24287  255 
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

256 
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

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

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

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

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

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

265 
defs lhs rhs 
35963  266 
 _ => false 
24287  267 
end; 
268 

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

269 
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

270 

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

272 
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) 
24287  273 

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

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

275 
fun take_best max_new (newpairs : (annotated_thm * real) list) = 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

276 
let val nnew = length newpairs in 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

277 
if nnew <= max_new then 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

278 
(map #1 newpairs, []) 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

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

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

281 
val newpairs = sort compare_pairs newpairs 
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

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

284 
trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

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

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

288 
space_implode ", " (map (fst o fst o fst) accepted)); 
38587
1317657d6aa9
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
blanchet
parents:
38395
diff
changeset

289 
(map #1 accepted, map #1 (List.drop (newpairs, max_new))) 
24287  290 
end 
291 
end; 

292 

36922  293 
fun relevance_filter ctxt relevance_threshold relevance_convergence 
38594  294 
defs_relevant max_new theory_relevant 
295 
({add, del, ...} : relevance_override) 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

296 
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

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

298 
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

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

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

302 
val thy = ProofContext.theory_of ctxt 
37503
c2dfa26b9da6
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
blanchet
parents:
37502
diff
changeset

303 
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

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

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

306 
val relevance_threshold = 0.8 * relevance_threshold (* FIXME *) 
35963  307 
val _ = 
308 
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

309 
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

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

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

312 
> map fst)) 
38594  313 
val add_thms = maps (ProofContext.get_fact ctxt) add 
314 
val del_thms = maps (ProofContext.get_fact ctxt) del 

315 
fun iter threshold rel_const_tab = 

316 
let 

317 
fun relevant ([], rejects) [] = 

318 
(* Nothing was added this iteration: Add "add:" facts. *) 

319 
if null add_thms then 

320 
[] 

321 
else 

322 
map_filter (fn (p as (name, th), _) => 

323 
if member Thm.eq_thm add_thms th then SOME p 

324 
else NONE) rejects 

325 
 relevant (newpairs, rejects) [] = 

326 
let 

327 
val (newrels, more_rejects) = take_best max_new newpairs 

328 
val new_consts = maps #2 newrels 

329 
val rel_const_tab = 

330 
rel_const_tab > fold add_const_type_to_table new_consts 

331 
val threshold = 

332 
threshold + (1.0  threshold) / relevance_convergence 

333 
in 

334 
trace_msg (fn () => "relevant this iteration: " ^ 

335 
Int.toString (length newrels)); 

336 
map #1 newrels @ iter threshold rel_const_tab 

337 
(more_rejects @ rejects) 

338 
end 

339 
 relevant (newrels, rejects) 

340 
((ax as ((name, th), consts_typs)) :: axs) = 

341 
let 

342 
val weight = 

343 
if member Thm.eq_thm del_thms th then 0.0 

344 
else formula_weight const_tab rel_const_tab consts_typs 

345 
in 

346 
if weight >= threshold orelse 

347 
(defs_relevant andalso defines thy th rel_const_tab) then 

348 
(trace_msg (fn () => 

349 
name ^ " passes: " ^ Real.toString weight 

350 
(* ^ " consts: " ^ commas (map fst consts_typs) *)); 

351 
relevant ((ax, weight) :: newrels, rejects) axs) 

352 
else 

353 
relevant (newrels, ax :: rejects) axs 

354 
end 

355 
in 

356 
trace_msg (fn () => "relevant_facts, current threshold: " ^ 

357 
Real.toString threshold); 

358 
relevant ([], []) 

359 
end 

360 
val relevant = iter relevance_threshold goal_const_tab 

361 
(map (pair_consts_typs_axiom theory_relevant thy) 

362 
axioms) 

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

365 
relevant 

366 
end 

24287  367 

368 
(***************************************************************) 

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

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

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

371 

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

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

373 

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

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

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

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

377 
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

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

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

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

381 
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

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

383 

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

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

385 
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

386 
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

387 

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

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

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

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

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

392 

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

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

394 

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

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

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

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

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

399 
 term_has_too_many_lambdas _ _ = false 
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 
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) 
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 
(* 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

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

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

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

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

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

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

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

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

412 

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

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

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

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

416 

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

417 
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

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

419 
 apply_depth _ = 0 
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 
fun is_formula_too_complex t = 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38027
diff
changeset

422 
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

423 

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

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

426 

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

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

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

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

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

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

432 

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

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

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

435 

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

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

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

438 

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

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

440 
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

441 
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

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

443 

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

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

445 
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

446 
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

447 
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

448 
 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

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

450 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

465 
do_formula (not pos) t1 andalso do_formula pos t2 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

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

467 
do_formula (not pos) t1 andalso do_formula pos t2 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

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

469 
 (true, @{const "op "} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

470 
 (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2] 
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

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

472 
 (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 
38615
4e1d828ee514
improve "x = A  x = B  x = C"style axiom detection
blanchet
parents:
38611
diff
changeset

473 
 (_, @{const False}) => true 
4e1d828ee514
improve "x = A  x = B  x = C"style axiom detection
blanchet
parents:
38611
diff
changeset

474 
 (_, @{const True}) => true 
38607
a2abe8c2a1c2
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
blanchet
parents:
38606
diff
changeset

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

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

477 

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

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

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

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

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

482 

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

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

484 
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

485 
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

486 
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

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

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

489 

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

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

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

492 
are omitted. *) 
38593  493 
fun is_dangerous_term full_types t = 
38609  494 
not full_types andalso 
495 
(has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t) 

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

496 

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

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

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

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

500 
is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

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

503 

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

504 
fun all_name_thms_pairs ctxt full_types add_thms chained_ths = 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

506 
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

507 
val local_facts = ProofContext.facts_of ctxt; 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

509 
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

510 

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

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

512 
(facts, []) > Facts.fold_static (fn (name, ths0) => 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

513 
if (Facts.is_concealed facts name orelse 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

514 
(respect_no_atp andalso is_package_def name) orelse 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

515 
member (op =) multi_base_blacklist (Long_Name.base_name name) orelse 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

516 
String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

517 
forall (not o member Thm.eq_thm add_thms) ths0 then 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

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

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

521 
fun check_thms a = 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

522 
(case try (ProofContext.get_thms ctxt) a of 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

523 
NONE => false 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

524 
 SOME ths1 => Thm.eq_thms (ths0, ths1)) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

525 
val name1 = Facts.extern facts name; 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

526 
val name2 = Name_Space.extern full_space name; 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

528 
ths0 > map Clausifier.transform_elim_theorem 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

529 
> filter ((not o is_theorem_bad_for_atps full_types) orf 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

530 
member Thm.eq_thm add_thms) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

532 
case find_first check_thms [name1, name2, name] of 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

533 
NONE => I 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

534 
 SOME name' => 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

535 
cons (name' > forall (member Thm.eq_thm chained_ths) ths 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

536 
? prefix chained_prefix, ths) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

538 
in valid_facts global_facts @ valid_facts local_facts end; 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

539 

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

540 
fun multi_name a th (n, pairs) = 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

541 
(n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

542 

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

543 
fun add_names (_, []) pairs = pairs 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

544 
 add_names (a, [th]) pairs = (a, th) :: pairs 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

545 
 add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

546 

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

547 
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

548 

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

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

550 
names are preferred when both are available. *) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

551 
fun name_thm_pairs ctxt respect_no_atp name_thms_pairs = 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

553 
val (mults, singles) = List.partition is_multi name_thms_pairs 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

554 
val ps = [] > fold add_names singles > fold add_names mults 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

555 
in ps > respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

556 

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

557 
fun is_named ("", th) = 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

558 
(warning ("No name for theorem " ^ 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

559 
Display.string_of_thm_without_context th); false) 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

560 
 is_named _ = true 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

561 
fun checked_name_thm_pairs respect_no_atp ctxt = 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

563 
#> tap (fn ps => trace_msg 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

564 
(fn () => ("Considering " ^ Int.toString (length ps) ^ 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

566 
#> filter is_named 
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

567 

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

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

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

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

571 

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

572 
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

573 
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

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

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

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

577 
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

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

579 
checked_name_thm_pairs (respect_no_atp andalso not only) ctxt 
38617  580 
(if only then map (name_thms_pair_from_ref ctxt chained_ths) add 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

581 
else all_name_thms_pairs ctxt full_types add_thms chained_ths) 
38595
bbb0982656eb
make sure that "add:" doesn't influence the relevance filter too much
blanchet
parents:
38594
diff
changeset

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

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

584 
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

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

586 
axioms (concl_t :: hyp_ts) 
38595
bbb0982656eb
make sure that "add:" doesn't influence the relevance filter too much
blanchet
parents:
38594
diff
changeset

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

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

589 

15347  590 
end; 