345 show ?thesis |
339 show ?thesis |
346 by (simp add: Nmul_def x y Let_def INum_def) |
340 by (simp add: Nmul_def x y Let_def INum_def) |
347 qed |
341 qed |
348 qed |
342 qed |
349 |
343 |
350 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a::field)" |
344 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x :: 'a::field)" |
351 by (simp add: Nneg_def split_def INum_def) |
345 by (simp add: Nneg_def split_def INum_def) |
352 |
346 |
353 lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0,field})" |
347 lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a::{field_char_0,field})" |
354 by (simp add: Nsub_def split_def) |
348 by (simp add: Nsub_def split_def) |
355 |
349 |
356 lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field) / (INum x)" |
350 lemma Ninv[simp]: "INum (Ninv x) = (1 :: 'a::field) / INum x" |
357 by (simp add: Ninv_def INum_def split_def) |
351 by (simp add: Ninv_def INum_def split_def) |
358 |
352 |
359 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0,field})" |
353 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y :: 'a::{field_char_0,field})" |
360 by (simp add: Ndiv_def) |
354 by (simp add: Ndiv_def) |
361 |
355 |
362 lemma Nlt0_iff[simp]: |
356 lemma Nlt0_iff[simp]: |
363 assumes nx: "isnormNum x" |
357 assumes nx: "isnormNum x" |
364 shows "((INum x :: 'a::{field_char_0,linordered_field})< 0) = 0>\<^sub>N x" |
358 shows "((INum x :: 'a::{field_char_0,linordered_field}) < 0) = 0>\<^sub>N x" |
365 proof - |
359 proof - |
366 obtain a b where x: "x = (a, b)" by (cases x) |
360 obtain a b where x: "x = (a, b)" by (cases x) |
367 show ?thesis |
361 show ?thesis |
368 proof (cases "a = 0") |
362 proof (cases "a = 0") |
369 case True |
363 case True |
399 qed |
393 qed |
400 qed |
394 qed |
401 |
395 |
402 lemma Ngt0_iff[simp]: |
396 lemma Ngt0_iff[simp]: |
403 assumes nx: "isnormNum x" |
397 assumes nx: "isnormNum x" |
404 shows "((INum x :: 'a::{field_char_0,linordered_field})> 0) = 0<\<^sub>N x" |
398 shows "((INum x :: 'a::{field_char_0,linordered_field}) > 0) = 0<\<^sub>N x" |
405 proof - |
399 proof - |
406 obtain a b where x: "x = (a, b)" by (cases x) |
400 obtain a b where x: "x = (a, b)" by (cases x) |
407 show ?thesis |
401 show ?thesis |
408 proof (cases "a = 0") |
402 proof (cases "a = 0") |
409 case True |
403 case True |
419 qed |
413 qed |
420 qed |
414 qed |
421 |
415 |
422 lemma Nge0_iff[simp]: |
416 lemma Nge0_iff[simp]: |
423 assumes nx: "isnormNum x" |
417 assumes nx: "isnormNum x" |
424 shows "((INum x :: 'a::{field_char_0,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x" |
418 shows "(INum x :: 'a::{field_char_0,linordered_field}) \<ge> 0 \<longleftrightarrow> 0\<le>\<^sub>N x" |
425 proof - |
419 proof - |
426 obtain a b where x: "x = (a, b)" by (cases x) |
420 obtain a b where x: "x = (a, b)" by (cases x) |
427 show ?thesis |
421 show ?thesis |
428 proof (cases "a = 0") |
422 proof (cases "a = 0") |
429 case True |
423 case True |
440 qed |
434 qed |
441 |
435 |
442 lemma Nlt_iff[simp]: |
436 lemma Nlt_iff[simp]: |
443 assumes nx: "isnormNum x" |
437 assumes nx: "isnormNum x" |
444 and ny: "isnormNum y" |
438 and ny: "isnormNum y" |
445 shows "((INum x :: 'a::{field_char_0,linordered_field}) < INum y) = (x <\<^sub>N y)" |
439 shows "((INum x :: 'a::{field_char_0,linordered_field}) < INum y) \<longleftrightarrow> x <\<^sub>N y" |
446 proof - |
440 proof - |
447 let ?z = "0::'a" |
441 let ?z = "0::'a" |
448 have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" |
442 have "((INum x ::'a) < INum y) \<longleftrightarrow> INum (x -\<^sub>N y) < ?z" |
449 using nx ny by simp |
443 using nx ny by simp |
450 also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" |
444 also have "\<dots> \<longleftrightarrow> 0>\<^sub>N (x -\<^sub>N y)" |
451 using Nlt0_iff[OF Nsub_normN[OF ny]] by simp |
445 using Nlt0_iff[OF Nsub_normN[OF ny]] by simp |
452 finally show ?thesis |
446 finally show ?thesis |
453 by (simp add: Nlt_def) |
447 by (simp add: Nlt_def) |
454 qed |
448 qed |
455 |
449 |
456 lemma Nle_iff[simp]: |
450 lemma Nle_iff[simp]: |
457 assumes nx: "isnormNum x" |
451 assumes nx: "isnormNum x" |
458 and ny: "isnormNum y" |
452 and ny: "isnormNum y" |
459 shows "((INum x :: 'a::{field_char_0,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)" |
453 shows "((INum x :: 'a::{field_char_0,linordered_field}) \<le> INum y) \<longleftrightarrow> x \<le>\<^sub>N y" |
460 proof - |
454 proof - |
461 have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" |
455 have "((INum x ::'a) \<le> INum y) \<longleftrightarrow> INum (x -\<^sub>N y) \<le> (0::'a)" |
462 using nx ny by simp |
456 using nx ny by simp |
463 also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" |
457 also have "\<dots> \<longleftrightarrow> 0\<ge>\<^sub>N (x -\<^sub>N y)" |
464 using Nle0_iff[OF Nsub_normN[OF ny]] by simp |
458 using Nle0_iff[OF Nsub_normN[OF ny]] by simp |
465 finally show ?thesis |
459 finally show ?thesis |
466 by (simp add: Nle_def) |
460 by (simp add: Nle_def) |
467 qed |
461 qed |
468 |
462 |
506 lemma normNum_nilpotent[simp]: |
500 lemma normNum_nilpotent[simp]: |
507 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
501 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
508 shows "normNum (normNum x) = normNum x" |
502 shows "normNum (normNum x) = normNum x" |
509 by simp |
503 by simp |
510 |
504 |
511 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N" |
505 lemma normNum0[simp]: "normNum (0, b) = 0\<^sub>N" "normNum (a, 0) = 0\<^sub>N" |
512 by (simp_all add: normNum_def) |
506 by (simp_all add: normNum_def) |
513 |
507 |
514 lemma normNum_Nadd: |
508 lemma normNum_Nadd: |
515 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
509 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
516 shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" |
510 shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" |
518 |
512 |
519 lemma Nadd_normNum1[simp]: |
513 lemma Nadd_normNum1[simp]: |
520 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
514 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
521 shows "normNum x +\<^sub>N y = x +\<^sub>N y" |
515 shows "normNum x +\<^sub>N y = x +\<^sub>N y" |
522 proof - |
516 proof - |
523 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all |
517 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" |
524 have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp |
518 by simp_all |
525 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
519 have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" |
526 finally show ?thesis using isnormNum_unique[OF n] by simp |
520 by simp |
|
521 also have "\<dots> = INum (x +\<^sub>N y)" |
|
522 by simp |
|
523 finally show ?thesis |
|
524 using isnormNum_unique[OF n] by simp |
527 qed |
525 qed |
528 |
526 |
529 lemma Nadd_normNum2[simp]: |
527 lemma Nadd_normNum2[simp]: |
530 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
528 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
531 shows "x +\<^sub>N normNum y = x +\<^sub>N y" |
529 shows "x +\<^sub>N normNum y = x +\<^sub>N y" |
532 proof - |
530 proof - |
533 have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all |
531 have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" |
534 have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp |
532 by simp_all |
535 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
533 have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" |
536 finally show ?thesis using isnormNum_unique[OF n] by simp |
534 by simp |
|
535 also have "\<dots> = INum (x +\<^sub>N y)" |
|
536 by simp |
|
537 finally show ?thesis |
|
538 using isnormNum_unique[OF n] by simp |
537 qed |
539 qed |
538 |
540 |
539 lemma Nadd_assoc: |
541 lemma Nadd_assoc: |
540 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
542 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
541 shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" |
543 shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" |
542 proof - |
544 proof - |
543 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all |
545 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" |
544 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
546 by simp_all |
545 with isnormNum_unique[OF n] show ?thesis by simp |
547 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" |
|
548 by simp |
|
549 with isnormNum_unique[OF n] show ?thesis |
|
550 by simp |
546 qed |
551 qed |
547 |
552 |
548 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x" |
553 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x" |
549 by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute) |
554 by (simp add: Nmul_def split_def Let_def gcd_commute_int mult.commute) |
550 |
555 |
555 and nz: "isnormNum z" |
560 and nz: "isnormNum z" |
556 shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" |
561 shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" |
557 proof - |
562 proof - |
558 from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" |
563 from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" |
559 by simp_all |
564 by simp_all |
560 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
565 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" |
561 with isnormNum_unique[OF n] show ?thesis by simp |
566 by simp |
|
567 with isnormNum_unique[OF n] show ?thesis |
|
568 by simp |
562 qed |
569 qed |
563 |
570 |
564 lemma Nsub0: |
571 lemma Nsub0: |
565 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
572 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
566 assumes x: "isnormNum x" |
573 assumes x: "isnormNum x" |
567 and y: "isnormNum y" |
574 and y: "isnormNum y" |
568 shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y" |
575 shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y" |
569 proof - |
576 proof - |
570 from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] |
577 from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] |
571 have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp |
578 have "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)" |
572 also have "\<dots> = (INum x = (INum y :: 'a))" by simp |
579 by simp |
573 also have "\<dots> = (x = y)" using x y by simp |
580 also have "\<dots> \<longleftrightarrow> INum x = (INum y :: 'a)" |
|
581 by simp |
|
582 also have "\<dots> \<longleftrightarrow> x = y" |
|
583 using x y by simp |
574 finally show ?thesis . |
584 finally show ?thesis . |
575 qed |
585 qed |
576 |
586 |
577 lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N" |
587 lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N" |
578 by (simp_all add: Nmul_def Let_def split_def) |
588 by (simp_all add: Nmul_def Let_def split_def) |