author | wenzelm |
Fri, 09 Aug 2013 15:49:50 +0200 | |
changeset 52941 | 28407b5f1c72 |
parent 52940 | 6fce81e92e7c |
child 52942 | 07093b66fc9d |
permissions | -rw-r--r-- |
30143 | 1 |
(* Title: Pure/Tools/find_theorems.ML |
26283 | 2 |
Author: Rafal Kolanski and Gerwin Klein, NICTA |
46718 | 3 |
Author: Lars Noschinski and Alexander Krauss, TU Muenchen |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
4 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
5 |
Retrieve theorems from proof context. |
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 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
8 |
signature FIND_THEOREMS = |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
9 |
sig |
16036 | 10 |
datatype 'term criterion = |
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
11 |
Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term |
43070 | 12 |
type 'term query = { |
13 |
goal: thm option, |
|
14 |
limit: int option, |
|
15 |
rem_dups: bool, |
|
16 |
criteria: (bool * 'term criterion) list |
|
17 |
} |
|
52925 | 18 |
val read_query: Position.T -> string -> (bool * string criterion) list |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
19 |
val find_theorems: Proof.context -> thm option -> int option -> bool -> |
43067 | 20 |
(bool * term criterion) list -> int option * (Facts.ref * thm) list |
21 |
val find_theorems_cmd: Proof.context -> thm option -> int option -> bool -> |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
22 |
(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
|
23 |
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
24 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
25 |
|
33301 | 26 |
structure Find_Theorems: FIND_THEOREMS = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
27 |
struct |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
28 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
29 |
(** search criteria **) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
30 |
|
16036 | 31 |
datatype 'term criterion = |
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
32 |
Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term; |
16036 | 33 |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
34 |
fun apply_dummies tm = |
33301 | 35 |
let |
36 |
val (xs, _) = Term.strip_abs tm; |
|
37 |
val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs); |
|
38 |
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
|
39 |
|
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
40 |
fun parse_pattern ctxt nm = |
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
41 |
let |
42360 | 42 |
val consts = Proof_Context.consts_of ctxt; |
33301 | 43 |
val nm' = |
44 |
(case Syntax.parse_term ctxt nm of |
|
45 |
Const (c, _) => c |
|
46 |
| _ => Consts.intern consts nm); |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
47 |
in |
33301 | 48 |
(case try (Consts.the_abbreviation consts) nm' of |
42360 | 49 |
SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs) |
50 |
| NONE => Proof_Context.read_term_pattern ctxt nm) |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
51 |
end; |
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
52 |
|
16036 | 53 |
fun read_criterion _ (Name name) = Name name |
54 |
| read_criterion _ Intro = Intro |
|
55 |
| read_criterion _ Elim = Elim |
|
56 |
| read_criterion _ Dest = Dest |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
57 |
| read_criterion _ Solves = Solves |
42360 | 58 |
| read_criterion ctxt (Simp str) = Simp (Proof_Context.read_term_pattern ctxt str) |
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
59 |
| read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str); |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
60 |
|
16036 | 61 |
fun pretty_criterion ctxt (b, c) = |
62 |
let |
|
63 |
fun prfx s = if b then s else "-" ^ s; |
|
64 |
in |
|
65 |
(case c of |
|
66 |
Name name => Pretty.str (prfx "name: " ^ quote name) |
|
67 |
| Intro => Pretty.str (prfx "intro") |
|
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 |
|
43620 | 78 |
|
43070 | 79 |
(** queries **) |
80 |
||
81 |
type 'term query = { |
|
82 |
goal: thm option, |
|
83 |
limit: int option, |
|
84 |
rem_dups: bool, |
|
85 |
criteria: (bool * 'term criterion) list |
|
86 |
}; |
|
87 |
||
88 |
fun map_criteria f {goal, limit, rem_dups, criteria} = |
|
46718 | 89 |
{goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria}; |
43070 | 90 |
|
43620 | 91 |
|
92 |
||
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
93 |
(** theorems, either internal or external (without proof) **) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
94 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
95 |
datatype theorem = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
96 |
Internal of Facts.ref * thm | |
43071 | 97 |
External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *) |
98 |
||
99 |
fun fact_ref_markup (Facts.Named ((name, pos), SOME [Facts.Single i])) = |
|
100 |
Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)] |
|
101 |
| fact_ref_markup (Facts.Named ((name, pos), NONE)) = |
|
102 |
Position.markup pos o Markup.properties [("name", name)] |
|
43620 | 103 |
| fact_ref_markup fact_ref = raise Fail "bad fact ref"; |
43071 | 104 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
105 |
fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
106 |
| prop_of (External (_, prop)) = prop; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
107 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
108 |
fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
109 |
| nprems_of (External (_, prop)) = Logic.count_prems prop; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
110 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
111 |
fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
112 |
| major_prem_of (External (_, prop)) = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
113 |
Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop)); |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
114 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
115 |
fun fact_ref_of (Internal (fact_ref, _)) = fact_ref |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
116 |
| fact_ref_of (External (fact_ref, _)) = fact_ref; |
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
117 |
|
43620 | 118 |
|
119 |
||
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
120 |
(** search criterion filters **) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
121 |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
122 |
(*generated filters are to be of the form |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
123 |
input: theorem |
17106 | 124 |
output: (p:int, s:int) option, where |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
125 |
NONE indicates no match |
17106 | 126 |
p is the primary sorting criterion |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
127 |
(eg. number of assumptions in the theorem) |
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
128 |
s is the secondary sorting criterion |
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
129 |
(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
|
130 |
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
|
131 |
(biggest p, sum of all s) |
17106 | 132 |
currently p and s only matter for intro, elim, dest and simp filters, |
133 |
otherwise the default ordering is used. |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
134 |
*) |
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
135 |
|
16088 | 136 |
|
137 |
(* matching theorems *) |
|
17106 | 138 |
|
35625 | 139 |
fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy; |
16088 | 140 |
|
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
141 |
(*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
|
142 |
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
|
143 |
trivial matches are ignored. |
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
144 |
returns: smallest substitution size*) |
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
145 |
fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src = |
16088 | 146 |
let |
42360 | 147 |
val thy = Proof_Context.theory_of ctxt; |
16088 | 148 |
|
16486 | 149 |
fun matches pat = |
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
150 |
is_nontrivial thy pat andalso |
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
151 |
Pattern.matches thy (if po then (pat, obj) else (obj, pat)); |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
152 |
|
52940 | 153 |
fun subst_size pat = |
18184 | 154 |
let val (_, subst) = |
155 |
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) |
|
17205 | 156 |
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end; |
16088 | 157 |
|
52941 | 158 |
fun best_match [] = NONE |
159 |
| best_match xs = SOME (foldl1 Int.min xs); |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
160 |
|
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
161 |
val match_thm = matches o refine_term; |
16486 | 162 |
in |
52940 | 163 |
map (subst_size o refine_term) (filter match_thm (extract_terms term_src)) |
52941 | 164 |
|> best_match |
16088 | 165 |
end; |
166 |
||
167 |
||
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
168 |
(* filter_name *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
169 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
170 |
fun filter_name str_pat theorem = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
171 |
if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem)) |
17205 | 172 |
then SOME (0, 0) else NONE; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
173 |
|
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
|
174 |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
175 |
(* filter intro/elim/dest/solves rules *) |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
176 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
177 |
fun filter_dest ctxt goal theorem = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
178 |
let |
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
179 |
val extract_dest = |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
180 |
(fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem], |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
181 |
hd o Logic.strip_imp_prems); |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
182 |
val prems = Logic.prems_of_goal goal 1; |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
183 |
|
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
184 |
fun try_subst prem = is_matching_thm extract_dest ctxt true prem theorem; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset
|
185 |
val successful = prems |> map_filter try_subst; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
186 |
in |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
187 |
(*if possible, keep best substitution (one with smallest size)*) |
17106 | 188 |
(*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
|
189 |
assumption is as good as an intro rule with none*) |
17205 | 190 |
if not (null successful) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
191 |
then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
192 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
193 |
|
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
194 |
fun filter_intro ctxt goal theorem = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
195 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
196 |
val extract_intro = (single o prop_of, Logic.strip_imp_concl); |
16036 | 197 |
val concl = Logic.concl_of_goal goal 1; |
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
198 |
val ss = is_matching_thm extract_intro ctxt true concl theorem; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
199 |
in |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
200 |
if is_some ss then SOME (nprems_of theorem, the ss) else NONE |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
201 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
202 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
203 |
fun filter_elim ctxt goal theorem = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
204 |
if nprems_of theorem > 0 then |
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
205 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
206 |
val rule = prop_of theorem; |
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
207 |
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
|
208 |
val goal_concl = Logic.concl_of_goal goal 1; |
26283 | 209 |
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
|
210 |
val rule_concl = Logic.strip_imp_concl rule; |
52941 | 211 |
fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2); (* FIXME ?? *) |
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
212 |
val rule_tree = combine rule_mp rule_concl; |
26283 | 213 |
fun goal_tree prem = combine prem goal_concl; |
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
214 |
fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset
|
215 |
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
|
216 |
in |
32798 | 217 |
(*elim rules always have assumptions, so an elim with one |
218 |
assumption is as good as an intro rule with none*) |
|
42360 | 219 |
if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem) |
17205 | 220 |
andalso not (null successful) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
221 |
then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE |
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
222 |
end |
46718 | 223 |
else NONE; |
16036 | 224 |
|
30143 | 225 |
fun filter_solves ctxt goal = |
226 |
let |
|
52704
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset
|
227 |
val thy' = |
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset
|
228 |
Proof_Context.theory_of ctxt |
52788 | 229 |
|> Context_Position.set_visible_global (Context_Position.is_visible ctxt); |
52704
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset
|
230 |
val ctxt' = Proof_Context.transfer thy' ctxt; |
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset
|
231 |
val goal' = Thm.transfer thy' goal; |
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset
|
232 |
|
52941 | 233 |
fun limited_etac thm i = |
52702 | 234 |
Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i; |
30143 | 235 |
fun try_thm thm = |
52704
b824497c8e86
modify background theory where it is actually required (cf. 51dfdcd88e84);
wenzelm
parents:
52703
diff
changeset
|
236 |
if Thm.no_prems thm then rtac thm 1 goal' |
52941 | 237 |
else (limited_etac 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
|
238 |
in |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
239 |
fn Internal (_, thm) => |
43620 | 240 |
if is_some (Seq.pull (try_thm thm)) |
241 |
then SOME (Thm.nprems_of thm, 0) else NONE |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
242 |
| External _ => NONE |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
243 |
end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
244 |
|
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
|
245 |
|
16074 | 246 |
(* filter_simp *) |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
247 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
248 |
fun filter_simp ctxt t (Internal (_, thm)) = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
249 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
250 |
val mksimps = Simplifier.mksimps ctxt; |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
251 |
val extract_simp = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
252 |
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); |
46717
b09afce1e54f
removed broken/unused introiff (cf. d452117ba564);
wenzelm
parents:
46716
diff
changeset
|
253 |
val ss = is_matching_thm extract_simp ctxt false t thm; |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
254 |
in |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
255 |
if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
256 |
end |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
257 |
| filter_simp _ _ (External _) = NONE; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
258 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
259 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
260 |
(* filter_pattern *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
261 |
|
32798 | 262 |
fun get_names t = Term.add_const_names t (Term.add_free_names t []); |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
263 |
|
52940 | 264 |
(*Including all constants and frees is only sound because matching |
265 |
uses higher-order patterns. If full matching were used, then |
|
266 |
constants that may be subject to beta-reduction after substitution |
|
267 |
of frees should not be included for LHS set because they could be |
|
268 |
thrown away by the substituted function. E.g. for (?F 1 2) do not |
|
269 |
include 1 or 2, if it were possible for ?F to be (%x y. 3). The |
|
270 |
largest possible set should always be included on the RHS.*) |
|
30143 | 271 |
|
272 |
fun filter_pattern ctxt pat = |
|
273 |
let |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
274 |
val pat_consts = get_names pat; |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
275 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
276 |
fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem))) |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
277 |
| check (theorem, c as SOME thm_consts) = |
33038 | 278 |
(if subset (op =) (pat_consts, thm_consts) andalso |
42360 | 279 |
Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem) |
32798 | 280 |
then SOME (0, 0) else NONE, c); |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
281 |
in check end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
282 |
|
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
|
283 |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
284 |
(* interpret criteria as filters *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
285 |
|
16036 | 286 |
local |
287 |
||
288 |
fun err_no_goal c = |
|
289 |
error ("Current goal required for " ^ c ^ " search criterion"); |
|
290 |
||
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
291 |
fun filter_crit _ _ (Name name) = apfst (filter_name name) |
16036 | 292 |
| filter_crit _ NONE Intro = err_no_goal "intro" |
293 |
| filter_crit _ NONE Elim = err_no_goal "elim" |
|
294 |
| filter_crit _ NONE Dest = err_no_goal "dest" |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
295 |
| filter_crit _ NONE Solves = err_no_goal "solves" |
52940 | 296 |
| filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal)) |
297 |
| filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal)) |
|
298 |
| filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal)) |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
299 |
| filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal) |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
300 |
| filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) |
16088 | 301 |
| filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; |
16036 | 302 |
|
19502 | 303 |
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
|
304 |
|
17756 | 305 |
fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) |
26283 | 306 |
| opt_add _ _ = NONE; |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
307 |
|
30143 | 308 |
fun app_filters thm = |
309 |
let |
|
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
310 |
fun app (NONE, _, _) = NONE |
32798 | 311 |
| app (SOME v, _, []) = SOME (v, thm) |
30143 | 312 |
| app (r, consts, f :: fs) = |
313 |
let val (r', consts') = f (thm, consts) |
|
314 |
in app (opt_add r r', consts', fs) end; |
|
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
315 |
in app end; |
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
316 |
|
16036 | 317 |
in |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
318 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
319 |
fun filter_criterion ctxt opt_goal (b, c) = |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
320 |
(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
|
321 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
322 |
fun sorted_filter filters theorems = |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
323 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
324 |
fun eval_filters theorem = app_filters theorem (SOME (0, 0), NONE, filters); |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
325 |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
326 |
(*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
|
327 |
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
|
328 |
then by the substitution size*) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
329 |
fun result_ord (((p0, s0), _), ((p1, s1), _)) = |
17205 | 330 |
prod_ord int_ord int_ord ((p1, s1), (p0, s0)); |
46977 | 331 |
in |
332 |
grouped 100 Par_List.map eval_filters theorems |
|
333 |
|> map_filter I |> sort result_ord |> map #2 |
|
334 |
end; |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
335 |
|
30822 | 336 |
fun lazy_filter filters = |
337 |
let |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
338 |
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
|
339 |
and first_match [] = NONE |
30822 | 340 |
| first_match (thm :: thms) = |
341 |
(case app_filters thm (SOME (0, 0), NONE, filters) of |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
342 |
NONE => first_match thms |
30822 | 343 |
| SOME (_, t) => SOME (t, lazy_match thms)); |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
344 |
in lazy_match end; |
30822 | 345 |
|
16036 | 346 |
end; |
347 |
||
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
348 |
|
52940 | 349 |
(* removing duplicates, preferring nicer names, roughly O(n log n) *) |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
350 |
|
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
351 |
local |
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
352 |
|
27486 | 353 |
val index_ord = option_ord (K EQUAL); |
33095
bbd52d2f8696
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents:
33039
diff
changeset
|
354 |
val hidden_ord = bool_ord o pairself Name_Space.is_hidden; |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30318
diff
changeset
|
355 |
val qual_ord = int_ord o pairself (length o Long_Name.explode); |
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
356 |
val txt_ord = int_ord o pairself size; |
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
357 |
|
27486 | 358 |
fun nicer_name (x, i) (y, j) = |
359 |
(case hidden_ord (x, y) of EQUAL => |
|
360 |
(case index_ord (i, j) of EQUAL => |
|
361 |
(case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) |
|
362 |
| ord => ord) |
|
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
363 |
| ord => ord) <> GREATER; |
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
364 |
|
29848 | 365 |
fun rem_cdups nicer xs = |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
366 |
let |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
367 |
fun rem_c rev_seen [] = rev rev_seen |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
368 |
| rem_c rev_seen [x] = rem_c (x :: rev_seen) [] |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
369 |
| rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
370 |
if (prop_of t) aconv (prop_of t') |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
371 |
then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs) |
30822 | 372 |
else rem_c (x :: rev_seen) (y :: xs) |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
373 |
in rem_c [] xs end; |
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
374 |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
375 |
in |
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
376 |
|
30143 | 377 |
fun nicer_shortest ctxt = |
378 |
let |
|
46718 | 379 |
(* FIXME Why global name space!?? *) |
42360 | 380 |
val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt)); |
29848 | 381 |
|
30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset
|
382 |
val shorten = |
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42012
diff
changeset
|
383 |
Name_Space.extern |
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42012
diff
changeset
|
384 |
(ctxt |
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
385 |
|> Config.put Name_Space.names_long false |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
386 |
|> Config.put Name_Space.names_short false |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
387 |
|> Config.put Name_Space.names_unique false) space; |
29848 | 388 |
|
389 |
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = |
|
390 |
nicer_name (shorten x, i) (shorten y, j) |
|
391 |
| nicer (Facts.Fact _) (Facts.Named _) = true |
|
392 |
| nicer (Facts.Named _) (Facts.Fact _) = false; |
|
393 |
in nicer end; |
|
394 |
||
395 |
fun rem_thm_dups nicer xs = |
|
52940 | 396 |
(xs ~~ (1 upto length xs)) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
397 |
|> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1)) |
29848 | 398 |
|> rem_cdups nicer |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
399 |
|> sort (int_ord o pairself #2) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
400 |
|> map #1; |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
401 |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
402 |
end; |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
403 |
|
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
404 |
|
52941 | 405 |
|
406 |
(** main operations **) |
|
407 |
||
408 |
(* filter_theorems *) |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
409 |
|
26283 | 410 |
fun all_facts_of ctxt = |
33381 | 411 |
let |
33382 | 412 |
fun visible_facts facts = |
413 |
Facts.dest_static [] facts |
|
414 |
|> filter_out (Facts.is_concealed facts o #1); |
|
33381 | 415 |
in |
416 |
maps Facts.selections |
|
42360 | 417 |
(visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @ |
418 |
visible_facts (Proof_Context.facts_of ctxt)) |
|
33381 | 419 |
end; |
17972 | 420 |
|
43070 | 421 |
fun filter_theorems ctxt theorems query = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
422 |
let |
46718 | 423 |
val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query; |
43069
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
424 |
val filters = map (filter_criterion ctxt opt_goal) criteria; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
425 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
426 |
fun find_all theorems = |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
427 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
428 |
val raw_matches = sorted_filter filters theorems; |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
429 |
|
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
430 |
val matches = |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
431 |
if rem_dups |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
432 |
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
|
433 |
else raw_matches; |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
434 |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
435 |
val len = length matches; |
52702 | 436 |
val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit; |
34088 | 437 |
in (SOME len, drop (Int.max (len - lim, 0)) matches) end; |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
438 |
|
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
439 |
val find = |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
440 |
if rem_dups orelse is_none opt_limit |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
441 |
then find_all |
30822 | 442 |
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
|
443 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
444 |
in find theorems end; |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
445 |
|
46718 | 446 |
fun filter_theorems_cmd ctxt theorems raw_query = |
52941 | 447 |
filter_theorems ctxt theorems (map_criteria (map (apsnd (read_criterion ctxt))) raw_query); |
448 |
||
449 |
||
450 |
(* find_theorems *) |
|
451 |
||
452 |
local |
|
43067 | 453 |
|
454 |
fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria = |
|
43069
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
455 |
let |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
456 |
val assms = |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
457 |
Proof_Context.get_fact ctxt (Facts.named "local.assms") |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
458 |
handle ERROR _ => []; |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
459 |
val add_prems = Seq.hd o TRY (Method.insert_tac assms 1); |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
460 |
val opt_goal' = Option.map add_prems opt_goal; |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
461 |
in |
46718 | 462 |
filter ctxt (map Internal (all_facts_of ctxt)) |
463 |
{goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria} |
|
43069
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
464 |
|> apsnd (map (fn Internal f => f)) |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
465 |
end; |
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
|
466 |
|
52941 | 467 |
in |
468 |
||
43067 | 469 |
val find_theorems = gen_find_theorems filter_theorems; |
470 |
val find_theorems_cmd = gen_find_theorems filter_theorems_cmd; |
|
471 |
||
52941 | 472 |
end; |
473 |
||
474 |
||
475 |
(* pretty_theorems *) |
|
476 |
||
477 |
local |
|
478 |
||
49888 | 479 |
fun pretty_ref ctxt thmref = |
480 |
let |
|
481 |
val (name, sel) = |
|
482 |
(case thmref of |
|
483 |
Facts.Named ((name, _), sel) => (name, sel) |
|
484 |
| Facts.Fact _ => raise Fail "Illegal literal fact"); |
|
485 |
in |
|
486 |
[Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name), |
|
487 |
Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1] |
|
488 |
end; |
|
489 |
||
490 |
fun pretty_theorem ctxt (Internal (thmref, thm)) = |
|
491 |
Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]) |
|
492 |
| pretty_theorem ctxt (External (thmref, prop)) = |
|
493 |
Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]); |
|
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
|
494 |
|
52941 | 495 |
in |
496 |
||
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
497 |
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm)); |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
498 |
|
52941 | 499 |
fun pretty_theorems state opt_limit rem_dups raw_criteria = |
30143 | 500 |
let |
52941 | 501 |
val ctxt = Proof.context_of state; |
502 |
val opt_goal = try Proof.simple_goal state |> Option.map #goal; |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
503 |
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; |
52941 | 504 |
|
52940 | 505 |
val (opt_found, theorems) = |
52855 | 506 |
filter_theorems ctxt (map Internal (all_facts_of ctxt)) |
507 |
{goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria}; |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
508 |
val returned = length theorems; |
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
31042
diff
changeset
|
509 |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
510 |
val tally_msg = |
52940 | 511 |
(case opt_found of |
38335 | 512 |
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)" |
30822 | 513 |
| SOME found => |
38335 | 514 |
"found " ^ string_of_int found ^ " theorem(s)" ^ |
30822 | 515 |
(if returned < found |
516 |
then " (" ^ string_of_int returned ^ " displayed)" |
|
517 |
else "")); |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
518 |
in |
38335 | 519 |
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: |
520 |
Pretty.str "" :: |
|
46716
c45a4427db39
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
wenzelm
parents:
46713
diff
changeset
|
521 |
(if null theorems then [Pretty.str "nothing found"] |
38335 | 522 |
else |
46716
c45a4427db39
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
wenzelm
parents:
46713
diff
changeset
|
523 |
[Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ |
52927 | 524 |
grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) theorems) |
52855 | 525 |
end |> Pretty.fbreaks |> curry Pretty.blk 0; |
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
|
526 |
|
52941 | 527 |
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
|
528 |
|
32798 | 529 |
|
46718 | 530 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52863
diff
changeset
|
531 |
(** Isar command syntax **) |
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
|
532 |
|
52941 | 533 |
fun proof_state st = |
534 |
(case try Toplevel.proof_of st of |
|
535 |
SOME state => state |
|
536 |
| NONE => Proof.init (Toplevel.context_of st)); |
|
537 |
||
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
|
538 |
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
|
539 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
540 |
val criterion = |
36950 | 541 |
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
542 |
Parse.reserved "intro" >> K Intro || |
|
543 |
Parse.reserved "elim" >> K Elim || |
|
544 |
Parse.reserved "dest" >> K Dest || |
|
545 |
Parse.reserved "solves" >> K Solves || |
|
546 |
Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp || |
|
547 |
Parse.term >> Pattern; |
|
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
548 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
549 |
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
|
550 |
Scan.optional |
36950 | 551 |
(Parse.$$$ "(" |-- |
552 |
Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true |
|
553 |
--| Parse.$$$ ")")) (NONE, true); |
|
52855 | 554 |
|
52925 | 555 |
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion); |
52855 | 556 |
|
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
|
557 |
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
|
558 |
|
52925 | 559 |
fun read_query pos str = |
560 |
Outer_Syntax.scan pos str |
|
52855 | 561 |
|> filter Token.is_proper |
52925 | 562 |
|> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof))) |
563 |
|> #1; |
|
43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
564 |
|
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
|
565 |
val _ = |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
46977
diff
changeset
|
566 |
Outer_Syntax.improper_command @{command_spec "find_theorems"} |
50214 | 567 |
"find theorems meeting specified criteria" |
52925 | 568 |
(options -- query >> (fn ((opt_lim, rem_dups), spec) => |
52941 | 569 |
Toplevel.keep (fn st => |
570 |
Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec)))); |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
571 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
572 |
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
|
573 |
|
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52788
diff
changeset
|
574 |
|
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52788
diff
changeset
|
575 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52863
diff
changeset
|
576 |
(** PIDE query operation **) |
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52851
diff
changeset
|
577 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52863
diff
changeset
|
578 |
val _ = |
52925 | 579 |
Query_Operation.register "find_theorems" (fn st => fn args => |
52941 | 580 |
if can Toplevel.context_of st then |
581 |
Pretty.string_of |
|
582 |
(pretty_theorems (proof_state st) NONE false (maps (read_query Position.none) args)) |
|
583 |
else error "Unknown context"); |
|
52851
e71b5160f242
minimal print function "find_theorems", which merely echos its arguments;
wenzelm
parents:
52788
diff
changeset
|
584 |
|
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
|
585 |
end; |