author wenzelm Mon Feb 27 20:23:57 2012 +0100 (2012-02-27) changeset 46717 b09afce1e54f parent 46716 c45a4427db39 child 46718 dfaf51de90ad
removed broken/unused introiff (cf. d452117ba564);
```     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 19:54:50 2012 +0100
1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 20:23:57 2012 +0100
1.3 @@ -7,8 +7,7 @@
1.4  signature FIND_THEOREMS =
1.5  sig
1.6    datatype 'term criterion =
1.7 -    Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
1.8 -    Pattern of 'term
1.9 +    Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term
1.10
1.11    datatype theorem =
1.12      Internal of Facts.ref * thm | External of Facts.ref * term
1.13 @@ -52,8 +51,7 @@
1.14  (** search criteria **)
1.15
1.16  datatype 'term criterion =
1.17 -  Name of string | Intro | IntroIff | Elim | Dest | Solves | Simp of 'term |
1.18 -  Pattern of 'term;
1.19 +  Name of string | Intro | Elim | Dest | Solves | Simp of 'term | Pattern of 'term;
1.20
1.21  fun apply_dummies tm =
1.22    let
1.23 @@ -76,7 +74,6 @@
1.24
1.25  fun read_criterion _ (Name name) = Name name
1.26    | read_criterion _ Intro = Intro
1.27 -  | read_criterion _ IntroIff = IntroIff
1.28    | read_criterion _ Elim = Elim
1.29    | read_criterion _ Dest = Dest
1.30    | read_criterion _ Solves = Solves
1.31 @@ -90,7 +87,6 @@
1.32      (case c of
1.33        Name name => Pretty.str (prfx "name: " ^ quote name)
1.34      | Intro => Pretty.str (prfx "intro")
1.35 -    | IntroIff => Pretty.str (prfx "introiff")
1.36      | Elim => Pretty.str (prfx "elim")
1.37      | Dest => Pretty.str (prfx "dest")
1.38      | Solves => Pretty.str (prfx "solves")
1.39 @@ -116,7 +112,6 @@
1.40
1.41  fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
1.42    | xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
1.43 -  | xml_of_criterion IntroIff = XML.Elem (("IntroIff", []) , [])
1.44    | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
1.45    | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
1.46    | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
1.47 @@ -125,7 +120,6 @@
1.48
1.49  fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
1.50    | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
1.51 -  | criterion_of_xml (XML.Elem (("IntroIff", []) , [])) = IntroIff
1.52    | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
1.53    | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
1.54    | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
1.55 @@ -234,32 +228,17 @@
1.56
1.57  fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
1.58
1.59 -(*educated guesses on HOL*)  (* FIXME utterly broken *)
1.60 -val boolT = Type ("bool", []);
1.61 -val iff_const = Const ("op =", boolT --> boolT --> boolT);
1.62 -
1.63  (*extract terms from term_src, refine them to the parts that concern us,
1.64    if po try match them against obj else vice versa.
1.65    trivial matches are ignored.
1.66    returns: smallest substitution size*)
1.67 -fun is_matching_thm doiff (extract_terms, refine_term) ctxt po obj term_src =
1.68 +fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src =
1.69    let
1.70      val thy = Proof_Context.theory_of ctxt;
1.71
1.72 -    fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
1.73      fun matches pat =
1.74 -      let
1.75 -        val jpat = Object_Logic.drop_judgment thy pat;
1.76 -        val c = Term.head_of jpat;
1.77 -        val pats =
1.78 -          if Term.is_Const c
1.79 -          then
1.80 -            if doiff andalso c = iff_const then
1.81 -              (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
1.82 -                |> filter (is_nontrivial thy)
1.83 -            else [pat]
1.84 -          else [];
1.85 -      in filter check_match pats end;
1.86 +      is_nontrivial thy pat andalso
1.87 +      Pattern.matches thy (if po then (pat, obj) else (obj, pat));
1.88
1.89      fun substsize pat =
1.90        let val (_, subst) =
1.91 @@ -271,8 +250,7 @@
1.92
1.93      val match_thm = matches o refine_term;
1.94    in
1.95 -    maps match_thm (extract_terms term_src)
1.96 -    |> map substsize
1.97 +    map (substsize o refine_term) (filter match_thm (extract_terms term_src))
1.98      |> bestmatch
1.99    end;
1.100
1.101 @@ -293,7 +271,7 @@
1.102        hd o Logic.strip_imp_prems);
1.103      val prems = Logic.prems_of_goal goal 1;
1.104
1.105 -    fun try_subst prem = is_matching_thm false extract_dest ctxt true prem theorem;
1.106 +    fun try_subst prem = is_matching_thm extract_dest ctxt true prem theorem;
1.107      val successful = prems |> map_filter try_subst;
1.108    in
1.109      (*if possible, keep best substitution (one with smallest size)*)
1.110 @@ -303,11 +281,11 @@
1.111      then SOME (nprems_of theorem - 1, foldl1 Int.min successful) else NONE
1.112    end;
1.113
1.114 -fun filter_intro doiff ctxt goal theorem =
1.115 +fun filter_intro ctxt goal theorem =
1.116    let
1.117      val extract_intro = (single o prop_of, Logic.strip_imp_concl);
1.118      val concl = Logic.concl_of_goal goal 1;
1.119 -    val ss = is_matching_thm doiff extract_intro ctxt true concl theorem;
1.120 +    val ss = is_matching_thm extract_intro ctxt true concl theorem;
1.121    in
1.122      if is_some ss then SOME (nprems_of theorem, the ss) else NONE
1.123    end;
1.124 @@ -323,8 +301,7 @@
1.125        fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) \$ (t1 \$ t2);
1.126        val rule_tree = combine rule_mp rule_concl;
1.127        fun goal_tree prem = combine prem goal_concl;
1.128 -      fun try_subst prem =
1.129 -        is_matching_thm false (single, I) ctxt true (goal_tree prem) rule_tree;
1.130 +      fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
1.131        val successful = prems |> map_filter try_subst;
1.132      in
1.133        (*elim rules always have assumptions, so an elim with one
1.134 @@ -358,7 +335,7 @@
1.135          val mksimps = Simplifier.mksimps (simpset_of ctxt);
1.136          val extract_simp =
1.137            (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
1.138 -        val ss = is_matching_thm false extract_simp ctxt false t thm;
1.139 +        val ss = is_matching_thm extract_simp ctxt false t thm;
1.140        in
1.141          if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
1.142        end
1.143 @@ -403,12 +380,10 @@
1.144
1.145  fun filter_crit _ _ (Name name) = apfst (filter_name name)
1.146    | filter_crit _ NONE Intro = err_no_goal "intro"
1.147 -  | filter_crit _ NONE IntroIff = err_no_goal "introiff"
1.148    | filter_crit _ NONE Elim = err_no_goal "elim"
1.149    | filter_crit _ NONE Dest = err_no_goal "dest"
1.150    | filter_crit _ NONE Solves = err_no_goal "solves"
1.151 -  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro false ctxt (fix_goal goal))
1.152 -  | filter_crit ctxt (SOME goal) IntroIff = apfst (filter_intro true ctxt (fix_goal goal))
1.153 +  | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt (fix_goal goal))
1.154    | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt (fix_goal goal))
1.155    | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt (fix_goal goal))
1.156    | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal)
1.157 @@ -619,7 +594,6 @@
1.158  val criterion =
1.159    Parse.reserved "name" |-- Parse.!!! (Parse.\$\$\$ ":" |-- Parse.xname) >> Name ||
1.160    Parse.reserved "intro" >> K Intro ||
1.161 -  Parse.reserved "introiff" >> K IntroIff ||
1.162    Parse.reserved "elim" >> K Elim ||
1.163    Parse.reserved "dest" >> K Dest ||
1.164    Parse.reserved "solves" >> K Solves ||
```