tuned;
authorwenzelm
Fri Aug 09 15:14:59 2013 +0200 (2013-08-09)
changeset 529406fce81e92e7c
parent 52939 3b549ee12623
child 52941 28407b5f1c72
tuned;
src/Pure/Tools/find_theorems.ML
     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.6  
     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.13  
    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.20  
    1.21 @@ -275,16 +275,13 @@
    1.22  
    1.23  fun get_names t = Term.add_const_names t (Term.add_free_names t []);
    1.24  
    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.42  
    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.48  
    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.67  
    1.68  
    1.69 -(* removing duplicates, preferring nicer names, roughly n log n *)
    1.70 +(* removing duplicates, preferring nicer names, roughly O(n log n) *)
    1.71  
    1.72  local
    1.73  
    1.74 @@ -412,7 +407,7 @@
    1.75    in nicer end;
    1.76  
    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.92  
    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)" ^