diff -r 53460ac408b5 -r 5bb2d29553c2 CookBook/Package/Ind_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Package/Ind_Examples.thy	Fri Oct 10 17:13:21 2008 +0200
@@ -0,0 +1,274 @@
+theory Ind_Examples
+imports Main
+begin
+
+section{* Examples of inductive definitions *}
+
+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}:
+*}
+
+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"
+
+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.
+
+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:
+  assumes trcl: "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)+
+(*>*)
+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}.
+
+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.
+*}
+(*<*)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)+
+  proof -
+    case goal1
+    show ?case
+      apply (rule goal1(4) [rule_format])
+      apply (rule goal1(1))
+      apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp,
+	OF goal1(3-4)])
+      done
+  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}.
+*}
+
+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 "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"
+
+text {*
+\noindent
+For proving the induction rule, we use exactly the same technique as in the transitive
+closure example:
+*}
+
+lemma even_induct:
+  assumes even: "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
+
+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.
+*}
+
+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
+(*>*)
+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:
+*}
+
+definition "accpart \<equiv> \<lambda>R x. \<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:
+*}
+
+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)+
+(*>*)
+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.
+*}
+(*<*)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
+
+end