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 of the negated formula 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 be 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 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_response_fake [display,gray] "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+
−