84 text{* |
84 text{* |
85 A second reason why your proposition may not be amenable to induction is that |
85 A second reason why your proposition may not be amenable to induction is that |
86 you want to induct on a whole term, rather than an individual variable. In |
86 you want to induct on a whole term, rather than an individual variable. In |
87 general, when inducting on some term $t$ you must rephrase the conclusion $C$ |
87 general, when inducting on some term $t$ you must rephrase the conclusion $C$ |
88 as |
88 as |
89 \[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] |
89 \begin{equation}\label{eqn:ind-over-term} |
|
90 \forall y@1 \dots y@n.~ x = t \longrightarrow C |
|
91 \end{equation} |
90 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and |
92 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and |
91 perform induction on $x$ afterwards. An example appears in |
93 perform induction on $x$ afterwards. An example appears in |
92 \S\ref{sec:complete-ind} below. |
94 \S\ref{sec:complete-ind} below. |
93 |
95 |
94 The very same problem may occur in connection with rule induction. Remember |
96 The very same problem may occur in connection with rule induction. Remember |
99 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \] |
101 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \] |
100 For an example see \S\ref{sec:CTL-revisited} below. |
102 For an example see \S\ref{sec:CTL-revisited} below. |
101 |
103 |
102 Of course, all premises that share free variables with $t$ need to be pulled into |
104 Of course, all premises that share free variables with $t$ need to be pulled into |
103 the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above. |
105 the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above. |
104 *}; |
106 |
|
107 Readers who are puzzled by the form of statement |
|
108 (\ref{eqn:ind-over-term}) above should remember that the |
|
109 transformation is only performed to permit induction. Once induction |
|
110 has been applied, the statement can be transformed back into something quite |
|
111 intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\ |
|
112 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a |
|
113 little leads to the goal |
|
114 \[ \bigwedge\vec{y}.~\forall \vec{z}.~ t(\vec{z}) \prec t(\vec{y}) \longrightarrow C(\vec{z}) |
|
115 \Longrightarrow C(\vec{y}) \] |
|
116 where the dependence of $t$ and $C$ on their free variables has been made explicit. |
|
117 Unfortunately, this induction schema cannot be expressed as a single theorem because it depends |
|
118 on the number of free variables in $t$ --- the notation $\vec{y}$ is merely an informal device. |
|
119 *} |
105 |
120 |
106 subsection{*Beyond Structural and Recursion Induction*}; |
121 subsection{*Beyond Structural and Recursion Induction*}; |
107 |
122 |
108 text{*\label{sec:complete-ind} |
123 text{*\label{sec:complete-ind} |
109 So far, inductive proofs were by structural induction for |
124 So far, inductive proofs were by structural induction for |