38 Since \isa{hd} and \isa{last} return the first and last element of a |
38 Since \isa{hd} and \isa{last} return the first and last element of a |
39 non-empty list, this lemma looks easy to prove:% |
39 non-empty list, this lemma looks easy to prove:% |
40 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
41 \isamarkuptrue% |
41 \isamarkuptrue% |
42 \isacommand{lemma}\isamarkupfalse% |
42 \isacommand{lemma}\isamarkupfalse% |
43 \ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}\isanewline |
43 \ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
44 % |
44 % |
45 \isadelimproof |
45 \isadelimproof |
46 % |
46 % |
47 \endisadelimproof |
47 \endisadelimproof |
48 % |
48 % |
49 \isatagproof |
49 \isatagproof |
50 \isacommand{apply}\isamarkupfalse% |
50 \isacommand{apply}\isamarkupfalse% |
51 {\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}% |
51 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}% |
52 \begin{isamarkuptxt}% |
52 \begin{isamarkuptxt}% |
53 \noindent |
53 \noindent |
54 But induction produces the warning |
54 But induction produces the warning |
55 \begin{quote}\tt |
55 \begin{quote}\tt |
56 Induction variable occurs also among premises! |
56 Induction variable occurs also among premises! |
57 \end{quote} |
57 \end{quote} |
58 and leads to the base case |
58 and leads to the base case |
59 \begin{isabelle}% |
59 \begin{isabelle}% |
60 \ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% |
60 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}% |
61 \end{isabelle} |
61 \end{isabelle} |
62 Simplification reduces the base case to this: |
62 Simplification reduces the base case to this: |
63 \begin{isabelle} |
63 \begin{isabelle} |
64 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] |
64 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] |
65 \end{isabelle} |
65 \end{isabelle} |
66 We cannot prove this equality because we do not know what \isa{hd} and |
66 We cannot prove this equality because we do not know what \isa{hd} and |
67 \isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}. |
67 \isa{last} return when applied to \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}. |
68 |
68 |
69 We should not have ignored the warning. Because the induction |
69 We should not have ignored the warning. Because the induction |
70 formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises. |
70 formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises. |
71 Thus the case that should have been trivial |
71 Thus the case that should have been trivial |
72 becomes unprovable. Fortunately, the solution is easy:\footnote{A similar |
72 becomes unprovable. Fortunately, the solution is easy:\footnote{A similar |
73 heuristic applies to rule inductions; see \S\ref{sec:rtc}.} |
73 heuristic applies to rule inductions; see \S\ref{sec:rtc}.} |
74 \begin{quote} |
74 \begin{quote} |
75 \emph{Pull all occurrences of the induction variable into the conclusion |
75 \emph{Pull all occurrences of the induction variable into the conclusion |
76 using \isa{{\isasymlongrightarrow}}.} |
76 using \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}.} |
77 \end{quote} |
77 \end{quote} |
78 Thus we should state the lemma as an ordinary |
78 Thus we should state the lemma as an ordinary |
79 implication~(\isa{{\isasymlongrightarrow}}), letting |
79 implication~(\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}), letting |
80 \attrdx{rule_format} (\S\ref{sec:forward}) convert the |
80 \attrdx{rule_format} (\S\ref{sec:forward}) convert the |
81 result to the usual \isa{{\isasymLongrightarrow}} form:% |
81 result to the usual \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} form:% |
82 \end{isamarkuptxt}% |
82 \end{isamarkuptxt}% |
83 \isamarkuptrue% |
83 \isamarkuptrue% |
84 % |
84 % |
85 \endisatagproof |
85 \endisatagproof |
86 {\isafoldproof}% |
86 {\isafoldproof}% |
87 % |
87 % |
88 \isadelimproof |
88 \isadelimproof |
89 % |
89 % |
90 \endisadelimproof |
90 \endisadelimproof |
91 \isacommand{lemma}\isamarkupfalse% |
91 \isacommand{lemma}\isamarkupfalse% |
92 \ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequoteclose}% |
92 \ hd{\isaliteral{5F}{\isacharunderscore}}rev\ {\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ xs{\isaliteral{22}{\isachardoublequoteclose}}% |
93 \isadelimproof |
93 \isadelimproof |
94 % |
94 % |
95 \endisadelimproof |
95 \endisadelimproof |
96 % |
96 % |
97 \isatagproof |
97 \isatagproof |
98 % |
98 % |
99 \begin{isamarkuptxt}% |
99 \begin{isamarkuptxt}% |
100 \noindent |
100 \noindent |
101 This time, induction leaves us with a trivial base case: |
101 This time, induction leaves us with a trivial base case: |
102 \begin{isabelle}% |
102 \begin{isabelle}% |
103 \ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% |
103 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ hd\ {\isaliteral{28}{\isacharparenleft}}rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}% |
104 \end{isabelle} |
104 \end{isabelle} |
105 And \isa{auto} completes the proof. |
105 And \isa{auto} completes the proof. |
106 |
106 |
107 If there are multiple premises $A@1$, \dots, $A@n$ containing the |
107 If there are multiple premises $A@1$, \dots, $A@n$ containing the |
108 induction variable, you should turn the conclusion $C$ into |
108 induction variable, you should turn the conclusion $C$ into |
109 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \] |
109 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \] |
110 Additionally, you may also have to universally quantify some other variables, |
110 Additionally, you may also have to universally quantify some other variables, |
111 which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format} |
111 which can yield a fairly complex conclusion. However, \isa{rule{\isaliteral{5F}{\isacharunderscore}}format} |
112 can remove any number of occurrences of \isa{{\isasymforall}} and |
112 can remove any number of occurrences of \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}} and |
113 \isa{{\isasymlongrightarrow}}. |
113 \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}. |
114 |
114 |
115 \index{induction!on a term}% |
115 \index{induction!on a term}% |
116 A second reason why your proposition may not be amenable to induction is that |
116 A second reason why your proposition may not be amenable to induction is that |
117 you want to induct on a complex term, rather than a variable. In |
117 you want to induct on a complex term, rather than a variable. In |
118 general, induction on a term~$t$ requires rephrasing the conclusion~$C$ |
118 general, induction on a term~$t$ requires rephrasing the conclusion~$C$ |
131 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as |
131 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as |
132 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \] |
132 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \] |
133 For an example see \S\ref{sec:CTL-revisited} below. |
133 For an example see \S\ref{sec:CTL-revisited} below. |
134 |
134 |
135 Of course, all premises that share free variables with $t$ need to be pulled into |
135 Of course, all premises that share free variables with $t$ need to be pulled into |
136 the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above. |
136 the conclusion as well, under the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}, again using \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} as shown above. |
137 |
137 |
138 Readers who are puzzled by the form of statement |
138 Readers who are puzzled by the form of statement |
139 (\ref{eqn:ind-over-term}) above should remember that the |
139 (\ref{eqn:ind-over-term}) above should remember that the |
140 transformation is only performed to permit induction. Once induction |
140 transformation is only performed to permit induction. Once induction |
141 has been applied, the statement can be transformed back into something quite |
141 has been applied, the statement can be transformed back into something quite |
177 usually known as mathematical induction. There is also \textbf{complete} |
177 usually known as mathematical induction. There is also \textbf{complete} |
178 \index{induction!complete}% |
178 \index{induction!complete}% |
179 induction, where you prove $P(n)$ under the assumption that $P(m)$ |
179 induction, where you prove $P(n)$ under the assumption that $P(m)$ |
180 holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}: |
180 holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}: |
181 \begin{isabelle}% |
181 \begin{isabelle}% |
182 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n% |
182 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n% |
183 \end{isabelle} |
183 \end{isabelle} |
184 As an application, we prove a property of the following |
184 As an application, we prove a property of the following |
185 function:% |
185 function:% |
186 \end{isamarkuptext}% |
186 \end{isamarkuptext}% |
187 \isamarkuptrue% |
187 \isamarkuptrue% |
188 \isacommand{consts}\isamarkupfalse% |
188 \isacommand{consts}\isamarkupfalse% |
189 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
189 \ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
190 \isacommand{axioms}\isamarkupfalse% |
190 \isacommand{axioms}\isamarkupfalse% |
191 \ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequoteopen}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
191 \ f{\isaliteral{5F}{\isacharunderscore}}ax{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f{\isaliteral{28}{\isacharparenleft}}f{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ f{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
192 \begin{isamarkuptext}% |
192 \begin{isamarkuptext}% |
193 \begin{warn} |
193 \begin{warn} |
194 We discourage the use of axioms because of the danger of |
194 We discourage the use of axioms because of the danger of |
195 inconsistencies. Axiom \isa{f{\isacharunderscore}ax} does |
195 inconsistencies. Axiom \isa{f{\isaliteral{5F}{\isacharunderscore}}ax} does |
196 not introduce an inconsistency because, for example, the identity function |
196 not introduce an inconsistency because, for example, the identity function |
197 satisfies it. Axioms can be useful in exploratory developments, say when |
197 satisfies it. Axioms can be useful in exploratory developments, say when |
198 you assume some well-known theorems so that you can quickly demonstrate some |
198 you assume some well-known theorems so that you can quickly demonstrate some |
199 point about methodology. If your example turns into a substantial proof |
199 point about methodology. If your example turns into a substantial proof |
200 development, you should replace axioms by theorems. |
200 development, you should replace axioms by theorems. |
201 \end{warn}\noindent |
201 \end{warn}\noindent |
202 The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can |
202 The axiom for \isa{f} implies \isa{n\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ n}, which can |
203 be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined |
203 be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined |
204 above, we have to phrase the proposition as follows to allow induction:% |
204 above, we have to phrase the proposition as follows to allow induction:% |
205 \end{isamarkuptext}% |
205 \end{isamarkuptext}% |
206 \isamarkuptrue% |
206 \isamarkuptrue% |
207 \isacommand{lemma}\isamarkupfalse% |
207 \isacommand{lemma}\isamarkupfalse% |
208 \ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequoteclose}% |
208 \ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ k\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{22}{\isachardoublequoteclose}}% |
209 \isadelimproof |
209 \isadelimproof |
210 % |
210 % |
211 \endisadelimproof |
211 \endisadelimproof |
212 % |
212 % |
213 \isatagproof |
213 \isatagproof |
214 % |
214 % |
215 \begin{isamarkuptxt}% |
215 \begin{isamarkuptxt}% |
216 \noindent |
216 \noindent |
217 To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use |
217 To perform induction on \isa{k} using \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct}, we use |
218 the same general induction method as for recursion induction (see |
218 the same general induction method as for recursion induction (see |
219 \S\ref{sec:fun-induction}):% |
219 \S\ref{sec:fun-induction}):% |
220 \end{isamarkuptxt}% |
220 \end{isamarkuptxt}% |
221 \isamarkuptrue% |
221 \isamarkuptrue% |
222 \isacommand{apply}\isamarkupfalse% |
222 \isacommand{apply}\isamarkupfalse% |
223 {\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}% |
223 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ k\ rule{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{29}{\isacharparenright}}% |
224 \begin{isamarkuptxt}% |
224 \begin{isamarkuptxt}% |
225 \noindent |
225 \noindent |
226 We get the following proof state: |
226 We get the following proof state: |
227 \begin{isabelle}% |
227 \begin{isabelle}% |
228 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% |
228 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ m\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i% |
229 \end{isabelle} |
229 \end{isabelle} |
230 After stripping the \isa{{\isasymforall}i}, the proof continues with a case |
230 After stripping the \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i}, the proof continues with a case |
231 distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on |
231 distinction on \isa{i}. The case \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} is trivial and we focus on |
232 the other case:% |
232 the other case:% |
233 \end{isamarkuptxt}% |
233 \end{isamarkuptxt}% |
234 \isamarkuptrue% |
234 \isamarkuptrue% |
235 \isacommand{apply}\isamarkupfalse% |
235 \isacommand{apply}\isamarkupfalse% |
236 {\isacharparenleft}rule\ allI{\isacharparenright}\isanewline |
236 {\isaliteral{28}{\isacharparenleft}}rule\ allI{\isaliteral{29}{\isacharparenright}}\isanewline |
237 \isacommand{apply}\isamarkupfalse% |
237 \isacommand{apply}\isamarkupfalse% |
238 {\isacharparenleft}case{\isacharunderscore}tac\ i{\isacharparenright}\isanewline |
238 {\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ i{\isaliteral{29}{\isacharparenright}}\isanewline |
239 \ \isacommand{apply}\isamarkupfalse% |
239 \ \isacommand{apply}\isamarkupfalse% |
240 {\isacharparenleft}simp{\isacharparenright}% |
240 {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}% |
241 \begin{isamarkuptxt}% |
241 \begin{isamarkuptxt}% |
242 \begin{isabelle}% |
242 \begin{isabelle}% |
243 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline |
243 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}n\ i\ nat{\isaliteral{2E}{\isachardot}}\isanewline |
244 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% |
244 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ m\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{3B}{\isacharsemicolon}}\ i\ {\isaliteral{3D}{\isacharequal}}\ Suc\ nat{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i% |
245 \end{isabelle}% |
245 \end{isabelle}% |
246 \end{isamarkuptxt}% |
246 \end{isamarkuptxt}% |
247 \isamarkuptrue% |
247 \isamarkuptrue% |
248 \isacommand{by}\isamarkupfalse% |
248 \isacommand{by}\isamarkupfalse% |
249 {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}% |
249 {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{21}{\isacharbang}}{\isaliteral{3A}{\isacharcolon}}\ f{\isaliteral{5F}{\isacharunderscore}}ax\ Suc{\isaliteral{5F}{\isacharunderscore}}leI\ intro{\isaliteral{3A}{\isacharcolon}}\ le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{29}{\isacharparenright}}% |
250 \endisatagproof |
250 \endisatagproof |
251 {\isafoldproof}% |
251 {\isafoldproof}% |
252 % |
252 % |
253 \isadelimproof |
253 \isadelimproof |
254 % |
254 % |
256 % |
256 % |
257 \begin{isamarkuptext}% |
257 \begin{isamarkuptext}% |
258 \noindent |
258 \noindent |
259 If you find the last step puzzling, here are the two lemmas it employs: |
259 If you find the last step puzzling, here are the two lemmas it employs: |
260 \begin{isabelle} |
260 \begin{isabelle} |
261 \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n} |
261 \isa{m\ {\isaliteral{3C}{\isacharless}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n} |
262 \rulename{Suc_leI}\isanewline |
262 \rulename{Suc_leI}\isanewline |
263 \isa{{\isasymlbrakk}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z} |
263 \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}x\ {\isaliteral{5C3C6C653E}{\isasymle}}\ y{\isaliteral{3B}{\isacharsemicolon}}\ y\ {\isaliteral{3C}{\isacharless}}\ z{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{3C}{\isacharless}}\ z} |
264 \rulename{le_less_trans} |
264 \rulename{le_less_trans} |
265 \end{isabelle} |
265 \end{isabelle} |
266 % |
266 % |
267 The proof goes like this (writing \isa{j} instead of \isa{nat}). |
267 The proof goes like this (writing \isa{j} instead of \isa{nat}). |
268 Since \isa{i\ {\isacharequal}\ Suc\ j} it suffices to show |
268 Since \isa{i\ {\isaliteral{3D}{\isacharequal}}\ Suc\ j} it suffices to show |
269 \hbox{\isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}}}, |
269 \hbox{\isa{j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}}}, |
270 by \isa{Suc{\isacharunderscore}leI}\@. This is |
270 by \isa{Suc{\isaliteral{5F}{\isacharunderscore}}leI}\@. This is |
271 proved as follows. From \isa{f{\isacharunderscore}ax} we have \isa{f\ {\isacharparenleft}f\ j{\isacharparenright}\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} |
271 proved as follows. From \isa{f{\isaliteral{5F}{\isacharunderscore}}ax} we have \isa{f\ {\isaliteral{28}{\isacharparenleft}}f\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}} |
272 (1) which implies \isa{f\ j\ {\isasymle}\ f\ {\isacharparenleft}f\ j{\isacharparenright}} by the induction hypothesis. |
272 (1) which implies \isa{f\ j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ {\isaliteral{28}{\isacharparenleft}}f\ j{\isaliteral{29}{\isacharparenright}}} by the induction hypothesis. |
273 Using (1) once more we obtain \isa{f\ j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (2) by the transitivity |
273 Using (1) once more we obtain \isa{f\ j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}} (2) by the transitivity |
274 rule \isa{le{\isacharunderscore}less{\isacharunderscore}trans}. |
274 rule \isa{le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}trans}. |
275 Using the induction hypothesis once more we obtain \isa{j\ {\isasymle}\ f\ j} |
275 Using the induction hypothesis once more we obtain \isa{j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ j} |
276 which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by |
276 which, together with (2) yields \isa{j\ {\isaliteral{3C}{\isacharless}}\ f\ {\isaliteral{28}{\isacharparenleft}}Suc\ j{\isaliteral{29}{\isacharparenright}}} (again by |
277 \isa{le{\isacharunderscore}less{\isacharunderscore}trans}). |
277 \isa{le{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}trans}). |
278 |
278 |
279 This last step shows both the power and the danger of automatic proofs. They |
279 This last step shows both the power and the danger of automatic proofs. They |
280 will usually not tell you how the proof goes, because it can be hard to |
280 will usually not tell you how the proof goes, because it can be hard to |
281 translate the internal proof into a human-readable format. Automatic |
281 translate the internal proof into a human-readable format. Automatic |
282 proofs are easy to write but hard to read and understand. |
282 proofs are easy to write but hard to read and understand. |
283 |
283 |
284 The desired result, \isa{i\ {\isasymle}\ f\ i}, follows from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:% |
284 The desired result, \isa{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i}, follows from \isa{f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem}:% |
285 \end{isamarkuptext}% |
285 \end{isamarkuptext}% |
286 \isamarkuptrue% |
286 \isamarkuptrue% |
287 \isacommand{lemmas}\isamarkupfalse% |
287 \isacommand{lemmas}\isamarkupfalse% |
288 \ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}% |
288 \ f{\isaliteral{5F}{\isacharunderscore}}incr\ {\isaliteral{3D}{\isacharequal}}\ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ OF\ refl{\isaliteral{5D}{\isacharbrackright}}% |
289 \begin{isamarkuptext}% |
289 \begin{isamarkuptext}% |
290 \noindent |
290 \noindent |
291 The final \isa{refl} gets rid of the premise \isa{{\isacharquery}k\ {\isacharequal}\ f\ {\isacharquery}i}. |
291 The final \isa{refl} gets rid of the premise \isa{{\isaliteral{3F}{\isacharquery}}k\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{3F}{\isacharquery}}i}. |
292 We could have included this derivation in the original statement of the lemma:% |
292 We could have included this derivation in the original statement of the lemma:% |
293 \end{isamarkuptext}% |
293 \end{isamarkuptext}% |
294 \isamarkuptrue% |
294 \isamarkuptrue% |
295 \isacommand{lemma}\isamarkupfalse% |
295 \isacommand{lemma}\isamarkupfalse% |
296 \ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequoteclose}% |
296 \ f{\isaliteral{5F}{\isacharunderscore}}incr{\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ OF\ refl{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}i{\isaliteral{2E}{\isachardot}}\ k\ {\isaliteral{3D}{\isacharequal}}\ f\ i\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ f\ i{\isaliteral{22}{\isachardoublequoteclose}}% |
297 \isadelimproof |
297 \isadelimproof |
298 % |
298 % |
299 \endisadelimproof |
299 \endisadelimproof |
300 % |
300 % |
301 \isatagproof |
301 \isatagproof |
315 |
315 |
316 Method \methdx{induct_tac} can be applied with any rule $r$ |
316 Method \methdx{induct_tac} can be applied with any rule $r$ |
317 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the |
317 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the |
318 format is |
318 format is |
319 \begin{quote} |
319 \begin{quote} |
320 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}} |
320 \isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac} $y@1 \dots y@n$ \isa{rule{\isaliteral{3A}{\isacharcolon}}} $r$\isa{{\isaliteral{29}{\isacharparenright}}} |
321 \end{quote} |
321 \end{quote} |
322 where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal. |
322 where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal. |
323 |
323 |
324 A further useful induction rule is \isa{length{\isacharunderscore}induct}, |
324 A further useful induction rule is \isa{length{\isaliteral{5F}{\isacharunderscore}}induct}, |
325 induction on the length of a list\indexbold{*length_induct} |
325 induction on the length of a list\indexbold{*length_induct} |
326 \begin{isabelle}% |
326 \begin{isabelle}% |
327 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs% |
327 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}xs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}ys{\isaliteral{2E}{\isachardot}}\ length\ ys\ {\isaliteral{3C}{\isacharless}}\ length\ xs\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ xs% |
328 \end{isabelle} |
328 \end{isabelle} |
329 which is a special case of \isa{measure{\isacharunderscore}induct} |
329 which is a special case of \isa{measure{\isaliteral{5F}{\isacharunderscore}}induct} |
330 \begin{isabelle}% |
330 \begin{isabelle}% |
331 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ f\ y\ {\isacharless}\ f\ x\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a% |
331 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ f\ y\ {\isaliteral{3C}{\isacharless}}\ f\ x\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ a% |
332 \end{isabelle} |
332 \end{isabelle} |
333 where \isa{f} may be any function into type \isa{nat}.% |
333 where \isa{f} may be any function into type \isa{nat}.% |
334 \end{isamarkuptext}% |
334 \end{isamarkuptext}% |
335 \isamarkuptrue% |
335 \isamarkuptrue% |
336 % |
336 % |
341 \begin{isamarkuptext}% |
341 \begin{isamarkuptext}% |
342 \label{sec:derive-ind} |
342 \label{sec:derive-ind} |
343 \index{induction!deriving new schemas}% |
343 \index{induction!deriving new schemas}% |
344 Induction schemas are ordinary theorems and you can derive new ones |
344 Induction schemas are ordinary theorems and you can derive new ones |
345 whenever you wish. This section shows you how, using the example |
345 whenever you wish. This section shows you how, using the example |
346 of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction |
346 of \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct}. Assume we only have structural induction |
347 available for \isa{nat} and want to derive complete induction. We |
347 available for \isa{nat} and want to derive complete induction. We |
348 must generalize the statement as shown:% |
348 must generalize the statement as shown:% |
349 \end{isamarkuptext}% |
349 \end{isamarkuptext}% |
350 \isamarkuptrue% |
350 \isamarkuptrue% |
351 \isacommand{lemma}\isamarkupfalse% |
351 \isacommand{lemma}\isamarkupfalse% |
352 \ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequoteclose}\isanewline |
352 \ induct{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
353 % |
353 % |
354 \isadelimproof |
354 \isadelimproof |
355 % |
355 % |
356 \endisadelimproof |
356 \endisadelimproof |
357 % |
357 % |
358 \isatagproof |
358 \isatagproof |
359 \isacommand{apply}\isamarkupfalse% |
359 \isacommand{apply}\isamarkupfalse% |
360 {\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}% |
360 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ n{\isaliteral{29}{\isacharparenright}}% |
361 \begin{isamarkuptxt}% |
361 \begin{isamarkuptxt}% |
362 \noindent |
362 \noindent |
363 The base case is vacuously true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction |
363 The base case is vacuously true. For the induction step (\isa{m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isaliteral{3C}{\isacharless}}\ n} is true by induction |
364 hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using |
364 hypothesis and case \isa{m\ {\isaliteral{3D}{\isacharequal}}\ n} follows from the assumption, again using |
365 the induction hypothesis:% |
365 the induction hypothesis:% |
366 \end{isamarkuptxt}% |
366 \end{isamarkuptxt}% |
367 \isamarkuptrue% |
367 \isamarkuptrue% |
368 \ \isacommand{apply}\isamarkupfalse% |
368 \ \isacommand{apply}\isamarkupfalse% |
369 {\isacharparenleft}blast{\isacharparenright}\isanewline |
369 {\isaliteral{28}{\isacharparenleft}}blast{\isaliteral{29}{\isacharparenright}}\isanewline |
370 \isacommand{by}\isamarkupfalse% |
370 \isacommand{by}\isamarkupfalse% |
371 {\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}% |
371 {\isaliteral{28}{\isacharparenleft}}blast\ elim{\isaliteral{3A}{\isacharcolon}}\ less{\isaliteral{5F}{\isacharunderscore}}SucE{\isaliteral{29}{\isacharparenright}}% |
372 \endisatagproof |
372 \endisatagproof |
373 {\isafoldproof}% |
373 {\isafoldproof}% |
374 % |
374 % |
375 \isadelimproof |
375 \isadelimproof |
376 % |
376 % |
377 \endisadelimproof |
377 \endisadelimproof |
378 % |
378 % |
379 \begin{isamarkuptext}% |
379 \begin{isamarkuptext}% |
380 \noindent |
380 \noindent |
381 The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction: |
381 The elimination rule \isa{less{\isaliteral{5F}{\isacharunderscore}}SucE} expresses the case distinction: |
382 \begin{isabelle}% |
382 \begin{isabelle}% |
383 \ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% |
383 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{3B}{\isacharsemicolon}}\ m\ {\isaliteral{3C}{\isacharless}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{3B}{\isacharsemicolon}}\ m\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P% |
384 \end{isabelle} |
384 \end{isabelle} |
385 |
385 |
386 Now it is straightforward to derive the original version of |
386 Now it is straightforward to derive the original version of |
387 \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulating the conclusion of the above |
387 \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct} by manipulating the conclusion of the above |
388 lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} |
388 lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} |
389 and remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this |
389 and remove the trivial condition \isa{n\ {\isaliteral{3C}{\isacharless}}\ Suc\ n}. Fortunately, this |
390 happens automatically when we add the lemma as a new premise to the |
390 happens automatically when we add the lemma as a new premise to the |
391 desired goal:% |
391 desired goal:% |
392 \end{isamarkuptext}% |
392 \end{isamarkuptext}% |
393 \isamarkuptrue% |
393 \isamarkuptrue% |
394 \isacommand{theorem}\isamarkupfalse% |
394 \isacommand{theorem}\isamarkupfalse% |
395 \ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequoteclose}\isanewline |
395 \ nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{3C}{\isacharless}}n{\isaliteral{2E}{\isachardot}}\ P\ m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
396 % |
396 % |
397 \isadelimproof |
397 \isadelimproof |
398 % |
398 % |
399 \endisadelimproof |
399 \endisadelimproof |
400 % |
400 % |
401 \isatagproof |
401 \isatagproof |
402 \isacommand{by}\isamarkupfalse% |
402 \isacommand{by}\isamarkupfalse% |
403 {\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}% |
403 {\isaliteral{28}{\isacharparenleft}}insert\ induct{\isaliteral{5F}{\isacharunderscore}}lem{\isaliteral{2C}{\isacharcomma}}\ blast{\isaliteral{29}{\isacharparenright}}% |
404 \endisatagproof |
404 \endisatagproof |
405 {\isafoldproof}% |
405 {\isafoldproof}% |
406 % |
406 % |
407 \isadelimproof |
407 \isadelimproof |
408 % |
408 % |
409 \endisadelimproof |
409 \endisadelimproof |
410 % |
410 % |
411 \begin{isamarkuptext}% |
411 \begin{isamarkuptext}% |
412 HOL already provides the mother of |
412 HOL already provides the mother of |
413 all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For |
413 all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For |
414 example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is |
414 example theorem \isa{nat{\isaliteral{5F}{\isacharunderscore}}less{\isaliteral{5F}{\isacharunderscore}}induct} is |
415 a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on |
415 a special case of \isa{wf{\isaliteral{5F}{\isacharunderscore}}induct} where \isa{r} is \isa{{\isaliteral{3C}{\isacharless}}} on |
416 \isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.% |
416 \isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.% |
417 \end{isamarkuptext}% |
417 \end{isamarkuptext}% |
418 \isamarkuptrue% |
418 \isamarkuptrue% |
419 % |
419 % |
420 \isadelimtheory |
420 \isadelimtheory |