100 right increases or decreases the difference by 1, we must have passed through |
100 right increases or decreases the difference by 1, we must have passed through |
101 1 on our way from 0 to 2. Formally, we appeal to the following discrete |
101 1 on our way from 0 to 2. Formally, we appeal to the following discrete |
102 intermediate value theorem @{thm[source]nat0_intermed_int_val} |
102 intermediate value theorem @{thm[source]nat0_intermed_int_val} |
103 @{thm[display]nat0_intermed_int_val[no_vars]} |
103 @{thm[display]nat0_intermed_int_val[no_vars]} |
104 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers, |
104 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers, |
105 @{text"\<bar>.\<bar>"} is the absolute value function, and @{term"#1::int"} is the |
105 @{text"\<bar>.\<bar>"} is the absolute value function\footnote{See |
106 integer 1 (see \S\ref{sec:numbers}). |
106 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii} |
|
107 syntax.}, and @{term"#1::int"} is the integer 1 (see \S\ref{sec:numbers}). |
107 |
108 |
108 First we show that our specific function, the difference between the |
109 First we show that our specific function, the difference between the |
109 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every |
110 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every |
110 move to the right. At this point we also start generalizing from @{term a}'s |
111 move to the right. At this point we also start generalizing from @{term a}'s |
111 and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have |
112 and @{term b}'s to an arbitrary property @{term P}. Otherwise we would have |