theory Oracle

imports "../Appendix"

begin

section \<open>Writing an Oracle (TBD)\label{rec:oracle}\<close> 

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.

  \smallskip

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

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

  mark to inform the user of their potential incorrectness.

  \smallskip

  \begin{readmore}

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

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

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

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

  \end{readmore}

  For our explanation here, we restrict ourselves to decide propositional

  formulae which consist only of equivalences between propositional variables,

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

  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 \<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

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

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

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

  and all token are separated by at least one space.

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

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

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

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

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

  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 \<open>Buffer\<close> module.

\<close>

ML %grayML\<open>fun translate t =

  let

    fun trans t =

      (case t of

        @{term "(=) :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u =>

          Buffer.add " (" #>

          trans t #>

          Buffer.add "<=>" #> 

          trans u #>

          Buffer.add ") "

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

         Buffer.add " " #> 

         Buffer.add n #>

         Buffer.add " "

      | _ => error "inacceptable term")

  in Buffer.content (trans t Buffer.empty) end\<close>

text \<open>

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

  @{ML_matchresult \<open>translate @{term "p = (q = p)"}\<close> 

    \<open>" ( p <=> ( q <=> p ) ) "\<close>}

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

  @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p) = q"})\<close>

    \<open>true\<close>}

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

  @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p)"})\<close> 

    \<open>false\<close>}

\<close>

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

  kernel ``magically'' makes a theorem.

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

  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 = \<open>fn ct =>

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

  then ct

  else error "Proof failed."\<close>

text \<open>

  Here is what we get when applying the oracle:

  (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\<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))\<close>

text \<open>

  and create a new method solely based on this tactic:

\<close>

method_setup iff_oracle = \<open>

   Scan.succeed (fn ctxt => (Method.SIMPLE_METHOD' (iff_oracle_tac ctxt)))

\<close> "Oracle-based decision procedure for chains of equivalences"

text \<open>

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

\<close>

lemma "p = (p::bool)"

   by iff_oracle

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

   by iff_oracle

text \<open>

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

\<close> 

end