src/Pure/Tools/find_theorems.ML
changeset 46717 b09afce1e54f
parent 46716 c45a4427db39
child 46718 dfaf51de90ad
     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 ||