--- a/CookBook/FirstSteps.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/FirstSteps.thy Sun Feb 15 18:58:21 2009 +0000
@@ -521,6 +521,7 @@
@{ML_file "Pure/thm.ML"}.
\end{readmore}
+ (FIXME: how to add case-names to goal states)
*}
section {* Theories and Local Theories *}
--- a/CookBook/Intro.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Intro.thy Sun Feb 15 18:58:21 2009 +0000
@@ -118,8 +118,8 @@
\begin{itemize}
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
\simpleinductive-package and the code for the @{text "chunk"}-antiquotation. He also wrote the first
- version of the chapter describing the package and has generally be
- helpful beyond measure with answering questions about Isabelle.
+ version of the chapter describing the package and has be
+ helpful \emph{beyond measure} with answering questions about Isabelle.
\item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout},
\ref{rec:config}, \ref{rec:storingdata}, \ref{rec:external} and \ref{rec:oracle}.
--- a/CookBook/Package/Ind_Examples.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy Sun Feb 15 18:58:21 2009 +0000
@@ -5,8 +5,8 @@
section{* Examples of Inductive Definitions \label{sec:ind-examples} *}
text {*
- Let us first give three examples showing how to define by hand inductive
- predicates and then also how to prove by hand characteristic properties
+ Let us first give three examples showing how to define inductive
+ predicates by hand and then also how to prove by hand characteristic properties
about them, such as introduction rules and induction principles. From
these examples, we will figure out a general method for defining inductive
predicates. The aim in this section is \emph{not} to write proofs that are as
@@ -66,7 +66,7 @@
text {*
The proofs for the introduction are slightly more complicated. We need to prove
the facs @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}.
- In order to prove the first goal, we again unfold the definition and
+ In order to prove the first fact, we again unfold the definition and
then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible.
We then end up in the goal state:
*}
@@ -270,7 +270,7 @@
and the implication in the premise. We first convert the meta-level universal quantifier
and implication to their object-level counterparts. Unfolding the definition of
@{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
- yields the following proof state:
+ yields the following goal state:
*}
(*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
@@ -280,7 +280,7 @@
(*<*)oops(*>*)
text {*
- Applying the second assumption produces a proof state with the new local assumption
+ Applying the second assumption produces a goal state with the new local assumption
@{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the
first assumption.
*}
--- a/CookBook/Package/Ind_General_Scheme.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/Ind_General_Scheme.thy Sun Feb 15 18:58:21 2009 +0000
@@ -7,11 +7,9 @@
text {*
Before we start with the implementation, it is useful to describe the general
- form of inductive definitions that our package should accept. We closely follow
- the notation for inductive definitions introduced by Schwichtenberg
- \cite{Schwichtenberg-MLCF} for the Minlog system.
- Let $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be
- parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have
+ form of inductive definitions that our package should accept.
+ Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be
+ some fixed parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have
the form
\[
@@ -24,8 +22,8 @@
Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure
that all occurrences of the predicates in the premises of the introduction rules are
\emph{strictly positive}. This condition guarantees the existence of predicates
- that are closed under the introduction rules shown above. The inductive predicates
- $R_1,\ldots,R_n$ can then be defined as follows:
+ that are closed under the introduction rules shown above. Then the definitions of the
+ inductive predicates $R_1,\ldots,R_n$ is:
\[
\begin{array}{l@ {\qquad}l}
--- a/CookBook/Package/Ind_Interface.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy Sun Feb 15 18:58:21 2009 +0000
@@ -1,5 +1,5 @@
theory Ind_Interface
-imports "../Base" Simple_Inductive_Package
+imports "../Base" "../Parsing" Simple_Inductive_Package
begin
section {* The Interface \label{sec:ind-interface} *}
@@ -7,10 +7,10 @@
text {*
The purpose of the package we show next is that the user just specifies the
inductive predicate by stating some introduction rules and then the packages
- makes the equivalent definition and derives from it useful properties.
+ makes the equivalent definition and derives from it the needed properties.
To be able to write down the specification in Isabelle, we have to introduce
a new command (see Section~\ref{sec:newcommand}). As the keyword for the new
- command we use \simpleinductive{}. The specifications corresponding to our
+ command we chose \simpleinductive{}. The specifications corresponding to our
examples described earlier are:
*}
@@ -33,7 +33,8 @@
accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
text {*
- We expect a constant (or constants) with possible typing annotations and a
+ After the keyword we expect a constant (or constants) with possible typing
+ annotations and a
list of introduction rules. While these specifications are all
straightforward, there is a technicality we like to deal with to do with
fixed parameters and locales. Remember we pointed out that the parameter
@@ -46,8 +47,8 @@
*}
text_raw {*
-\begin{figure}[p]
-\begin{isabelle}
+ \begin{figure}[p]
+ \begin{isabelle}
*}
simple_inductive
trcl' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -72,18 +73,34 @@
where
accpartI: "(\<forall>y. R y x \<longrightarrow> accpart'' y) \<Longrightarrow> accpart'' x"
text_raw {*
-\end{isabelle}
-\caption{The first definition is for the transitive closure where the
-relation @{text R} is explicitly fixed. Simiraly the second definition
-of the accessible part of the relation @{text R}. The last two definitions
-specify the same inductive predicates, but this time defined inside
-a locale.\label{fig:inddefsfixed}}
-\end{figure}
+ \end{isabelle}
+ \caption{The first definition is for the transitive closure where the
+ relation @{text R} is explicitly fixed. Simiraly the second definition
+ of the accessible part of the relation @{text R}. The last two definitions
+ specify the same inductive predicates, but this time defined inside
+ a locale.\label{fig:inddefsfixed}}
+ \end{figure}
*}
text {*
-\begin{figure}[p]
-\begin{isabelle}
+ From a high-level perspective the package consists of 6 subtasks:
+
+ \begin{itemize}
+ \item reading the various parts of specification (i.e.~parser),
+ \item transforming the parser outut into an internal
+ (typed) datastructure,
+ \item making the definitions,
+ \item deriving the induction principles,
+ \item deriving the introduction rules, and
+ \item storing the results in the given theory to be visible
+ to the user.
+ \end{itemize}
+
+*}
+
+text {*
+ \begin{figure}[p]
+ \begin{isabelle}
\railnontermfont{\rmfamily\itshape}
\railterm{simpleinductive,where,for}
\railalias{simpleinductive}{\simpleinductive{}}
@@ -94,37 +111,102 @@
(where (thmdecl? prop + '|'))?
;
\end{rail}
-\end{isabelle}
-\caption{A railroad diagram describing the syntax of \simpleinductive{}.
-The \emph{target} indicates an optional locale; the \emph{fixes} are an
-\isacommand{and}-separated list of names for the inductive predicates (they
-can also contain typing- and syntax anotations); similarly the \emph{fixes}
-after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a
-introduction rule with an optional theorem declaration (\emph{thmdecl}).
-\label{fig:railroad}}
-\end{figure}
+ \end{isabelle}
+ \caption{A railroad diagram describing the syntax of \simpleinductive{}.
+ The \emph{target} indicates an optional locale; the \emph{fixes} are an
+ \isacommand{and}-separated list of names for the inductive predicates (they
+ can also contain typing- and syntax anotations); similarly the \emph{fixes}
+ after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a
+ introduction rule with an optional theorem declaration (\emph{thmdecl}).
+ \label{fig:railroad}}
+ \end{figure}
*}
text {*
- The syntax of the \simpleinductive{} command can be described by the
- railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less
- translates directly into the parser:
+ For the first subtask, the syntax of the \simpleinductive{} command can be
+ described by the railroad diagram in Figure~\ref{fig:railroad}. This diagram
+ more or less translates directly into the parser:
+
@{ML_chunk [display,gray] parser}
- which we also described in Section~\ref{sec:parsingspecs}. Its return value
- of this parser is a locale, the predicates, parameters and specifications of
- the introduction rules. This is all the information we need to call the package.
+ which we described in Section~\ref{sec:parsingspecs}. If we feed into the
+ parser the string (which corresponds to our definition of @{term even} and
+ @{term odd}):
+
+ @{ML_response [display,gray]
+"let
+ val input = filtered_input
+ (\"even and odd \" ^
+ \"where \" ^
+ \" even0[intro]: \\\"even 0\\\" \" ^
+ \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
+ \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+in
+ parse spec_parser input
+end"
+"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
+ [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
+ ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
+ ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
+*}
+
+
+text {*
+ then we get back a locale (in this case @{ML NONE}), the predicates (with type
+ and syntax annotations), the parameters (similar as the predicates) and
+ the specifications of the introduction rules.
+
+
+
+ This is all the information we
+ need for calling the package and setting up the keyword. The latter is
+ done in Lines 6 and 7 in the code below.
@{ML_chunk [display,gray,linenos] syntax}
+
+ We call @{ML OuterSyntax.command} with the kind-indicator @{ML
+ OuterKeyword.thy_decl} since the package does not need to open up any goal
+ state (see Section~\ref{sec:newcommand}). Note that the predicates and
+ parameters are at the moment only some ``naked'' variables: they have no
+ type yet (even if we annotate them with types) and they are also no defined
+ constants yet (which the predicates will eventually be). In Lines 1 to 4 we
+ gather the information from the parser to be processed further. The locale
+ is passed as argument to the function @{ML
+ Toplevel.local_theory}.\footnote{FIXME Is this already described?} The other
+ arguments, i.e.~the predicates, parameters and intro rule specifications,
+ are passed to the function @{ML add_inductive in SimpleInductivePackage}
+ (Line 4).
- The locale is passed as argument to the function
- @{ML Toplevel.local_theory}.\footnote{FIXME Is this already described?} The
- other arguments, i.e.~the predicates, parameters and specifications, are passed
- to the function @{ML add_inductive in SimpleInductivePackage} (Line 4). The
- actual command is defined in Lines 6 and 7. We called @{ML OuterSyntax.command}
- with the kind-indicator @{ML OuterKeyword.thy_decl} since the package does
- not need to open up any goal state (see Section~\ref{sec:newcommand}).
+ We now come to the second subtask of the package, namely transforming the
+ parser output into some internal datastructures that can be processed further.
+ Remember that at the moment the introduction rules are just strings, and even
+ if the predicates and parameters can contain some typing annotations, they
+ are not yet in any way reflected in the introduction rules. So the task of
+ @{ML add_inductive in SimpleInductivePackage} is to transform the strings
+ into properly typed terms. For this it can use the function
+ @{ML read_specification in Specification}. This function takes some constants
+ with possible typing annotations and some rule specifications and attempts to
+ find a type according to the given type constraints and the type constraints
+ by the surrounding (local theory). However this function is a bit
+ too general for our purposes: we want that each introduction rule has only
+ name (for example @{text even0} or @{text evenS}), if a name is given at all.
+ The function @{ML read_specification in Specification} however allows more
+ than one rule. Since it is quite convenient to rely on this function (instead of
+ building your own) we just quick ly write a wrapper function that translates
+ between our specific format and the general format expected by
+ @{ML read_specification in Specification}. The code of this wrapper is as follows:
+
+ @{ML_chunk [display,gray,linenos] read_specification}
+
+ It takes a list of constants, a list of rule specifications and a local theory
+ as input. Does the transformation of the rule specifications in Line 3; calls
+ the function and transforms the now typed rule specifications back into our
+ format and returns the type parameter and typed rule specifications.
+
+
+ @{ML_chunk [display,gray,linenos] add_inductive}
+
In order to add a new inductive predicate to a theory with the help of our
package, the user must \emph{invoke} it. For every package, there are
@@ -136,7 +218,7 @@
actually make the definition, the type and introduction rules have to be
parsed. In contrast, internal invocation means that the package is called by
some other package. For example, the function definition package
- \cite{Krauss-IJCAR06} calls the inductive definition package to define the
+ calls the inductive definition package to define the
graph of the function. However, it is not a good idea for the function
definition package to pass the introduction rules for the function graph to
the inductive definition package as strings. In this case, it is better to
--- a/CookBook/Package/Ind_Intro.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy Sun Feb 15 18:58:21 2009 +0000
@@ -17,9 +17,9 @@
\medskip
HOL is based on just a few primitive constants, like equality and
implication, whose properties are described by axioms. All other concepts,
- such as inductive predicates, datatypes, or recursive functions are defined
+ such as inductive predicates, datatypes, or recursive functions have to be defined
in terms of those constants, and the desired properties, for example
- induction theorems, or recursion equations are derived from the definitions
+ induction theorems, or recursion equations have to be derived from the definitions
by a formal proof. Since it would be very tedious for a user to define
complex inductive predicates or datatypes ``by hand'' just using the
primitive operators of higher order logic, \emph{definitional packages} have
--- a/CookBook/Package/simple_inductive_package.ML Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Sun Feb 15 18:58:21 2009 +0000
@@ -155,16 +155,19 @@
end
(* @end *)
-(* @chunk add_inductive *)
+(* @chunk read_specification *)
fun read_specification' vars specs lthy =
let
val specs' = map (fn (a, s) => [(a, [s])]) specs
- val ((varst, specst), _) = Specification.read_specification vars specs' lthy
+ val ((varst, specst), _) =
+ Specification.read_specification vars specs' lthy
val specst' = map (apsnd the_single) specst
in
(varst, specst')
end
+(* @end *)
+(* @chunk add_inductive *)
fun add_inductive preds params specs lthy =
let
val (vars, specs') = read_specification' (preds @ params) specs lthy;
@@ -176,7 +179,7 @@
(* @end *)
(* @chunk parser *)
-val parser =
+val spec_parser =
OuterParse.opt_target --
OuterParse.fixes --
OuterParse.for_fixes --
@@ -189,7 +192,7 @@
(* @chunk syntax *)
val ind_decl =
- parser >>
+ spec_parser >>
(fn (((loc, preds), params), specs) =>
Toplevel.local_theory loc (add_inductive preds params specs))
--- a/CookBook/Parsing.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Parsing.thy Sun Feb 15 18:58:21 2009 +0000
@@ -190,7 +190,7 @@
"Exception ABORT raised"}
then the parsing aborts and the error message @{text "foo"} is printed. In order to
- see the error message properly, we need to prefix the parser with the function
+ see the error message properly, you need to prefix the parser with the function
@{ML "Scan.error"}. For example:
@{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
@@ -599,6 +599,16 @@
(FIXME: why is intro, elim and dest treated differently from bar?)
*}
+ML{*val spec_parser =
+ OuterParse.opt_target --
+ OuterParse.fixes --
+ OuterParse.for_fixes --
+ Scan.optional
+ (OuterParse.$$$ "where" |--
+ OuterParse.!!!
+ (OuterParse.enum1 "|"
+ (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+
text {*
@{ML_response [display,gray]
"let
@@ -608,18 +618,8 @@
\" even0[intro]: \\\"even 0\\\" \" ^
\"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
\"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
-
- val parser =
- OuterParse.opt_target --
- OuterParse.fixes --
- OuterParse.for_fixes --
- Scan.optional
- (OuterParse.$$$ \"where\" |--
- OuterParse.!!!
- (OuterParse.enum1 \"|\"
- (SpecParse.opt_thm_name \":\" -- OuterParse.prop))) []
in
- parse parser input
+ parse spec_parser input
end"
"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
[((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
--- a/CookBook/ROOT.ML Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/ROOT.ML Sun Feb 15 18:58:21 2009 +0000
@@ -22,6 +22,7 @@
use_thy "Recipes/Config";
use_thy "Recipes/StoringData";
use_thy "Recipes/ExternalSolver";
+use_thy "Recipes/Oracle";
use_thy "Solutions";
use_thy "Readme";
--- 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/Oracle.thy Sun Feb 15 18:58:21 2009 +0000
@@ -0,0 +1,157 @@
+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/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
--- a/CookBook/Tactical.thy Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Tactical.thy Sun Feb 15 18:58:21 2009 +0000
@@ -56,7 +56,7 @@
@{text xs} that will be generalised once the goal is proved (in our case
@{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
it can make use of the local assumptions (there are none in this example).
- The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to
+ The functions @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond to
@{text erule}, @{text rule} and @{text assumption}, respectively.
The operator @{ML THEN} strings the tactics together.
@@ -68,7 +68,7 @@
Isabelle Reference Manual.
\end{readmore}
- Note that in the code above we used antiquotations for referencing the theorems. Many theorems
+ Note that in the code above we use antiquotations for referencing the theorems. Many theorems
also have ML-bindings with the same name. Therefore, we could also just have
written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
the theorem dynamically using the function @{ML thm}; for example
@@ -309,7 +309,7 @@
form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
"(C)"}. Since the goal @{term C} can potentially be an implication, there is
a ``protector'' wrapped around it (in from of an outermost constant @{text
- "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal; however this constant
+ "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
is invisible in the figure). This prevents that premises of @{text C} are
mis-interpreted as open subgoals. While tactics can operate on the subgoals
(the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
@@ -952,7 +952,7 @@
text {*
is completely analysed according to the theorems we chose to
- include in @{ML select_tac}.
+ include in @{ML select_tac'}.
Recall that tactics produce a lazy sequence of successor goal states. These
states can be explored using the command \isacommand{back}. For example
@@ -1015,8 +1015,13 @@
text {*
@{ML rewrite_goals_tac}
+
@{ML ObjectLogic.full_atomize_tac}
+
@{ML ObjectLogic.rulify_tac}
+
+ Something about simprocs.
+
*}
Binary file cookbook.pdf has changed