author  krauss 
Fri, 25 Feb 2011 16:57:43 +0100  
changeset 41844  b933142e02d0 
parent 41841  c27b0b37041a 
child 41845  6611b9cef38b 
permissions  rwrr 
30143  1 
(* Title: Pure/Tools/find_theorems.ML 
26283  2 
Author: Rafal Kolanski and Gerwin Klein, NICTA 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

3 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

4 
Retrieve theorems from proof context. 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

5 
*) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

6 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

7 
signature FIND_THEOREMS = 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

8 
sig 
16036  9 
datatype 'term criterion = 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

10 
Name of string  Intro  IntroIff  Elim  Dest  Solves  Simp of 'term  
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

11 
Pattern of 'term 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

12 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

13 
datatype theorem = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

14 
Internal of Facts.ref * thm  
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

15 
External of Facts.ref * term 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

16 

32738  17 
val tac_limit: int Unsynchronized.ref 
18 
val limit: int Unsynchronized.ref 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

19 
val find_theorems: Proof.context > thm option > int option > bool > 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

20 
(bool * string criterion) list > int option * (Facts.ref * thm) list 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

21 
val filter_theorems: Proof.context > theorem list > thm option > 
41841
c27b0b37041a
Refactor find_theorems to provide a more general filter_facts method
noschinl
parents:
41835
diff
changeset

22 
int option > bool > (bool * string criterion) list > 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

23 
int option * theorem list 
41841
c27b0b37041a
Refactor find_theorems to provide a more general filter_facts method
noschinl
parents:
41835
diff
changeset

24 

30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

25 
val pretty_thm: Proof.context > Facts.ref * thm > Pretty.T 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

26 
end; 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

27 

33301  28 
structure Find_Theorems: FIND_THEOREMS = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

29 
struct 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

30 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

31 
(** search criteria **) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

32 

16036  33 
datatype 'term criterion = 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

34 
Name of string  Intro  IntroIff  Elim  Dest  Solves  Simp of 'term  
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

35 
Pattern of 'term; 
16036  36 

33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

37 
fun apply_dummies tm = 
33301  38 
let 
39 
val (xs, _) = Term.strip_abs tm; 

40 
val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs); 

41 
in #1 (Term.replace_dummy_patterns tm' 1) end; 

33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

42 

c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

43 
fun parse_pattern ctxt nm = 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

44 
let 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

45 
val consts = ProofContext.consts_of ctxt; 
33301  46 
val nm' = 
47 
(case Syntax.parse_term ctxt nm of 

48 
Const (c, _) => c 

49 
 _ => Consts.intern consts nm); 

33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

50 
in 
33301  51 
(case try (Consts.the_abbreviation consts) nm' of 
33923
7fc1ab75b4fa
Expand nested abbreviations before applying dummy patterns.
kleing
parents:
33382
diff
changeset

52 
SOME (_, rhs) => apply_dummies (ProofContext.expand_abbrevs ctxt rhs) 
33301  53 
 NONE => ProofContext.read_term_pattern ctxt nm) 
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

54 
end; 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

55 

16036  56 
fun read_criterion _ (Name name) = Name name 
57 
 read_criterion _ Intro = Intro 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

58 
 read_criterion _ IntroIff = IntroIff 
16036  59 
 read_criterion _ Elim = Elim 
60 
 read_criterion _ Dest = Dest 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

61 
 read_criterion _ Solves = Solves 
24683  62 
 read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str) 
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

63 
 read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

64 

16036  65 
fun pretty_criterion ctxt (b, c) = 
66 
let 

67 
fun prfx s = if b then s else "" ^ s; 

68 
in 

69 
(case c of 

70 
Name name => Pretty.str (prfx "name: " ^ quote name) 

71 
 Intro => Pretty.str (prfx "intro") 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

72 
 IntroIff => Pretty.str (prfx "introiff") 
16036  73 
 Elim => Pretty.str (prfx "elim") 
74 
 Dest => Pretty.str (prfx "dest") 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

75 
 Solves => Pretty.str (prfx "solves") 
16088  76 
 Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1, 
24920  77 
Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))] 
16036  78 
 Pattern pat => Pretty.enclose (prfx " \"") "\"" 
24920  79 
[Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)]) 
16036  80 
end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

81 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

82 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

83 
(** theorems, either internal or external (without proof) *) 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

84 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

85 
datatype theorem = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

86 
Internal of Facts.ref * thm  
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

87 
External of Facts.ref * term; 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

88 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

89 
fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

90 
 prop_of (External (_, prop)) = prop; 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

91 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

92 
fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

93 
 nprems_of (External (_, prop)) = Logic.count_prems prop; 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

94 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

95 
fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

96 
 major_prem_of (External (_, prop)) = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

97 
Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop)); 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

98 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

99 
fun fact_ref_of (Internal (fact_ref, _)) = fact_ref 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

100 
 fact_ref_of (External (fact_ref, _)) = fact_ref; 
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

101 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

102 
(** search criterion filters **) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

103 

16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

104 
(*generated filters are to be of the form 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

105 
input: theorem 
17106  106 
output: (p:int, s:int) option, where 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

107 
NONE indicates no match 
17106  108 
p is the primary sorting criterion 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

109 
(eg. number of assumptions in the theorem) 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

110 
s is the secondary sorting criterion 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

111 
(eg. size of the substitution for intro, elim and dest) 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

112 
when applying a set of filters to a thm, fold results in: 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

113 
(biggest p, sum of all s) 
17106  114 
currently p and s only matter for intro, elim, dest and simp filters, 
115 
otherwise the default ordering is used. 

16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

116 
*) 
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

117 

16088  118 

119 
(* matching theorems *) 

17106  120 

35625  121 
fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy; 
16088  122 

32798  123 
(*educated guesses on HOL*) (* FIXME broken *) 
124 
val boolT = Type ("bool", []); 

125 
val iff_const = Const ("op =", boolT > boolT > boolT); 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

126 

16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

127 
(*extract terms from term_src, refine them to the parts that concern us, 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

128 
if po try match them against obj else vice versa. 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

129 
trivial matches are ignored. 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

130 
returns: smallest substitution size*) 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

131 
fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src = 
16088  132 
let 
17106  133 
val thy = ProofContext.theory_of ctxt; 
16088  134 

32798  135 
fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat)); 
16486  136 
fun matches pat = 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

137 
let 
35625  138 
val jpat = Object_Logic.drop_judgment thy pat; 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

139 
val c = Term.head_of jpat; 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

140 
val pats = 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

141 
if Term.is_Const c 
32798  142 
then 
143 
if doiff andalso c = iff_const then 

35625  144 
(pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat))) 
32798  145 
> filter (is_nontrivial thy) 
146 
else [pat] 

31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

147 
else []; 
32798  148 
in filter check_match pats end; 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

149 

df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

150 
fun substsize pat = 
18184  151 
let val (_, subst) = 
152 
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) 

17205  153 
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end; 
16088  154 

16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

155 
fun bestmatch [] = NONE 
33029  156 
 bestmatch xs = SOME (foldl1 Int.min xs); 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

157 

16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

158 
val match_thm = matches o refine_term; 
16486  159 
in 
32798  160 
maps match_thm (extract_terms term_src) 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

161 
> map substsize 
26283  162 
> bestmatch 
16088  163 
end; 
164 

165 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

166 
(* filter_name *) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

167 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

168 
fun filter_name str_pat theorem = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

169 
if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem)) 
17205  170 
then SOME (0, 0) else NONE; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

171 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

172 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

173 
(* filter intro/elim/dest/solves rules *) 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

174 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

175 
fun filter_dest ctxt goal theorem = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

176 
let 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

177 
val extract_dest = 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

178 
(fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem], 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

179 
hd o Logic.strip_imp_prems); 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

180 
val prems = Logic.prems_of_goal goal 1; 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

181 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

182 
fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset

183 
val successful = prems > map_filter try_subst; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

184 
in 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

185 
(*if possible, keep best substitution (one with smallest size)*) 
17106  186 
(*dest rules always have assumptions, so a dest with one 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

187 
assumption is as good as an intro rule with none*) 
17205  188 
if not (null successful) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

189 
then SOME (nprems_of theorem  1, foldl1 Int.min successful) else NONE 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

190 
end; 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

191 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

192 
fun filter_intro doiff ctxt goal theorem = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

193 
let 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

194 
val extract_intro = (single o prop_of, Logic.strip_imp_concl); 
16036  195 
val concl = Logic.concl_of_goal goal 1; 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

196 
val ss = is_matching_thm doiff extract_intro ctxt true concl theorem; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

197 
in 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

198 
if is_some ss then SOME (nprems_of theorem, the ss) else NONE 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

199 
end; 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

200 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

201 
fun filter_elim ctxt goal theorem = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

202 
if nprems_of theorem > 0 then 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

203 
let 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

204 
val rule = prop_of theorem; 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

205 
val prems = Logic.prems_of_goal goal 1; 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

206 
val goal_concl = Logic.concl_of_goal goal 1; 
26283  207 
val rule_mp = hd (Logic.strip_imp_prems rule); 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

208 
val rule_concl = Logic.strip_imp_concl rule; 
26283  209 
fun combine t1 t2 = Const ("*combine*", dummyT > dummyT) $ (t1 $ t2); 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

210 
val rule_tree = combine rule_mp rule_concl; 
26283  211 
fun goal_tree prem = combine prem goal_concl; 
17106  212 
fun try_subst prem = 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

213 
is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset

214 
val successful = prems > map_filter try_subst; 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

215 
in 
32798  216 
(*elim rules always have assumptions, so an elim with one 
217 
assumption is as good as an intro rule with none*) 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

218 
if is_nontrivial (ProofContext.theory_of ctxt) (major_prem_of theorem) 
17205  219 
andalso not (null successful) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

220 
then SOME (nprems_of theorem  1, foldl1 Int.min successful) else NONE 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

221 
end 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

222 
else NONE 
16036  223 

32738  224 
val tac_limit = Unsynchronized.ref 5; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

225 

30143  226 
fun filter_solves ctxt goal = 
227 
let 

228 
fun etacn thm i = Seq.take (! tac_limit) o etac thm i; 

229 
fun try_thm thm = 

230 
if Thm.no_prems thm then rtac thm 1 goal 

30318
3d03190d2864
replaced archaic use of rep_ss by Simplifier.mksimps;
wenzelm
parents:
30234
diff
changeset

231 
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

232 
in 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

233 
fn Internal (_, thm) => 
32798  234 
if is_some (Seq.pull (try_thm thm)) 
30143  235 
then SOME (Thm.nprems_of thm, 0) else NONE 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

236 
 External _ => NONE 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

237 
end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

238 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

239 

16074  240 
(* filter_simp *) 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

241 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

242 
fun filter_simp ctxt t (Internal (_, thm)) = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

243 
let 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

244 
val mksimps = Simplifier.mksimps (simpset_of ctxt); 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

245 
val extract_simp = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

246 
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

247 
val ss = is_matching_thm false extract_simp ctxt false t thm; 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

248 
in 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

249 
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

250 
end 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

251 
 filter_simp _ _ (External _) = NONE; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

252 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

253 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

254 
(* filter_pattern *) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

255 

32798  256 
fun get_names t = Term.add_const_names t (Term.add_free_names t []); 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

257 

30143  258 
(*Including all constants and frees is only sound because 
259 
matching uses higherorder patterns. If full matching 

260 
were used, then constants that may be subject to 

261 
betareduction after substitution of frees should 

262 
not be included for LHS set because they could be 

263 
thrown away by the substituted function. 

264 
e.g. for (?F 1 2) do not include 1 or 2, if it were 

265 
possible for ?F to be (% x y. 3) 

266 
The largest possible set should always be included on 

267 
the RHS.*) 

268 

269 
fun filter_pattern ctxt pat = 

270 
let 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

271 
val pat_consts = get_names pat; 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

272 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

273 
fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem))) 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

274 
 check (theorem, c as SOME thm_consts) = 
33038  275 
(if subset (op =) (pat_consts, thm_consts) andalso 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

276 
Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, prop_of theorem) 
32798  277 
then SOME (0, 0) else NONE, c); 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

278 
in check end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

279 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

280 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

281 
(* interpret criteria as filters *) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

282 

16036  283 
local 
284 

285 
fun err_no_goal c = 

286 
error ("Current goal required for " ^ c ^ " search criterion"); 

287 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

288 
val fix_goal = Thm.prop_of; 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

289 

28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

290 
fun filter_crit _ _ (Name name) = apfst (filter_name name) 
16036  291 
 filter_crit _ NONE Intro = err_no_goal "intro" 
41835
9712fae15200
fix nonexhaustive pattern match in find_theorems
noschinl
parents:
39557
diff
changeset

292 
 filter_crit _ NONE IntroIff = err_no_goal "introiff" 
16036  293 
 filter_crit _ NONE Elim = err_no_goal "elim" 
294 
 filter_crit _ NONE Dest = err_no_goal "dest" 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

295 
 filter_crit _ NONE Solves = err_no_goal "solves" 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

296 
 filter_crit ctxt (SOME goal) Intro = apfst (filter_intro false ctxt (fix_goal goal)) 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

297 
 filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal)) 
30143  298 
 filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal)) 
299 
 filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal)) 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

300 
 filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal) 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

301 
 filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) 
16088  302 
 filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; 
16036  303 

19502  304 
fun opt_not x = if is_some x then NONE else SOME (0, 0); 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

305 

17756  306 
fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) 
26283  307 
 opt_add _ _ = NONE; 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

308 

30143  309 
fun app_filters thm = 
310 
let 

28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

311 
fun app (NONE, _, _) = NONE 
32798  312 
 app (SOME v, _, []) = SOME (v, thm) 
30143  313 
 app (r, consts, f :: fs) = 
314 
let val (r', consts') = f (thm, consts) 

315 
in app (opt_add r r', consts', fs) end; 

28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

316 
in app end; 
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

317 

31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
31042
diff
changeset

318 

16036  319 
in 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

320 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

321 
fun filter_criterion ctxt opt_goal (b, c) = 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

322 
(if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c; 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

323 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

324 
fun sorted_filter filters theorems = 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

325 
let 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

326 
fun eval_filters theorem = app_filters theorem (SOME (0, 0), NONE, filters); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

327 

16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

328 
(*filters return: (number of assumptions, substitution size) option, so 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

329 
sort (desc. in both cases) according to number of assumptions first, 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

330 
then by the substitution size*) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

331 
fun result_ord (((p0, s0), _), ((p1, s1), _)) = 
17205  332 
prod_ord int_ord int_ord ((p1, s1), (p0, s0)); 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

333 
in map_filter eval_filters theorems > sort result_ord > map #2 end; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

334 

30822  335 
fun lazy_filter filters = 
336 
let 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

337 
fun lazy_match thms = Seq.make (fn () => first_match thms) 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

338 

15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

339 
and first_match [] = NONE 
30822  340 
 first_match (thm :: thms) = 
341 
(case app_filters thm (SOME (0, 0), NONE, filters) of 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

342 
NONE => first_match thms 
30822  343 
 SOME (_, t) => SOME (t, lazy_match thms)); 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

344 
in lazy_match end; 
30822  345 

16036  346 
end; 
347 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

348 

22414  349 
(* removing duplicates, preferring nicer names, roughly n log n *) 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

350 

25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

351 
local 
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

352 

27486  353 
val index_ord = option_ord (K EQUAL); 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33039
diff
changeset

354 
val hidden_ord = bool_ord o pairself Name_Space.is_hidden; 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30318
diff
changeset

355 
val qual_ord = int_ord o pairself (length o Long_Name.explode); 
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

356 
val txt_ord = int_ord o pairself size; 
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

357 

27486  358 
fun nicer_name (x, i) (y, j) = 
359 
(case hidden_ord (x, y) of EQUAL => 

360 
(case index_ord (i, j) of EQUAL => 

361 
(case qual_ord (x, y) of EQUAL => txt_ord (x, y)  ord => ord) 

362 
 ord => ord) 

25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

363 
 ord => ord) <> GREATER; 
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

364 

29848  365 
fun rem_cdups nicer xs = 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

366 
let 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

367 
fun rem_c rev_seen [] = rev rev_seen 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

368 
 rem_c rev_seen [x] = rem_c (x :: rev_seen) [] 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

369 
 rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

370 
if (prop_of t) aconv (prop_of t') 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

371 
then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs) 
30822  372 
else rem_c (x :: rev_seen) (y :: xs) 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

373 
in rem_c [] xs end; 
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

374 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

375 
in 
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

376 

30143  377 
fun nicer_shortest ctxt = 
378 
let 

30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset

379 
(* FIXME global name space!? *) 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38335
diff
changeset

380 
val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt)); 
29848  381 

30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset

382 
val shorten = 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33039
diff
changeset

383 
Name_Space.extern_flags 
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33039
diff
changeset

384 
{long_names = false, short_names = false, unique_names = false} space; 
29848  385 

386 
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = 

387 
nicer_name (shorten x, i) (shorten y, j) 

388 
 nicer (Facts.Fact _) (Facts.Named _) = true 

389 
 nicer (Facts.Named _) (Facts.Fact _) = false; 

390 
in nicer end; 

391 

392 
fun rem_thm_dups nicer xs = 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

393 
xs ~~ (1 upto length xs) 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

394 
> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1)) 
29848  395 
> rem_cdups nicer 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

396 
> sort (int_ord o pairself #2) 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

397 
> map #1; 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

398 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

399 
end; 
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

400 

275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset

401 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

402 
(* print_theorems *) 
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

403 

26283  404 
fun all_facts_of ctxt = 
33381  405 
let 
33382  406 
fun visible_facts facts = 
407 
Facts.dest_static [] facts 

408 
> filter_out (Facts.is_concealed facts o #1); 

33381  409 
in 
410 
maps Facts.selections 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38335
diff
changeset

411 
(visible_facts (Global_Theory.facts_of (ProofContext.theory_of ctxt)) @ 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

412 

b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

413 

33381  414 
visible_facts (ProofContext.facts_of ctxt)) 
415 
end; 

17972  416 

32738  417 
val limit = Unsynchronized.ref 40; 
25992
928594f50893
renamed thms_containing_limit to FindTheorems.limit;
wenzelm
parents:
25226
diff
changeset

418 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

419 
fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

420 
let 
30822  421 
val assms = 
422 
ProofContext.get_fact ctxt (Facts.named "local.assms") 

423 
handle ERROR _ => []; 

424 
val add_prems = Seq.hd o TRY (Method.insert_tac assms 1); 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

425 
val opt_goal' = Option.map add_prems opt_goal; 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

426 

16036  427 
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

428 
val filters = map (filter_criterion ctxt opt_goal') criteria; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

429 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

430 
fun find_all theorems = 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

431 
let 
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

432 
val raw_matches = sorted_filter filters theorems; 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

433 

15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

434 
val matches = 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

435 
if rem_dups 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

436 
then rem_thm_dups (nicer_shortest ctxt) raw_matches 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

437 
else raw_matches; 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

438 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

439 
val len = length matches; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

440 
val lim = the_default (! limit) opt_limit; 
34088  441 
in (SOME len, drop (Int.max (len  lim, 0)) matches) end; 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

442 

15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

443 
val find = 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

444 
if rem_dups orelse is_none opt_limit 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

445 
then find_all 
30822  446 
else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters; 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

447 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

448 
in find theorems end; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

449 

41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

450 
fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

451 
filter_theorems ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

452 
rem_dups raw_criteria 
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset

453 
> apsnd (map (fn Internal f => f)); 
30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

454 

1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

455 
fun pretty_thm ctxt (thmref, thm) = Pretty.block 
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

456 
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31687
diff
changeset

457 
Display.pretty_thm ctxt thm]; 
30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

458 

41841
c27b0b37041a
Refactor find_theorems to provide a more general filter_facts method
noschinl
parents:
41835
diff
changeset

459 
fun print_theorems ctxt (foundo, thms) raw_criteria = 
30143  460 
let 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

461 
val start = start_timing (); 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

462 

2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

463 
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

464 
val returned = length thms; 
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
31042
diff
changeset

465 

30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

466 
val tally_msg = 
30822  467 
(case foundo of 
38335  468 
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)" 
30822  469 
 SOME found => 
38335  470 
"found " ^ string_of_int found ^ " theorem(s)" ^ 
30822  471 
(if returned < found 
472 
then " (" ^ string_of_int returned ^ " displayed)" 

473 
else "")); 

16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

474 

31687  475 
val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

476 
in 
38335  477 
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: 
478 
Pretty.str "" :: 

479 
(if null thms then [Pretty.str ("nothing found" ^ end_msg)] 

480 
else 

481 
[Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @ 

30186
1f836e949ac2
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
wenzelm
parents:
30143
diff
changeset

482 
map (pretty_thm ctxt) thms) 
38335  483 
end > Pretty.chunks > Pretty.writeln; 
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

484 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

485 

32798  486 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

487 
(** command syntax **) 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

488 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

489 
local 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

490 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

491 
val criterion = 
36950  492 
Parse.reserved "name"  Parse.!!! (Parse.$$$ ":"  Parse.xname) >> Name  
493 
Parse.reserved "intro" >> K Intro  

494 
Parse.reserved "introiff" >> K IntroIff  

495 
Parse.reserved "elim" >> K Elim  

496 
Parse.reserved "dest" >> K Dest  

497 
Parse.reserved "solves" >> K Solves  

498 
Parse.reserved "simp"  Parse.!!! (Parse.$$$ ":"  Parse.term) >> Simp  

499 
Parse.term >> Pattern; 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

500 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

501 
val options = 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

502 
Scan.optional 
36950  503 
(Parse.$$$ "("  
504 
Parse.!!! (Scan.option Parse.nat  Scan.optional (Parse.reserved "with_dups" >> K false) true 

505 
 Parse.$$$ ")")) (NONE, true); 

30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

506 
in 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

507 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

508 
val _ = 
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset

509 
Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria" 
36950  510 
Keyword.diag 
511 
(options  Scan.repeat (((Scan.option Parse.minus >> is_none)  criterion)) 

38334  512 
>> (fn ((opt_lim, rem_dups), spec) => 
513 
Toplevel.no_timing o 

514 
Toplevel.keep (fn state => 

515 
let 

516 
val ctxt = Toplevel.context_of state; 

517 
val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state > Option.map #goal; 

41841
c27b0b37041a
Refactor find_theorems to provide a more general filter_facts method
noschinl
parents:
41835
diff
changeset

518 
val found = find_theorems ctxt opt_goal opt_lim rem_dups spec; 
c27b0b37041a
Refactor find_theorems to provide a more general filter_facts method
noschinl
parents:
41835
diff
changeset

519 
in print_theorems ctxt found spec end))); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

520 

f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

521 
end; 
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

522 

8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

523 
end; 