author wenzelm Fri, 09 Aug 2013 15:14:59 +0200 changeset 52940 6fce81e92e7c parent 52939 3b549ee12623 child 52941 28407b5f1c72
tuned;
--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 15:00:29 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 15:14:59 2013 +0200
@@ -164,7 +164,7 @@
is_nontrivial thy pat andalso
Pattern.matches thy (if po then (pat, obj) else (obj, pat));

-    fun substsize pat =
+    fun subst_size pat =
let val (_, subst) =
Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
@@ -174,7 +174,7 @@

val match_thm = matches o refine_term;
in
-    map (substsize o refine_term) (filter match_thm (extract_terms term_src))
+    map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
|> bestmatch
end;

@@ -275,16 +275,13 @@

-(*Including all constants and frees is only sound because
-  matching uses higher-order patterns. If full matching
-  were used, then constants that may be subject to
-  beta-reduction after substitution of frees should
-  not be included for LHS set because they could be
-  thrown away by the substituted function.
-  e.g. for (?F 1 2) do not include 1 or 2, if it were
-       possible for ?F to be (% x y. 3)
-  The largest possible set should always be included on
-  the RHS.*)
+(*Including all constants and frees is only sound because matching
+  uses higher-order patterns. If full matching were used, then
+  constants that may be subject to beta-reduction after substitution
+  of frees should not be included for LHS set because they could be
+  thrown away by the substituted function.  E.g. for (?F 1 2) do not
+  include 1 or 2, if it were possible for ?F to be (%x y. 3).  The
+  largest possible set should always be included on the RHS.*)

fun filter_pattern ctxt pat =
let
@@ -305,16 +302,14 @@
fun err_no_goal c =
error ("Current goal required for " ^ c ^ " search criterion");

-val fix_goal = Thm.prop_of;
-
fun filter_crit _ _ (Name name) = apfst (filter_name name)
| filter_crit _ NONE Intro = err_no_goal "intro"
| filter_crit _ NONE Elim = err_no_goal "elim"
| filter_crit _ NONE Dest = err_no_goal "dest"
| filter_crit _ NONE Solves = err_no_goal "solves"
-  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
-  | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
-  | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
+  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal))
+  | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal))
+  | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal))
| filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
| filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
| filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
@@ -365,7 +360,7 @@
end;

-(* removing duplicates, preferring nicer names, roughly n log n *)
+(* removing duplicates, preferring nicer names, roughly O(n log n) *)

local

@@ -412,7 +407,7 @@
in nicer end;

fun rem_thm_dups nicer xs =
-  xs ~~ (1 upto length xs)
+  (xs ~~ (1 upto length xs))
|> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
|> rem_cdups nicer
|> sort (int_ord o pairself #2)
@@ -500,13 +495,13 @@
fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
-    val (foundo, theorems) =
+    val (opt_found, theorems) =
filter_theorems ctxt (map Internal (all_facts_of ctxt))
{goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
val returned = length theorems;

val tally_msg =
-      (case foundo of
+      (case opt_found of
NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
| SOME found =>
"found " ^ string_of_int found ^ " theorem(s)" ^