diff -r 90189a97b3f8 -r ebbd0dd008c8 CookBook/Package/Ind_Examples.thy
--- 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)+