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