src/Pure/Tools/find_theorems.ML
 changeset 52940 6fce81e92e7c parent 52928 facb4f6dc391 child 52941 28407b5f1c72
1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 15:00:29 2013 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 15:14:59 2013 +0200
1.3 @@ -164,7 +164,7 @@
1.4        is_nontrivial thy pat andalso
1.5        Pattern.matches thy (if po then (pat, obj) else (obj, pat));
1.7 -    fun substsize pat =
1.8 +    fun subst_size pat =
1.9        let val (_, subst) =
1.10          Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty)
1.11        in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
1.12 @@ -174,7 +174,7 @@
1.14      val match_thm = matches o refine_term;
1.15    in
1.16 -    map (substsize o refine_term) (filter match_thm (extract_terms term_src))
1.17 +    map (subst_size o refine_term) (filter match_thm (extract_terms term_src))
1.18      |> bestmatch
1.19    end;
1.21 @@ -275,16 +275,13 @@
1.23  fun get_names t = Term.add_const_names t (Term.add_free_names t []);
1.25 -(*Including all constants and frees is only sound because
1.26 -  matching uses higher-order patterns. If full matching
1.27 -  were used, then constants that may be subject to
1.28 -  beta-reduction after substitution of frees should
1.29 -  not be included for LHS set because they could be
1.30 -  thrown away by the substituted function.
1.31 -  e.g. for (?F 1 2) do not include 1 or 2, if it were
1.32 -       possible for ?F to be (% x y. 3)
1.33 -  The largest possible set should always be included on
1.34 -  the RHS.*)
1.35 +(*Including all constants and frees is only sound because matching
1.36 +  uses higher-order patterns. If full matching were used, then
1.37 +  constants that may be subject to beta-reduction after substitution
1.38 +  of frees should not be included for LHS set because they could be
1.39 +  thrown away by the substituted function.  E.g. for (?F 1 2) do not
1.40 +  include 1 or 2, if it were possible for ?F to be (%x y. 3).  The
1.41 +  largest possible set should always be included on the RHS.*)
1.43  fun filter_pattern ctxt pat =
1.44    let
1.45 @@ -305,16 +302,14 @@
1.46  fun err_no_goal c =
1.47    error ("Current goal required for " ^ c ^ " search criterion");
1.49 -val fix_goal = Thm.prop_of;
1.50 -
1.51  fun filter_crit _ _ (Name name) = apfst (filter_name name)
1.52    | filter_crit _ NONE Intro = err_no_goal "intro"
1.53    | filter_crit _ NONE Elim = err_no_goal "elim"
1.54    | filter_crit _ NONE Dest = err_no_goal "dest"
1.55    | filter_crit _ NONE Solves = err_no_goal "solves"
1.56 -  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
1.57 -  | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
1.58 -  | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
1.59 +  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (Thm.prop_of goal))
1.60 +  | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (Thm.prop_of goal))
1.61 +  | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (Thm.prop_of goal))
1.62    | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
1.63    | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
1.64    | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
1.65 @@ -365,7 +360,7 @@
1.66  end;
1.69 -(* removing duplicates, preferring nicer names, roughly n log n *)
1.70 +(* removing duplicates, preferring nicer names, roughly O(n log n) *)
1.72  local
1.74 @@ -412,7 +407,7 @@
1.75    in nicer end;
1.77  fun rem_thm_dups nicer xs =
1.78 -  xs ~~ (1 upto length xs)
1.79 +  (xs ~~ (1 upto length xs))
1.80    |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1))
1.81    |> rem_cdups nicer
1.82    |> sort (int_ord o pairself #2)
1.83 @@ -500,13 +495,13 @@
1.84  fun pretty_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
1.85    let
1.86      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.87 -    val (foundo, theorems) =
1.88 +    val (opt_found, theorems) =
1.89        filter_theorems ctxt (map Internal (all_facts_of ctxt))
1.90          {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
1.91      val returned = length theorems;
1.93      val tally_msg =
1.94 -      (case foundo of
1.95 +      (case opt_found of
1.96          NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
1.97        | SOME found =>
1.98            "found " ^ string_of_int found ^ " theorem(s)" ^