# HG changeset patch # User kleing # Date 1114766561 -7200 # Node ID a191d2bee3e113bda7a2806fe9258e6fe88b93db # Parent dcce462301315d5f4182866297531d7c1ca9643e new thms_containing that searches for patterns instead of constants (by Rafal Kolanski, NICTA) diff -r dcce46230131 -r a191d2bee3e1 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Apr 29 08:05:06 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Apr 29 11:22:41 2005 +0200 @@ -1463,38 +1463,52 @@ | SOME ths' => Library.equal_lists Thm.eq_thm (ths, ths')); in gen_distinct eq_fst (List.filter valid (FactIndex.find idx index)) end; +(* facts which are local to the current context, with their names + examples are "prems" and "x" in "assumes x:" during a proof *) +fun local_facts (ctxt as Context {thms = (_, _, _, index), ...}) = + (* things like "prems" can occur twice under some circumstances *) + gen_distinct eq_fst (FactIndex.find ([],[]) index); fun print_thms_containing ctxt opt_limit ss = let val prt_term = pretty_term ctxt; val prt_fact = pretty_fact ctxt; - fun prt_consts [] = [] - | prt_consts cs = [Pretty.block (Pretty.breaks (Pretty.str "constants" :: - map (Pretty.quote o prt_term o Syntax.const) cs))]; - fun prt_frees [] = [] - | prt_frees xs = [Pretty.block (Pretty.breaks (Pretty.str "variables" :: - map (Pretty.quote o prt_term o Syntax.free) xs))]; + + (* theorems from the theory and its ancestors *) + val thy = theory_of ctxt; + val sg1 = Theory.sign_of thy; + val all_thys = thy :: (Theory.ancestors_of thy) + val thms1 = List.concat (map PureThy.thms_with_names_of all_thys); + val facts1 = + PureThy.find_theorems sg1 thms1 ss; - val (cs, xs) = Library.foldl (FactIndex.index_term (is_known ctxt)) - (([], []), map (read_term_dummies ctxt) ss); - val empty_idx = null cs andalso null xs; - - val header = - if empty_idx then [Pretty.block [Pretty.str "Known facts:", Pretty.fbrk]] - else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" :: - separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @ - [Pretty.str ":", Pretty.fbrk])] - val facts = - PureThy.thms_containing (theory_of ctxt) (cs, xs) @ lthms_containing ctxt (cs, xs) - |> sort_wrt #1; + (* theorems from the local context *) + val sg2 = sign_of ctxt; + val thms2 = local_facts ctxt; + val facts2 = + PureThy.find_theorems sg2 thms2 ss; + + (* combine them, use a limit, then print *) + val facts = facts1 @ facts2; val len = length facts; val limit = getOpt (opt_limit, ! thms_containing_limit); + val count = Int.min (limit, len); + + val header = Pretty.blk (0, [Pretty.str "Searched for:", Pretty.fbrk, + Pretty.indent 4 ( + Pretty.blk (0, separate Pretty.fbrk (map Pretty.str ss))), + Pretty.fbrk, Pretty.fbrk, + Pretty.str ("Found " ^ (Int.toString len) ^ + " theorems (" ^ (Int.toString count) ^ " displayed):"), + Pretty.fbrk]); in - if empty_idx andalso not (null ss) then - warning "thms_containing: no consts/frees in specification" - else (header @ (if len <= limit then [] else [Pretty.str "..."]) @ - map prt_fact (Library.drop (len - limit, facts))) |> Pretty.chunks |> Pretty.writeln + if null facts then + warning "find_theorems: nothing found" + else + Pretty.writeln header; + ((if len <= limit then [] else [Pretty.str "..."]) @ + map (prt_fact) (Library.drop (len - limit, facts))) |> + Pretty.chunks |> Pretty.writeln end; - end; diff -r dcce46230131 -r a191d2bee3e1 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Apr 29 08:05:06 2005 +0200 +++ b/src/Pure/pure_thy.ML Fri Apr 29 11:22:41 2005 +0200 @@ -14,6 +14,7 @@ val get_thms: theory -> thmref -> thm list val get_thmss: theory -> thmref list -> thm list val thms_of: theory -> (string * thm) list + val thms_with_names_of: theory -> (string * thm list) list structure ProtoPure: sig val thy: theory @@ -31,6 +32,7 @@ val select_thm: thmref -> thm list -> thm list val cond_extern_thm_sg: Sign.sg -> string -> xstring val thms_containing: theory -> string list * string list -> (string * thm list) list + val find_theorems: Sign.sg -> (string * thm list) list -> string list -> (string * thm list) list val thms_containing_consts: theory -> string list -> (string * thm) list val find_matching_thms: (thm -> thm list) * (term -> term) -> theory -> term -> (string * thm) list @@ -226,6 +228,10 @@ map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest thms_tab))) end; +(* thms_with_names_of - theorems in this theory and their names *) +fun thms_with_names_of thy = + TheoremsData.get thy |> ! |> #index |> FactIndex.find ([],[]); + (* looking for nothing in a FactIndex finds everything, i.e. all theorems *) (* thms_containing *) @@ -245,6 +251,49 @@ thms_containing thy (consts, []) |> map #2 |> List.concat |> map (fn th => (Thm.name_of_thm th, th)) +(* find_theorems - finding theorems by matching on a series of subterms *) + +(* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into + a term with all free variables made schematic *) +fun str_pattern_to_term sg str_pattern = + let + (* pattern as term with dummies as Consts *) + val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) + |> Thm.term_of; + (* with dummies as Vars *) + val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern)); + in + (* with schematic vars *) + #1 (Type.varify (v_pattern, [])) + end; + +(* find all thms such that for each returned thm, all given + propositions are subterms of it *) +fun thms_matching_patterns tsign (pat::pats) thms = + let + fun match_single pattern thm = + Pattern.matches_subterm tsign (pat, Thm.prop_of thm); + in + thms_matching_patterns tsign pats + (List.filter (match_single pat) thms) + end + | thms_matching_patterns _ _ thms = thms; + +(* facts are pairs of theorem name and a list of its thms *) +fun find_theorems sg facts str_patterns = + let + val typesg = Sign.tsig_of sg; + + (* the patterns we will be looking for *) + val patterns = map (str_pattern_to_term sg) str_patterns; + + (* we are interested in theorems which have one or more thms for which + all patterns are subterms *) + fun matches (_, thms) = + (not o null o (thms_matching_patterns typesg patterns)) thms + in + List.filter matches facts + end; (* intro/elim theorems *)