683 |
684 |
684 notation (xsymbols) |
685 notation (xsymbols) |
685 Rats ("\<rat>") |
686 Rats ("\<rat>") |
686 |
687 |
687 end |
688 end |
|
689 |
|
690 lemma Rats_of_rat [simp]: "of_rat r \<in> Rats" |
|
691 by (simp add: Rats_def) |
|
692 |
|
693 lemma Rats_of_int [simp]: "of_int z \<in> Rats" |
|
694 by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat) |
|
695 |
|
696 lemma Rats_of_nat [simp]: "of_nat n \<in> Rats" |
|
697 by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat) |
|
698 |
|
699 lemma Rats_number_of [simp]: |
|
700 "(number_of w::'a::{number_ring,field_char_0}) \<in> Rats" |
|
701 by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat) |
|
702 |
|
703 lemma Rats_0 [simp]: "0 \<in> Rats" |
|
704 apply (unfold Rats_def) |
|
705 apply (rule range_eqI) |
|
706 apply (rule of_rat_0 [symmetric]) |
|
707 done |
|
708 |
|
709 lemma Rats_1 [simp]: "1 \<in> Rats" |
|
710 apply (unfold Rats_def) |
|
711 apply (rule range_eqI) |
|
712 apply (rule of_rat_1 [symmetric]) |
|
713 done |
|
714 |
|
715 lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats" |
|
716 apply (auto simp add: Rats_def) |
|
717 apply (rule range_eqI) |
|
718 apply (rule of_rat_add [symmetric]) |
|
719 done |
|
720 |
|
721 lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats" |
|
722 apply (auto simp add: Rats_def) |
|
723 apply (rule range_eqI) |
|
724 apply (rule of_rat_minus [symmetric]) |
|
725 done |
|
726 |
|
727 lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats" |
|
728 apply (auto simp add: Rats_def) |
|
729 apply (rule range_eqI) |
|
730 apply (rule of_rat_diff [symmetric]) |
|
731 done |
|
732 |
|
733 lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats" |
|
734 apply (auto simp add: Rats_def) |
|
735 apply (rule range_eqI) |
|
736 apply (rule of_rat_mult [symmetric]) |
|
737 done |
|
738 |
|
739 lemma nonzero_Rats_inverse: |
|
740 fixes a :: "'a::field_char_0" |
|
741 shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats" |
|
742 apply (auto simp add: Rats_def) |
|
743 apply (rule range_eqI) |
|
744 apply (erule nonzero_of_rat_inverse [symmetric]) |
|
745 done |
|
746 |
|
747 lemma Rats_inverse [simp]: |
|
748 fixes a :: "'a::{field_char_0,division_by_zero}" |
|
749 shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats" |
|
750 apply (auto simp add: Rats_def) |
|
751 apply (rule range_eqI) |
|
752 apply (rule of_rat_inverse [symmetric]) |
|
753 done |
|
754 |
|
755 lemma nonzero_Rats_divide: |
|
756 fixes a b :: "'a::field_char_0" |
|
757 shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats" |
|
758 apply (auto simp add: Rats_def) |
|
759 apply (rule range_eqI) |
|
760 apply (erule nonzero_of_rat_divide [symmetric]) |
|
761 done |
|
762 |
|
763 lemma Rats_divide [simp]: |
|
764 fixes a b :: "'a::{field_char_0,division_by_zero}" |
|
765 shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats" |
|
766 apply (auto simp add: Rats_def) |
|
767 apply (rule range_eqI) |
|
768 apply (rule of_rat_divide [symmetric]) |
|
769 done |
|
770 |
|
771 lemma Rats_power [simp]: |
|
772 fixes a :: "'a::{field_char_0,recpower}" |
|
773 shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats" |
|
774 apply (auto simp add: Rats_def) |
|
775 apply (rule range_eqI) |
|
776 apply (rule of_rat_power [symmetric]) |
|
777 done |
|
778 |
|
779 lemma Rats_cases [cases set: Rats]: |
|
780 assumes "q \<in> \<rat>" |
|
781 obtains (of_rat) r where "q = of_rat r" |
|
782 unfolding Rats_def |
|
783 proof - |
|
784 from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def . |
|
785 then obtain r where "q = of_rat r" .. |
|
786 then show thesis .. |
|
787 qed |
|
788 |
|
789 lemma Rats_induct [case_names of_rat, induct set: Rats]: |
|
790 "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q" |
|
791 by (rule Rats_cases) auto |
688 |
792 |
689 |
793 |
690 subsection {* Implementation of rational numbers as pairs of integers *} |
794 subsection {* Implementation of rational numbers as pairs of integers *} |
691 |
795 |
692 lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b" |
796 lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b" |