src/Pure/Tools/find_theorems.ML
 changeset 30143 98a986b02022 parent 30142 8d6145694bb5 child 30186 1f836e949ac2
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Feb 27 15:46:22 2009 +0100
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Feb 27 16:05:40 2009 +0100
1.3 @@ -1,4 +1,4 @@
1.4 -(*  Title:      Pure/Isar/find_theorems.ML
1.5 +(*  Title:      Pure/Tools/find_theorems.ML
1.6      Author:     Rafal Kolanski and Gerwin Klein, NICTA
1.7
1.8  Retrieve theorems from proof context.
1.9 @@ -163,17 +163,20 @@
1.10
1.11  val tac_limit = ref 5;
1.12
1.13 -fun filter_solves ctxt goal = let
1.14 -    val baregoal = Logic.get_goal (prop_of goal) 1;
1.15 +fun filter_solves ctxt goal =
1.16 +  let
1.17 +    val baregoal = Logic.get_goal (Thm.prop_of goal) 1;
1.18
1.19 -    fun etacn thm i = Seq.take (!tac_limit) o etac thm i;
1.20 -    fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal
1.21 -                      else (etacn thm THEN_ALL_NEW
1.22 -                             (Goal.norm_hhf_tac THEN'
1.23 -                               Method.assumption_tac ctxt)) 1 goal;
1.24 +    fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
1.25 +    fun try_thm thm =
1.26 +      if Thm.no_prems thm then rtac thm 1 goal
1.27 +      else (etacn thm THEN_ALL_NEW
1.28 +             (Goal.norm_hhf_tac THEN'
1.29 +               Method.assumption_tac ctxt)) 1 goal;
1.30    in
1.31 -    fn (_, thm) => if (is_some o Seq.pull o try_thm) thm
1.32 -                   then SOME (Thm.nprems_of thm, 0) else NONE
1.33 +    fn (_, thm) =>
1.34 +      if (is_some o Seq.pull o try_thm) thm
1.35 +      then SOME (Thm.nprems_of thm, 0) else NONE
1.36    end;
1.37
1.38
1.39 @@ -195,18 +198,20 @@
1.40
1.41  fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []);
1.42  fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm);
1.43 -  (* Including all constants and frees is only sound because
1.44 -     matching uses higher-order patterns. If full matching
1.45 -     were used, then constants that may be subject to
1.46 -     beta-reduction after substitution of frees should
1.47 -     not be included for LHS set because they could be
1.48 -     thrown away by the substituted function.
1.49 -     e.g. for (?F 1 2) do not include 1 or 2, if it were
1.50 -          possible for ?F to be (% x y. 3)
1.51 -     The largest possible set should always be included on
1.52 -     the RHS. *)
1.53
1.54 -fun filter_pattern ctxt pat = let
1.55 +(*Including all constants and frees is only sound because
1.56 +  matching uses higher-order patterns. If full matching
1.57 +  were used, then constants that may be subject to
1.58 +  beta-reduction after substitution of frees should
1.59 +  not be included for LHS set because they could be
1.60 +  thrown away by the substituted function.
1.61 +  e.g. for (?F 1 2) do not include 1 or 2, if it were
1.62 +       possible for ?F to be (% x y. 3)
1.63 +  The largest possible set should always be included on
1.64 +  the RHS.*)
1.65 +
1.66 +fun filter_pattern ctxt pat =
1.67 +  let
1.68      val pat_consts = get_names pat;
1.69
1.70      fun check (t, NONE) = check (t, SOME (get_thm_names t))
1.71 @@ -233,12 +238,9 @@
1.72    | filter_crit _ NONE Elim = err_no_goal "elim"
1.73    | filter_crit _ NONE Dest = err_no_goal "dest"
1.74    | filter_crit _ NONE Solves = err_no_goal "solves"
1.75 -  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt
1.76 -                                                  (fix_goal goal))
1.77 -  | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt
1.78 -                                                  (fix_goal goal))
1.79 -  | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt
1.80 -                                                  (fix_goal goal))
1.81 +  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
1.82 +  | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
1.83 +  | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
1.84    | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
1.85    | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat)
1.86    | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
1.87 @@ -248,11 +250,13 @@
1.88  fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
1.89    | opt_add _ _ = NONE;
1.90
1.91 -fun app_filters thm = let
1.92 +fun app_filters thm =
1.93 +  let
1.94      fun app (NONE, _, _) = NONE
1.95        | app (SOME v, consts, []) = SOME (v, thm)
1.96 -      | app (r, consts, f::fs) = let val (r', consts') = f (thm, consts)
1.97 -                                 in app (opt_add r r', consts', fs) end;
1.98 +      | app (r, consts, f :: fs) =
1.99 +          let val (r', consts') = f (thm, consts)
1.100 +          in app (opt_add r r', consts', fs) end;
1.101    in app end;
1.102
1.103  in
1.104 @@ -302,7 +306,8 @@
1.105
1.106  in
1.107
1.108 -fun nicer_shortest ctxt = let
1.109 +fun nicer_shortest ctxt =
1.110 +  let
1.111      val ns = ProofContext.theory_of ctxt
1.112               |> PureThy.facts_of
1.113               |> Facts.space_of;
1.114 @@ -354,7 +359,8 @@
1.115        else raw_matches;
1.116    in matches end;
1.117
1.118 -fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let
1.119 +fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
1.120 +  let
1.121      val start = start_timing ();
1.122
1.123      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
```