author  blanchet 
Thu, 12 Nov 2015 21:12:09 +0100  
changeset 61646  61995131cf28 
parent 61322  44f4ffe2b210 
child 61877  276ad4354069 
permissions  rwrr 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact.ML 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

2 
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

4 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

5 
Sledgehammer fact handling. 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

6 
*) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

7 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

8 
signature SLEDGEHAMMER_FACT = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

9 
sig 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

10 
type status = ATP_Problem_Generate.status 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

11 
type stature = ATP_Problem_Generate.stature 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

12 

51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
50815
diff
changeset

13 
type raw_fact = ((unit > string) * stature) * thm 
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
50815
diff
changeset

14 
type fact = (string * stature) * thm 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48292
diff
changeset

15 

48292  16 
type fact_override = 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57983
diff
changeset

17 
{add : (Facts.ref * Token.src list) list, 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57983
diff
changeset

18 
del : (Facts.ref * Token.src list) list, 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

19 
only : bool} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

20 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

21 
val instantiate_inducts : bool Config.T 
48292  22 
val no_fact_override : fact_override 
55212  23 

58919  24 
val fact_of_ref : Proof.context > Keyword.keywords > thm list > status Termtab.table > 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57983
diff
changeset

25 
Facts.ref * Token.src list > ((string * stature) * thm) list 
50047
45684acf0b94
thread context correctly when printing backquoted facts
blanchet
parents:
49981
diff
changeset

26 
val backquote_thm : Proof.context > thm > string 
50511
8825c36cb1ce
don't query blacklisted theorems in evaluation driver
blanchet
parents:
50510
diff
changeset

27 
val is_blacklisted_or_something : Proof.context > bool > string > bool 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

28 
val clasimpset_rule_table_of : Proof.context > status Termtab.table 
55212  29 
val build_name_tables : (thm > string) > ('a * thm) list > 
30 
string Symtab.table * string Symtab.table 

61322  31 
val fact_distinct : (term * term > bool) > ('a * thm) list > ('a * thm) list 
55212  32 
val maybe_instantiate_inducts : Proof.context > term list > term > 
33 
(((unit > string) * 'a) * thm) list > (((unit > string) * 'a) * thm) list 

51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
50815
diff
changeset

34 
val fact_of_raw_fact : raw_fact > fact 
58089
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

35 
val is_useful_unnamed_local_fact : Proof.context > thm > bool 
55212  36 

58919  37 
val all_facts : Proof.context > bool > bool > Keyword.keywords > thm list > thm list > 
55212  38 
status Termtab.table > raw_fact list 
58919  39 
val nearly_all_facts : Proof.context > bool > fact_override > Keyword.keywords > 
55212  40 
status Termtab.table > thm list > term list > term > raw_fact list 
54142
5f3c1b445253
no fact subsumption  this only confuses later code, e.g. 'add:'
blanchet
parents:
54112
diff
changeset

41 
val drop_duplicate_facts : raw_fact list > raw_fact list 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

42 
end; 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

43 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

44 
structure Sledgehammer_Fact : SLEDGEHAMMER_FACT = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

45 
struct 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

46 

50495
bd9a0028b063
better tautology check  don't reject "prod_cases3" for example
blanchet
parents:
50490
diff
changeset

47 
open ATP_Util 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

48 
open ATP_Problem_Generate 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

49 
open Sledgehammer_Util 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

50 

51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
50815
diff
changeset

51 
type raw_fact = ((unit > string) * stature) * thm 
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
50815
diff
changeset

52 
type fact = (string * stature) * thm 
48296
e7f01b7e244e
gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents:
48292
diff
changeset

53 

48292  54 
type fact_override = 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57983
diff
changeset

55 
{add : (Facts.ref * Token.src list) list, 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57983
diff
changeset

56 
del : (Facts.ref * Token.src list) list, 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

57 
only : bool} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

58 

60252
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59970
diff
changeset

59 
val local_thisN = Long_Name.localN ^ Long_Name.separator ^ Auto_Bind.thisN 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59970
diff
changeset

60 

54080
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

61 
(* gracefully handle huge background theories *) 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

62 
val max_facts_for_duplicates = 50000 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

63 
val max_facts_for_complex_check = 25000 
54083
824db6ab3339
crank up limit a bit  truly huge background theories are still nearly 3 times larger
blanchet
parents:
54081
diff
changeset

64 
val max_simps_for_clasimpset = 10000 
54080
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

65 

53511
3ea6b9461c55
got rid of another slowdown factor in relevance filter
blanchet
parents:
53510
diff
changeset

66 
(* experimental feature *) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

67 
val instantiate_inducts = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

68 
Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

69 

48292  70 
val no_fact_override = {add = [], del = [], only = false} 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

71 

58919  72 
fun needs_quoting keywords s = 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58919
diff
changeset

73 
Keyword.is_literal keywords s orelse 
50239  74 
exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

75 

58919  76 
fun make_name keywords multi j name = 
77 
(name > needs_quoting keywords name ? quote) ^ 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

78 
(if multi then "(" ^ string_of_int j ^ ")" else "") 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

79 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

80 
fun explode_interval _ (Facts.FromTo (i, j)) = i upto j 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

81 
 explode_interval max (Facts.From i) = i upto i + max  1 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

82 
 explode_interval _ (Facts.Single i) = [i] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

83 

61646  84 
val backquote = enclose "\<open>" "\<close>" 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

85 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

86 
(* unfolding these can yield really huge terms *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

87 
val risky_defs = @{thms Bit0_def Bit1_def} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

88 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

89 
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) 
57468  90 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

91 
fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t 
56245  92 
 is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2 
93 
 is_rec_def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

94 
 is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

95 
 is_rec_def _ = false 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

96 

59582  97 
fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms 
48396  98 
fun is_chained chained = member Thm.eq_thm_prop chained 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

99 

48396  100 
fun scope_of_thm global assms chained th = 
101 
if is_chained chained th then Chained 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

102 
else if global then Global 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

103 
else if is_assum assms th then Assum 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

104 
else Local 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

105 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

106 
val may_be_induction = 
57729  107 
exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => body_type T = @{typ bool} 
108 
 _ => false) 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

109 

54077  110 
(* TODO: get rid of *) 
53501  111 
fun normalize_vars t = 
112 
let 

113 
fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s 

114 
 normT (TVar (z as (_, S))) = 

115 
(fn ((knownT, nT), accum) => 

55286  116 
(case find_index (equal z) knownT of 
53501  117 
~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum)) 
55286  118 
 j => (TVar ((Name.uu, nT  j  1), S), ((knownT, nT), accum)))) 
53501  119 
 normT (T as TFree _) = pair T 
57468  120 

53501  121 
fun norm (t $ u) = norm t ##>> norm u #>> op $ 
122 
 norm (Const (s, T)) = normT T #>> curry Const s 

57729  123 
 norm (Var (z as (_, T))) = normT T 
53501  124 
#> (fn (T, (accumT, (known, n))) => 
57729  125 
(case find_index (equal z) known of 
126 
~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) 

127 
 j => (Var ((Name.uu, n  j  1), T), (accumT, (known, n))))) 

128 
 norm (Abs (_, T, t)) = norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t)) 

53501  129 
 norm (Bound j) = pair (Bound j) 
130 
 norm (Free (s, T)) = normT T #>> curry Free s 

131 
in fst (norm t (([], 0), ([], 0))) end 

132 

48396  133 
fun status_of_thm css name th = 
54081  134 
if Termtab.is_empty css then 
135 
General 

136 
else 

59582  137 
let val t = Thm.prop_of th in 
54081  138 
(* FIXME: use structured name *) 
139 
if String.isSubstring ".induct" name andalso may_be_induction t then 

140 
Induction 

141 
else 

142 
let val t = normalize_vars t in 

55286  143 
(case Termtab.lookup css t of 
54081  144 
SOME status => status 
145 
 NONE => 

146 
let val concl = Logic.strip_imp_concl t in 

55286  147 
(case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of 
54081  148 
SOME lrhss => 
149 
let 

150 
val prems = Logic.strip_imp_prems t 

151 
val t' = Logic.list_implies (prems, Logic.mk_equals lrhss) 

152 
in 

153 
Termtab.lookup css t' > the_default General 

154 
end 

55286  155 
 NONE => General) 
156 
end) 

54081  157 
end 
158 
end 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

159 

48396  160 
fun stature_of_thm global assms chained css name th = 
161 
(scope_of_thm global assms chained th, status_of_thm css name th) 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

162 

58919  163 
fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

164 
let 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

165 
val ths = Attrib.eval_thms ctxt [xthm] 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
57983
diff
changeset

166 
val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args) 
57468  167 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

168 
fun nth_name j = 
55286  169 
(case xref of 
59433  170 
Facts.Fact s => backquote (simplify_spaces (YXML.content_of s)) ^ bracket 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

171 
 Facts.Named (("", _), _) => "[" ^ bracket ^ "]" 
58919  172 
 Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

173 
 Facts.Named ((name, _), SOME intervals) => 
58919  174 
make_name keywords true 
55286  175 
(nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket) 
57468  176 

48396  177 
fun add_nth th (j, rest) = 
178 
let val name = nth_name j in 

57729  179 
(j + 1, ((name, stature_of_thm false [] chained css name th), th) :: rest) 
48396  180 
end 
57468  181 
in 
182 
(0, []) > fold add_nth ths > snd 

183 
end 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

184 

57729  185 
(* Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as 
186 
these are definitions arising from packages. *) 

50736  187 
fun is_package_def s = 
188 
let val ss = Long_Name.explode s in 

189 
length ss > 2 andalso not (hd ss = "local") andalso 

190 
exists (fn suf => String.isSuffix suf s) 

57729  191 
["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"] 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

192 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

193 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

194 
(* FIXME: put other record thms here, or declare as "no_atp" *) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

195 
fun multi_base_blacklist ctxt ho_atp = 
57729  196 
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps", 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57963
diff
changeset

197 
"eq.refl", "nchotomy", "case_cong", "case_cong_weak", "nat_of_char_simps", "nibble.simps", 
48440
159e320ef851
identified "evil" theories for MaSh  this is rather ad hoc, but so is MaSh anyway
blanchet
parents:
48438
diff
changeset

198 
"nibble.distinct"] 
57729  199 
> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"] 
48440
159e320ef851
identified "evil" theories for MaSh  this is rather ad hoc, but so is MaSh anyway
blanchet
parents:
48438
diff
changeset

200 
> map (prefix Long_Name.separator) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

201 

57729  202 
(* The maximum apply depth of any "metis" call in "Metis_Examples" (back in 2007) was 11. *) 
53529
1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

203 
val max_apply_depth = 18 
1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

204 

1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

205 
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) 
1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

206 
 apply_depth (Abs (_, _, t)) = apply_depth t 
1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

207 
 apply_depth _ = 0 
1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

208 

53533  209 
fun is_too_complex t = apply_depth t > max_apply_depth 
53529
1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

210 

48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

211 
(* FIXME: Ad hoc list *) 
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

212 
val technical_prefixes = 
57729  213 
["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence", "Limited_Sequence", "Meson", 
214 
"Metis", "Nitpick", "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing", 

50736  215 
"Random_Sequence", "Sledgehammer", "SMT"] 
48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

216 
> map (suffix Long_Name.separator) 
48440
159e320ef851
identified "evil" theories for MaSh  this is rather ad hoc, but so is MaSh anyway
blanchet
parents:
48438
diff
changeset

217 

57729  218 
fun is_technical_const s = exists (fn pref => String.isPrefix pref s) technical_prefixes 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

219 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

220 
(* FIXME: make more reliable *) 
53507  221 
val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator 
57468  222 

57729  223 
fun is_low_level_class_const s = 
53507  224 
s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

225 

60448  226 
val sep_that = Long_Name.separator ^ Auto_Bind.thatN 
54081  227 
val skolem_thesis = Name.skolem Auto_Bind.thesisN 
228 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

229 
fun is_that_fact th = 
59582  230 
exists_subterm (fn Free (s, _) => s = skolem_thesis  _ => false) (Thm.prop_of th) 
54081  231 
andalso String.isSuffix sep_that (Thm.get_name_hint th) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

232 

53513  233 
datatype interest = Deal_Breaker  Interesting  Boring 
234 

235 
fun combine_interests Deal_Breaker _ = Deal_Breaker 

236 
 combine_interests _ Deal_Breaker = Deal_Breaker 

237 
 combine_interests Interesting _ = Interesting 

238 
 combine_interests _ Interesting = Interesting 

239 
 combine_interests Boring Boring = Boring 

240 

54914
25212efcd0de
removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabellemetisproofstatecontainstheuniversalsort/20785045#20785045)
blanchet
parents:
54503
diff
changeset

241 
val type_has_top_sort = 
25212efcd0de
removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabellemetisproofstatecontainstheuniversalsort/20785045#20785045)
blanchet
parents:
54503
diff
changeset

242 
exists_subtype (fn TFree (_, []) => true  TVar (_, []) => true  _ => false) 
25212efcd0de
removed pointless warning (cf. http://stackoverflow.com/questions/20233463/isabellemetisproofstatecontainstheuniversalsort/20785045#20785045)
blanchet
parents:
54503
diff
changeset

243 

50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50512
diff
changeset

244 
fun is_likely_tautology_too_meta_or_too_technical th = 
48406  245 
let 
50053
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

246 
fun is_interesting_subterm (Const (s, _)) = 
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

247 
not (member (op =) atp_widely_irrelevant_consts s) 
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

248 
 is_interesting_subterm (Free _) = true 
fea589c8583e
fixed detection of tautologies  things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
blanchet
parents:
50049
diff
changeset

249 
 is_interesting_subterm _ = false 
57468  250 

53513  251 
fun interest_of_bool t = 
57729  252 
if exists_Const ((is_technical_const o fst) orf (is_low_level_class_const o fst) orf 
253 
type_has_top_sort o snd) t then 

53513  254 
Deal_Breaker 
255 
else if exists_type (exists_subtype (curry (op =) @{typ prop})) t orelse 

57729  256 
not (exists_subterm is_interesting_subterm t) then 
53513  257 
Boring 
258 
else 

259 
Interesting 

57468  260 

53513  261 
fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t 
56245  262 
 interest_of_prop Ts (@{const Pure.imp} $ t $ u) = 
53513  263 
combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u) 
56245  264 
 interest_of_prop Ts (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = 
54040  265 
if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t 
56245  266 
 interest_of_prop Ts ((t as Const (@{const_name Pure.all}, _)) $ u) = 
53513  267 
interest_of_prop Ts (t $ eta_expand Ts u 1) 
56245  268 
 interest_of_prop _ (Const (@{const_name Pure.eq}, _) $ t $ u) = 
53513  269 
combine_interests (interest_of_bool t) (interest_of_bool u) 
270 
 interest_of_prop _ _ = Deal_Breaker 

57468  271 

59582  272 
val t = Thm.prop_of th 
48406  273 
in 
57729  274 
(interest_of_prop [] t <> Interesting andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse 
53507  275 
is_that_fact th 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

276 
end 
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

277 

53512  278 
fun is_blacklisted_or_something ctxt ho_atp = 
57468  279 
let val blist = multi_base_blacklist ctxt ho_atp in 
280 
fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist 

281 
end 

50510  282 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

283 
(* This is a terrible hack. Free variables are sometimes coded as "M__" when 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

284 
they are displayed as "M" and we want to avoid clashes with these. But 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

285 
sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

286 
prefixes of all free variables. In the worse case scenario, where the fact 
49981  287 
won't be resolved correctly, the user can fix it manually, e.g., by giving a 
288 
name to the offending fact. *) 

57729  289 
fun all_prefixes_of s = map (fn i => String.extract (s, 0, SOME i)) (1 upto size s  1) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

290 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

291 
fun close_form t = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

292 
(t, [] > Term.add_free_names t > maps all_prefixes_of) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

293 
> fold (fn ((s, i), T) => fn (t', taken) => 
57729  294 
let val s' = singleton (Name.variant_list taken) s in 
295 
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const 

296 
else Logic.all_const) T 

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

298 
s' :: taken) 

299 
end) 

60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
60448
diff
changeset

300 
(Term.add_vars t [] > sort_by (fst o fst)) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

301 
> fst 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

302 

51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51160
diff
changeset

303 
fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote 
59582  304 
fun backquote_thm ctxt = backquote_term ctxt o Thm.prop_of 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48332
diff
changeset

305 

54084  306 
(* TODO: rewrite to use nets and/or to reuse existing data structures *) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

307 
fun clasimpset_rule_table_of ctxt = 
53502  308 
let val simps = ctxt > simpset_of > dest_ss > #simps in 
309 
if length simps >= max_simps_for_clasimpset then 

310 
Termtab.empty 

311 
else 

312 
let 

59582  313 
fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature) 
57468  314 

60943  315 
val {safeIs, (* safeEs, *) unsafeIs, (* unsafeEs, *) ...} = 
316 
ctxt > claset_of > Classical.rep_cs 

60945  317 
val intros = map #1 (Item_Net.content safeIs @ Item_Net.content unsafeIs) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

318 
(* Add once it is used: 
60943  319 
val elims = Item_Net.content safeEs @ Item_Net.content unsafeEs 
53502  320 
> map Classical.classical_rule 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

321 
*) 
57729  322 
val specs = Spec_Rules.get ctxt 
323 
val (rec_defs, nonrec_defs) = specs 

324 
> filter (curry (op =) Spec_Rules.Equational o fst) 

325 
> maps (snd o snd) 

326 
> filter_out (member Thm.eq_thm_prop risky_defs) 

59582  327 
> List.partition (is_rec_def o Thm.prop_of) 
57729  328 
val spec_intros = specs 
329 
> filter (member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] o fst) 

330 
> maps (snd o snd) 

53502  331 
in 
57468  332 
Termtab.empty 
333 
> fold (add Simp o snd) simps 

334 
> fold (add Rec_Def) rec_defs 

335 
> fold (add Non_Rec_Def) nonrec_defs 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

336 
(* Add once it is used: 
57468  337 
> fold (add Elim) elims 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

338 
*) 
57468  339 
> fold (add Intro) intros 
340 
> fold (add Inductive) spec_intros 

53502  341 
end 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

342 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

343 

54092  344 
fun normalize_eq (@{const Trueprop} $ (t as (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) = 
345 
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else t0 $ t2 $ t1 

346 
 normalize_eq (@{const Trueprop} $ (t as @{const Not} 

57729  347 
$ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) = 
54092  348 
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1) 
56245  349 
 normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) = 
54092  350 
(if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1)) 
351 
> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2) 

50481
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

352 
 normalize_eq t = t 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

353 

50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

354 
fun if_thm_before th th' = 
60948  355 
if Context.subthy_id (apply2 Thm.theory_id_of_thm (th, th')) then th else th' 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

356 

57468  357 
(* Hack: Conflate the facts about a class as seen from the outside with the corresponding lowlevel 
358 
facts, so that MaSh can learn from the lowlevel proofs. *) 

50734  359 
fun un_class_ify s = 
55286  360 
(case first_field "_class" s of 
50734  361 
SOME (pref, suf) => [s, pref ^ suf] 
55286  362 
 NONE => [s]) 
50734  363 

50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

364 
fun build_name_tables name_of facts = 
50733  365 
let 
59582  366 
fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (Thm.prop_of th)), th) 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

367 
fun add_plain canon alias = 
54092  368 
Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias)) 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

369 
fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases 
54092  370 
fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name) 
50815  371 
val prop_tab = fold cons_thm facts Termtab.empty 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

372 
val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

373 
val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty 
57108
dc0b4f50e288
more generous max number of suggestions, for more safety
blanchet
parents:
56245
diff
changeset

374 
in 
dc0b4f50e288
more generous max number of suggestions, for more safety
blanchet
parents:
56245
diff
changeset

375 
(plain_name_tab, inclass_name_tab) 
dc0b4f50e288
more generous max number of suggestions, for more safety
blanchet
parents:
56245
diff
changeset

376 
end 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

377 

54080
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

378 
fun fact_distinct eq facts = 
61322  379 
fold (fn (i, fact as (_, th)) => 
380 
Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd o snd)) 

381 
(normalize_eq (Thm.prop_of th), (i, fact))) 

382 
(tag_list 0 facts) Net.empty 

54076  383 
> Net.entries 
61322  384 
> sort (int_ord o apply2 fst) 
385 
> map snd 

53504  386 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

387 
fun struct_induct_rule_on th = 
59582  388 
(case Logic.strip_horn (Thm.prop_of th) of 
57729  389 
(prems, @{const Trueprop} $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

390 
if not (is_TVar ind_T) andalso length prems > 1 andalso 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

391 
exists (exists_subterm (curry (op aconv) p)) prems andalso 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

392 
not (exists (exists_subterm (curry (op aconv) a)) prems) then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

393 
SOME (p_name, ind_T) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

394 
else 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

395 
NONE 
55286  396 
 _ => NONE) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

397 

50586  398 
val instantiate_induct_timeout = seconds 0.01 
399 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

400 
fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

401 
let 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

402 
fun varify_noninducts (t as Free (s, T)) = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

403 
if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

404 
 varify_noninducts t = t 
57468  405 

57729  406 
val p_inst = concl_prop 
407 
> map_aterms varify_noninducts 

408 
> close_form 

409 
> lambda (Free ind_x) 

410 
> hackish_string_of_term ctxt 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

411 
in 
57729  412 
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), 
59755  413 
th > Rule_Insts.read_instantiate ctxt [(((p_name, 0), Position.none), p_inst)] []) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

414 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

415 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

416 
fun type_match thy (T1, T2) = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

417 
(Sign.typ_match thy (T2, T1) Vartab.empty; true) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

418 
handle Type.TYPE_MATCH => false 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

419 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

420 
fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = 
55286  421 
(case struct_induct_rule_on th of 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

422 
SOME (p_name, ind_T) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

423 
let val thy = Proof_Context.theory_of ctxt in 
55286  424 
stmt_xs 
425 
> filter (fn (_, T) => type_match thy (T, ind_T)) 

426 
> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout 

57729  427 
(instantiate_induct_rule ctxt stmt p_name ax))) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

428 
end 
55286  429 
 NONE => [ax]) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

430 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

431 
fun external_frees t = 
55948  432 
[] > Term.add_frees t > filter_out (Name.is_internal o fst) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

433 

1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

434 
fun maybe_instantiate_inducts ctxt hyp_ts concl_t = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

435 
if Config.get ctxt instantiate_inducts then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

436 
let 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

437 
val ind_stmt = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

438 
(hyp_ts > filter_out (null o external_frees), concl_t) 
59970  439 
> Logic.list_implies > Object_Logic.atomize_term ctxt 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

440 
val ind_stmt_xs = external_frees ind_stmt 
57729  441 
in 
442 
maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) 

443 
end 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

444 
else 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

445 
I 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

446 

51004
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
50815
diff
changeset

447 
fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th) 
5f2788c38127
distinguish raw and nonraw facts, using raw for 10 000s of facts and nonraw after selection of some hundreds
blanchet
parents:
50815
diff
changeset

448 

53532
4ad9599a0847
disable some checks for huge background theories
blanchet
parents:
53531
diff
changeset

449 
fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0 
4ad9599a0847
disable some checks for huge background theories
blanchet
parents:
53531
diff
changeset

450 

58089
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

451 
fun is_useful_unnamed_local_fact ctxt = 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

452 
let 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

453 
val thy = Proof_Context.theory_of ctxt 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

454 
val global_facts = Global_Theory.facts_of thy 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

455 
val local_facts = Proof_Context.facts_of ctxt 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

456 
val named_locals = Facts.dest_static true [global_facts] local_facts 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

457 
in 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

458 
fn th => 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

459 
not (Thm.has_name_hint th) andalso 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

460 
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

461 
end 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

462 

58919  463 
fun all_facts ctxt generous ho_atp keywords add_ths chained css = 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

464 
let 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

465 
val thy = Proof_Context.theory_of ctxt 
61054  466 
val transfer = Global_Theory.transfer_theories thy; 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

467 
val global_facts = Global_Theory.facts_of thy 
53532
4ad9599a0847
disable some checks for huge background theories
blanchet
parents:
53531
diff
changeset

468 
val is_too_complex = 
57729  469 
if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false 
470 
else is_too_complex 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

471 
val local_facts = Proof_Context.facts_of ctxt 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

472 
val assms = Assumption.all_assms_of ctxt 
58089
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

473 
val named_locals = Facts.dest_static true [global_facts] local_facts 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

474 
val unnamed_locals = 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

475 
Facts.props local_facts 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

476 
> filter (is_useful_unnamed_local_fact ctxt) 
20e76da3a0ef
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
blanchet
parents:
58011
diff
changeset

477 
> map (pair "" o single) 
57468  478 

57729  479 
val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) 
53512  480 
val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp 
57468  481 

56141
c06202417c4a
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
wenzelm
parents:
56140
diff
changeset

482 
fun add_facts global foldx facts = 
54081  483 
foldx (fn (name0, ths) => fn accum => 
50512
c283bc0a8f1a
tweaked which facts are included for MaSh evaluations
blanchet
parents:
50511
diff
changeset

484 
if name0 <> "" andalso 
59916  485 
(Long_Name.is_hidden (Facts.intern facts name0) orelse 
58226
04faf6dc262e
never include hidden names  these cannot be referenced afterward
blanchet
parents:
58089
diff
changeset

486 
((Facts.is_concealed facts name0 orelse 
04faf6dc262e
never include hidden names  these cannot be referenced afterward
blanchet
parents:
58089
diff
changeset

487 
(not generous andalso is_blacklisted_or_something name0)) andalso 
04faf6dc262e
never include hidden names  these cannot be referenced afterward
blanchet
parents:
58089
diff
changeset

488 
forall (not o member Thm.eq_thm_prop add_ths) ths)) then 
54081  489 
accum 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

490 
else 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

491 
let 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

492 
val n = length ths 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

493 
val multi = n > 1 
57468  494 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

495 
fun check_thms a = 
55286  496 
(case try (Proof_Context.get_thms ctxt) a of 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

497 
NONE => false 
55286  498 
 SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

499 
in 
61054  500 
snd (fold_rev (fn th0 => fn (j, accum) => 
501 
let val th = transfer th0 in 

502 
(j  1, 

503 
if not (member Thm.eq_thm_prop add_ths th) andalso 

504 
(is_likely_tautology_too_meta_or_too_technical th orelse 

505 
is_too_complex (Thm.prop_of th)) then 

506 
accum 

507 
else 

508 
let 

509 
fun get_name () = 

510 
if name0 = "" orelse name0 = local_thisN then 

511 
backquote_thm ctxt th 

512 
else 

513 
let val short_name = Facts.extern ctxt facts name0 in 

514 
if check_thms short_name then 

515 
short_name 

516 
else 

517 
let val long_name = Name_Space.extern ctxt full_space name0 in 

518 
if check_thms long_name then 

519 
long_name 

520 
else 

521 
name0 

522 
end 

523 
end 

524 
> make_name keywords multi j 

525 
val stature = stature_of_thm global assms chained css name0 th 

526 
val new = ((get_name, stature), th) 

527 
in 

528 
(if multi then apsnd else apfst) (cons new) accum 

529 
end) 

530 
end) ths (n, accum)) 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

531 
end) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

532 
in 
57729  533 
(* The singletheorem names go before the multipletheorem ones (e.g., "xxx" vs. "xxx(3)"), so 
534 
that single names are preferred when both are available. *) 

535 
`I [] 

536 
> add_facts false fold local_facts (unnamed_locals @ named_locals) 

537 
> add_facts true Facts.fold_static global_facts global_facts 

538 
> op @ 

48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

539 
end 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

540 

58919  541 
fun nearly_all_facts ctxt ho_atp {add, del, only} keywords css chained hyp_ts concl_t = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

542 
if only andalso null add then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

543 
[] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

544 
else 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

545 
let 
57729  546 
val chained = chained > maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th]) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

547 
in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

548 
(if only then 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

549 
maps (map (fn ((name, stature), th) => ((K name, stature), th)) 
58919  550 
o fact_of_ref ctxt keywords chained css) add 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

551 
else 
54080
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

552 
let 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset

553 
val (add, del) = apply2 (Attrib.eval_thms ctxt) (add, del) 
54080
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

554 
val facts = 
58919  555 
all_facts ctxt false ho_atp keywords add chained css 
54143
18def1c73c79
make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents:
54142
diff
changeset

556 
> filter_out ((member Thm.eq_thm_prop del orf 
57963  557 
(Named_Theorems.member ctxt @{named_theorems no_atp} andf 
558 
not o member Thm.eq_thm_prop add)) o snd) 

54080
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

559 
in 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

560 
facts 
48292  561 
end) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

562 
> maybe_instantiate_inducts ctxt hyp_ts concl_t 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

563 
end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

564 

54142
5f3c1b445253
no fact subsumption  this only confuses later code, e.g. 'add:'
blanchet
parents:
54112
diff
changeset

565 
fun drop_duplicate_facts facts = 
54112
9c0f464d1854
drop only real duplicates, not subsumed facts  this confuses MaSh
blanchet
parents:
54092
diff
changeset

566 
let val num_facts = length facts in 
54142
5f3c1b445253
no fact subsumption  this only confuses later code, e.g. 'add:'
blanchet
parents:
54112
diff
changeset

567 
facts > num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv) 
54112
9c0f464d1854
drop only real duplicates, not subsumed facts  this confuses MaSh
blanchet
parents:
54092
diff
changeset

568 
end 
9c0f464d1854
drop only real duplicates, not subsumed facts  this confuses MaSh
blanchet
parents:
54092
diff
changeset

569 

48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

570 
end; 