src/Pure/Tools/find_theorems.ML
changeset 52926 6415d95bf7a2
parent 52925 71e938856a03
child 52927 9c6aef15a7ad
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Aug 08 23:34:52 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Aug 08 23:52:35 2013 +0200
     1.3 @@ -23,11 +23,6 @@
     1.4    val read_criterion: Proof.context -> string criterion -> term criterion
     1.5    val read_query: Position.T -> string -> (bool * string criterion) list
     1.6  
     1.7 -  val xml_of_query: term query -> XML.tree
     1.8 -  val query_of_xml: XML.tree -> term query
     1.9 -  val xml_of_result: int option * theorem list -> XML.tree
    1.10 -  val result_of_xml: XML.tree -> int option * theorem list
    1.11 -
    1.12    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    1.13      (bool * term criterion) list -> int option * (Facts.ref * thm) list
    1.14    val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
    1.15 @@ -40,7 +35,6 @@
    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 @@ -108,46 +102,6 @@
    1.24  fun map_criteria f {goal, limit, rem_dups, criteria} =
    1.25    {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
    1.26  
    1.27 -fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
    1.28 -  | xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
    1.29 -  | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
    1.30 -  | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
    1.31 -  | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
    1.32 -  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat])
    1.33 -  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]);
    1.34 -
    1.35 -fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
    1.36 -  | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
    1.37 -  | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
    1.38 -  | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
    1.39 -  | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
    1.40 -  | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree)
    1.41 -  | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree)
    1.42 -  | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
    1.43 -
    1.44 -fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
    1.45 -      let
    1.46 -        val properties = []
    1.47 -          |> (if rem_dups then cons ("rem_dups", "") else I)
    1.48 -          |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
    1.49 -      in
    1.50 -        XML.Elem (("Query", properties), XML.Encode.list
    1.51 -          (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
    1.52 -      end
    1.53 -  | xml_of_query _ = raise Fail "cannot serialize goal";
    1.54 -
    1.55 -fun query_of_xml (XML.Elem (("Query", properties), body)) =
    1.56 -      let
    1.57 -        val rem_dups = Properties.defined properties "rem_dups";
    1.58 -        val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
    1.59 -        val criteria =
    1.60 -          XML.Decode.list (XML.Decode.pair XML.Decode.bool
    1.61 -            (criterion_of_xml o the_single)) body;
    1.62 -      in
    1.63 -        {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
    1.64 -      end
    1.65 -  | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree);
    1.66 -
    1.67  
    1.68  
    1.69  (** theorems, either internal or external (without proof) **)
    1.70 @@ -162,35 +116,6 @@
    1.71        Position.markup pos o Markup.properties [("name", name)]
    1.72    | fact_ref_markup fact_ref = raise Fail "bad fact ref";
    1.73  
    1.74 -fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
    1.75 -  | xml_of_theorem (External (fact_ref, prop)) =
    1.76 -      XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]);
    1.77 -
    1.78 -fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
    1.79 -      let
    1.80 -        val name = the (Properties.get properties "name");
    1.81 -        val pos = Position.of_properties properties;
    1.82 -        val intvs_opt =
    1.83 -          Option.map (single o Facts.Single o Markup.parse_int)
    1.84 -            (Properties.get properties "index");
    1.85 -      in
    1.86 -        External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree)
    1.87 -      end
    1.88 -  | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
    1.89 -
    1.90 -fun xml_of_result (opt_found, theorems) =
    1.91 -  let
    1.92 -    val properties =
    1.93 -      if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
    1.94 -  in
    1.95 -    XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
    1.96 -  end;
    1.97 -
    1.98 -fun result_of_xml (XML.Elem (("Result", properties), body)) =
    1.99 -      (Properties.get properties "found" |> Option.map Markup.parse_int,
   1.100 -       XML.Decode.list (theorem_of_xml o the_single) body)
   1.101 -  | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree);
   1.102 -
   1.103  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
   1.104    | prop_of (External (_, prop)) = prop;
   1.105