equal
deleted
inserted
replaced
23 assumes mod_size_less: |
23 assumes mod_size_less: |
24 "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b" |
24 "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b" |
25 assumes size_mult_mono: |
25 assumes size_mult_mono: |
26 "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)" |
26 "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)" |
27 begin |
27 begin |
|
28 |
|
29 lemma euclidean_size_normalize [simp]: |
|
30 "euclidean_size (normalize a) = euclidean_size a" |
|
31 proof (cases "a = 0") |
|
32 case True |
|
33 then show ?thesis |
|
34 by simp |
|
35 next |
|
36 case [simp]: False |
|
37 have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)" |
|
38 by (rule size_mult_mono) simp |
|
39 moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))" |
|
40 by (rule size_mult_mono) simp |
|
41 ultimately show ?thesis |
|
42 by simp |
|
43 qed |
28 |
44 |
29 lemma euclidean_division: |
45 lemma euclidean_division: |
30 fixes a :: 'a and b :: 'a |
46 fixes a :: 'a and b :: 'a |
31 assumes "b \<noteq> 0" |
47 assumes "b \<noteq> 0" |
32 obtains s and t where "a = s * b + t" |
48 obtains s and t where "a = s * b + t" |