author  kleing 
Wed, 21 Oct 2009 16:41:22 +1100  
changeset 33036  c61fe520602b 
parent 33029  2fefe039edf1 
child 33039  5018f6a76b3f 
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 

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

21 
structure FindTheorems: FIND_THEOREMS = 
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 = 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

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

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

33 
> map (Term.dummy_pattern o snd) 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

34 
> betapplys o pair tm 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

35 
> (fn x => Term.replace_dummy_patterns x 1) 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

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

37 

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

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

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

40 
val nm' = case Syntax.parse_term ctxt nm of Const (n, _) => n  _ => nm; 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

41 
val consts = ProofContext.consts_of ctxt; 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

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

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

44 
> Consts.intern consts 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

45 
> Consts.the_abbreviation consts 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

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

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

48 
handle TYPE _ => ProofContext.read_term_pattern ctxt nm 
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset

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

50 

16036  51 
fun read_criterion _ (Name name) = Name name 
52 
 read_criterion _ Intro = Intro 

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

53 
 read_criterion _ IntroIff = IntroIff 
16036  54 
 read_criterion _ Elim = Elim 
55 
 read_criterion _ Dest = Dest 

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

56 
 read_criterion _ Solves = Solves 
24683  57 
 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

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

59 

16036  60 
fun pretty_criterion ctxt (b, c) = 
61 
let 

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

63 
in 

64 
(case c of 

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

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

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

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

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

76 

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

77 

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

78 

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

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

80 

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

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

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

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

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

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

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

89 
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

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

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

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

94 

16088  95 

96 
(* matching theorems *) 

17106  97 

17205  98 
fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy; 
16088  99 

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

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

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

103 

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

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

105 
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

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

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

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

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

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

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

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

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

118 
if Term.is_Const c 
32798  119 
then 
120 
if doiff andalso c = iff_const then 

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

122 
> filter (is_nontrivial thy) 

123 
else [pat] 

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

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

126 

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

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

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

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

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

134 

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

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

138 
> map substsize 
26283  139 
> bestmatch 
16088  140 
end; 
141 

142 

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

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

144 

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

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

148 

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

149 

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

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

151 

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

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

154 
val extract_dest = 
17205  155 
(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

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

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

158 

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

159 
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

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

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

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

164 
assumption is as good as an intro rule with none*) 
17205  165 
if not (null successful) 
33029  166 
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

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

168 

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

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

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

173 
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

174 
in 
18939  175 
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

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

177 

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

179 
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

180 
let 
17205  181 
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

182 
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

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

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

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

190 
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

191 
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

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

17106  195 
if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm) 
17205  196 
andalso not (null successful) 
33029  197 
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

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

199 
else NONE 
16036  200 

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

202 

30143  203 
fun filter_solves ctxt goal = 
204 
let 

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

206 
fun try_thm thm = 

207 
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

208 
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

209 
in 
30143  210 
fn (_, thm) => 
32798  211 
if is_some (Seq.pull (try_thm thm)) 
30143  212 
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

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

214 

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

215 

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

217 

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

219 
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

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

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

223 
val ss = is_matching_thm false extract_simp ctxt false t thm; 
17106  224 
in 
18939  225 
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

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

227 

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

228 

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

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

230 

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

232 
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

233 

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

236 
were used, then constants that may be subject to 

237 
betareduction after substitution of frees should 

238 
not be included for LHS set because they could be 

239 
thrown away by the substituted function. 

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

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

242 
The largest possible set should always be included on 

243 
the RHS.*) 

244 

245 
fun filter_pattern ctxt pat = 

246 
let 

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

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

248 

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

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

250 
 check ((_, thm), c as SOME thm_consts) = 
32798  251 
(if pat_consts subset_string thm_consts andalso 
252 
Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) 

253 
then SOME (0, 0) else NONE, c); 

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

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

255 

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

256 

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

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

258 

16036  259 
local 
260 

261 
fun err_no_goal c = 

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

263 

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

264 
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

265 

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

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

269 
 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

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

271 
 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

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

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

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

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

280 

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

283 

30143  284 
fun app_filters thm = 
285 
let 

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

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

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

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

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

292 

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

293 

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

295 

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

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

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

298 

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

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

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

301 
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

302 

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

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

304 
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

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

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

308 
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

309 

30822  310 
fun lazy_filter filters = 
311 
let 

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

312 
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

313 

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

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

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

319 
in lazy_match end; 
30822  320 

16036  321 
end; 
322 

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

323 

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

325 

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

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

327 

27486  328 
val index_ord = option_ord (K EQUAL); 
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset

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

330 
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

331 
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

332 

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

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

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

337 
 ord => ord) 

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

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

339 

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

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

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

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

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

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

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

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

349 

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

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

351 

30143  352 
fun nicer_shortest ctxt = 
353 
let 

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

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

355 
val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt)); 
29848  356 

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

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

358 
NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space; 
29848  359 

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

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

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

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

364 
in nicer end; 

365 

366 
fun rem_thm_dups nicer xs = 

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

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

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

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

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

372 

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

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

374 

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

375 

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

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

377 

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

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

17972  382 

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

384 

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

385 
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

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

389 
handle ERROR _ => []; 

390 
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

391 
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

392 

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

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

395 

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

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

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

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

399 

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

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

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

402 
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

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

404 

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

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

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

407 
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

408 

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

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

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

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

413 

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

414 
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

415 

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

416 

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

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

419 
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

420 

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

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

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

424 

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

425 
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

426 
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

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

428 

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

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

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

434 
(if returned < found 

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

436 
else "")); 

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

437 

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

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

440 
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

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

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

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

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

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

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

447 
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

448 

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

449 

32798  450 

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

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

452 

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

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

457 
val ctxt = Proof.context_of proof_state; 

32859
204f749f35a9
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32798
diff
changeset

458 
val opt_goal = try Proof.flat_goal proof_state > Option.map #2; 
30822  459 
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

460 

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

462 

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

464 

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

466 
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

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

468 
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

469 
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

470 
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

471 
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

472 
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

473 
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

474 

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

476 
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

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

478 
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

479 
 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

480 
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

481 

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

483 
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

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

485 
>> (Toplevel.no_timing oo find_theorems_cmd)); 
16033
f93ca3d4ffa7
Retrieve theorems from proof context  improved version of
wenzelm
parents:
diff
changeset

486 

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

487 
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

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