author | krauss |
Mon, 30 May 2011 17:07:48 +0200 | |
changeset 43069 | 88e45168272c |
parent 43068 | ac769b5edd1d |
child 43070 | 0318781be055 |
permissions | -rw-r--r-- |
30143 | 1 |
(* Title: Pure/Tools/find_theorems.ML |
26283 | 2 |
Author: Rafal Kolanski and Gerwin Klein, NICTA |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
3 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
4 |
Retrieve theorems from proof context. |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
5 |
*) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
6 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
7 |
signature FIND_THEOREMS = |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
8 |
sig |
16036 | 9 |
datatype 'term criterion = |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
10 |
Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term | |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
11 |
Pattern of 'term |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
12 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
13 |
datatype theorem = |
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
14 |
Internal of Facts.ref * thm | External of Facts.ref * term |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
15 |
|
32738 | 16 |
val tac_limit: int Unsynchronized.ref |
17 |
val limit: int Unsynchronized.ref |
|
43067 | 18 |
|
19 |
val read_criterion: Proof.context -> string criterion -> term criterion |
|
43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
20 |
val query_parser: (bool * string criterion) list parser |
43067 | 21 |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
22 |
val find_theorems: Proof.context -> thm option -> int option -> bool -> |
43067 | 23 |
(bool * term criterion) list -> int option * (Facts.ref * thm) list |
24 |
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
|
25 |
(bool * string criterion) list -> int option * (Facts.ref * thm) list |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
26 |
val filter_theorems: Proof.context -> theorem list -> thm option -> |
43067 | 27 |
int option -> bool -> (bool * term criterion) list -> |
28 |
int option * theorem list |
|
29 |
val filter_theorems_cmd: Proof.context -> theorem list -> thm option -> |
|
41841
c27b0b37041a
Refactor find_theorems to provide a more general filter_facts method
noschinl
parents:
41835
diff
changeset
|
30 |
int option -> bool -> (bool * string criterion) list -> |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
31 |
int option * theorem list |
41841
c27b0b37041a
Refactor find_theorems to provide a more general filter_facts method
noschinl
parents:
41835
diff
changeset
|
32 |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
33 |
val pretty_theorem: Proof.context -> theorem -> Pretty.T |
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
|
34 |
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T |
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
35 |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
36 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
37 |
|
33301 | 38 |
structure Find_Theorems: FIND_THEOREMS = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
39 |
struct |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
40 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
41 |
(** search criteria **) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
42 |
|
16036 | 43 |
datatype 'term criterion = |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
44 |
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
|
45 |
Pattern of 'term; |
16036 | 46 |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
47 |
fun apply_dummies tm = |
33301 | 48 |
let |
49 |
val (xs, _) = Term.strip_abs tm; |
|
50 |
val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs); |
|
51 |
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
|
52 |
|
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
53 |
fun parse_pattern ctxt nm = |
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
54 |
let |
42360 | 55 |
val consts = Proof_Context.consts_of ctxt; |
33301 | 56 |
val nm' = |
57 |
(case Syntax.parse_term ctxt nm of |
|
58 |
Const (c, _) => c |
|
59 |
| _ => Consts.intern consts nm); |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
60 |
in |
33301 | 61 |
(case try (Consts.the_abbreviation consts) nm' of |
42360 | 62 |
SOME (_, rhs) => apply_dummies (Proof_Context.expand_abbrevs ctxt rhs) |
63 |
| NONE => Proof_Context.read_term_pattern ctxt nm) |
|
33036
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
64 |
end; |
c61fe520602b
find_theorems: better handling of abbreviations (by Timothy Bourke)
kleing
parents:
33029
diff
changeset
|
65 |
|
16036 | 66 |
fun read_criterion _ (Name name) = Name name |
67 |
| read_criterion _ Intro = Intro |
|
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
68 |
| read_criterion _ IntroIff = IntroIff |
16036 | 69 |
| read_criterion _ Elim = Elim |
70 |
| read_criterion _ Dest = Dest |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
71 |
| read_criterion _ Solves = Solves |
42360 | 72 |
| 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
|
73 |
| read_criterion ctxt (Pattern str) = Pattern (parse_pattern ctxt str); |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
74 |
|
16036 | 75 |
fun pretty_criterion ctxt (b, c) = |
76 |
let |
|
77 |
fun prfx s = if b then s else "-" ^ s; |
|
78 |
in |
|
79 |
(case c of |
|
80 |
Name name => Pretty.str (prfx "name: " ^ quote name) |
|
81 |
| Intro => Pretty.str (prfx "intro") |
|
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
82 |
| IntroIff => Pretty.str (prfx "introiff") |
16036 | 83 |
| Elim => Pretty.str (prfx "elim") |
84 |
| 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
|
85 |
| Solves => Pretty.str (prfx "solves") |
16088 | 86 |
| Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1, |
24920 | 87 |
Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))] |
16036 | 88 |
| Pattern pat => Pretty.enclose (prfx " \"") "\"" |
24920 | 89 |
[Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)]) |
16036 | 90 |
end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
91 |
|
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
|
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 | |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
97 |
External of Facts.ref * term; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
98 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
99 |
fun 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
|
100 |
| prop_of (External (_, prop)) = prop; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
101 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
102 |
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
|
103 |
| nprems_of (External (_, prop)) = Logic.count_prems prop; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
104 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
105 |
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
|
106 |
| major_prem_of (External (_, prop)) = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
107 |
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
|
108 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
109 |
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
|
110 |
| 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
|
111 |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
112 |
(** search criterion filters **) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
113 |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
114 |
(*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
|
115 |
input: theorem |
17106 | 116 |
output: (p:int, s:int) option, where |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
117 |
NONE indicates no match |
17106 | 118 |
p is the primary sorting criterion |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
119 |
(eg. number of assumptions in the theorem) |
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
120 |
s is the secondary sorting criterion |
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
121 |
(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
|
122 |
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
|
123 |
(biggest p, sum of all s) |
17106 | 124 |
currently p and s only matter for intro, elim, dest and simp filters, |
125 |
otherwise the default ordering is used. |
|
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 |
|
16088 | 128 |
|
129 |
(* matching theorems *) |
|
17106 | 130 |
|
35625 | 131 |
fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy; |
16088 | 132 |
|
32798 | 133 |
(*educated guesses on HOL*) (* FIXME broken *) |
134 |
val boolT = Type ("bool", []); |
|
135 |
val iff_const = Const ("op =", boolT --> boolT --> boolT); |
|
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
136 |
|
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
137 |
(*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
|
138 |
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
|
139 |
trivial matches are ignored. |
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
140 |
returns: smallest substitution size*) |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
141 |
fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src = |
16088 | 142 |
let |
42360 | 143 |
val thy = Proof_Context.theory_of ctxt; |
16088 | 144 |
|
32798 | 145 |
fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat)); |
16486 | 146 |
fun matches pat = |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
147 |
let |
35625 | 148 |
val jpat = Object_Logic.drop_judgment thy pat; |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
149 |
val c = Term.head_of jpat; |
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
150 |
val pats = |
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
151 |
if Term.is_Const c |
32798 | 152 |
then |
153 |
if doiff andalso c = iff_const then |
|
35625 | 154 |
(pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat))) |
32798 | 155 |
|> filter (is_nontrivial thy) |
156 |
else [pat] |
|
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
157 |
else []; |
32798 | 158 |
in filter check_match pats end; |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
159 |
|
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
160 |
fun substsize pat = |
18184 | 161 |
let val (_, subst) = |
162 |
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) |
|
17205 | 163 |
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end; |
16088 | 164 |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
165 |
fun bestmatch [] = NONE |
33029 | 166 |
| bestmatch xs = SOME (foldl1 Int.min xs); |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
167 |
|
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
168 |
val match_thm = matches o refine_term; |
16486 | 169 |
in |
32798 | 170 |
maps match_thm (extract_terms term_src) |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
171 |
|> map substsize |
26283 | 172 |
|> bestmatch |
16088 | 173 |
end; |
174 |
||
175 |
||
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
176 |
(* filter_name *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
177 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
178 |
fun filter_name str_pat theorem = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
179 |
if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem)) |
17205 | 180 |
then SOME (0, 0) else NONE; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
181 |
|
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
|
182 |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
183 |
(* filter intro/elim/dest/solves rules *) |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
184 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
185 |
fun filter_dest ctxt goal theorem = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
186 |
let |
16964
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
187 |
val extract_dest = |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
188 |
(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
|
189 |
hd o Logic.strip_imp_prems); |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
190 |
val prems = Logic.prems_of_goal goal 1; |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
191 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
192 |
fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19476
diff
changeset
|
193 |
val successful = prems |> map_filter try_subst; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
194 |
in |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
195 |
(*if possible, keep best substitution (one with smallest size)*) |
17106 | 196 |
(*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
|
197 |
assumption is as good as an intro rule with none*) |
17205 | 198 |
if not (null successful) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
199 |
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
|
200 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
201 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
202 |
fun filter_intro doiff ctxt goal theorem = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
203 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
204 |
val extract_intro = (single o prop_of, Logic.strip_imp_concl); |
16036 | 205 |
val concl = Logic.concl_of_goal goal 1; |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
206 |
val ss = is_matching_thm doiff extract_intro ctxt true concl theorem; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
207 |
in |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
208 |
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
|
209 |
end; |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
210 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
211 |
fun filter_elim ctxt goal theorem = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
212 |
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
|
213 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
214 |
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
|
215 |
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
|
216 |
val goal_concl = Logic.concl_of_goal goal 1; |
26283 | 217 |
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
|
218 |
val rule_concl = Logic.strip_imp_concl rule; |
26283 | 219 |
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
|
220 |
val rule_tree = combine rule_mp rule_concl; |
26283 | 221 |
fun goal_tree prem = combine prem goal_concl; |
17106 | 222 |
fun try_subst prem = |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
223 |
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
|
224 |
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
|
225 |
in |
32798 | 226 |
(*elim rules always have assumptions, so an elim with one |
227 |
assumption is as good as an intro rule with none*) |
|
42360 | 228 |
if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem) |
17205 | 229 |
andalso not (null successful) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
230 |
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
|
231 |
end |
6a25e42eaff5
Ordering is now: first by number of assumptions, second by the substitution size.
kleing
parents:
16895
diff
changeset
|
232 |
else NONE |
16036 | 233 |
|
32738 | 234 |
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
|
235 |
|
30143 | 236 |
fun filter_solves ctxt goal = |
237 |
let |
|
238 |
fun etacn thm i = Seq.take (! tac_limit) o etac thm i; |
|
239 |
fun try_thm thm = |
|
240 |
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
|
241 |
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
|
242 |
in |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
243 |
fn Internal (_, thm) => |
32798 | 244 |
if is_some (Seq.pull (try_thm thm)) |
30143 | 245 |
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
|
246 |
| External _ => NONE |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
247 |
end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
248 |
|
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
|
249 |
|
16074 | 250 |
(* filter_simp *) |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
251 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
252 |
fun filter_simp ctxt t (Internal (_, thm)) = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
253 |
let |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
254 |
val mksimps = Simplifier.mksimps (simpset_of ctxt); |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
255 |
val extract_simp = |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
256 |
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
257 |
val ss = is_matching_thm false extract_simp ctxt false t thm; |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
258 |
in |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
259 |
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
|
260 |
end |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
261 |
| filter_simp _ _ (External _) = NONE; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
262 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
263 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
264 |
(* filter_pattern *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
265 |
|
32798 | 266 |
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
|
267 |
|
30143 | 268 |
(*Including all constants and frees is only sound because |
269 |
matching uses higher-order patterns. If full matching |
|
270 |
were used, then constants that may be subject to |
|
271 |
beta-reduction after substitution of frees should |
|
272 |
not be included for LHS set because they could be |
|
273 |
thrown away by the substituted function. |
|
274 |
e.g. for (?F 1 2) do not include 1 or 2, if it were |
|
275 |
possible for ?F to be (% x y. 3) |
|
276 |
The largest possible set should always be included on |
|
277 |
the RHS.*) |
|
278 |
||
279 |
fun filter_pattern ctxt pat = |
|
280 |
let |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
281 |
val pat_consts = get_names pat; |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
282 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
283 |
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
|
284 |
| check (theorem, c as SOME thm_consts) = |
33038 | 285 |
(if subset (op =) (pat_consts, thm_consts) andalso |
42360 | 286 |
Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem) |
32798 | 287 |
then SOME (0, 0) else NONE, c); |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
288 |
in check end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
289 |
|
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
|
290 |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
291 |
(* interpret criteria as filters *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
292 |
|
16036 | 293 |
local |
294 |
||
295 |
fun err_no_goal c = |
|
296 |
error ("Current goal required for " ^ c ^ " search criterion"); |
|
297 |
||
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
298 |
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
|
299 |
|
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
300 |
fun filter_crit _ _ (Name name) = apfst (filter_name name) |
16036 | 301 |
| filter_crit _ NONE Intro = err_no_goal "intro" |
41835
9712fae15200
fix non-exhaustive pattern match in find_theorems
noschinl
parents:
39557
diff
changeset
|
302 |
| filter_crit _ NONE IntroIff = err_no_goal "introiff" |
16036 | 303 |
| filter_crit _ NONE Elim = err_no_goal "elim" |
304 |
| 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
|
305 |
| filter_crit _ NONE Solves = err_no_goal "solves" |
31042
d452117ba564
Prototype introiff option for find_theorems.
Timothy Bourke
parents:
30822
diff
changeset
|
306 |
| 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
|
307 |
| filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal)) |
30143 | 308 |
| filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal)) |
309 |
| 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
|
310 |
| filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal) |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
311 |
| filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) |
16088 | 312 |
| filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; |
16036 | 313 |
|
19502 | 314 |
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
|
315 |
|
17756 | 316 |
fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) |
26283 | 317 |
| opt_add _ _ = NONE; |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
318 |
|
30143 | 319 |
fun app_filters thm = |
320 |
let |
|
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
321 |
fun app (NONE, _, _) = NONE |
32798 | 322 |
| app (SOME v, _, []) = SOME (v, thm) |
30143 | 323 |
| app (r, consts, f :: fs) = |
324 |
let val (r', consts') = f (thm, consts) |
|
325 |
in app (opt_add r r', consts', fs) end; |
|
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
326 |
in app end; |
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
327 |
|
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
31042
diff
changeset
|
328 |
|
16036 | 329 |
in |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
330 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
331 |
fun filter_criterion ctxt opt_goal (b, c) = |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
332 |
(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
|
333 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
334 |
fun sorted_filter filters theorems = |
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
335 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
336 |
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
|
337 |
|
16895
df67fc190e06
Sort search results in order of relevance, where relevance =
kleing
parents:
16486
diff
changeset
|
338 |
(*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
|
339 |
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
|
340 |
then by the substitution size*) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
341 |
fun result_ord (((p0, s0), _), ((p1, s1), _)) = |
17205 | 342 |
prod_ord int_ord int_ord ((p1, s1), (p0, s0)); |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
343 |
in map_filter eval_filters theorems |> sort result_ord |> map #2 end; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
344 |
|
30822 | 345 |
fun lazy_filter filters = |
346 |
let |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
347 |
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
|
348 |
|
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
349 |
and first_match [] = NONE |
30822 | 350 |
| first_match (thm :: thms) = |
351 |
(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
|
352 |
NONE => first_match thms |
30822 | 353 |
| SOME (_, t) => SOME (t, lazy_match thms)); |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
354 |
in lazy_match end; |
30822 | 355 |
|
16036 | 356 |
end; |
357 |
||
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
358 |
|
22414 | 359 |
(* removing duplicates, preferring nicer names, roughly n log n *) |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
360 |
|
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
361 |
local |
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
362 |
|
27486 | 363 |
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
|
364 |
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
|
365 |
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
|
366 |
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
|
367 |
|
27486 | 368 |
fun nicer_name (x, i) (y, j) = |
369 |
(case hidden_ord (x, y) of EQUAL => |
|
370 |
(case index_ord (i, j) of EQUAL => |
|
371 |
(case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) |
|
372 |
| ord => ord) |
|
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
373 |
| ord => ord) <> GREATER; |
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
374 |
|
29848 | 375 |
fun rem_cdups nicer xs = |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
376 |
let |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
377 |
fun rem_c rev_seen [] = rev rev_seen |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
378 |
| 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
|
379 |
| 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
|
380 |
if (prop_of t) aconv (prop_of t') |
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
381 |
then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs) |
30822 | 382 |
else rem_c (x :: rev_seen) (y :: xs) |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
383 |
in rem_c [] xs end; |
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
384 |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
385 |
in |
25226
502d8676cdd6
improved notion of 'nicer' fact names (observe some name space properties);
wenzelm
parents:
24920
diff
changeset
|
386 |
|
30143 | 387 |
fun nicer_shortest ctxt = |
388 |
let |
|
30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset
|
389 |
(* FIXME global name space!? *) |
42360 | 390 |
val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt)); |
29848 | 391 |
|
30216
0300b7420b07
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm
parents:
30188
diff
changeset
|
392 |
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
|
393 |
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
|
394 |
(ctxt |
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
395 |
|> Config.put Name_Space.names_long false |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
396 |
|> Config.put Name_Space.names_short false |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42360
diff
changeset
|
397 |
|> Config.put Name_Space.names_unique false) space; |
29848 | 398 |
|
399 |
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = |
|
400 |
nicer_name (shorten x, i) (shorten y, j) |
|
401 |
| nicer (Facts.Fact _) (Facts.Named _) = true |
|
402 |
| nicer (Facts.Named _) (Facts.Fact _) = false; |
|
403 |
in nicer end; |
|
404 |
||
405 |
fun rem_thm_dups nicer xs = |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
406 |
xs ~~ (1 upto length xs) |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
407 |
|> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1)) |
29848 | 408 |
|> rem_cdups nicer |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
409 |
|> sort (int_ord o pairself #2) |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
410 |
|> map #1; |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
411 |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26283
diff
changeset
|
412 |
end; |
22340
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
413 |
|
275802767bf3
Remove duplicates from printed theorems in find_theorems
kleing
parents:
19502
diff
changeset
|
414 |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
415 |
(* print_theorems *) |
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
416 |
|
26283 | 417 |
fun all_facts_of ctxt = |
33381 | 418 |
let |
33382 | 419 |
fun visible_facts facts = |
420 |
Facts.dest_static [] facts |
|
421 |
|> filter_out (Facts.is_concealed facts o #1); |
|
33381 | 422 |
in |
423 |
maps Facts.selections |
|
42360 | 424 |
(visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @ |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
425 |
|
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
426 |
|
42360 | 427 |
visible_facts (Proof_Context.facts_of ctxt)) |
33381 | 428 |
end; |
17972 | 429 |
|
32738 | 430 |
val limit = Unsynchronized.ref 40; |
25992
928594f50893
renamed thms_containing_limit to FindTheorems.limit;
wenzelm
parents:
25226
diff
changeset
|
431 |
|
43067 | 432 |
fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups criteria = |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
433 |
let |
43069
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
434 |
val filters = map (filter_criterion ctxt opt_goal) criteria; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
435 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
436 |
fun find_all theorems = |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
437 |
let |
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
438 |
val raw_matches = sorted_filter filters theorems; |
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
439 |
|
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
440 |
val matches = |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
441 |
if rem_dups |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
442 |
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
|
443 |
else raw_matches; |
28900
53fd5cc685b4
FindTheorems performance improvements (from Timothy Bourke)
kleing
parents:
28211
diff
changeset
|
444 |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
445 |
val len = length matches; |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
446 |
val lim = the_default (! limit) opt_limit; |
34088 | 447 |
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
|
448 |
|
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
449 |
val find = |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
450 |
if rem_dups orelse is_none opt_limit |
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
451 |
then find_all |
30822 | 452 |
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
|
453 |
|
41844
b933142e02d0
generalize find_theorems filters to work on raw propositions, too
krauss
parents:
41841
diff
changeset
|
454 |
in find theorems end; |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
455 |
|
43067 | 456 |
fun filter_theorems_cmd ctxt theorems opt_goal opt_limit rem_dups raw_criteria = |
457 |
filter_theorems ctxt theorems opt_goal opt_limit rem_dups |
|
458 |
(map (apsnd (read_criterion ctxt)) raw_criteria); |
|
459 |
||
460 |
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
|
461 |
let |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
462 |
val assms = |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
463 |
Proof_Context.get_fact ctxt (Facts.named "local.assms") |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
464 |
handle ERROR _ => []; |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
465 |
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
|
466 |
val opt_goal' = Option.map add_prems opt_goal; |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
467 |
in |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
468 |
filter ctxt (map Internal (all_facts_of ctxt)) opt_goal' opt_limit |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
469 |
rem_dups raw_criteria |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
470 |
|> apsnd (map (fn Internal f => f)) |
88e45168272c
moved questionable goal modification out of filter_theorems
krauss
parents:
43068
diff
changeset
|
471 |
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
|
472 |
|
43067 | 473 |
val find_theorems = gen_find_theorems filter_theorems; |
474 |
val find_theorems_cmd = gen_find_theorems filter_theorems_cmd; |
|
475 |
||
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
476 |
fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
477 |
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
478 |
Display.pretty_thm ctxt thm] |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
479 |
| pretty_theorem ctxt (External (thmref, prop)) = Pretty.block |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
480 |
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
481 |
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
|
482 |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
483 |
fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm)); |
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
484 |
|
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
485 |
fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = |
30143 | 486 |
let |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41845
diff
changeset
|
487 |
val start = Timing.start (); |
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
488 |
|
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29848
diff
changeset
|
489 |
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; |
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
490 |
val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt)) |
43067 | 491 |
opt_goal opt_limit rem_dups criteria; |
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
492 |
val returned = length theorems; |
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
31042
diff
changeset
|
493 |
|
30785
15f64e05e703
Limit the number of results returned by auto_solves.
Timothy Bourke
parents:
30693
diff
changeset
|
494 |
val tally_msg = |
30822 | 495 |
(case foundo of |
38335 | 496 |
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)" |
30822 | 497 |
| SOME found => |
38335 | 498 |
"found " ^ string_of_int found ^ " theorem(s)" ^ |
30822 | 499 |
(if returned < found |
500 |
then " (" ^ string_of_int returned ^ " displayed)" |
|
501 |
else "")); |
|
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
502 |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41845
diff
changeset
|
503 |
val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs"; |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
504 |
in |
38335 | 505 |
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: |
506 |
Pretty.str "" :: |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
507 |
(if null theorems then [Pretty.str ("nothing found" ^ end_msg)] |
38335 | 508 |
else |
509 |
[Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @ |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
510 |
map (pretty_theorem ctxt) theorems) |
38335 | 511 |
end |> Pretty.chunks |> Pretty.writeln; |
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
512 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
513 |
|
32798 | 514 |
|
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
|
515 |
(** 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
|
516 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
517 |
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
|
518 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
519 |
val criterion = |
36950 | 520 |
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
521 |
Parse.reserved "intro" >> K Intro || |
|
522 |
Parse.reserved "introiff" >> K IntroIff || |
|
523 |
Parse.reserved "elim" >> K Elim || |
|
524 |
Parse.reserved "dest" >> K Dest || |
|
525 |
Parse.reserved "solves" >> K Solves || |
|
526 |
Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp || |
|
527 |
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
|
528 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
529 |
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
|
530 |
Scan.optional |
36950 | 531 |
(Parse.$$$ "(" |-- |
532 |
Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true |
|
533 |
--| Parse.$$$ ")")) (NONE, true); |
|
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
534 |
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
|
535 |
|
43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
536 |
val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion)); |
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
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 |
val _ = |
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
539 |
Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria" |
36950 | 540 |
Keyword.diag |
43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
541 |
(options -- query_parser |
38334 | 542 |
>> (fn ((opt_lim, rem_dups), spec) => |
543 |
Toplevel.no_timing o |
|
544 |
Toplevel.keep (fn state => |
|
545 |
let |
|
546 |
val ctxt = Toplevel.context_of state; |
|
547 |
val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal; |
|
41845
6611b9cef38b
reactivate time measurement (partly reverting c27b0b37041a);
krauss
parents:
41844
diff
changeset
|
548 |
in print_theorems ctxt opt_goal opt_lim rem_dups spec end))); |
16033
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
549 |
|
f93ca3d4ffa7
Retrieve theorems from proof context -- improved version of
wenzelm
parents:
diff
changeset
|
550 |
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
|
551 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29882
diff
changeset
|
552 |
end; |