reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
authorhaftmann
Wed Jan 04 21:28:28 2017 +0100 (2017-01-04)
changeset 647845cb5e7ecb284
parent 64783 0be08e4cd0ec
child 64785 ae0bbc8e45ad
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
src/HOL/Library/Field_as_Ring.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Euclidean_Division.thy
     1.1 --- a/src/HOL/Library/Field_as_Ring.thy	Wed Jan 04 22:57:39 2017 +0100
     1.2 +++ b/src/HOL/Library/Field_as_Ring.thy	Wed Jan 04 21:28:28 2017 +0100
     1.3 @@ -24,15 +24,19 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instantiation real :: euclidean_ring
     1.8 +instantiation real :: unique_euclidean_ring
     1.9  begin
    1.10  
    1.11  definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    1.12  definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
    1.13  definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
    1.14 +definition [simp]: "uniqueness_constraint_real = (top :: real \<Rightarrow> real \<Rightarrow> bool)"
    1.15  definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
    1.16  
    1.17 -instance by standard (simp_all add: dvd_field_iff divide_simps)
    1.18 +instance
    1.19 +  by standard
    1.20 +    (simp_all add: dvd_field_iff divide_simps split: if_splits)
    1.21 +
    1.22  end
    1.23  
    1.24  instantiation real :: euclidean_ring_gcd
    1.25 @@ -51,15 +55,19 @@
    1.26  
    1.27  end
    1.28  
    1.29 -instantiation rat :: euclidean_ring
    1.30 +instantiation rat :: unique_euclidean_ring
    1.31  begin
    1.32  
    1.33  definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    1.34  definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
    1.35  definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
    1.36 +definition [simp]: "uniqueness_constraint_rat = (top :: rat \<Rightarrow> rat \<Rightarrow> bool)"
    1.37  definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
    1.38  
    1.39 -instance by standard (simp_all add: dvd_field_iff divide_simps)
    1.40 +instance
    1.41 +  by standard
    1.42 +    (simp_all add: dvd_field_iff divide_simps split: if_splits)
    1.43 +
    1.44  end
    1.45  
    1.46  instantiation rat :: euclidean_ring_gcd
    1.47 @@ -78,15 +86,19 @@
    1.48  
    1.49  end
    1.50  
    1.51 -instantiation complex :: euclidean_ring
    1.52 +instantiation complex :: unique_euclidean_ring
    1.53  begin
    1.54  
    1.55  definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
    1.56  definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
    1.57  definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
    1.58 +definition [simp]: "uniqueness_constraint_complex = (top :: complex \<Rightarrow> complex \<Rightarrow> bool)"
    1.59  definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
    1.60  
    1.61 -instance by standard (simp_all add: dvd_field_iff divide_simps)
    1.62 +instance
    1.63 +  by standard
    1.64 +    (simp_all add: dvd_field_iff divide_simps split: if_splits)
    1.65 +
    1.66  end
    1.67  
    1.68  instantiation complex :: euclidean_ring_gcd
     2.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Jan 04 22:57:39 2017 +0100
     2.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Jan 04 21:28:28 2017 +0100
     2.3 @@ -1400,7 +1400,7 @@
     2.4  
     2.5  subsection \<open>Formal power series form a Euclidean ring\<close>
     2.6  
     2.7 -instantiation fps :: (field) euclidean_ring
     2.8 +instantiation fps :: (field) euclidean_ring_cancel
     2.9  begin
    2.10  
    2.11  definition fps_euclidean_size_def:
     3.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Wed Jan 04 22:57:39 2017 +0100
     3.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Wed Jan 04 21:28:28 2017 +0100
     3.3 @@ -676,14 +676,15 @@
     3.4    "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
     3.5  
     3.6  lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
     3.7 -    by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
     3.8 +  by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
     3.9  
    3.10  interpretation field_poly: 
    3.11 -  euclidean_ring where zero = "0 :: 'a :: field poly"
    3.12 +  unique_euclidean_ring where zero = "0 :: 'a :: field poly"
    3.13      and one = 1 and plus = plus and uminus = uminus and minus = minus
    3.14      and times = times
    3.15      and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly
    3.16      and euclidean_size = euclidean_size_field_poly
    3.17 +    and uniqueness_constraint = top
    3.18      and divide = divide and modulo = modulo
    3.19  proof (standard, unfold dvd_field_poly)
    3.20    fix p :: "'a poly"
    3.21 @@ -698,6 +699,17 @@
    3.22    fix p :: "'a poly" assume "p \<noteq> 0"
    3.23    thus "is_unit (unit_factor_field_poly p)"
    3.24      by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
    3.25 +next
    3.26 +  fix p q s :: "'a poly" assume "s \<noteq> 0"
    3.27 +  moreover assume "euclidean_size_field_poly p < euclidean_size_field_poly q"
    3.28 +  ultimately show "euclidean_size_field_poly (p * s) < euclidean_size_field_poly (q * s)"
    3.29 +    by (auto simp add: euclidean_size_field_poly_def degree_mult_eq)
    3.30 +next
    3.31 +  fix p q r :: "'a poly" assume "p \<noteq> 0"
    3.32 +  moreover assume "euclidean_size_field_poly r < euclidean_size_field_poly p"
    3.33 +  ultimately show "(q * p + r) div p = q"
    3.34 +    by (cases "r = 0")
    3.35 +      (auto simp add: unit_factor_field_poly_def euclidean_size_field_poly_def div_poly_less)
    3.36  qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
    3.37         euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
    3.38  
    3.39 @@ -1011,17 +1023,22 @@
    3.40  
    3.41  end
    3.42  
    3.43 -instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring
    3.44 +instantiation poly :: ("{field,factorial_ring_gcd}") unique_euclidean_ring
    3.45  begin
    3.46  
    3.47 -definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" where
    3.48 -  "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
    3.49 +definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
    3.50 +  where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
    3.51 +
    3.52 +definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
    3.53 +  where [simp]: "uniqueness_constraint_poly = top"
    3.54  
    3.55  instance 
    3.56 -  by standard (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
    3.57 +  by standard
    3.58 +   (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le
    3.59 +    split: if_splits)
    3.60 +
    3.61  end
    3.62  
    3.63 -
    3.64  instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
    3.65    by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
    3.66  
     4.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 22:57:39 2017 +0100
     4.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 21:28:28 2017 +0100
     4.3 @@ -1,133 +1,17 @@
     4.4 -(* Author: Manuel Eberl *)
     4.5 +(*  Title:      HOL/Number_Theory/Euclidean_Algorithm.thy
     4.6 +    Author:     Manuel Eberl, TU Muenchen
     4.7 +*)
     4.8  
     4.9 -section \<open>Abstract euclidean algorithm\<close>
    4.10 +section \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close>
    4.11  
    4.12  theory Euclidean_Algorithm
    4.13 -imports "~~/src/HOL/GCD" Factorial_Ring
    4.14 -begin
    4.15 -
    4.16 -text \<open>
    4.17 -  A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
    4.18 -  implemented. It must provide:
    4.19 -  \begin{itemize}
    4.20 -  \item division with remainder
    4.21 -  \item a size function such that @{term "size (a mod b) < size b"} 
    4.22 -        for any @{term "b \<noteq> 0"}
    4.23 -  \end{itemize}
    4.24 -  The existence of these functions makes it possible to derive gcd and lcm functions 
    4.25 -  for any Euclidean semiring.
    4.26 -\<close> 
    4.27 -class euclidean_semiring = semidom_modulo + normalization_semidom + 
    4.28 -  fixes euclidean_size :: "'a \<Rightarrow> nat"
    4.29 -  assumes size_0 [simp]: "euclidean_size 0 = 0"
    4.30 -  assumes mod_size_less: 
    4.31 -    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    4.32 -  assumes size_mult_mono:
    4.33 -    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    4.34 +  imports "~~/src/HOL/GCD"
    4.35 +    "~~/src/HOL/Number_Theory/Factorial_Ring"
    4.36 +    "~~/src/HOL/Number_Theory/Euclidean_Division"
    4.37  begin
    4.38  
    4.39 -lemma euclidean_size_normalize [simp]:
    4.40 -  "euclidean_size (normalize a) = euclidean_size a"
    4.41 -proof (cases "a = 0")
    4.42 -  case True
    4.43 -  then show ?thesis
    4.44 -    by simp
    4.45 -next
    4.46 -  case [simp]: False
    4.47 -  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
    4.48 -    by (rule size_mult_mono) simp
    4.49 -  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
    4.50 -    by (rule size_mult_mono) simp
    4.51 -  ultimately show ?thesis
    4.52 -    by simp
    4.53 -qed
    4.54 -
    4.55 -lemma euclidean_division:
    4.56 -  fixes a :: 'a and b :: 'a
    4.57 -  assumes "b \<noteq> 0"
    4.58 -  obtains s and t where "a = s * b + t" 
    4.59 -    and "euclidean_size t < euclidean_size b"
    4.60 -proof -
    4.61 -  from div_mult_mod_eq [of a b] 
    4.62 -     have "a = a div b * b + a mod b" by simp
    4.63 -  with that and assms show ?thesis by (auto simp add: mod_size_less)
    4.64 -qed
    4.65 -
    4.66 -lemma dvd_euclidean_size_eq_imp_dvd:
    4.67 -  assumes "a \<noteq> 0" and b_dvd_a: "b dvd a" and size_eq: "euclidean_size a = euclidean_size b"
    4.68 -  shows "a dvd b"
    4.69 -proof (rule ccontr)
    4.70 -  assume "\<not> a dvd b"
    4.71 -  hence "b mod a \<noteq> 0" using mod_0_imp_dvd[of b a] by blast
    4.72 -  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
    4.73 -  from b_dvd_a have b_dvd_mod: "b dvd b mod a" by (simp add: dvd_mod_iff)
    4.74 -  from b_dvd_mod obtain c where "b mod a = b * c" unfolding dvd_def by blast
    4.75 -    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
    4.76 -  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
    4.77 -      using size_mult_mono by force
    4.78 -  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
    4.79 -  have "euclidean_size (b mod a) < euclidean_size a"
    4.80 -      using mod_size_less by blast
    4.81 -  ultimately show False using size_eq by simp
    4.82 -qed
    4.83 -
    4.84 -lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
    4.85 -  by (subst mult.commute) (rule size_mult_mono)
    4.86 -
    4.87 -lemma euclidean_size_times_unit:
    4.88 -  assumes "is_unit a"
    4.89 -  shows   "euclidean_size (a * b) = euclidean_size b"
    4.90 -proof (rule antisym)
    4.91 -  from assms have [simp]: "a \<noteq> 0" by auto
    4.92 -  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
    4.93 -  from assms have "is_unit (1 div a)" by simp
    4.94 -  hence "1 div a \<noteq> 0" by (intro notI) simp_all
    4.95 -  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
    4.96 -    by (rule size_mult_mono')
    4.97 -  also from assms have "(1 div a) * (a * b) = b"
    4.98 -    by (simp add: algebra_simps unit_div_mult_swap)
    4.99 -  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
   4.100 -qed
   4.101 -
   4.102 -lemma euclidean_size_unit: "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
   4.103 -  using euclidean_size_times_unit[of a 1] by simp
   4.104 -
   4.105 -lemma unit_iff_euclidean_size: 
   4.106 -  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
   4.107 -proof safe
   4.108 -  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
   4.109 -  show "is_unit a" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all
   4.110 -qed (auto intro: euclidean_size_unit)
   4.111 -
   4.112 -lemma euclidean_size_times_nonunit:
   4.113 -  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not>is_unit a"
   4.114 -  shows   "euclidean_size b < euclidean_size (a * b)"
   4.115 -proof (rule ccontr)
   4.116 -  assume "\<not>euclidean_size b < euclidean_size (a * b)"
   4.117 -  with size_mult_mono'[OF assms(1), of b] 
   4.118 -    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
   4.119 -  have "a * b dvd b"
   4.120 -    by (rule dvd_euclidean_size_eq_imp_dvd[OF _ _ eq]) (insert assms, simp_all)
   4.121 -  hence "a * b dvd 1 * b" by simp
   4.122 -  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
   4.123 -  with assms(3) show False by contradiction
   4.124 -qed
   4.125 -
   4.126 -lemma dvd_imp_size_le:
   4.127 -  assumes "a dvd b" "b \<noteq> 0" 
   4.128 -  shows   "euclidean_size a \<le> euclidean_size b"
   4.129 -  using assms by (auto elim!: dvdE simp: size_mult_mono)
   4.130 -
   4.131 -lemma dvd_proper_imp_size_less:
   4.132 -  assumes "a dvd b" "\<not>b dvd a" "b \<noteq> 0" 
   4.133 -  shows   "euclidean_size a < euclidean_size b"
   4.134 -proof -
   4.135 -  from assms(1) obtain c where "b = a * c" by (erule dvdE)
   4.136 -  hence z: "b = c * a" by (simp add: mult.commute)
   4.137 -  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
   4.138 -  with z assms show ?thesis
   4.139 -    by (auto intro!: euclidean_size_times_nonunit simp: )
   4.140 -qed
   4.141 +context euclidean_semiring
   4.142 +begin
   4.143  
   4.144  function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   4.145  where
   4.146 @@ -432,7 +316,7 @@
   4.147    
   4.148  end
   4.149  
   4.150 -class euclidean_ring = euclidean_semiring + idom
   4.151 +context euclidean_ring
   4.152  begin
   4.153  
   4.154  function euclid_ext_aux :: "'a \<Rightarrow> _" where
   4.155 @@ -680,27 +564,6 @@
   4.156  
   4.157  subsection \<open>Typical instances\<close>
   4.158  
   4.159 -instantiation nat :: euclidean_semiring
   4.160 -begin
   4.161 -
   4.162 -definition [simp]:
   4.163 -  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   4.164 -
   4.165 -instance by standard simp_all
   4.166 -
   4.167 -end
   4.168 -
   4.169 -
   4.170 -instantiation int :: euclidean_ring
   4.171 -begin
   4.172 -
   4.173 -definition [simp]:
   4.174 -  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   4.175 -
   4.176 -instance by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
   4.177 -
   4.178 -end
   4.179 -
   4.180  instance nat :: euclidean_semiring_gcd
   4.181  proof
   4.182    show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)"
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Number_Theory/Euclidean_Division.thy	Wed Jan 04 21:28:28 2017 +0100
     5.3 @@ -0,0 +1,295 @@
     5.4 +(*  Title:      HOL/Number_Theory/Euclidean_Division.thy
     5.5 +    Author:     Manuel Eberl, TU Muenchen
     5.6 +    Author:     Florian Haftmann, TU Muenchen
     5.7 +*)
     5.8 +
     5.9 +section \<open>Division with remainder in euclidean (semi)rings\<close>
    5.10 +
    5.11 +theory Euclidean_Division
    5.12 +  imports Main
    5.13 +begin
    5.14 +
    5.15 +subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    5.16 +  
    5.17 +class euclidean_semiring = semidom_modulo + normalization_semidom + 
    5.18 +  fixes euclidean_size :: "'a \<Rightarrow> nat"
    5.19 +  assumes size_0 [simp]: "euclidean_size 0 = 0"
    5.20 +  assumes mod_size_less: 
    5.21 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    5.22 +  assumes size_mult_mono:
    5.23 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
    5.24 +begin
    5.25 +
    5.26 +lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
    5.27 +  by (subst mult.commute) (rule size_mult_mono)
    5.28 +
    5.29 +lemma euclidean_size_normalize [simp]:
    5.30 +  "euclidean_size (normalize a) = euclidean_size a"
    5.31 +proof (cases "a = 0")
    5.32 +  case True
    5.33 +  then show ?thesis
    5.34 +    by simp
    5.35 +next
    5.36 +  case [simp]: False
    5.37 +  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
    5.38 +    by (rule size_mult_mono) simp
    5.39 +  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
    5.40 +    by (rule size_mult_mono) simp
    5.41 +  ultimately show ?thesis
    5.42 +    by simp
    5.43 +qed
    5.44 +
    5.45 +lemma dvd_euclidean_size_eq_imp_dvd:
    5.46 +  assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
    5.47 +    and "b dvd a" 
    5.48 +  shows "a dvd b"
    5.49 +proof (rule ccontr)
    5.50 +  assume "\<not> a dvd b"
    5.51 +  hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
    5.52 +  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
    5.53 +  from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
    5.54 +  then obtain c where "b mod a = b * c" unfolding dvd_def by blast
    5.55 +    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
    5.56 +  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
    5.57 +    using size_mult_mono by force
    5.58 +  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
    5.59 +  have "euclidean_size (b mod a) < euclidean_size a"
    5.60 +    using mod_size_less by blast
    5.61 +  ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
    5.62 +    by simp
    5.63 +qed
    5.64 +
    5.65 +lemma euclidean_size_times_unit:
    5.66 +  assumes "is_unit a"
    5.67 +  shows   "euclidean_size (a * b) = euclidean_size b"
    5.68 +proof (rule antisym)
    5.69 +  from assms have [simp]: "a \<noteq> 0" by auto
    5.70 +  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
    5.71 +  from assms have "is_unit (1 div a)" by simp
    5.72 +  hence "1 div a \<noteq> 0" by (intro notI) simp_all
    5.73 +  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
    5.74 +    by (rule size_mult_mono')
    5.75 +  also from assms have "(1 div a) * (a * b) = b"
    5.76 +    by (simp add: algebra_simps unit_div_mult_swap)
    5.77 +  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
    5.78 +qed
    5.79 +
    5.80 +lemma euclidean_size_unit:
    5.81 +  "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
    5.82 +  using euclidean_size_times_unit [of a 1] by simp
    5.83 +
    5.84 +lemma unit_iff_euclidean_size: 
    5.85 +  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
    5.86 +proof safe
    5.87 +  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
    5.88 +  show "is_unit a"
    5.89 +    by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
    5.90 +qed (auto intro: euclidean_size_unit)
    5.91 +
    5.92 +lemma euclidean_size_times_nonunit:
    5.93 +  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
    5.94 +  shows   "euclidean_size b < euclidean_size (a * b)"
    5.95 +proof (rule ccontr)
    5.96 +  assume "\<not>euclidean_size b < euclidean_size (a * b)"
    5.97 +  with size_mult_mono'[OF assms(1), of b] 
    5.98 +    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
    5.99 +  have "a * b dvd b"
   5.100 +    by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
   5.101 +  hence "a * b dvd 1 * b" by simp
   5.102 +  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
   5.103 +  with assms(3) show False by contradiction
   5.104 +qed
   5.105 +
   5.106 +lemma dvd_imp_size_le:
   5.107 +  assumes "a dvd b" "b \<noteq> 0" 
   5.108 +  shows   "euclidean_size a \<le> euclidean_size b"
   5.109 +  using assms by (auto elim!: dvdE simp: size_mult_mono)
   5.110 +
   5.111 +lemma dvd_proper_imp_size_less:
   5.112 +  assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
   5.113 +  shows   "euclidean_size a < euclidean_size b"
   5.114 +proof -
   5.115 +  from assms(1) obtain c where "b = a * c" by (erule dvdE)
   5.116 +  hence z: "b = c * a" by (simp add: mult.commute)
   5.117 +  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
   5.118 +  with z assms show ?thesis
   5.119 +    by (auto intro!: euclidean_size_times_nonunit)
   5.120 +qed
   5.121 +
   5.122 +end
   5.123 +
   5.124 +class euclidean_ring = idom_modulo + euclidean_semiring
   5.125 +
   5.126 +  
   5.127 +subsection \<open>Euclidean (semi)rings with cancel rules\<close>
   5.128 +
   5.129 +class euclidean_semiring_cancel = euclidean_semiring + semiring_div
   5.130 +
   5.131 +class euclidean_ring_cancel = euclidean_ring + ring_div
   5.132 +  
   5.133 +  
   5.134 +subsection \<open>Uniquely determined division\<close>
   5.135 +  
   5.136 +class unique_euclidean_semiring = euclidean_semiring + 
   5.137 +  fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   5.138 +  assumes size_mono_mult:
   5.139 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
   5.140 +      \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
   5.141 +    -- \<open>FIXME justify\<close>
   5.142 +  assumes uniqueness_constraint_mono_mult:
   5.143 +    "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
   5.144 +  assumes uniqueness_constraint_mod:
   5.145 +    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
   5.146 +  assumes div_bounded:
   5.147 +    "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
   5.148 +    \<Longrightarrow> euclidean_size r < euclidean_size b
   5.149 +    \<Longrightarrow> (q * b + r) div b = q"
   5.150 +begin
   5.151 +
   5.152 +lemma divmod_cases [case_names divides remainder by0]:
   5.153 +  obtains 
   5.154 +    (divides) q where "b \<noteq> 0"
   5.155 +      and "a div b = q"
   5.156 +      and "a mod b = 0"
   5.157 +      and "a = q * b"
   5.158 +  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
   5.159 +      and "uniqueness_constraint r b"
   5.160 +      and "euclidean_size r < euclidean_size b"
   5.161 +      and "a div b = q"
   5.162 +      and "a mod b = r"
   5.163 +      and "a = q * b + r"
   5.164 +  | (by0) "b = 0"
   5.165 +proof (cases "b = 0")
   5.166 +  case True
   5.167 +  then show thesis
   5.168 +  by (rule by0)
   5.169 +next
   5.170 +  case False
   5.171 +  show thesis
   5.172 +  proof (cases "b dvd a")
   5.173 +    case True
   5.174 +    then obtain q where "a = b * q" ..
   5.175 +    with \<open>b \<noteq> 0\<close> divides
   5.176 +    show thesis
   5.177 +      by (simp add: ac_simps)
   5.178 +  next
   5.179 +    case False
   5.180 +    then have "a mod b \<noteq> 0"
   5.181 +      by (simp add: mod_eq_0_iff_dvd)
   5.182 +    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
   5.183 +      by (rule uniqueness_constraint_mod)
   5.184 +    moreover have "euclidean_size (a mod b) < euclidean_size b"
   5.185 +      using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
   5.186 +    moreover have "a = a div b * b + a mod b"
   5.187 +      by (simp add: div_mult_mod_eq)
   5.188 +    ultimately show thesis
   5.189 +      using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
   5.190 +  qed
   5.191 +qed
   5.192 +
   5.193 +lemma div_eqI:
   5.194 +  "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
   5.195 +    "euclidean_size r < euclidean_size b" "q * b + r = a"
   5.196 +proof -
   5.197 +  from that have "(q * b + r) div b = q"
   5.198 +    by (auto intro: div_bounded)
   5.199 +  with that show ?thesis
   5.200 +    by simp
   5.201 +qed
   5.202 +
   5.203 +lemma mod_eqI:
   5.204 +  "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
   5.205 +    "euclidean_size r < euclidean_size b" "q * b + r = a" 
   5.206 +proof -
   5.207 +  from that have "a div b = q"
   5.208 +    by (rule div_eqI)
   5.209 +  moreover have "a div b * b + a mod b = a"
   5.210 +    by (fact div_mult_mod_eq)
   5.211 +  ultimately have "a div b * b + a mod b = a div b * b + r"
   5.212 +    using \<open>q * b + r = a\<close> by simp
   5.213 +  then show ?thesis
   5.214 +    by simp
   5.215 +qed
   5.216 +
   5.217 +subclass euclidean_semiring_cancel
   5.218 +proof
   5.219 +  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   5.220 +  proof (cases a b rule: divmod_cases)
   5.221 +    case by0
   5.222 +    with \<open>b \<noteq> 0\<close> show ?thesis
   5.223 +      by simp
   5.224 +  next
   5.225 +    case (divides q)
   5.226 +    then show ?thesis
   5.227 +      by (simp add: ac_simps)
   5.228 +  next
   5.229 +    case (remainder q r)
   5.230 +    then show ?thesis
   5.231 +      by (auto intro: div_eqI simp add: algebra_simps)
   5.232 +  qed
   5.233 +next
   5.234 +  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   5.235 +  proof (cases a b rule: divmod_cases)
   5.236 +    case by0
   5.237 +    then show ?thesis
   5.238 +      by simp
   5.239 +  next
   5.240 +    case (divides q)
   5.241 +    with \<open>c \<noteq> 0\<close> show ?thesis
   5.242 +      by (simp add: mult.left_commute [of c])
   5.243 +  next
   5.244 +    case (remainder q r)
   5.245 +    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   5.246 +      by simp
   5.247 +    from remainder \<open>c \<noteq> 0\<close>
   5.248 +    have "uniqueness_constraint (r * c) (b * c)"
   5.249 +      and "euclidean_size (r * c) < euclidean_size (b * c)"
   5.250 +      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   5.251 +    with remainder show ?thesis
   5.252 +      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   5.253 +        (use \<open>b * c \<noteq> 0\<close> in simp)
   5.254 +  qed
   5.255 +qed
   5.256 +  
   5.257 +end
   5.258 +
   5.259 +class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
   5.260 +begin
   5.261 +
   5.262 +subclass euclidean_ring_cancel ..
   5.263 +
   5.264 +end
   5.265 +
   5.266 +subsection \<open>Typical instances\<close>
   5.267 +
   5.268 +instantiation nat :: unique_euclidean_semiring
   5.269 +begin
   5.270 +
   5.271 +definition [simp]:
   5.272 +  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   5.273 +
   5.274 +definition [simp]:
   5.275 +  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   5.276 +
   5.277 +instance
   5.278 +  by standard
   5.279 +    (simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd)
   5.280 +
   5.281 +end
   5.282 +
   5.283 +instantiation int :: unique_euclidean_ring
   5.284 +begin
   5.285 +
   5.286 +definition [simp]:
   5.287 +  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   5.288 +
   5.289 +definition [simp]:
   5.290 +  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   5.291 +  
   5.292 +instance
   5.293 +  by standard
   5.294 +    (auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split)
   5.295 +
   5.296 +end
   5.297 +
   5.298 +end