# HG changeset patch # User kleing # Date 1122859651 -7200 # Node ID 6a25e42eaff52fc8bc7824b5c30f3bf3aeb57b79 # Parent 32626fb8ae495a09d06841805d75992bfd52c567 Ordering is now: first by number of assumptions, second by the substitution size. Treat elim/dest rules like erule/drule would: * "elim" is now a subset of "dest" and matches on conclusion of goal and major premise against any premise of goal. Computed substitution size takes both into account. * "dest" no longer has a restriction that limits its conclusion to a var. (contributed by Raf) diff -r 32626fb8ae49 -r 6a25e42eaff5 src/Pure/Isar/find_theorems.ML --- a/src/Pure/Isar/find_theorems.ML Sat Jul 30 16:50:55 2005 +0200 +++ b/src/Pure/Isar/find_theorems.ML Mon Aug 01 03:27:31 2005 +0200 @@ -78,16 +78,20 @@ (* matching theorems *) + +fun is_nontrivial sg = is_Const o head_of o ObjectLogic.drop_judgment sg; -fun is_matching_thm (extract_thms, extract_term) ctxt po obj thm = +(*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 (extract_terms, refine_term) ctxt po obj term_src = let val sg = ProofContext.sign_of ctxt; val tsig = Sign.tsig_of sg; - val is_nontrivial = is_Const o head_of o ObjectLogic.drop_judgment sg; - fun matches pat = - is_nontrivial pat andalso + is_nontrivial sg pat andalso Pattern.matches tsig (if po then (pat,obj) else (obj,pat)); fun substsize pat = @@ -97,12 +101,12 @@ end; fun bestmatch [] = NONE - | bestmatch (x :: xs) = SOME (nprems_of thm, foldl Int.min x xs); + | bestmatch (x :: xs) = SOME (foldl Int.min x xs); - val match_thm = matches o extract_term o Thm.prop_of; + val match_thm = matches o refine_term; in - map (substsize o extract_term o Thm.prop_of) - (List.filter match_thm (extract_thms thm)) |> bestmatch + map (substsize o refine_term) + (List.filter match_thm (extract_terms term_src)) |> bestmatch end; @@ -123,57 +127,61 @@ (* filter intro/elim/dest rules *) -local - -(*elimination rule: conclusion is a Var which does not appear in the major premise*) -fun is_elim ctxt thm = +fun filter_dest ctxt goal (_,thm) = let - val sg = ProofContext.sign_of ctxt; - val prop = Thm.prop_of thm; - val concl = ObjectLogic.drop_judgment sg (Logic.strip_imp_concl prop); - val major_prem = Library.take (1, Logic.strip_imp_prems prop); - val prem_vars = Drule.vars_of_terms major_prem; - in - not (null major_prem) andalso - Term.is_Var concl andalso - not (Term.dest_Var concl mem prem_vars) - end; - -fun filter_elim_dest check_thm ctxt goal (_,thm) = - let - val extract_elim = - (fn thm => if Thm.no_prems thm then [] else [thm], + val extract_dest = + (fn thm => if Thm.no_prems thm then [] else [prop_of thm], hd o Logic.strip_imp_prems); val prems = Logic.prems_of_goal goal 1; - fun try_subst prem = is_matching_thm extract_elim ctxt true prem thm; + fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm; (*keep successful substitutions*) val ss = prems |> List.map try_subst |> List.filter isSome - |> List.map (#2 o valOf); + |> List.map valOf; in (*if possible, keep best substitution (one with smallest size)*) - (*elim and dest rules always have assumptions, so an elim with one + (*dest rules always have assumptions, so a dest with one assumption is as good as an intro rule with none*) - if check_thm ctxt thm andalso not (null ss) + if not (null ss) then SOME (nprems_of thm - 1, foldl Int.min (hd ss) (tl ss)) else NONE end; -in - fun filter_intro ctxt goal (_,thm) = let - val extract_intro = (single, Logic.strip_imp_concl); + val extract_intro = (single o prop_of, Logic.strip_imp_concl); val concl = Logic.concl_of_goal goal 1; + val ss = is_matching_thm extract_intro ctxt true concl thm; in - is_matching_thm extract_intro ctxt true concl thm + if is_some ss then SOME (nprems_of thm, valOf ss) else NONE end; -fun filter_elim ctxt = filter_elim_dest is_elim ctxt; -fun filter_dest ctxt = filter_elim_dest (not oo is_elim) ctxt; - -end; +fun filter_elim ctxt goal (_,thm) = + if not (Thm.no_prems thm) then + let + val rule = prop_of thm; + val prems = Logic.prems_of_goal goal 1; + val goal_concl = Logic.concl_of_goal goal 1; + val rule_mp = (hd o Logic.strip_imp_prems) rule; + val rule_concl = Logic.strip_imp_concl rule; + 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 (single, I) ctxt true (goal_tree prem) rule_tree; + (*keep successful substitutions*) + val ss = prems |> List.map try_subst + |> List.filter isSome + |> List.map valOf; + in + (*elim rules always have assumptions, so an elim with one + assumption is as good as an intro rule with none*) + if is_nontrivial (ProofContext.sign_of ctxt) (Thm.major_prem_of thm) + andalso not (null ss) + then SOME (nprems_of thm - 1, foldl Int.min (hd ss) (tl ss)) else NONE + end + else NONE (* filter_simp *) @@ -182,8 +190,12 @@ let val (_, {mk_rews = {mk, ...}, ...}) = MetaSimplifier.rep_ss (Simplifier.local_simpset_of ctxt); - val extract_simp = (mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); - in is_matching_thm extract_simp ctxt false t thm end; + val extract_simp = + ((List.map prop_of) o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); + val ss = is_matching_thm extract_simp ctxt false t thm + in + if is_some ss then SOME (nprems_of thm, valOf ss) else NONE + end; (* filter_pattern *) @@ -226,11 +238,10 @@ map (fn f => f thm) filters |> List.foldl opt_add (SOME (0,0)); (*filters return: (number of assumptions, substitution size) option, so - sort (desc. in both cases) according to whether a theorem has assumptions, + sort (desc. in both cases) according to number of assumptions first, then by the substitution size*) fun thm_ord (((p0,s0),_),((p1,s1),_)) = - prod_ord (int_ord o pairself (fn 0 => 0 | x => 1)) - int_ord ((p1,s1),(p0,s0)); + prod_ord int_ord int_ord ((p1,s1),(p0,s0)); val processed = List.map (fn t => (eval_filters filters t, t)) thms; val filtered = List.filter (isSome o #1) processed;