# HG changeset patch # User wenzelm # Date 1393088851 -3600 # Node ID aeca05e62fef3f0adcae33d67cd636692f339868 # Parent 95454b2980ee4053813a5a3937da62f309bdc448 removed remains of old experiment (see b933142e02d0); diff -r 95454b2980ee -r aeca05e62fef src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sat Feb 22 17:13:30 2014 +0100 +++ b/src/Pure/Tools/find_theorems.ML Sat Feb 22 18:07:31 2014 +0100 @@ -89,35 +89,10 @@ {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria}; - -(** theorems, either internal or external (without proof) **) - -datatype theorem = - Internal of Facts.ref * thm | - External of Facts.ref * term; (* FIXME: Facts.ref not appropriate *) - -fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm - | prop_of (External (_, prop)) = prop; - -fun nprems_of (Internal (_, thm)) = Thm.nprems_of thm - | nprems_of (External (_, prop)) = Logic.count_prems prop; - -fun size_of (Internal (_, thm)) = size_of_term (Thm.prop_of thm) - | size_of (External (_, prop)) = size_of_term prop; - -fun major_prem_of (Internal (_, thm)) = Thm.major_prem_of thm - | major_prem_of (External (_, prop)) = - Logic.strip_assums_concl (hd (Logic.strip_imp_prems prop)); - -fun fact_ref_of (Internal (fact_ref, _)) = fact_ref - | fact_ref_of (External (fact_ref, _)) = fact_ref; - - - (** search criterion filters **) (*generated filters are to be of the form - input: theorem + input: (Facts.ref * thm) output: (p:int, s:int, t:int) option, where NONE indicates no match p is the primary sorting criterion @@ -164,43 +139,45 @@ (* filter_name *) -fun filter_name str_pat theorem = - if match_string str_pat (Facts.name_of_ref (fact_ref_of theorem)) +fun filter_name str_pat (thmref, _) = + if match_string str_pat (Facts.name_of_ref thmref) then SOME (0, 0, 0) else NONE; (* filter intro/elim/dest/solves rules *) -fun filter_dest ctxt goal theorem = +fun filter_dest ctxt goal (_, thm) = let val extract_dest = - (fn theorem => if nprems_of theorem = 0 then [] else [prop_of theorem], + (fn thm => if Thm.no_prems thm then [] else [Thm.full_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_dest ctxt true prem theorem; + fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm; val successful = prems |> map_filter try_subst; in (*if possible, keep best substitution (one with smallest size)*) (*dest rules always have assumptions, so a dest with one assumption is as good as an intro rule with none*) - if not (null successful) - then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE + if not (null successful) then + SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful) + else NONE end; -fun filter_intro ctxt goal theorem = +fun filter_intro ctxt goal (_, thm) = let - val extract_intro = (single o prop_of, Logic.strip_imp_concl); + val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); val concl = Logic.concl_of_goal goal 1; - val ss = is_matching_thm extract_intro ctxt true concl theorem; in - if is_some ss then SOME (size_of theorem, nprems_of theorem, the ss) else NONE + (case is_matching_thm extract_intro ctxt true concl thm of + SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss) + | NONE => NONE) end; -fun filter_elim ctxt goal theorem = - if nprems_of theorem > 0 then +fun filter_elim ctxt goal (_, thm) = + if Thm.nprems_of thm > 0 then let - val rule = prop_of theorem; + val rule = Thm.full_prop_of thm; val prems = Logic.prems_of_goal goal 1; val goal_concl = Logic.concl_of_goal goal 1; val rule_mp = hd (Logic.strip_imp_prems rule); @@ -213,9 +190,10 @@ in (*elim rules always have assumptions, so an elim with one assumption is as good as an intro rule with none*) - if is_nontrivial (Proof_Context.theory_of ctxt) (major_prem_of theorem) - andalso not (null successful) - then SOME (size_of theorem, nprems_of theorem - 1, foldl1 Int.min successful) else NONE + if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm) + andalso not (null successful) then + SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful) + else NONE end else NONE; @@ -235,27 +213,25 @@ (limited_etac thm THEN_ALL_NEW (Goal.norm_hhf_tac ctxt' THEN' Method.assm_tac ctxt')) 1 goal'; in - fn Internal (_, thm) => - if is_some (Seq.pull (try_thm thm)) - then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE - | External _ => NONE + fn (_, thm) => + if is_some (Seq.pull (try_thm thm)) + then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) + else NONE end; (* filter_simp *) -fun filter_simp ctxt t (Internal (_, thm)) = - let - val mksimps = Simplifier.mksimps 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 extract_simp ctxt false t thm; - in - if is_some ss - then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, the ss) - else NONE - end - | filter_simp _ _ (External _) = NONE; +fun filter_simp ctxt t (_, thm) = + let + val mksimps = Simplifier.mksimps ctxt; + val extract_simp = + (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); + in + (case is_matching_thm extract_simp ctxt false t thm of + SOME ss => SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, ss) + | NONE => NONE) + end; (* filter_pattern *) @@ -274,11 +250,11 @@ let val pat_consts = get_names pat; - fun check (theorem, NONE) = check (theorem, SOME (get_names (prop_of theorem))) - | check (theorem, c as SOME thm_consts) = + fun check ((x, thm), NONE) = check ((x, thm), SOME (get_names (Thm.full_prop_of thm))) + | check ((_, thm), c as SOME thm_consts) = (if subset (op =) (pat_consts, thm_consts) andalso - Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, prop_of theorem) - then SOME (size_of theorem, nprems_of theorem, 0) else NONE, c); + Pattern.matches_subterm (Proof_Context.theory_of ctxt) (pat, Thm.full_prop_of thm) + then SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm, 0) else NONE, c); in check end; @@ -320,18 +296,18 @@ fun filter_criterion ctxt opt_goal (b, c) = (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c; -fun sorted_filter filters theorems = +fun sorted_filter filters thms = let - fun eval_filters theorem = app_filters theorem (SOME (0, 0, 0), NONE, filters); + fun eval_filters thm = app_filters thm (SOME (0, 0, 0), NONE, filters); (*filters return: (thm size, number of assumptions, substitution size) option, so sort according to size of thm first, then number of assumptions, then by the substitution size, then by term order *) - fun result_ord (((p0, s0, t0), thm0), ((p1, s1, t1), thm1)) = - prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord)) - ((p1, (s1, (t1, prop_of thm1))), (p0, (s0, (t0, prop_of thm0)))); + fun result_ord (((p0, s0, t0), (_, thm0)), ((p1, s1, t1), (_, thm1))) = + prod_ord int_ord (prod_ord int_ord (prod_ord int_ord Term_Ord.term_ord)) + ((p1, (s1, (t1, Thm.full_prop_of thm1))), (p0, (s0, (t0, Thm.full_prop_of thm0)))); in - grouped 100 Par_List.map eval_filters theorems + grouped 100 Par_List.map eval_filters thms |> map_filter I |> sort result_ord |> map #2 end; @@ -368,10 +344,10 @@ let fun rem_c rev_seen [] = rev rev_seen | rem_c rev_seen [x] = rem_c (x :: rev_seen) [] - | rem_c rev_seen ((x as (t, _)) :: (y as (t', _)) :: xs) = - if prop_of t aconv prop_of t' - then rem_c rev_seen ((if nicer (fact_ref_of t) (fact_ref_of t') then x else y) :: xs) - else rem_c (x :: rev_seen) (y :: xs); + | rem_c rev_seen ((x as ((n, thm), _)) :: (y as ((n', thm'), _)) :: rest) = + if Thm.eq_thm_prop (thm, thm') + then rem_c rev_seen ((if nicer n n' then x else y) :: rest) + else rem_c (x :: rev_seen) (y :: rest); in rem_c [] xs end; in @@ -396,7 +372,7 @@ fun rem_thm_dups nicer xs = (xs ~~ (1 upto length xs)) - |> sort (Term_Ord.fast_term_ord o pairself (prop_of o #1)) + |> sort (Term_Ord.fast_term_ord o pairself (Thm.full_prop_of o #2 o #1)) |> rem_cdups nicer |> sort (int_ord o pairself #2) |> map #1; @@ -461,9 +437,8 @@ val add_prems = Seq.hd o TRY (Method.insert_tac assms 1); val opt_goal' = Option.map add_prems opt_goal; in - filter ctxt (map Internal (all_facts_of ctxt)) + filter ctxt (all_facts_of ctxt) {goal = opt_goal', limit = opt_limit, rem_dups = rem_dups, criteria = raw_criteria} - |> apsnd (map (fn Internal f => f)) end; in @@ -489,14 +464,10 @@ Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1] end; -fun pretty_theorem ctxt (Internal (thmref, thm)) = - Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]) - | pretty_theorem ctxt (External (thmref, prop)) = - Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]); - in -fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm)); +fun pretty_thm ctxt (thmref, thm) = + Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]); fun pretty_theorems state opt_limit rem_dups raw_criteria = let @@ -505,7 +476,7 @@ val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; val (opt_found, theorems) = - filter_theorems ctxt (map Internal (all_facts_of ctxt)) + filter_theorems ctxt (all_facts_of ctxt) {goal = opt_goal, limit = opt_limit, rem_dups = rem_dups, criteria = criteria}; val returned = length theorems; @@ -523,7 +494,7 @@ (if null theorems then [Pretty.str "nothing found"] else [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ - grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) (rev theorems)) + grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems)) end |> Pretty.fbreaks |> curry Pretty.blk 0; end;