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:

  @{ML_response \<open>iff_oracle @{cprop "p = (p::bool)"}\<close> \<open>p = p\<close>}

  (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