
diff -r 039845fc96bd -r c9ff326e3ce5 CookBook/Package/Ind_Examples.thy
--- 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




