--- a/CookBook/Package/Ind_Examples.thy Fri Feb 13 14:15:28 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy Sat Feb 14 00:11:50 2009 +0000
@@ -5,27 +5,27 @@
section{* Examples of Inductive Definitions \label{sec:ind-examples} *}
text {*
- Let us first give three examples showing how to define inductive predicates
- by hand and then how to prove characteristic properties about them, such as
- introduction rules and an induction principle. From these examples, we will
- figure out a
- general method for defining inductive predicates. The aim in this section is
- not to write proofs that are as beautiful as possible, but as close as
- possible to the ML-code producing the proofs that we will develop later.
+ Let us first give three examples showing how to define by hand inductive
+ predicates 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
+ beautiful as possible, but as close as possible to the ML-code we will
+ develop later.
+
As a first example, let us consider the transitive closure of a relation @{text
- R}. It is an inductive predicate characterized by the two introduction rules
+ R}. It is an inductive predicate characterised by the two introduction rules:
\begin{center}
- @{term[mode=Axiom] "trcl R x x"} \hspace{5mm}
- @{term[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
+ @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}
+ @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
\end{center}
- (FIXME first rule should be an ``axiom'')
-
Note that the @{text trcl} predicate has two different kinds of parameters: the
first parameter @{text R} stays \emph{fixed} throughout the definition, whereas
- the second and third parameter changes in the ``recursive call''.
+ the second and third parameter changes in the ``recursive call''. This will
+ become important later on when we deal with fixed parameters and locales.
Since an inductively defined predicate is the least predicate closed under
a collection of introduction rules, we define the predicate @{text "trcl R x y"} in
@@ -38,15 +38,16 @@
text {*
where we quantify over the predicate @{text P}. Note that we have to use the
- object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for stating
- this definition. The introduction rules and induction principles derived later
- should use the corresponding meta-connectives since they simplify the reasoning for
- the user.
+ object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for
+ stating this definition (there is no other way for definitions in
+ HOL). However, the introduction rules and induction principles derived later
+ should use the corresponding meta-connectives since they simplify the
+ reasoning for the user.
- With this definition, the proof of the induction theorem for the transitive
+ With this definition, the proof of the induction principle for the transitive
closure is almost immediate. It suffices to convert all the meta-level
- connectives in the induction rule to object-level connectives using the
- @{text atomize} proof method (Line 4), expand the definition of @{text trcl}
+ connectives in the lemma to object-level connectives using the
+ proof method @{text atomize} (Line 4), expand the definition of @{text trcl}
(Line 5 and 6), eliminate the universal quantifier contained in it (Line 7),
and then solve the goal by assumption (Line 8).
@@ -64,11 +65,10 @@
text {*
The proofs for the introduction are slightly more complicated. We need to prove
- the goals @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}.
+ 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
then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible.
- We then end up in the goal state
-
+ We then end up in the goal state:
*}
(*<*)lemma "trcl R x x"
@@ -92,9 +92,10 @@
done
text {*
- Since the second introduction rule has premises, its proof is not as easy. After unfolding
- the definitions and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we
- get the goal state
+ Since the second @{text trcl}-rule has premises, the proof of its
+ introduction rule is not as easy. After unfolding the definitions and
+ applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we get the
+ goal state:
*}
(*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
@@ -104,7 +105,7 @@
(*<*)oops(*>*)
text {*
- The third and fourth assumption corresponds to the first and second
+ The third and fourth assumption correspond to the first and second
introduction rule, respectively, whereas the first and second assumption
corresponds to the pre\-mises of the introduction rule. Since we want to prove
the second introduction rule, we apply the fourth assumption to the goal
@@ -149,14 +150,14 @@
show "P x z"
apply(rule a4[rule_format])
apply(rule a1)
- apply(rule a2 [THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4])
+ apply(rule a2[THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4])
done
qed
text {*
- It might be surprising that we are not using the automatic tactics in
- Isabelle in order to prove the lemmas we are after. After all @{text "blast"}
- would easily dispense of the lemmas.
+ It might be surprising that we are not using the automatic tactics available in
+ Isabelle for proving this lemmas. After all @{text "blast"} would easily
+ dispense of it.
*}
lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
@@ -165,22 +166,23 @@
done
text {*
- Experience has shown that it is generally a bad idea to rely heavily on @{term blast}
- and the like in automated proofs. The reason is that you do not have precise control
- over them (the user can, for example, declare new intro- or simplification rules that
- can throw automatic tactics off course) and also it is very hard to debug
- proofs involving automatic tactics. Therefore whenever possible, automatic tactics
- should be avoided or constrained.
-
+ Experience has shown that it is generally a bad idea to rely heavily on
+ @{text blast}, @{text auto} and the like in automated proofs. The reason is
+ that you do not have precise control over them (the user can, for example,
+ declare new intro- or simplification rules that can throw automatic tactics
+ off course) and also it is very hard to debug proofs involving automatic
+ tactics whenever something goes wrong. Therefore if possible, automatic
+ tactics should be avoided or sufficiently constrained.
- This method of defining inductive predicates generalises also to mutually inductive
- predicates. The next example defines the predicates @{text even} and @{text odd}
- characterised by the following rules:
+ The method of defining inductive predicates by impredicative quantification
+ also generalises to mutually inductive predicates. The next example defines
+ the predicates @{text even} and @{text odd} characterised by the following
+ rules:
\begin{center}
- @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm}
- @{term[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}
- @{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
+ @{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)"}
\end{center}
Since the predicates are mutually inductive, each definition
@@ -196,8 +198,8 @@
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
text {*
- For proving the induction rule, we use exactly the same technique as in the transitive
- closure example:
+ For proving the induction principles, we use exactly the same technique
+ as in the transitive closure example, namely:
*}
lemma even_induct:
@@ -213,9 +215,9 @@
done
text {*
- We omit the other induction rule having @{term "Q n"} as conclusion.
+ We omit the other induction principle that has @{term "Q n"} as conclusion.
The proofs of the introduction rules are also very similar to the ones in the
- @{text "trcl"}-example. We only show the proof of the second introduction rule:
+ @{text "trcl"}-example. We only show the proof of the second introduction rule.
*}
lemma evenS: "odd m \<Longrightarrow> even (Suc m)"
@@ -236,7 +238,7 @@
qed
text {*
- As a final example, we definethe accessible part of a relation @{text R} characterised
+ As a final example, we define the accessible part of a relation @{text R} characterised
by the introduction rule
\begin{center}
@@ -244,13 +246,13 @@
\end{center}
whose premise involves a universal quantifier and an implication. The
- definition of @{text accpart} is as follows:
+ definition of @{text accpart} is:
*}
definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
text {*
- The proof of the induction theorem is again straightforward.
+ The proof of the induction principle is again straightforward.
*}
lemma accpart_induct:
@@ -304,9 +306,10 @@
qed
text {*
- Now the point is to figure out what the automatic proofs should do. For
- this it might be instructive to look at the general construction principle
- of inductive definitions, which we shall do next.
+ 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. For this
+ it is instructive to look at the general construction principle
+ of inductive definitions, which we shall do in the next section.
*}
end