# HG changeset patch # User paulson # Date 831635192 -7200 # Node ID 328fb06a16481f06d8e00e589eb1ee004bf6a811 # Parent 8b3de497b49dc8c794181ec0b829d7645da53627 Updated for new form of induction rules diff -r 8b3de497b49d -r 328fb06a1648 doc-src/ind-defs.tex --- a/doc-src/ind-defs.tex Thu May 09 11:45:53 1996 +0200 +++ b/doc-src/ind-defs.tex Thu May 09 11:46:32 1996 +0200 @@ -387,18 +387,21 @@ \section{Induction and coinduction rules} -Here we must consider inductive and coinductive definitions separately. -For an inductive definition, the package returns an induction rule derived -directly from the properties of least fixedpoints, as well as a modified -rule for mutual recursion and inductively defined relations. For a -coinductive definition, the package returns a basic coinduction rule. +Here we must consider inductive and coinductive definitions separately. For +an inductive definition, the package returns an induction rule derived +directly from the properties of least fixedpoints, as well as a modified rule +for mutual recursion. For a coinductive definition, the package returns a +basic coinduction rule. \subsection{The basic induction rule}\label{basic-ind-sec} The basic rule, called {\tt induct}, is appropriate in most situations. For inductive definitions, it is strong rule induction~\cite{camilleri92}; for datatype definitions (see below), it is just structural induction. -The induction rule for an inductively defined set~$R$ has the following form. +The induction rule for an inductively defined set~$R$ has the form described +below. For the time being, assume that $R$'s domain is not a Cartesian +product; inductively defined relations are treated slightly differently. + The major premise is $x\in R$. There is a minor premise for each introduction rule: \begin{itemize} @@ -427,12 +430,24 @@ for $\Fin(A)$ whose third premise discharges the extra assumption $a\not\in b$. The Isabelle/\textsc{zf} theory defines the \defn{rank} of a set~\cite[\S3.4]{paulson-set-II}, which supports well-founded induction and -recursion over datatypes. The package proves a rule for mutual induction -and inductive relations. +recursion over datatypes. The package proves a rule for mutual induction, and +modifies the default rule if~$R$ is a relation. + + +\subsection{Modified induction rules} -\subsection{Mutual induction} +If the domain of $R$ is a Cartesian product $A_1\times\cdots\times A_m$ +(however nested), then the corresponding predicate $P_i$ takes $m$ arguments. +The major premise becomes $\pair{z_1,\ldots,z_m}\in R$ instead of $x\in R$; +the conclusion becomes $P(z_1,\ldots,z_m)$. This simplifies reasoning about +inductively defined relations, eliminating the need to express properties of +$z_1$, \ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$. +Occasionally it may require you to split up the induction variable +using {\tt SigmaE} and {\tt dom\_subset}, especially if the constant {\tt + split} appears in the rule. + The mutual induction rule is called {\tt -mutual\_induct}. It differs from the basic rule in several respects: +mutual\_induct}. It differs from the basic rule in two respects: \begin{itemize} \item Instead of a single predicate~$P$, it uses $n$ predicates $P_1$, \ldots,~$P_n$: one for each recursive set. @@ -444,17 +459,12 @@ \] Proving the premises establishes $P_i(z)$ for $z\in R_i$ and $i=1$, \ldots,~$n$. - -\item If the domain of some $R_i$ is the Cartesian product - $A_1\times\cdots\times A_m$ (associated to the right), then the - corresponding predicate $P_i$ takes $m$ arguments and the corresponding - conjunct of the conclusion is -\[ (\forall z_1\ldots z_m.\pair{z_1,\ldots,z_m}\in R_i\imp P_i(z_1,\ldots,z_m)) -\] \end{itemize} -The last point above simplifies reasoning about inductively defined -relations. It eliminates the need to express properties of $z_1$, -\ldots,~$z_m$ as properties of the tuple $\pair{z_1,\ldots,z_m}$. +% +If the domain of some $R_i$ is a Cartesian product, then the mutual induction +rule is modified accordingly. The predicates are made to take $m$ separate +arguments instead of a tuple, and the quantification in the conclusion is over +the separate variables $z_1$, \ldots, $z_m$. \subsection{Coinduction}\label{coind-sec} A coinductive definition yields a primitive coinduction rule, with no @@ -581,18 +591,12 @@ The package returns introduction, elimination and induction rules for $\listn$. The basic induction rule, {\tt listn.induct}, is -\[ \infer{P(x)}{x\in\listn(A) & P(\pair{0,\Nil}) & - \infer*{P(\pair{\succ(n),\Cons(a,l)})} - {[a\in A & \pair{n,l}\in\listn(A) & P(\pair{n,l})]_{a,l,n}}} -\] -This rule requires the induction formula to be a -unary property of pairs,~$P(\pair{n,l})$. The alternative rule, {\tt -listn.mutual\_induct}, uses a binary property instead: -\[ \infer{\forall n\,l. \pair{n,l}\in\listn(A) \imp P(n,l)} - {P(0,\Nil) & - \infer*{P(\succ(n),\Cons(a,l))} +\[ \infer{P(z_1,z_2)}{\pair{z_1,z_2}\in\listn(A) & P(0,\Nil) & + \infer*{P(\succ(n),\Cons(a,l))} {[a\in A & \pair{n,l}\in\listn(A) & P(n,l)]_{a,l,n}}} \] +This rule lets the induction formula to be a +binary property of pairs, $P(n,l)$. It is now a simple matter to prove theorems about $\listn(A)$, such as \[ \forall l\in\lst(A). \pair{\length(l),\, l}\in\listn(A) \] \[ \listn(A)``\{n\} = \{l\in\lst(A). \length(l)=n\} \] @@ -682,10 +686,9 @@ \[ \{\pair{\LNil,\LNil}\} \un \{\pair{\LCons(a,l),\LCons(a,l')} . a\in A \conj \pair{l,l'}\in R\}. \] - -A pair of lazy lists are \defn{equivalent} if they belong to some bisimulation. -Equivalence can be coinductively defined as the greatest fixedpoint for the -introduction rules +A pair of lazy lists are \defn{equivalent} if they belong to some +bisimulation. Equivalence can be coinductively defined as the greatest +fixedpoint for the introduction rules \[ \pair{\LNil,\LNil} \in\lleq(A) \qquad \infer[(-)]{\pair{\LCons(a,l),\LCons(a,l')} \in\lleq(A)} {a\in A & \pair{l,l'}\in \lleq(A)} @@ -894,8 +897,8 @@ \subsection{Constructors and their domain}\label{univ-sec} A (co)inductive definition selects a subset of an existing set; a (co)datatype -definition creates a new set. The package reduces the latter to the -former. Isabelle/\textsc{zf} supplies sets having strong closure properties to serve +definition creates a new set. The package reduces the latter to the former. +Isabelle/\textsc{zf} supplies sets having strong closure properties to serve as domains for (co)inductive definitions. Isabelle/\textsc{zf} defines the Cartesian product $A\times @@ -905,7 +908,6 @@ $\pair{x_1,\ldots,x_m}$ to be the empty set~$\emptyset$ if $m=0$, simply $x_1$ if $m=1$ and $\pair{x_1,\pair{x_2,\ldots,x_m}}$ if $m\geq2$. - A datatype constructor $\Con(x_1,\ldots,x_m)$ is defined to be $h(\pair{x_1,\ldots,x_m})$, where $h$ is composed of $\Inl$ and~$\Inr$. In a mutually recursive definition, all constructors for the set~$R_i$ have @@ -1342,11 +1344,10 @@ elim}, using freeness reasoning on some underlying datatype. \end{description} -For an inductive definition, the result structure contains two induction rules, -{\tt induct} and \verb|mutual_induct|. (To save storage, the latter rule is -replaced by {\tt True} if it is not significantly different from -{\tt induct}.) For a coinductive definition, it -contains the rule \verb|coinduct|. +For an inductive definition, the result structure contains two induction +rules, {\tt induct} and \verb|mutual_induct|. (To save storage, the latter +rule is just {\tt True} unless more than one set is being defined.) For a +coinductive definition, it contains the rule \verb|coinduct|. Figure~\ref{def-result-fig} summarizes the two result signatures, specifying the types of all these components. diff -r 8b3de497b49d -r 328fb06a1648 src/ZF/IMP/Equiv.ML --- a/src/ZF/IMP/Equiv.ML Thu May 09 11:45:53 1996 +0200 +++ b/src/ZF/IMP/Equiv.ML Thu May 09 11:46:32 1996 +0200 @@ -52,7 +52,7 @@ goal Equiv.thy "!!c. -c-> sigma' ==> : C(c)"; (* start with rule induction *) -by (etac (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1); +by (etac evalc.induct 1); by (rewrite_tac (Gamma_def::C_rewrite_rules)); (* skip *)