src/HOL/Euclidean_Division.thy
 changeset 66817 0b12755ccbb2 parent 66816 212a3334e7da child 66837 6ba663ff2b1c
```     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
1.3 @@ -3,15 +3,15 @@
1.4      Author:     Florian Haftmann, TU Muenchen
1.5  *)
1.6
1.7 -section \<open>Uniquely determined division in euclidean (semi)rings\<close>
1.8 +section \<open>Division in euclidean (semi)rings\<close>
1.9
1.10  theory Euclidean_Division
1.11 -  imports Nat_Transfer Lattices_Big
1.12 +  imports Int Lattices_Big
1.13  begin
1.14
1.15  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
1.16
1.17 -class euclidean_semiring = semidom_modulo + normalization_semidom +
1.18 +class euclidean_semiring = semidom_modulo +
1.19    fixes euclidean_size :: "'a \<Rightarrow> nat"
1.20    assumes size_0 [simp]: "euclidean_size 0 = 0"
1.21    assumes mod_size_less:
1.22 @@ -23,22 +23,6 @@
1.23  lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
1.24    by (subst mult.commute) (rule size_mult_mono)
1.25
1.26 -lemma euclidean_size_normalize [simp]:
1.27 -  "euclidean_size (normalize a) = euclidean_size a"
1.28 -proof (cases "a = 0")
1.29 -  case True
1.30 -  then show ?thesis
1.31 -    by simp
1.32 -next
1.33 -  case [simp]: False
1.34 -  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
1.35 -    by (rule size_mult_mono) simp
1.36 -  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
1.37 -    by (rule size_mult_mono) simp
1.38 -  ultimately show ?thesis
1.39 -    by simp
1.40 -qed
1.41 -
1.42  lemma dvd_euclidean_size_eq_imp_dvd:
1.43    assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
1.44      and "b dvd a"
```