182 lemma INum_int [simp]: "INum i\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" |
182 lemma INum_int [simp]: "INum i\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" |
183 by (simp_all add: INum_def) |
183 by (simp_all add: INum_def) |
184 |
184 |
185 lemma isnormNum_unique[simp]: |
185 lemma isnormNum_unique[simp]: |
186 assumes na: "isnormNum x" and nb: "isnormNum y" |
186 assumes na: "isnormNum x" and nb: "isnormNum y" |
187 shows "((INum x ::'a::{ring_char_0,field, division_ring_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs") |
187 shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs") |
188 proof |
188 proof |
189 have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto |
189 have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto |
190 then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast |
190 then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast |
191 assume H: ?lhs |
191 assume H: ?lhs |
192 {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" |
192 {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" |
215 next |
215 next |
216 assume ?rhs thus ?lhs by simp |
216 assume ?rhs thus ?lhs by simp |
217 qed |
217 qed |
218 |
218 |
219 |
219 |
220 lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{ring_char_0, field,division_ring_inverse_zero})) = (x = 0\<^sub>N)" |
220 lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)" |
221 unfolding INum_int(2)[symmetric] |
221 unfolding INum_int(2)[symmetric] |
222 by (rule isnormNum_unique, simp_all) |
222 by (rule isnormNum_unique, simp_all) |
223 |
223 |
224 lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::{field, ring_char_0}) / (of_int d) = |
224 lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) = |
225 of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)" |
225 of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)" |
226 proof - |
226 proof - |
227 assume "d ~= 0" |
227 assume "d ~= 0" |
228 hence dz: "of_int d \<noteq> (0::'a)" by (simp add: of_int_eq_0_iff) |
228 hence dz: "of_int d \<noteq> (0::'a)" by (simp add: of_int_eq_0_iff) |
229 let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)" |
229 let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)" |
236 using cong[OF refl[of ?f] eq] by simp |
236 using cong[OF refl[of ?f] eq] by simp |
237 then show ?thesis by (simp add: add_divide_distrib algebra_simps prems) |
237 then show ?thesis by (simp add: add_divide_distrib algebra_simps prems) |
238 qed |
238 qed |
239 |
239 |
240 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==> |
240 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==> |
241 (of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d" |
241 (of_int(n div d)::'a::field_char_0) = of_int n / of_int d" |
242 apply (frule of_int_div_aux [of d n, where ?'a = 'a]) |
242 apply (frule of_int_div_aux [of d n, where ?'a = 'a]) |
243 apply simp |
243 apply simp |
244 apply (simp add: dvd_eq_mod_eq_0) |
244 apply (simp add: dvd_eq_mod_eq_0) |
245 done |
245 done |
246 |
246 |
247 |
247 |
248 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{ring_char_0,field, division_ring_inverse_zero})" |
248 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})" |
249 proof- |
249 proof- |
250 have "\<exists> a b. x = (a,b)" by auto |
250 have "\<exists> a b. x = (a,b)" by auto |
251 then obtain a b where x[simp]: "x = (a,b)" by blast |
251 then obtain a b where x[simp]: "x = (a,b)" by blast |
252 {assume "a=0 \<or> b = 0" hence ?thesis |
252 {assume "a=0 \<or> b = 0" hence ?thesis |
253 by (simp add: INum_def normNum_def split_def Let_def)} |
253 by (simp add: INum_def normNum_def split_def Let_def)} |
258 from of_int_div[OF g, where ?'a = 'a] |
258 from of_int_div[OF g, where ?'a = 'a] |
259 have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)} |
259 have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)} |
260 ultimately show ?thesis by blast |
260 ultimately show ?thesis by blast |
261 qed |
261 qed |
262 |
262 |
263 lemma INum_normNum_iff: "(INum x ::'a::{field, division_ring_inverse_zero, ring_char_0}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs") |
263 lemma INum_normNum_iff: "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs") |
264 proof - |
264 proof - |
265 have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)" |
265 have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)" |
266 by (simp del: normNum) |
266 by (simp del: normNum) |
267 also have "\<dots> = ?lhs" by simp |
267 also have "\<dots> = ?lhs" by simp |
268 finally show ?thesis by simp |
268 finally show ?thesis by simp |
269 qed |
269 qed |
270 |
270 |
271 lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {ring_char_0,division_ring_inverse_zero,field})" |
271 lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})" |
272 proof- |
272 proof- |
273 let ?z = "0:: 'a" |
273 let ?z = "0:: 'a" |
274 have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto |
274 have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto |
275 then obtain a b a' b' where x[simp]: "x = (a,b)" |
275 then obtain a b a' b' where x[simp]: "x = (a,b)" |
276 and y[simp]: "y = (a',b')" by blast |
276 and y[simp]: "y = (a',b')" by blast |
298 ultimately have ?thesis using aa' bb' |
298 ultimately have ?thesis using aa' bb' |
299 by (simp add: Nadd_def INum_def normNum_def x y Let_def) } |
299 by (simp add: Nadd_def INum_def normNum_def x y Let_def) } |
300 ultimately show ?thesis by blast |
300 ultimately show ?thesis by blast |
301 qed |
301 qed |
302 |
302 |
303 lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field}) " |
303 lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero}) " |
304 proof- |
304 proof- |
305 let ?z = "0::'a" |
305 let ?z = "0::'a" |
306 have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto |
306 have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto |
307 then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast |
307 then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast |
308 {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis |
308 {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis |
321 qed |
321 qed |
322 |
322 |
323 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)" |
323 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)" |
324 by (simp add: Nneg_def split_def INum_def) |
324 by (simp add: Nneg_def split_def INum_def) |
325 |
325 |
326 lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {ring_char_0,division_ring_inverse_zero,field})" |
326 lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})" |
327 by (simp add: Nsub_def split_def) |
327 by (simp add: Nsub_def split_def) |
328 |
328 |
329 lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: {division_ring_inverse_zero,field}) / (INum x)" |
329 lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)" |
330 by (simp add: Ninv_def INum_def split_def) |
330 by (simp add: Ninv_def INum_def split_def) |
331 |
331 |
332 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {ring_char_0, division_ring_inverse_zero,field})" by (simp add: Ndiv_def) |
332 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def) |
333 |
333 |
334 lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" |
334 lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" |
335 shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})< 0) = 0>\<^sub>N x " |
335 shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x " |
336 proof- |
336 proof- |
337 have " \<exists> a b. x = (a,b)" by simp |
337 have " \<exists> a b. x = (a,b)" by simp |
338 then obtain a b where x[simp]:"x = (a,b)" by blast |
338 then obtain a b where x[simp]:"x = (a,b)" by blast |
339 {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) } |
339 {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) } |
340 moreover |
340 moreover |
343 have ?thesis by (simp add: Nlt0_def INum_def)} |
343 have ?thesis by (simp add: Nlt0_def INum_def)} |
344 ultimately show ?thesis by blast |
344 ultimately show ?thesis by blast |
345 qed |
345 qed |
346 |
346 |
347 lemma Nle0_iff[simp]:assumes nx: "isnormNum x" |
347 lemma Nle0_iff[simp]:assumes nx: "isnormNum x" |
348 shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x" |
348 shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x" |
349 proof- |
349 proof- |
350 have " \<exists> a b. x = (a,b)" by simp |
350 have " \<exists> a b. x = (a,b)" by simp |
351 then obtain a b where x[simp]:"x = (a,b)" by blast |
351 then obtain a b where x[simp]:"x = (a,b)" by blast |
352 {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) } |
352 {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) } |
353 moreover |
353 moreover |
355 from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"] |
355 from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"] |
356 have ?thesis by (simp add: Nle0_def INum_def)} |
356 have ?thesis by (simp add: Nle0_def INum_def)} |
357 ultimately show ?thesis by blast |
357 ultimately show ?thesis by blast |
358 qed |
358 qed |
359 |
359 |
360 lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})> 0) = 0<\<^sub>N x" |
360 lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x" |
361 proof- |
361 proof- |
362 have " \<exists> a b. x = (a,b)" by simp |
362 have " \<exists> a b. x = (a,b)" by simp |
363 then obtain a b where x[simp]:"x = (a,b)" by blast |
363 then obtain a b where x[simp]:"x = (a,b)" by blast |
364 {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) } |
364 {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) } |
365 moreover |
365 moreover |
367 from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"] |
367 from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"] |
368 have ?thesis by (simp add: Ngt0_def INum_def)} |
368 have ?thesis by (simp add: Ngt0_def INum_def)} |
369 ultimately show ?thesis by blast |
369 ultimately show ?thesis by blast |
370 qed |
370 qed |
371 lemma Nge0_iff[simp]:assumes nx: "isnormNum x" |
371 lemma Nge0_iff[simp]:assumes nx: "isnormNum x" |
372 shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x" |
372 shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x" |
373 proof- |
373 proof- |
374 have " \<exists> a b. x = (a,b)" by simp |
374 have " \<exists> a b. x = (a,b)" by simp |
375 then obtain a b where x[simp]:"x = (a,b)" by blast |
375 then obtain a b where x[simp]:"x = (a,b)" by blast |
376 {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) } |
376 {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) } |
377 moreover |
377 moreover |
380 have ?thesis by (simp add: Nge0_def INum_def)} |
380 have ?thesis by (simp add: Nge0_def INum_def)} |
381 ultimately show ?thesis by blast |
381 ultimately show ?thesis by blast |
382 qed |
382 qed |
383 |
383 |
384 lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" |
384 lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" |
385 shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field}) < INum y) = (x <\<^sub>N y)" |
385 shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)" |
386 proof- |
386 proof- |
387 let ?z = "0::'a" |
387 let ?z = "0::'a" |
388 have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp |
388 have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp |
389 also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp |
389 also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp |
390 finally show ?thesis by (simp add: Nlt_def) |
390 finally show ?thesis by (simp add: Nlt_def) |
391 qed |
391 qed |
392 |
392 |
393 lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" |
393 lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" |
394 shows "((INum x :: 'a :: {ring_char_0,division_ring_inverse_zero,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)" |
394 shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)" |
395 proof- |
395 proof- |
396 have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp |
396 have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp |
397 also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp |
397 also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp |
398 finally show ?thesis by (simp add: Nle_def) |
398 finally show ?thesis by (simp add: Nle_def) |
399 qed |
399 qed |
400 |
400 |
401 lemma Nadd_commute: |
401 lemma Nadd_commute: |
402 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
402 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
403 shows "x +\<^sub>N y = y +\<^sub>N x" |
403 shows "x +\<^sub>N y = y +\<^sub>N x" |
404 proof- |
404 proof- |
405 have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all |
405 have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all |
406 have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp |
406 have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp |
407 with isnormNum_unique[OF n] show ?thesis by simp |
407 with isnormNum_unique[OF n] show ?thesis by simp |
408 qed |
408 qed |
409 |
409 |
410 lemma [simp]: |
410 lemma [simp]: |
411 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
411 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
412 shows "(0, b) +\<^sub>N y = normNum y" |
412 shows "(0, b) +\<^sub>N y = normNum y" |
413 and "(a, 0) +\<^sub>N y = normNum y" |
413 and "(a, 0) +\<^sub>N y = normNum y" |
414 and "x +\<^sub>N (0, b) = normNum x" |
414 and "x +\<^sub>N (0, b) = normNum x" |
415 and "x +\<^sub>N (a, 0) = normNum x" |
415 and "x +\<^sub>N (a, 0) = normNum x" |
416 apply (simp add: Nadd_def split_def) |
416 apply (simp add: Nadd_def split_def) |
418 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
418 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
419 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
419 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
420 done |
420 done |
421 |
421 |
422 lemma normNum_nilpotent_aux[simp]: |
422 lemma normNum_nilpotent_aux[simp]: |
423 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
423 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
424 assumes nx: "isnormNum x" |
424 assumes nx: "isnormNum x" |
425 shows "normNum x = x" |
425 shows "normNum x = x" |
426 proof- |
426 proof- |
427 let ?a = "normNum x" |
427 let ?a = "normNum x" |
428 have n: "isnormNum ?a" by simp |
428 have n: "isnormNum ?a" by simp |
430 with isnormNum_unique[OF n nx] |
430 with isnormNum_unique[OF n nx] |
431 show ?thesis by simp |
431 show ?thesis by simp |
432 qed |
432 qed |
433 |
433 |
434 lemma normNum_nilpotent[simp]: |
434 lemma normNum_nilpotent[simp]: |
435 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
435 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
436 shows "normNum (normNum x) = normNum x" |
436 shows "normNum (normNum x) = normNum x" |
437 by simp |
437 by simp |
438 |
438 |
439 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N" |
439 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N" |
440 by (simp_all add: normNum_def) |
440 by (simp_all add: normNum_def) |
441 |
441 |
442 lemma normNum_Nadd: |
442 lemma normNum_Nadd: |
443 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
443 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
444 shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp |
444 shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp |
445 |
445 |
446 lemma Nadd_normNum1[simp]: |
446 lemma Nadd_normNum1[simp]: |
447 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
447 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
448 shows "normNum x +\<^sub>N y = x +\<^sub>N y" |
448 shows "normNum x +\<^sub>N y = x +\<^sub>N y" |
449 proof- |
449 proof- |
450 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all |
450 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all |
451 have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp |
451 have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp |
452 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
452 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
453 finally show ?thesis using isnormNum_unique[OF n] by simp |
453 finally show ?thesis using isnormNum_unique[OF n] by simp |
454 qed |
454 qed |
455 |
455 |
456 lemma Nadd_normNum2[simp]: |
456 lemma Nadd_normNum2[simp]: |
457 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
457 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
458 shows "x +\<^sub>N normNum y = x +\<^sub>N y" |
458 shows "x +\<^sub>N normNum y = x +\<^sub>N y" |
459 proof- |
459 proof- |
460 have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all |
460 have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all |
461 have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp |
461 have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp |
462 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
462 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
463 finally show ?thesis using isnormNum_unique[OF n] by simp |
463 finally show ?thesis using isnormNum_unique[OF n] by simp |
464 qed |
464 qed |
465 |
465 |
466 lemma Nadd_assoc: |
466 lemma Nadd_assoc: |
467 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
467 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
468 shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" |
468 shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" |
469 proof- |
469 proof- |
470 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all |
470 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all |
471 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
471 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
472 with isnormNum_unique[OF n] show ?thesis by simp |
472 with isnormNum_unique[OF n] show ?thesis by simp |
474 |
474 |
475 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x" |
475 lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x" |
476 by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute) |
476 by (simp add: Nmul_def split_def Let_def gcd_commute_int mult_commute) |
477 |
477 |
478 lemma Nmul_assoc: |
478 lemma Nmul_assoc: |
479 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
479 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
480 assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z" |
480 assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z" |
481 shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" |
481 shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" |
482 proof- |
482 proof- |
483 from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" |
483 from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" |
484 by simp_all |
484 by simp_all |
485 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
485 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
486 with isnormNum_unique[OF n] show ?thesis by simp |
486 with isnormNum_unique[OF n] show ?thesis by simp |
487 qed |
487 qed |
488 |
488 |
489 lemma Nsub0: |
489 lemma Nsub0: |
490 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
490 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
491 assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)" |
491 assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)" |
492 proof- |
492 proof- |
493 { fix h :: 'a |
493 { fix h :: 'a |
494 from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] |
494 from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] |
495 have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp |
495 have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp |
500 |
500 |
501 lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N" |
501 lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N" |
502 by (simp_all add: Nmul_def Let_def split_def) |
502 by (simp_all add: Nmul_def Let_def split_def) |
503 |
503 |
504 lemma Nmul_eq0[simp]: |
504 lemma Nmul_eq0[simp]: |
505 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_ring_inverse_zero,field})" |
505 assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" |
506 assumes nx:"isnormNum x" and ny: "isnormNum y" |
506 assumes nx:"isnormNum x" and ny: "isnormNum y" |
507 shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)" |
507 shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)" |
508 proof- |
508 proof- |
509 { fix h :: 'a |
509 { fix h :: 'a |
510 have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto |
510 have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto |