summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.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)" ^