diff -r 4536782969fa -r c39f83d8daeb CookBook/Recipes/ExternalSolver.thy --- a/CookBook/Recipes/ExternalSolver.thy Sat Feb 14 16:09:04 2009 +0000 +++ b/CookBook/Recipes/ExternalSolver.thy Sun Feb 15 18:58:21 2009 +0000 @@ -1,6 +1,5 @@ theory ExternalSolver imports "../Base" -uses ("external_solver.ML") begin @@ -53,161 +52,4 @@ *} - - - - -section {* Writing an Oracle\label{rec:oracle} *} - -text {* - (FIXME: should go into a separate file) - - {\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, which we will slightly extend here, - is given in @{ML_file "FOL/ex/IffOracle.thy"}. The raw interface for adding - oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}. - \end{readmore} - - 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" - -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 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_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 {* - 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. - - 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: -*} - -oracle iff_oracle = {* fn ct => - if IffSolver.decide (translate (HOLogic.dest_Trueprop (Thm.term_of ct))) - then ct - else error "Proof failed."*} - -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{*val iff_oracle_tac = - CSUBGOAL (fn (goal, i) => - (case try iff_oracle goal of - NONE => no_tac - | SOME thm => rtac thm i))*} - -text {* - and create a new method solely based on this tactic: -*} - -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?) - - Finally, we can test our oracle to prove some theorems: -*} - -lemma "p = (p::bool)" - by iff_oracle - -lemma "p = (q = p) = q" - by iff_oracle - - -text {* -(FIXME: say something about what the proof of the oracle is ... what do you mean?) -*} - - end \ No newline at end of file