src/Pure/Tools/find_theorems.ML
 changeset 41845 6611b9cef38b parent 41844 b933142e02d0 child 42012 2c3fe3cbebae
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Feb 25 16:57:43 2011 +0100
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Feb 25 16:57:44 2011 +0100
1.3 @@ -11,8 +11,7 @@
1.4      Pattern of 'term
1.5
1.6    datatype theorem =
1.7 -    Internal of Facts.ref * thm |
1.8 -    External of Facts.ref * term
1.9 +    Internal of Facts.ref * thm | External of Facts.ref * term
1.10
1.11    val tac_limit: int Unsynchronized.ref
1.12    val limit: int Unsynchronized.ref
1.13 @@ -22,7 +21,9 @@
1.14      int option -> bool -> (bool * string criterion) list ->
1.15      int option * theorem list
1.16
1.17 +  val pretty_theorem: Proof.context -> theorem -> Pretty.T
1.18    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
1.19 +
1.20  end;
1.21
1.22  structure Find_Theorems: FIND_THEOREMS =
1.23 @@ -80,7 +81,7 @@
1.24    end;
1.25
1.26
1.27 -(** theorems, either internal or external (without proof) *)
1.28 +(** theorems, either internal or external (without proof) **)
1.29
1.30  datatype theorem =
1.31    Internal of Facts.ref * thm |
1.32 @@ -452,16 +453,23 @@
1.33       rem_dups raw_criteria
1.34    |> apsnd (map (fn Internal f => f));
1.35
1.36 -fun pretty_thm ctxt (thmref, thm) = Pretty.block
1.37 -  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
1.38 -    Display.pretty_thm ctxt thm];
1.39 +fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
1.40 +      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
1.41 +        Display.pretty_thm ctxt thm]
1.42 +  | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block
1.43 +      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
1.44 +        Syntax.unparse_term ctxt prop];
1.45
1.46 -fun print_theorems ctxt (foundo, thms) raw_criteria =
1.47 +fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
1.48 +
1.49 +fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
1.50    let
1.51      val start = start_timing ();
1.52
1.53      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.54 -    val returned = length thms;
1.55 +    val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
1.56 +      opt_goal opt_limit rem_dups raw_criteria;
1.57 +    val returned = length theorems;
1.58
1.59      val tally_msg =
1.60        (case foundo of
1.61 @@ -476,10 +484,10 @@
1.62    in
1.63      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
1.64      Pretty.str "" ::
1.65 -    (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
1.66 +    (if null theorems then [Pretty.str ("nothing found" ^ end_msg)]
1.67       else
1.68        [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
1.69 -        map (pretty_thm ctxt) thms)
1.70 +        map (pretty_theorem ctxt) theorems)
1.71    end |> Pretty.chunks |> Pretty.writeln;
1.72
1.73
1.74 @@ -515,8 +523,7 @@
1.75            let
1.76              val ctxt = Toplevel.context_of state;
1.77              val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
1.78 -            val found = find_theorems ctxt opt_goal opt_lim rem_dups spec;
1.79 -          in print_theorems ctxt found spec end)));
1.80 +          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
1.81
1.82  end;
1.83
```