author  blanchet 
Wed, 25 Aug 2010 09:42:28 +0200  
changeset 38743  69fa75354c58 
parent 38742  4fe1bb9e7434 
child 38744  2b6333f78a9e 
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 
38617  14 
val name_thms_pair_from_ref : 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

15 
Proof.context > unit Symtab.table > thm list > Facts.ref 
38699  16 
> (unit > string * bool) * 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 : 
38741  18 
bool > real > real > 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 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38697
diff
changeset

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

35826  23 
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = 
15347  24 
struct 
25 

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

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

27 

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

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

29 
fun trace_msg msg = if !trace then tracing (msg ()) else () 
35826  30 

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

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

32 

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

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

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

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

36 
only: bool} 
21070  37 

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

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

39 

38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

40 
fun name_thms_pair_from_ref ctxt reserved chained_ths xref = 
38699  41 
let val ths = ProofContext.get_fact ctxt xref in 
42 
(fn () => let 

43 
val name = Facts.string_of_ref xref 

44 
val name = name > Symtab.defined reserved name ? quote 

45 
val chained = forall (member Thm.eq_thm chained_ths) ths 

46 
in (name, chained) end, ths) 

47 
end 

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?*) 

38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

67 
fun const_mem const_tab (c, c_typ) = 
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

68 
exists (match_types c_typ) (these (Symtab.lookup const_tab c)) 
37505
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.*) 

38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

83 
fun add_const_to_table (c, ctyps) = 
37502  84 
Symtab.map_default (c, [ctyps]) 
85 
(fn [] => []  ctypss => insert (op =) ctyps ctypss) 

24287  86 

38692  87 
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) 
88 

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

89 
val fresh_prefix = "Sledgehammer.FRESH." 
37537  90 
val flip = Option.map not 
38091  91 
(* These are typically simplified away by "Meson.presimplify". *) 
38682  92 
val boring_consts = 
93 
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}] 

37537  94 

38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

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

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

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

98 
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

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

38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

102 
Const x => add_const_to_table (const_with_typ thy x) 
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

103 
 Free (s, _) => add_const_to_table (s, []) 
38688  104 
 t1 $ t2 => fold do_term [t1, t2] 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

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

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

109 
#> (if will_surely_be_skolemized then 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

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

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

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

113 
and do_term_or_formula T = 
38692  114 
if is_formula_type T then do_formula NONE else do_term 
37537  115 
and do_formula pos t = 
116 
case t of 

117 
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

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

121 
 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

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

125 
 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

126 
do_quantifier (pos = SOME false) body_t 
37537  127 
 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

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

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

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

133 
 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

134 
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

135 
 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

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

137 
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

138 
 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

139 
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

140 
 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

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

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

143 
 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

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

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

148 
 _ => do_term t 

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

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

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

152 
end 
24287  153 

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

155 
takes the given theory into account.*) 

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

156 
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

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

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

159 
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

160 
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

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

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

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

164 

24287  165 
(**** Constant / Type Frequencies ****) 
166 

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

169 
latter, we need a linear ordering on "const_typ list". *) 

24287  170 

38743  171 
fun const_typ_ord p = 
172 
case p of 

173 
(CTVar, CTVar) => EQUAL 

174 
 (CTVar, CType _) => LESS 

175 
 (CType _, CTVar) => GREATER 

176 
 (CType q1, CType q2) => 

177 
prod_ord fast_string_ord (dict_ord const_typ_ord) (q1, q2) 

24287  178 

38743  179 
structure CTtab = 
180 
Table(type key = const_typ list val ord = dict_ord const_typ_ord) 

24287  181 

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

182 
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

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

184 
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

185 
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

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

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

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

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

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

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

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

193 
 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

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

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

196 
in th > theory_const_prop_of theory_relevant > do_term end 
24287  197 

198 

199 
(**** Actual Filtering Code ****) 

200 

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

202 
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

203 
CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m) 
38686  204 
(the (Symtab.lookup const_tab c)) 0 
205 
handle Option.Option => 0 

206 

24287  207 

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

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

209 
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

210 

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

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

212 
frequencies. *) 
38686  213 
fun rel_log (x : real) = 1.0 + 2.0 / Math.ln (x + 1.0) 
214 
fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4 

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

215 

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

216 
(* Computes a constant's weight, as determined by its frequency. *) 
38686  217 
val rel_const_weight = rel_log o real oo const_frequency 
218 
val irrel_const_weight = irrel_log o real oo const_frequency 

38692  219 
(* fun irrel_const_weight _ _ = 1.0 FIXME: OLD CODE *) 
24287  220 

38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

221 
fun axiom_weight const_tab relevant_consts axiom_consts = 
38686  222 
let 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

223 
val (rel, irrel) = List.partition (const_mem relevant_consts) axiom_consts 
38686  224 
val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0 
225 
val irrel_weight = fold (curry Real.+ o irrel_const_weight const_tab) irrel 0.0 

226 
val res = rel_weight / (rel_weight + irrel_weight) 

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

228 

229 
(* OLD CODE: 

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

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

232 
which are rare, would harm a formula's chances of being picked.*) 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

233 
fun axiom_weight const_tab relevant_consts axiom_consts = 
38101
34b75b71235d
handle division by zero gracefully (used to raise Unordered later on)
blanchet
parents:
38095
diff
changeset

234 
let 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

235 
val rel = filter (const_mem relevant_consts) axiom_consts 
38686  236 
val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

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

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

240 

38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

241 
fun consts_of_term thy t = 
38742  242 
Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys) 
243 
(get_consts thy (SOME true) [t]) [] 

24287  244 

38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

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

246 
(axiom, axiom > snd > theory_const_prop_of theory_relevant 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

247 
> consts_of_term thy) 
24287  248 

38699  249 
type annotated_thm = 
250 
((unit > string * bool) * 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

251 

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

253 
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) 
24287  254 

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

255 
(* Limit the number of new facts, to prevent runaway acceptance. *) 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

256 
fun take_best max_relevant_per_iter (new_pairs : (annotated_thm * real) list) = 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

257 
let val nnew = length new_pairs in 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

258 
if nnew <= max_relevant_per_iter then 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

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

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

261 
let 
38687
97509445c569
cache previous iteration's weights, and keep track of what's dirty and what's clean;
blanchet
parents:
38686
diff
changeset

262 
val new_pairs = sort compare_pairs new_pairs 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

263 
val accepted = List.take (new_pairs, max_relevant_per_iter) 
24287  264 
in 
37505
d9af5c01dc4a
added code to optionally perform fact filtering on the original (nonCNF) formulas
blanchet
parents:
37504
diff
changeset

265 
trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

266 
", exceeds the limit of " ^ Int.toString max_relevant_per_iter)); 
35865  267 
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); 
268 
trace_msg (fn () => "Actually passed: " ^ 

38699  269 
space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted)); 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

270 
(map #1 accepted, List.drop (new_pairs, max_relevant_per_iter)) 
24287  271 
end 
272 
end; 

273 

38683
23266607cb81
if no facts were selected on first iteration, try again with a lower threshold
blanchet
parents:
38682
diff
changeset

274 
val threshold_divisor = 2.0 
23266607cb81
if no facts were selected on first iteration, try again with a lower threshold
blanchet
parents:
38682
diff
changeset

275 
val ridiculous_threshold = 0.1 
23266607cb81
if no facts were selected on first iteration, try again with a lower threshold
blanchet
parents:
38682
diff
changeset

276 

38741  277 
fun relevance_filter ctxt relevance_threshold relevance_decay 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

278 
max_relevant_per_iter theory_relevant 
38594  279 
({add, del, ...} : relevance_override) axioms goal_ts = 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

281 
val thy = ProofContext.theory_of ctxt 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

282 
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

283 
Symtab.empty 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

284 
val goal_const_tab = get_consts thy (SOME false) goal_ts 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

285 
val _ = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

286 
trace_msg (fn () => "Initial constants: " ^ 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

287 
commas (goal_const_tab > Symtab.dest 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

288 
> filter (curry (op <>) [] o snd) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

289 
> map fst)) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

290 
val add_thms = maps (ProofContext.get_fact ctxt) add 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

291 
val del_thms = maps (ProofContext.get_fact ctxt) del 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

292 
fun iter j threshold rel_const_tab = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

294 
fun relevant ([], rejects) [] = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

295 
(* Nothing was added this iteration. *) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

296 
if j = 0 andalso threshold >= ridiculous_threshold then 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

297 
(* First iteration? Try again. *) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

298 
iter 0 (threshold / threshold_divisor) rel_const_tab 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

299 
(map (apsnd SOME) rejects) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

301 
(* Add "add:" facts. *) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

302 
if null add_thms then 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

303 
[] 
38594  304 
else 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

305 
map_filter (fn ((p as (_, th), _), _) => 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

306 
if member Thm.eq_thm add_thms th then SOME p 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

307 
else NONE) rejects 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

308 
 relevant (new_pairs, rejects) [] = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

310 
val (new_rels, more_rejects) = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

311 
take_best max_relevant_per_iter new_pairs 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

312 
val rel_const_tab' = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

313 
rel_const_tab > fold add_const_to_table (maps snd new_rels) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

314 
fun is_dirty c = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

315 
const_mem rel_const_tab' c andalso 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

316 
not (const_mem rel_const_tab c) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

317 
val rejects = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

318 
more_rejects @ rejects 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

319 
> map (fn (ax as (_, consts), old_weight) => 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

320 
(ax, if exists is_dirty consts then NONE 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

321 
else SOME old_weight)) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

322 
val threshold = threshold + (1.0  threshold) * relevance_decay 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

324 
trace_msg (fn () => "relevant this iteration: " ^ 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

325 
Int.toString (length new_rels)); 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

326 
map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

328 
 relevant (new_rels, rejects) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

329 
(((ax as ((name, th), axiom_consts)), cached_weight) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

330 
:: rest) = 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

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

334 
SOME w => w 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

335 
 NONE => axiom_weight const_tab rel_const_tab axiom_consts 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

336 
in 
38741  337 
if weight >= threshold then 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

338 
(trace_msg (fn () => 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

339 
fst (name ()) ^ " passes: " ^ Real.toString weight 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

340 
^ " consts: " ^ commas (map fst axiom_consts)); 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

341 
relevant ((ax, weight) :: new_rels, rejects) rest) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

343 
relevant (new_rels, (ax, weight) :: rejects) rest 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

346 
trace_msg (fn () => "relevant_facts, current threshold: " ^ 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

347 
Real.toString threshold); 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

348 
relevant ([], []) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

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

351 
axioms > filter_out (member Thm.eq_thm del_thms o snd) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

352 
> map (rpair NONE o pair_consts_axiom theory_relevant thy) 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

353 
> iter 0 relevance_threshold goal_const_tab 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

354 
> tap (fn res => trace_msg (fn () => 
38686  355 
"Total relevant: " ^ Int.toString (length res))) 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

356 
end 
24287  357 

358 
(***************************************************************) 

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

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

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

361 

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

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

363 

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

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

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

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

367 
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

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

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

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

371 
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

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

373 

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

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

375 
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

376 
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

377 

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

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

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

380 
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", 
38682  381 
"split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", 
382 
"case_cong", "weak_case_cong"] 

383 
> map (prefix ".") 

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

384 

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

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

386 

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

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

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

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

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

391 
 term_has_too_many_lambdas _ _ = false 
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 
(* 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

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

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

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

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

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

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

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

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

402 

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

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

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

406 

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

407 
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

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

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

410 

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

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

412 
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

413 

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

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

416 

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

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

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

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

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

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

422 

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

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

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

425 

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

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

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

428 

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

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

430 
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

431 
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

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

433 

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

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

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

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

437 
let 
38629  438 
fun is_bad_equal (Var z) t = 
439 
not (exists_subterm (fn Var z' => z = z'  _ => false) t) 

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

441 
 is_bad_equal _ _ = false 

442 
fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 

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

443 
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

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

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

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

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

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

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

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

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

452 
 (_, @{const "==>"} $ t1 $ t2) => 
38629  453 
do_formula (not pos) t1 andalso 
454 
(t2 = @{prop False} orelse do_formula pos t2) 

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

455 
 (_, @{const "op >"} $ t1 $ t2) => 
38629  456 
do_formula (not pos) t1 andalso 
457 
(t2 = @{const False} orelse do_formula pos t2) 

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

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

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

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

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

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

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

464 
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

465 

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

466 
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

467 
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

468 
 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

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

470 

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

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

472 
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

473 
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

474 
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

475 
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

476 
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

477 

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

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

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

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

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

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

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

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

487 

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

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

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

490 
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

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

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

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

494 

38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

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

496 
let 
38697
9bbd5141d0a1
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
blanchet
parents:
38696
diff
changeset

497 
val is_chained = member Thm.eq_thm chained_ths 
9bbd5141d0a1
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
blanchet
parents:
38696
diff
changeset

498 
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt) 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

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

500 
val named_locals = local_facts > Facts.dest_static [] 
38697
9bbd5141d0a1
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
blanchet
parents:
38696
diff
changeset

501 
(* Unnamed, not chained formulas with schematic variables are omitted, 
9bbd5141d0a1
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
blanchet
parents:
38696
diff
changeset

502 
because they are rejected by the backticks (`...`) parser for some 
9bbd5141d0a1
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
blanchet
parents:
38696
diff
changeset

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

504 
fun is_good_unnamed_local th = 
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

505 
forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals 
0ce517c1970f
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for nonprintable characters  and avoid those in ``style facts
blanchet
parents:
38699
diff
changeset

506 
andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) 
38644
25bbbaf7ce65
don't penalize abstractions in relevance filter + support nameless `foo`style facts
blanchet
parents:
38629
diff
changeset

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

508 
local_facts > Facts.props > filter is_good_unnamed_local 
38697
9bbd5141d0a1
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
blanchet
parents:
38696
diff
changeset

509 
> map (pair "" o single) 
38627
760a2d5cc671
make sure minimizer facts go through "transform_elim_theorems"
blanchet
parents:
38617
diff
changeset

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

511 
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) 
38697
9bbd5141d0a1
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
blanchet
parents:
38696
diff
changeset

512 
fun add_valid_facts foldx facts = 
38699  513 
foldx (fn (name0, ths) => 
514 
if name0 <> "" andalso 

515 
forall (not o member Thm.eq_thm add_thms) ths andalso 

516 
(Facts.is_concealed facts name0 orelse 

517 
(respect_no_atp andalso is_package_def name0) orelse 

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

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

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

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

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

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

524 
fun backquotify th = 
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

525 
"`" ^ Print_Mode.setmp [Print_Mode.input] 
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

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

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

528 
> simplify_spaces 
38699  529 
fun check_thms a = 
530 
case try (ProofContext.get_thms ctxt) a of 

531 
NONE => false 

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

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

533 
in 
38699  534 
pair 1 
535 
#> fold (fn th => fn (j, rest) => 

536 
(j + 1, 

537 
if is_theorem_bad_for_atps full_types th andalso 

538 
not (member Thm.eq_thm add_thms th) then 

539 
rest 

540 
else 

541 
(fn () => 

542 
(if name0 = "" then 

543 
th > backquotify 

544 
else 

545 
let 

546 
val name1 = Facts.extern facts name0 

547 
val name2 = Name_Space.extern full_space name0 

548 
in 

549 
case find_first check_thms [name1, name2, name0] of 

550 
SOME name => 

551 
let 

552 
val name = 

553 
name > Symtab.defined reserved name ? quote 

554 
in 

555 
if multi then name ^ "(" ^ Int.toString j ^ ")" 

556 
else name 

557 
end 

558 
 NONE => "" 

559 
end, is_chained th), (multi, th)) :: rest)) ths 

560 
#> snd 

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

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

562 
in 
38688  563 
[] > add_valid_facts fold local_facts (unnamed_locals @ named_locals) 
564 
> add_valid_facts Facts.fold_static global_facts global_facts 

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

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

566 

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

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

568 
names are preferred when both are available. *) 
38699  569 
fun name_thm_pairs ctxt respect_no_atp = 
570 
List.partition (fst o snd) #> op @ 

571 
#> map (apsnd snd) 

572 
#> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) 

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

573 

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

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

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

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

577 

38741  578 
fun relevant_facts full_types relevance_threshold relevance_decay 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

579 
max_relevant_per_iter 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

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

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

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

583 
val add_thms = maps (ProofContext.get_fact ctxt) add 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38692
diff
changeset

584 
val reserved = reserved_isar_keyword_table () 
37538
97ab019d5ac8
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
blanchet
parents:
37537
diff
changeset

585 
val axioms = 
38699  586 
(if only then 
587 
maps ((fn (n, ths) => map (pair n o pair false) ths) 

588 
o name_thms_pair_from_ref ctxt reserved chained_ths) add 

589 
else 

590 
all_name_thms_pairs ctxt reserved full_types add_thms chained_ths) 

38688  591 
> name_thm_pairs ctxt (respect_no_atp andalso not only) 
38595
bbb0982656eb
make sure that "add:" doesn't influence the relevance filter too much
blanchet
parents:
38594
diff
changeset

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

593 
in 
38688  594 
trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^ 
595 
" theorems"); 

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

596 
(if relevance_threshold > 1.0 then 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

598 
else if relevance_threshold < 0.0 then 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

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

600 
else 
38741  601 
relevance_filter ctxt relevance_threshold relevance_decay 
38739
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

602 
max_relevant_per_iter theory_relevant relevance_override 
8b8ed80b5699
renamed "relevance_convergence" to "relevance_decay"
blanchet
parents:
38738
diff
changeset

603 
axioms (concl_t :: hyp_ts)) 
38699  604 
> map (apfst (fn f => f ())) 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38697
diff
changeset

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

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

607 

15347  608 
end; 