# HG changeset patch # User boehmes # Date 1233331111 -3600 # Node ID 531e453c9d674b3e8deac0016bc5970b50b18931 # Parent 62fb91f869081616231c6c06f36befc73d33abc2 rewrote recipes describing external solvers diff -r 62fb91f86908 -r 531e453c9d67 CookBook/Recipes/ExternalSolver.thy --- a/CookBook/Recipes/ExternalSolver.thy Fri Jan 30 08:24:48 2009 +0000 +++ b/CookBook/Recipes/ExternalSolver.thy Fri Jan 30 16:58:31 2009 +0100 @@ -1,161 +1,211 @@ theory ExternalSolver imports "../Base" +uses ("external_solver.ML") begin -section {* Using an External Solver\label{rec:external} *} + +section {* Executing an External Application *} 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. + You want to use an external application. + \smallskip + + {\bf Solution:} The function @{ML system_out} might be the right thing for + you. \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. + This function executes an external command as if printed in a shell. It + returns the output of the program and its return value. + + For example, consider running an ordinary shell commands: + + @{ML_response [display,gray] + "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"} + + Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout} + on Page~\pageref{rec:timeout}), i.e. external applications are killed + properly. For example, the following expression takes only approximately + one second: + + @{ML_response [display,gray] + "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\" + handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"} +*} + +text {* + The function @{ML system_out} can also be used for more reasonable + applications, e.g. coupling external solvers with Isabelle. In that case, + one has to make sure that Isabelle can find the particular executable. + One way to ensure this is by adding a Bash-like variable binding into + one of Isabelle's settings file (prefer the user settings file usually to + be found at @{text "$HOME/.isabelle/etc/settings"}). + + For example, assume you want to use the application @{text foo} which + is here supposed to be located at @{text "/usr/local/bin/"}. + The following line has to be added to one of Isabelle's settings file: + + @{text "FOO=/usr/local/bin/foo"} + + In Isabelle, this application may now be executed by + + @{ML_response_fake [display,gray] "system_out \"$FOO\"" "\"} +*} + + + + + + +section {* Writing an Oracle\label{rec:external} *} + +text {* + {\bf Problem:} + You want to use a fast, new decision procedure not based one Isabelle's + tactics, and you do not care whether it is sound. + \smallskip + + {\bf Solution:} Isabelle provides the oracle mechanisms to bypass the + inference kernel. Note that theorems proven by an oracle carry a special + mark to inform the user of their potential incorrectness. \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) + for section 3.11]. A simple example, which we will slightly extend here, + is given in @{ML_file "FOL/ex/IffOracle"}. The raw interface for adding + oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm"}. \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?). + For our explanation here, we restrict ourselves to decide propositional + formulae which consist only of equivalences between propositional variables, + i.e. we want to decide whether @{term "P = (Q = P) = Q"} is a tautology. + + Assume, that we have a decision procedure for such formulae, implemented + in ML. Since we do not care how it works, we will use it here as an + ``external solver'': +*} + +use "external_solver.ML" - The translation function from Isabelle propositions into formulae of - @{text metis} is as follows: +text {* + We do, however, know that the solver provides a function + @{ML IffSolver.decide}. + It takes a string representation of a formula and returns either + @{ML true} if the formula is a tautology or + @{ML false} otherwise. The input syntax is specified as follows: + + formula $::=$ atom $\mid$ \verb|(| formula \verb|<=>| formula \verb|)| + + and all token are separated by at least one space. + + (FIXME: is there a better way for describing the syntax?) + + We will proceed in the following way. We start by translating a HOL formula + into the string representation expected by the solver. The solver's result + is then used to build an oracle, which we will subsequently use as a core + for an Isar method to be able to apply the oracle in proving theorems. + + Let us start with the translation function from Isabelle propositions into + the solver's string representation. To increase efficiency while building + the string, we use functions from the @{text Buffer} module. *} -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 \ B\"}" -"Metis.Formula.And - (Metis.Formula.Atom (\"A\", []), Metis.Formula.Atom (\"B\", []))"} - - - The next function computes the conjunctive-normal-form. +ML {*fun translate t = + let + fun trans t = + (case t of + @{term "op = :: bool \ bool \ bool"} $ t $ u => + Buffer.add " (" #> + trans t #> + Buffer.add "<=>" #> + trans u #> + Buffer.add ") " + | Free (n, @{typ bool}) => + Buffer.add " " #> + Buffer.add n #> + Buffer.add " " + | _ => error "inacceptable term") + in Buffer.content (trans t Buffer.empty) end *} +text {* + Here is the string representation of the term @{term "p = (q = p)"}: -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)*} + @{ML_response + "translate @{term \"p = (q = p)\"}" + "\" ( p <=> ( q <=> p ) ) \""} + + Let us check, what the solver returns when given a tautology: + + @{ML_response + "IffSolver.decide (translate @{term \"p = (q = p) = q\"})" + "true"} + + And here is what it returns for a formula which is not valid: + + @{ML_response + "IffSolver.decide (translate @{term \"p = (q = p)\"})" + "false"} +*} text {* - (FIXME: Is there a deep reason why Metis.Normalize.cnf returns a list?) - - (FIXME: What does Line 8 do?) + Now, we combine these functions into an oracle. In general, an oracle may + be given any input, but it has to return a certified proposition (a + special term which is type-checked), out of which Isabelle's inference + kernel ``magically'' makes a theorem. - (FIXME: Can this code be improved?) - - - Setting up the resolution. + Here, we take the proposition to be show as input. Note that we have + to first extract the term which is then passed to the translation and + decision procedure. If the solver finds this term to be valid, we return + the given proposition unchanged to be turned then into a theorem: *} -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*} +oracle iff_oracle = {* fn ct => + if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct))) + then ct + else error "Proof failed."*} -text {* - Stringing the functions together. +text {* + Here is what we get when applying the oracle: + + @{ML_response_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"} + + (FIXME: is there a better way to present the theorem?) + + To be able to use our oracle for Isar proofs, we wrap it into a tactic: *} -ML{*fun solve f = List.all refute (make_cnfs f)*} +ML{*val iff_oracle_tac = + CSUBGOAL (fn (goal, i) => + (case try iff_oracle goal of + NONE => no_tac + | SOME thm => rtac thm i))*} -text {* Setting up the oracle*} +text {* + and create a new method solely based on this tactic: +*} -ML{*fun prop_dp (thy, t) = - if solve (trans t) then (Thm.cterm_of thy t) - else error "Proof failed."*} +method_setup iff_oracle = {* + Method.no_args (Method.SIMPLE_METHOD' iff_oracle_tac) +*} "Oracle-based decision procedure for chains of equivalences" + +text {* + (FIXME: what does @{ML "Method.SIMPLE_METHOD'"} do? ... what do you mean?) -oracle prop_oracle = prop_dp + Finally, we can test our oracle to prove some theorems: +*} -text {* (FIXME: What does oracle do?) *} +lemma "p = (p::bool)" + by iff_oracle + +lemma "p = (q = p) = q" + by iff_oracle -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 \ \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}" "???"} - +(FIXME: say something about what the proof of the oracle is ... what do you mean?) *} - -lemma "((p \ q) \ p) \ p" - by prop_oracle - -lemma "\x::nat. x \ 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 \ No newline at end of file diff -r 62fb91f86908 -r 531e453c9d67 CookBook/Recipes/TimeLimit.thy --- a/CookBook/Recipes/TimeLimit.thy Fri Jan 30 08:24:48 2009 +0000 +++ b/CookBook/Recipes/TimeLimit.thy Fri Jan 30 16:58:31 2009 +0100 @@ -2,7 +2,7 @@ imports "../Base" begin -section {* Restricting the Runtime of a Function *} +section {* Restricting the Runtime of a Function\label{rec:timeout} *} text {* {\bf Problem:} @@ -30,7 +30,7 @@ @{ML_response [display,gray] "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) - handle TimeOut => ~1" + handle TimeLimit.TimeOut => ~1" "~1"} where @{ML_text TimeOut} is the exception raised when the time limit diff -r 62fb91f86908 -r 531e453c9d67 CookBook/Recipes/external_solver.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Recipes/external_solver.ML Fri Jan 30 16:58:31 2009 +0100 @@ -0,0 +1,56 @@ +signature IFF_SOLVER = +sig + val decide : string -> bool +end + + +structure IffSolver : IFF_SOLVER = +struct + +exception FAIL + +datatype formula = Atom of string | Iff of formula * formula + +fun scan s = + let + + fun push yss = [] :: yss + + fun add x (ys :: yss) = (x :: ys) :: yss + | add _ _ = raise FAIL + + fun pop ([a, b] :: yss) = add (Iff (b, a)) yss + | pop _ = raise FAIL + + fun formula [] acc = acc + | formula ("(" :: xs) acc = formula xs (push acc) + | formula (")" :: xs) acc = formula xs (pop acc) + | formula ("<=>" :: xs) acc = formula xs acc + | formula (x :: xs) acc = formula xs (add (Atom x) acc) + + val tokens = String.tokens (fn c => c = #" ") s + in + (case formula tokens [[]] of + [[f]] => f + | _ => raise FAIL) + end + + +fun decide s = + let + fun fold_atoms f (Atom n) = f s + | fold_atoms f (Iff (p, q)) = fold_atoms f p #> fold_atoms f q + + fun collect s tab = + (case Symtab.lookup tab s of + NONE => Symtab.update (s, false) tab + | SOME v => Symtab.update (s, not v) tab) + + fun check tab = Symtab.fold (fn (_, v) => fn b => b andalso v) tab true + in + (case try scan s of + NONE => false + | SOME f => check (fold_atoms collect f Symtab.empty)) + end + +end diff -r 62fb91f86908 -r 531e453c9d67 cookbook.pdf Binary file cookbook.pdf has changed