108 word. We start with 0 and end (at the right end) with 2. Since each move to the |
108 word. We start with 0 and end (at the right end) with 2. Since each move to the |
109 right increases or decreases the difference by 1, we must have passed through |
109 right increases or decreases the difference by 1, we must have passed through |
110 1 on our way from 0 to 2. Formally, we appeal to the following discrete |
110 1 on our way from 0 to 2. Formally, we appeal to the following discrete |
111 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val} |
111 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val} |
112 \begin{isabelle}% |
112 \begin{isabelle}% |
113 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isacharless}n{\isachardot}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k% |
113 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isacharless}n{\isachardot}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline |
|
114 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k% |
114 \end{isabelle} |
115 \end{isabelle} |
115 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers, |
116 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers, |
116 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See |
117 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See |
117 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii} |
118 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii} |
118 syntax.}, and \isa{{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}). |
119 syntax.}, and \isa{{\isadigit{1}}} is the integer 1 (see \S\ref{sec:numbers}). |