107 text {* Abstract divisibility *} |
107 text {* Abstract divisibility *} |
108 |
108 |
109 class dvd = times |
109 class dvd = times |
110 begin |
110 begin |
111 |
111 |
112 definition |
112 definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where |
113 dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) |
113 [code del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)" |
114 where |
|
115 [code func del]: "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)" |
|
116 |
114 |
117 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a" |
115 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a" |
118 unfolding dvd_def .. |
116 unfolding dvd_def .. |
119 |
117 |
120 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P" |
118 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P" |
127 begin |
125 begin |
128 |
126 |
129 subclass semiring_1 .. |
127 subclass semiring_1 .. |
130 |
128 |
131 lemma dvd_refl: "a dvd a" |
129 lemma dvd_refl: "a dvd a" |
132 proof - |
130 proof |
133 have "a = a * 1" by simp |
131 show "a = a * 1" by simp |
134 then show ?thesis unfolding dvd_def .. |
|
135 qed |
132 qed |
136 |
133 |
137 lemma dvd_trans: |
134 lemma dvd_trans: |
138 assumes "a dvd b" and "b dvd c" |
135 assumes "a dvd b" and "b dvd c" |
139 shows "a dvd c" |
136 shows "a dvd c" |
140 proof - |
137 proof - |
141 from assms obtain v where "b = a * v" unfolding dvd_def by auto |
138 from assms obtain v where "b = a * v" by (auto elim!: dvdE) |
142 moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto |
139 moreover from assms obtain w where "c = b * w" by (auto elim!: dvdE) |
143 ultimately have "c = a * (v * w)" by (simp add: mult_assoc) |
140 ultimately have "c = a * (v * w)" by (simp add: mult_assoc) |
144 then show ?thesis unfolding dvd_def .. |
141 then show ?thesis .. |
145 qed |
142 qed |
146 |
143 |
147 lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0" |
144 lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0" |
148 unfolding dvd_def by simp |
145 by (auto intro: dvd_refl elim!: dvdE) |
149 |
146 |
150 lemma dvd_0 [simp]: "a dvd 0" |
147 lemma dvd_0_right [iff]: "a dvd 0" |
151 unfolding dvd_def proof |
148 proof |
152 show "0 = a * 0" by simp |
149 show "0 = a * 0" by simp |
153 qed |
150 qed |
154 |
151 |
155 lemma one_dvd [simp]: "1 dvd a" |
152 lemma one_dvd [simp]: "1 dvd a" |
156 unfolding dvd_def by simp |
153 by (auto intro!: dvdI) |
157 |
154 |
158 lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)" |
155 lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)" |
159 unfolding dvd_def by (blast intro: mult_left_commute) |
156 by (auto intro!: mult_left_commute dvdI elim!: dvdE) |
160 |
157 |
161 lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)" |
158 lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)" |
162 apply (subst mult_commute) |
159 apply (subst mult_commute) |
163 apply (erule dvd_mult) |
160 apply (erule dvd_mult) |
164 done |
161 done |
183 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c" |
180 lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c" |
184 by (simp add: dvd_def mult_assoc, blast) |
181 by (simp add: dvd_def mult_assoc, blast) |
185 |
182 |
186 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c" |
183 lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c" |
187 unfolding mult_ac [of a] by (rule dvd_mult_left) |
184 unfolding mult_ac [of a] by (rule dvd_mult_left) |
188 |
|
189 lemma dvd_0_right [iff]: "a dvd 0" |
|
190 proof - |
|
191 have "0 = a * 0" by simp |
|
192 then show ?thesis unfolding dvd_def .. |
|
193 qed |
|
194 |
185 |
195 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0" |
186 lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0" |
196 by simp |
187 by simp |
197 |
188 |
198 lemma dvd_add: |
189 lemma dvd_add: |
531 "a / 0 = (0::'a::{field,division_by_zero})" |
522 "a / 0 = (0::'a::{field,division_by_zero})" |
532 by (simp add: divide_inverse) |
523 by (simp add: divide_inverse) |
533 |
524 |
534 lemma divide_self_if [simp]: |
525 lemma divide_self_if [simp]: |
535 "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" |
526 "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" |
536 by (simp add: divide_self) |
527 by simp |
537 |
528 |
538 class mult_mono = times + zero + ord + |
529 class mult_mono = times + zero + ord + |
539 assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" |
530 assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" |
540 assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" |
531 assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" |
541 |
532 |