5 section {* Using an External Solver\label{rec:external} *} 

     6 

     7 section {* Executing an External Application *}

     9   You want to use an external solver, because the solver might be more efficient 

    11   You want to use an external application.

    10   for deciding a certain class of formulae than Isabelle tactics.

    12   \smallskip

    11   \smallskip

    13 

    12 

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

    13   {\bf Solution:} The easiest way to do this is by implementing an oracle.

    15   you.

    14   We will also construct proofs inside Isabelle by using the results produced 

    16   \smallskip

    15   by the oracle.

    17 

    18   This function executes an external command as if printed in a shell. It

    19   returns the output of the program and its return value.

    20 

    21   For example, consider running an ordinary shell commands:

    22 

    23   @{ML_response [display,gray] 

    24     "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}

    25 

    26   Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}

    27   on Page~\pageref{rec:timeout}), i.e. external applications are killed

    28   properly. For example, the following expression takes only approximately

    29   one second:

    30 

    31   @{ML_response [display,gray] 

    32     "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"

    33      handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}

    34 *}

    35 

    36 text {*

    37   The function @{ML system_out} can also be used for more reasonable

    38   applications, e.g. coupling external solvers with Isabelle. In that case,

    39   one has to make sure that Isabelle can find the particular executable.

    40   One way to ensure this is by adding a Bash-like variable binding into

    41   one of Isabelle's settings file (prefer the user settings file usually to

    42   be found at @{text "$HOME/.isabelle/etc/settings"}).

    43   

    44   For example, assume you want to use the application @{text foo} which

    45   is here supposed to be located at @{text "/usr/local/bin/"}.

    46   The following line has to be added to one of Isabelle's settings file:

    47 

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

    49 

    50   In Isabelle, this application may now be executed by

    51 

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

    53 *}

    54 

    55 

    56 

    57 

    58 

    59 

    60 section {* Writing an Oracle\label{rec:external} *} 

    61 

    62 text {*

    63   {\bf Problem:}

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

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

    66   \smallskip

    67 

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

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

    70   mark to inform the user of their potential incorrectness.

    20   for section 3.11]. A simple example is given in 

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

    21   @{ML_file "FOL/ex/IffOracle"}.

    76   is given in @{ML_file "FOL/ex/IffOracle"}. The raw interface for adding

    22   (TODO: add more references to the code)

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

    25   For our explanation here, we will use the @{text metis} prover for proving

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

    26   propositional formulae. The general method will be roughly as follows: 

    81   formulae which consist only of equivalences between propositional variables,

    27   Given a goal @{text G}, we transform it into the syntactical respresentation 

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

    28   of @{text "metis"}, build the CNF of the negated formula and then let metis search 

    83 

    29   for a refutation. @{text Metis} will either return the proved goal or raise 

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

    30   an exception meaning 

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

    31   that it was unable to prove the goal (FIXME: is this so?).

    86   ``external solver'':

    32 

    87 *}

    33   The translation function from Isabelle propositions into formulae of 

    88 

    34   @{text metis} is as follows:

    89 use "external_solver.ML"

    90 

    91 text {*

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

    93   @{ML IffSolver.decide}.

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

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

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

    97 

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

    99 

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

   101 

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

   103  

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

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

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

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

   108 

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

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

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

    37 ML{*fun trans t =

   114 ML {*fun translate t =

    38   (case t of

   115   let

    39     @{term Trueprop} $ t => trans t

   116     fun trans t =

    40   | @{term True} => Metis.Formula.True

   117       (case t of

    41   | @{term False} => Metis.Formula.False

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

    42   | @{term Not} $ t => Metis.Formula.Not (trans t)

   119           Buffer.add " (" #>

    43   | @{term "op &"} $ t1 $ t2 => Metis.Formula.And (trans t1, trans t2)

   120           trans t #>

    44   | @{term "op |"} $ t1 $ t2 => Metis.Formula.Or (trans t1, trans t2)

   121           Buffer.add "<=>" #> 

    45   | @{term "op -->"} $ t1 $ t2 => Metis.Formula.Imp (trans t1, trans t2)

   122           trans u #>

    46   | @{term "op = :: bool => bool => bool"} $ t1 $ t2 => 

   123           Buffer.add ") "

    47                                      Metis.Formula.Iff (trans t1, trans t2)

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

    48   | Free (n, @{typ bool}) => Metis.Formula.Atom (n, [])

   125          Buffer.add " " #> 

    49   | _ => error "inacceptable term")*}

   126          Buffer.add n #>

    50 

   127          Buffer.add " "

   128       | _ => error "inacceptable term")

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

   130 *}

   131 

   132 text {*

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

   134 

   135   @{ML_response 

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

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

   138 

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

   140 

   141   @{ML_response 

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

   143     "true"}

   144 

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

   146 

   147   @{ML_response 

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

   149     "false"}

   150 *}

    53   An example is as follows:

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

    54 

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

    55 @{ML_response [display,gray] "trans @{prop \"A \<and> B\"}" 

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

    56 "Metis.Formula.And 

   156   kernel ``magically'' makes a theorem.

    57         (Metis.Formula.Atom (\"A\", []), Metis.Formula.Atom (\"B\", []))"}

   157 

    58 

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

    59 

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

    60   The next function computes the conjunctive-normal-form.

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

    61 *}

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

    62 

   162 *}

    63 

   163 

    64 ML %linenumbers{*fun make_cnfs fm =

   164 oracle iff_oracle = {* fn ct =>

    65        fm |> Metis.Formula.Not

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

    66           |> Metis.Normalize.cnf

   166   then ct

    67           |> map Metis.Formula.stripConj

   167   else error "Proof failed."*}

    68           |> map (map Metis.Formula.stripDisj)

   168 

    69           |> map (map (map Metis.Literal.fromFormula))

   169 text {*

    70           |> map (map Metis.LiteralSet.fromList)

   170   Here is what we get when applying the oracle:

    71           |> map (map Metis.Thm.axiom)*}

   171 

    72 

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

    73 text {* 

   173 

    74   (FIXME: Is there a deep reason why Metis.Normalize.cnf returns a list?)

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

    75 

   175 

    76   (FIXME: What does Line 8 do?)

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

    77 

   177 *}

    78   (FIXME: Can this code be improved?)

   178 

    79 

   179 ML{*val iff_oracle_tac =

    80 

   180   CSUBGOAL (fn (goal, i) => 

    81   Setting up the resolution.

   181     (case try iff_oracle goal of

    82 *}

   182       NONE => no_tac

    83 

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

    84 ML{*fun refute cls =

   184 

    85  let val result = 

   185 text {*

    86         Metis.Resolution.loop             

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

    87           (Metis.Resolution.new Metis.Resolution.default cls)

   187 *}

    88  in

   188 

    89    (case result of

   189 method_setup iff_oracle = {*

    90       Metis.Resolution.Contradiction _ => true

   190    Method.no_args (Method.SIMPLE_METHOD' iff_oracle_tac)

    91     | Metis.Resolution.Satisfiable _ => false)

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

    92  end*}

   192 

    93 

   193 text {*

    94 text {* 

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

    95   Stringing the functions together.

   195 

    96 *}

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

    97 

   197 *}

    98 ML{*fun solve f = List.all refute (make_cnfs f)*}

   198 

    99 

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

   100 text {* Setting up the oracle*}

   200    by iff_oracle

   101 

   201 

   102 ML{*fun prop_dp (thy, t) = 

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

   103         if solve (trans t) then (Thm.cterm_of thy t) 

   203    by iff_oracle

   104         else error "Proof failed."*}

   204 

   105 

   205 

   106 oracle prop_oracle = prop_dp

   206 text {*

   107 

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

   108 text {* (FIXME: What does oracle do?) *}

   109 

   110 

   111 ML{*fun prop_oracle_tac ctxt = 

   112   SUBGOAL (fn (goal, i) => 

   113     (case (try prop_oracle (ProofContext.theory_of ctxt, goal)) of

   114       SOME thm => rtac thm i

   115     | NONE => no_tac))*}

   116 

   117 text {*

   118   (FIXME: The oracle returns a @{text cterm}. How is it possible

   119   that I can apply this cterm with @{ML rtac}?)

   120 *}

   121 

   122 method_setup prop_oracle = {*

   123   Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (prop_oracle_tac ctxt))

   124 *} "Oracle-based decision procedure for propositional logic"

   125 

   126 text {* (FIXME What does @{ML Method.SIMPLE_METHOD'} do?) *}

   127 

   128 lemma test: "p \<or> \<not>p"

   129   by prop_oracle

   130 

   131 text {* (FIXME: say something about what the proof of the oracle is)

   132 

   133   @{ML_response_fake [display,gray] "Thm.proof_of @{thm test}" "???"}

   134