--- a/CookBook/Appendix.thy Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Appendix.thy Sun Feb 22 03:44:03 2009 +0000
@@ -5,6 +5,12 @@
text {* \appendix *}
+text {*
+ Possible topics: translations/print translations
+
+*}
+
+
chapter {* Recipes *}
end
--- a/CookBook/Package/Ind_Interface.thy Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy Sun Feb 22 03:44:03 2009 +0000
@@ -1,15 +1,15 @@
theory Ind_Interface
-imports "../Base" "../Parsing" Simple_Inductive_Package
+imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package
begin
-section {* Parsing the Specification *}
+section {* Parsing and Typing the Specification *}
text {*
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 chose \simpleinductive{}. We want that the package can cope with
+ a new command (see Section~\ref{sec:newcommand}). As the keyword for the
+ new command we chose \simpleinductive{}. In the package we want to support
+ some ``advanced'' features: First, we want that the package can cope with
specifications inside locales. For example it should be possible to declare
-
*}
locale rel =
@@ -20,35 +20,68 @@
*}
-simple_inductive (in rel) trcl'
+simple_inductive (in rel)
+ trcl'
where
base: "trcl' x x"
| step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"
-simple_inductive (in rel) accpart'
+simple_inductive (in rel)
+ accpart'
where
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
+text {*
+ Second, we want that the user can specify fixed parameters.
+ Remember in the previous section we stated that the user can give the
+ specification for the transitive closure of a relation @{text R} as
+*}
+simple_inductive
+ trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ base: "trcl\<iota>\<iota> R x x"
+| step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"
text {*
- 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
- @{text R} is fixed throughout the specifications of @{text trcl} and @{text
- accpart}. The point is that they might be fixed in a locale and we like to
- support this. Accordingly we treat some parameters of the inductive
- definition specially; see Figure~\ref{fig:inddefsfixed} where the transitive
- closure and accessible part are defined with a fixed parameter @{text R} and
- also inside a locale fixing @{text R}.
+ Note that there is no locale given in this specification---the parameter
+ @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but
+ stays fixed throughout the specification. The problem with this way of
+ stating the specification for the transitive closure is that it derives the
+ following induction principle.
+
+ \begin{center}\small
+ \mprset{flushleft}
+ \mbox{\inferrule{
+ @{thm_style prem1 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+ @{thm_style prem2 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+ @{thm_style prem3 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
+ {@{thm_style concl trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}
+ \end{center}
+
+ But this does not correspond to the induction principle we derived by hand, which
+ was
+
+ \begin{center}\small
+ \mprset{flushleft}
+ \mbox{\inferrule{
+ @{thm_style prem1 trcl_induct[no_vars]}\\\\
+ @{thm_style prem2 trcl_induct[no_vars]}\\\\
+ @{thm_style prem3 trcl_induct[no_vars]}}
+ {@{thm_style concl trcl_induct[no_vars]}}}
+ \end{center}
+
+ The difference is that in the one derived by hand the relation @{term R} is not
+ a parameter of the proposition @{term P} to be proved and it is also not universally
+ qunatified in the second and third premise. The point is that the parameter @{term R}
+ stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''
+ argument of the transitive closure, but one that can be freely instantiated.
+ In order to recognise such parameters, we have to extend the specification
+ to include a mechanism to state fixed parameters. The user should be able
+ to write
+
*}
-text_raw {*
- \begin{figure}[p]
- \begin{isabelle}
-*}
simple_inductive
trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
where
@@ -60,18 +93,8 @@
where
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R 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}
-*}
-
text {*
- \begin{figure}[p]
+ \begin{figure}[t]
\begin{isabelle}
\railnontermfont{\rmfamily\itshape}
\railterm{simpleinductive,where,for}
@@ -95,11 +118,10 @@
*}
text {*
- For the first subtask, the syntax of the \simpleinductive{} command can be
- described by the railroad diagram in Figure~\ref{fig:railroad}. This diagram
+ This leads directly to the railroad diagram shown in
+ Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram
more or less translates directly into the parser:
-
@{ML_chunk [display,gray] parser}
which we described in Section~\ref{sec:parsingspecs}. If we feed into the
--- a/CookBook/Package/Ind_Prelims.thy Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Package/Ind_Prelims.thy Sun Feb 22 03:44:03 2009 +0000
@@ -5,11 +5,11 @@
section{* Preliminaries *}
text {*
- On the Isabelle level, the user will just give a specification of an
- inductive predicate and expects from the package to produce a convenient
- reasoning infrastructure. This infrastructure needs to be derived from the
- definition that correspond to the specified predicate. This will roughly
- mean that the package has three main parts, namely:
+ The user will just give a specification of an inductive predicate and
+ expects from the package to produce a convenient reasoning
+ infrastructure. This infrastructure needs to be derived from the definition
+ that correspond to the specified predicate. This will roughly mean that the
+ package has three main parts, namely:
\begin{itemize}
@@ -18,13 +18,14 @@
\item storing the results in the theory.
\end{itemize}
- Before we start with explaining all parts,
- let us first give three examples showing how to define inductive predicates
- by hand and then also how to prove by hand important properties about
- them. 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 beautiful as possible, but as close as possible to the ML-code
- we will develop in later sections.
+ Before we start with explaining all parts, let us first give three examples
+ showing how to define inductive predicates by hand and then also how to
+ prove by hand important properties about them. 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 beautiful as
+ possible, but as close as possible to the ML-code we will develop in later
+ sections.
+
We first consider the transitive closure of a relation @{text R}. It is
an inductive predicate characterised by the two introduction rules:
@@ -34,7 +35,7 @@
@{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
\end{center}
- In Isabelle the user will state for @{term trcl\<iota>} the specification:
+ In Isabelle, the user will state for @{term trcl\<iota>} the specification:
*}
simple_inductive
@@ -65,7 +66,7 @@
reasoning for the user.
With this definition, the proof of the induction principle for @{term trcl}
- closure is almost immediate. It suffices to convert all the meta-level
+ is almost immediate. It suffices to convert all the meta-level
connectives in the lemma to object-level connectives using the
proof method @{text atomize} (Line 4), expand the definition of @{term trcl}
(Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),
@@ -203,8 +204,8 @@
\begin{center}\small
@{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
- @{prop[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}
- @{prop[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
+ @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm}
+ @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"}
\end{center}
The user will state for this inductive definition the specification:
@@ -339,13 +340,13 @@
text {*
In Line 11, applying the assumption @{text "r1"} generates a goal state with
the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the
- proof above (Line 14). This local assumption will be used to solve
- the goal @{term "P y"} using the assumption @{text "p1"}.
+ proof above (Line 14). This local assumption is used to solve
+ the goal @{term "P y"} with the help of assumption @{text "p1"}.
The point of these examples is to get a feeling what the automatic proofs
should do in order to solve all inductive definitions we throw at them.
- This is usually the first step in writing a package.
+ This is usually the first step in writing a package. We next explain
+ the parsing and typing part of the package.
*}
-
-end
+(*<*)end(*>*)
--- a/CookBook/Package/simple_inductive_package.ML Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Sun Feb 22 03:44:03 2009 +0000
@@ -191,13 +191,13 @@
(* @end *)
(* @chunk syntax *)
-val ind_decl =
+val specification =
spec_parser >>
(fn (((loc, preds), params), specs) =>
Toplevel.local_theory loc (add_inductive preds params specs))
val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
- OuterKeyword.thy_decl ind_decl
+ OuterKeyword.thy_decl specification
(* @end *)
end;
--- a/CookBook/Tactical.thy Sat Feb 21 11:38:14 2009 +0000
+++ b/CookBook/Tactical.thy Sun Feb 22 03:44:03 2009 +0000
@@ -68,6 +68,8 @@
Isabelle Reference Manual.
\end{readmore}
+ (FIXME: what is @{ML Goal.prove_global}?)
+
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
@@ -1018,13 +1020,211 @@
@{ML ObjectLogic.rulify_tac}
- Something about simprocs.
+*}
+
+section {* Simprocs *}
+
+text {*
+ In Isabelle you can also implement custom simplification procedures, called
+ \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and
+ rewrite a term according to a given theorem. They are useful in cases where
+ a rewriting rule must be produced on ``demand'' or when rewriting by
+ simplification is too unpredictable and potentially loops.
+
+ To see how simprocs work, let us first write a simproc that just prints out
+ the pattern that triggers it and otherwise does nothing. For this
+ you can use the function:
+*}
+
+ML %linenosgray{*fun fail_sp_aux simpset redex =
+let
+ val ctxt = Simplifier.the_context simpset
+ val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))
+in
+ NONE
+end*}
+
+text {*
+ This function takes a simpset and a redex (a @{ML_type cterm}) as
+ argument. In Lines 3 and~4, we first extract the context from the given
+ simpset and then print out a message containing the redex. The function
+ returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
+ moment we are \emph{not} interested in actually rewriting anything. We want
+ that the simproc is triggered by the pattern @{term "Suc n"}. For this we
+ can add the simproc with this pattern to the current simpset as follows
+*}
+
+simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
+
+text {*
+ where the second argument specifies the pattern and the right-hand side
+ contains the code of the simproc (we have to use @{ML K} since we ignoring
+ an argument). After this setup, the simplifier is aware of
+ this simproc and you can test whether it fires with the lemma
+*}
+lemma shows "Suc 0 = 1"
+apply(simp)
+(*<*)oops(*>*)
+
+text {*
+ This will print out the message twice: once for the left-hand side and
+ once for the right-hand side. This is because during simplification the
+ simplifier will by default reduce the term @{term "1::nat"} to @{term "Suc
+ 0"}, and then the simproc ``fires'' also on that term.
+
+ We can add or delete the simproc by the usual methods. For example
+ the simproc will be deleted by the declaration:
+*}
+
+declare [[simproc del: fail_sp]]
+
+text {*
+ If you want to see what happens with just \emph{this} simproc, without any
+ interference from other rewrite rules, you can call @{text fail_sp}
+ as follows:
+*}
+
+lemma shows "Suc 0 = 1"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})
+(*<*)oops(*>*)
+
+text {*
+ (FIXME: should one use HOL-basic-ss or HOL-ss?)
+
+ Now the message shows up only once.
+
+ Setting up a simproc using the command \isacommand{setup\_simproc} will
+ always add automatically the simproc to the current simpset. If you do not
+ want this, then you have to use a slightly different method for setting
+ up the simproc. First the function @{ML fail_sp_aux} needs to be modified
+ to
+*}
+
+ML{*fun fail_sp_aux' simpset redex =
+let
+ val ctxt = Simplifier.the_context simpset
+ val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+in
+ NONE
+end*}
+
+text {*
+ Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}.
+ We can turn this function into a simproc using
*}
+ML{*val fail_sp' =
+ Simplifier.simproc_i @{theory} "fail_sp'" [@{term "Suc n"}]
+ (K fail_sp_aux')*}
+
+text {*
+ Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
+
+ Simprocs are applied from inside to outside, from left to right. You can see
+ this in the proof
+*}
+
+lemma shows "Suc (Suc 0) = (Suc 1)"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})
+(*<*)oops(*>*)
+
+text {*
+ since it prints out the sequence @{term "Suc 0"}, @{term "Suc (Suc 0)"} and
+ @{term "Suc 1"}.
+
+ To see how a simproc applies a theorem let us rewrite terms according to the
+ equation:
+*}
+
+lemma plus_one:
+ shows "Suc n \<equiv> n + 1" by simp
+
+text {*
+ The simproc expects the equation to be a meta-equation, however it can contain
+ possible preconditions (the simproc then only fires if the preconditions can be
+ solved). Let us further assume we want to only rewrite terms greater than
+ @{term "Suc 0"}. For this we can write
+*}
+
+ML{*fun plus_one_sp_aux thy ss redex =
+ case redex of
+ @{term "Suc 0"} => NONE
+ | _ => SOME @{thm plus_one}*}
+
+text {*
+ and set up the simproc as follows.
+*}
+
+ML{*val plus_one_sproc =
+ Simplifier.simproc_i @{theory} "sproc +1" [@{term "Suc n"}]
+ plus_one_sp_aux*}
+
+text {*
+ Now the simproc fires one every term of the for @{term "Suc n"}, but
+ the lemma is only applied whenever the term is not @{term "Suc 0"}. So
+ in
+*}
+
+lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
+apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sproc]) 1*})
+txt{*
+ the simproc produces the goal state
+
+ @{subgoals[display]}
+*}
+(*<*)oops(*>*)
+
+text {*
+ where the first argument is rewritten, but not the second. With @{ML
+ plus_one_sproc} you already have to be careful to not cause the simplifier
+ to loop. If we call this simproc together with the default simpset, we
+ already have a loop as it contains a rule which just undoes the rewriting of
+ the simproc.
+*}
+
+ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
+ | dest_suc_trm t = snd (HOLogic.dest_number t)*}
+
+text {* This function might raise @{ML TERM}. *}
+
+ML{*fun nat_number_sp_aux ss t =
+let
+ val ctxt = Simplifier.the_context ss
+
+ fun get_thm (t, n) =
+ let
+ val num = HOLogic.mk_number @{typ "nat"} n
+ val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t,num))
+ in
+ Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1))
+ end
+in
+ SOME (mk_meta_eq (get_thm (t,dest_suc_trm t)))
+ handle TERM _ => NONE
+end*}
+
+text {*
+ (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following loops.)
+*}
+
+ML{*val nat_number_sp =
+ Simplifier.simproc_i @{theory} "nat_number" [@{term "Suc n"}]
+ (K nat_number_sp_aux) *}
+
+lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
+ apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
+txt {*
+ @{subgoals [display]}
+ *}
+(*<*)oops(*>*)
+
+
section {* Structured Proofs *}
+text {* TBD *}
+
lemma True
proof
Binary file cookbook.pdf has changed