--- a/src/Doc/Isar_Ref/Proof.thy Sat Aug 17 11:52:47 2019 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Sat Aug 17 12:44:22 2019 +0200
@@ -735,7 +735,7 @@
development, or if the @{attribute quick_and_dirty} is enabled. Facts
emerging from fake proofs are not the real thing. Internally, the derivation
object is tainted by an oracle invocation, which may be inspected via the
- theorem status @{cite "isabelle-implementation"}.
+ command @{command "thm_oracles"} (\secref{sec:oracles}).
The most important application of @{command "sorry"} is to support
experimentation and top-down proof development.
--- a/src/Doc/Isar_Ref/Spec.thy Sat Aug 17 11:52:47 2019 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Aug 17 12:44:22 2019 +0200
@@ -1419,11 +1419,12 @@
\<close>
-section \<open>Oracles\<close>
+section \<open>Oracles \label{sec:oracles}\<close>
text \<open>
\begin{matharray}{rcll}
@{command_def "oracle"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\
+ @{command_def "thm_oracles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\end{matharray}
Oracles allow Isabelle to take advantage of external reasoners such as
@@ -1439,10 +1440,15 @@
Isabelle merely guarantees well-formedness of the propositions being
asserted, and records within the internal derivation object how presumed
- theorems depend on unproven suppositions.
+ theorems depend on unproven suppositions. This also includes implicit
+ type-class reasoning via the order-sorted algebra of class relations and
+ type arities (see also @{command_ref instantiation} and @{command_ref
+ instance}).
\<^rail>\<open>
@@{command oracle} @{syntax name} '=' @{syntax text}
+ ;
+ @@{command thm_oracles} @{syntax thms}
\<close>
\<^descr> \<^theory_text>\<open>oracle name = "text"\<close> turns the given ML expression \<open>text\<close> of type
@@ -1451,9 +1457,12 @@
infinitary specification of axioms! Invoking the oracle only works within
the scope of the resulting theory.
-
See \<^file>\<open>~~/src/HOL/ex/Iff_Oracle.thy\<close> for a worked example of defining a new
primitive rule as oracle, and turning it into a proof method.
+
+ \<^descr> \<^theory_text>\<open>thm_oracles thms\<close> displays all oracles used in the internal derivation
+ of the given theorems; this covers the full graph of transitive
+ dependencies.
\<close>
--- a/src/Pure/Pure.thy Sat Aug 17 11:52:47 2019 +0200
+++ b/src/Pure/Pure.thy Sat Aug 17 12:44:22 2019 +0200
@@ -84,7 +84,7 @@
"print_interps" "print_dependencies" "print_attributes"
"print_simpset" "print_rules" "print_trans_rules" "print_methods"
"print_antiquotations" "print_ML_antiquotations" "thy_deps"
- "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
+ "locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings"
"print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
and "print_state" :: diag
@@ -1307,6 +1307,15 @@
Thm_Deps.thm_deps (Toplevel.theory_of st)
(Attrib.eval_thms (Toplevel.context_of st) args))));
+val _ =
+ Outer_Syntax.command \<^command_keyword>\<open>thm_oracles\<close>
+ "print all oracles used in theorems (full graph of transitive dependencies)"
+ (Parse.thms1 >> (fn args =>
+ Toplevel.keep (fn st =>
+ let
+ val ctxt = Toplevel.context_of st;
+ val thms = Attrib.eval_thms ctxt args;
+ in Pretty.writeln (Thm_Deps.pretty_thm_oracles ctxt thms) end)));
val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name);
--- a/src/Pure/Thy/thm_deps.ML Sat Aug 17 11:52:47 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML Sat Aug 17 12:44:22 2019 +0200
@@ -8,6 +8,7 @@
signature THM_DEPS =
sig
val all_oracles: thm list -> Proofterm.oracle list
+ val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
val thm_deps: theory -> thm list -> unit
val unused_thms: theory list * theory list -> (string * thm) list
end;
@@ -20,6 +21,13 @@
fun all_oracles thms =
Proofterm.all_oracles_of (map Thm.proof_body_of thms);
+fun pretty_thm_oracles ctxt thms =
+ let
+ fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name]
+ | prt_oracle (name, SOME prop) =
+ [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, Syntax.pretty_term ctxt prop];
+ in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;
+
(* thm_deps *)
--- a/src/Pure/thm.ML Sat Aug 17 11:52:47 2019 +0200
+++ b/src/Pure/thm.ML Sat Aug 17 12:44:22 2019 +0200
@@ -124,6 +124,8 @@
val arity_proof: theory -> string * sort list * class -> proof
(*oracles*)
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
+ val oracle_space: theory -> Name_Space.T
+ val pretty_oracle: Proof.context -> string -> Pretty.T
val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list
(*inference rules*)
val assume: cterm -> thm
@@ -1058,6 +1060,11 @@
end;
in ((name, invoke_oracle), thy') end;
+val oracle_space = Name_Space.space_of_table o get_oracles;
+
+fun pretty_oracle ctxt =
+ Name_Space.pretty ctxt (oracle_space (Proof_Context.theory_of ctxt));
+
fun extern_oracles verbose ctxt =
map #1 (Name_Space.markup_table verbose ctxt (get_oracles (Proof_Context.theory_of ctxt)));