# HG changeset patch
# User wenzelm
# Date 1330370637 -3600
# Node ID b09afce1e54ffad39282a172ca446fb8156fd339
# Parent  c45a4427db391f6ed4f5d4971e897c8970bc0350
removed broken/unused introiff (cf. d452117ba564);

diff -r c45a4427db39 -r b09afce1e54f src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 19:54:50 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 20:23:57 2012 +0100
@@ -7,8 +7,7 @@
 signature FIND_THEOREMS =
 sig
   datatype 'term criterion =
-    Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
-    Pattern of 'term
+    Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
 
   datatype theorem =
     Internal of Facts.ref * thm | External of Facts.ref * term
@@ -52,8 +51,7 @@
 (** search criteria **)
 
 datatype 'term criterion =
-  Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
-  Pattern of 'term;
+  Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term;
 
 fun apply_dummies tm =
   let
@@ -76,7 +74,6 @@
 
 fun read_criterion _ (Name name) = Name name
   | read_criterion _ Intro = Intro
-  | read_criterion _ IntroIff = IntroIff
   | read_criterion _ Elim = Elim
   | read_criterion _ Dest = Dest
   | read_criterion _ Solves = Solves
@@ -90,7 +87,6 @@
     (case c of
       Name name => Pretty.str (prfx "name: " ^ quote name)
     | Intro => Pretty.str (prfx "intro")
-    | IntroIff => Pretty.str (prfx "introiff")
     | Elim => Pretty.str (prfx "elim")
     | Dest => Pretty.str (prfx "dest")
     | Solves => Pretty.str (prfx "solves")
@@ -116,7 +112,6 @@
 
 fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
   | xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
-  | xml_of_criterion IntroIff = XML.Elem (("IntroIff", []) , [])
   | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
   | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
   | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
@@ -125,7 +120,6 @@
 
 fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
   | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
-  | criterion_of_xml (XML.Elem (("IntroIff", []) , [])) = IntroIff
   | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
   | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
   | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
@@ -234,32 +228,17 @@
 
 fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
 
-(*educated guesses on HOL*)  (* FIXME utterly broken *)
-val boolT = Type ("bool", []);
-val iff_const = Const ("op =", boolT --> boolT --> boolT);
-
 (*extract terms from term_src, refine them to the parts that concern us,
   if po try match them against obj else vice versa.
   trivial matches are ignored.
   returns: smallest substitution size*)
-fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src =
+fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
     fun matches pat =
-      let
-        val jpat = Object_Logic.drop_judgment thy pat;
-        val c = Term.head_of jpat;
-        val pats =
-          if Term.is_Const c
-          then
-            if doiff andalso c = iff_const then
-              (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
-                |> filter (is_nontrivial thy)
-            else [pat]
-          else [];
-      in filter check_match pats end;
+      is_nontrivial thy pat andalso
+      Pattern.matches thy (if po then (pat, obj) else (obj, pat));
 
     fun substsize pat =
       let val (_, subst) =
@@ -271,8 +250,7 @@
 
     val match_thm = matches o refine_term;
   in
-    maps match_thm (extract_terms term_src)
-    |> map substsize
+    map (substsize o refine_term) (filter match_thm (extract_terms term_src))
     |> bestmatch
   end;
 
@@ -293,7 +271,7 @@
       hd o Logic.strip_imp_prems);
     val prems = Logic.prems_of_goal goal 1;
 
-    fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem;
+    fun try_subst prem = is_matching_thm extract_dest ctxt true prem theorem;
     val successful = prems |> map_filter try_subst;
   in
     (*if possible, keep best substitution (one with smallest size)*)
@@ -303,11 +281,11 @@
     then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
   end;
 
-fun filter_intro doiff ctxt goal theorem =
+fun filter_intro ctxt goal theorem =
   let
     val extract_intro = (single o prop_of, Logic.strip_imp_concl);
     val concl = Logic.concl_of_goal goal 1;
-    val ss = is_matching_thm doiff extract_intro ctxt true concl theorem;
+    val ss = is_matching_thm extract_intro ctxt true concl theorem;
   in
     if is_some ss then SOME (nprems_of theorem, the ss) else NONE
   end;
@@ -323,8 +301,7 @@
       fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2);
       val rule_tree = combine rule_mp rule_concl;
       fun goal_tree prem = combine prem goal_concl;
-      fun try_subst prem =
-        is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree;
+      fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
       val successful = prems |> map_filter try_subst;
     in
       (*elim rules always have assumptions, so an elim with one
@@ -358,7 +335,7 @@
         val mksimps = Simplifier.mksimps (simpset_of ctxt);
         val extract_simp =
           (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
-        val ss = is_matching_thm false extract_simp ctxt false t thm;
+        val ss = is_matching_thm extract_simp ctxt false t thm;
       in
         if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
       end
@@ -403,12 +380,10 @@
 
 fun filter_crit _ _ (Name name) = apfst (filter_name name)
   | filter_crit _ NONE Intro = err_no_goal "intro"
-  | filter_crit _ NONE IntroIff = err_no_goal "introiff"
   | filter_crit _ NONE Elim = err_no_goal "elim"
   | filter_crit _ NONE Dest = err_no_goal "dest"
   | filter_crit _ NONE Solves = err_no_goal "solves"
-  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro false ctxt (fix_goal goal))
-  | filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal))
+  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
   | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
   | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
   | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
@@ -619,7 +594,6 @@
 val criterion =
   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
   Parse.reserved "intro" >> K Intro ||
-  Parse.reserved "introiff" >> K IntroIff ||
   Parse.reserved "elim" >> K Elim ||
   Parse.reserved "dest" >> K Dest ||
   Parse.reserved "solves" >> K Solves ||