ProgTutorial/Recipes/Oracle.thy
changeset 565 cecd7a941885
parent 562 daf404920ab9
child 567 f7c97e64cc2a
--- a/ProgTutorial/Recipes/Oracle.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Recipes/Oracle.thy	Tue May 14 17:10:47 2019 +0200
@@ -2,9 +2,9 @@
 imports "../Appendix"
 begin
 
-section {* Writing an Oracle (TBD)\label{rec:oracle} *} 
+section \<open>Writing an Oracle (TBD)\label{rec:oracle}\<close> 
 
-text {*
+text \<open>
   {\bf Problem:}
   You want to use a fast, new decision procedure not based one Isabelle's
   tactics, and you do not care whether it is sound.
@@ -29,11 +29,11 @@
   Assume, that we have a decision procedure for such formulae, implemented
   in ML. Since we do not care how it works, we will use it here as an
   ``external solver'':
-*}
+\<close>
 
 ML_file "external_solver.ML"
 
-text {*
+text \<open>
   We do, however, know that the solver provides a function
   @{ML IffSolver.decide}.
   It takes a string representation of a formula and returns either
@@ -53,10 +53,10 @@
 
   Let us start with the translation function from Isabelle propositions into
   the solver's string representation. To increase efficiency while building
-  the string, we use functions from the @{text Buffer} module.
-  *}
+  the string, we use functions from the \<open>Buffer\<close> module.
+\<close>
 
-ML %grayML{*fun translate t =
+ML %grayML\<open>fun translate t =
   let
     fun trans t =
       (case t of
@@ -71,9 +71,9 @@
          Buffer.add n #>
          Buffer.add " "
       | _ => error "inacceptable term")
-  in Buffer.content (trans t Buffer.empty) end*}
+  in Buffer.content (trans t Buffer.empty) end\<close>
 
-text {*
+text \<open>
   Here is the string representation of the term @{term "p = (q = p)"}:
 
   @{ML_response 
@@ -91,9 +91,9 @@
   @{ML_response 
     "IffSolver.decide (translate @{term \"p = (q = p)\"})" 
     "false"}
-*}
+\<close>
 
-text {* 
+text \<open>
   Now, we combine these functions into an oracle. In general, an oracle may
   be given any input, but it has to return a certified proposition (a
   special term which is type-checked), out of which Isabelle's inference
@@ -103,14 +103,14 @@
   to first extract the term which is then passed to the translation and
   decision procedure. If the solver finds this term to be valid, we return
   the given proposition unchanged to be turned then into a theorem:
-*}
+\<close>
 
-oracle iff_oracle = {* fn ct =>
+oracle iff_oracle = \<open>fn ct =>
   if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct)))
   then ct
-  else error "Proof failed."*}
+  else error "Proof failed."\<close>
 
-text {*
+text \<open>
   Here is what we get when applying the oracle:
 
   @{ML_response_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"}
@@ -118,25 +118,25 @@
   (FIXME: is there a better way to present the theorem?)
 
   To be able to use our oracle for Isar proofs, we wrap it into a tactic:
-*}
+\<close>
 
-ML %grayML{*fun iff_oracle_tac ctxt =
+ML %grayML\<open>fun iff_oracle_tac ctxt =
   CSUBGOAL (fn (goal, i) => 
     (case try iff_oracle goal of
       NONE => no_tac
-    | SOME thm => resolve_tac ctxt [thm] i))*}
+    | SOME thm => resolve_tac ctxt [thm] i))\<close>
 
-text {*
+text \<open>
   and create a new method solely based on this tactic:
-*}
+\<close>
 
-method_setup iff_oracle = {*
+method_setup iff_oracle = \<open>
    Scan.succeed (fn ctxt => (Method.SIMPLE_METHOD' (iff_oracle_tac ctxt)))
-*} "Oracle-based decision procedure for chains of equivalences"
+\<close> "Oracle-based decision procedure for chains of equivalences"
 
-text {*
+text \<open>
   Finally, we can test our oracle to prove some theorems:
-*}
+\<close>
 
 lemma "p = (p::bool)"
    by iff_oracle
@@ -145,9 +145,9 @@
    by iff_oracle
 
 
-text {*
+text \<open>
 (FIXME: say something about what the proof of the oracle is ... what do you mean?)
-*} 
+\<close> 
 
 
 end