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