theory Oracle+ −
imports "../Base"+ −
uses ("external_solver.ML")+ −
begin+ −
+ −
section {* Writing an Oracle\label{rec:oracle} *} + −
+ −
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, which we will slightly extend here,+ −
is given in @{ML_file "FOL/ex/Iff_Oracle.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 = {*+ −
Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac))+ −
*} "Oracle-based decision procedure for chains of equivalences"+ −
+ −
text {*+ −
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+ −