79 induction variable, you should turn the conclusion $C$ into |
79 induction variable, you should turn the conclusion $C$ into |
80 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \] |
80 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \] |
81 Additionally, you may also have to universally quantify some other variables, |
81 Additionally, you may also have to universally quantify some other variables, |
82 which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format} |
82 which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format} |
83 can remove any number of occurrences of \isa{{\isasymforall}} and |
83 can remove any number of occurrences of \isa{{\isasymforall}} and |
84 \isa{{\isasymlongrightarrow}}.% |
84 \isa{{\isasymlongrightarrow}}. |
85 \end{isamarkuptxt}% |
85 |
86 \isamarkuptrue% |
|
87 \isamarkupfalse% |
|
88 % |
|
89 \begin{isamarkuptext}% |
|
90 \index{induction!on a term}% |
86 \index{induction!on a term}% |
91 A second reason why your proposition may not be amenable to induction is that |
87 A second reason why your proposition may not be amenable to induction is that |
92 you want to induct on a complex term, rather than a variable. In |
88 you want to induct on a complex term, rather than a variable. In |
93 general, induction on a term~$t$ requires rephrasing the conclusion~$C$ |
89 general, induction on a term~$t$ requires rephrasing the conclusion~$C$ |
94 as |
90 as |
124 where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and |
120 where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and |
125 $C$ on the free variables of $t$ has been made explicit. |
121 $C$ on the free variables of $t$ has been made explicit. |
126 Unfortunately, this induction schema cannot be expressed as a |
122 Unfortunately, this induction schema cannot be expressed as a |
127 single theorem because it depends on the number of free variables in $t$ --- |
123 single theorem because it depends on the number of free variables in $t$ --- |
128 the notation $\overline{y}$ is merely an informal device.% |
124 the notation $\overline{y}$ is merely an informal device.% |
129 \end{isamarkuptext}% |
125 \end{isamarkuptxt}% |
130 \isamarkuptrue% |
126 \isamarkuptrue% |
|
127 \isamarkupfalse% |
131 % |
128 % |
132 \isamarkupsubsection{Beyond Structural and Recursion Induction% |
129 \isamarkupsubsection{Beyond Structural and Recursion Induction% |
133 } |
130 } |
134 \isamarkuptrue% |
131 \isamarkuptrue% |
135 % |
132 % |