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"