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;