9   You want to use an external solver, say, because it is more efficient in

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

    10   deciding particular formulas than any Isabelle tactic.

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

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

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

    14   To yield results checked by Isabelle's kernel, one can reconstruct the

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

    15   proofs.

    15   by the oracle.

    25   The general layout will be as follows. Given a goal G, we transform it into

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

    26   the syntactical respresentation of the external solver, and invoke the

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

    27   solver. The solver's result is then used inside the oracle to either return

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

    28   the proved goal or raise an exception meaning that the solver was unable to

    28   of @{text "metis"}, build the CNF and then let metis search for a refutation. 

    29   prove the goal.

    29   @{text Metis} will either return the proved goal or raise an exception meaning 

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

    31   For communication with external programs, there are the primitives

    32   The translation function from Isabelle propositions into formulae of 

    32   @{ML_text system} and @{ML_text system_out}, the latter of which captures

    33   @{text metis} is as follows:

    33   the invoked program's output. For simplicity, here, we will use metis, an

    34   external solver included in the Isabelle destribution. Since it is written

    35   in ML, we can call it directly without the detour of invoking an external

    36   program.

    37 

    38   We will restrict ourselves to proving formulas of propositional logic, a

    39   task metis is very good at.

    42 

    36 ML{*fun trans t =

    43 ML {*

    44 fun trans t =

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

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

    56   | _ => error "inacceptable term")

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

    49 

    50 

    51 text {* 

    52   An example is as follows:

    53 

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

    55 "Metis.Formula.And 

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

    57 

    58 

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

    60 ML {*

    63 ML %linenumbers{*fun make_cnfs fm =

    61 fun solve f =

    64        fm |> Metis.Formula.Not

    62   let

    65           |> Metis.Normalize.cnf

    63     open Metis

    66           |> map Metis.Formula.stripConj

    64     fun fromLiterals fms = LiteralSet.fromList (map Literal.fromFormula fms)

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

    65     fun fromClause fm = fromLiterals (Formula.stripDisj fm)

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

    66     fun fromCnf fm = map fromClause (Formula.stripConj fm)

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

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

    68     val mk_cnfs = map fromCnf o Normalize.cnf o Formula.Not

    72 text {* 

    69     fun refute cls =

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

    70       let val res = Resolution.new Resolution.default (map Thm.axiom cls)

    74 

    71       in

    75   (FIXME: What does Line 8 do?)

    72         (case Resolution.loop res of

    76 

    73           Resolution.Contradiction _ => true

    77   (FIXME: Can this code improved?)

    74         | Resolution.Satisfiable _ => false)

    78 

    75       end

    79 

    76   in List.all refute (mk_cnfs f) end

    80   Setting up the resolution.

    80 ML {*

    93 text {* 

    81 fun prop_dp (thy, t) = if solve (trans t) then Thm.cterm_of thy t 

    94   Stringing the functions together.

    82   else error "Proof failed."

    87 ML {*

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

    88 fun prop_oracle_tac ctxt = 

   108 

   109 

   110 ML{*fun prop_oracle_tac ctxt = 

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

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

    92     | NONE => no_tac))

   114     | NONE => no_tac))*}

   115 

   116 text {*

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

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

    99 lemma "p \<or> \<not>p"

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

   126 

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

   109 (* TODO: proof reconstruction *)

   144 

   145 

   146 text {*

   147   For communication with external programs, there are the primitives

   148   @{ML_text system} and @{ML_text system_out}, the latter of which captures

   149   the invoked program's output. For simplicity, here, we will use metis, an

   150   external solver included in the Isabelle destribution. Since it is written

   151   in ML, we can call it directly without the detour of invoking an external

   152   program.

   153 *}