# HG changeset patch
# User wenzelm
# Date 1566038662 -7200
# Node ID 7714971a58b56ea04142f68f0c771c788480825e
# Parent  c92443e8d724fd661808eb7191d1ce81c37531c5
added command 'thm_oracles';

diff -r c92443e8d724 -r 7714971a58b5 src/Doc/Isar_Ref/Proof.thy
--- 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.
diff -r c92443e8d724 -r 7714971a58b5 src/Doc/Isar_Ref/Spec.thy
--- 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>
 
 
diff -r c92443e8d724 -r 7714971a58b5 src/Pure/Pure.thy
--- 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);
 
diff -r c92443e8d724 -r 7714971a58b5 src/Pure/Thy/thm_deps.ML
--- 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 *)
 
diff -r c92443e8d724 -r 7714971a58b5 src/Pure/thm.ML
--- 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)));