author  wenzelm 
Thu, 29 Oct 2009 11:56:02 +0100  
changeset 33301  1fe9fc908ec3 
parent 33290  6dcb0a970783 
child 33381  81269c72321a 
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 
32738  12 
val tac_limit: int Unsynchronized.ref 
13 
val limit: int Unsynchronized.ref 

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

14 
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

15 
(bool * string criterion) list > int option * (Facts.ref * thm) list 
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

16 
val pretty_thm: Proof.context > Facts.ref * thm > Pretty.T 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

17 
val print_theorems: Proof.context > thm option > int option > bool > 
16036  18 
(bool * string criterion) list > unit 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

20 

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

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

23 

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

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

25 

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

27 
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

28 
Pattern of 'term; 
16036  29 

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

30 
fun apply_dummies tm = 
33301  31 
let 
32 
val (xs, _) = Term.strip_abs tm; 

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

34 
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

35 

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

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

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

38 
val consts = ProofContext.consts_of ctxt; 
33301  39 
val nm' = 
40 
(case Syntax.parse_term ctxt nm of 

41 
Const (c, _) => c 

42 
 _ => Consts.intern consts nm); 

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

43 
in 
33301  44 
(case try (Consts.the_abbreviation consts) nm' of 
45 
SOME (_, rhs) => apply_dummies rhs 

46 
 NONE => ProofContext.read_term_pattern ctxt nm) 

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

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

48 

16036  49 
fun read_criterion _ (Name name) = Name name 
50 
 read_criterion _ Intro = Intro 

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

51 
 read_criterion _ IntroIff = IntroIff 
16036  52 
 read_criterion _ Elim = Elim 
53 
 read_criterion _ Dest = Dest 

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

54 
 read_criterion _ Solves = Solves 
24683  55 
 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

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

57 

16036  58 
fun pretty_criterion ctxt (b, c) = 
59 
let 

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

61 
in 

62 
(case c of 

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

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

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

65 
 IntroIff => Pretty.str (prfx "introiff") 
16036  66 
 Elim => Pretty.str (prfx "elim") 
67 
 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

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

74 

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

75 

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

76 

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

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

78 

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

79 
(*generated filters are to be of the form 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

80 
input: (Facts.ref * thm) 
17106  81 
output: (p:int, s:int) option, where 
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset

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

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

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

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

87 
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

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

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

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

92 

16088  93 

94 
(* matching theorems *) 

17106  95 

17205  96 
fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy; 
16088  97 

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

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

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

101 

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

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

103 
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

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

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

106 
fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src = 
16088  107 
let 
17106  108 
val thy = ProofContext.theory_of ctxt; 
16088  109 

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

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

113 
val jpat = ObjectLogic.drop_judgment thy pat; 
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

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

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

116 
if Term.is_Const c 
32798  117 
then 
118 
if doiff andalso c = iff_const then 

119 
(pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat))) 

120 
> filter (is_nontrivial thy) 

121 
else [pat] 

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

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

124 

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

125 
fun substsize pat = 
18184  126 
let val (_, subst) = 
127 
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) 

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

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

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

132 

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

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

136 
> map substsize 
26283  137 
> bestmatch 
16088  138 
end; 
139 

140 

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

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

142 

17106  143 
fun filter_name str_pat (thmref, _) = 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

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

146 

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

147 

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

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

149 

17205  150 
fun filter_dest ctxt goal (_, thm) = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

152 
val extract_dest = 
17205  153 
(fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm], 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

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

156 

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

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

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

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

160 
(*if possible, keep best substitution (one with smallest size)*) 
17106  161 
(*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

162 
assumption is as good as an intro rule with none*) 
17205  163 
if not (null successful) 
33029  164 
then SOME (Thm.nprems_of thm  1, foldl1 Int.min successful) else NONE 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

166 

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

167 
fun filter_intro doiff ctxt goal (_, thm) = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

168 
let 
17205  169 
val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); 
16036  170 
val concl = Logic.concl_of_goal goal 1; 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

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

172 
in 
18939  173 
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

175 

17205  176 
fun filter_elim ctxt goal (_, thm) = 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

177 
if not (Thm.no_prems thm) then 
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

178 
let 
17205  179 
val rule = Thm.full_prop_of thm; 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

180 
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

181 
val goal_concl = Logic.concl_of_goal goal 1; 
26283  182 
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

183 
val rule_concl = Logic.strip_imp_concl rule; 
26283  184 
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

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

188 
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

189 
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

190 
in 
32798  191 
(*elim rules always have assumptions, so an elim with one 
192 
assumption is as good as an intro rule with none*) 

17106  193 
if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm) 
17205  194 
andalso not (null successful) 
33029  195 
then SOME (Thm.nprems_of thm  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

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

197 
else NONE 
16036  198 

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

200 

30143  201 
fun filter_solves ctxt goal = 
202 
let 

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

204 
fun try_thm thm = 

205 
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

206 
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

207 
in 
30143  208 
fn (_, thm) => 
32798  209 
if is_some (Seq.pull (try_thm thm)) 
30143  210 
then SOME (Thm.nprems_of thm, 0) else NONE 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

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

212 

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

213 

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

215 

17205  216 
fun filter_simp ctxt t (_, thm) = 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

217 
let 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

218 
val mksimps = Simplifier.mksimps (simpset_of ctxt); 
17106  219 
val extract_simp = 
30318
3d03190d2864
replaced archaic use of rep_ss by Simplifier.mksimps;
wenzelm
parents:
30234
diff
changeset

220 
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); 
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

221 
val ss = is_matching_thm false extract_simp ctxt false t thm; 
17106  222 
in 
18939  223 
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE 
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset

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

225 

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

226 

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

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

228 

32798  229 
fun get_names t = Term.add_const_names t (Term.add_free_names t []); 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

230 
fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm); 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

231 

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

234 
were used, then constants that may be subject to 

235 
betareduction after substitution of frees should 

236 
not be included for LHS set because they could be 

237 
thrown away by the substituted function. 

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

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

240 
The largest possible set should always be included on 

241 
the RHS.*) 

242 

243 
fun filter_pattern ctxt pat = 

244 
let 

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

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

246 

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

247 
fun check (t, NONE) = check (t, SOME (get_thm_names t)) 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

248 
 check ((_, thm), c as SOME thm_consts) = 
33038  249 
(if subset (op =) (pat_consts, thm_consts) andalso 
32798  250 
Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) 
251 
then SOME (0, 0) else NONE, c); 

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

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

253 

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

254 

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

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

256 

16036  257 
local 
258 

259 
fun err_no_goal c = 

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

261 

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

262 
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

263 

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

264 
fun filter_crit _ _ (Name name) = apfst (filter_name name) 
16036  265 
 filter_crit _ NONE Intro = err_no_goal "intro" 
266 
 filter_crit _ NONE Elim = err_no_goal "elim" 

267 
 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

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

269 
 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

270 
 filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal)) 
30143  271 
 filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal)) 
272 
 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

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

274 
 filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) 
16088  275 
 filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; 
16036  276 

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

278 

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

281 

30143  282 
fun app_filters thm = 
283 
let 

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

284 
fun app (NONE, _, _) = NONE 
32798  285 
 app (SOME v, _, []) = SOME (v, thm) 
30143  286 
 app (r, consts, f :: fs) = 
287 
let val (r', consts') = f (thm, consts) 

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

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

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

290 

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

291 

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

293 

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

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

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

296 

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

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

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

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

300 

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

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

302 
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

303 
then by the substitution size*) 
17205  304 
fun thm_ord (((p0, s0), _), ((p1, s1), _)) = 
305 
prod_ord int_ord int_ord ((p1, s1), (p0, s0)); 

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

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

307 

30822  308 
fun lazy_filter filters = 
309 
let 

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

310 
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

311 

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

312 
and first_match [] = NONE 
30822  313 
 first_match (thm :: thms) = 
314 
(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

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

317 
in lazy_match end; 
30822  318 

16036  319 
end; 
320 

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

321 

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

323 

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

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

325 

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

327 
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

328 
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

329 
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

330 

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

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

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

335 
 ord => ord) 

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

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

337 

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

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

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

341 
 rem_c rev_seen [x] = rem_c (x :: rev_seen) [] 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

342 
 rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = 
30822  343 
if Thm.eq_thm_prop (t, t') 
344 
then rem_c rev_seen ((if nicer n n' then x else y) :: xs) 

345 
else rem_c (x :: rev_seen) (y :: xs) 

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

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

347 

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

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

349 

30143  350 
fun nicer_shortest ctxt = 
351 
let 

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

352 
(* FIXME global name space!? *) 
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset

353 
val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt)); 
29848  354 

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

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

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

357 
{long_names = false, short_names = false, unique_names = false} space; 
29848  358 

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

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

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

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

363 
in nicer end; 

364 

365 
fun rem_thm_dups nicer xs = 

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

366 
xs ~~ (1 upto length xs) 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28900
diff
changeset

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

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

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

371 

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

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

373 

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

374 

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

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

376 

26283  377 
fun all_facts_of ctxt = 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset

378 
maps Facts.selections 
27173  379 
(Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @ 
380 
Facts.dest_static [] (ProofContext.facts_of ctxt)); 

17972  381 

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

383 

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

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

385 
let 
30822  386 
val assms = 
387 
ProofContext.get_fact ctxt (Facts.named "local.assms") 

388 
handle ERROR _ => []; 

389 
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

390 
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

391 

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

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

394 

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

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

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

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

398 

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

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

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

401 
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

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

403 

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

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

405 
val lim = the_default (! limit) opt_limit; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

406 
in (SOME len, Library.drop (len  lim, matches)) end; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

407 

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

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

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

410 
then find_all 
30822  411 
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

412 

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

413 
in find (all_facts_of ctxt) end; 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

414 

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

415 

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

416 
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

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

418 
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

419 

30143  420 
fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = 
421 
let 

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

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

423 

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

424 
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

425 
val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria; 
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

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

427 

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

428 
val tally_msg = 
30822  429 
(case foundo of 
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset

430 
NONE => "displaying " ^ string_of_int returned ^ " theorems" 
30822  431 
 SOME found => 
432 
"found " ^ string_of_int found ^ " theorems" ^ 

433 
(if returned < found 

434 
then " (" ^ string_of_int returned ^ " displayed)" 

435 
else "")); 

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

436 

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

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

439 
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) 
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset

440 
:: Pretty.str "" :: 
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset

441 
(if null thms then [Pretty.str ("nothing found" ^ end_msg)] 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

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

444 
map (pretty_thm ctxt) thms) 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

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

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

447 

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

448 

32798  449 

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

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

451 

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

452 
fun find_theorems_cmd ((opt_lim, rem_dups), spec) = 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

453 
Toplevel.unknown_theory o Toplevel.keep (fn state => 
30822  454 
let 
455 
val proof_state = Toplevel.enter_proof_body state; 

456 
val ctxt = Proof.context_of proof_state; 

33290  457 
val opt_goal = try Proof.simple_goal proof_state > Option.map #goal; 
30822  458 
in print_theorems ctxt opt_goal opt_lim rem_dups spec 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

459 

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

460 
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

461 

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

462 
structure P = OuterParse and K = OuterKeyword; 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

463 

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

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

465 
P.reserved "name"  P.!!! (P.$$$ ":"  P.xname) >> Name  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

466 
P.reserved "intro" >> K Intro  
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset

467 
P.reserved "introiff" >> K IntroIff  
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

468 
P.reserved "elim" >> K Elim  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

469 
P.reserved "dest" >> K Dest  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

470 
P.reserved "solves" >> K Solves  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

471 
P.reserved "simp"  P.!!! (P.$$$ ":"  P.term) >> Simp  
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

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

473 

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

474 
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

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

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

477 
P.!!! (Scan.option P.nat  Scan.optional (P.reserved "with_dups" >> K false) true 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

478 
 P.$$$ ")")) (NONE, true); 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

479 
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

480 

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

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

482 
OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset

483 
(options  Scan.repeat (((Scan.option P.minus >> is_none)  criterion)) 
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 
>> (Toplevel.no_timing oo find_theorems_cmd)); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

485 

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

486 
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

487 

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