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 \ trcl R y z \ trcl R x z"} + @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm} + @{prop[mode=Rule] "R x y \ trcl R y z \ 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 "\"} and object quantification @{text "\"} 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 "\"} and object quantification @{text "\"} 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 \ trcl R y z \ trcl R x z"}. + the facs @{prop "trcl R x x"} and @{prop "R x y \ trcl R y z \ trcl R x z"}. In order to prove the first goal, we again unfold the definition and then apply the introdution rules for @{text "\"} and @{text "\"} 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 "\"} and @{text "\"}, 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 "\"} and @{text "\"}, we get the + goal state: *} (*<*)lemma "R x y \ trcl R y z \ 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 \ trcl R y z \ 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 \ even (Suc m)"} \hspace{5mm} - @{term[mode=Rule] "even m \ odd (Suc m)"} + @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm} + @{prop[mode=Rule] "odd m \ even (Suc m)"} \hspace{5mm} + @{prop[mode=Rule] "even m \ odd (Suc m)"} \end{center} Since the predicates are mutually inductive, each definition @@ -196,8 +198,8 @@ \ (\m. P m \ Q (Suc m)) \ 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 \ 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 \ \P. (\x. (\y. R y x \ P y) \ P x) \ 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