theory ExternalSolver

imports "../Base"

uses ("external_solver.ML")

begin

section {* Executing an External Application *}

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

text {*

  {\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"}. The raw interface for adding

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

  \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