theory ExternalSolverimports "../Base"beginsection {* 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_dpML {*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_oraclelemma "((p \<longrightarrow> q) \<longrightarrow> p) \<longrightarrow> p" by prop_oraclelemma "\<forall>x::nat. x \<ge> 0" sorry(* TODO: proof reconstruction *)end