theory ExternalSolver
imports "../Base"
uses ("external_solver.ML")
begin


section {* Executing an External Application \label{rec:external}*}

text {*
  {\bf Problem:}
  You want to use an external application.
  \smallskip

  {\bf Solution:} The function @{ML system_out} might be the right thing for
  you.
  \smallskip

  This function executes an external command as if printed in a shell. It
  returns the output of the program and its return value.

  For example, consider running an ordinary shell commands:

  @{ML_response [display,gray] 
    "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}

  Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
  on Page~\pageref{rec:timeout}), i.e. external applications are killed
  properly. For example, the following expression takes only approximately
  one second:

  @{ML_response [display,gray] 
    "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"
     handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
*}

text {*
  The function @{ML system_out} can also be used for more reasonable
  applications, e.g. coupling external solvers with Isabelle. In that case,
  one has to make sure that Isabelle can find the particular executable.
  One way to ensure this is by adding a Bash-like variable binding into
  one of Isabelle's settings file (prefer the user settings file usually to
  be found at @{text "$HOME/.isabelle/etc/settings"}).
  
  For example, assume you want to use the application @{text foo} which
  is here supposed to be located at @{text "/usr/local/bin/"}.
  The following line has to be added to one of Isabelle's settings file:

  @{text "FOO=/usr/local/bin/foo"}

  In Isabelle, this application may now be executed by

  @{ML_response_fake [display,gray] "system_out \"$FOO\"" "\<dots>"}
*}






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

text {*
  (FIXME: should go into a separate file)

  {\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 "FOL/ex/IffOracle.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'':
*}

use "external_solver.ML"

text {*
  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 @{text Buffer} module.
  *}

ML {*fun translate t =
  let
    fun trans t =
      (case t of
        @{term "op = :: 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
*}

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

  @{ML_response 
    "translate @{term \"p = (q = p)\"}" 
    "\" ( p <=> ( q <=> p ) ) \""}

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

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

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

  @{ML_response 
    "IffSolver.decide (translate @{term \"p = (q = p)\"})" 
    "false"}
*}

text {* 
  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:
*}

oracle iff_oracle = {* fn ct =>
  if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct)))
  then ct
  else error "Proof failed."*}

text {*
  Here is what we get when applying the oracle:

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

  (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:
*}

ML{*val iff_oracle_tac =
  CSUBGOAL (fn (goal, i) => 
    (case try iff_oracle goal of
      NONE => no_tac
    | SOME thm => rtac thm i))*}

text {*
  and create a new method solely based on this tactic:
*}

method_setup iff_oracle = {*
   Method.no_args (Method.SIMPLE_METHOD' iff_oracle_tac)
*} "Oracle-based decision procedure for chains of equivalences"

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

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

lemma "p = (p::bool)"
   by iff_oracle

lemma "p = (q = p) = q"
   by iff_oracle


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


end