author  blanchet 
Sun, 03 May 2015 22:15:29 +0200  
changeset 60252  2c468c062589 
parent 59970  e9f73d87d904 
child 60448  78f3c67bc35e 
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 

31 
val maybe_instantiate_inducts : Proof.context > term list > term > 

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

33 
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

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

58919  36 
val all_facts : Proof.context > bool > bool > Keyword.keywords > thm list > thm list > 
55212  37 
status Termtab.table > raw_fact list 
58919  38 
val nearly_all_facts : Proof.context > bool > fact_override > Keyword.keywords > 
55212  39 
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

40 
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

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

42 

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

43 
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

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

45 

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

46 
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

47 
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

48 
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

49 

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

50 
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

51 
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

52 

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

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

55 
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

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

57 

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

58 
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

59 

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

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

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

62 
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

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

64 

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

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

66 
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

67 
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

68 

48292  69 
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

70 

58919  71 
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

72 
Keyword.is_literal keywords s orelse 
50239  73 
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

74 

58919  75 
fun make_name keywords multi j name = 
76 
(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

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

78 

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

79 
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

80 
 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

81 
 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

82 

57727
02a53c1bbb6c
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
blanchet
parents:
57469
diff
changeset

83 
val backquote = raw_explode #> map (fn "`" => "\\`"  s => s) #> implode #> enclose "`" "`" 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

84 

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

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

86 
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

87 

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

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

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

90 
fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t 
56245  91 
 is_rec_def (@{const Pure.imp} $ _ $ t2) = is_rec_def t2 
92 
 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

93 
 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

94 
 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

95 

59582  96 
fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms 
48396  97 
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

98 

48396  99 
fun scope_of_thm global assms chained th = 
100 
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

101 
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

102 
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

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

104 

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

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

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

108 

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

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

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

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

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

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

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

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

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

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

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

131 

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

135 
else 

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

139 
Induction 

140 
else 

141 
let val t = normalize_vars t in 

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

145 
let val concl = Logic.strip_imp_concl t in 

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

149 
val prems = Logic.strip_imp_prems t 

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

151 
in 

152 
Termtab.lookup css t' > the_default General 

153 
end 

55286  154 
 NONE => General) 
155 
end) 

54081  156 
end 
157 
end 

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

158 

48396  159 
fun stature_of_thm global assms chained css name th = 
160 
(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

161 

58919  162 
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

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

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

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

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

167 
fun nth_name j = 
55286  168 
(case xref of 
59433  169 
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

170 
 Facts.Named (("", _), _) => "[" ^ bracket ^ "]" 
58919  171 
 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

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

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

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

182 
end 

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

183 

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

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

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

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

57729  190 
["_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

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

192 

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

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

194 
fun multi_base_blacklist ctxt ho_atp = 
57729  195 
["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

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

197 
"nibble.distinct"] 
57729  198 
> 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

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

200 

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

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

203 

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

204 
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

205 
 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

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

207 

53533  208 
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

209 

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

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

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

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

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

216 

57729  217 
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

218 

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

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

57729  222 
fun is_low_level_class_const s = 
53507  223 
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

224 

53509  225 
val sep_that = Long_Name.separator ^ Obtain.thatN 
54081  226 
val skolem_thesis = Name.skolem Auto_Bind.thesisN 
227 

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

228 
fun is_that_fact th = 
59582  229 
exists_subterm (fn Free (s, _) => s = skolem_thesis  _ => false) (Thm.prop_of th) 
54081  230 
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

231 

53513  232 
datatype interest = Deal_Breaker  Interesting  Boring 
233 

234 
fun combine_interests Deal_Breaker _ = Deal_Breaker 

235 
 combine_interests _ Deal_Breaker = Deal_Breaker 

236 
 combine_interests Interesting _ = Interesting 

237 
 combine_interests _ Interesting = Interesting 

238 
 combine_interests Boring Boring = Boring 

239 

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

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

241 
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

242 

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

243 
fun is_likely_tautology_too_meta_or_too_technical th = 
48406  244 
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

245 
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

246 
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

247 
 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

248 
 is_interesting_subterm _ = false 
57468  249 

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

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

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

258 
Interesting 

57468  259 

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

57468  270 

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

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

276 

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

280 
end 

50510  281 

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

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

283 
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

284 
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

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

57729  288 
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

289 

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

290 
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

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

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

295 
else Logic.all_const) T 

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

297 
s' :: taken) 

298 
end) 

299 
(Term.add_vars t [] > sort_wrt (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

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

301 

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

302 
fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote 
59582  303 
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

304 

54084  305 
(* 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

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

309 
Termtab.empty 

310 
else 

311 
let 

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

57729  314 
val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = ctxt > claset_of > Classical.rep_cs 
53502  315 
val intros = Item_Net.content safeIs @ Item_Net.content hazIs 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

316 
(* Add once it is used: 
57729  317 
val elims = Item_Net.content safeEs @ Item_Net.content hazEs 
53502  318 
> 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

319 
*) 
57729  320 
val specs = Spec_Rules.get ctxt 
321 
val (rec_defs, nonrec_defs) = specs 

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

323 
> maps (snd o snd) 

324 
> filter_out (member Thm.eq_thm_prop risky_defs) 

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

328 
> maps (snd o snd) 

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

332 
> fold (add Rec_Def) rec_defs 

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

334 
(* Add once it is used: 
57468  335 
> 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

336 
*) 
57468  337 
> fold (add Intro) intros 
338 
> fold (add Inductive) spec_intros 

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

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

341 

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

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

57729  345 
$ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) = 
54092  346 
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1) 
56245  347 
 normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) = 
54092  348 
(if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1)) 
349 
> (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

350 
 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

351 

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

352 
fun if_thm_before th th' = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset

353 
if Theory.subthy (apply2 Thm.theory_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

354 

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

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

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

362 
fun build_name_tables name_of facts = 
50733  363 
let 
59582  364 
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

365 
fun add_plain canon alias = 
54092  366 
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

367 
fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases 
54092  368 
fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name) 
50815  369 
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

370 
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

371 
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

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

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

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

375 

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

376 
fun fact_distinct eq facts = 
54076  377 
fold (fn fact as (_, th) => 
59582  378 
Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd)) 
379 
(normalize_eq (Thm.prop_of th), fact)) 

54077  380 
facts Net.empty 
54076  381 
> Net.entries 
53504  382 

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

383 
fun struct_induct_rule_on th = 
59582  384 
(case Logic.strip_horn (Thm.prop_of th) of 
57729  385 
(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

386 
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

387 
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

388 
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

389 
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

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

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

393 

50586  394 
val instantiate_induct_timeout = seconds 0.01 
395 

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

396 
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

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

398 
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

399 
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

400 
 varify_noninducts t = t 
57468  401 

57729  402 
val p_inst = concl_prop 
403 
> map_aterms varify_noninducts 

404 
> close_form 

405 
> lambda (Free ind_x) 

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

407 
in 
57729  408 
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), 
59755  409 
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

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

411 

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

412 
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

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

414 
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

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 instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = 
55286  417 
(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

418 
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

419 
let val thy = Proof_Context.theory_of ctxt in 
55286  420 
stmt_xs 
421 
> filter (fn (_, T) => type_match thy (T, ind_T)) 

422 
> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout 

57729  423 
(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

424 
end 
55286  425 
 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

426 

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

427 
fun external_frees t = 
55948  428 
[] > 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

429 

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

430 
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

431 
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

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

433 
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

434 
(hyp_ts > filter_out (null o external_frees), concl_t) 
59970  435 
> 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

436 
val ind_stmt_xs = external_frees ind_stmt 
57729  437 
in 
438 
maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) 

439 
end 

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

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

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

442 

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

443 
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

444 

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

445 
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

446 

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

447 
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

448 
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

449 
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

450 
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

451 
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

452 
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

453 
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

454 
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

455 
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

456 
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

457 
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

458 

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

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

461 
val thy = Proof_Context.theory_of ctxt 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

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

463 
val is_too_complex = 
57729  464 
if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false 
465 
else is_too_complex 

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

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

467 
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

468 
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

469 
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

470 
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

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

472 
> map (pair "" o single) 
57468  473 

57729  474 
val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) 
53512  475 
val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp 
57468  476 

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

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

479 
if name0 <> "" andalso 
59916  480 
(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

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

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

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

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

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

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

488 
val multi = n > 1 
57468  489 

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

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

492 
NONE => false 
55286  493 
 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

494 
in 
57469
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

495 
snd (fold_rev (fn th => fn (j, accum) => 
54081  496 
(j  1, 
497 
if not (member Thm.eq_thm_prop add_ths th) andalso 

498 
(is_likely_tautology_too_meta_or_too_technical th orelse 

59582  499 
is_too_complex (Thm.prop_of th)) then 
54081  500 
accum 
501 
else 

502 
let 

57469
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

503 
fun get_name () = 
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

504 
if name0 = "" orelse name0 = local_thisN then 
57469
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

505 
backquote_thm ctxt th 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

506 
else 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

507 
let val short_name = Facts.extern ctxt facts name0 in 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

508 
if check_thms short_name then 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

509 
short_name 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

510 
else 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

511 
let val long_name = Name_Space.extern ctxt full_space name0 in 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

512 
if check_thms long_name then 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

513 
long_name 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

514 
else 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

515 
name0 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

516 
end 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

517 
end 
58919  518 
> make_name keywords multi j 
57469
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

519 
val stature = stature_of_thm global assms chained css name0 th 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

520 
val new = ((get_name, stature), th) 
54081  521 
in 
57469
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

522 
(if multi then apsnd else apfst) (cons new) accum 
54081  523 
end)) ths (n, accum)) 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

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

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

528 
`I [] 

529 
> add_facts false fold local_facts (unnamed_locals @ named_locals) 

530 
> add_facts true Facts.fold_static global_facts global_facts 

531 
> op @ 

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

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

533 

58919  534 
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

535 
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

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

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

538 
let 
57729  539 
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

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

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

542 
maps (map (fn ((name, stature), th) => ((K name, stature), th)) 
58919  543 
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

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

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

546 
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

547 
val facts = 
58919  548 
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

549 
> filter_out ((member Thm.eq_thm_prop del orf 
57963  550 
(Named_Theorems.member ctxt @{named_theorems no_atp} andf 
551 
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

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

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

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

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

557 

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

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

559 
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

560 
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

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

562 

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

563 
end; 