102 transformation is only performed to permit induction. Once induction |
102 transformation is only performed to permit induction. Once induction |
103 has been applied, the statement can be transformed back into something quite |
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.\ |
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 |
105 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a |
106 little leads to the goal |
106 little leads to the goal |
107 \[ \bigwedge\vec{y}.~\forall \vec{z}.~ t(\vec{z}) \prec t(\vec{y}) \longrightarrow C(\vec{z}) |
107 \[ \bigwedge\overline{y}.\ |
108 \Longrightarrow C(\vec{y}) \] |
108 \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z} |
109 where the dependence of $t$ and $C$ on their free variables has been made explicit. |
109 \ \Longrightarrow\ C\,\overline{y} \] |
110 Unfortunately, this induction schema cannot be expressed as a single theorem because it depends |
110 where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and |
111 on the number of free variables in $t$ --- the notation $\vec{y}$ is merely an informal device.% |
111 $C$ on the free variables of $t$ has been made explicit. |
|
112 Unfortunately, this induction schema cannot be expressed as a |
|
113 single theorem because it depends on the number of free variables in $t$ --- |
|
114 the notation $\overline{y}$ is merely an informal device.% |
112 \end{isamarkuptext}% |
115 \end{isamarkuptext}% |
113 % |
116 % |
114 \isamarkupsubsection{Beyond Structural and Recursion Induction% |
117 \isamarkupsubsection{Beyond Structural and Recursion Induction% |
115 } |
118 } |
116 % |
119 % |
128 induction, where you must prove $P(n)$ under the assumption that $P(m)$ |
131 induction, where you must prove $P(n)$ under the assumption that $P(m)$ |
129 holds for all $m<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}: |
132 holds for all $m<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}: |
130 \begin{isabelle}% |
133 \begin{isabelle}% |
131 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n% |
134 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n% |
132 \end{isabelle} |
135 \end{isabelle} |
133 Here is an example of its application.% |
136 As an example of its application we prove a property of the following |
|
137 function:% |
134 \end{isamarkuptext}% |
138 \end{isamarkuptext}% |
135 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
139 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
136 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
140 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
137 \begin{isamarkuptext}% |
141 \begin{isamarkuptext}% |
138 \begin{warn} |
142 \begin{warn} |