777 with False \<open>a = b * c\<close> show ?thesis |
777 with False \<open>a = b * c\<close> show ?thesis |
778 by simp |
778 by simp |
779 qed |
779 qed |
780 |
780 |
781 end |
781 end |
782 |
|
783 text \<open>Integral (semi)domains with cancellation rules\<close> |
|
784 |
|
785 class semidom_divide_cancel = semidom_divide + |
|
786 assumes div_mult_self1: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b" |
|
787 and div_mult_mult1: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b" |
|
788 begin |
|
789 |
|
790 context |
|
791 fixes b |
|
792 assumes "b \<noteq> 0" |
|
793 begin |
|
794 |
|
795 lemma div_mult_self2: |
|
796 "(a + b * c) div b = c + a div b" |
|
797 using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps) |
|
798 |
|
799 lemma div_mult_self3: |
|
800 "(c * b + a) div b = c + a div b" |
|
801 using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps) |
|
802 |
|
803 lemma div_mult_self4: |
|
804 "(b * c + a) div b = c + a div b" |
|
805 using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a c] by (simp add: ac_simps) |
|
806 |
|
807 lemma div_add_self1: |
|
808 "(b + a) div b = a div b + 1" |
|
809 using \<open>b \<noteq> 0\<close> div_mult_self1 [of b a 1] by (simp add: ac_simps) |
|
810 |
|
811 lemma div_add_self2: |
|
812 "(a + b) div b = a div b + 1" |
|
813 using \<open>b \<noteq> 0\<close> div_add_self1 [of a] by (simp add: ac_simps) |
|
814 |
|
815 end |
|
816 |
|
817 lemma div_mult_mult2: |
|
818 "(a * c) div (b * c) = a div b" if "c \<noteq> 0" |
|
819 using that div_mult_mult1 [of c a b] by (simp add: ac_simps) |
|
820 |
|
821 lemma div_mult_mult1_if [simp]: |
|
822 "(c * a) div (c * b) = (if c = 0 then 0 else a div b)" |
|
823 by (simp add: div_mult_mult1) |
|
824 |
|
825 lemma div_mult_mult2_if [simp]: |
|
826 "(a * c) div (b * c) = (if c = 0 then 0 else a div b)" |
|
827 using div_mult_mult1_if [of c a b] by (simp add: ac_simps) |
|
828 |
|
829 end |
|
830 |
|
831 class idom_divide_cancel = idom_divide + semidom_divide_cancel |
|
832 begin |
|
833 |
|
834 lemma div_minus_minus [simp]: "(- a) div (- b) = a div b" |
|
835 using div_mult_mult1 [of "- 1" a b] by simp |
|
836 |
|
837 lemma div_minus_right: "a div (- b) = (- a) div b" |
|
838 using div_minus_minus [of "- a" b] by simp |
|
839 |
|
840 lemma div_minus1_right [simp]: "a div (- 1) = - a" |
|
841 using div_minus_right [of a 1] by simp |
|
842 |
|
843 end |
|
844 |
|
845 |
|
846 subsection \<open>Basic notions following from divisibility\<close> |
|
847 |
782 |
848 class algebraic_semidom = semidom_divide |
783 class algebraic_semidom = semidom_divide |
849 begin |
784 begin |
850 |
785 |
851 text \<open> |
786 text \<open> |