diff -r ef778679d3e0 -r a53c7810e38b CookBook/Recipes/ExternalSolver.thy --- a/CookBook/Recipes/ExternalSolver.thy Mon Jan 26 12:28:43 2009 +0000 +++ b/CookBook/Recipes/ExternalSolver.thy Mon Jan 26 12:29:01 2009 +0000 @@ -6,13 +6,13 @@ text {* {\bf Problem:} - You want to use an external solver, say, because it is more efficient in - deciding particular formulas than any Isabelle tactic. + 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 writing an oracle. - To yield results checked by Isabelle's kernel, one can reconstruct the - proofs. + {\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} @@ -22,26 +22,18 @@ (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 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?). - 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. + The translation function from Isabelle propositions into formulae of + @{text metis} is as follows: *} - -ML {* -fun trans t = +ML{*fun trans t = (case t of @{term Trueprop} $ t => trans t | @{term True} => Metis.Formula.True @@ -51,62 +43,114 @@ | @{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) + Metis.Formula.Iff (trans t1, trans t2) | Free (n, @{typ bool}) => Metis.Formula.Atom (n, []) - | _ => error "inacceptable term") + | _ => error "inacceptable term")*} + + +text {* + An example is as follows: + +@{ML_response [display,gray] "trans @{prop \"A \ B\"}" +"Metis.Formula.And + (Metis.Formula.Atom (\"A\", []), Metis.Formula.Atom (\"B\", []))"} + + + The next function computes the conjunctive-normal-form. *} -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) +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)*} - 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 +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*} -ML {* -fun prop_dp (thy, t) = if solve (trans t) then Thm.cterm_of thy t - else error "Proof failed." +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 -ML {* -fun prop_oracle_tac ctxt = +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 + (case (try prop_oracle (ProofContext.theory_of ctxt, goal)) of SOME thm => rtac thm i - | NONE => no_tac)) + | 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" -lemma "p \ \p" +text {* (FIXME What does @{ML Method.SIMPLE_METHOD'} do?) *} + +lemma test: "p \ \p" by prop_oracle +text {* (FIXME: say something about what the proof of the oracle is) *} + +ML {* Thm.proof_of @{thm test} *} + lemma "((p \ q) \ p) \ p" by prop_oracle lemma "\x::nat. x \ 0" sorry +text {* + (FIXME: proof reconstruction) +*} -(* TODO: 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 \ No newline at end of file