author  wenzelm 
Fri, 03 Apr 2015 18:36:19 +0200  
changeset 59916  f673ce6b1e2b 
parent 59888  27e4d0ab0948 
child 59970  e9f73d87d904 
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 

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

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

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

60 
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

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

62 

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

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

64 
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

65 
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

66 

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

68 

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

70 
Keyword.is_literal keywords s orelse 
50239  71 
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

72 

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

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

76 

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

77 
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

78 
 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

79 
 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

80 

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

81 
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

82 

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

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

84 
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

85 

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

86 
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) 
57468  87 

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

91 
 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

92 
 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

93 

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

96 

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

99 
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

100 
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

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

102 

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

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

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

106 

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

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

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

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

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

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

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

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

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

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

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

129 

48396  130 
fun status_of_thm css name th = 
54081  131 
if Termtab.is_empty css then 
132 
General 

133 
else 

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

137 
Induction 

138 
else 

139 
let val t = normalize_vars t in 

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

143 
let val concl = Logic.strip_imp_concl t in 

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

147 
val prems = Logic.strip_imp_prems t 

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

149 
in 

150 
Termtab.lookup css t' > the_default General 

151 
end 

55286  152 
 NONE => General) 
153 
end) 

54081  154 
end 
155 
end 

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

156 

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

159 

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

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

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

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

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

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

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

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

48396  174 
fun add_nth th (j, rest) = 
175 
let val name = nth_name j in 

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

180 
end 

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

181 

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

50736  184 
fun is_package_def s = 
185 
let val ss = Long_Name.explode s in 

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

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

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

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

190 

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

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

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

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

195 
"nibble.distinct"] 
57729  196 
> 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

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

198 

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

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

201 

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

202 
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

203 
 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

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

205 

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

207 

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

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

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

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

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

214 

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

216 

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

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

57729  220 
fun is_low_level_class_const s = 
53507  221 
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

222 

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

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

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

229 

53513  230 
datatype interest = Deal_Breaker  Interesting  Boring 
231 

232 
fun combine_interests Deal_Breaker _ = Deal_Breaker 

233 
 combine_interests _ Deal_Breaker = Deal_Breaker 

234 
 combine_interests Interesting _ = Interesting 

235 
 combine_interests _ Interesting = Interesting 

236 
 combine_interests Boring Boring = Boring 

237 

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

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

239 
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

240 

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

241 
fun is_likely_tautology_too_meta_or_too_technical th = 
48406  242 
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

243 
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

244 
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

245 
 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

246 
 is_interesting_subterm _ = false 
57468  247 

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

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

57729  253 
not (exists_subterm is_interesting_subterm t) then 
53513  254 
Boring 
255 
else 

256 
Interesting 

57468  257 

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

57468  268 

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

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

274 

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

278 
end 

50510  279 

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

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

281 
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

282 
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

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

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

287 

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

288 
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

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

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

293 
else Logic.all_const) T 

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

295 
s' :: taken) 

296 
end) 

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

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

299 

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

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

302 

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

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

307 
Termtab.empty 

308 
else 

309 
let 

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

57729  312 
val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = ctxt > claset_of > Classical.rep_cs 
53502  313 
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

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

317 
*) 
57729  318 
val specs = Spec_Rules.get ctxt 
319 
val (rec_defs, nonrec_defs) = specs 

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

321 
> maps (snd o snd) 

322 
> filter_out (member Thm.eq_thm_prop risky_defs) 

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

326 
> maps (snd o snd) 

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

330 
> fold (add Rec_Def) rec_defs 

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

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

334 
*) 
57468  335 
> fold (add Intro) intros 
336 
> fold (add Inductive) spec_intros 

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

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

339 

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

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

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

348 
 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

349 

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

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

351 
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

352 

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

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

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

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

363 
fun add_plain canon alias = 
54092  364 
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

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

368 
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

369 
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

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

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

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

373 

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

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

54077  378 
facts Net.empty 
54076  379 
> Net.entries 
53504  380 

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

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

384 
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

385 
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

386 
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

387 
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

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

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

391 

50586  392 
val instantiate_induct_timeout = seconds 0.01 
393 

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

394 
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

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

396 
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

397 
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

398 
 varify_noninducts t = t 
57468  399 

57729  400 
val p_inst = concl_prop 
401 
> map_aterms varify_noninducts 

402 
> close_form 

403 
> lambda (Free ind_x) 

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

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

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

409 

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

410 
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

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

412 
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

413 

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

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

416 
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

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

420 
> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout 

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

422 
end 
55286  423 
 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

424 

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

425 
fun external_frees t = 
55948  426 
[] > 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

427 

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

428 
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

429 
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

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

431 
val thy = Proof_Context.theory_of ctxt 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

432 
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

433 
(hyp_ts > filter_out (null o external_frees), concl_t) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

434 
> Logic.list_implies > Object_Logic.atomize_term thy 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

438 
end 

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

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

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

441 

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

442 
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

443 

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

444 
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

445 

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

446 
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

447 
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

448 
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

449 
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

450 
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

451 
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

452 
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

453 
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

454 
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

455 
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

456 
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

457 

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

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

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

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

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

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

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

466 
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

467 
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

468 
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

469 
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

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

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

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

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

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

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

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

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

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

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

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

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

487 
val multi = n > 1 
57468  488 

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

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

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

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

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

497 
(is_likely_tautology_too_meta_or_too_technical th orelse 

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

501 
let 

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

502 
fun get_name () = 
29e7e6e89a0e
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
blanchet
parents:
57468
diff
changeset

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

504 
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

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

506 
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

507 
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

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

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

510 
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

511 
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

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

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

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

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

516 
end 
58919  517 
> 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

518 
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

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

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

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

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

527 
`I [] 

528 
> add_facts false fold local_facts (unnamed_locals @ named_locals) 

529 
> add_facts true Facts.fold_static global_facts global_facts 

530 
> op @ 

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 

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

534 
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

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

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

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

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

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

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

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

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

545 
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

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

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

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

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

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

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

556 

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

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

558 
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

559 
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

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

561 

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

562 
end; 