tuned section "Oracles";
Thu, 13 Nov 2008 21:38:44 +0100
changeset 28756 529798e71924
parent 28755 d5c1b7d67ea9
child 28757 7f7002ad6289
tuned section "Oracles";
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:38:02 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:38:44 2008 +0100
@@ -1133,19 +1133,25 @@
 section {* Oracles *}
-text {*
+text {* Oracles allow Isabelle to take advantage of external reasoners
+  such as arithmetic decision procedures, model checkers, fast
+  tautology checkers or computer algebra systems.  Invoked as an
+  oracle, an external reasoner can create arbitrary Isabelle theorems.
+  It is the responsibility of the user to ensure that the external
+  reasoner is as trustworthy as the application requires.  Another
+  typical source of errors is the linkup between Isabelle and the
+  external tool, not just its concrete implementation, but also the
+  required translation between two different logical environments.
+  Isabelle merely guarantees well-formedness of the propositions being
+  asserted, and records within the internal derivation object how
+  presumed theorems depend on unproven suppositions.
     @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
-  The oracle interface promotes a given ML function @{ML_text "'a -> cterm"}
-  to @{ML_text "'a -> thm"}.  This acts like an infinitary
-  specification of axioms -- there is no internal check of the
-  correctness of the results!  The inference kernel records oracle
-  invocations within the internal derivation object of theorems, and
-  the pretty printer attaches ``@{text "[!]"}'' to indicate results
-  that are not fully checked by Isabelle inferences.
     'oracle' name '=' text
@@ -1156,9 +1162,15 @@
   \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
   expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
   ML function of type @{ML_text "'a -> thm"}, which is bound to the
-  global identifier @{ML_text name}.
+  global identifier @{ML_text name}.  This acts like an infinitary
+  specification of axioms!  Invoking the oracle only works within the
+  scope of the resulting theory.
+  See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
+  defining a new primitive rule as oracle, and turning it into a proof
+  method.
@@ -1201,7 +1213,7 @@
   (unqualified) names may never be hidden.
   Note that hiding name space accesses has no impact on logical
-  declarations -- they remain valid internally.  Entities that are no
+  declarations --- they remain valid internally.  Entities that are no
   longer accessible to the user are printed with the special qualifier
   ``@{text "??"}'' prefixed to the full internal name.