24 binary case splits. Here is another example:% |
24 binary case splits. Here is another example:% |
25 \end{isamarkuptext}% |
25 \end{isamarkuptext}% |
26 \isamarkuptrue% |
26 \isamarkuptrue% |
27 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline |
27 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline |
28 \isamarkupfalse% |
28 \isamarkupfalse% |
29 \isacommand{proof}\ cases\isanewline |
29 \isamarkupfalse% |
30 \ \ \isamarkupfalse% |
30 \isamarkupfalse% |
31 \isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% |
31 \isamarkupfalse% |
32 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% |
32 \isamarkupfalse% |
33 \isacommand{{\isachardot}{\isachardot}}\isanewline |
33 \isamarkupfalse% |
34 \isamarkupfalse% |
34 \isamarkupfalse% |
35 \isacommand{next}\isanewline |
35 \isamarkupfalse% |
36 \ \ \isamarkupfalse% |
36 \isamarkupfalse% |
37 \isacommand{assume}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\ \isamarkupfalse% |
37 \isamarkupfalse% |
38 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% |
|
39 \isacommand{{\isachardot}{\isachardot}}\isanewline |
|
40 \isamarkupfalse% |
|
41 \isacommand{qed}\isamarkupfalse% |
|
42 % |
38 % |
43 \begin{isamarkuptext}% |
39 \begin{isamarkuptext}% |
44 \noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where |
40 \noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where |
45 \isa{case{\isacharunderscore}split{\isacharunderscore}thm} is \isa{{\isasymlbrakk}{\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}. If we reverse |
41 \isa{case{\isacharunderscore}split{\isacharunderscore}thm} is \isa{{\isasymlbrakk}{\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}. If we reverse |
46 the order of the two cases in the proof, the first case would prove |
42 the order of the two cases in the proof, the first case would prove |
53 be avoided by the following idiom% |
49 be avoided by the following idiom% |
54 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
55 \isamarkuptrue% |
51 \isamarkuptrue% |
56 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline |
52 \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline |
57 \isamarkupfalse% |
53 \isamarkupfalse% |
58 \isacommand{proof}\ {\isacharparenleft}cases\ {\isachardoublequote}A{\isachardoublequote}{\isacharparenright}\isanewline |
54 \isamarkupfalse% |
59 \ \ \isamarkupfalse% |
55 \isamarkupfalse% |
60 \isacommand{case}\ True\ \isamarkupfalse% |
56 \isamarkupfalse% |
61 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% |
57 \isamarkupfalse% |
62 \isacommand{{\isachardot}{\isachardot}}\isanewline |
58 \isamarkupfalse% |
63 \isamarkupfalse% |
59 \isamarkupfalse% |
64 \isacommand{next}\isanewline |
60 \isamarkupfalse% |
65 \ \ \isamarkupfalse% |
61 \isamarkupfalse% |
66 \isacommand{case}\ False\ \isamarkupfalse% |
62 \isamarkupfalse% |
67 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% |
|
68 \isacommand{{\isachardot}{\isachardot}}\isanewline |
|
69 \isamarkupfalse% |
|
70 \isacommand{qed}\isamarkupfalse% |
|
71 % |
63 % |
72 \begin{isamarkuptext}% |
64 \begin{isamarkuptext}% |
73 \noindent which is like the previous proof but instantiates |
65 \noindent which is like the previous proof but instantiates |
74 \isa{{\isacharquery}P} right away with \isa{A}. Thus we could prove the two |
66 \isa{{\isacharquery}P} right away with \isa{A}. Thus we could prove the two |
75 cases in any order. The phrase `\isakeyword{case}~\isa{True}' |
67 cases in any order. The phrase `\isakeyword{case}~\isa{True}' |
82 \end{isamarkuptext}% |
74 \end{isamarkuptext}% |
83 \isamarkuptrue% |
75 \isamarkuptrue% |
84 \isamarkupfalse% |
76 \isamarkupfalse% |
85 \isacommand{lemma}\ {\isachardoublequote}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
77 \isacommand{lemma}\ {\isachardoublequote}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
86 \isamarkupfalse% |
78 \isamarkupfalse% |
87 \isacommand{proof}\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline |
79 \isamarkupfalse% |
88 \ \ \isamarkupfalse% |
80 \isamarkupfalse% |
89 \isacommand{case}\ Nil\ \isamarkupfalse% |
81 \isamarkupfalse% |
90 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% |
82 \isamarkupfalse% |
91 \isacommand{by}\ simp\isanewline |
83 \isamarkupfalse% |
92 \isamarkupfalse% |
84 \isamarkupfalse% |
93 \isacommand{next}\isanewline |
85 \isamarkupfalse% |
94 \ \ \isamarkupfalse% |
86 \isamarkupfalse% |
95 \isacommand{case}\ Cons\ \isamarkupfalse% |
87 \isamarkupfalse% |
96 \isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% |
|
97 \isacommand{by}\ simp\isanewline |
|
98 \isamarkupfalse% |
|
99 \isacommand{qed}\isamarkupfalse% |
|
100 % |
88 % |
101 \begin{isamarkuptext}% |
89 \begin{isamarkuptext}% |
102 \noindent Here `\isakeyword{case}~\isa{Nil}' abbreviates |
90 \noindent Here `\isakeyword{case}~\isa{Nil}' abbreviates |
103 `\isakeyword{assume}~\isa{Nil{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}' and |
91 `\isakeyword{assume}~\isa{Nil{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}' and |
104 `\isakeyword{case}~\isa{Cons}' |
92 `\isakeyword{case}~\isa{Cons}' |
125 % |
113 % |
126 \begin{isamarkuptext}% |
114 \begin{isamarkuptext}% |
127 We start with an inductive proof where both cases are proved automatically:% |
115 We start with an inductive proof where both cases are proved automatically:% |
128 \end{isamarkuptext}% |
116 \end{isamarkuptext}% |
129 \isamarkuptrue% |
117 \isamarkuptrue% |
130 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
118 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
131 \isamarkupfalse% |
119 \isamarkupfalse% |
132 \isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% |
120 \isamarkupfalse% |
133 % |
121 % |
134 \begin{isamarkuptext}% |
122 \begin{isamarkuptext}% |
135 \noindent If we want to expose more of the structure of the |
123 \noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of |
|
124 the operations involved are overloaded. |
|
125 |
|
126 If we want to expose more of the structure of the |
136 proof, we can use pattern matching to avoid having to repeat the goal |
127 proof, we can use pattern matching to avoid having to repeat the goal |
137 statement:% |
128 statement:% |
138 \end{isamarkuptext}% |
129 \end{isamarkuptext}% |
139 \isamarkuptrue% |
130 \isamarkuptrue% |
140 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline |
131 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline |
141 \isamarkupfalse% |
132 \isamarkupfalse% |
142 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
133 \isamarkupfalse% |
143 \ \ \isamarkupfalse% |
134 \isamarkupfalse% |
144 \isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse% |
135 \isamarkupfalse% |
145 \isacommand{by}\ simp\isanewline |
136 \isamarkupfalse% |
146 \isamarkupfalse% |
137 \isamarkupfalse% |
147 \isacommand{next}\isanewline |
138 \isamarkupfalse% |
148 \ \ \isamarkupfalse% |
139 \isamarkupfalse% |
149 \isacommand{fix}\ n\ \isamarkupfalse% |
140 \isamarkupfalse% |
150 \isacommand{assume}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}\isanewline |
141 \isamarkupfalse% |
151 \ \ \isamarkupfalse% |
|
152 \isacommand{thus}\ {\isachardoublequote}{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
|
153 \isacommand{by}\ simp\isanewline |
|
154 \isamarkupfalse% |
|
155 \isacommand{qed}\isamarkupfalse% |
|
156 % |
142 % |
157 \begin{isamarkuptext}% |
143 \begin{isamarkuptext}% |
158 \noindent We could refine this further to show more of the equational |
144 \noindent We could refine this further to show more of the equational |
159 proof. Instead we explore the same avenue as for case distinctions: |
145 proof. Instead we explore the same avenue as for case distinctions: |
160 introducing context via the \isakeyword{case} command:% |
146 introducing context via the \isakeyword{case} command:% |
161 \end{isamarkuptext}% |
147 \end{isamarkuptext}% |
162 \isamarkuptrue% |
148 \isamarkuptrue% |
163 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
149 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
164 \isamarkupfalse% |
150 \isamarkupfalse% |
165 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
151 \isamarkupfalse% |
166 \ \ \isamarkupfalse% |
152 \isamarkupfalse% |
167 \isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse% |
153 \isamarkupfalse% |
168 \isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% |
154 \isamarkupfalse% |
169 \isacommand{by}\ simp\isanewline |
155 \isamarkupfalse% |
170 \isamarkupfalse% |
156 \isamarkupfalse% |
171 \isacommand{next}\isanewline |
157 \isamarkupfalse% |
172 \ \ \isamarkupfalse% |
158 \isamarkupfalse% |
173 \isacommand{case}\ Suc\ \isamarkupfalse% |
159 \isamarkupfalse% |
174 \isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% |
|
175 \isacommand{by}\ simp\isanewline |
|
176 \isamarkupfalse% |
|
177 \isacommand{qed}\isamarkupfalse% |
|
178 % |
160 % |
179 \begin{isamarkuptext}% |
161 \begin{isamarkuptext}% |
180 \noindent The implicitly defined \isa{{\isacharquery}case} refers to the |
162 \noindent The implicitly defined \isa{{\isacharquery}case} refers to the |
181 corresponding case to be proved, i.e.\ \isa{{\isacharquery}P\ {\isadigit{0}}} in the first case and |
163 corresponding case to be proved, i.e.\ \isa{{\isacharquery}P\ {\isadigit{0}}} in the first case and |
182 \isa{{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}} in the second case. Context \isakeyword{case}~\isa{{\isadigit{0}}} is |
164 \isa{{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}} in the second case. Context \isakeyword{case}~\isa{{\isadigit{0}}} is |
187 \isa{Cons} above: replace \isa{Suc} by \isa{{\isacharparenleft}Suc\ i{\isacharparenright}}:% |
169 \isa{Cons} above: replace \isa{Suc} by \isa{{\isacharparenleft}Suc\ i{\isacharparenright}}:% |
188 \end{isamarkuptext}% |
170 \end{isamarkuptext}% |
189 \isamarkuptrue% |
171 \isamarkuptrue% |
190 \isacommand{lemma}\ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\ \isakeyword{shows}\ {\isachardoublequote}n\ {\isacharless}\ n{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
172 \isacommand{lemma}\ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\ \isakeyword{shows}\ {\isachardoublequote}n\ {\isacharless}\ n{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
191 \isamarkupfalse% |
173 \isamarkupfalse% |
192 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
174 \isamarkupfalse% |
193 \ \ \isamarkupfalse% |
175 \isamarkupfalse% |
194 \isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse% |
176 \isamarkupfalse% |
195 \isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% |
177 \isamarkupfalse% |
196 \isacommand{by}\ simp\isanewline |
178 \isamarkupfalse% |
197 \isamarkupfalse% |
179 \isamarkupfalse% |
198 \isacommand{next}\isanewline |
180 \isamarkupfalse% |
199 \ \ \isamarkupfalse% |
181 \isamarkupfalse% |
200 \isacommand{case}\ {\isacharparenleft}Suc\ i{\isacharparenright}\ \isamarkupfalse% |
182 \isamarkupfalse% |
201 \isacommand{thus}\ {\isachardoublequote}Suc\ i\ {\isacharless}\ Suc\ i\ {\isacharasterisk}\ Suc\ i\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\ \isamarkupfalse% |
|
202 \isacommand{by}\ simp\isanewline |
|
203 \isamarkupfalse% |
|
204 \isacommand{qed}\isamarkupfalse% |
|
205 % |
183 % |
206 \begin{isamarkuptext}% |
184 \begin{isamarkuptext}% |
207 \noindent Of course we could again have written |
185 \noindent Of course we could again have written |
208 \isakeyword{thus}~\isa{{\isacharquery}case} instead of giving the term explicitly |
186 \isakeyword{thus}~\isa{{\isacharquery}case} instead of giving the term explicitly |
209 but we wanted to use \isa{i} somewhere.% |
187 but we wanted to use \isa{i} somewhere.% |
231 \end{isamarkuptext}% |
209 \end{isamarkuptext}% |
232 \isamarkuptrue% |
210 \isamarkuptrue% |
233 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isacharparenleft}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}{\isachardoublequote}\isanewline |
211 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isacharparenleft}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}{\isachardoublequote}\isanewline |
234 \ \ \isakeyword{shows}\ {\isachardoublequote}P{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline |
212 \ \ \isakeyword{shows}\ {\isachardoublequote}P{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline |
235 \isamarkupfalse% |
213 \isamarkupfalse% |
236 \isacommand{proof}\ {\isacharparenleft}rule\ A{\isacharparenright}\isanewline |
214 \isamarkupfalse% |
237 \ \ \isamarkupfalse% |
215 \isamarkupfalse% |
238 \isacommand{show}\ {\isachardoublequote}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isachardoublequote}\isanewline |
216 \isamarkupfalse% |
239 \ \ \isamarkupfalse% |
217 \isamarkupfalse% |
240 \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
218 \isamarkupfalse% |
241 \ \ \ \ \isamarkupfalse% |
219 \isamarkupfalse% |
242 \isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse% |
220 \isamarkupfalse% |
243 \isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% |
221 \isamarkupfalse% |
244 \isacommand{by}\ simp\isanewline |
222 \isamarkupfalse% |
245 \ \ \isamarkupfalse% |
223 \isamarkupfalse% |
246 \isacommand{next}\isanewline |
224 \isamarkupfalse% |
247 \ \ \ \ \isamarkupfalse% |
225 \isamarkupfalse% |
248 \isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ % |
226 \isamarkupfalse% |
249 \isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}} \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}m\ {\isacharless}\ Suc\ n{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}}% |
227 \isamarkupfalse% |
250 } |
228 \isamarkupfalse% |
251 \isanewline |
229 \isamarkupfalse% |
252 \ \ \ \ \isamarkupfalse% |
230 \isamarkupfalse% |
253 \isacommand{show}\ {\isacharquery}case\ \ \ \ % |
231 \isamarkupfalse% |
254 \isamarkupcmt{\isa{P\ m}% |
232 \isamarkupfalse% |
255 } |
233 \isamarkupfalse% |
256 \isanewline |
234 \isamarkupfalse% |
257 \ \ \ \ \isamarkupfalse% |
235 \isamarkupfalse% |
258 \isacommand{proof}\ cases\isanewline |
236 \isamarkupfalse% |
259 \ \ \ \ \ \ \isamarkupfalse% |
237 \isamarkupfalse% |
260 \isacommand{assume}\ eq{\isacharcolon}\ {\isachardoublequote}m\ {\isacharequal}\ n{\isachardoublequote}\isanewline |
238 \isamarkupfalse% |
261 \ \ \ \ \ \ \isamarkupfalse% |
239 \isamarkupfalse% |
262 \isacommand{from}\ Suc\ \isakeyword{and}\ A\ \isamarkupfalse% |
240 \isamarkupfalse% |
263 \isacommand{have}\ {\isachardoublequote}P\ n{\isachardoublequote}\ \isamarkupfalse% |
|
264 \isacommand{by}\ blast\isanewline |
|
265 \ \ \ \ \ \ \isamarkupfalse% |
|
266 \isacommand{with}\ eq\ \isamarkupfalse% |
|
267 \isacommand{show}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse% |
|
268 \isacommand{by}\ simp\isanewline |
|
269 \ \ \ \ \isamarkupfalse% |
|
270 \isacommand{next}\isanewline |
|
271 \ \ \ \ \ \ \isamarkupfalse% |
|
272 \isacommand{assume}\ {\isachardoublequote}m\ {\isasymnoteq}\ n{\isachardoublequote}\isanewline |
|
273 \ \ \ \ \ \ \isamarkupfalse% |
|
274 \isacommand{with}\ Suc\ \isamarkupfalse% |
|
275 \isacommand{have}\ {\isachardoublequote}m\ {\isacharless}\ n{\isachardoublequote}\ \isamarkupfalse% |
|
276 \isacommand{by}\ arith\isanewline |
|
277 \ \ \ \ \ \ \isamarkupfalse% |
|
278 \isacommand{thus}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse% |
|
279 \isacommand{by}{\isacharparenleft}rule\ Suc{\isacharparenright}\isanewline |
|
280 \ \ \ \ \isamarkupfalse% |
|
281 \isacommand{qed}\isanewline |
|
282 \ \ \isamarkupfalse% |
|
283 \isacommand{qed}\isanewline |
|
284 \isamarkupfalse% |
|
285 \isacommand{qed}\isamarkupfalse% |
|
286 % |
241 % |
287 \begin{isamarkuptext}% |
242 \begin{isamarkuptext}% |
288 \noindent Given the explanations above and the comments in the |
243 \noindent Given the explanations above and the comments in the |
289 proof text (only necessary for novices), the proof should be quite |
244 proof text (only necessary for novices), the proof should be quite |
290 readable. |
245 readable. |
327 \isa{r{\isacharasterisk}} is indeed transitive:% |
282 \isa{r{\isacharasterisk}} is indeed transitive:% |
328 \end{isamarkuptext}% |
283 \end{isamarkuptext}% |
329 \isamarkuptrue% |
284 \isamarkuptrue% |
330 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline |
285 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline |
331 \isamarkupfalse% |
286 \isamarkupfalse% |
332 \isacommand{using}\ A\isanewline |
287 \isamarkupfalse% |
333 \isamarkupfalse% |
288 \isamarkupfalse% |
334 \isacommand{proof}\ induct\isanewline |
289 \isamarkupfalse% |
335 \ \ \isamarkupfalse% |
290 \isamarkupfalse% |
336 \isacommand{case}\ refl\ \isamarkupfalse% |
291 \isamarkupfalse% |
337 \isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% |
292 \isamarkupfalse% |
338 \isacommand{{\isachardot}}\isanewline |
293 \isamarkupfalse% |
339 \isamarkupfalse% |
294 \isamarkupfalse% |
340 \isacommand{next}\isanewline |
295 \isamarkupfalse% |
341 \ \ \isamarkupfalse% |
296 \isamarkupfalse% |
342 \isacommand{case}\ step\ \isamarkupfalse% |
|
343 \isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% |
|
344 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isachardot}step{\isacharparenright}\isanewline |
|
345 \isamarkupfalse% |
|
346 \isacommand{qed}\isamarkupfalse% |
|
347 % |
297 % |
348 \begin{isamarkuptext}% |
298 \begin{isamarkuptext}% |
349 \noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) |
299 \noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) |
350 \in R$ piped into the proof, here \isakeyword{using}~\isa{A}. The |
300 \in R$ piped into the proof, here \isakeyword{using}~\isa{A}. The |
351 proof itself follows the inductive definition very |
301 proof itself follows the inductive definition very |
356 \end{isamarkuptext}% |
306 \end{isamarkuptext}% |
357 \isamarkuptrue% |
307 \isamarkuptrue% |
358 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\ B{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline |
308 \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\ B{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline |
359 \ \ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline |
309 \ \ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline |
360 \isamarkupfalse% |
310 \isamarkupfalse% |
361 \isacommand{proof}\ {\isacharminus}\isanewline |
311 \isamarkupfalse% |
362 \ \ \isamarkupfalse% |
312 \isamarkupfalse% |
363 \isacommand{from}\ A\ B\ \isamarkupfalse% |
313 \isamarkupfalse% |
364 \isacommand{show}\ {\isacharquery}thesis\isanewline |
314 \isamarkupfalse% |
365 \ \ \isamarkupfalse% |
315 \isamarkupfalse% |
366 \isacommand{proof}\ induct\isanewline |
316 \isamarkupfalse% |
367 \ \ \ \ \isamarkupfalse% |
317 \isamarkupfalse% |
368 \isacommand{fix}\ x\ \isamarkupfalse% |
318 \isamarkupfalse% |
369 \isacommand{assume}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \ % |
319 \isamarkupfalse% |
370 \isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]% |
320 \isamarkupfalse% |
371 } |
321 \isamarkupfalse% |
372 \isanewline |
322 \isamarkupfalse% |
373 \ \ \ \ \isamarkupfalse% |
323 \isamarkupfalse% |
374 \isacommand{thus}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse% |
324 \isamarkupfalse% |
375 \isacommand{{\isachardot}}\isanewline |
325 \isamarkupfalse% |
376 \ \ \isamarkupfalse% |
326 \isamarkupfalse% |
377 \isacommand{next}\isanewline |
|
378 \ \ \ \ \isamarkupfalse% |
|
379 \isacommand{fix}\ x{\isacharprime}\ x\ y\isanewline |
|
380 \ \ \ \ \isamarkupfalse% |
|
381 \isacommand{assume}\ {\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isachardoublequote}\ \isakeyword{and}\isanewline |
|
382 \ \ \ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\isanewline |
|
383 \ \ \ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline |
|
384 \ \ \ \ \isamarkupfalse% |
|
385 \isacommand{from}\ {\isadigit{1}}\ IH{\isacharbrackleft}OF\ B{\isacharbrackright}\ \isamarkupfalse% |
|
386 \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse% |
|
387 \isacommand{by}{\isacharparenleft}rule\ rtc{\isachardot}step{\isacharparenright}\isanewline |
|
388 \ \ \isamarkupfalse% |
|
389 \isacommand{qed}\isanewline |
|
390 \isamarkupfalse% |
|
391 \isacommand{qed}\isamarkupfalse% |
|
392 % |
327 % |
393 \begin{isamarkuptext}% |
328 \begin{isamarkuptext}% |
394 \noindent We start the proof with \isakeyword{from}~\isa{A\ B}. Only \isa{A} is ``consumed'' by the induction step. |
329 \noindent We start the proof with \isakeyword{from}~\isa{A\ B}. Only \isa{A} is ``consumed'' by the induction step. |
395 Since \isa{B} is left over we don't just prove \isa{{\isacharquery}thesis} but \isa{B\ {\isasymLongrightarrow}\ {\isacharquery}thesis}, just as in the previous proof. The |
330 Since \isa{B} is left over we don't just prove \isa{{\isacharquery}thesis} but \isa{B\ {\isasymLongrightarrow}\ {\isacharquery}thesis}, just as in the previous proof. The |
396 base case is trivial. In the assumptions for the induction step we can |
331 base case is trivial. In the assumptions for the induction step we can |
444 functions.% |
379 functions.% |
445 \end{isamarkuptext}% |
380 \end{isamarkuptext}% |
446 \isamarkuptrue% |
381 \isamarkuptrue% |
447 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ rot\ xs\ {\isacharequal}\ tl\ xs\ {\isacharat}\ {\isacharbrackleft}hd\ xs{\isacharbrackright}{\isachardoublequote}\isanewline |
382 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ rot\ xs\ {\isacharequal}\ tl\ xs\ {\isacharat}\ {\isacharbrackleft}hd\ xs{\isacharbrackright}{\isachardoublequote}\isanewline |
448 \isamarkupfalse% |
383 \isamarkupfalse% |
449 \isacommand{proof}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\isanewline |
384 \isamarkupfalse% |
450 \ \ \isamarkupfalse% |
385 \isamarkupfalse% |
451 \isacommand{case}\ {\isadigit{1}}\ \isamarkupfalse% |
386 \isamarkupfalse% |
452 \isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% |
387 \isamarkupfalse% |
453 \isacommand{by}\ simp\isanewline |
388 \isamarkupfalse% |
454 \isamarkupfalse% |
389 \isamarkupfalse% |
455 \isacommand{next}\isanewline |
390 \isamarkupfalse% |
456 \ \ \isamarkupfalse% |
391 \isamarkupfalse% |
457 \isacommand{case}\ {\isadigit{2}}\ \isamarkupfalse% |
392 \isamarkupfalse% |
458 \isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% |
393 \isamarkupfalse% |
459 \isacommand{by}\ simp\isanewline |
394 \isamarkupfalse% |
460 \isamarkupfalse% |
395 \isamarkupfalse% |
461 \isacommand{next}\isanewline |
396 \isamarkupfalse% |
462 \ \ \isamarkupfalse% |
397 \isamarkupfalse% |
463 \isacommand{case}\ {\isacharparenleft}{\isadigit{3}}\ a\ b\ cs{\isacharparenright}\isanewline |
398 \isamarkupfalse% |
464 \ \ \isamarkupfalse% |
399 \isamarkupfalse% |
465 \isacommand{have}\ {\isachardoublequote}rot\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharequal}\ b\ {\isacharhash}\ rot{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% |
400 \isamarkupfalse% |
466 \isacommand{by}\ simp\isanewline |
401 \isamarkupfalse% |
467 \ \ \isamarkupfalse% |
402 \isamarkupfalse% |
468 \isacommand{also}\ \isamarkupfalse% |
403 \isamarkupfalse% |
469 \isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ b\ {\isacharhash}\ tl{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse% |
404 \isamarkupfalse% |
470 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}{\isadigit{3}}{\isacharparenright}\isanewline |
405 \isamarkupfalse% |
471 \ \ \isamarkupfalse% |
|
472 \isacommand{also}\ \isamarkupfalse% |
|
473 \isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ tl\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse% |
|
474 \isacommand{by}\ simp\isanewline |
|
475 \ \ \isamarkupfalse% |
|
476 \isacommand{finally}\ \isamarkupfalse% |
|
477 \isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% |
|
478 \isacommand{{\isachardot}}\isanewline |
|
479 \isamarkupfalse% |
|
480 \isacommand{qed}\isamarkupfalse% |
|
481 % |
406 % |
482 \begin{isamarkuptext}% |
407 \begin{isamarkuptext}% |
483 \noindent |
408 \noindent |
484 The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01} |
409 The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01} |
485 for how to reason with chains of equations) to demonstrate that the |
410 for how to reason with chains of equations) to demonstrate that the |