1 theory Oracle

     2 imports "../Base"

     3 uses ("external_solver.ML")

     4 begin

     5 

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

     7 

     8 text {*

     9   {\bf Problem:}

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

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

    12   \smallskip

    13 

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

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

    16   mark to inform the user of their potential incorrectness.

    17   \smallskip

    18 

    19   \begin{readmore}

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

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

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

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

    24   \end{readmore}

    25 

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

    27   formulae which consist only of equivalences between propositional variables,

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

    29 

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

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

    32   ``external solver'':

    33 *}

    34 

    35 use "external_solver.ML"

    36 

    37 text {*

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

    39   @{ML IffSolver.decide}.

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

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

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

    43 

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

    45 

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

    47 

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

    49  

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

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

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

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

    54 

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

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

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

    58   *}

    59 

    60 ML {*fun translate t =

    61   let

    62     fun trans t =

    63       (case t of

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

    65           Buffer.add " (" #>

    66           trans t #>

    67           Buffer.add "<=>" #> 

    68           trans u #>

    69           Buffer.add ") "

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

    71          Buffer.add " " #> 

    72          Buffer.add n #>

    73          Buffer.add " "

    74       | _ => error "inacceptable term")

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

    76 *}

    77 

    78 text {*

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

    80 

    81   @{ML_response 

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

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

    84 

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

    86 

    87   @{ML_response 

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

    89     "true"}

    90 

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

    92 

    93   @{ML_response 

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

    95     "false"}

    96 *}

    97 

    98 text {* 

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

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

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

   102   kernel ``magically'' makes a theorem.

   103 

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

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

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

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

   108 *}

   109 

   110 oracle iff_oracle = {* fn ct =>

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

   112   then ct

   113   else error "Proof failed."*}

   114 

   115 text {*

   116   Here is what we get when applying the oracle:

   117 

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

   119 

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

   121 

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

   123 *}

   124 

   125 ML{*val iff_oracle_tac =

   126   CSUBGOAL (fn (goal, i) => 

   127     (case try iff_oracle goal of

   128       NONE => no_tac

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

   130 

   131 text {*

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

   133 *}

   134 

   135 method_setup iff_oracle = {*

   136    Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac))

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

   138 

   139 text {*

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

   141 *}

   142 

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

   144    by iff_oracle

   145 

   146 lemma "p = (q = p) = q"

   147    by iff_oracle

   148 

   149 

   150 text {*

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

   152 *} 

   153 

   154 

   155 end