--- a/CookBook/Package/Ind_Examples.thy Wed Jan 28 06:43:51 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy Thu Jan 29 09:46:17 2009 +0000
@@ -1,58 +1,58 @@
theory Ind_Examples
-imports Main
+imports Main LaTeXsugar
begin
-section{* Examples of inductive definitions *}
+section{* Examples of Inductive Definitions \label{sec:ind-examples} *}
text {*
-\label{sec:ind-examples}
-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, which will be described in
-\S\ref{sec:ind-general-method}. This description will serve as a basis for the
-actual implementation to be developed in \S\ref{sec:ind-interface} -- \S\ref{sec:ind-proofs}.
-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 \emph{transitive closure} @{text "trcl R"}
-of a relation @{text R}. It is characterized by the following
-two introduction rules
-\[
-\begin{array}{l}
-@{term "trcl R x x"} \\
-@{term [mode=no_brackets] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
-\end{array}
-\]
-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''.
-Since an inductively defined predicate is the \emph{least} predicate closed under
-a collection of introduction rules, we define the predicate @{text "trcl R x y"} in
-such a way that it holds if and only if @{text "P x y"} holds for every predicate
-@{text P} closed under the above rules. This gives rise to a definition containing
-a universal quantifier over the predicate @{text P}:
+
+ 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
+
+ \begin{center}
+ @{term[mode=Axiom] "trcl R x x"} \hspace{5mm}
+ @{term[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> 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''.
+
+ 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
+ such a way that it holds if and only if @{text "P x y"} holds for every predicate
+ @{text P} closed under the rules 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"
+definition "trcl R x y \<equiv>
+ \<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 {*
-\noindent
-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.
+ where we quantify over the predicate @{text P}.
-With this definition of the transitive closure, the proof of the (weak) 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.
+ 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
+ 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.
*}
lemma trcl_induct:
@@ -69,54 +69,61 @@
apply (unfold trcl_def)
apply (rule allI impI)+
(*>*)
+
txt {*
-\noindent
-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}.
+
+ 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}.
-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:
-*}
+ 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:
+ *}
(*<*)oops(*>*)
+
lemma trcl_base: "trcl R x x"
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 {*
-\noindent
-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]}
-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.
+
+ 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]}
+ 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.
*}
(*<*)oops(*>*)
+
lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
apply (unfold trcl_def)
apply (rule allI impI)+
@@ -131,31 +138,32 @@
qed
text {*
-\noindent
-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:
-\[
-\begin{array}{l}
-@{term "even (0::nat)"} \\
-@{term "odd m \<Longrightarrow> even (Suc m)"} \\
-@{term "even m \<Longrightarrow> odd (Suc m)"}
-\end{array}
-\]
-Since the predicates are mutually inductive, each of the definitions contain two
-quantifiers over the predicates @{text P} and @{text Q}.
+
+ 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:
+
+ \begin{center}
+ @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm}
+ @{term[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}
+ @{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}.
*}
-definition "even \<equiv> \<lambda>n.
- \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
+definition "even n \<equiv>
+ \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
+ \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
-definition "odd \<equiv> \<lambda>n.
- \<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 n"
+definition "odd n \<equiv>
+ \<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 n"
text {*
-\noindent
-For proving the induction rule, we use exactly the same technique as in the transitive
-closure example:
+ For proving the induction rule, we use exactly the same technique as in the transitive
+ closure example:
*}
lemma even_induct:
@@ -171,13 +179,12 @@
done
text {*
-\noindent
-A similar induction rule having @{term "Q n"} as a conclusion can be proved for
-the @{text odd} predicate.
-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.
+ A similar induction rule having @{term "Q n"} as a conclusion can be proved for
+ the @{text odd} predicate.
+ 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.
*}
lemma evenS: "odd m \<Longrightarrow> even (Suc m)"
@@ -210,22 +217,23 @@
done
qed
(*>*)
+
text {*
-\noindent
-As a final example, we will consider the definition of the accessible
-part of a relation @{text R} characterized by the introduction rule
-\[
-@{term "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}
-\]
-whose premise involves a universal quantifier and an implication. The
-definition of @{text accpart} is as follows:
+ As a final example, we will consider the definition of the accessible
+ part of a relation @{text R} characterized by the introduction rule
+
+ \begin{center}
+ @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}
+ \end{center}
+
+ whose premise involves a universal quantifier and an implication. The
+ definition of @{text accpart} is as follows:
*}
-definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
+definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
text {*
-\noindent
-The proof of the induction theorem is again straightforward:
+ The proof of the induction theorem is again straightforward:
*}
lemma accpart_induct:
@@ -242,19 +250,21 @@
apply (unfold accpart_def)
apply (rule allI impI)+
(*>*)
+
txt {*
-\noindent
-Proving the introduction rule is a little more complicated, due to 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]}
-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.
+
+ Proving the introduction rule is a little more complicated, due to 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]}
+ 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)+