moved euclidean ring to HOL
authorhaftmann
Wed Jan 04 21:28:29 2017 +0100 (2017-01-04)
changeset 64785ae0bbc8e45ad
parent 64784 5cb5e7ecb284
child 64786 340db65fd2c1
moved euclidean ring to HOL
NEWS
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Euclidean_Division.thy
src/HOL/Parity.thy
     1.1 --- a/NEWS	Wed Jan 04 21:28:28 2017 +0100
     1.2 +++ b/NEWS	Wed Jan 04 21:28:29 2017 +0100
     1.3 @@ -23,6 +23,11 @@
     1.4  use constants transp, antisymp, single_valuedp instead.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Algebraic type class hierarchy of euclidean (semi)rings in HOL:
     1.8 +euclidean_(semi)ring, euclidean_(semi)ring_cancel,
     1.9 +unique_euclidean_(semi)ring; instantiation requires
    1.10 +provision of a euclidean size.
    1.11 +
    1.12  * Swapped orientation of congruence rules mod_add_left_eq,
    1.13  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.14  mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
     2.1 --- a/src/HOL/Divides.thy	Wed Jan 04 21:28:28 2017 +0100
     2.2 +++ b/src/HOL/Divides.thy	Wed Jan 04 21:28:29 2017 +0100
     2.3 @@ -3,88 +3,12 @@
     2.4      Copyright   1999  University of Cambridge
     2.5  *)
     2.6  
     2.7 -section \<open>Quotient and remainder\<close>
     2.8 +section \<open>More on quotient and remainder\<close>
     2.9  
    2.10  theory Divides
    2.11  imports Parity
    2.12  begin
    2.13  
    2.14 -subsection \<open>Quotient and remainder in integral domains\<close>
    2.15 -
    2.16 -class semidom_modulo = algebraic_semidom + semiring_modulo
    2.17 -begin
    2.18 -
    2.19 -lemma mod_0 [simp]: "0 mod a = 0"
    2.20 -  using div_mult_mod_eq [of 0 a] by simp
    2.21 -
    2.22 -lemma mod_by_0 [simp]: "a mod 0 = a"
    2.23 -  using div_mult_mod_eq [of a 0] by simp
    2.24 -
    2.25 -lemma mod_by_1 [simp]:
    2.26 -  "a mod 1 = 0"
    2.27 -proof -
    2.28 -  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    2.29 -  then have "a + a mod 1 = a + 0" by simp
    2.30 -  then show ?thesis by (rule add_left_imp_eq)
    2.31 -qed
    2.32 -
    2.33 -lemma mod_self [simp]:
    2.34 -  "a mod a = 0"
    2.35 -  using div_mult_mod_eq [of a a] by simp
    2.36 -
    2.37 -lemma dvd_imp_mod_0 [simp]:
    2.38 -  assumes "a dvd b"
    2.39 -  shows "b mod a = 0"
    2.40 -  using assms minus_div_mult_eq_mod [of b a] by simp
    2.41 -
    2.42 -lemma mod_0_imp_dvd: 
    2.43 -  assumes "a mod b = 0"
    2.44 -  shows   "b dvd a"
    2.45 -proof -
    2.46 -  have "b dvd ((a div b) * b)" by simp
    2.47 -  also have "(a div b) * b = a"
    2.48 -    using div_mult_mod_eq [of a b] by (simp add: assms)
    2.49 -  finally show ?thesis .
    2.50 -qed
    2.51 -
    2.52 -lemma mod_eq_0_iff_dvd:
    2.53 -  "a mod b = 0 \<longleftrightarrow> b dvd a"
    2.54 -  by (auto intro: mod_0_imp_dvd)
    2.55 -
    2.56 -lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    2.57 -  "a dvd b \<longleftrightarrow> b mod a = 0"
    2.58 -  by (simp add: mod_eq_0_iff_dvd)
    2.59 -
    2.60 -lemma dvd_mod_iff: 
    2.61 -  assumes "c dvd b"
    2.62 -  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    2.63 -proof -
    2.64 -  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    2.65 -    by (simp add: dvd_add_right_iff)
    2.66 -  also have "(a div b) * b + a mod b = a"
    2.67 -    using div_mult_mod_eq [of a b] by simp
    2.68 -  finally show ?thesis .
    2.69 -qed
    2.70 -
    2.71 -lemma dvd_mod_imp_dvd:
    2.72 -  assumes "c dvd a mod b" and "c dvd b"
    2.73 -  shows "c dvd a"
    2.74 -  using assms dvd_mod_iff [of c b a] by simp
    2.75 -
    2.76 -end
    2.77 -
    2.78 -class idom_modulo = idom + semidom_modulo
    2.79 -begin
    2.80 -
    2.81 -subclass idom_divide ..
    2.82 -
    2.83 -lemma div_diff [simp]:
    2.84 -  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    2.85 -  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    2.86 -
    2.87 -end
    2.88 -
    2.89 -
    2.90  subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
    2.91  
    2.92  class semiring_div = semidom_modulo +
    2.93 @@ -440,6 +364,65 @@
    2.94  
    2.95  end
    2.96  
    2.97 +  
    2.98 +subsection \<open>Euclidean (semi)rings with cancel rules\<close>
    2.99 +
   2.100 +class euclidean_semiring_cancel = euclidean_semiring + semiring_div
   2.101 +
   2.102 +class euclidean_ring_cancel = euclidean_ring + ring_div
   2.103 +
   2.104 +context unique_euclidean_semiring
   2.105 +begin
   2.106 +
   2.107 +subclass euclidean_semiring_cancel
   2.108 +proof
   2.109 +  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   2.110 +  proof (cases a b rule: divmod_cases)
   2.111 +    case by0
   2.112 +    with \<open>b \<noteq> 0\<close> show ?thesis
   2.113 +      by simp
   2.114 +  next
   2.115 +    case (divides q)
   2.116 +    then show ?thesis
   2.117 +      by (simp add: ac_simps)
   2.118 +  next
   2.119 +    case (remainder q r)
   2.120 +    then show ?thesis
   2.121 +      by (auto intro: div_eqI simp add: algebra_simps)
   2.122 +  qed
   2.123 +next
   2.124 +  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   2.125 +  proof (cases a b rule: divmod_cases)
   2.126 +    case by0
   2.127 +    then show ?thesis
   2.128 +      by simp
   2.129 +  next
   2.130 +    case (divides q)
   2.131 +    with \<open>c \<noteq> 0\<close> show ?thesis
   2.132 +      by (simp add: mult.left_commute [of c])
   2.133 +  next
   2.134 +    case (remainder q r)
   2.135 +    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   2.136 +      by simp
   2.137 +    from remainder \<open>c \<noteq> 0\<close>
   2.138 +    have "uniqueness_constraint (r * c) (b * c)"
   2.139 +      and "euclidean_size (r * c) < euclidean_size (b * c)"
   2.140 +      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   2.141 +    with remainder show ?thesis
   2.142 +      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   2.143 +        (use \<open>b * c \<noteq> 0\<close> in simp)
   2.144 +  qed
   2.145 +qed
   2.146 +
   2.147 +end
   2.148 +
   2.149 +context unique_euclidean_ring
   2.150 +begin
   2.151 +
   2.152 +subclass euclidean_ring_cancel ..
   2.153 +
   2.154 +end
   2.155 +
   2.156  
   2.157  subsection \<open>Parity\<close>
   2.158  
   2.159 @@ -1097,6 +1080,20 @@
   2.160    shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   2.161    by (simp add: dvd_eq_mod_eq_0)
   2.162  
   2.163 +instantiation nat :: unique_euclidean_semiring
   2.164 +begin
   2.165 +
   2.166 +definition [simp]:
   2.167 +  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   2.168 +
   2.169 +definition [simp]:
   2.170 +  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   2.171 +
   2.172 +instance
   2.173 +  by standard (use mult_le_mono2 [of 1] in \<open>simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd\<close>)
   2.174 +
   2.175 +end
   2.176 +
   2.177  text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
   2.178  
   2.179  lemma (in semiring_modulo) cancel_div_mod_rules:
   2.180 @@ -2415,6 +2412,22 @@
   2.181      by simp
   2.182  qed
   2.183  
   2.184 +instantiation int :: unique_euclidean_ring
   2.185 +begin
   2.186 +
   2.187 +definition [simp]:
   2.188 +  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   2.189 +
   2.190 +definition [simp]:
   2.191 +  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   2.192 +  
   2.193 +instance
   2.194 +  by standard
   2.195 +    (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split\<close>)
   2.196 +
   2.197 +end
   2.198 +
   2.199 +  
   2.200  subsubsection \<open>Quotients of Signs\<close>
   2.201  
   2.202  lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Euclidean_Division.thy	Wed Jan 04 21:28:29 2017 +0100
     3.3 @@ -0,0 +1,287 @@
     3.4 +(*  Title:      HOL/Euclidean_Division.thy
     3.5 +    Author:     Manuel Eberl, TU Muenchen
     3.6 +    Author:     Florian Haftmann, TU Muenchen
     3.7 +*)
     3.8 +
     3.9 +section \<open>Uniquely determined division in euclidean (semi)rings\<close>
    3.10 +
    3.11 +theory Euclidean_Division
    3.12 +  imports Nat_Transfer
    3.13 +begin
    3.14 +
    3.15 +subsection \<open>Quotient and remainder in integral domains\<close>
    3.16 +
    3.17 +class semidom_modulo = algebraic_semidom + semiring_modulo
    3.18 +begin
    3.19 +
    3.20 +lemma mod_0 [simp]: "0 mod a = 0"
    3.21 +  using div_mult_mod_eq [of 0 a] by simp
    3.22 +
    3.23 +lemma mod_by_0 [simp]: "a mod 0 = a"
    3.24 +  using div_mult_mod_eq [of a 0] by simp
    3.25 +
    3.26 +lemma mod_by_1 [simp]:
    3.27 +  "a mod 1 = 0"
    3.28 +proof -
    3.29 +  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
    3.30 +  then have "a + a mod 1 = a + 0" by simp
    3.31 +  then show ?thesis by (rule add_left_imp_eq)
    3.32 +qed
    3.33 +
    3.34 +lemma mod_self [simp]:
    3.35 +  "a mod a = 0"
    3.36 +  using div_mult_mod_eq [of a a] by simp
    3.37 +
    3.38 +lemma dvd_imp_mod_0 [simp]:
    3.39 +  assumes "a dvd b"
    3.40 +  shows "b mod a = 0"
    3.41 +  using assms minus_div_mult_eq_mod [of b a] by simp
    3.42 +
    3.43 +lemma mod_0_imp_dvd: 
    3.44 +  assumes "a mod b = 0"
    3.45 +  shows   "b dvd a"
    3.46 +proof -
    3.47 +  have "b dvd ((a div b) * b)" by simp
    3.48 +  also have "(a div b) * b = a"
    3.49 +    using div_mult_mod_eq [of a b] by (simp add: assms)
    3.50 +  finally show ?thesis .
    3.51 +qed
    3.52 +
    3.53 +lemma mod_eq_0_iff_dvd:
    3.54 +  "a mod b = 0 \<longleftrightarrow> b dvd a"
    3.55 +  by (auto intro: mod_0_imp_dvd)
    3.56 +
    3.57 +lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
    3.58 +  "a dvd b \<longleftrightarrow> b mod a = 0"
    3.59 +  by (simp add: mod_eq_0_iff_dvd)
    3.60 +
    3.61 +lemma dvd_mod_iff: 
    3.62 +  assumes "c dvd b"
    3.63 +  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
    3.64 +proof -
    3.65 +  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 
    3.66 +    by (simp add: dvd_add_right_iff)
    3.67 +  also have "(a div b) * b + a mod b = a"
    3.68 +    using div_mult_mod_eq [of a b] by simp
    3.69 +  finally show ?thesis .
    3.70 +qed
    3.71 +
    3.72 +lemma dvd_mod_imp_dvd:
    3.73 +  assumes "c dvd a mod b" and "c dvd b"
    3.74 +  shows "c dvd a"
    3.75 +  using assms dvd_mod_iff [of c b a] by simp
    3.76 +
    3.77 +end
    3.78 +
    3.79 +class idom_modulo = idom + semidom_modulo
    3.80 +begin
    3.81 +
    3.82 +subclass idom_divide ..
    3.83 +
    3.84 +lemma div_diff [simp]:
    3.85 +  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
    3.86 +  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
    3.87 +
    3.88 +end
    3.89 +
    3.90 +  
    3.91 +subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    3.92 +  
    3.93 +class euclidean_semiring = semidom_modulo + normalization_semidom + 
    3.94 +  fixes euclidean_size :: "'a \<Rightarrow> nat"
    3.95 +  assumes size_0 [simp]: "euclidean_size 0 = 0"
    3.96 +  assumes mod_size_less: 
    3.97 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    3.98 +  assumes size_mult_mono:
    3.99 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
   3.100 +begin
   3.101 +
   3.102 +lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
   3.103 +  by (subst mult.commute) (rule size_mult_mono)
   3.104 +
   3.105 +lemma euclidean_size_normalize [simp]:
   3.106 +  "euclidean_size (normalize a) = euclidean_size a"
   3.107 +proof (cases "a = 0")
   3.108 +  case True
   3.109 +  then show ?thesis
   3.110 +    by simp
   3.111 +next
   3.112 +  case [simp]: False
   3.113 +  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
   3.114 +    by (rule size_mult_mono) simp
   3.115 +  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
   3.116 +    by (rule size_mult_mono) simp
   3.117 +  ultimately show ?thesis
   3.118 +    by simp
   3.119 +qed
   3.120 +
   3.121 +lemma dvd_euclidean_size_eq_imp_dvd:
   3.122 +  assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
   3.123 +    and "b dvd a" 
   3.124 +  shows "a dvd b"
   3.125 +proof (rule ccontr)
   3.126 +  assume "\<not> a dvd b"
   3.127 +  hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast
   3.128 +  then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd)
   3.129 +  from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff)
   3.130 +  then obtain c where "b mod a = b * c" unfolding dvd_def by blast
   3.131 +    with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto
   3.132 +  with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b"
   3.133 +    using size_mult_mono by force
   3.134 +  moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close>
   3.135 +  have "euclidean_size (b mod a) < euclidean_size a"
   3.136 +    using mod_size_less by blast
   3.137 +  ultimately show False using \<open>euclidean_size a = euclidean_size b\<close>
   3.138 +    by simp
   3.139 +qed
   3.140 +
   3.141 +lemma euclidean_size_times_unit:
   3.142 +  assumes "is_unit a"
   3.143 +  shows   "euclidean_size (a * b) = euclidean_size b"
   3.144 +proof (rule antisym)
   3.145 +  from assms have [simp]: "a \<noteq> 0" by auto
   3.146 +  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
   3.147 +  from assms have "is_unit (1 div a)" by simp
   3.148 +  hence "1 div a \<noteq> 0" by (intro notI) simp_all
   3.149 +  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
   3.150 +    by (rule size_mult_mono')
   3.151 +  also from assms have "(1 div a) * (a * b) = b"
   3.152 +    by (simp add: algebra_simps unit_div_mult_swap)
   3.153 +  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
   3.154 +qed
   3.155 +
   3.156 +lemma euclidean_size_unit:
   3.157 +  "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1"
   3.158 +  using euclidean_size_times_unit [of a 1] by simp
   3.159 +
   3.160 +lemma unit_iff_euclidean_size: 
   3.161 +  "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0"
   3.162 +proof safe
   3.163 +  assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1"
   3.164 +  show "is_unit a"
   3.165 +    by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all
   3.166 +qed (auto intro: euclidean_size_unit)
   3.167 +
   3.168 +lemma euclidean_size_times_nonunit:
   3.169 +  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a"
   3.170 +  shows   "euclidean_size b < euclidean_size (a * b)"
   3.171 +proof (rule ccontr)
   3.172 +  assume "\<not>euclidean_size b < euclidean_size (a * b)"
   3.173 +  with size_mult_mono'[OF assms(1), of b] 
   3.174 +    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
   3.175 +  have "a * b dvd b"
   3.176 +    by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
   3.177 +  hence "a * b dvd 1 * b" by simp
   3.178 +  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
   3.179 +  with assms(3) show False by contradiction
   3.180 +qed
   3.181 +
   3.182 +lemma dvd_imp_size_le:
   3.183 +  assumes "a dvd b" "b \<noteq> 0" 
   3.184 +  shows   "euclidean_size a \<le> euclidean_size b"
   3.185 +  using assms by (auto elim!: dvdE simp: size_mult_mono)
   3.186 +
   3.187 +lemma dvd_proper_imp_size_less:
   3.188 +  assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 
   3.189 +  shows   "euclidean_size a < euclidean_size b"
   3.190 +proof -
   3.191 +  from assms(1) obtain c where "b = a * c" by (erule dvdE)
   3.192 +  hence z: "b = c * a" by (simp add: mult.commute)
   3.193 +  from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff)
   3.194 +  with z assms show ?thesis
   3.195 +    by (auto intro!: euclidean_size_times_nonunit)
   3.196 +qed
   3.197 +
   3.198 +end
   3.199 +
   3.200 +class euclidean_ring = idom_modulo + euclidean_semiring
   3.201 +
   3.202 +  
   3.203 +subsection \<open>Uniquely determined division\<close>
   3.204 +  
   3.205 +class unique_euclidean_semiring = euclidean_semiring + 
   3.206 +  fixes uniqueness_constraint :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   3.207 +  assumes size_mono_mult:
   3.208 +    "b \<noteq> 0 \<Longrightarrow> euclidean_size a < euclidean_size c
   3.209 +      \<Longrightarrow> euclidean_size (a * b) < euclidean_size (c * b)"
   3.210 +    -- \<open>FIXME justify\<close>
   3.211 +  assumes uniqueness_constraint_mono_mult:
   3.212 +    "uniqueness_constraint a b \<Longrightarrow> uniqueness_constraint (a * c) (b * c)"
   3.213 +  assumes uniqueness_constraint_mod:
   3.214 +    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> uniqueness_constraint (a mod b) b"
   3.215 +  assumes div_bounded:
   3.216 +    "b \<noteq> 0 \<Longrightarrow> uniqueness_constraint r b
   3.217 +    \<Longrightarrow> euclidean_size r < euclidean_size b
   3.218 +    \<Longrightarrow> (q * b + r) div b = q"
   3.219 +begin
   3.220 +
   3.221 +lemma divmod_cases [case_names divides remainder by0]:
   3.222 +  obtains 
   3.223 +    (divides) q where "b \<noteq> 0"
   3.224 +      and "a div b = q"
   3.225 +      and "a mod b = 0"
   3.226 +      and "a = q * b"
   3.227 +  | (remainder) q r where "b \<noteq> 0" and "r \<noteq> 0"
   3.228 +      and "uniqueness_constraint r b"
   3.229 +      and "euclidean_size r < euclidean_size b"
   3.230 +      and "a div b = q"
   3.231 +      and "a mod b = r"
   3.232 +      and "a = q * b + r"
   3.233 +  | (by0) "b = 0"
   3.234 +proof (cases "b = 0")
   3.235 +  case True
   3.236 +  then show thesis
   3.237 +  by (rule by0)
   3.238 +next
   3.239 +  case False
   3.240 +  show thesis
   3.241 +  proof (cases "b dvd a")
   3.242 +    case True
   3.243 +    then obtain q where "a = b * q" ..
   3.244 +    with \<open>b \<noteq> 0\<close> divides
   3.245 +    show thesis
   3.246 +      by (simp add: ac_simps)
   3.247 +  next
   3.248 +    case False
   3.249 +    then have "a mod b \<noteq> 0"
   3.250 +      by (simp add: mod_eq_0_iff_dvd)
   3.251 +    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "uniqueness_constraint (a mod b) b"
   3.252 +      by (rule uniqueness_constraint_mod)
   3.253 +    moreover have "euclidean_size (a mod b) < euclidean_size b"
   3.254 +      using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
   3.255 +    moreover have "a = a div b * b + a mod b"
   3.256 +      by (simp add: div_mult_mod_eq)
   3.257 +    ultimately show thesis
   3.258 +      using \<open>b \<noteq> 0\<close> by (blast intro: remainder)
   3.259 +  qed
   3.260 +qed
   3.261 +
   3.262 +lemma div_eqI:
   3.263 +  "a div b = q" if "b \<noteq> 0" "uniqueness_constraint r b"
   3.264 +    "euclidean_size r < euclidean_size b" "q * b + r = a"
   3.265 +proof -
   3.266 +  from that have "(q * b + r) div b = q"
   3.267 +    by (auto intro: div_bounded)
   3.268 +  with that show ?thesis
   3.269 +    by simp
   3.270 +qed
   3.271 +
   3.272 +lemma mod_eqI:
   3.273 +  "a mod b = r" if "b \<noteq> 0" "uniqueness_constraint r b"
   3.274 +    "euclidean_size r < euclidean_size b" "q * b + r = a" 
   3.275 +proof -
   3.276 +  from that have "a div b = q"
   3.277 +    by (rule div_eqI)
   3.278 +  moreover have "a div b * b + a mod b = a"
   3.279 +    by (fact div_mult_mod_eq)
   3.280 +  ultimately have "a div b * b + a mod b = a div b * b + r"
   3.281 +    using \<open>q * b + r = a\<close> by simp
   3.282 +  then show ?thesis
   3.283 +    by simp
   3.284 +qed
   3.285 +
   3.286 +end
   3.287 +
   3.288 +class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
   3.289 +
   3.290 +end
     4.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 21:28:28 2017 +0100
     4.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 21:28:29 2017 +0100
     4.3 @@ -7,7 +7,6 @@
     4.4  theory Euclidean_Algorithm
     4.5    imports "~~/src/HOL/GCD"
     4.6      "~~/src/HOL/Number_Theory/Factorial_Ring"
     4.7 -    "~~/src/HOL/Number_Theory/Euclidean_Division"
     4.8  begin
     4.9  
    4.10  context euclidean_semiring
     5.1 --- a/src/HOL/Number_Theory/Euclidean_Division.thy	Wed Jan 04 21:28:28 2017 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,295 +0,0 @@
     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
     6.1 --- a/src/HOL/Parity.thy	Wed Jan 04 21:28:28 2017 +0100
     6.2 +++ b/src/HOL/Parity.thy	Wed Jan 04 21:28:29 2017 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  section \<open>Parity in rings and semirings\<close>
     6.5  
     6.6  theory Parity
     6.7 -  imports Nat_Transfer
     6.8 +  imports Nat_Transfer Euclidean_Division
     6.9  begin
    6.10  
    6.11  subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>