--- a/doc-src/IsarRef/pure.tex Thu Feb 01 20:42:34 2001 +0100
+++ b/doc-src/IsarRef/pure.tex Thu Feb 01 20:43:14 2001 +0100
@@ -1276,7 +1276,7 @@
\railterm{thmdeps}
\begin{rail}
- thmscontaining (name * )
+ thmscontaining (term * )
;
thmdeps thmrefs
;
@@ -1301,9 +1301,10 @@
current theory context. In interactive mode this actually refers to the
theorems left by the last transaction; this allows to inspect the result of
advanced definitional packages, such as $\isarkeyword{datatype}$.
-\item [$\isarkeyword{thms_containing}~\vec c$] retrieves theorems from the
- theory context containing all of the constants $\vec c$. Note that giving
- the empty list yields \emph{all} theorems of the current theory.
+\item [$\isarkeyword{thms_containing}~\vec t$] retrieves theorems from the
+ theory context containing all of the constants occurring in the terms $\vec
+ t$. Note that giving the empty list yields \emph{all} theorems of the
+ current theory.
\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of theorems
and lemmas, using Isabelle's graph browser tool (see also
\cite{isabelle-sys}).
--- a/src/Pure/Interface/proof_general.ML Thu Feb 01 20:42:34 2001 +0100
+++ b/src/Pure/Interface/proof_general.ML Thu Feb 01 20:43:14 2001 +0100
@@ -13,7 +13,7 @@
val try_update_thy_only: string -> unit
val inform_file_processed: string -> unit
val inform_file_retracted: string -> unit
- val thms_containing: xstring list -> unit
+ val thms_containing: string list -> unit
val help: unit -> unit
val show_context: unit -> theory
val kill_goal: unit -> unit
@@ -180,7 +180,11 @@
(* misc commands for ProofGeneral/isa *)
-fun thms_containing cs = ThmDatabase.print_thms_containing (the_context ()) cs;
+fun thms_containing ss =
+ let
+ val thy = the_context ();
+ fun read_term s = Thm.term_of (Thm.read_cterm (Theory.sign_of thy) (s, TypeInfer.logicT));
+ in ThmDatabase.print_thms_containing thy (map read_term ss) end;
val welcome = priority o Session.welcome;
val help = welcome;
--- a/src/Pure/Isar/isar_cmd.ML Thu Feb 01 20:42:34 2001 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Thu Feb 01 20:43:14 2001 +0100
@@ -50,7 +50,7 @@
val print_trans_rules: Toplevel.transition -> Toplevel.transition
val print_methods: Toplevel.transition -> Toplevel.transition
val print_antiquotations: Toplevel.transition -> Toplevel.transition
- val print_thms_containing: xstring list -> Toplevel.transition -> Toplevel.transition
+ val print_thms_containing: string list -> Toplevel.transition -> Toplevel.transition
val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
val print_binds: Toplevel.transition -> Toplevel.transition
val print_lthms: Toplevel.transition -> Toplevel.transition
@@ -195,8 +195,9 @@
val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
-fun print_thms_containing cs = Toplevel.unknown_theory o
- Toplevel.keep (fn state => ThmDatabase.print_thms_containing (Toplevel.theory_of state) cs);
+fun print_thms_containing ss = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+ ThmDatabase.print_thms_containing (Toplevel.theory_of state)
+ (map (ProofContext.read_term (Toplevel.context_of state)) ss));
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
--- a/src/Pure/Isar/isar_syn.ML Thu Feb 01 20:42:34 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Feb 01 20:43:14 2001 +0100
@@ -539,8 +539,8 @@
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
val thms_containingP =
- OuterSyntax.improper_command "thms_containing" "print theorems containing all given constants"
- K.diag (Scan.repeat P.xname >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
+ OuterSyntax.improper_command "thms_containing" "print theorems containing certain constants"
+ K.diag (Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
val thm_depsP =
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
--- a/src/Pure/Thy/thm_database.ML Thu Feb 01 20:42:34 2001 +0100
+++ b/src/Pure/Thy/thm_database.ML Thu Feb 01 20:43:14 2001 +0100
@@ -29,7 +29,7 @@
val ml_store_thm: string * thm -> unit
val ml_store_thms: string * thm list -> unit
val is_ml_identifier: string -> bool
- val print_thms_containing: theory -> xstring list -> unit
+ val print_thms_containing: theory -> term list -> unit
end;
structure ThmDatabase: THM_DATABASE =
@@ -95,22 +95,34 @@
(** retrieve theorems **)
-(*get theorems that contain all of given constants*)
-fun thms_containing_thy thy raw_consts =
- let val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
- in PureThy.thms_containing thy consts end
- handle THEORY (msg,_) => error msg;
+fun thms_containing_thy thy consts = PureThy.thms_containing thy consts
+ handle THEORY (msg, _) => error msg | THM (msg, _, _) => error msg;
+
+fun theory_of_goal () = ThyInfo.theory_of_sign (Thm.sign_of_thm (Goals.topthm ()));
+
+fun thms_containing raw_consts =
+ let
+ val thy = theory_of_goal ();
+ val consts = map (Sign.intern_const (Theory.sign_of thy)) raw_consts;
+ in thms_containing_thy thy consts end;
-fun thms_containing cs =
- thms_containing_thy (ThyInfo.theory_of_sign (Thm.sign_of_thm (Goals.topthm ()))) cs;
+fun print_thms_containing thy ts =
+ let
+ val prt_const =
+ Pretty.quote o Pretty.str o Sign.cond_extern (Theory.sign_of thy) Sign.constK;
+ fun prt_thm (a, th) = Pretty.block [Pretty.str (a ^ ":"),
+ Pretty.brk 1, Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
-fun prt_thm (a, th) =
- Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
- Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
-
-fun print_thms_containing thy cs =
- Pretty.writeln (Pretty.blk (0, Pretty.fbreaks (map prt_thm (thms_containing_thy thy cs))));
-
+ val cs = foldr Term.add_term_consts (ts, []);
+ val header =
+ if Library.null cs then []
+ else [Pretty.block (Pretty.breaks (Pretty.str "theorems containing constants:" ::
+ map prt_const cs)), Pretty.str ""];
+ in
+ if Library.null cs andalso not (Library.null ts) then
+ warning "thms_containing: no constants in specification"
+ else (header @ map prt_thm (thms_containing_thy thy cs)) |> Pretty.chunks |> Pretty.writeln
+ end;
(*top_const: main constant, ignoring Trueprop*)
fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None)
@@ -133,13 +145,13 @@
(* could be provided by thm db *)
fun index_intros c =
let fun topc(_,thm) = intro_const thm = Some(c);
- val named_thms = thms_containing [c]
+ val named_thms = thms_containing_thy (theory_of_goal ()) [c]
in filter topc named_thms end;
(* could be provided by thm db *)
fun index_elims c =
let fun topc(_,thm) = elim_const thm = Some(c);
- val named_thms = thms_containing [c]
+ val named_thms = thms_containing_thy (theory_of_goal ()) [c]
in filter topc named_thms end;
(*assume that parameters have unique names; reverse them for substitution*)