|
1 theory Normalization_Semidom |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 context algebraic_semidom |
|
6 begin |
|
7 |
|
8 lemma is_unit_divide_mult_cancel_left: |
|
9 assumes "a \<noteq> 0" and "is_unit b" |
|
10 shows "a div (a * b) = 1 div b" |
|
11 proof - |
|
12 from assms have "a div (a * b) = a div a div b" |
|
13 by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq) |
|
14 with assms show ?thesis by simp |
|
15 qed |
|
16 |
|
17 lemma is_unit_divide_mult_cancel_right: |
|
18 assumes "a \<noteq> 0" and "is_unit b" |
|
19 shows "a div (b * a) = 1 div b" |
|
20 using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps) |
|
21 |
|
22 end |
|
23 |
|
24 class normalization_semidom = algebraic_semidom + |
|
25 fixes normalize :: "'a \<Rightarrow> 'a" |
|
26 and unit_factor :: "'a \<Rightarrow> 'a" |
|
27 assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" |
|
28 assumes normalize_0 [simp]: "normalize 0 = 0" |
|
29 and unit_factor_0 [simp]: "unit_factor 0 = 0" |
|
30 assumes is_unit_normalize: |
|
31 "is_unit a \<Longrightarrow> normalize a = 1" |
|
32 assumes unit_factor_is_unit [iff]: |
|
33 "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)" |
|
34 assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" |
|
35 begin |
|
36 |
|
37 lemma unit_factor_dvd [simp]: |
|
38 "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b" |
|
39 by (rule unit_imp_dvd) simp |
|
40 |
|
41 lemma unit_factor_self [simp]: |
|
42 "unit_factor a dvd a" |
|
43 by (cases "a = 0") simp_all |
|
44 |
|
45 lemma normalize_mult_unit_factor [simp]: |
|
46 "normalize a * unit_factor a = a" |
|
47 using unit_factor_mult_normalize [of a] by (simp add: ac_simps) |
|
48 |
|
49 lemma normalize_eq_0_iff [simp]: |
|
50 "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q") |
|
51 proof |
|
52 assume ?P |
|
53 moreover have "unit_factor a * normalize a = a" by simp |
|
54 ultimately show ?Q by simp |
|
55 next |
|
56 assume ?Q then show ?P by simp |
|
57 qed |
|
58 |
|
59 lemma unit_factor_eq_0_iff [simp]: |
|
60 "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q") |
|
61 proof |
|
62 assume ?P |
|
63 moreover have "unit_factor a * normalize a = a" by simp |
|
64 ultimately show ?Q by simp |
|
65 next |
|
66 assume ?Q then show ?P by simp |
|
67 qed |
|
68 |
|
69 lemma is_unit_unit_factor: |
|
70 assumes "is_unit a" shows "unit_factor a = a" |
|
71 proof - |
|
72 from assms have "normalize a = 1" by (rule is_unit_normalize) |
|
73 moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" . |
|
74 ultimately show ?thesis by simp |
|
75 qed |
|
76 |
|
77 lemma unit_factor_1 [simp]: |
|
78 "unit_factor 1 = 1" |
|
79 by (rule is_unit_unit_factor) simp |
|
80 |
|
81 lemma normalize_1 [simp]: |
|
82 "normalize 1 = 1" |
|
83 by (rule is_unit_normalize) simp |
|
84 |
|
85 lemma normalize_1_iff: |
|
86 "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q") |
|
87 proof |
|
88 assume ?Q then show ?P by (rule is_unit_normalize) |
|
89 next |
|
90 assume ?P |
|
91 then have "a \<noteq> 0" by auto |
|
92 from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1" |
|
93 by simp |
|
94 then have "unit_factor a = a" |
|
95 by simp |
|
96 moreover have "is_unit (unit_factor a)" |
|
97 using \<open>a \<noteq> 0\<close> by simp |
|
98 ultimately show ?Q by simp |
|
99 qed |
|
100 |
|
101 lemma div_normalize [simp]: |
|
102 "a div normalize a = unit_factor a" |
|
103 proof (cases "a = 0") |
|
104 case True then show ?thesis by simp |
|
105 next |
|
106 case False then have "normalize a \<noteq> 0" by simp |
|
107 with nonzero_mult_divide_cancel_right |
|
108 have "unit_factor a * normalize a div normalize a = unit_factor a" by blast |
|
109 then show ?thesis by simp |
|
110 qed |
|
111 |
|
112 lemma div_unit_factor [simp]: |
|
113 "a div unit_factor a = normalize a" |
|
114 proof (cases "a = 0") |
|
115 case True then show ?thesis by simp |
|
116 next |
|
117 case False then have "unit_factor a \<noteq> 0" by simp |
|
118 with nonzero_mult_divide_cancel_left |
|
119 have "unit_factor a * normalize a div unit_factor a = normalize a" by blast |
|
120 then show ?thesis by simp |
|
121 qed |
|
122 |
|
123 lemma normalize_div [simp]: |
|
124 "normalize a div a = 1 div unit_factor a" |
|
125 proof (cases "a = 0") |
|
126 case True then show ?thesis by simp |
|
127 next |
|
128 case False |
|
129 have "normalize a div a = normalize a div (unit_factor a * normalize a)" |
|
130 by simp |
|
131 also have "\<dots> = 1 div unit_factor a" |
|
132 using False by (subst is_unit_divide_mult_cancel_right) simp_all |
|
133 finally show ?thesis . |
|
134 qed |
|
135 |
|
136 lemma mult_one_div_unit_factor [simp]: |
|
137 "a * (1 div unit_factor b) = a div unit_factor b" |
|
138 by (cases "b = 0") simp_all |
|
139 |
|
140 lemma normalize_mult: |
|
141 "normalize (a * b) = normalize a * normalize b" |
|
142 proof (cases "a = 0 \<or> b = 0") |
|
143 case True then show ?thesis by auto |
|
144 next |
|
145 case False |
|
146 from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" . |
|
147 then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp |
|
148 also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps) |
|
149 also have "\<dots> = a * b div unit_factor b div unit_factor a" |
|
150 using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) |
|
151 also have "\<dots> = a * (b div unit_factor b) div unit_factor a" |
|
152 using False by (subst unit_div_mult_swap) simp_all |
|
153 also have "\<dots> = normalize a * normalize b" |
|
154 using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) |
|
155 finally show ?thesis . |
|
156 qed |
|
157 |
|
158 lemma unit_factor_idem [simp]: |
|
159 "unit_factor (unit_factor a) = unit_factor a" |
|
160 by (cases "a = 0") (auto intro: is_unit_unit_factor) |
|
161 |
|
162 lemma normalize_unit_factor [simp]: |
|
163 "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1" |
|
164 by (rule is_unit_normalize) simp |
|
165 |
|
166 lemma normalize_idem [simp]: |
|
167 "normalize (normalize a) = normalize a" |
|
168 proof (cases "a = 0") |
|
169 case True then show ?thesis by simp |
|
170 next |
|
171 case False |
|
172 have "normalize a = normalize (unit_factor a * normalize a)" by simp |
|
173 also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)" |
|
174 by (simp only: normalize_mult) |
|
175 finally show ?thesis using False by simp_all |
|
176 qed |
|
177 |
|
178 lemma unit_factor_normalize [simp]: |
|
179 assumes "a \<noteq> 0" |
|
180 shows "unit_factor (normalize a) = 1" |
|
181 proof - |
|
182 from assms have "normalize a \<noteq> 0" by simp |
|
183 have "unit_factor (normalize a) * normalize (normalize a) = normalize a" |
|
184 by (simp only: unit_factor_mult_normalize) |
|
185 then have "unit_factor (normalize a) * normalize a = normalize a" |
|
186 by simp |
|
187 with \<open>normalize a \<noteq> 0\<close> |
|
188 have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" |
|
189 by simp |
|
190 with \<open>normalize a \<noteq> 0\<close> |
|
191 show ?thesis by simp |
|
192 qed |
|
193 |
|
194 lemma dvd_unit_factor_div: |
|
195 assumes "b dvd a" |
|
196 shows "unit_factor (a div b) = unit_factor a div unit_factor b" |
|
197 proof - |
|
198 from assms have "a = a div b * b" |
|
199 by simp |
|
200 then have "unit_factor a = unit_factor (a div b * b)" |
|
201 by simp |
|
202 then show ?thesis |
|
203 by (cases "b = 0") (simp_all add: unit_factor_mult) |
|
204 qed |
|
205 |
|
206 lemma dvd_normalize_div: |
|
207 assumes "b dvd a" |
|
208 shows "normalize (a div b) = normalize a div normalize b" |
|
209 proof - |
|
210 from assms have "a = a div b * b" |
|
211 by simp |
|
212 then have "normalize a = normalize (a div b * b)" |
|
213 by simp |
|
214 then show ?thesis |
|
215 by (cases "b = 0") (simp_all add: normalize_mult) |
|
216 qed |
|
217 |
|
218 lemma normalize_dvd_iff [simp]: |
|
219 "normalize a dvd b \<longleftrightarrow> a dvd b" |
|
220 proof - |
|
221 have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b" |
|
222 using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b] |
|
223 by (cases "a = 0") simp_all |
|
224 then show ?thesis by simp |
|
225 qed |
|
226 |
|
227 lemma dvd_normalize_iff [simp]: |
|
228 "a dvd normalize b \<longleftrightarrow> a dvd b" |
|
229 proof - |
|
230 have "a dvd normalize b \<longleftrightarrow> a dvd normalize b * unit_factor b" |
|
231 using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"] |
|
232 by (cases "b = 0") simp_all |
|
233 then show ?thesis by simp |
|
234 qed |
|
235 |
|
236 lemma associated_normalize_left [simp]: |
|
237 "associated (normalize a) b \<longleftrightarrow> associated a b" |
|
238 by (auto simp add: associated_def) |
|
239 |
|
240 lemma associated_normalize_right [simp]: |
|
241 "associated a (normalize b) \<longleftrightarrow> associated a b" |
|
242 by (auto simp add: associated_def) |
|
243 |
|
244 lemma associated_iff_normalize: |
|
245 "associated a b \<longleftrightarrow> normalize a = normalize b" (is "?P \<longleftrightarrow> ?Q") |
|
246 proof (cases "a = 0 \<or> b = 0") |
|
247 case True then show ?thesis by auto |
|
248 next |
|
249 case False |
|
250 show ?thesis |
|
251 proof |
|
252 assume ?P then show ?Q |
|
253 by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize) |
|
254 next |
|
255 from False have *: "is_unit (unit_factor a div unit_factor b)" |
|
256 by auto |
|
257 assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b" |
|
258 by simp |
|
259 then have "a = unit_factor a * (b div unit_factor b)" |
|
260 by simp |
|
261 with False have "a = (unit_factor a div unit_factor b) * b" |
|
262 by (simp add: unit_div_commute unit_div_mult_swap [symmetric]) |
|
263 with * show ?P |
|
264 by (rule is_unit_associatedI) |
|
265 qed |
|
266 qed |
|
267 |
|
268 lemma normalize_power: |
|
269 "normalize (a ^ n) = normalize a ^ n" |
|
270 by (induct n) (simp_all add: normalize_mult) |
|
271 |
|
272 lemma unit_factor_power: |
|
273 "unit_factor (a ^ n) = unit_factor a ^ n" |
|
274 by (induct n) (simp_all add: unit_factor_mult) |
|
275 |
|
276 lemma associated_eqI: |
|
277 assumes "associated a b" |
|
278 assumes "unit_factor a \<in> {0, 1}" and "unit_factor b \<in> {0, 1}" |
|
279 shows "a = b" |
|
280 proof (cases "a = 0") |
|
281 case True with assms show ?thesis by simp |
|
282 next |
|
283 case False with assms have "b \<noteq> 0" by auto |
|
284 with False assms have "unit_factor a = unit_factor b" |
|
285 by simp |
|
286 moreover from assms have "normalize a = normalize b" |
|
287 by (simp add: associated_iff_normalize) |
|
288 ultimately have "unit_factor a * normalize a = unit_factor b * normalize b" |
|
289 by simp |
|
290 then show ?thesis |
|
291 by simp |
|
292 qed |
|
293 |
|
294 end |
|
295 |
|
296 instantiation nat :: normalization_semidom |
|
297 begin |
|
298 |
|
299 definition normalize_nat |
|
300 where [simp]: "normalize = (id :: nat \<Rightarrow> nat)" |
|
301 |
|
302 definition unit_factor_nat |
|
303 where "unit_factor n = (if n = 0 then 0 else 1 :: nat)" |
|
304 |
|
305 lemma unit_factor_simps [simp]: |
|
306 "unit_factor 0 = (0::nat)" |
|
307 "unit_factor (Suc n) = 1" |
|
308 by (simp_all add: unit_factor_nat_def) |
|
309 |
|
310 instance |
|
311 by default (simp_all add: unit_factor_nat_def) |
|
312 |
|
313 end |
|
314 |
|
315 instantiation int :: normalization_semidom |
|
316 begin |
|
317 |
|
318 definition normalize_int |
|
319 where [simp]: "normalize = (abs :: int \<Rightarrow> int)" |
|
320 |
|
321 definition unit_factor_int |
|
322 where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)" |
|
323 |
|
324 instance |
|
325 proof |
|
326 fix k :: int |
|
327 assume "k \<noteq> 0" |
|
328 then have "\<bar>sgn k\<bar> = 1" |
|
329 by (cases "0::int" k rule: linorder_cases) simp_all |
|
330 then show "is_unit (unit_factor k)" |
|
331 by simp |
|
332 qed (simp_all add: sgn_times mult_sgn_abs) |
|
333 |
|
334 end |
|
335 |
|
336 end |