abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
authorhaftmann
Sun Oct 08 22:28:21 2017 +0200 (20 months ago)
changeset 66806a4e82b58d833
parent 66805 274b4edca859
child 66807 c3631f32dfeb
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
src/HOL/Binomial.thy
src/HOL/Code_Numeral.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Computational_Algebra/Polynomial.thy
src/HOL/Computational_Algebra/Polynomial_Factorial.thy
src/HOL/Divides.thy
src/HOL/Enum.thy
src/HOL/Euclidean_Division.thy
src/HOL/Factorial.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Rat.thy
src/HOL/ex/Simproc_Tests.thy
src/HOL/ex/Word_Type.thy
     1.1 --- a/src/HOL/Binomial.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Binomial.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -1011,7 +1011,7 @@
     1.4    by (subst binomial_fact_lemma [symmetric]) auto
     1.5  
     1.6  lemma choose_dvd:
     1.7 -  "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::{semiring_div,linordered_semidom})"
     1.8 +  "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::linordered_semidom)"
     1.9    unfolding dvd_def
    1.10    apply (rule exI [where x="of_nat (n choose k)"])
    1.11    using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]
    1.12 @@ -1019,7 +1019,7 @@
    1.13    done
    1.14  
    1.15  lemma fact_fact_dvd_fact:
    1.16 -  "fact k * fact n dvd (fact (k + n) :: 'a::{semiring_div,linordered_semidom})"
    1.17 +  "fact k * fact n dvd (fact (k + n) :: 'a::linordered_semidom)"
    1.18    by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)
    1.19  
    1.20  lemma choose_mult_lemma:
     2.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:21 2017 +0200
     2.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:21 2017 +0200
     2.3 @@ -247,7 +247,7 @@
     2.4  
     2.5  end
     2.6  
     2.7 -instantiation integer :: ring_div
     2.8 +instantiation integer :: unique_euclidean_ring
     2.9  begin
    2.10    
    2.11  lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    2.12 @@ -256,12 +256,33 @@
    2.13  
    2.14  declare modulo_integer.rep_eq [simp]
    2.15  
    2.16 +lift_definition euclidean_size_integer :: "integer \<Rightarrow> nat"
    2.17 +  is "euclidean_size :: int \<Rightarrow> nat"
    2.18 +  .
    2.19 +
    2.20 +declare euclidean_size_integer.rep_eq [simp]
    2.21 +
    2.22 +lift_definition uniqueness_constraint_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool"
    2.23 +  is "uniqueness_constraint :: int \<Rightarrow> int \<Rightarrow> bool"
    2.24 +  .
    2.25 +
    2.26 +declare uniqueness_constraint_integer.rep_eq [simp]
    2.27 +
    2.28  instance
    2.29 -  by (standard; transfer) simp_all
    2.30 +  by (standard; transfer)
    2.31 +    (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>, rule div_eqI, simp_all)
    2.32  
    2.33  end
    2.34  
    2.35 -instantiation integer :: semiring_numeral_div
    2.36 +lemma [code]:
    2.37 +  "euclidean_size = nat_of_integer \<circ> abs"
    2.38 +  by (simp add: fun_eq_iff nat_of_integer.rep_eq)
    2.39 +
    2.40 +lemma [code]:
    2.41 +  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
    2.42 +  by (simp add: integer_eq_iff)
    2.43 +
    2.44 +instantiation integer :: unique_euclidean_semiring_numeral
    2.45  begin
    2.46  
    2.47  definition divmod_integer :: "num \<Rightarrow> num \<Rightarrow> integer \<times> integer"
    2.48 @@ -283,15 +304,15 @@
    2.49      by (fact divmod_step_integer_def)
    2.50  qed (transfer,
    2.51    fact le_add_diff_inverse2
    2.52 -  semiring_numeral_div_class.div_less
    2.53 -  semiring_numeral_div_class.mod_less
    2.54 -  semiring_numeral_div_class.div_positive
    2.55 -  semiring_numeral_div_class.mod_less_eq_dividend
    2.56 -  semiring_numeral_div_class.pos_mod_bound
    2.57 -  semiring_numeral_div_class.pos_mod_sign
    2.58 -  semiring_numeral_div_class.mod_mult2_eq
    2.59 -  semiring_numeral_div_class.div_mult2_eq
    2.60 -  semiring_numeral_div_class.discrete)+
    2.61 +  unique_euclidean_semiring_numeral_class.div_less
    2.62 +  unique_euclidean_semiring_numeral_class.mod_less
    2.63 +  unique_euclidean_semiring_numeral_class.div_positive
    2.64 +  unique_euclidean_semiring_numeral_class.mod_less_eq_dividend
    2.65 +  unique_euclidean_semiring_numeral_class.pos_mod_bound
    2.66 +  unique_euclidean_semiring_numeral_class.pos_mod_sign
    2.67 +  unique_euclidean_semiring_numeral_class.mod_mult2_eq
    2.68 +  unique_euclidean_semiring_numeral_class.div_mult2_eq
    2.69 +  unique_euclidean_semiring_numeral_class.discrete)+
    2.70  
    2.71  end
    2.72  
    2.73 @@ -853,7 +874,7 @@
    2.74    "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)"
    2.75    by transfer rule
    2.76  
    2.77 -instantiation natural :: "{semiring_div, normalization_semidom}"
    2.78 +instantiation natural :: unique_euclidean_semiring
    2.79  begin
    2.80  
    2.81  lift_definition normalize_natural :: "natural \<Rightarrow> natural"
    2.82 @@ -880,11 +901,32 @@
    2.83  
    2.84  declare modulo_natural.rep_eq [simp]
    2.85  
    2.86 +lift_definition euclidean_size_natural :: "natural \<Rightarrow> nat"
    2.87 +  is "euclidean_size :: nat \<Rightarrow> nat"
    2.88 +  .
    2.89 +
    2.90 +declare euclidean_size_natural.rep_eq [simp]
    2.91 +
    2.92 +lift_definition uniqueness_constraint_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool"
    2.93 +  is "uniqueness_constraint :: nat \<Rightarrow> nat \<Rightarrow> bool"
    2.94 +  .
    2.95 +
    2.96 +declare uniqueness_constraint_natural.rep_eq [simp]
    2.97 +
    2.98  instance
    2.99 -  by standard (transfer, auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)+
   2.100 +  by (standard; transfer)
   2.101 +    (auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc)
   2.102  
   2.103  end
   2.104  
   2.105 +lemma [code]:
   2.106 +  "euclidean_size = nat_of_natural"
   2.107 +  by (simp add: fun_eq_iff)
   2.108 +
   2.109 +lemma [code]:
   2.110 +  "uniqueness_constraint = (\<top> :: natural \<Rightarrow> natural \<Rightarrow> bool)"
   2.111 +  by (simp add: fun_eq_iff)
   2.112 +
   2.113  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   2.114    is "nat :: int \<Rightarrow> nat"
   2.115    .
     3.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:21 2017 +0200
     3.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:21 2017 +0200
     3.3 @@ -1181,7 +1181,7 @@
     3.4  
     3.5  end
     3.6  
     3.7 -instantiation fps :: (field) ring_div
     3.8 +instantiation fps :: (field) idom_modulo
     3.9  begin
    3.10  
    3.11  definition fps_mod_def:
    3.12 @@ -1224,39 +1224,6 @@
    3.13    from assms show "f mod g = 0" by (intro fps_mod_eq_zero) auto
    3.14  qed
    3.15  
    3.16 -context
    3.17 -begin
    3.18 -private lemma fps_divide_cancel_aux1:
    3.19 -  assumes "h$0 \<noteq> (0 :: 'a :: field)"
    3.20 -  shows   "(h * f) div (h * g) = f div g"
    3.21 -proof (cases "g = 0")
    3.22 -  assume "g \<noteq> 0"
    3.23 -  from assms have "h \<noteq> 0" by auto
    3.24 -  note nz [simp] = \<open>g \<noteq> 0\<close> \<open>h \<noteq> 0\<close>
    3.25 -  from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff)
    3.26 -
    3.27 -  have "(h * f) div (h * g) =
    3.28 -          fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))"
    3.29 -    by (simp add: fps_divide_def Let_def)
    3.30 -  also have "h * f * inverse (fps_shift (subdegree g) (h*g)) =
    3.31 -               (inverse h * h) * f * inverse (fps_shift (subdegree g) g)"
    3.32 -    by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult)
    3.33 -  also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1)
    3.34 -  finally show "(h * f) div (h * g) = f div g" by (simp_all add: fps_divide_def Let_def)
    3.35 -qed (simp_all add: fps_divide_def)
    3.36 -
    3.37 -private lemma fps_divide_cancel_aux2:
    3.38 -  "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
    3.39 -proof (cases "g = 0")
    3.40 -  assume [simp]: "g \<noteq> 0"
    3.41 -  have "(f * fps_X^m) div (g * fps_X^m) =
    3.42 -          fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
    3.43 -    by (simp add: fps_divide_def Let_def algebra_simps)
    3.44 -  also have "... = f div g"
    3.45 -    by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
    3.46 -  finally show ?thesis .
    3.47 -qed (simp_all add: fps_divide_def)
    3.48 -
    3.49  instance proof
    3.50    fix f g :: "'a fps"
    3.51    define n where "n = subdegree g"
    3.52 @@ -1284,39 +1251,9 @@
    3.53        finally show ?thesis by simp
    3.54      qed
    3.55    qed (auto simp: fps_mod_def fps_divide_def Let_def)
    3.56 -next
    3.57 -
    3.58 -  fix f g h :: "'a fps"
    3.59 -  assume "h \<noteq> 0"
    3.60 -  show "(h * f) div (h * g) = f div g"
    3.61 -  proof -
    3.62 -    define m where "m = subdegree h"
    3.63 -    define h' where "h' = fps_shift m h"
    3.64 -    have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
    3.65 -    from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
    3.66 -    have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
    3.67 -      by (simp add: h_decomp algebra_simps)
    3.68 -    also have "... = f div g" by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
    3.69 -    finally show ?thesis .
    3.70 -  qed
    3.71 -
    3.72 -next
    3.73 -  fix f g h :: "'a fps"
    3.74 -  assume [simp]: "h \<noteq> 0"
    3.75 -  define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
    3.76 -  have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
    3.77 -    by (simp add: fps_divide_def Let_def dfs[symmetric] algebra_simps fps_shift_add)
    3.78 -  also have "h * inverse h' = (inverse h' * h') * fps_X^n"
    3.79 -    by (subst subdegree_decompose) (simp_all add: dfs)
    3.80 -  also have "... = fps_X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs)
    3.81 -  also have "fps_shift n (g * fps_X^n) = g" by simp
    3.82 -  also have "fps_shift n (f * inverse h') = f div h"
    3.83 -    by (simp add: fps_divide_def Let_def dfs)
    3.84 -  finally show "(f + g * h) div h = g + f div h" by simp
    3.85  qed
    3.86  
    3.87  end
    3.88 -end
    3.89  
    3.90  lemma subdegree_mod:
    3.91    assumes "f \<noteq> 0" "subdegree f < subdegree g"
    3.92 @@ -1411,6 +1348,40 @@
    3.93  definition fps_euclidean_size_def:
    3.94    "euclidean_size f = (if f = 0 then 0 else 2 ^ subdegree f)"
    3.95  
    3.96 +context
    3.97 +begin
    3.98 +
    3.99 +private lemma fps_divide_cancel_aux1:
   3.100 +  assumes "h$0 \<noteq> (0 :: 'a :: field)"
   3.101 +  shows   "(h * f) div (h * g) = f div g"
   3.102 +proof (cases "g = 0")
   3.103 +  assume "g \<noteq> 0"
   3.104 +  from assms have "h \<noteq> 0" by auto
   3.105 +  note nz [simp] = \<open>g \<noteq> 0\<close> \<open>h \<noteq> 0\<close>
   3.106 +  from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff)
   3.107 +
   3.108 +  have "(h * f) div (h * g) =
   3.109 +          fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))"
   3.110 +    by (simp add: fps_divide_def Let_def)
   3.111 +  also have "h * f * inverse (fps_shift (subdegree g) (h*g)) =
   3.112 +               (inverse h * h) * f * inverse (fps_shift (subdegree g) g)"
   3.113 +    by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult)
   3.114 +  also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1)
   3.115 +  finally show "(h * f) div (h * g) = f div g" by (simp_all add: fps_divide_def Let_def)
   3.116 +qed (simp_all add: fps_divide_def)
   3.117 +
   3.118 +private lemma fps_divide_cancel_aux2:
   3.119 +  "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)"
   3.120 +proof (cases "g = 0")
   3.121 +  assume [simp]: "g \<noteq> 0"
   3.122 +  have "(f * fps_X^m) div (g * fps_X^m) =
   3.123 +          fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)"
   3.124 +    by (simp add: fps_divide_def Let_def algebra_simps)
   3.125 +  also have "... = f div g"
   3.126 +    by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def)
   3.127 +  finally show ?thesis .
   3.128 +qed (simp_all add: fps_divide_def)
   3.129 +
   3.130  instance proof
   3.131    fix f g :: "'a fps" assume [simp]: "g \<noteq> 0"
   3.132    show "euclidean_size f \<le> euclidean_size (f * g)"
   3.133 @@ -1420,10 +1391,40 @@
   3.134      apply (rule disjE[OF le_less_linear[of "subdegree g" "subdegree f"]])
   3.135      apply (simp_all add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod)
   3.136      done
   3.137 +  show "(h * f) div (h * g) = f div g" if "h \<noteq> 0"
   3.138 +    for f g h :: "'a fps"
   3.139 +  proof -
   3.140 +    define m where "m = subdegree h"
   3.141 +    define h' where "h' = fps_shift m h"
   3.142 +    have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose)
   3.143 +    from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def)
   3.144 +    have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)"
   3.145 +      by (simp add: h_decomp algebra_simps)
   3.146 +    also have "... = f div g"
   3.147 +      by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2)
   3.148 +    finally show ?thesis .
   3.149 +  qed
   3.150 +  show "(f + g * h) div h = g + f div h"
   3.151 +    if "h \<noteq> 0" for f g h :: "'a fps"
   3.152 +  proof -
   3.153 +    define n h' where dfs: "n = subdegree h" "h' = fps_shift n h"
   3.154 +    have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))"
   3.155 +      by (simp add: fps_divide_def Let_def dfs [symmetric] algebra_simps fps_shift_add that)
   3.156 +    also have "h * inverse h' = (inverse h' * h') * fps_X^n"
   3.157 +      by (subst subdegree_decompose) (simp_all add: dfs)
   3.158 +    also have "... = fps_X^n"
   3.159 +      by (subst inverse_mult_eq_1) (simp_all add: dfs that)
   3.160 +    also have "fps_shift n (g * fps_X^n) = g" by simp
   3.161 +    also have "fps_shift n (f * inverse h') = f div h"
   3.162 +      by (simp add: fps_divide_def Let_def dfs)
   3.163 +    finally show ?thesis by simp
   3.164 +  qed
   3.165  qed (simp_all add: fps_euclidean_size_def)
   3.166  
   3.167  end
   3.168  
   3.169 +end
   3.170 +
   3.171  instantiation fps :: (field) euclidean_ring_gcd
   3.172  begin
   3.173  definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"
     4.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:21 2017 +0200
     4.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:21 2017 +0200
     4.3 @@ -3637,40 +3637,7 @@
     4.4    for x :: "'a::field poly"
     4.5    by (rule eucl_rel_poly_unique_mod [OF eucl_rel_poly])
     4.6  
     4.7 -instance poly :: (field) ring_div
     4.8 -proof
     4.9 -  fix x y z :: "'a poly"
    4.10 -  assume "y \<noteq> 0"
    4.11 -  with eucl_rel_poly [of x y] have "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
    4.12 -    by (simp add: eucl_rel_poly_iff distrib_right)
    4.13 -  then show "(x + z * y) div y = z + x div y"
    4.14 -    by (rule div_poly_eq)
    4.15 -next
    4.16 -  fix x y z :: "'a poly"
    4.17 -  assume "x \<noteq> 0"
    4.18 -  show "(x * y) div (x * z) = y div z"
    4.19 -  proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
    4.20 -    have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
    4.21 -      by (rule eucl_rel_poly_by_0)
    4.22 -    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
    4.23 -      by (rule div_poly_eq)
    4.24 -    have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
    4.25 -      by (rule eucl_rel_poly_0)
    4.26 -    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
    4.27 -      by (rule div_poly_eq)
    4.28 -    case False
    4.29 -    then show ?thesis by auto
    4.30 -  next
    4.31 -    case True
    4.32 -    then have "y \<noteq> 0" and "z \<noteq> 0" by auto
    4.33 -    with \<open>x \<noteq> 0\<close> have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
    4.34 -      by (auto simp: eucl_rel_poly_iff algebra_simps) (rule classical, simp add: degree_mult_eq)
    4.35 -    moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
    4.36 -    ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
    4.37 -    then show ?thesis
    4.38 -      by (simp add: div_poly_eq)
    4.39 -  qed
    4.40 -qed
    4.41 +instance poly :: (field) idom_modulo ..
    4.42  
    4.43  lemma div_pCons_eq:
    4.44    "pCons a p div q =
     5.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     5.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     5.3 @@ -459,11 +459,17 @@
     5.4      ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))"
     5.5        by (auto simp add: degree_mult_eq)
     5.6    next
     5.7 -    fix p q r :: "'a poly" assume "p \<noteq> 0"
     5.8 +    fix p q r :: "'a poly"
     5.9 +    assume "p \<noteq> 0"
    5.10 +    with eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
    5.11 +      by (simp add: eucl_rel_poly_iff distrib_right)
    5.12 +    then have "(r + q * p) div p = q + r div p"
    5.13 +      by (rule div_poly_eq)
    5.14      moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r)
    5.15 -    < (if p = 0 then 0 else 2 ^ degree p)"
    5.16 +      < (if p = 0 then 0 else 2 ^ degree p)"
    5.17      ultimately show "(q * p + r) div p = q"
    5.18 -      by (cases "r = 0") (auto simp add: div_poly_less)
    5.19 +      using \<open>p \<noteq> 0\<close>
    5.20 +      by (cases "r = 0") (simp_all add: div_poly_less ac_simps)
    5.21    qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
    5.22  qed
    5.23  
    5.24 @@ -761,9 +767,18 @@
    5.25  definition uniqueness_constraint_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
    5.26    where [simp]: "uniqueness_constraint_poly = top"
    5.27  
    5.28 -instance 
    5.29 -  by standard
    5.30 -   (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
    5.31 +instance proof
    5.32 +  show "(q * p + r) div p = q" if "p \<noteq> 0"
    5.33 +    and "euclidean_size r < euclidean_size p" for q p r :: "'a poly"
    5.34 +  proof -
    5.35 +    from \<open>p \<noteq> 0\<close> eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
    5.36 +      by (simp add: eucl_rel_poly_iff distrib_right)
    5.37 +    then have "(r + q * p) div p = q + r div p"
    5.38 +      by (rule div_poly_eq)
    5.39 +    with that show ?thesis
    5.40 +      by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps)
    5.41 +  qed
    5.42 +qed (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
    5.43      split: if_splits)
    5.44  
    5.45  end
     6.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     6.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     6.3 @@ -9,433 +9,9 @@
     6.4  imports Parity
     6.5  begin
     6.6  
     6.7 -subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
     6.8 -
     6.9 -class semiring_div = semidom_modulo +
    6.10 -  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    6.11 -    and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
    6.12 -begin
    6.13 -
    6.14 -lemma div_mult_self2 [simp]:
    6.15 -  assumes "b \<noteq> 0"
    6.16 -  shows "(a + b * c) div b = c + a div b"
    6.17 -  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
    6.18 -
    6.19 -lemma div_mult_self3 [simp]:
    6.20 -  assumes "b \<noteq> 0"
    6.21 -  shows "(c * b + a) div b = c + a div b"
    6.22 -  using assms by (simp add: add.commute)
    6.23 -
    6.24 -lemma div_mult_self4 [simp]:
    6.25 -  assumes "b \<noteq> 0"
    6.26 -  shows "(b * c + a) div b = c + a div b"
    6.27 -  using assms by (simp add: add.commute)
    6.28 -
    6.29 -lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
    6.30 -proof (cases "b = 0")
    6.31 -  case True then show ?thesis by simp
    6.32 -next
    6.33 -  case False
    6.34 -  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
    6.35 -    by (simp add: div_mult_mod_eq)
    6.36 -  also from False div_mult_self1 [of b a c] have
    6.37 -    "\<dots> = (c + a div b) * b + (a + c * b) mod b"
    6.38 -      by (simp add: algebra_simps)
    6.39 -  finally have "a = a div b * b + (a + c * b) mod b"
    6.40 -    by (simp add: add.commute [of a] add.assoc distrib_right)
    6.41 -  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
    6.42 -    by (simp add: div_mult_mod_eq)
    6.43 -  then show ?thesis by simp
    6.44 -qed
    6.45 -
    6.46 -lemma mod_mult_self2 [simp]:
    6.47 -  "(a + b * c) mod b = a mod b"
    6.48 -  by (simp add: mult.commute [of b])
    6.49 -
    6.50 -lemma mod_mult_self3 [simp]:
    6.51 -  "(c * b + a) mod b = a mod b"
    6.52 -  by (simp add: add.commute)
    6.53 -
    6.54 -lemma mod_mult_self4 [simp]:
    6.55 -  "(b * c + a) mod b = a mod b"
    6.56 -  by (simp add: add.commute)
    6.57 -
    6.58 -lemma mod_mult_self1_is_0 [simp]:
    6.59 -  "b * a mod b = 0"
    6.60 -  using mod_mult_self2 [of 0 b a] by simp
    6.61 -
    6.62 -lemma mod_mult_self2_is_0 [simp]:
    6.63 -  "a * b mod b = 0"
    6.64 -  using mod_mult_self1 [of 0 a b] by simp
    6.65 -
    6.66 -lemma div_add_self1:
    6.67 -  assumes "b \<noteq> 0"
    6.68 -  shows "(b + a) div b = a div b + 1"
    6.69 -  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
    6.70 -
    6.71 -lemma div_add_self2:
    6.72 -  assumes "b \<noteq> 0"
    6.73 -  shows "(a + b) div b = a div b + 1"
    6.74 -  using assms div_add_self1 [of b a] by (simp add: add.commute)
    6.75 -
    6.76 -lemma mod_add_self1 [simp]:
    6.77 -  "(b + a) mod b = a mod b"
    6.78 -  using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
    6.79 -
    6.80 -lemma mod_add_self2 [simp]:
    6.81 -  "(a + b) mod b = a mod b"
    6.82 -  using mod_mult_self1 [of a 1 b] by simp
    6.83 -
    6.84 -lemma mod_div_trivial [simp]:
    6.85 -  "a mod b div b = 0"
    6.86 -proof (cases "b = 0")
    6.87 -  assume "b = 0"
    6.88 -  thus ?thesis by simp
    6.89 -next
    6.90 -  assume "b \<noteq> 0"
    6.91 -  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
    6.92 -    by (rule div_mult_self1 [symmetric])
    6.93 -  also have "\<dots> = a div b"
    6.94 -    by (simp only: mod_div_mult_eq)
    6.95 -  also have "\<dots> = a div b + 0"
    6.96 -    by simp
    6.97 -  finally show ?thesis
    6.98 -    by (rule add_left_imp_eq)
    6.99 -qed
   6.100 -
   6.101 -lemma mod_mod_trivial [simp]:
   6.102 -  "a mod b mod b = a mod b"
   6.103 -proof -
   6.104 -  have "a mod b mod b = (a mod b + a div b * b) mod b"
   6.105 -    by (simp only: mod_mult_self1)
   6.106 -  also have "\<dots> = a mod b"
   6.107 -    by (simp only: mod_div_mult_eq)
   6.108 -  finally show ?thesis .
   6.109 -qed
   6.110 -
   6.111 -lemma mod_mod_cancel:
   6.112 -  assumes "c dvd b"
   6.113 -  shows "a mod b mod c = a mod c"
   6.114 -proof -
   6.115 -  from \<open>c dvd b\<close> obtain k where "b = c * k"
   6.116 -    by (rule dvdE)
   6.117 -  have "a mod b mod c = a mod (c * k) mod c"
   6.118 -    by (simp only: \<open>b = c * k\<close>)
   6.119 -  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
   6.120 -    by (simp only: mod_mult_self1)
   6.121 -  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
   6.122 -    by (simp only: ac_simps)
   6.123 -  also have "\<dots> = a mod c"
   6.124 -    by (simp only: div_mult_mod_eq)
   6.125 -  finally show ?thesis .
   6.126 -qed
   6.127 -
   6.128 -lemma div_mult_mult2 [simp]:
   6.129 -  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   6.130 -  by (drule div_mult_mult1) (simp add: mult.commute)
   6.131 -
   6.132 -lemma div_mult_mult1_if [simp]:
   6.133 -  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
   6.134 -  by simp_all
   6.135 -
   6.136 -lemma mod_mult_mult1:
   6.137 -  "(c * a) mod (c * b) = c * (a mod b)"
   6.138 -proof (cases "c = 0")
   6.139 -  case True then show ?thesis by simp
   6.140 -next
   6.141 -  case False
   6.142 -  from div_mult_mod_eq
   6.143 -  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   6.144 -  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
   6.145 -    = c * a + c * (a mod b)" by (simp add: algebra_simps)
   6.146 -  with div_mult_mod_eq show ?thesis by simp
   6.147 -qed
   6.148 -
   6.149 -lemma mod_mult_mult2:
   6.150 -  "(a * c) mod (b * c) = (a mod b) * c"
   6.151 -  using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
   6.152 -
   6.153 -lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
   6.154 -  by (fact mod_mult_mult2 [symmetric])
   6.155 -
   6.156 -lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   6.157 -  by (fact mod_mult_mult1 [symmetric])
   6.158 -
   6.159 -lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   6.160 -  unfolding dvd_def by (auto simp add: mod_mult_mult1)
   6.161 -
   6.162 -lemma div_plus_div_distrib_dvd_left:
   6.163 -  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
   6.164 -  by (cases "c = 0") (auto elim: dvdE)
   6.165 -
   6.166 -lemma div_plus_div_distrib_dvd_right:
   6.167 -  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
   6.168 -  using div_plus_div_distrib_dvd_left [of c b a]
   6.169 -  by (simp add: ac_simps)
   6.170 -
   6.171 -named_theorems mod_simps
   6.172 -
   6.173 -text \<open>Addition respects modular equivalence.\<close>
   6.174 -
   6.175 -lemma mod_add_left_eq [mod_simps]:
   6.176 -  "(a mod c + b) mod c = (a + b) mod c"
   6.177 -proof -
   6.178 -  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   6.179 -    by (simp only: div_mult_mod_eq)
   6.180 -  also have "\<dots> = (a mod c + b + a div c * c) mod c"
   6.181 -    by (simp only: ac_simps)
   6.182 -  also have "\<dots> = (a mod c + b) mod c"
   6.183 -    by (rule mod_mult_self1)
   6.184 -  finally show ?thesis
   6.185 -    by (rule sym)
   6.186 -qed
   6.187 -
   6.188 -lemma mod_add_right_eq [mod_simps]:
   6.189 -  "(a + b mod c) mod c = (a + b) mod c"
   6.190 -  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
   6.191 -
   6.192 -lemma mod_add_eq:
   6.193 -  "(a mod c + b mod c) mod c = (a + b) mod c"
   6.194 -  by (simp add: mod_add_left_eq mod_add_right_eq)
   6.195 -
   6.196 -lemma mod_sum_eq [mod_simps]:
   6.197 -  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
   6.198 -proof (induct A rule: infinite_finite_induct)
   6.199 -  case (insert i A)
   6.200 -  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
   6.201 -    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
   6.202 -    by simp
   6.203 -  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
   6.204 -    by (simp add: mod_simps)
   6.205 -  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
   6.206 -    by (simp add: insert.hyps)
   6.207 -  finally show ?case
   6.208 -    by (simp add: insert.hyps mod_simps)
   6.209 -qed simp_all
   6.210 -
   6.211 -lemma mod_add_cong:
   6.212 -  assumes "a mod c = a' mod c"
   6.213 -  assumes "b mod c = b' mod c"
   6.214 -  shows "(a + b) mod c = (a' + b') mod c"
   6.215 -proof -
   6.216 -  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
   6.217 -    unfolding assms ..
   6.218 -  then show ?thesis
   6.219 -    by (simp add: mod_add_eq)
   6.220 -qed
   6.221 -
   6.222 -text \<open>Multiplication respects modular equivalence.\<close>
   6.223 -
   6.224 -lemma mod_mult_left_eq [mod_simps]:
   6.225 -  "((a mod c) * b) mod c = (a * b) mod c"
   6.226 -proof -
   6.227 -  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   6.228 -    by (simp only: div_mult_mod_eq)
   6.229 -  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
   6.230 -    by (simp only: algebra_simps)
   6.231 -  also have "\<dots> = (a mod c * b) mod c"
   6.232 -    by (rule mod_mult_self1)
   6.233 -  finally show ?thesis
   6.234 -    by (rule sym)
   6.235 -qed
   6.236 -
   6.237 -lemma mod_mult_right_eq [mod_simps]:
   6.238 -  "(a * (b mod c)) mod c = (a * b) mod c"
   6.239 -  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
   6.240 -
   6.241 -lemma mod_mult_eq:
   6.242 -  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
   6.243 -  by (simp add: mod_mult_left_eq mod_mult_right_eq)
   6.244 -
   6.245 -lemma mod_prod_eq [mod_simps]:
   6.246 -  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
   6.247 -proof (induct A rule: infinite_finite_induct)
   6.248 -  case (insert i A)
   6.249 -  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
   6.250 -    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
   6.251 -    by simp
   6.252 -  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
   6.253 -    by (simp add: mod_simps)
   6.254 -  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
   6.255 -    by (simp add: insert.hyps)
   6.256 -  finally show ?case
   6.257 -    by (simp add: insert.hyps mod_simps)
   6.258 -qed simp_all
   6.259 -
   6.260 -lemma mod_mult_cong:
   6.261 -  assumes "a mod c = a' mod c"
   6.262 -  assumes "b mod c = b' mod c"
   6.263 -  shows "(a * b) mod c = (a' * b') mod c"
   6.264 -proof -
   6.265 -  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   6.266 -    unfolding assms ..
   6.267 -  then show ?thesis
   6.268 -    by (simp add: mod_mult_eq)
   6.269 -qed
   6.270 -
   6.271 -text \<open>Exponentiation respects modular equivalence.\<close>
   6.272 -
   6.273 -lemma power_mod [mod_simps]: 
   6.274 -  "((a mod b) ^ n) mod b = (a ^ n) mod b"
   6.275 -proof (induct n)
   6.276 -  case 0
   6.277 -  then show ?case by simp
   6.278 -next
   6.279 -  case (Suc n)
   6.280 -  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
   6.281 -    by (simp add: mod_mult_right_eq)
   6.282 -  with Suc show ?case
   6.283 -    by (simp add: mod_mult_left_eq mod_mult_right_eq)
   6.284 -qed
   6.285 -
   6.286 -end
   6.287 -
   6.288 -class ring_div = comm_ring_1 + semiring_div
   6.289 -begin
   6.290 -
   6.291 -subclass idom_divide ..
   6.292 -
   6.293 -lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
   6.294 -  using div_mult_mult1 [of "- 1" a b] by simp
   6.295 -
   6.296 -lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   6.297 -  using mod_mult_mult1 [of "- 1" a b] by simp
   6.298 -
   6.299 -lemma div_minus_right: "a div (- b) = (- a) div b"
   6.300 -  using div_minus_minus [of "- a" b] by simp
   6.301 -
   6.302 -lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   6.303 -  using mod_minus_minus [of "- a" b] by simp
   6.304 -
   6.305 -lemma div_minus1_right [simp]: "a div (- 1) = - a"
   6.306 -  using div_minus_right [of a 1] by simp
   6.307 -
   6.308 -lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   6.309 -  using mod_minus_right [of a 1] by simp
   6.310 -
   6.311 -text \<open>Negation respects modular equivalence.\<close>
   6.312 -
   6.313 -lemma mod_minus_eq [mod_simps]:
   6.314 -  "(- (a mod b)) mod b = (- a) mod b"
   6.315 -proof -
   6.316 -  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   6.317 -    by (simp only: div_mult_mod_eq)
   6.318 -  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
   6.319 -    by (simp add: ac_simps)
   6.320 -  also have "\<dots> = (- (a mod b)) mod b"
   6.321 -    by (rule mod_mult_self1)
   6.322 -  finally show ?thesis
   6.323 -    by (rule sym)
   6.324 -qed
   6.325 -
   6.326 -lemma mod_minus_cong:
   6.327 -  assumes "a mod b = a' mod b"
   6.328 -  shows "(- a) mod b = (- a') mod b"
   6.329 -proof -
   6.330 -  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
   6.331 -    unfolding assms ..
   6.332 -  then show ?thesis
   6.333 -    by (simp add: mod_minus_eq)
   6.334 -qed
   6.335 -
   6.336 -text \<open>Subtraction respects modular equivalence.\<close>
   6.337 -
   6.338 -lemma mod_diff_left_eq [mod_simps]:
   6.339 -  "(a mod c - b) mod c = (a - b) mod c"
   6.340 -  using mod_add_cong [of a c "a mod c" "- b" "- b"]
   6.341 -  by simp
   6.342 -
   6.343 -lemma mod_diff_right_eq [mod_simps]:
   6.344 -  "(a - b mod c) mod c = (a - b) mod c"
   6.345 -  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   6.346 -  by simp
   6.347 -
   6.348 -lemma mod_diff_eq:
   6.349 -  "(a mod c - b mod c) mod c = (a - b) mod c"
   6.350 -  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   6.351 -  by simp
   6.352 -
   6.353 -lemma mod_diff_cong:
   6.354 -  assumes "a mod c = a' mod c"
   6.355 -  assumes "b mod c = b' mod c"
   6.356 -  shows "(a - b) mod c = (a' - b') mod c"
   6.357 -  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
   6.358 -  by simp
   6.359 -
   6.360 -lemma minus_mod_self2 [simp]:
   6.361 -  "(a - b) mod b = a mod b"
   6.362 -  using mod_diff_right_eq [of a b b]
   6.363 -  by (simp add: mod_diff_right_eq)
   6.364 -
   6.365 -lemma minus_mod_self1 [simp]:
   6.366 -  "(b - a) mod b = - a mod b"
   6.367 -  using mod_add_self2 [of "- a" b] by simp
   6.368 -
   6.369 -end
   6.370 -
   6.371 -  
   6.372 -subsection \<open>Euclidean (semi)rings with cancel rules\<close>
   6.373 -
   6.374 -class euclidean_semiring_cancel = euclidean_semiring + semiring_div
   6.375 -
   6.376 -class euclidean_ring_cancel = euclidean_ring + ring_div
   6.377 -
   6.378 -context unique_euclidean_semiring
   6.379 -begin
   6.380 -
   6.381 -subclass euclidean_semiring_cancel
   6.382 -proof
   6.383 -  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   6.384 -  proof (cases a b rule: divmod_cases)
   6.385 -    case by0
   6.386 -    with \<open>b \<noteq> 0\<close> show ?thesis
   6.387 -      by simp
   6.388 -  next
   6.389 -    case (divides q)
   6.390 -    then show ?thesis
   6.391 -      by (simp add: ac_simps)
   6.392 -  next
   6.393 -    case (remainder q r)
   6.394 -    then show ?thesis
   6.395 -      by (auto intro: div_eqI simp add: algebra_simps)
   6.396 -  qed
   6.397 -next
   6.398 -  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   6.399 -  proof (cases a b rule: divmod_cases)
   6.400 -    case by0
   6.401 -    then show ?thesis
   6.402 -      by simp
   6.403 -  next
   6.404 -    case (divides q)
   6.405 -    with \<open>c \<noteq> 0\<close> show ?thesis
   6.406 -      by (simp add: mult.left_commute [of c])
   6.407 -  next
   6.408 -    case (remainder q r)
   6.409 -    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   6.410 -      by simp
   6.411 -    from remainder \<open>c \<noteq> 0\<close>
   6.412 -    have "uniqueness_constraint (r * c) (b * c)"
   6.413 -      and "euclidean_size (r * c) < euclidean_size (b * c)"
   6.414 -      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   6.415 -    with remainder show ?thesis
   6.416 -      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   6.417 -        (use \<open>b * c \<noteq> 0\<close> in simp)
   6.418 -  qed
   6.419 -qed
   6.420 -
   6.421 -end
   6.422 -
   6.423 -context unique_euclidean_ring
   6.424 -begin
   6.425 -
   6.426 -subclass euclidean_ring_cancel ..
   6.427 -
   6.428 -end
   6.429 -
   6.430 -
   6.431  subsection \<open>Parity\<close>
   6.432  
   6.433 -class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
   6.434 +class unique_euclidean_semiring_parity = unique_euclidean_semiring +
   6.435    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   6.436    assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   6.437    assumes zero_not_eq_two: "0 \<noteq> 2"
   6.438 @@ -532,7 +108,7 @@
   6.439    and less technical class hierarchy.
   6.440  \<close>
   6.441  
   6.442 -class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
   6.443 +class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
   6.444    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
   6.445      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
   6.446      and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
   6.447 @@ -553,7 +129,7 @@
   6.448      yields a significant speedup.\<close>
   6.449  begin
   6.450  
   6.451 -subclass semiring_div_parity
   6.452 +subclass unique_euclidean_semiring_parity
   6.453  proof
   6.454    fix a
   6.455    show "a mod 2 = 0 \<or> a mod 2 = 1"
   6.456 @@ -1050,58 +626,6 @@
   6.457  
   6.458  end
   6.459  
   6.460 -instance nat :: semiring_div
   6.461 -proof
   6.462 -  fix m n q :: nat
   6.463 -  assume "n \<noteq> 0"
   6.464 -  then show "(q + m * n) div n = m + q div n"
   6.465 -    by (induct m) (simp_all add: le_div_geq)
   6.466 -next
   6.467 -  fix m n q :: nat
   6.468 -  assume "m \<noteq> 0"
   6.469 -  show "(m * n) div (m * q) = n div q"
   6.470 -  proof (cases "q = 0")
   6.471 -    case True
   6.472 -    then show ?thesis
   6.473 -      by simp
   6.474 -  next
   6.475 -    case False
   6.476 -    show ?thesis
   6.477 -    proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
   6.478 -      show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
   6.479 -        by (rule eucl_rel_natI)
   6.480 -          (use \<open>m \<noteq> 0\<close> \<open>q \<noteq> 0\<close> div_mult_mod_eq [of n q] in \<open>auto simp add: algebra_simps distrib_left [symmetric]\<close>)
   6.481 -    qed          
   6.482 -  qed
   6.483 -qed
   6.484 -
   6.485 -lemma div_by_Suc_0 [simp]:
   6.486 -  "m div Suc 0 = m"
   6.487 -  using div_by_1 [of m] by simp
   6.488 -
   6.489 -lemma mod_by_Suc_0 [simp]:
   6.490 -  "m mod Suc 0 = 0"
   6.491 -  using mod_by_1 [of m] by simp
   6.492 -
   6.493 -lemma mod_greater_zero_iff_not_dvd:
   6.494 -  fixes m n :: nat
   6.495 -  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   6.496 -  by (simp add: dvd_eq_mod_eq_0)
   6.497 -
   6.498 -instantiation nat :: unique_euclidean_semiring
   6.499 -begin
   6.500 -
   6.501 -definition [simp]:
   6.502 -  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   6.503 -
   6.504 -definition [simp]:
   6.505 -  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   6.506 -
   6.507 -instance
   6.508 -  by standard (use mult_le_mono2 [of 1] in \<open>simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd\<close>)
   6.509 -
   6.510 -end
   6.511 -
   6.512  text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
   6.513  
   6.514  lemma (in semiring_modulo) cancel_div_mod_rules:
   6.515 @@ -1142,6 +666,41 @@
   6.516  simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   6.517    \<open>K Cancel_Div_Mod_Nat.proc\<close>
   6.518  
   6.519 +lemma div_by_Suc_0 [simp]:
   6.520 +  "m div Suc 0 = m"
   6.521 +  using div_by_1 [of m] by simp
   6.522 +
   6.523 +lemma mod_by_Suc_0 [simp]:
   6.524 +  "m mod Suc 0 = 0"
   6.525 +  using mod_by_1 [of m] by simp
   6.526 +
   6.527 +lemma mod_greater_zero_iff_not_dvd:
   6.528 +  fixes m n :: nat
   6.529 +  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   6.530 +  by (simp add: dvd_eq_mod_eq_0)
   6.531 +
   6.532 +instantiation nat :: unique_euclidean_semiring
   6.533 +begin
   6.534 +
   6.535 +definition [simp]:
   6.536 +  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   6.537 +
   6.538 +definition [simp]:
   6.539 +  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   6.540 +
   6.541 +instance proof
   6.542 +  fix n q r :: nat
   6.543 +  assume "euclidean_size r < euclidean_size n"
   6.544 +  then have "n > r"
   6.545 +    by simp_all
   6.546 +  then have "eucl_rel_nat (q * n + r) n (q, r)"
   6.547 +    by (rule eucl_rel_natI) rule
   6.548 +  then show "(q * n + r) div n = q"
   6.549 +    by (rule div_nat_unique)
   6.550 +qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
   6.551 +
   6.552 +end
   6.553 +  
   6.554  lemma divmod_nat_if [code]:
   6.555    "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   6.556      let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   6.557 @@ -1262,7 +821,7 @@
   6.558  lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
   6.559  by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
   6.560  
   6.561 -instantiation nat :: semiring_numeral_div
   6.562 +instantiation nat :: unique_euclidean_semiring_numeral
   6.563  begin
   6.564  
   6.565  definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
   6.566 @@ -1820,6 +1379,25 @@
   6.567  
   6.568  end
   6.569  
   6.570 +ML \<open>
   6.571 +structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   6.572 +(
   6.573 +  val div_name = @{const_name divide};
   6.574 +  val mod_name = @{const_name modulo};
   6.575 +  val mk_binop = HOLogic.mk_binop;
   6.576 +  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
   6.577 +  val dest_sum = Arith_Data.dest_sum;
   6.578 +
   6.579 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   6.580 +
   6.581 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   6.582 +    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   6.583 +)
   6.584 +\<close>
   6.585 +
   6.586 +simproc_setup cancel_div_mod_int ("(k::int) + l") =
   6.587 +  \<open>K Cancel_Div_Mod_Int.proc\<close>
   6.588 +
   6.589  lemma is_unit_int:
   6.590    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   6.591    by auto
   6.592 @@ -1921,50 +1499,28 @@
   6.593    using assms unfolding modulo_int_def [of k l]
   6.594    by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
   6.595  
   6.596 -instance int :: ring_div
   6.597 -proof
   6.598 -  fix k l s :: int
   6.599 -  assume "l \<noteq> 0"
   6.600 -  then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
   6.601 -    using eucl_rel_int [of k l]
   6.602 -    unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
   6.603 -  then show "(k + s * l) div l = s + k div l"
   6.604 +instantiation int :: unique_euclidean_ring
   6.605 +begin
   6.606 +
   6.607 +definition [simp]:
   6.608 +  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   6.609 +
   6.610 +definition [simp]:
   6.611 +  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   6.612 +  
   6.613 +instance proof
   6.614 +  fix l q r:: int
   6.615 +  assume "uniqueness_constraint r l"
   6.616 +    and "euclidean_size r < euclidean_size l"
   6.617 +  then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
   6.618 +    by simp_all
   6.619 +  then have "eucl_rel_int (q * l + r) l (q, r)"
   6.620 +    by (rule eucl_rel_int_remainderI) simp
   6.621 +  then show "(q * l + r) div l = q"
   6.622      by (rule div_int_unique)
   6.623 -next
   6.624 -  fix k l s :: int
   6.625 -  assume "s \<noteq> 0"
   6.626 -  have "\<And>q r. eucl_rel_int k l (q, r)
   6.627 -    \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
   6.628 -    unfolding eucl_rel_int_iff
   6.629 -    by (rule linorder_cases [of 0 l])
   6.630 -      (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
   6.631 -      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
   6.632 -      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
   6.633 -  then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
   6.634 -    using eucl_rel_int [of k l] .
   6.635 -  then show "(s * k) div (s * l) = k div l"
   6.636 -    by (rule div_int_unique)
   6.637 -qed
   6.638 +qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
   6.639  
   6.640 -ML \<open>
   6.641 -structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   6.642 -(
   6.643 -  val div_name = @{const_name divide};
   6.644 -  val mod_name = @{const_name modulo};
   6.645 -  val mk_binop = HOLogic.mk_binop;
   6.646 -  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
   6.647 -  val dest_sum = Arith_Data.dest_sum;
   6.648 -
   6.649 -  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   6.650 -
   6.651 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   6.652 -    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   6.653 -)
   6.654 -\<close>
   6.655 -
   6.656 -simproc_setup cancel_div_mod_int ("(k::int) + l") =
   6.657 -  \<open>K Cancel_Div_Mod_Int.proc\<close>
   6.658 -
   6.659 +end
   6.660  
   6.661  text\<open>Basic laws about division and remainder\<close>
   6.662  
   6.663 @@ -2420,21 +1976,6 @@
   6.664      by simp
   6.665  qed
   6.666  
   6.667 -instantiation int :: unique_euclidean_ring
   6.668 -begin
   6.669 -
   6.670 -definition [simp]:
   6.671 -  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   6.672 -
   6.673 -definition [simp]:
   6.674 -  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   6.675 -  
   6.676 -instance
   6.677 -  by standard
   6.678 -    (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>)
   6.679 -
   6.680 -end
   6.681 -
   6.682    
   6.683  subsubsection \<open>Quotients of Signs\<close>
   6.684  
   6.685 @@ -2506,7 +2047,7 @@
   6.686  
   6.687  subsubsection \<open>Computation of Division and Remainder\<close>
   6.688  
   6.689 -instantiation int :: semiring_numeral_div
   6.690 +instantiation int :: unique_euclidean_semiring_numeral
   6.691  begin
   6.692  
   6.693  definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
   6.694 @@ -2687,22 +2228,6 @@
   6.695  apply (rule Divides.div_less_dividend, simp_all)
   6.696  done
   6.697  
   6.698 -lemma (in ring_div) mod_eq_dvd_iff:
   6.699 -  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
   6.700 -proof
   6.701 -  assume ?P
   6.702 -  then have "(a mod c - b mod c) mod c = 0"
   6.703 -    by simp
   6.704 -  then show ?Q
   6.705 -    by (simp add: dvd_eq_mod_eq_0 mod_simps)
   6.706 -next
   6.707 -  assume ?Q
   6.708 -  then obtain d where d: "a - b = c * d" ..
   6.709 -  then have "a = c * d + b"
   6.710 -    by (simp add: algebra_simps)
   6.711 -  then show ?P by simp
   6.712 -qed
   6.713 -
   6.714  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
   6.715    shows "\<exists>q. x = y + n * q"
   6.716  proof-
   6.717 @@ -2742,23 +2267,23 @@
   6.718  \<close>
   6.719  
   6.720  simproc_setup numeral_divmod
   6.721 -  ("0 div 0 :: 'a :: semiring_numeral_div" | "0 mod 0 :: 'a :: semiring_numeral_div" |
   6.722 -   "0 div 1 :: 'a :: semiring_numeral_div" | "0 mod 1 :: 'a :: semiring_numeral_div" |
   6.723 +  ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
   6.724 +   "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
   6.725     "0 div - 1 :: int" | "0 mod - 1 :: int" |
   6.726 -   "0 div numeral b :: 'a :: semiring_numeral_div" | "0 mod numeral b :: 'a :: semiring_numeral_div" |
   6.727 +   "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
   6.728     "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
   6.729 -   "1 div 0 :: 'a :: semiring_numeral_div" | "1 mod 0 :: 'a :: semiring_numeral_div" |
   6.730 -   "1 div 1 :: 'a :: semiring_numeral_div" | "1 mod 1 :: 'a :: semiring_numeral_div" |
   6.731 +   "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
   6.732 +   "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
   6.733     "1 div - 1 :: int" | "1 mod - 1 :: int" |
   6.734 -   "1 div numeral b :: 'a :: semiring_numeral_div" | "1 mod numeral b :: 'a :: semiring_numeral_div" |
   6.735 +   "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
   6.736     "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
   6.737     "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
   6.738     "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
   6.739     "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
   6.740 -   "numeral a div 0 :: 'a :: semiring_numeral_div" | "numeral a mod 0 :: 'a :: semiring_numeral_div" |
   6.741 -   "numeral a div 1 :: 'a :: semiring_numeral_div" | "numeral a mod 1 :: 'a :: semiring_numeral_div" |
   6.742 +   "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
   6.743 +   "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
   6.744     "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
   6.745 -   "numeral a div numeral b :: 'a :: semiring_numeral_div" | "numeral a mod numeral b :: 'a :: semiring_numeral_div" |
   6.746 +   "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
   6.747     "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
   6.748     "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
   6.749     "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
   6.750 @@ -2818,7 +2343,7 @@
   6.751    code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   6.752  
   6.753  lemma dvd_eq_mod_eq_0_numeral:
   6.754 -  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
   6.755 +  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
   6.756    by (fact dvd_eq_mod_eq_0)
   6.757  
   6.758  declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
     7.1 --- a/src/HOL/Enum.thy	Sun Oct 08 22:28:21 2017 +0200
     7.2 +++ b/src/HOL/Enum.thy	Sun Oct 08 22:28:21 2017 +0200
     7.3 @@ -683,7 +683,7 @@
     7.4  
     7.5  instance finite_2 :: complete_linorder ..
     7.6  
     7.7 -instantiation finite_2 :: "{field, idom_abs_sgn}" begin
     7.8 +instantiation finite_2 :: "{field, idom_abs_sgn, idom_modulo}" begin
     7.9  definition [simp]: "0 = a\<^sub>1"
    7.10  definition [simp]: "1 = a\<^sub>2"
    7.11  definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
    7.12 @@ -692,12 +692,15 @@
    7.13  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    7.14  definition "inverse = (\<lambda>x :: finite_2. x)"
    7.15  definition "divide = (op * :: finite_2 \<Rightarrow> _)"
    7.16 +definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    7.17  definition "abs = (\<lambda>x :: finite_2. x)"
    7.18  definition "sgn = (\<lambda>x :: finite_2. x)"
    7.19  instance
    7.20    by standard
    7.21 -    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    7.22 -      inverse_finite_2_def divide_finite_2_def abs_finite_2_def sgn_finite_2_def
    7.23 +    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def
    7.24 +      times_finite_2_def
    7.25 +      inverse_finite_2_def divide_finite_2_def modulo_finite_2_def
    7.26 +      abs_finite_2_def sgn_finite_2_def
    7.27        split: finite_2.splits)
    7.28  end
    7.29  
    7.30 @@ -709,14 +712,15 @@
    7.31    "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
    7.32    by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
    7.33  
    7.34 -instantiation finite_2 :: "{ring_div, normalization_semidom}" begin
    7.35 +instantiation finite_2 :: unique_euclidean_semiring begin
    7.36  definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
    7.37  definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
    7.38 -definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    7.39 +definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
    7.40 +definition [simp]: "uniqueness_constraint = (\<top> :: finite_2 \<Rightarrow> _)"
    7.41  instance
    7.42    by standard
    7.43 -    (simp_all add: dvd_finite_2_unfold times_finite_2_def
    7.44 -      divide_finite_2_def modulo_finite_2_def split: finite_2.splits)
    7.45 +    (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
    7.46 +    split: finite_2.splits)
    7.47  end
    7.48  
    7.49   
    7.50 @@ -826,7 +830,7 @@
    7.51  
    7.52  instance finite_3 :: complete_linorder ..
    7.53  
    7.54 -instantiation finite_3 :: "{field, idom_abs_sgn}" begin
    7.55 +instantiation finite_3 :: "{field, idom_abs_sgn, idom_modulo}" begin
    7.56  definition [simp]: "0 = a\<^sub>1"
    7.57  definition [simp]: "1 = a\<^sub>2"
    7.58  definition
    7.59 @@ -839,12 +843,15 @@
    7.60  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
    7.61  definition "inverse = (\<lambda>x :: finite_3. x)" 
    7.62  definition "x div y = x * inverse (y :: finite_3)"
    7.63 +definition "x mod y = (case y of a\<^sub>1 \<Rightarrow> x | _ \<Rightarrow> a\<^sub>1)"
    7.64  definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    7.65  definition "sgn = (\<lambda>x :: finite_3. x)"
    7.66  instance
    7.67    by standard
    7.68 -    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    7.69 -      inverse_finite_3_def divide_finite_3_def abs_finite_3_def sgn_finite_3_def
    7.70 +    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def
    7.71 +      times_finite_3_def
    7.72 +      inverse_finite_3_def divide_finite_3_def modulo_finite_3_def
    7.73 +      abs_finite_3_def sgn_finite_3_def
    7.74        less_finite_3_def
    7.75        split: finite_3.splits)
    7.76  end
    7.77 @@ -857,20 +864,21 @@
    7.78    "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
    7.79    by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
    7.80  
    7.81 -instantiation finite_3 :: "{ring_div, normalization_semidom}" begin
    7.82 -definition "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    7.83 +instantiation finite_3 :: unique_euclidean_semiring begin
    7.84 +definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    7.85  definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
    7.86 -definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
    7.87 -instance
    7.88 -  by standard
    7.89 -    (auto simp add: finite_3_not_eq_unfold plus_finite_3_def
    7.90 -      dvd_finite_3_unfold times_finite_3_def inverse_finite_3_def
    7.91 -      normalize_finite_3_def divide_finite_3_def modulo_finite_3_def
    7.92 -      split: finite_3.splits)
    7.93 +definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
    7.94 +definition [simp]: "uniqueness_constraint = (\<top> :: finite_3 \<Rightarrow> _)"
    7.95 +instance proof
    7.96 +  fix x :: finite_3
    7.97 +  assume "x \<noteq> 0"
    7.98 +  then show "is_unit (unit_factor x)"
    7.99 +    by (cases x) (simp_all add: dvd_finite_3_unfold)
   7.100 +qed (auto simp add: divide_finite_3_def times_finite_3_def
   7.101 +  dvd_finite_3_unfold inverse_finite_3_def plus_finite_3_def
   7.102 +  split: finite_3.splits)
   7.103  end
   7.104  
   7.105 -
   7.106 -
   7.107  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
   7.108  
   7.109  datatype (plugins only: code "quickcheck" extraction) finite_4 =
     8.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     8.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
     8.3 @@ -201,6 +201,388 @@
     8.4  class euclidean_ring = idom_modulo + euclidean_semiring
     8.5  
     8.6    
     8.7 +subsection \<open>Euclidean (semi)rings with cancel rules\<close>
     8.8 +
     8.9 +class euclidean_semiring_cancel = euclidean_semiring +
    8.10 +  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    8.11 +  and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
    8.12 +begin
    8.13 +
    8.14 +lemma div_mult_self2 [simp]:
    8.15 +  assumes "b \<noteq> 0"
    8.16 +  shows "(a + b * c) div b = c + a div b"
    8.17 +  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
    8.18 +
    8.19 +lemma div_mult_self3 [simp]:
    8.20 +  assumes "b \<noteq> 0"
    8.21 +  shows "(c * b + a) div b = c + a div b"
    8.22 +  using assms by (simp add: add.commute)
    8.23 +
    8.24 +lemma div_mult_self4 [simp]:
    8.25 +  assumes "b \<noteq> 0"
    8.26 +  shows "(b * c + a) div b = c + a div b"
    8.27 +  using assms by (simp add: add.commute)
    8.28 +
    8.29 +lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
    8.30 +proof (cases "b = 0")
    8.31 +  case True then show ?thesis by simp
    8.32 +next
    8.33 +  case False
    8.34 +  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
    8.35 +    by (simp add: div_mult_mod_eq)
    8.36 +  also from False div_mult_self1 [of b a c] have
    8.37 +    "\<dots> = (c + a div b) * b + (a + c * b) mod b"
    8.38 +      by (simp add: algebra_simps)
    8.39 +  finally have "a = a div b * b + (a + c * b) mod b"
    8.40 +    by (simp add: add.commute [of a] add.assoc distrib_right)
    8.41 +  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
    8.42 +    by (simp add: div_mult_mod_eq)
    8.43 +  then show ?thesis by simp
    8.44 +qed
    8.45 +
    8.46 +lemma mod_mult_self2 [simp]:
    8.47 +  "(a + b * c) mod b = a mod b"
    8.48 +  by (simp add: mult.commute [of b])
    8.49 +
    8.50 +lemma mod_mult_self3 [simp]:
    8.51 +  "(c * b + a) mod b = a mod b"
    8.52 +  by (simp add: add.commute)
    8.53 +
    8.54 +lemma mod_mult_self4 [simp]:
    8.55 +  "(b * c + a) mod b = a mod b"
    8.56 +  by (simp add: add.commute)
    8.57 +
    8.58 +lemma mod_mult_self1_is_0 [simp]:
    8.59 +  "b * a mod b = 0"
    8.60 +  using mod_mult_self2 [of 0 b a] by simp
    8.61 +
    8.62 +lemma mod_mult_self2_is_0 [simp]:
    8.63 +  "a * b mod b = 0"
    8.64 +  using mod_mult_self1 [of 0 a b] by simp
    8.65 +
    8.66 +lemma div_add_self1:
    8.67 +  assumes "b \<noteq> 0"
    8.68 +  shows "(b + a) div b = a div b + 1"
    8.69 +  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
    8.70 +
    8.71 +lemma div_add_self2:
    8.72 +  assumes "b \<noteq> 0"
    8.73 +  shows "(a + b) div b = a div b + 1"
    8.74 +  using assms div_add_self1 [of b a] by (simp add: add.commute)
    8.75 +
    8.76 +lemma mod_add_self1 [simp]:
    8.77 +  "(b + a) mod b = a mod b"
    8.78 +  using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
    8.79 +
    8.80 +lemma mod_add_self2 [simp]:
    8.81 +  "(a + b) mod b = a mod b"
    8.82 +  using mod_mult_self1 [of a 1 b] by simp
    8.83 +
    8.84 +lemma mod_div_trivial [simp]:
    8.85 +  "a mod b div b = 0"
    8.86 +proof (cases "b = 0")
    8.87 +  assume "b = 0"
    8.88 +  thus ?thesis by simp
    8.89 +next
    8.90 +  assume "b \<noteq> 0"
    8.91 +  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
    8.92 +    by (rule div_mult_self1 [symmetric])
    8.93 +  also have "\<dots> = a div b"
    8.94 +    by (simp only: mod_div_mult_eq)
    8.95 +  also have "\<dots> = a div b + 0"
    8.96 +    by simp
    8.97 +  finally show ?thesis
    8.98 +    by (rule add_left_imp_eq)
    8.99 +qed
   8.100 +
   8.101 +lemma mod_mod_trivial [simp]:
   8.102 +  "a mod b mod b = a mod b"
   8.103 +proof -
   8.104 +  have "a mod b mod b = (a mod b + a div b * b) mod b"
   8.105 +    by (simp only: mod_mult_self1)
   8.106 +  also have "\<dots> = a mod b"
   8.107 +    by (simp only: mod_div_mult_eq)
   8.108 +  finally show ?thesis .
   8.109 +qed
   8.110 +
   8.111 +lemma mod_mod_cancel:
   8.112 +  assumes "c dvd b"
   8.113 +  shows "a mod b mod c = a mod c"
   8.114 +proof -
   8.115 +  from \<open>c dvd b\<close> obtain k where "b = c * k"
   8.116 +    by (rule dvdE)
   8.117 +  have "a mod b mod c = a mod (c * k) mod c"
   8.118 +    by (simp only: \<open>b = c * k\<close>)
   8.119 +  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
   8.120 +    by (simp only: mod_mult_self1)
   8.121 +  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
   8.122 +    by (simp only: ac_simps)
   8.123 +  also have "\<dots> = a mod c"
   8.124 +    by (simp only: div_mult_mod_eq)
   8.125 +  finally show ?thesis .
   8.126 +qed
   8.127 +
   8.128 +lemma div_mult_mult2 [simp]:
   8.129 +  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   8.130 +  by (drule div_mult_mult1) (simp add: mult.commute)
   8.131 +
   8.132 +lemma div_mult_mult1_if [simp]:
   8.133 +  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
   8.134 +  by simp_all
   8.135 +
   8.136 +lemma mod_mult_mult1:
   8.137 +  "(c * a) mod (c * b) = c * (a mod b)"
   8.138 +proof (cases "c = 0")
   8.139 +  case True then show ?thesis by simp
   8.140 +next
   8.141 +  case False
   8.142 +  from div_mult_mod_eq
   8.143 +  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   8.144 +  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
   8.145 +    = c * a + c * (a mod b)" by (simp add: algebra_simps)
   8.146 +  with div_mult_mod_eq show ?thesis by simp
   8.147 +qed
   8.148 +
   8.149 +lemma mod_mult_mult2:
   8.150 +  "(a * c) mod (b * c) = (a mod b) * c"
   8.151 +  using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
   8.152 +
   8.153 +lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
   8.154 +  by (fact mod_mult_mult2 [symmetric])
   8.155 +
   8.156 +lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   8.157 +  by (fact mod_mult_mult1 [symmetric])
   8.158 +
   8.159 +lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   8.160 +  unfolding dvd_def by (auto simp add: mod_mult_mult1)
   8.161 +
   8.162 +lemma div_plus_div_distrib_dvd_left:
   8.163 +  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
   8.164 +  by (cases "c = 0") (auto elim: dvdE)
   8.165 +
   8.166 +lemma div_plus_div_distrib_dvd_right:
   8.167 +  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
   8.168 +  using div_plus_div_distrib_dvd_left [of c b a]
   8.169 +  by (simp add: ac_simps)
   8.170 +
   8.171 +named_theorems mod_simps
   8.172 +
   8.173 +text \<open>Addition respects modular equivalence.\<close>
   8.174 +
   8.175 +lemma mod_add_left_eq [mod_simps]:
   8.176 +  "(a mod c + b) mod c = (a + b) mod c"
   8.177 +proof -
   8.178 +  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   8.179 +    by (simp only: div_mult_mod_eq)
   8.180 +  also have "\<dots> = (a mod c + b + a div c * c) mod c"
   8.181 +    by (simp only: ac_simps)
   8.182 +  also have "\<dots> = (a mod c + b) mod c"
   8.183 +    by (rule mod_mult_self1)
   8.184 +  finally show ?thesis
   8.185 +    by (rule sym)
   8.186 +qed
   8.187 +
   8.188 +lemma mod_add_right_eq [mod_simps]:
   8.189 +  "(a + b mod c) mod c = (a + b) mod c"
   8.190 +  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
   8.191 +
   8.192 +lemma mod_add_eq:
   8.193 +  "(a mod c + b mod c) mod c = (a + b) mod c"
   8.194 +  by (simp add: mod_add_left_eq mod_add_right_eq)
   8.195 +
   8.196 +lemma mod_sum_eq [mod_simps]:
   8.197 +  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
   8.198 +proof (induct A rule: infinite_finite_induct)
   8.199 +  case (insert i A)
   8.200 +  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
   8.201 +    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
   8.202 +    by simp
   8.203 +  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
   8.204 +    by (simp add: mod_simps)
   8.205 +  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
   8.206 +    by (simp add: insert.hyps)
   8.207 +  finally show ?case
   8.208 +    by (simp add: insert.hyps mod_simps)
   8.209 +qed simp_all
   8.210 +
   8.211 +lemma mod_add_cong:
   8.212 +  assumes "a mod c = a' mod c"
   8.213 +  assumes "b mod c = b' mod c"
   8.214 +  shows "(a + b) mod c = (a' + b') mod c"
   8.215 +proof -
   8.216 +  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
   8.217 +    unfolding assms ..
   8.218 +  then show ?thesis
   8.219 +    by (simp add: mod_add_eq)
   8.220 +qed
   8.221 +
   8.222 +text \<open>Multiplication respects modular equivalence.\<close>
   8.223 +
   8.224 +lemma mod_mult_left_eq [mod_simps]:
   8.225 +  "((a mod c) * b) mod c = (a * b) mod c"
   8.226 +proof -
   8.227 +  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   8.228 +    by (simp only: div_mult_mod_eq)
   8.229 +  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
   8.230 +    by (simp only: algebra_simps)
   8.231 +  also have "\<dots> = (a mod c * b) mod c"
   8.232 +    by (rule mod_mult_self1)
   8.233 +  finally show ?thesis
   8.234 +    by (rule sym)
   8.235 +qed
   8.236 +
   8.237 +lemma mod_mult_right_eq [mod_simps]:
   8.238 +  "(a * (b mod c)) mod c = (a * b) mod c"
   8.239 +  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
   8.240 +
   8.241 +lemma mod_mult_eq:
   8.242 +  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
   8.243 +  by (simp add: mod_mult_left_eq mod_mult_right_eq)
   8.244 +
   8.245 +lemma mod_prod_eq [mod_simps]:
   8.246 +  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
   8.247 +proof (induct A rule: infinite_finite_induct)
   8.248 +  case (insert i A)
   8.249 +  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
   8.250 +    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
   8.251 +    by simp
   8.252 +  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
   8.253 +    by (simp add: mod_simps)
   8.254 +  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
   8.255 +    by (simp add: insert.hyps)
   8.256 +  finally show ?case
   8.257 +    by (simp add: insert.hyps mod_simps)
   8.258 +qed simp_all
   8.259 +
   8.260 +lemma mod_mult_cong:
   8.261 +  assumes "a mod c = a' mod c"
   8.262 +  assumes "b mod c = b' mod c"
   8.263 +  shows "(a * b) mod c = (a' * b') mod c"
   8.264 +proof -
   8.265 +  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   8.266 +    unfolding assms ..
   8.267 +  then show ?thesis
   8.268 +    by (simp add: mod_mult_eq)
   8.269 +qed
   8.270 +
   8.271 +text \<open>Exponentiation respects modular equivalence.\<close>
   8.272 +
   8.273 +lemma power_mod [mod_simps]: 
   8.274 +  "((a mod b) ^ n) mod b = (a ^ n) mod b"
   8.275 +proof (induct n)
   8.276 +  case 0
   8.277 +  then show ?case by simp
   8.278 +next
   8.279 +  case (Suc n)
   8.280 +  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
   8.281 +    by (simp add: mod_mult_right_eq)
   8.282 +  with Suc show ?case
   8.283 +    by (simp add: mod_mult_left_eq mod_mult_right_eq)
   8.284 +qed
   8.285 +
   8.286 +end
   8.287 +
   8.288 +
   8.289 +class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel
   8.290 +begin
   8.291 +
   8.292 +subclass idom_divide ..
   8.293 +
   8.294 +lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
   8.295 +  using div_mult_mult1 [of "- 1" a b] by simp
   8.296 +
   8.297 +lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   8.298 +  using mod_mult_mult1 [of "- 1" a b] by simp
   8.299 +
   8.300 +lemma div_minus_right: "a div (- b) = (- a) div b"
   8.301 +  using div_minus_minus [of "- a" b] by simp
   8.302 +
   8.303 +lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   8.304 +  using mod_minus_minus [of "- a" b] by simp
   8.305 +
   8.306 +lemma div_minus1_right [simp]: "a div (- 1) = - a"
   8.307 +  using div_minus_right [of a 1] by simp
   8.308 +
   8.309 +lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   8.310 +  using mod_minus_right [of a 1] by simp
   8.311 +
   8.312 +text \<open>Negation respects modular equivalence.\<close>
   8.313 +
   8.314 +lemma mod_minus_eq [mod_simps]:
   8.315 +  "(- (a mod b)) mod b = (- a) mod b"
   8.316 +proof -
   8.317 +  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   8.318 +    by (simp only: div_mult_mod_eq)
   8.319 +  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
   8.320 +    by (simp add: ac_simps)
   8.321 +  also have "\<dots> = (- (a mod b)) mod b"
   8.322 +    by (rule mod_mult_self1)
   8.323 +  finally show ?thesis
   8.324 +    by (rule sym)
   8.325 +qed
   8.326 +
   8.327 +lemma mod_minus_cong:
   8.328 +  assumes "a mod b = a' mod b"
   8.329 +  shows "(- a) mod b = (- a') mod b"
   8.330 +proof -
   8.331 +  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
   8.332 +    unfolding assms ..
   8.333 +  then show ?thesis
   8.334 +    by (simp add: mod_minus_eq)
   8.335 +qed
   8.336 +
   8.337 +text \<open>Subtraction respects modular equivalence.\<close>
   8.338 +
   8.339 +lemma mod_diff_left_eq [mod_simps]:
   8.340 +  "(a mod c - b) mod c = (a - b) mod c"
   8.341 +  using mod_add_cong [of a c "a mod c" "- b" "- b"]
   8.342 +  by simp
   8.343 +
   8.344 +lemma mod_diff_right_eq [mod_simps]:
   8.345 +  "(a - b mod c) mod c = (a - b) mod c"
   8.346 +  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   8.347 +  by simp
   8.348 +
   8.349 +lemma mod_diff_eq:
   8.350 +  "(a mod c - b mod c) mod c = (a - b) mod c"
   8.351 +  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   8.352 +  by simp
   8.353 +
   8.354 +lemma mod_diff_cong:
   8.355 +  assumes "a mod c = a' mod c"
   8.356 +  assumes "b mod c = b' mod c"
   8.357 +  shows "(a - b) mod c = (a' - b') mod c"
   8.358 +  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
   8.359 +  by simp
   8.360 +
   8.361 +lemma minus_mod_self2 [simp]:
   8.362 +  "(a - b) mod b = a mod b"
   8.363 +  using mod_diff_right_eq [of a b b]
   8.364 +  by (simp add: mod_diff_right_eq)
   8.365 +
   8.366 +lemma minus_mod_self1 [simp]:
   8.367 +  "(b - a) mod b = - a mod b"
   8.368 +  using mod_add_self2 [of "- a" b] by simp
   8.369 +
   8.370 +lemma mod_eq_dvd_iff:
   8.371 +  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
   8.372 +proof
   8.373 +  assume ?P
   8.374 +  then have "(a mod c - b mod c) mod c = 0"
   8.375 +    by simp
   8.376 +  then show ?Q
   8.377 +    by (simp add: dvd_eq_mod_eq_0 mod_simps)
   8.378 +next
   8.379 +  assume ?Q
   8.380 +  then obtain d where d: "a - b = c * d" ..
   8.381 +  then have "a = c * d + b"
   8.382 +    by (simp add: algebra_simps)
   8.383 +  then show ?P by simp
   8.384 +qed
   8.385 +
   8.386 +end
   8.387 +
   8.388 +  
   8.389  subsection \<open>Uniquely determined division\<close>
   8.390    
   8.391  class unique_euclidean_semiring = euclidean_semiring + 
   8.392 @@ -284,8 +666,53 @@
   8.393      by simp
   8.394  qed
   8.395  
   8.396 +subclass euclidean_semiring_cancel
   8.397 +proof
   8.398 +  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   8.399 +  proof (cases a b rule: divmod_cases)
   8.400 +    case by0
   8.401 +    with \<open>b \<noteq> 0\<close> show ?thesis
   8.402 +      by simp
   8.403 +  next
   8.404 +    case (divides q)
   8.405 +    then show ?thesis
   8.406 +      by (simp add: ac_simps)
   8.407 +  next
   8.408 +    case (remainder q r)
   8.409 +    then show ?thesis
   8.410 +      by (auto intro: div_eqI simp add: algebra_simps)
   8.411 +  qed
   8.412 +next
   8.413 +  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   8.414 +  proof (cases a b rule: divmod_cases)
   8.415 +    case by0
   8.416 +    then show ?thesis
   8.417 +      by simp
   8.418 +  next
   8.419 +    case (divides q)
   8.420 +    with \<open>c \<noteq> 0\<close> show ?thesis
   8.421 +      by (simp add: mult.left_commute [of c])
   8.422 +  next
   8.423 +    case (remainder q r)
   8.424 +    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   8.425 +      by simp
   8.426 +    from remainder \<open>c \<noteq> 0\<close>
   8.427 +    have "uniqueness_constraint (r * c) (b * c)"
   8.428 +      and "euclidean_size (r * c) < euclidean_size (b * c)"
   8.429 +      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   8.430 +    with remainder show ?thesis
   8.431 +      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   8.432 +        (use \<open>b * c \<noteq> 0\<close> in simp)
   8.433 +  qed
   8.434 +qed
   8.435 +
   8.436  end
   8.437  
   8.438  class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
   8.439 +begin
   8.440 +  
   8.441 +subclass euclidean_ring_cancel ..
   8.442  
   8.443  end
   8.444 +
   8.445 +end
     9.1 --- a/src/HOL/Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     9.2 +++ b/src/HOL/Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     9.3 @@ -130,11 +130,11 @@
     9.4  lemma fact_ge_self: "fact n \<ge> n"
     9.5    by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
     9.6  
     9.7 -lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::{semiring_div,linordered_semidom})"
     9.8 +lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::linordered_semidom)"
     9.9    by (induct m) (auto simp: le_Suc_eq)
    9.10  
    9.11 -lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semiring_div,linordered_semidom}) = 0"
    9.12 -  by (auto simp add: fact_dvd)
    9.13 +lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semidom_modulo, linordered_semidom}) = 0"
    9.14 +  by (simp add: mod_eq_0_iff_dvd fact_dvd)
    9.15  
    9.16  lemma fact_div_fact:
    9.17    assumes "m \<ge> n"
    10.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:21 2017 +0200
    10.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Oct 08 22:28:21 2017 +0200
    10.3 @@ -772,9 +772,6 @@
    10.4  instance star :: (semidom_divide) semidom_divide
    10.5    by (intro_classes; transfer) simp_all
    10.6  
    10.7 -instance star :: (semiring_div) semiring_div
    10.8 -  by (intro_classes; transfer) (simp_all add: div_mult_mod_eq)
    10.9 -
   10.10  instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
   10.11  instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
   10.12  instance star :: (idom) idom ..
   10.13 @@ -821,6 +818,22 @@
   10.14  
   10.15  instance star :: (linordered_field) linordered_field ..
   10.16  
   10.17 +instance star :: (algebraic_semidom) algebraic_semidom ..
   10.18 +
   10.19 +instantiation star :: (normalization_semidom) normalization_semidom
   10.20 +begin
   10.21 +
   10.22 +definition unit_factor_star :: "'a star \<Rightarrow> 'a star"
   10.23 +  where [transfer_unfold]: "unit_factor_star = *f* unit_factor"
   10.24 +
   10.25 +definition normalize_star :: "'a star \<Rightarrow> 'a star"
   10.26 +  where [transfer_unfold]: "normalize_star = *f* normalize"
   10.27 +
   10.28 +instance
   10.29 +  by standard (transfer; simp add: is_unit_unit_factor unit_factor_mult)+
   10.30 +
   10.31 +end
   10.32 +
   10.33  
   10.34  subsection \<open>Power\<close>
   10.35  
   10.36 @@ -912,49 +925,6 @@
   10.37    apply (transfer, erule odd_ex_decrement)
   10.38    done
   10.39  
   10.40 -instance star :: (semiring_div_parity) semiring_div_parity
   10.41 -  apply intro_classes
   10.42 -    apply (transfer, rule parity)
   10.43 -   apply (transfer, rule one_mod_two_eq_one)
   10.44 -  apply (transfer, rule zero_not_eq_two)
   10.45 -  done
   10.46 -
   10.47 -instantiation star :: (semiring_numeral_div) semiring_numeral_div
   10.48 -begin
   10.49 -
   10.50 -definition divmod_star :: "num \<Rightarrow> num \<Rightarrow> 'a star \<times> 'a star"
   10.51 -  where divmod_star_def: "divmod_star m n = (numeral m div numeral n, numeral m mod numeral n)"
   10.52 -
   10.53 -definition divmod_step_star :: "num \<Rightarrow> 'a star \<times> 'a star \<Rightarrow> 'a star \<times> 'a star"
   10.54 -  where "divmod_step_star l qr =
   10.55 -    (let (q, r) = qr
   10.56 -     in if r \<ge> numeral l then (2 * q + 1, r - numeral l) else (2 * q, r))"
   10.57 -
   10.58 -instance
   10.59 -proof
   10.60 -  show "divmod m n = (numeral m div numeral n :: 'a star, numeral m mod numeral n)" for m n
   10.61 -    by (fact divmod_star_def)
   10.62 -  show "divmod_step l qr =
   10.63 -    (let (q, r) = qr
   10.64 -     in if r \<ge> numeral l then (2 * q + 1, r - numeral l) else (2 * q, r))"
   10.65 -    for l and qr :: "'a star \<times> 'a star"
   10.66 -    by (fact divmod_step_star_def)
   10.67 -qed (transfer,
   10.68 -  fact
   10.69 -  semiring_numeral_div_class.div_less
   10.70 -  semiring_numeral_div_class.mod_less
   10.71 -  semiring_numeral_div_class.div_positive
   10.72 -  semiring_numeral_div_class.mod_less_eq_dividend
   10.73 -  semiring_numeral_div_class.pos_mod_bound
   10.74 -  semiring_numeral_div_class.pos_mod_sign
   10.75 -  semiring_numeral_div_class.mod_mult2_eq
   10.76 -  semiring_numeral_div_class.div_mult2_eq
   10.77 -  semiring_numeral_div_class.discrete)+
   10.78 -
   10.79 -end
   10.80 -
   10.81 -declare divmod_algorithm_code [where ?'a = "'a::semiring_numeral_div star", code]
   10.82 -
   10.83  
   10.84  subsection \<open>Finite class\<close>
   10.85  
    11.1 --- a/src/HOL/Numeral_Simprocs.thy	Sun Oct 08 22:28:21 2017 +0200
    11.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sun Oct 08 22:28:21 2017 +0200
    11.3 @@ -169,8 +169,8 @@
    11.4  
    11.5  (* TODO: remove comm_ring_1 constraint if possible *)
    11.6  simproc_setup int_div_cancel_numeral_factors
    11.7 -  ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n"
    11.8 -  |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") =
    11.9 +  ("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n"
   11.10 +  |"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") =
   11.11    \<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>
   11.12  
   11.13  simproc_setup divide_cancel_numeral_factor
   11.14 @@ -194,13 +194,13 @@
   11.15    \<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>
   11.16  
   11.17  simproc_setup int_div_cancel_factor
   11.18 -  ("((l::'a::semiring_div) * m) div n"
   11.19 -  |"(l::'a::semiring_div) div (m * n)") =
   11.20 +  ("((l::'a::euclidean_semiring_cancel) * m) div n"
   11.21 +  |"(l::'a::euclidean_semiring_cancel) div (m * n)") =
   11.22    \<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>
   11.23  
   11.24  simproc_setup int_mod_cancel_factor
   11.25 -  ("((l::'a::semiring_div) * m) mod n"
   11.26 -  |"(l::'a::semiring_div) mod (m * n)") =
   11.27 +  ("((l::'a::euclidean_semiring_cancel) * m) mod n"
   11.28 +  |"(l::'a::euclidean_semiring_cancel) mod (m * n)") =
   11.29    \<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>
   11.30  
   11.31  simproc_setup dvd_cancel_factor
    12.1 --- a/src/HOL/Rat.thy	Sun Oct 08 22:28:21 2017 +0200
    12.2 +++ b/src/HOL/Rat.thy	Sun Oct 08 22:28:21 2017 +0200
    12.3 @@ -199,12 +199,12 @@
    12.4  
    12.5  (* We cannot state these two rules earlier because of pending sort hypotheses *)
    12.6  lemma div_add_self1_no_field [simp]:
    12.7 -  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: semiring_div) \<noteq> 0"
    12.8 +  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: euclidean_semiring_cancel) \<noteq> 0"
    12.9    shows "(b + a) div b = a div b + 1"
   12.10    using assms(2) by (fact div_add_self1)
   12.11  
   12.12  lemma div_add_self2_no_field [simp]:
   12.13 -  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: semiring_div) \<noteq> 0"
   12.14 +  assumes "NO_MATCH (x :: 'b :: field) b" "(b :: 'a :: euclidean_semiring_cancel) \<noteq> 0"
   12.15    shows "(a + b) div b = a div b + 1"
   12.16    using assms(2) by (fact div_add_self2)
   12.17  
    13.1 --- a/src/HOL/ex/Simproc_Tests.thy	Sun Oct 08 22:28:21 2017 +0200
    13.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Sun Oct 08 22:28:21 2017 +0200
    13.3 @@ -199,7 +199,7 @@
    13.4  subsection \<open>\<open>int_div_cancel_numeral_factors\<close>\<close>
    13.5  
    13.6  notepad begin
    13.7 -  fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}"
    13.8 +  fix x y z :: "'a::{unique_euclidean_semiring,comm_ring_1,ring_char_0}"
    13.9    {
   13.10      assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
   13.11        by (tactic \<open>test @{context} [@{simproc int_div_cancel_numeral_factors}]\<close>) fact
   13.12 @@ -325,7 +325,7 @@
   13.13  subsection \<open>\<open>int_div_cancel_factor\<close>\<close>
   13.14  
   13.15  notepad begin
   13.16 -  fix a b c d k uu x y :: "'a::semiring_div"
   13.17 +  fix a b c d k uu x y :: "'a::unique_euclidean_semiring"
   13.18    {
   13.19      assume "(if k = 0 then 0 else x div y) = uu"
   13.20      have "(x*k) div (k*y) = uu"
    14.1 --- a/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:21 2017 +0200
    14.2 +++ b/src/HOL/ex/Word_Type.thy	Sun Oct 08 22:28:21 2017 +0200
    14.3 @@ -11,7 +11,7 @@
    14.4  
    14.5  subsection \<open>Truncating bit representations of numeric types\<close>
    14.6  
    14.7 -class semiring_bits = semiring_div_parity +
    14.8 +class semiring_bits = unique_euclidean_semiring_parity +
    14.9    assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
   14.10  begin
   14.11