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