--- a/CookBook/Package/Ind_Examples.thy Fri Feb 13 01:05:09 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy Fri Feb 13 01:05:31 2009 +0000
@@ -5,16 +5,15 @@
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 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.
- In this section, we will 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. It should be noted that
- our 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 R}. It is an inductive predicate characterized
- by the two introduction rules
+ As a first example, we consider the transitive closure of a relation @{text
+ R}. It is an inductive predicate characterized by the two introduction rules
\begin{center}
@{term[mode=Axiom] "trcl R x x"} \hspace{5mm}
@@ -37,79 +36,72 @@
\<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 {*
- where we quantify over the predicate @{text P}.
+ 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.
- Since the predicate @{term "trcl R x y"} yields an element of the type of object
- level truth values @{text bool}, the meta-level implications @{text "\<Longrightarrow>"} in the
- above introduction rules have to be converted to object-level implications
- @{text "\<longrightarrow>"}. Moreover, we use object-level universal quantifiers @{text "\<forall>"}
- rather than meta-level universal quantifiers @{text "\<And>"} for quantifying over
- the variable parameters of the introduction rules. Isabelle already offers some
- infrastructure for converting between meta-level and object-level connectives,
- which we will use later on.
-
- With this definition of the transitive closure, the proof of the (weak) induction
+ 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.
+
+ (FIXME: add linenumbers to the proof below and the text above)
*}
lemma trcl_induct:
- assumes trcl: "trcl R x y"
+ assumes asm: "trcl R x y"
shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
- apply (atomize (full))
- apply (cut_tac trcl)
- apply (unfold trcl_def)
- apply (drule spec [where x=P])
- apply assumption
- done
-(*<*)
-lemma "trcl R x x"
- apply (unfold trcl_def)
- apply (rule allI impI)+
-(*>*)
+apply(atomize (full))
+apply(cut_tac asm)
+apply(unfold trcl_def)
+apply(drule spec[where x=P])
+apply(assumption)
+done
-txt {*
-
- The above induction rule is \emph{weak} in the sense that the induction step may
- only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not
- using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule
- containing this additional assumption can be derived from the weaker one with the
- help of the introduction rules for @{text trcl}.
-
+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
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:
-
- @{subgoals [display]}
+
+*}
- The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been
- replaced by @{term "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:
- *}
+(*<*)lemma "trcl R x x"
+ apply (unfold trcl_def)
+ apply (rule allI impI)+(*>*)
+txt {* @{subgoals [display]} *}
(*<*)oops(*>*)
+text {*
+ 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:
+*}
+
+
lemma trcl_base: "trcl R x x"
- apply (unfold trcl_def)
- apply (rule allI impI)+
- apply (drule spec)
- apply assumption
- done
+apply(unfold trcl_def)
+apply(rule allI impI)+
+apply(drule spec)
+apply(assumption)
+done
-(*<*)
-lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
- apply (unfold trcl_def)
- apply (rule allI impI)+
-(*>*)
-
-txt {*
-
+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
- @{subgoals [display]}
+*}
+
+
+(*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+ 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
@@ -122,7 +114,7 @@
with higher order unification, it is advisable to provide an instantiation for the
universally quantified predicate variable in the assumption.
*}
-(*<*)oops(*>*)
+
lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
apply (unfold trcl_def)