1 (* Title: CTT/Arith.thy |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1991 University of Cambridge |
|
4 *) |
|
5 |
|
6 section \<open>Elementary arithmetic\<close> |
|
7 |
|
8 theory Arith |
|
9 imports Bool |
|
10 begin |
|
11 |
|
12 subsection \<open>Arithmetic operators and their definitions\<close> |
|
13 |
|
14 definition add :: "[i,i]\<Rightarrow>i" (infixr "#+" 65) |
|
15 where "a#+b \<equiv> rec(a, b, \<lambda>u v. succ(v))" |
|
16 |
|
17 definition diff :: "[i,i]\<Rightarrow>i" (infixr "-" 65) |
|
18 where "a-b \<equiv> rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))" |
|
19 |
|
20 definition absdiff :: "[i,i]\<Rightarrow>i" (infixr "|-|" 65) |
|
21 where "a|-|b \<equiv> (a-b) #+ (b-a)" |
|
22 |
|
23 definition mult :: "[i,i]\<Rightarrow>i" (infixr "#*" 70) |
|
24 where "a#*b \<equiv> rec(a, 0, \<lambda>u v. b #+ v)" |
|
25 |
|
26 definition mod :: "[i,i]\<Rightarrow>i" (infixr "mod" 70) |
|
27 where "a mod b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(v) |-| b, 0, \<lambda>x y. succ(v)))" |
|
28 |
|
29 definition div :: "[i,i]\<Rightarrow>i" (infixr "div" 70) |
|
30 where "a div b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))" |
|
31 |
|
32 lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def |
|
33 |
|
34 |
|
35 subsection \<open>Proofs about elementary arithmetic: addition, multiplication, etc.\<close> |
|
36 |
|
37 subsubsection \<open>Addition\<close> |
|
38 |
|
39 text \<open>Typing of \<open>add\<close>: short and long versions.\<close> |
|
40 |
|
41 lemma add_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b : N" |
|
42 unfolding arith_defs by typechk |
|
43 |
|
44 lemma add_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #+ b = c #+ d : N" |
|
45 unfolding arith_defs by equal |
|
46 |
|
47 |
|
48 text \<open>Computation for \<open>add\<close>: 0 and successor cases.\<close> |
|
49 |
|
50 lemma addC0: "b:N \<Longrightarrow> 0 #+ b = b : N" |
|
51 unfolding arith_defs by rew |
|
52 |
|
53 lemma addC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #+ b = succ(a #+ b) : N" |
|
54 unfolding arith_defs by rew |
|
55 |
|
56 |
|
57 subsubsection \<open>Multiplication\<close> |
|
58 |
|
59 text \<open>Typing of \<open>mult\<close>: short and long versions.\<close> |
|
60 |
|
61 lemma mult_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b : N" |
|
62 unfolding arith_defs by (typechk add_typing) |
|
63 |
|
64 lemma mult_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #* b = c #* d : N" |
|
65 unfolding arith_defs by (equal add_typingL) |
|
66 |
|
67 |
|
68 text \<open>Computation for \<open>mult\<close>: 0 and successor cases.\<close> |
|
69 |
|
70 lemma multC0: "b:N \<Longrightarrow> 0 #* b = 0 : N" |
|
71 unfolding arith_defs by rew |
|
72 |
|
73 lemma multC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #* b = b #+ (a #* b) : N" |
|
74 unfolding arith_defs by rew |
|
75 |
|
76 |
|
77 subsubsection \<open>Difference\<close> |
|
78 |
|
79 text \<open>Typing of difference.\<close> |
|
80 |
|
81 lemma diff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a - b : N" |
|
82 unfolding arith_defs by typechk |
|
83 |
|
84 lemma diff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a - b = c - d : N" |
|
85 unfolding arith_defs by equal |
|
86 |
|
87 |
|
88 text \<open>Computation for difference: 0 and successor cases.\<close> |
|
89 |
|
90 lemma diffC0: "a:N \<Longrightarrow> a - 0 = a : N" |
|
91 unfolding arith_defs by rew |
|
92 |
|
93 text \<open>Note: \<open>rec(a, 0, \<lambda>z w.z)\<close> is \<open>pred(a).\<close>\<close> |
|
94 |
|
95 lemma diff_0_eq_0: "b:N \<Longrightarrow> 0 - b = 0 : N" |
|
96 unfolding arith_defs |
|
97 apply (NE b) |
|
98 apply hyp_rew |
|
99 done |
|
100 |
|
101 text \<open> |
|
102 Essential to simplify FIRST!! (Else we get a critical pair) |
|
103 \<open>succ(a) - succ(b)\<close> rewrites to \<open>pred(succ(a) - b)\<close>. |
|
104 \<close> |
|
105 lemma diff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) - succ(b) = a - b : N" |
|
106 unfolding arith_defs |
|
107 apply hyp_rew |
|
108 apply (NE b) |
|
109 apply hyp_rew |
|
110 done |
|
111 |
|
112 |
|
113 subsection \<open>Simplification\<close> |
|
114 |
|
115 lemmas arith_typing_rls = add_typing mult_typing diff_typing |
|
116 and arith_congr_rls = add_typingL mult_typingL diff_typingL |
|
117 |
|
118 lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls |
|
119 |
|
120 lemmas arithC_rls = |
|
121 addC0 addC_succ |
|
122 multC0 multC_succ |
|
123 diffC0 diff_0_eq_0 diff_succ_succ |
|
124 |
|
125 ML \<open> |
|
126 structure Arith_simp = TSimpFun( |
|
127 val refl = @{thm refl_elem} |
|
128 val sym = @{thm sym_elem} |
|
129 val trans = @{thm trans_elem} |
|
130 val refl_red = @{thm refl_red} |
|
131 val trans_red = @{thm trans_red} |
|
132 val red_if_equal = @{thm red_if_equal} |
|
133 val default_rls = @{thms arithC_rls comp_rls} |
|
134 val routine_tac = routine_tac @{thms arith_typing_rls routine_rls} |
|
135 ) |
|
136 |
|
137 fun arith_rew_tac ctxt prems = |
|
138 make_rew_tac ctxt (Arith_simp.norm_tac ctxt (@{thms congr_rls}, prems)) |
|
139 |
|
140 fun hyp_arith_rew_tac ctxt prems = |
|
141 make_rew_tac ctxt |
|
142 (Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, @{thms congr_rls}, prems)) |
|
143 \<close> |
|
144 |
|
145 method_setup arith_rew = \<open> |
|
146 Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths)) |
|
147 \<close> |
|
148 |
|
149 method_setup hyp_arith_rew = \<open> |
|
150 Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths)) |
|
151 \<close> |
|
152 |
|
153 |
|
154 subsection \<open>Addition\<close> |
|
155 |
|
156 text \<open>Associative law for addition.\<close> |
|
157 lemma add_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #+ c = a #+ (b #+ c) : N" |
|
158 apply (NE a) |
|
159 apply hyp_arith_rew |
|
160 done |
|
161 |
|
162 text \<open>Commutative law for addition. Can be proved using three inductions. |
|
163 Must simplify after first induction! Orientation of rewrites is delicate.\<close> |
|
164 lemma add_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b = b #+ a : N" |
|
165 apply (NE a) |
|
166 apply hyp_arith_rew |
|
167 apply (rule sym_elem) |
|
168 prefer 2 |
|
169 apply (NE b) |
|
170 prefer 4 |
|
171 apply (NE b) |
|
172 apply hyp_arith_rew |
|
173 done |
|
174 |
|
175 |
|
176 subsection \<open>Multiplication\<close> |
|
177 |
|
178 text \<open>Right annihilation in product.\<close> |
|
179 lemma mult_0_right: "a:N \<Longrightarrow> a #* 0 = 0 : N" |
|
180 apply (NE a) |
|
181 apply hyp_arith_rew |
|
182 done |
|
183 |
|
184 text \<open>Right successor law for multiplication.\<close> |
|
185 lemma mult_succ_right: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* succ(b) = a #+ (a #* b) : N" |
|
186 apply (NE a) |
|
187 apply (hyp_arith_rew add_assoc [THEN sym_elem]) |
|
188 apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ |
|
189 done |
|
190 |
|
191 text \<open>Commutative law for multiplication.\<close> |
|
192 lemma mult_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b = b #* a : N" |
|
193 apply (NE a) |
|
194 apply (hyp_arith_rew mult_0_right mult_succ_right) |
|
195 done |
|
196 |
|
197 text \<open>Addition distributes over multiplication.\<close> |
|
198 lemma add_mult_distrib: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" |
|
199 apply (NE a) |
|
200 apply (hyp_arith_rew add_assoc [THEN sym_elem]) |
|
201 done |
|
202 |
|
203 text \<open>Associative law for multiplication.\<close> |
|
204 lemma mult_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #* b) #* c = a #* (b #* c) : N" |
|
205 apply (NE a) |
|
206 apply (hyp_arith_rew add_mult_distrib) |
|
207 done |
|
208 |
|
209 |
|
210 subsection \<open>Difference\<close> |
|
211 |
|
212 text \<open> |
|
213 Difference on natural numbers, without negative numbers |
|
214 \<^item> \<open>a - b = 0\<close> iff \<open>a \<le> b\<close> |
|
215 \<^item> \<open>a - b = succ(c)\<close> iff \<open>a > b\<close> |
|
216 \<close> |
|
217 |
|
218 lemma diff_self_eq_0: "a:N \<Longrightarrow> a - a = 0 : N" |
|
219 apply (NE a) |
|
220 apply hyp_arith_rew |
|
221 done |
|
222 |
|
223 |
|
224 lemma add_0_right: "\<lbrakk>c : N; 0 : N; c : N\<rbrakk> \<Longrightarrow> c #+ 0 = c : N" |
|
225 by (rule addC0 [THEN [3] add_commute [THEN trans_elem]]) |
|
226 |
|
227 text \<open> |
|
228 Addition is the inverse of subtraction: if \<open>b \<le> x\<close> then \<open>b #+ (x - b) = x\<close>. |
|
229 An example of induction over a quantified formula (a product). |
|
230 Uses rewriting with a quantified, implicative inductive hypothesis. |
|
231 \<close> |
|
232 schematic_goal add_diff_inverse_lemma: |
|
233 "b:N \<Longrightarrow> ?a : \<Prod>x:N. Eq(N, b-x, 0) \<longrightarrow> Eq(N, b #+ (x-b), x)" |
|
234 apply (NE b) |
|
235 \<comment> \<open>strip one "universal quantifier" but not the "implication"\<close> |
|
236 apply (rule_tac [3] intr_rls) |
|
237 \<comment> \<open>case analysis on \<open>x\<close> in \<open>succ(u) \<le> x \<longrightarrow> succ(u) #+ (x - succ(u)) = x\<close>\<close> |
|
238 prefer 4 |
|
239 apply (NE x) |
|
240 apply assumption |
|
241 \<comment> \<open>Prepare for simplification of types -- the antecedent \<open>succ(u) \<le> x\<close>\<close> |
|
242 apply (rule_tac [2] replace_type) |
|
243 apply (rule_tac [1] replace_type) |
|
244 apply arith_rew |
|
245 \<comment> \<open>Solves first 0 goal, simplifies others. Two sugbgoals remain. |
|
246 Both follow by rewriting, (2) using quantified induction hyp.\<close> |
|
247 apply intr \<comment> \<open>strips remaining \<open>\<Prod>\<close>s\<close> |
|
248 apply (hyp_arith_rew add_0_right) |
|
249 apply assumption |
|
250 done |
|
251 |
|
252 text \<open> |
|
253 Version of above with premise \<open>b - a = 0\<close> i.e. \<open>a \<ge> b\<close>. |
|
254 Using @{thm ProdE} does not work -- for \<open>?B(?a)\<close> is ambiguous. |
|
255 Instead, @{thm add_diff_inverse_lemma} states the desired induction scheme; |
|
256 the use of \<open>THEN\<close> below instantiates Vars in @{thm ProdE} automatically. |
|
257 \<close> |
|
258 lemma add_diff_inverse: "\<lbrakk>a:N; b:N; b - a = 0 : N\<rbrakk> \<Longrightarrow> b #+ (a-b) = a : N" |
|
259 apply (rule EqE) |
|
260 apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE]) |
|
261 apply (assumption | rule EqI)+ |
|
262 done |
|
263 |
|
264 |
|
265 subsection \<open>Absolute difference\<close> |
|
266 |
|
267 text \<open>Typing of absolute difference: short and long versions.\<close> |
|
268 |
|
269 lemma absdiff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b : N" |
|
270 unfolding arith_defs by typechk |
|
271 |
|
272 lemma absdiff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a |-| b = c |-| d : N" |
|
273 unfolding arith_defs by equal |
|
274 |
|
275 lemma absdiff_self_eq_0: "a:N \<Longrightarrow> a |-| a = 0 : N" |
|
276 unfolding absdiff_def by (arith_rew diff_self_eq_0) |
|
277 |
|
278 lemma absdiffC0: "a:N \<Longrightarrow> 0 |-| a = a : N" |
|
279 unfolding absdiff_def by hyp_arith_rew |
|
280 |
|
281 lemma absdiff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) |-| succ(b) = a |-| b : N" |
|
282 unfolding absdiff_def by hyp_arith_rew |
|
283 |
|
284 text \<open>Note how easy using commutative laws can be? ...not always...\<close> |
|
285 lemma absdiff_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b = b |-| a : N" |
|
286 unfolding absdiff_def |
|
287 apply (rule add_commute) |
|
288 apply (typechk diff_typing) |
|
289 done |
|
290 |
|
291 text \<open>If \<open>a + b = 0\<close> then \<open>a = 0\<close>. Surprisingly tedious.\<close> |
|
292 schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : Eq(N,a#+b,0) \<longrightarrow> Eq(N,a,0)" |
|
293 apply (NE a) |
|
294 apply (rule_tac [3] replace_type) |
|
295 apply arith_rew |
|
296 apply intr \<comment> \<open>strips remaining \<open>\<Prod>\<close>s\<close> |
|
297 apply (rule_tac [2] zero_ne_succ [THEN FE]) |
|
298 apply (erule_tac [3] EqE [THEN sym_elem]) |
|
299 apply (typechk add_typing) |
|
300 done |
|
301 |
|
302 text \<open> |
|
303 Version of above with the premise \<open>a + b = 0\<close>. |
|
304 Again, resolution instantiates variables in @{thm ProdE}. |
|
305 \<close> |
|
306 lemma add_eq0: "\<lbrakk>a:N; b:N; a #+ b = 0 : N\<rbrakk> \<Longrightarrow> a = 0 : N" |
|
307 apply (rule EqE) |
|
308 apply (rule add_eq0_lemma [THEN ProdE]) |
|
309 apply (rule_tac [3] EqI) |
|
310 apply typechk |
|
311 done |
|
312 |
|
313 text \<open>Here is a lemma to infer \<open>a - b = 0\<close> and \<open>b - a = 0\<close> from \<open>a |-| b = 0\<close>, below.\<close> |
|
314 schematic_goal absdiff_eq0_lem: |
|
315 "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : Eq(N, a-b, 0) \<times> Eq(N, b-a, 0)" |
|
316 apply (unfold absdiff_def) |
|
317 apply intr |
|
318 apply eqintr |
|
319 apply (rule_tac [2] add_eq0) |
|
320 apply (rule add_eq0) |
|
321 apply (rule_tac [6] add_commute [THEN trans_elem]) |
|
322 apply (typechk diff_typing) |
|
323 done |
|
324 |
|
325 text \<open>If \<open>a |-| b = 0\<close> then \<open>a = b\<close> |
|
326 proof: \<open>a - b = 0\<close> and \<open>b - a = 0\<close>, so \<open>b = a + (b - a) = a + 0 = a\<close>. |
|
327 \<close> |
|
328 lemma absdiff_eq0: "\<lbrakk>a |-| b = 0 : N; a:N; b:N\<rbrakk> \<Longrightarrow> a = b : N" |
|
329 apply (rule EqE) |
|
330 apply (rule absdiff_eq0_lem [THEN SumE]) |
|
331 apply eqintr |
|
332 apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) |
|
333 apply (erule_tac [3] EqE) |
|
334 apply (hyp_arith_rew add_0_right) |
|
335 done |
|
336 |
|
337 |
|
338 subsection \<open>Remainder and Quotient\<close> |
|
339 |
|
340 text \<open>Typing of remainder: short and long versions.\<close> |
|
341 |
|
342 lemma mod_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b : N" |
|
343 unfolding mod_def by (typechk absdiff_typing) |
|
344 |
|
345 lemma mod_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a mod b = c mod d : N" |
|
346 unfolding mod_def by (equal absdiff_typingL) |
|
347 |
|
348 |
|
349 text \<open>Computation for \<open>mod\<close>: 0 and successor cases.\<close> |
|
350 |
|
351 lemma modC0: "b:N \<Longrightarrow> 0 mod b = 0 : N" |
|
352 unfolding mod_def by (rew absdiff_typing) |
|
353 |
|
354 lemma modC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> |
|
355 succ(a) mod b = rec(succ(a mod b) |-| b, 0, \<lambda>x y. succ(a mod b)) : N" |
|
356 unfolding mod_def by (rew absdiff_typing) |
|
357 |
|
358 |
|
359 text \<open>Typing of quotient: short and long versions.\<close> |
|
360 |
|
361 lemma div_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a div b : N" |
|
362 unfolding div_def by (typechk absdiff_typing mod_typing) |
|
363 |
|
364 lemma div_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a div b = c div d : N" |
|
365 unfolding div_def by (equal absdiff_typingL mod_typingL) |
|
366 |
|
367 lemmas div_typing_rls = mod_typing div_typing absdiff_typing |
|
368 |
|
369 |
|
370 text \<open>Computation for quotient: 0 and successor cases.\<close> |
|
371 |
|
372 lemma divC0: "b:N \<Longrightarrow> 0 div b = 0 : N" |
|
373 unfolding div_def by (rew mod_typing absdiff_typing) |
|
374 |
|
375 lemma divC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> |
|
376 succ(a) div b = rec(succ(a) mod b, succ(a div b), \<lambda>x y. a div b) : N" |
|
377 unfolding div_def by (rew mod_typing) |
|
378 |
|
379 |
|
380 text \<open>Version of above with same condition as the \<open>mod\<close> one.\<close> |
|
381 lemma divC_succ2: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> |
|
382 succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \<lambda>x y. a div b) : N" |
|
383 apply (rule divC_succ [THEN trans_elem]) |
|
384 apply (rew div_typing_rls modC_succ) |
|
385 apply (NE "succ (a mod b) |-|b") |
|
386 apply (rew mod_typing div_typing absdiff_typing) |
|
387 done |
|
388 |
|
389 text \<open>For case analysis on whether a number is 0 or a successor.\<close> |
|
390 lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) : |
|
391 Eq(N,a,0) + (\<Sum>x:N. Eq(N,a, succ(x)))" |
|
392 apply (NE a) |
|
393 apply (rule_tac [3] PlusI_inr) |
|
394 apply (rule_tac [2] PlusI_inl) |
|
395 apply eqintr |
|
396 apply equal |
|
397 done |
|
398 |
|
399 text \<open>Main Result. Holds when \<open>b\<close> is 0 since \<open>a mod 0 = a\<close> and \<open>a div 0 = 0\<close>.\<close> |
|
400 lemma mod_div_equality: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b #+ (a div b) #* b = a : N" |
|
401 apply (NE a) |
|
402 apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) |
|
403 apply (rule EqE) |
|
404 \<comment> \<open>case analysis on \<open>succ(u mod b) |-| b\<close>\<close> |
|
405 apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE]) |
|
406 apply (erule_tac [3] SumE) |
|
407 apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) |
|
408 \<comment> \<open>Replace one occurrence of \<open>b\<close> by \<open>succ(u mod b)\<close>. Clumsy!\<close> |
|
409 apply (rule add_typingL [THEN trans_elem]) |
|
410 apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) |
|
411 apply (rule_tac [3] refl_elem) |
|
412 apply (hyp_arith_rew div_typing_rls) |
|
413 done |
|
414 |
|
415 end |
|