--- 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 \<Rightarrow> bool \<Rightarrow> 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