theory ExternalSolver

imports "../Base"

begin

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