--- a/CookBook/Package/Ind_Examples.thy Fri Feb 13 09:57:08 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy Fri Feb 13 14:15:28 2009 +0000
@@ -6,13 +6,14 @@
text {*
Let us first give three examples showing how to define inductive predicates
- by hand and prove characteristic properties such as introduction rules and
- an induction rule. From these examples, we will then 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.
+ 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.
- As a first example, we consider the transitive closure of a relation @{text
+ 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
\begin{center}
@@ -38,15 +39,17 @@
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.
+ this definition. 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 of the transitive closure, the proof of the induction
- theorem 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, expand the definition of @{text trcl}, eliminate the universal quantifier
- contained in it, and then solve the goal by assumption.
+ With this definition, the proof of the induction theorem 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}
+ (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7),
+ and then solve the goal by assumption (Line 8).
- (FIXME: add linenumbers to the proof below and the text above)
*}
lemma %linenos trcl_induct:
@@ -60,16 +63,17 @@
done
text {*
- We now turn to the proofs of the introduction rules, which are slightly more complicated.
- In order to prove the first introduction rule, we again unfold the definition and
+ 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"}.
+ 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 a proof state of the following form:
+ We then end up in the goal state
*}
(*<*)lemma "trcl R x x"
- apply (unfold trcl_def)
- apply (rule allI impI)+(*>*)
+apply (unfold trcl_def)
+apply (rule allI impI)+(*>*)
txt {* @{subgoals [display]} *}
(*<*)oops(*>*)
@@ -77,10 +81,9 @@
The two assumptions correspond to the introduction rules, where @{text "trcl
R"} has been replaced by P. Thus, all we have to do is to eliminate the
universal quantifier in front of the first assumption, and then solve the
- goal by assumption:
+ goal by assumption. Thus the proof is:
*}
-
lemma trcl_base: "trcl R x x"
apply(unfold trcl_def)
apply(rule allI impI)+
@@ -89,54 +92,90 @@
done
text {*
- Since the second introduction rule has premises, its proof is not as easy as the previous
- one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"}
- and @{text "\<longrightarrow>"}, we get the proof state
+ 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
*}
-
(*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
- apply (unfold trcl_def)
- apply (rule allI impI)+(*>*)
+apply (unfold trcl_def)
+apply (rule allI impI)+(*>*)
txt {*@{subgoals [display]} *}
(*<*)oops(*>*)
text {*
- The third and fourth assumption corresponds to the first and second introduction rule,
- respectively, whereas the first and second assumption corresponds to the premises of
- the introduction rule. Since we want to prove the second introduction rule, we apply
- the fourth assumption to the goal @{term "P x z"}. In order for the assumption to
- be applicable, we have to eliminate the universal quantifiers and turn the object-level
- implications into meta-level ones. This can be accomplished using the @{text rule_format}
- attribute. Applying the assumption produces two new subgoals, which can be solved using
- the first and second assumption. The second assumption again involves a quantifier and
- implications that have to be eliminated before it can be applied. To avoid problems
- with higher order unification, it is advisable to provide an instantiation for the
- universally quantified predicate variable in the assumption.
+ The third and fourth assumption corresponds 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
+ @{term "P x z"}. In order for the assumption to be applicable as a rule, we have to
+ eliminate the universal quantifier and turn the object-level implications
+ into meta-level ones. This can be accomplished using the @{text rule_format}
+ attribute. Applying the assumption produces the two new subgoals
+*}
+
+(*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+apply (unfold trcl_def)
+apply (rule allI impI)+
+proof -
+ case (goal1 P)
+ have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
+ show ?case
+ apply (rule a4[rule_format])(*>*)
+txt {*@{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {*
+ which can be
+ solved using the first and second assumption. The second assumption again
+ involves a quantifier and an implications that have to be eliminated before it
+ can be applied. To avoid potential problems with higher-order unification,
+ we should explcitly instantiate the universally quantified
+ predicate variable to @{text "P"} and also match explicitly the implications
+ with the the third and fourth assumption. This gives the proof:
*}
lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
- apply (unfold trcl_def)
- apply (rule allI impI)+
- proof -
- case (goal1 P)
- have g1: "R x y" by fact
- have g2: "\<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 y z" by fact
- have g3: "\<forall>x. P x x" by fact
- have g4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
- show ?case
- apply (rule g4 [rule_format])
- apply (rule g1)
- apply (rule g2 [THEN spec [where x=P], THEN mp, THEN mp, OF g3, OF g4])
- done
- qed
+apply(unfold trcl_def)
+apply(rule allI impI)+
+proof -
+ case (goal1 P)
+ have a1: "R x y" by fact
+ have a2: "\<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 y z" by fact
+ have a3: "\<forall>x. P x x" by fact
+ have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
+ 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])
+ 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.
+*}
- This method of defining inductive predicates easily generalizes to mutually inductive
- predicates, like the predicates @{text even} and @{text odd} characterized by the
- following introduction rules:
+lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+apply(unfold trcl_def)
+apply(blast)
+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.
+
+
+ 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:
\begin{center}
@{term[mode=Axiom] "even (0::nat)"} \hspace{5mm}
@@ -144,8 +183,8 @@
@{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
\end{center}
- Since the predicates are mutually inductive, each of the definitions contain two
- quantifiers over the predicates @{text P} and @{text Q}.
+ Since the predicates are mutually inductive, each definition
+ quantifies over both predicates, below named @{text P} and @{text Q}.
*}
definition "even n \<equiv>
@@ -162,60 +201,43 @@
*}
lemma even_induct:
- assumes even: "even n"
+ assumes asm: "even n"
shows "P 0 \<Longrightarrow>
(\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
- apply (atomize (full))
- apply (cut_tac even)
- apply (unfold even_def)
- apply (drule spec [where x=P])
- apply (drule spec [where x=Q])
- apply assumption
- done
+apply(atomize (full))
+apply(cut_tac asm)
+apply(unfold even_def)
+apply(drule spec[where x=P])
+apply(drule spec[where x=Q])
+apply(assumption)
+done
text {*
- A similar induction rule having @{term "Q n"} as a conclusion can be proved for
- the @{text odd} predicate.
+ We omit the other induction rule having @{term "Q n"} as conclusion.
The proofs of the introduction rules are also very similar to the ones in the
- previous example. We only show the proof of the second introduction rule,
- since it is almost the same as the one for the third introduction rule,
- and the proof of the first rule is trivial.
+ @{text "trcl"}-example. We only show the proof of the second introduction rule:
*}
lemma evenS: "odd m \<Longrightarrow> even (Suc m)"
- apply (unfold odd_def even_def)
- apply (rule allI impI)+
- proof -
- case goal1
- show ?case
- apply (rule goal1(3) [rule_format])
- apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],
- THEN mp, THEN mp, THEN mp, OF goal1(2-4)])
- done
- qed
-(*<*)
-lemma even0: "even 0"
- apply (unfold even_def)
- apply (rule allI impI)+
- apply assumption
- done
-
-lemma oddS: "even m \<Longrightarrow> odd (Suc m)"
- apply (unfold odd_def even_def)
- apply (rule allI impI)+
- proof -
- case goal1
- show ?case
- apply (rule goal1(4) [rule_format])
- apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],
- THEN mp, THEN mp, THEN mp, OF goal1(2-4)])
- done
- qed
-(*>*)
+apply (unfold odd_def even_def)
+apply (rule allI impI)+
+proof -
+ case (goal1 P)
+ have a1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
+ \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
+ have a2: "P 0" by fact
+ have a3: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact
+ have a4: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact
+ show "P (Suc m)"
+ apply(rule a3[rule_format])
+ apply(rule a1[THEN spec[where x=P], THEN spec[where x=Q],
+ THEN mp, THEN mp, THEN mp, OF a2, OF a3, OF a4])
+ done
+qed
text {*
- As a final example, we will consider the definition of the accessible
- part of a relation @{text R} characterized by the introduction rule
+ As a final example, we definethe accessible part of a relation @{text R} characterised
+ by the introduction rule
\begin{center}
@{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}
@@ -228,53 +250,63 @@
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 theorem is again straightforward.
*}
lemma accpart_induct:
- assumes acc: "accpart R x"
- shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
- apply (atomize (full))
- apply (cut_tac acc)
- apply (unfold accpart_def)
- apply (drule spec [where x=P])
- apply assumption
- done
-(*<*)
-lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
- apply (unfold accpart_def)
- apply (rule allI impI)+
-(*>*)
+ assumes asm: "accpart R x"
+ shows "(\<And>x. (\<forall>y. R y x \<longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
+apply(atomize (full))
+apply(cut_tac asm)
+apply(unfold accpart_def)
+apply(drule spec[where x=P])
+apply(assumption)
+done
-txt {*
-
- Proving the introduction rule is a little more complicated, due to the quantifier
+text {*
+ Proving the introduction rule is a little more complicated, because the quantifier
and the implication in the premise. We first convert the meta-level universal quantifier
and implication to their object-level counterparts. Unfolding the definition of
@{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
yields the following proof state:
- @{subgoals [display]}
+*}
+
+(*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+apply (unfold accpart_def)
+apply (rule allI impI)+(*>*)
+txt {* @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {*
Applying the second assumption produces a proof state with the new local assumption
@{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the
first assumption.
*}
-(*<*)oops(*>*)
-lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
- apply (unfold accpart_def)
- apply (rule allI impI)+
- proof -
- case goal1
- note goal1' = this
- show ?case
- apply (rule goal1'(2) [rule_format])
- proof -
- case goal1
- show ?case
- apply (rule goal1'(1) [OF goal1, THEN spec [where x=P],
- THEN mp, OF goal1'(2)])
- done
- qed
- qed
+lemma %small accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+apply (unfold accpart_def)
+apply (rule allI impI)+
+proof -
+ case (goal1 P)
+ have a1: "\<forall>y. R y x \<longrightarrow>
+ (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact
+ have a2: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
+ show "P x"
+ apply(rule a2[rule_format])
+ proof -
+ case (goal1 y)
+ have a3: "R y x" by fact
+ show "P y"
+ apply(rule a1[THEN spec[where x=y], THEN mp, OF a3,
+ THEN spec[where x=P], THEN mp, OF a2])
+ done
+ qed
+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.
+*}
end