--- 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 ||