src/Pure/Tools/find_theorems.ML
changeset 43067 76e1d25c6357
parent 42669 04dfffda5671
child 43068 ac769b5edd1d
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:00:38 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.3 @@ -15,9 +15,17 @@
     1.4  
     1.5    val tac_limit: int Unsynchronized.ref
     1.6    val limit: int Unsynchronized.ref
     1.7 +
     1.8 +  val read_criterion: Proof.context -> string criterion -> term criterion
     1.9 +
    1.10    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    1.11 +    (bool * term criterion) list -> int option * (Facts.ref * thm) list
    1.12 +  val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
    1.13      (bool * string criterion) list -> int option * (Facts.ref * thm) list
    1.14    val filter_theorems: Proof.context -> theorem list -> thm option ->
    1.15 +    int option -> bool -> (bool * term criterion) list ->
    1.16 +    int option * theorem list
    1.17 +  val filter_theorems_cmd: Proof.context -> theorem list -> thm option ->
    1.18      int option -> bool -> (bool * string criterion) list ->
    1.19      int option * theorem list
    1.20  
    1.21 @@ -420,7 +428,7 @@
    1.22  
    1.23  val limit = Unsynchronized.ref 40;
    1.24  
    1.25 -fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
    1.26 +fun filter_theorems ctxt theorems opt_goal opt_limit rem_dups criteria =
    1.27    let
    1.28      val assms =
    1.29        Proof_Context.get_fact ctxt (Facts.named "local.assms")
    1.30 @@ -428,7 +436,6 @@
    1.31      val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
    1.32      val opt_goal' = Option.map add_prems opt_goal;
    1.33  
    1.34 -    val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.35      val filters = map (filter_criterion ctxt opt_goal') criteria;
    1.36  
    1.37      fun find_all theorems =
    1.38 @@ -451,11 +458,18 @@
    1.39  
    1.40    in find theorems end;
    1.41  
    1.42 -fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.43 -  filter_theorems ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit
    1.44 +fun filter_theorems_cmd ctxt theorems opt_goal opt_limit rem_dups raw_criteria =
    1.45 +  filter_theorems ctxt theorems opt_goal opt_limit rem_dups
    1.46 +    (map (apsnd (read_criterion ctxt)) raw_criteria);
    1.47 +
    1.48 +fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.49 +  filter ctxt (map Internal (all_facts_of ctxt)) opt_goal opt_limit
    1.50       rem_dups raw_criteria
    1.51    |> apsnd (map (fn Internal f => f));
    1.52  
    1.53 +val find_theorems = gen_find_theorems filter_theorems;
    1.54 +val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
    1.55 +
    1.56  fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
    1.57        [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    1.58          Display.pretty_thm ctxt thm]
    1.59 @@ -471,7 +485,7 @@
    1.60  
    1.61      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.62      val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
    1.63 -      opt_goal opt_limit rem_dups raw_criteria;
    1.64 +      opt_goal opt_limit rem_dups criteria;
    1.65      val returned = length theorems;
    1.66  
    1.67      val tally_msg =