154 lemma INum_int [simp]: "INum (i)\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" |
154 lemma INum_int [simp]: "INum (i)\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" |
155 by (simp_all add: INum_def) |
155 by (simp_all add: INum_def) |
156 |
156 |
157 lemma isnormNum_unique[simp]: |
157 lemma isnormNum_unique[simp]: |
158 assumes na: "isnormNum x" and nb: "isnormNum y" |
158 assumes na: "isnormNum x" and nb: "isnormNum y" |
159 shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs") |
159 shows "((INum x ::'a::{field_char_0, field}) = INum y) = (x = y)" (is "?lhs = ?rhs") |
160 proof |
160 proof |
161 obtain a b where x: "x = (a, b)" by (cases x) |
161 obtain a b where x: "x = (a, b)" by (cases x) |
162 obtain a' b' where y: "y = (a', b')" by (cases y) |
162 obtain a' b' where y: "y = (a', b')" by (cases y) |
163 assume H: ?lhs |
163 assume H: ?lhs |
164 { assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" |
164 { assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" |
211 |
211 |
212 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==> |
212 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==> |
213 (of_int(n div d)::'a::field_char_0) = of_int n / of_int d" |
213 (of_int(n div d)::'a::field_char_0) = of_int n / of_int d" |
214 using of_int_div_aux [of d n, where ?'a = 'a] by simp |
214 using of_int_div_aux [of d n, where ?'a = 'a] by simp |
215 |
215 |
216 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})" |
216 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field})" |
217 proof - |
217 proof - |
218 obtain a b where x: "x = (a, b)" by (cases x) |
218 obtain a b where x: "x = (a, b)" by (cases x) |
219 { assume "a = 0 \<or> b = 0" |
219 { assume "a = 0 \<or> b = 0" |
220 hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) } |
220 hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) } |
221 moreover |
221 moreover |
226 have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) } |
226 have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) } |
227 ultimately show ?thesis by blast |
227 ultimately show ?thesis by blast |
228 qed |
228 qed |
229 |
229 |
230 lemma INum_normNum_iff: |
230 lemma INum_normNum_iff: |
231 "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y" |
231 "(INum x ::'a::{field_char_0, field}) = INum y \<longleftrightarrow> normNum x = normNum y" |
232 (is "?lhs = ?rhs") |
232 (is "?lhs = ?rhs") |
233 proof - |
233 proof - |
234 have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)" |
234 have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)" |
235 by (simp del: normNum) |
235 by (simp del: normNum) |
236 also have "\<dots> = ?lhs" by simp |
236 also have "\<dots> = ?lhs" by simp |
237 finally show ?thesis by simp |
237 finally show ?thesis by simp |
238 qed |
238 qed |
239 |
239 |
240 lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})" |
240 lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field})" |
241 proof - |
241 proof - |
242 let ?z = "0:: 'a" |
242 let ?z = "0:: 'a" |
243 obtain a b where x: "x = (a, b)" by (cases x) |
243 obtain a b where x: "x = (a, b)" by (cases x) |
244 obtain a' b' where y: "y = (a', b')" by (cases y) |
244 obtain a' b' where y: "y = (a', b')" by (cases y) |
245 { assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" |
245 { assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" |
272 ultimately have ?thesis using aa' bb' |
272 ultimately have ?thesis using aa' bb' |
273 by (simp add: x y Nadd_def INum_def normNum_def Let_def) } |
273 by (simp add: x y Nadd_def INum_def normNum_def Let_def) } |
274 ultimately show ?thesis by blast |
274 ultimately show ?thesis by blast |
275 qed |
275 qed |
276 |
276 |
277 lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})" |
277 lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field})" |
278 proof - |
278 proof - |
279 let ?z = "0::'a" |
279 let ?z = "0::'a" |
280 obtain a b where x: "x = (a, b)" by (cases x) |
280 obtain a b where x: "x = (a, b)" by (cases x) |
281 obtain a' b' where y: "y = (a', b')" by (cases y) |
281 obtain a' b' where y: "y = (a', b')" by (cases y) |
282 { assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" |
282 { assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" |
296 qed |
296 qed |
297 |
297 |
298 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)" |
298 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)" |
299 by (simp add: Nneg_def split_def INum_def) |
299 by (simp add: Nneg_def split_def INum_def) |
300 |
300 |
301 lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})" |
301 lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field})" |
302 by (simp add: Nsub_def split_def) |
302 by (simp add: Nsub_def split_def) |
303 |
303 |
304 lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)" |
304 lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field) / (INum x)" |
305 by (simp add: Ninv_def INum_def split_def) |
305 by (simp add: Ninv_def INum_def split_def) |
306 |
306 |
307 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" |
307 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field})" |
308 by (simp add: Ndiv_def) |
308 by (simp add: Ndiv_def) |
309 |
309 |
310 lemma Nlt0_iff[simp]: |
310 lemma Nlt0_iff[simp]: |
311 assumes nx: "isnormNum x" |
311 assumes nx: "isnormNum x" |
312 shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x" |
312 shows "((INum x :: 'a :: {field_char_0, linordered_field})< 0) = 0>\<^sub>N x" |
313 proof - |
313 proof - |
314 obtain a b where x: "x = (a, b)" by (cases x) |
314 obtain a b where x: "x = (a, b)" by (cases x) |
315 { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) } |
315 { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) } |
316 moreover |
316 moreover |
317 { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0" |
317 { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0" |
375 finally show ?thesis by (simp add: Nlt_def) |
375 finally show ?thesis by (simp add: Nlt_def) |
376 qed |
376 qed |
377 |
377 |
378 lemma Nle_iff[simp]: |
378 lemma Nle_iff[simp]: |
379 assumes nx: "isnormNum x" and ny: "isnormNum y" |
379 assumes nx: "isnormNum x" and ny: "isnormNum y" |
380 shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)" |
380 shows "((INum x :: 'a :: {field_char_0, linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)" |
381 proof - |
381 proof - |
382 have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" |
382 have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" |
383 using nx ny by simp |
383 using nx ny by simp |
384 also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" |
384 also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" |
385 using Nle0_iff[OF Nsub_normN[OF ny]] by simp |
385 using Nle0_iff[OF Nsub_normN[OF ny]] by simp |
386 finally show ?thesis by (simp add: Nle_def) |
386 finally show ?thesis by (simp add: Nle_def) |
387 qed |
387 qed |
388 |
388 |
389 lemma Nadd_commute: |
389 lemma Nadd_commute: |
390 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
390 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
391 shows "x +\<^sub>N y = y +\<^sub>N x" |
391 shows "x +\<^sub>N y = y +\<^sub>N x" |
392 proof - |
392 proof - |
393 have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all |
393 have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all |
394 have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp |
394 have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp |
395 with isnormNum_unique[OF n] show ?thesis by simp |
395 with isnormNum_unique[OF n] show ?thesis by simp |
396 qed |
396 qed |
397 |
397 |
398 lemma [simp]: |
398 lemma [simp]: |
399 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
399 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
400 shows "(0, b) +\<^sub>N y = normNum y" |
400 shows "(0, b) +\<^sub>N y = normNum y" |
401 and "(a, 0) +\<^sub>N y = normNum y" |
401 and "(a, 0) +\<^sub>N y = normNum y" |
402 and "x +\<^sub>N (0, b) = normNum x" |
402 and "x +\<^sub>N (0, b) = normNum x" |
403 and "x +\<^sub>N (a, 0) = normNum x" |
403 and "x +\<^sub>N (a, 0) = normNum x" |
404 apply (simp add: Nadd_def split_def) |
404 apply (simp add: Nadd_def split_def) |
406 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
406 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
407 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
407 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
408 done |
408 done |
409 |
409 |
410 lemma normNum_nilpotent_aux[simp]: |
410 lemma normNum_nilpotent_aux[simp]: |
411 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
411 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
412 assumes nx: "isnormNum x" |
412 assumes nx: "isnormNum x" |
413 shows "normNum x = x" |
413 shows "normNum x = x" |
414 proof - |
414 proof - |
415 let ?a = "normNum x" |
415 let ?a = "normNum x" |
416 have n: "isnormNum ?a" by simp |
416 have n: "isnormNum ?a" by simp |
417 have th: "INum ?a = (INum x ::'a)" by simp |
417 have th: "INum ?a = (INum x ::'a)" by simp |
418 with isnormNum_unique[OF n nx] show ?thesis by simp |
418 with isnormNum_unique[OF n nx] show ?thesis by simp |
419 qed |
419 qed |
420 |
420 |
421 lemma normNum_nilpotent[simp]: |
421 lemma normNum_nilpotent[simp]: |
422 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
422 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
423 shows "normNum (normNum x) = normNum x" |
423 shows "normNum (normNum x) = normNum x" |
424 by simp |
424 by simp |
425 |
425 |
426 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N" |
426 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N" |
427 by (simp_all add: normNum_def) |
427 by (simp_all add: normNum_def) |
428 |
428 |
429 lemma normNum_Nadd: |
429 lemma normNum_Nadd: |
430 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
430 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
431 shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp |
431 shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp |
432 |
432 |
433 lemma Nadd_normNum1[simp]: |
433 lemma Nadd_normNum1[simp]: |
434 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
434 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
435 shows "normNum x +\<^sub>N y = x +\<^sub>N y" |
435 shows "normNum x +\<^sub>N y = x +\<^sub>N y" |
436 proof - |
436 proof - |
437 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all |
437 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all |
438 have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp |
438 have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp |
439 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
439 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
440 finally show ?thesis using isnormNum_unique[OF n] by simp |
440 finally show ?thesis using isnormNum_unique[OF n] by simp |
441 qed |
441 qed |
442 |
442 |
443 lemma Nadd_normNum2[simp]: |
443 lemma Nadd_normNum2[simp]: |
444 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
444 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
445 shows "x +\<^sub>N normNum y = x +\<^sub>N y" |
445 shows "x +\<^sub>N normNum y = x +\<^sub>N y" |
446 proof - |
446 proof - |
447 have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all |
447 have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all |
448 have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp |
448 have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp |
449 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
449 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
450 finally show ?thesis using isnormNum_unique[OF n] by simp |
450 finally show ?thesis using isnormNum_unique[OF n] by simp |
451 qed |
451 qed |
452 |
452 |
453 lemma Nadd_assoc: |
453 lemma Nadd_assoc: |
454 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
454 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
455 shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" |
455 shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" |
456 proof - |
456 proof - |
457 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all |
457 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all |
458 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
458 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
459 with isnormNum_unique[OF n] show ?thesis by simp |
459 with isnormNum_unique[OF n] show ?thesis by simp |
461 |
461 |
462 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x" |
462 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x" |
463 by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute) |
463 by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute) |
464 |
464 |
465 lemma Nmul_assoc: |
465 lemma Nmul_assoc: |
466 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
466 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
467 assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z" |
467 assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z" |
468 shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" |
468 shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" |
469 proof - |
469 proof - |
470 from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" |
470 from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" |
471 by simp_all |
471 by simp_all |
472 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
472 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
473 with isnormNum_unique[OF n] show ?thesis by simp |
473 with isnormNum_unique[OF n] show ?thesis by simp |
474 qed |
474 qed |
475 |
475 |
476 lemma Nsub0: |
476 lemma Nsub0: |
477 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
477 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
478 assumes x: "isnormNum x" and y: "isnormNum y" |
478 assumes x: "isnormNum x" and y: "isnormNum y" |
479 shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y" |
479 shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y" |
480 proof - |
480 proof - |
481 fix h :: 'a |
481 fix h :: 'a |
482 from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] |
482 from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] |
488 |
488 |
489 lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N" |
489 lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N" |
490 by (simp_all add: Nmul_def Let_def split_def) |
490 by (simp_all add: Nmul_def Let_def split_def) |
491 |
491 |
492 lemma Nmul_eq0[simp]: |
492 lemma Nmul_eq0[simp]: |
493 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
493 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
494 assumes nx: "isnormNum x" and ny: "isnormNum y" |
494 assumes nx: "isnormNum x" and ny: "isnormNum y" |
495 shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N" |
495 shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N" |
496 proof - |
496 proof - |
497 fix h :: 'a |
497 fix h :: 'a |
498 obtain a b where x: "x = (a, b)" by (cases x) |
498 obtain a b where x: "x = (a, b)" by (cases x) |