1 theory ExternalSolver

     2 imports "../Base"

     3 begin

     4 

     5 section {* Using an External Solver *} 

     6 

     7 text {*

     8   {\bf Problem:}

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

    10   deciding particular formulas than any Isabelle tactic.

    11   \smallskip

    12 

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

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

    15   proofs.

    16   \smallskip

    17 

    18   \begin{readmore}

    19   A short introduction to oracles can be found in [isar-ref: no suitable label

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

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

    22   (TODO: add more references to the code)

    23   \end{readmore}

    24 

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

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

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

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

    29   prove the goal.

    30 

    31   For communication with external programs, there are the primitives

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

    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.

    40   *}

    41 

    42 

    43 ML {*

    44 fun trans t =

    45   (case t of

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

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

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

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

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

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

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

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

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

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

    56   | _ => error "inacceptable term")

    57 *}

    58 

    59 

    60 ML {*

    61 fun solve f =

    62   let

    63     open Metis

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

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

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

    67 

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

    69     fun refute cls =

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

    71       in

    72         (case Resolution.loop res of

    73           Resolution.Contradiction _ => true

    74         | Resolution.Satisfiable _ => false)

    75       end

    76   in List.all refute (mk_cnfs f) end

    77 *}

    78 

    79 

    80 ML {*

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

    82   else error "Proof failed."

    83 *}

    84 

    85 oracle prop_oracle = prop_dp

    86 

    87 ML {*

    88 fun prop_oracle_tac ctxt = 

    89   SUBGOAL (fn (goal, i) => 

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

    91       SOME thm => rtac thm i

    92     | NONE => no_tac))

    93 *}

    94 

    95 method_setup prop_oracle = {*

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

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

    98 

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

   100   by prop_oracle

   101 

   102 lemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p"

   103   by prop_oracle

   104 

   105 lemma "\<forall>x::nat. x \<ge> 0"

   106   sorry

   107 

   108 

   109 (* TODO: proof reconstruction *)

   110 

   111 

   112 end