# HG changeset patch # User wenzelm # Date 1205600883 -3600 # Node ID e19a5a7e83f1f64088f0ad3ee4abff8434648f40 # Parent 305d5ca4fa9ddf711ad690b35b02b39f8cd9bea4 more precise Author line; replaced obsolete FactIndex.T by Facts.T; simplified ML; diff -r 305d5ca4fa9d -r e19a5a7e83f1 src/Pure/Isar/find_theorems.ML --- a/src/Pure/Isar/find_theorems.ML Sat Mar 15 18:08:02 2008 +0100 +++ b/src/Pure/Isar/find_theorems.ML Sat Mar 15 18:08:03 2008 +0100 @@ -1,6 +1,6 @@ (* Title: Pure/Isar/find_theorems.ML ID: $Id$ - Author: Rafal Kolanski, NICTA and Tobias Nipkow, TU Muenchen + Author: Rafal Kolanski and Gerwin Klein, NICTA Retrieve theorems from proof context. *) @@ -89,8 +89,8 @@ val match_thm = matches o refine_term; in - map (substsize o refine_term) - (filter match_thm (extract_terms term_src)) |> bestmatch + map (substsize o refine_term) (filter match_thm (extract_terms term_src)) + |> bestmatch end; @@ -145,11 +145,11 @@ 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 o Logic.strip_imp_prems) rule; + val rule_mp = hd (Logic.strip_imp_prems rule); val rule_concl = Logic.strip_imp_concl rule; - fun combine t1 t2 = Const ("combine", dummyT --> dummyT) $ (t1 $ t2); + 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 goal_tree prem = combine prem goal_concl; fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree; val successful = prems |> map_filter try_subst; @@ -204,7 +204,7 @@ fun opt_not x = if is_some x then NONE else SOME (0, 0); fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) - | opt_add _ _ = NONE; + | opt_add _ _ = NONE; in @@ -213,7 +213,7 @@ fun all_filters filters thms = let - fun eval_filters filters thm = + fun eval_filters thm = fold opt_add (map (fn f => f thm) filters) (SOME (0, 0)); (*filters return: (number of assumptions, substitution size) option, so @@ -222,7 +222,7 @@ fun thm_ord (((p0, s0), _), ((p1, s1), _)) = prod_ord int_ord int_ord ((p1, s1), (p0, s0)); in - map (`(eval_filters filters)) thms + map (`eval_filters) thms |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE) |> sort thm_ord |> map #2 end; @@ -259,32 +259,28 @@ fun rem_cdups xs = 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 ((n,t),_))::(y as ((n',t'),_))::xs) = - if Thm.eq_thm_prop (t,t') - then if nicer n n' - then rem_c rev_seen (x::xs) - else rem_c rev_seen (y::xs) - else rem_c (x::rev_seen) (y::xs) + | rem_c rev_seen [x] = rem_c (x :: rev_seen) [] + | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = + if Thm.eq_thm_prop (t, t') + then rem_c rev_seen ((if nicer n n' then x else y) :: xs) + else rem_c (x :: rev_seen) (y :: xs) in rem_c [] xs end; - in ListPair.zip (xs, 1 upto length xs) - |> sort (Term.fast_term_ord o pairself (prop_of o #2 o #1)) - |> rem_cdups - |> sort (int_ord o pairself #2) - |> map #1 + in + xs ~~ (1 upto length xs) + |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1)) + |> rem_cdups + |> sort (int_ord o pairself #2) + |> map #1 end; (* print_theorems *) -fun find_thms ctxt spec = - (PureThy.thms_containing (ProofContext.theory_of ctxt) spec - |> maps PureThy.selections) @ - (ProofContext.lthms_containing ctxt spec - |> maps PureThy.selections - |> distinct (fn ((r1, th1), (r2, th2)) => - r1 = r2 andalso Thm.eq_thm_prop (th1, th2))); +fun all_facts_of ctxt = + maps PureThy.selections + (Facts.dest (PureThy.all_facts_of (ProofContext.theory_of ctxt)) @ + Facts.dest (ProofContext.facts_of ctxt)); val limit = ref 40; @@ -293,7 +289,7 @@ val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; val filters = map (filter_criterion ctxt opt_goal) criteria; - val raw_matches = all_filters filters (find_thms ctxt ([], [])); + val raw_matches = all_filters filters (all_facts_of ctxt); val matches = if rem_dups then rem_thm_dups raw_matches