isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:ee9d53fbb56b
+:24c68350d059
 text {*
 The user will just give a specification of inductive predicate(s) 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(s). Before we start with
-explaining all parts of the package, let us first give some examples
+explaining all parts of the package, let us first give some examples showing
-showing how to define inductive predicates and then also how
+how to define inductive predicates and then also how to generate a reasoning
-to generate a reasoning infrastructure for them. From the examples
+infrastructure for them. From the examples we will figure out a general
-we will figure out a general method for
+method for defining inductive predicates. This is usually the first step in
-defining inductive predicates.  The aim in this section is \emph{not} to
+writing a package for Isabelle. 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-implementation we will develop in later sections.
 We first consider the transitive closure of a relation @{text R}. The
 ``pencil-and-paper'' specification for the transitive closure is:
 \begin{center}\small
 @{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}
-The package has to make an appropriate definition for @{term "trcl"}.
+As mentioned before, the package has to make an appropriate definition for
-Since an inductively
+@{term "trcl"}. Since an inductively defined predicate is the least
-defined predicate is the least predicate closed under a collection of
+predicate closed under a collection of introduction rules, the predicate
-introduction rules, the predicate @{text "trcl R x y"} can be defined so
+@{text "trcl R x y"} can be defined so that it holds if and only if @{text
-that it holds if and only if @{text "P x y"} holds for every predicate
+"P x y"} holds for every predicate @{text P} closed under the rules
-@{text P} closed under the rules above. This gives rise to the definition
+above. This gives rise to the definition
 *}
 definition "trcl \<equiv>
 \<lambda>R x y. \<forall>P. (\<forall>x. P x x)
 \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"
 text {*
-We have to use the object implication @{text "\<longrightarrow>"} and object quantification
+Note we have to use the object implication @{text "\<longrightarrow>"} and object
-@{text "\<forall>"} for stating this definition (there is no other way for
+quantification @{text "\<forall>"} for stating this definition (there is no other
-definitions in HOL). However, the introduction rules and induction
+way for definitions in HOL). However, the introduction rules and induction
-principles associated with the transitive closure should use the meta-connectives,
+principles associated with the transitive closure should use the
-since they simplify the reasoning for the user.
+meta-connectives, since they simplify the reasoning for the user.
 With this definition, the proof of the induction principle for @{term trcl}
 is almost immediate. It suffices to convert all the meta-level
 connectives in the lemma to object-level connectives using the
 @{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 be constrained sufficiently.
+tactics in packages should be avoided or be constrained sufficiently.
 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} given by
 	           THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])
 done
 qed
 text {*
-The interesting lines are 7 to 15. The assumptions fall into two categories:
+The interesting lines are 7 to 15. Again, the assumptions fall into two categories:
 @{text p1} corresponds to the premise of the introduction rule; @{text "r1"}
 to @{text "r3"} come from the definition of @{text "even"}.
 In Line 13, we apply the assumption @{text "r2"} (since we prove the second
 introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if
 the second introduction rule had more premises we have to do that for all
 \begin{center}\small
 \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
 \end{center}
+The interesting point of this definition is that it contains a quantification
+that ranges only over the premise and the premise has also a precondition.
 The definition of @{text "accpart"} is:
 *}
 definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
 done
 qed
 qed
 text {*
-As you can see, there are now two subproofs. The assumptions fall again into
+As you can see, there are now two subproofs. The assumptions fall as usual into
 two categories (Lines 7 to 9). 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 second subproof (Line 14). This local assumption is
 used to solve the goal @{term "P y"} with the help of assumption @{text
 "p1"}.

changeset 295	24c68350d059
parent 244	dc95a56b1953
child 346	0fea8b7a14a1