src/Pure/Tools/find_theorems.ML
changeset 46718 dfaf51de90ad
parent 46717 b09afce1e54f
child 46961 5c6955f487e5
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 20:23:57 2012 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 20:33:18 2012 +0100
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      Pure/Tools/find_theorems.ML
     1.5      Author:     Rafal Kolanski and Gerwin Klein, NICTA
     1.6 +    Author:     Lars Noschinski and Alexander Krauss, TU Muenchen
     1.7  
     1.8  Retrieve theorems from proof context.
     1.9  *)
    1.10 @@ -108,7 +109,7 @@
    1.11  };
    1.12  
    1.13  fun map_criteria f {goal, limit, rem_dups, criteria} =
    1.14 -  {goal=goal, limit=limit, rem_dups=rem_dups, criteria=f criteria};
    1.15 +  {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
    1.16  
    1.17  fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
    1.18    | xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
    1.19 @@ -127,7 +128,7 @@
    1.20    | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
    1.21    | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
    1.22  
    1.23 -fun xml_of_query {goal=NONE, limit, rem_dups, criteria} =
    1.24 +fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
    1.25        let
    1.26          val properties = []
    1.27            |> (if rem_dups then cons ("rem_dups", "") else I)
    1.28 @@ -146,7 +147,7 @@
    1.29            XML.Decode.list (XML.Decode.pair XML.Decode.bool
    1.30              (criterion_of_xml o the_single)) body;
    1.31        in
    1.32 -        {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
    1.33 +        {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
    1.34        end
    1.35    | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
    1.36  
    1.37 @@ -172,8 +173,9 @@
    1.38        let
    1.39          val name = the (Properties.get properties "name");
    1.40          val pos = Position.of_properties properties;
    1.41 -        val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
    1.42 -          (Properties.get properties "index");
    1.43 +        val intvs_opt =
    1.44 +          Option.map (single o Facts.Single o Markup.parse_int)
    1.45 +            (Properties.get properties "index");
    1.46        in
    1.47          External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
    1.48        end
    1.49 @@ -310,7 +312,7 @@
    1.50          andalso not (null successful)
    1.51        then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
    1.52      end
    1.53 -  else NONE
    1.54 +  else NONE;
    1.55  
    1.56  val tac_limit = Unsynchronized.ref 5;
    1.57  
    1.58 @@ -423,7 +425,6 @@
    1.59  fun lazy_filter filters =
    1.60    let
    1.61      fun lazy_match thms = Seq.make (fn () => first_match thms)
    1.62 -
    1.63      and first_match [] = NONE
    1.64        | first_match (thm :: thms) =
    1.65            (case app_filters thm (SOME (0, 0), NONE, filters) of
    1.66 @@ -464,7 +465,7 @@
    1.67  
    1.68  fun nicer_shortest ctxt =
    1.69    let
    1.70 -    (* FIXME global name space!? *)
    1.71 +    (* FIXME Why global name space!?? *)
    1.72      val space = Facts.space_of (Global_Theory.facts_of (Proof_Context.theory_of ctxt));
    1.73  
    1.74      val shorten =
    1.75 @@ -507,7 +508,7 @@
    1.76  
    1.77  fun filter_theorems ctxt theorems query =
    1.78    let
    1.79 -    val {goal=opt_goal, limit=opt_limit, rem_dups, criteria} = query
    1.80 +    val {goal = opt_goal, limit = opt_limit, rem_dups, criteria} = query;
    1.81      val filters = map (filter_criterion ctxt opt_goal) criteria;
    1.82  
    1.83      fun find_all theorems =
    1.84 @@ -530,8 +531,8 @@
    1.85  
    1.86    in find theorems end;
    1.87  
    1.88 -fun filter_theorems_cmd ctxt theorems raw_query = 
    1.89 -  filter_theorems ctxt theorems (map_criteria 
    1.90 +fun filter_theorems_cmd ctxt theorems raw_query =
    1.91 +  filter_theorems ctxt theorems (map_criteria
    1.92      (map (apsnd (read_criterion ctxt))) raw_query);
    1.93  
    1.94  fun gen_find_theorems filter ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.95 @@ -542,8 +543,8 @@
    1.96      val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
    1.97      val opt_goal' = Option.map add_prems opt_goal;
    1.98    in
    1.99 -    filter ctxt (map Internal (all_facts_of ctxt)) 
   1.100 -      {goal=opt_goal', limit=opt_limit, rem_dups=rem_dups, criteria=raw_criteria}
   1.101 +    filter ctxt (map Internal (all_facts_of ctxt))
   1.102 +      {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria}
   1.103      |> apsnd (map (fn Internal f => f))
   1.104    end;
   1.105  
   1.106 @@ -563,7 +564,7 @@
   1.107    let
   1.108      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   1.109      val (foundo, theorems) = find
   1.110 -      {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
   1.111 +      {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria};
   1.112      val returned = length theorems;
   1.113  
   1.114      val tally_msg =
   1.115 @@ -587,6 +588,7 @@
   1.116    gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
   1.117  
   1.118  
   1.119 +
   1.120  (** command syntax **)
   1.121  
   1.122  local