3 uses ("external_solver.ML")

    56 

    57 

    58 

    59 

    60 section {* Writing an Oracle\label{rec:oracle} *} 

    61 

    62 text {*

    63   (FIXME: should go into a separate file)

    64 

    65   {\bf Problem:}

    66   You want to use a fast, new decision procedure not based one Isabelle's

    67   tactics, and you do not care whether it is sound.

    68   \smallskip

    69 

    70   {\bf Solution:} Isabelle provides the oracle mechanisms to bypass the

    71   inference kernel. Note that theorems proven by an oracle carry a special

    72   mark to inform the user of their potential incorrectness.

    73   \smallskip

    74 

    75   \begin{readmore}

    76   A short introduction to oracles can be found in [isar-ref: no suitable label

    77   for section 3.11]. A simple example, which we will slightly extend here,

    78   is given in @{ML_file "FOL/ex/IffOracle.thy"}. The raw interface for adding

    79   oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}.

    80   \end{readmore}

    81 

    82   For our explanation here, we restrict ourselves to decide propositional

    83   formulae which consist only of equivalences between propositional variables,

    84   i.e. we want to decide whether @{term "P = (Q = P) = Q"} is a tautology.

    85 

    86   Assume, that we have a decision procedure for such formulae, implemented

    87   in ML. Since we do not care how it works, we will use it here as an

    88   ``external solver'':

    89 *}

    90 

    91 use "external_solver.ML"

    92 

    93 text {*

    94   We do, however, know that the solver provides a function

    95   @{ML IffSolver.decide}.

    96   It takes a string representation of a formula and returns either

    97   @{ML true} if the formula is a tautology or

    98   @{ML false} otherwise. The input syntax is specified as follows:

    99 

   100   formula $::=$ atom $\mid$ \verb|(| formula \verb|<=>| formula \verb|)|

   101 

   102   and all token are separated by at least one space.

   103 

   104   (FIXME: is there a better way for describing the syntax?)

   105  

   106   We will proceed in the following way. We start by translating a HOL formula

   107   into the string representation expected by the solver. The solver's result

   108   is then used to build an oracle, which we will subsequently use as a core

   109   for an Isar method to be able to apply the oracle in proving theorems.

   110 

   111   Let us start with the translation function from Isabelle propositions into

   112   the solver's string representation. To increase efficiency while building

   113   the string, we use functions from the @{text Buffer} module.

   114   *}

   115 

   116 ML {*fun translate t =

   117   let

   118     fun trans t =

   119       (case t of

   120         @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u =>

   121           Buffer.add " (" #>

   122           trans t #>

   123           Buffer.add "<=>" #> 

   124           trans u #>

   125           Buffer.add ") "

   126       | Free (n, @{typ bool}) =>

   127          Buffer.add " " #> 

   128          Buffer.add n #>

   129          Buffer.add " "

   130       | _ => error "inacceptable term")

   131   in Buffer.content (trans t Buffer.empty) end

   132 *}

   133 

   134 text {*

   135   Here is the string representation of the term @{term "p = (q = p)"}:

   136 

   137   @{ML_response 

   138     "translate @{term \"p = (q = p)\"}" 

   139     "\" ( p <=> ( q <=> p ) ) \""}

   140 

   141   Let us check, what the solver returns when given a tautology:

   142 

   143   @{ML_response 

   144     "IffSolver.decide (translate @{term \"p = (q = p) = q\"})"

   145     "true"}

   146 

   147   And here is what it returns for a formula which is not valid:

   148 

   149   @{ML_response 

   150     "IffSolver.decide (translate @{term \"p = (q = p)\"})" 

   151     "false"}

   152 *}

   153 

   154 text {* 

   155   Now, we combine these functions into an oracle. In general, an oracle may

   156   be given any input, but it has to return a certified proposition (a

   157   special term which is type-checked), out of which Isabelle's inference

   158   kernel ``magically'' makes a theorem.

   159 

   160   Here, we take the proposition to be show as input. Note that we have

   161   to first extract the term which is then passed to the translation and

   162   decision procedure. If the solver finds this term to be valid, we return

   163   the given proposition unchanged to be turned then into a theorem:

   164 *}

   165 

   166 oracle iff_oracle = {* fn ct =>

   167   if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct)))

   168   then ct

   169   else error "Proof failed."*}

   170 

   171 text {*

   172   Here is what we get when applying the oracle:

   173 

   174   @{ML_response_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"}

   175 

   176   (FIXME: is there a better way to present the theorem?)

   177 

   178   To be able to use our oracle for Isar proofs, we wrap it into a tactic:

   179 *}

   180 

   181 ML{*val iff_oracle_tac =

   182   CSUBGOAL (fn (goal, i) => 

   183     (case try iff_oracle goal of

   184       NONE => no_tac

   185     | SOME thm => rtac thm i))*}

   186 

   187 text {*

   188   and create a new method solely based on this tactic:

   189 *}

   190 

   191 method_setup iff_oracle = {*

   192    Method.no_args (Method.SIMPLE_METHOD' iff_oracle_tac)

   193 *} "Oracle-based decision procedure for chains of equivalences"

   194 

   195 text {*

   196   (FIXME: what does @{ML "Method.SIMPLE_METHOD'"} do? ... what do you mean?)

   197 

   198   Finally, we can test our oracle to prove some theorems:

   199 *}

   200 

   201 lemma "p = (p::bool)"

   202    by iff_oracle

   203 

   204 lemma "p = (q = p) = q"

   205    by iff_oracle

   206 

   207 

   208 text {*

   209 (FIXME: say something about what the proof of the oracle is ... what do you mean?)

   210 *} 

   211 

   212