theory ExternalSolver
imports "../Base"
begin

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

text {*
  {\bf Problem:}
  You want to use an external solver, because the solver might be more efficient 
  for deciding a certain class of formulae than Isabelle tactics.
  \smallskip

  {\bf Solution:} The easiest way to do this is by implementing an oracle.
  We will also construct proofs inside Isabelle by using the results produced 
  by the oracle.
  \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}

  For our explanation here, we will use the @{text metis} prover for proving
  propositional formulae. The general method will be roughly as follows: 
  Given a goal @{text G}, we transform it into the syntactical respresentation 
  of @{text "metis"}, build the CNF and then let metis search for a refutation. 
  @{text Metis} will either return the proved goal or raise an exception meaning 
  that it was unable to prove the goal (FIXME: is this so?).

  The translation function from Isabelle propositions into formulae of 
  @{text metis} is as follows:
  *}

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")*}


text {* 
  An example is as follows:

@{ML_response [display,gray] "trans @{prop \"A \<and> B\"}" 
"Metis.Formula.And 
        (Metis.Formula.Atom (\"A\", []), Metis.Formula.Atom (\"B\", []))"}


  The next function computes the conjunctive-normal-form.
*}


ML %linenumbers{*fun make_cnfs fm =
       fm |> Metis.Formula.Not
          |> Metis.Normalize.cnf
          |> map Metis.Formula.stripConj
          |> map (map Metis.Formula.stripDisj)
          |> map (map (map Metis.Literal.fromFormula))
          |> map (map Metis.LiteralSet.fromList)
          |> map (map Metis.Thm.axiom)*}

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

  (FIXME: What does Line 8 do?)

  (FIXME: Can this code improved?)


  Setting up the resolution.
*}

ML{*fun refute cls =
 let val result = 
        Metis.Resolution.loop             
          (Metis.Resolution.new Metis.Resolution.default cls)
 in
   (case result of
      Metis.Resolution.Contradiction _ => true
    | Metis.Resolution.Satisfiable _ => false)
 end*}

text {* 
  Stringing the functions together.
*}

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

text {* Setting up the oracle*}

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

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


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))*}

text {*
  (FIXME: The oracle returns a @{text cterm}. How is it possible
  that I can apply this cterm with @{ML rtac}?)
*}

method_setup prop_oracle = {*
  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (prop_oracle_tac ctxt))
*} "Oracle-based decision procedure for propositional logic"

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

lemma test: "p \<or> \<not>p"
  by prop_oracle

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

ML {* Thm.proof_of @{thm test} *} 

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

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

text {*
  (FIXME: proof reconstruction)
*}



text {*
  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.
*}


end