theory ExternalSolver

imports "../Base"

begin

section {* Using an External Solver *} 

text {*

  {\bf Problem:}

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

  deciding particular formulas than any Isabelle tactic.

  \smallskip

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

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

  proofs.

  \smallskip

  \begin{readmore}

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

  for section 3.11]. A simple example is given in 

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

  (TODO: add more references to the code)

  \end{readmore}

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

  the syntactical respresentation of the external solver, and invoke the

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

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

  prove the goal.

  For communication with external programs, there are the primitives

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

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

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

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

  program.

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

  task metis is very good at.

  *}

ML {*

fun trans t =

  (case t of

    @{term Trueprop} $ t => trans t

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

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

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

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

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

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

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

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

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

  | _ => error "inacceptable term")

*}

ML {*

fun solve f =

  let

    open Metis

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

    fun fromClause fm = fromLiterals (Formula.stripDisj fm)

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

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

    fun refute cls =

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

      in

        (case Resolution.loop res of

          Resolution.Contradiction _ => true

        | Resolution.Satisfiable _ => false)

      end

  in List.all refute (mk_cnfs f) end

*}

ML {*

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

  else error "Proof failed."

*}

oracle prop_oracle = prop_dp

ML {*

fun prop_oracle_tac ctxt = 

  SUBGOAL (fn (goal, i) => 

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

      SOME thm => rtac thm i

    | NONE => no_tac))

*}

method_setup prop_oracle = {*

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

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

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

  by prop_oracle

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

  by prop_oracle

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

  sorry

(* TODO: proof reconstruction *)

end