author  blanchet 
Tue, 08 Oct 2013 21:19:46 +0200  
changeset 54081  c7e9f1df30bb 
parent 54080  540835cf11ed 
child 54083  824db6ab3339 
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 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

43 

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

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

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

46 

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

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

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

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

50 
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

51 

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

52 
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

53 
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

54 

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

56 
{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

57 
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

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

59 

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

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

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

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

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

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

65 

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

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

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

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

69 

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

71 

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

72 
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

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

75 

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

76 
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

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

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

79 

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

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

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

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

83 

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

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

85 
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

86 

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

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

88 
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

89 

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

90 
fun is_rec_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

91 
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

92 
 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

93 
 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

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

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

96 

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

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

99 

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

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

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

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

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

105 

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

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

107 
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

108 
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

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

110 

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

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

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

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

117 
case find_index (equal z) knownT of 

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

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

120 
 normT (T as TFree _) = pair T 

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

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

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

124 
normT T 

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

126 
case find_index (equal z) known of 

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

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

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

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

131 
 norm (Bound j) = pair (Bound j) 

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

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

134 

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

138 
else 

139 
let val t = prop_of th in 

140 
(* FIXME: use structured name *) 

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

142 
Induction 

143 
else 

144 
let val t = normalize_vars t in 

145 
case Termtab.lookup css t of 

146 
SOME status => status 

147 
 NONE => 

148 
let val concl = Logic.strip_imp_concl t in 

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

150 
SOME lrhss => 

151 
let 

152 
val prems = Logic.strip_imp_prems t 

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

154 
in 

155 
Termtab.lookup css t' > the_default General 

156 
end 

157 
 NONE => General 

158 
end 

159 
end 

160 
end 

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

161 

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

164 

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

165 
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

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

167 
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

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

169 
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

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

171 
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

172 
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

173 
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

174 
 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

175 
 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

176 
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

177 
 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

178 
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

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

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

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

184 
:: rest) 

185 
end 

186 
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

187 

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

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

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

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

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

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

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

196 

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

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

198 
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

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

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

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

202 
"nibble.distinct"] 
53531  203 
> 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

204 
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

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

206 

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

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

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

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

210 

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

211 
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

212 
 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

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

214 

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

216 

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

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

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

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

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

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

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

224 

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

226 
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

227 

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

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

231 
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

232 

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

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

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

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

240 

53513  241 
datatype interest = Deal_Breaker  Interesting  Boring 
242 

243 
fun combine_interests Deal_Breaker _ = Deal_Breaker 

244 
 combine_interests _ Deal_Breaker = Deal_Breaker 

245 
 combine_interests Interesting _ = Interesting 

246 
 combine_interests _ Interesting = Interesting 

247 
 combine_interests Boring Boring = Boring 

248 

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

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

251 
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

252 
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

253 
 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

254 
 is_interesting_subterm _ = false 
53513  255 
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

256 
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

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

260 
not (exists_subterm is_interesting_subterm t) then 

261 
Boring 

262 
else 

263 
Interesting 

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

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

266 
combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u) 

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

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

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

272 
combine_interests (interest_of_bool t) (interest_of_bool u) 

273 
 interest_of_prop _ _ = Deal_Breaker 

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

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

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

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

280 

53512  281 
fun is_blacklisted_or_something ctxt ho_atp = 
282 
let 

283 
val blist = multi_base_blacklist ctxt ho_atp 

284 
fun is_blisted name = 

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

286 
in is_blisted end 

50510  287 

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

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

289 
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

290 
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

291 
prefixes of all free variables. In the worse case scenario, where the fact 
49981  292 
won't be resolved correctly, the user can fix it manually, e.g., by giving a 
293 
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

294 
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

295 
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

296 

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

297 
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

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

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

300 
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

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

302 
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

303 
$ 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

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

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

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

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

308 

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

309 
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

310 
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

311 

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

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

315 
Termtab.empty 

316 
else 

317 
let 

318 
fun add stature th = 

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

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

321 
ctxt > claset_of > Classical.rep_cs 

322 
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

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

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

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

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

331 
> maps (snd o snd) 

332 
> filter_out (member Thm.eq_thm_prop risky_defs) 

333 
> List.partition (is_rec_def o prop_of) 

334 
val spec_intros = 

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

336 
Spec_Rules.Co_Inductive] o fst) 

337 
> maps (snd o snd) 

338 
in 

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

340 
> fold (add Rec_Def) rec_defs 

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

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

344 
*) 
53502  345 
> fold (add Intro) intros 
346 
> fold (add Inductive) spec_intros 

347 
end 

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

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

349 

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

350 
fun normalize_eq (t as @{const Trueprop} 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

351 
$ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) = 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

352 
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t 
5d147d492792
push normalization further  avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
blanchet
parents:
50442
diff
changeset

353 
else HOLogic.mk_Trueprop (t0 $ t2 $ t1) 
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

354 
 normalize_eq (t as @{const Trueprop} $ (@{const Not} 
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))) = 
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

356 
if Term_Ord.fast_term_ord (t1, t2) <> GREATER then 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

357 
else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1)) 
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

358 
 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

359 

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

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

361 
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

362 

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

365 
proofs. *) 

366 
fun un_class_ify s = 

367 
case first_field "_class" s of 

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

369 
 NONE => [s] 

370 

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

371 
fun build_name_tables name_of facts = 
50733  372 
let 
53503  373 
fun cons_thm (_, th) = 
54076  374 
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

375 
fun add_plain canon alias = 
50815  376 
Symtab.update (Thm.get_name_hint alias, 
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

377 
name_of (if_thm_before canon alias)) 
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 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

379 
fun add_inclass (name, target) = 
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50734
diff
changeset

380 
fold (fn s => Symtab.update (s, target)) (un_class_ify name) 
50815  381 
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

382 
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

383 
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

384 
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

385 

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

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

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

54076  391 
> Net.entries 
53504  392 

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

393 
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

394 
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

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

396 
$ ((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

397 
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

398 
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

399 
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

400 
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

401 
else 
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 
 _ => NONE 
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

404 

50586  405 
val instantiate_induct_timeout = seconds 0.01 
406 

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

407 
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

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

409 
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

410 
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

411 
 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

412 
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

413 
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

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

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

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

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

418 
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

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

420 

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

421 
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

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

423 
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

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

426 
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

427 
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

428 
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

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

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

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

434 

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

435 
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

436 
[] > 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

437 

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

438 
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

439 
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

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

441 
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

442 
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

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

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

445 
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

446 
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

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

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

449 

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

450 
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

451 

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

452 
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

453 

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

454 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

469 
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

470 
val unnamed_locals = 
48396  471 
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

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

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

474 
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) 
53512  475 
val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
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 
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset

479 
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

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

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

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

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

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

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

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

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

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

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

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

495 
(is_likely_tautology_too_meta_or_too_technical th orelse 

496 
is_too_complex (prop_of th)) then 

497 
accum 

498 
else 

499 
let 

500 
val new = 

501 
(((fn () => 

502 
if name0 = "" then 

503 
backquote_thm ctxt th 

504 
else 

505 
[Facts.extern ctxt facts name0, 

506 
Name_Space.extern ctxt full_space name0] 

507 
> find_first check_thms 

508 
> the_default name0 

509 
> make_name reserved multi j), 

510 
stature_of_thm global assms chained css name0 th), 

511 
th) 

512 
in 

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

514 
else (new :: uni_accum, multi_accum) 

515 
end)) ths (n, accum)) 

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

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

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

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

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

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

521 
`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

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

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

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

525 

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

528 
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

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

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

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

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

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

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

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

539 
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

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

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

542 
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

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

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

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

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

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

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

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

550 
val num_facts = length facts 
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 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

553 
> num_facts <= max_facts_for_duplicates 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

554 
? fact_distinct (if num_facts > max_facts_for_duplicate_matching then op aconv 
540835cf11ed
more gracefully handle huge theories in relevance filters
blanchet
parents:
54078
diff
changeset

555 
else Pattern.matches thy o swap) 
48292  556 
end) 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
diff
changeset

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

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

559 

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

560 
end; 