author  blanchet 
Tue, 15 Oct 2013 15:26:58 +0200  
changeset 54112  9c0f464d1854 
parent 54092  1e2585f56509 
child 54142  5f3c1b445253 
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 = 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

18 
del : (Facts.ref * Attrib.src list) list, 
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 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

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

24 
Proof.context > unit Symtab.table > thm list > status Termtab.table 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

25 
> Facts.ref * Attrib.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 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

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

30 
(thm > string) > ('a * thm) list 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

31 
> string Symtab.table * string Symtab.table 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

33 
Proof.context > term list > term > (((unit > string) * 'a) * thm) list 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

35 
val fact_of_raw_fact : raw_fact > fact 
48530
d443166f9520
repaired accessibility chains generated by MaSh exporter + tuned one function out
blanchet
parents:
48440
diff
changeset

36 
val all_facts : 
50442
4f6a4d32522c
don't blacklist "case" theorems  this causes problems in MaSh later
blanchet
parents:
50239
diff
changeset

37 
Proof.context > bool > bool > unit Symtab.table > thm list > 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

38 
> status Termtab.table > 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

39 
val nearly_all_facts : 
48299  40 
Proof.context > bool > fact_override > unit Symtab.table 
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

41 
> status Termtab.table > thm list > term list > term > raw_fact list 
54112
9c0f464d1854
drop only real duplicates, not subsumed facts  this confuses MaSh
blanchet
parents:
54092
diff
changeset

42 
val drop_duplicate_facts: theory > 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

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

44 

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

45 
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

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

47 

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

48 
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

49 
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

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

51 
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

52 

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

53 
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

54 
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

55 

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

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

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

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

60 

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

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

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

63 
val max_facts_for_duplicate_matching = 25000 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

64 
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

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

66 

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

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

68 
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

69 
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

70 

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

72 

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

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

74 
Symtab.defined reserved s orelse 
50239  75 
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

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 make_name reserved multi j name = 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

78 
(name > needs_quoting reserved name ? quote) ^ 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

80 

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

81 
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

82 
 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

83 
 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

84 

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

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

86 
raw_explode #> map (fn "`" => "\\`"  s => s) #> implode #> enclose "`" "`" 
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 
(* 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

89 
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

90 

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

91 
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

92 
fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t 
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 ==>} $ _ $ t2) = is_rec_def 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 (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

95 
 is_rec_def (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

96 
 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

97 

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

98 
fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms 
48396  99 
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

100 

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

103 
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

104 
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

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

106 

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

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

108 
exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

109 
body_type T = @{typ bool} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

111 

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

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

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

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

118 
case find_index (equal z) knownT of 

119 
~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum)) 

120 
 j => (TVar ((Name.uu, nT  j  1), S), ((knownT, nT), accum))) 

121 
 normT (T as TFree _) = pair T 

122 
fun norm (t $ u) = norm t ##>> norm u #>> op $ 

123 
 norm (Const (s, T)) = normT T #>> curry Const s 

124 
 norm (Var (z as (_, T))) = 

125 
normT T 

126 
#> (fn (T, (accumT, (known, n))) => 

127 
case find_index (equal z) known of 

128 
~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1))) 

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

130 
 norm (Abs (_, T, t)) = 

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

132 
 norm (Bound j) = pair (Bound j) 

133 
 norm (Free (s, T)) = normT T #>> curry Free s 

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

135 

48396  136 
fun status_of_thm css name th = 
54081  137 
if Termtab.is_empty css then 
138 
General 

139 
else 

140 
let val t = prop_of th in 

141 
(* FIXME: use structured name *) 

142 
if String.isSubstring ".induct" name andalso may_be_induction t then 

143 
Induction 

144 
else 

145 
let val t = normalize_vars t in 

146 
case Termtab.lookup css t of 

147 
SOME status => status 

148 
 NONE => 

149 
let val concl = Logic.strip_imp_concl t in 

150 
case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of 

151 
SOME lrhss => 

152 
let 

153 
val prems = Logic.strip_imp_prems t 

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

155 
in 

156 
Termtab.lookup css t' > the_default General 

157 
end 

158 
 NONE => General 

159 
end 

160 
end 

161 
end 

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

162 

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

165 

52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

166 
fun fact_of_ref ctxt reserved 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

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

168 
val ths = Attrib.eval_thms ctxt [xthm] 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

170 
map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

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

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

174 
Facts.Fact s => backquote s ^ bracket 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

175 
 Facts.Named (("", _), _) => "[" ^ bracket ^ "]" 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

176 
 Facts.Named ((name, _), NONE) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

177 
make_name reserved (length ths > 1) (j + 1) name ^ bracket 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

178 
 Facts.Named ((name, _), SOME intervals) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

180 
(nth (maps (explode_interval (length ths)) intervals) j) name ^ 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

181 
bracket 
48396  182 
fun add_nth th (j, rest) = 
183 
let val name = nth_name j in 

184 
(j + 1, ((name, stature_of_thm false [] chained css name th), th) 

185 
:: rest) 

186 
end 

187 
in (0, []) > fold add_nth ths > snd end 

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

188 

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

189 
(* Reject theorems with names like "List.filter.filter_list_def" or 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

190 
"Accessible_Part.acc.defs", as these are definitions arising from packages. *) 
50736  191 
fun is_package_def s = 
192 
let val ss = Long_Name.explode s in 

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

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

195 
["_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

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

197 

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

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

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

200 
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", 
50442
4f6a4d32522c
don't blacklist "case" theorems  this causes problems in MaSh later
blanchet
parents:
50239
diff
changeset

201 
"ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", 
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
51126
diff
changeset

202 
"weak_case_cong", "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

203 
"nibble.distinct"] 
53531  204 
> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

205 
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

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

207 

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

208 
(* The maximum apply depth of any "metis" call in "Metis_Examples" (on 
1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

209 
20071031) was 11. *) 
1eb7c65b526c
reverted f99ee3adb81d  that old logic seems to make a difference still today
blanchet
parents:
53513
diff
changeset

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

211 

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

212 
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

213 
 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

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

215 

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

217 

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

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

219 
val technical_prefixes = 
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
51004
diff
changeset

220 
["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence", 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
51004
diff
changeset

221 
"Limited_Sequence", "Meson", "Metis", "Nitpick", 
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
51004
diff
changeset

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

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

225 

53507  226 
fun is_technical_const (s, _) = 
48667
ac58317ef11f
rule out same "technical" theories for MePo as for MaSh
blanchet
parents:
48530
diff
changeset

227 
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

228 

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

229 
(* FIXME: make more reliable *) 
53507  230 
val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator 
231 
fun is_low_level_class_const (s, _) = 

232 
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

233 

53509  234 
val sep_that = Long_Name.separator ^ Obtain.thatN 
235 

54081  236 
val skolem_thesis = Name.skolem Auto_Bind.thesisN 
237 

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

238 
fun is_that_fact th = 
54081  239 
exists_subterm (fn Free (s, _) => s = skolem_thesis  _ => false) (prop_of th) 
240 
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

241 

53513  242 
datatype interest = Deal_Breaker  Interesting  Boring 
243 

244 
fun combine_interests Deal_Breaker _ = Deal_Breaker 

245 
 combine_interests _ Deal_Breaker = Deal_Breaker 

246 
 combine_interests Interesting _ = Interesting 

247 
 combine_interests _ Interesting = Interesting 

248 
 combine_interests Boring Boring = Boring 

249 

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

250 
fun is_likely_tautology_too_meta_or_too_technical th = 
48406  251 
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

252 
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

253 
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

254 
 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

255 
 is_interesting_subterm _ = false 
53513  256 
fun interest_of_bool t = 
53545
f7e987ef7304
reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
blanchet
parents:
53533
diff
changeset

257 
if exists_Const (is_technical_const orf is_low_level_class_const orf 
f7e987ef7304
reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
blanchet
parents:
53533
diff
changeset

258 
type_has_top_sort o snd) t then 
53513  259 
Deal_Breaker 
260 
else if exists_type (exists_subtype (curry (op =) @{typ prop})) t orelse 

261 
not (exists_subterm is_interesting_subterm t) then 

262 
Boring 

263 
else 

264 
Interesting 

265 
fun interest_of_prop _ (@{const Trueprop} $ t) = interest_of_bool t 

266 
 interest_of_prop Ts (@{const "==>"} $ t $ u) = 

267 
combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u) 

268 
 interest_of_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) = 

54040  269 
if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t 
53513  270 
 interest_of_prop Ts ((t as Const (@{const_name all}, _)) $ u) = 
271 
interest_of_prop Ts (t $ eta_expand Ts u 1) 

272 
 interest_of_prop _ (Const (@{const_name "=="}, _) $ t $ u) = 

273 
combine_interests (interest_of_bool t) (interest_of_bool u) 

274 
 interest_of_prop _ _ = Deal_Breaker 

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

275 
val t = prop_of th 
48406  276 
in 
53513  277 
(interest_of_prop [] t <> Interesting andalso 
278 
not (Thm.eq_thm_prop (@{thm ext}, th))) orelse 

53507  279 
is_that_fact th 
48438
3e45c98fe127
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents:
48437
diff
changeset

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

281 

53512  282 
fun is_blacklisted_or_something ctxt ho_atp = 
283 
let 

284 
val blist = multi_base_blacklist ctxt ho_atp 

285 
fun is_blisted name = 

286 
is_package_def name orelse exists (fn s => String.isSuffix s name) blist 

287 
in is_blisted end 

50510  288 

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

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

290 
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

291 
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

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

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

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

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

297 

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

298 
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

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

300 
> fold (fn ((s, i), T) => fn (t', taken) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

301 
let val s' = singleton (Name.variant_list taken) s in 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

302 
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

304 
$ Abs (s', T, abstract_over (Var ((s, i), T), t')), 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

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

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

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

309 

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

310 
fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote 
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51160
diff
changeset

311 
fun backquote_thm ctxt = backquote_term ctxt o 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

312 

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

314 
fun clasimpset_rule_table_of ctxt = 
53502  315 
let val simps = ctxt > simpset_of > dest_ss > #simps in 
316 
if length simps >= max_simps_for_clasimpset then 

317 
Termtab.empty 

318 
else 

319 
let 

320 
fun add stature th = 

321 
Termtab.update (normalize_vars (prop_of th), stature) 

322 
val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = 

323 
ctxt > claset_of > Classical.rep_cs 

324 
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

325 
(* Add once it is used: 
53502  326 
val elims = 
327 
Item_Net.content safeEs @ Item_Net.content hazEs 

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

329 
*) 
53502  330 
val specs = ctxt > Spec_Rules.get 
331 
val (rec_defs, nonrec_defs) = 

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

333 
> maps (snd o snd) 

334 
> filter_out (member Thm.eq_thm_prop risky_defs) 

335 
> List.partition (is_rec_def o prop_of) 

336 
val spec_intros = 

337 
specs > filter (member (op =) [Spec_Rules.Inductive, 

338 
Spec_Rules.Co_Inductive] o fst) 

339 
> maps (snd o snd) 

340 
in 

341 
Termtab.empty > fold (add Simp o snd) simps 

342 
> fold (add Rec_Def) rec_defs 

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

344 
(* Add once it is used: 
53502  345 
> 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

346 
*) 
53502  347 
> fold (add Intro) intros 
348 
> fold (add Inductive) spec_intros 

349 
end 

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

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

351 

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

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

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

355 
$ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) = 
54092  356 
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1) 
357 
 normalize_eq (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) = 

358 
(if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1)) 

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

360 
 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

361 

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

362 
fun if_thm_before th th' = 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

363 
if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th' 
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

364 

50734  365 
(* Hack: Conflate the facts about a class as seen from the outside with the 
366 
corresponding lowlevel facts, so that MaSh can learn from the lowlevel 

367 
proofs. *) 

368 
fun un_class_ify s = 

369 
case first_field "_class" s of 

370 
SOME (pref, suf) => [s, pref ^ suf] 

371 
 NONE => [s] 

372 

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

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

376 
fun add_plain canon alias = 
54092  377 
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

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

381 
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

382 
val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

383 
in (plain_name_tab, inclass_name_tab) end 
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50481
diff
changeset

384 

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

385 
fun fact_distinct eq facts = 
54076  386 
fold (fn fact as (_, th) => 
54080
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

387 
Net.insert_term_safe (eq o pairself (normalize_eq o prop_of o snd)) 
54077  388 
(normalize_eq (prop_of th), fact)) 
389 
facts Net.empty 

54076  390 
> Net.entries 
53504  391 

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

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

393 
case Logic.strip_horn (prop_of th) of 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

394 
(prems, @{const Trueprop} 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

395 
$ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

396 
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

397 
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

398 
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

399 
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

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

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

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

403 

50586  404 
val instantiate_induct_timeout = seconds 0.01 
405 

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

406 
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

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

408 
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

409 
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

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

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

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

413 
> lambda (Free ind_x) 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51160
diff
changeset

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

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

416 
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

417 
stature), th > read_instantiate ctxt [((p_name, 0), p_inst)]) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

419 

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

420 
fun 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

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

422 
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

423 

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

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

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

426 
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

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

428 
stmt_xs > filter (fn (_, T) => type_match thy (T, ind_T)) 
50586  429 
> map_filter (try (TimeLimit.timeLimit instantiate_induct_timeout 
430 
(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

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

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

433 

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

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

435 
[] > Term.add_frees t > filter_out (can Name.dest_internal o fst) 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

436 

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

437 
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

438 
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

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

440 
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

441 
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

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

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

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

445 
in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

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

448 

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

449 
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

450 

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

451 
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

452 

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

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

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

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

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

457 
val is_too_complex = 
4ad9599a0847
disable some checks for huge background theories
blanchet
parents:
53531
diff
changeset

458 
if generous orelse 
4ad9599a0847
disable some checks for huge background theories
blanchet
parents:
53531
diff
changeset

459 
fact_count global_facts >= max_facts_for_complex_check then 
4ad9599a0847
disable some checks for huge background theories
blanchet
parents:
53531
diff
changeset

460 
K false 
4ad9599a0847
disable some checks for huge background theories
blanchet
parents:
53531
diff
changeset

461 
else 
53533  462 
is_too_complex 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

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

464 
val named_locals = local_facts > Facts.dest_static [] 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

465 
val assms = Assumption.all_assms_of ctxt 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

466 
fun is_good_unnamed_local th = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

467 
not (Thm.has_name_hint th) andalso 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

468 
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

469 
val unnamed_locals = 
48396  470 
union Thm.eq_thm_prop (Facts.props local_facts) chained 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

471 
> filter is_good_unnamed_local > map (pair "" o single) 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

472 
val full_space = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

473 
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 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

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

477 
if name0 <> "" andalso 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

478 
forall (not o member Thm.eq_thm_prop add_ths) ths andalso 
50511
8825c36cb1ce
don't query blacklisted theorems in evaluation driver
blanchet
parents:
50510
diff
changeset

479 
(Facts.is_concealed facts name0 orelse 
53512  480 
(not generous andalso is_blacklisted_or_something name0)) then 
54081  481 
accum 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

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

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

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

485 
val multi = n > 1 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

486 
fun check_thms a = 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

487 
case try (Proof_Context.get_thms ctxt) a of 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

488 
NONE => false 
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

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

490 
in 
54081  491 
snd (fold_rev (fn th => fn (j, accum as (uni_accum, multi_accum)) => 
492 
(j  1, 

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

494 
(is_likely_tautology_too_meta_or_too_technical th orelse 

495 
is_too_complex (prop_of th)) then 

496 
accum 

497 
else 

498 
let 

499 
val new = 

500 
(((fn () => 

501 
if name0 = "" then 

502 
backquote_thm ctxt th 

503 
else 

504 
[Facts.extern ctxt facts name0, 

505 
Name_Space.extern ctxt full_space name0] 

506 
> find_first check_thms 

507 
> the_default name0 

508 
> make_name reserved multi j), 

509 
stature_of_thm global assms chained css name0 th), 

510 
th) 

511 
in 

512 
if multi then (uni_accum, new :: multi_accum) 

513 
else (new :: uni_accum, multi_accum) 

514 
end)) ths (n, accum)) 

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

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

516 
in 
50756
c96bb430ddb0
put singletheorem names before multitheorem ones (broken since 5d147d492792)
blanchet
parents:
50736
diff
changeset

517 
(* The singletheorem names go before the multipletheorem ones (e.g., 
c96bb430ddb0
put singletheorem names before multitheorem ones (broken since 5d147d492792)
blanchet
parents:
50736
diff
changeset

518 
"xxx" vs. "xxx(3)"), so that single names are preferred when both are 
c96bb430ddb0
put singletheorem names before multitheorem ones (broken since 5d147d492792)
blanchet
parents:
50736
diff
changeset

519 
available. *) 
c96bb430ddb0
put singletheorem names before multitheorem ones (broken since 5d147d492792)
blanchet
parents:
50736
diff
changeset

520 
`I [] > add_facts false fold local_facts (unnamed_locals @ named_locals) 
c96bb430ddb0
put singletheorem names before multitheorem ones (broken since 5d147d492792)
blanchet
parents:
50736
diff
changeset

521 
> add_facts true Facts.fold_static global_facts global_facts 
c96bb430ddb0
put singletheorem names before multitheorem ones (broken since 5d147d492792)
blanchet
parents:
50736
diff
changeset

522 
> op @ 
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 

48396  525 
fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts 
526 
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

527 
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

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

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

530 
let 
54077  531 
val thy = Proof_Context.theory_of ctxt 
48396  532 
val chained = 
533 
chained 

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

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

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

537 
maps (map (fn ((name, stature), th) => ((K name, stature), th)) 
52031
9a9238342963
tuning  renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset

538 
o fact_of_ref ctxt reserved 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

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

540 
(* The "fact_distinct" call would have cleaner semantics if it called "Pattern.equiv" 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

541 
instead of "Pattern.matches", but it would also be slower and less precise. 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

542 
"Pattern.matches" throws out theorems that are strict instances of other theorems, but 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

543 
only if the instance is met after the general version. *) 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

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

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

546 
val facts = 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

547 
all_facts ctxt false ho_atp reserved add chained css 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

548 
> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd) 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

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

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

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

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

554 

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

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

556 
let val num_facts = length facts in 
9c0f464d1854
drop only real duplicates, not subsumed facts  this confuses MaSh
blanchet
parents:
54092
diff
changeset

557 
facts > num_facts <= max_facts_for_duplicates 
9c0f464d1854
drop only real duplicates, not subsumed facts  this confuses MaSh
blanchet
parents:
54092
diff
changeset

558 
? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv 
9c0f464d1854
drop only real duplicates, not subsumed facts  this confuses MaSh
blanchet
parents:
54092
diff
changeset

559 
else Pattern.matches thy o swap) 
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; 