--- 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
--- a/CookBook/Package/Ind_Intro.thy Fri Feb 13 09:57:08 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy Fri Feb 13 14:15:28 2009 +0000
@@ -16,7 +16,7 @@
\medskip
HOL is based on just a few primitive constants, like equality and
- implication, whose properties are described by a few axioms. All other
+ implication, whose properties are described by axioms. All other
concepts, such as inductive predicates, datatypes, or recursive functions
are defined in terms of those constants, and the desired properties, for
example induction theorems, or recursion equations are derived from the
@@ -30,7 +30,7 @@
implemented.
As a running example, we have chosen a rather simple package for defining
- inductive predicates. To keep things simple, we will not use the general
+ inductive predicates. To keep things really simple, we will not use the general
Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis
of Isabelle's standard inductive definition package. Instead, we will use a
simpler \emph{impredicative} (i.e.\ involving quantification on predicate
@@ -38,7 +38,7 @@
\cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily
have a reduced functionality. It does neither support introduction rules
involving arbitrary monotone operators, nor does it prove case analysis (or
- inversion) rules. Moreover, it only proves a weaker form of the rule
+ inversion) rules. Moreover, it only proves a weaker form of the
induction theorem.
*}