more uniform div/mod relations
authorhaftmann
Thu Dec 22 10:42:08 2016 +0100 (2016-12-22)
changeset 64635255741c5f862
parent 64634 5bd30359e46e
child 64636 a42dbe9d2c1f
more uniform div/mod relations
src/HOL/Divides.thy
src/HOL/Library/Polynomial.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Dec 22 08:43:30 2016 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Dec 22 10:42:08 2016 +0100
     1.3 @@ -828,18 +828,18 @@
     1.4    @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
     1.5  \<close>
     1.6  
     1.7 -definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
     1.8 -  "divmod_nat_rel m n qr \<longleftrightarrow>
     1.9 -    m = fst qr * n + snd qr \<and>
    1.10 -      (if n = 0 then fst qr = 0 else if n > 0 then 0 \<le> snd qr \<and> snd qr < n else n < snd qr \<and> snd qr \<le> 0)"
    1.11 -
    1.12 -text \<open>@{const divmod_nat_rel} is total:\<close>
    1.13 -
    1.14 -qualified lemma divmod_nat_rel_ex:
    1.15 -  obtains q r where "divmod_nat_rel m n (q, r)"
    1.16 +inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
    1.17 +  where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
    1.18 +  | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
    1.19 +
    1.20 +text \<open>@{const eucl_rel_nat} is total:\<close>
    1.21 +
    1.22 +qualified lemma eucl_rel_nat_ex:
    1.23 +  obtains q r where "eucl_rel_nat m n (q, r)"
    1.24  proof (cases "n = 0")
    1.25 -  case True  with that show thesis
    1.26 -    by (auto simp add: divmod_nat_rel_def)
    1.27 +  case True
    1.28 +  with that eucl_rel_nat_by0 show thesis
    1.29 +    by blast
    1.30  next
    1.31    case False
    1.32    have "\<exists>q r. m = q * n + r \<and> r < n"
    1.33 @@ -864,74 +864,92 @@
    1.34        with \<open>n \<noteq> 0\<close> show ?thesis by blast
    1.35      qed
    1.36    qed
    1.37 -  with that show thesis
    1.38 -    using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def)
    1.39 +  with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
    1.40 +    by blast
    1.41  qed
    1.42  
    1.43 -text \<open>@{const divmod_nat_rel} is injective:\<close>
    1.44 -
    1.45 -qualified lemma divmod_nat_rel_unique:
    1.46 -  assumes "divmod_nat_rel m n qr"
    1.47 -    and "divmod_nat_rel m n qr'"
    1.48 -  shows "qr = qr'"
    1.49 +text \<open>@{const eucl_rel_nat} is injective:\<close>
    1.50 +
    1.51 +qualified lemma eucl_rel_nat_unique_div:
    1.52 +  assumes "eucl_rel_nat m n (q, r)"
    1.53 +    and "eucl_rel_nat m n (q', r')"
    1.54 +  shows "q = q'"
    1.55  proof (cases "n = 0")
    1.56    case True with assms show ?thesis
    1.57 -    by (cases qr, cases qr')
    1.58 -      (simp add: divmod_nat_rel_def)
    1.59 +    by (auto elim: eucl_rel_nat.cases)
    1.60  next
    1.61    case False
    1.62 -  have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
    1.63 -  apply (rule leI)
    1.64 -  apply (subst less_iff_Suc_add)
    1.65 -  apply (auto simp add: add_mult_distrib)
    1.66 -  done
    1.67 -  from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
    1.68 -    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
    1.69 -  with assms have "snd qr = snd qr'"
    1.70 -    by (simp add: divmod_nat_rel_def)
    1.71 -  with * show ?thesis by (cases qr, cases qr') simp
    1.72 +  have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
    1.73 +  proof (rule ccontr)
    1.74 +    assume "\<not> q' \<le> q"
    1.75 +    then have "q < q'"
    1.76 +      by (simp add: not_le)
    1.77 +    with that show False
    1.78 +      by (auto simp add: less_iff_Suc_add algebra_simps)
    1.79 +  qed
    1.80 +  from \<open>n \<noteq> 0\<close> assms show ?thesis
    1.81 +    by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
    1.82 +qed
    1.83 +
    1.84 +qualified lemma eucl_rel_nat_unique_mod:
    1.85 +  assumes "eucl_rel_nat m n (q, r)"
    1.86 +    and "eucl_rel_nat m n (q', r')"
    1.87 +  shows "r = r'"
    1.88 +proof -
    1.89 +  from assms have "q' = q"
    1.90 +    by (auto intro: eucl_rel_nat_unique_div)
    1.91 +  with assms show ?thesis
    1.92 +    by (auto elim!: eucl_rel_nat.cases)
    1.93  qed
    1.94  
    1.95  text \<open>
    1.96    We instantiate divisibility on the natural numbers by
    1.97 -  means of @{const divmod_nat_rel}:
    1.98 +  means of @{const eucl_rel_nat}:
    1.99  \<close>
   1.100  
   1.101  qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
   1.102 -  "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
   1.103 -
   1.104 -qualified lemma divmod_nat_rel_divmod_nat:
   1.105 -  "divmod_nat_rel m n (divmod_nat m n)"
   1.106 +  "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
   1.107 +
   1.108 +qualified lemma eucl_rel_nat_divmod_nat:
   1.109 +  "eucl_rel_nat m n (divmod_nat m n)"
   1.110  proof -
   1.111 -  from divmod_nat_rel_ex
   1.112 -    obtain qr where rel: "divmod_nat_rel m n qr" .
   1.113 +  from eucl_rel_nat_ex
   1.114 +    obtain q r where rel: "eucl_rel_nat m n (q, r)" .
   1.115    then show ?thesis
   1.116 -  by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
   1.117 +    by (auto simp add: divmod_nat_def intro: theI
   1.118 +      elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   1.119  qed
   1.120  
   1.121  qualified lemma divmod_nat_unique:
   1.122 -  assumes "divmod_nat_rel m n qr"
   1.123 -  shows "divmod_nat m n = qr"
   1.124 -  using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
   1.125 -
   1.126 -qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
   1.127 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.128 -
   1.129 -qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
   1.130 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.131 -
   1.132 -qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   1.133 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.134 +  "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
   1.135 +  using that
   1.136 +  by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
   1.137 +
   1.138 +qualified lemma divmod_nat_zero:
   1.139 +  "divmod_nat m 0 = (0, m)"
   1.140 +  by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
   1.141 +
   1.142 +qualified lemma divmod_nat_zero_left:
   1.143 +  "divmod_nat 0 n = (0, 0)"
   1.144 +  by (rule divmod_nat_unique) 
   1.145 +    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.146 +
   1.147 +qualified lemma divmod_nat_base:
   1.148 +  "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   1.149 +  by (rule divmod_nat_unique) 
   1.150 +    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.151  
   1.152  qualified lemma divmod_nat_step:
   1.153    assumes "0 < n" and "n \<le> m"
   1.154 -  shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
   1.155 +  shows "divmod_nat m n =
   1.156 +    (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   1.157  proof (rule divmod_nat_unique)
   1.158 -  have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
   1.159 -    by (fact divmod_nat_rel_divmod_nat)
   1.160 -  then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
   1.161 -    unfolding divmod_nat_rel_def using assms
   1.162 -      by (auto split: if_splits simp add: algebra_simps)
   1.163 +  have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
   1.164 +    by (fact eucl_rel_nat_divmod_nat)
   1.165 +  then show "eucl_rel_nat m n (Suc
   1.166 +    (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
   1.167 +    using assms
   1.168 +      by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
   1.169  qed
   1.170  
   1.171  end
   1.172 @@ -969,19 +987,19 @@
   1.173    by (simp add: prod_eq_iff)
   1.174  
   1.175  lemma div_nat_unique:
   1.176 -  assumes "divmod_nat_rel m n (q, r)"
   1.177 +  assumes "eucl_rel_nat m n (q, r)"
   1.178    shows "m div n = q"
   1.179    using assms
   1.180    by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   1.181  
   1.182  lemma mod_nat_unique:
   1.183 -  assumes "divmod_nat_rel m n (q, r)"
   1.184 +  assumes "eucl_rel_nat m n (q, r)"
   1.185    shows "m mod n = r"
   1.186    using assms
   1.187    by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   1.188  
   1.189 -lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   1.190 -  using Divides.divmod_nat_rel_divmod_nat
   1.191 +lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
   1.192 +  using Divides.eucl_rel_nat_divmod_nat
   1.193    by (simp add: divmod_nat_div_mod)
   1.194  
   1.195  text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
   1.196 @@ -1014,22 +1032,21 @@
   1.197    fixes m n :: nat
   1.198    assumes "n > 0"
   1.199    shows "m mod n < n"
   1.200 -  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
   1.201 -  by (auto split: if_splits)
   1.202 +  using assms eucl_rel_nat [of m n]
   1.203 +    by (auto elim: eucl_rel_nat.cases)
   1.204  
   1.205  lemma mod_le_divisor [simp]:
   1.206    fixes m n :: nat
   1.207    assumes "n > 0"
   1.208    shows "m mod n \<le> n"
   1.209 -proof (rule less_imp_le)
   1.210 -  from assms show "m mod n < n"
   1.211 -    by simp
   1.212 -qed
   1.213 +  using assms eucl_rel_nat [of m n]
   1.214 +    by (auto elim: eucl_rel_nat.cases)
   1.215  
   1.216  instance proof
   1.217    fix m n :: nat
   1.218    show "m div n * n + m mod n = m"
   1.219 -    using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
   1.220 +    using eucl_rel_nat [of m n]
   1.221 +    by (auto elim: eucl_rel_nat.cases)
   1.222  next
   1.223    fix n :: nat show "n div 0 = 0"
   1.224      by (simp add: div_nat_def Divides.divmod_nat_zero)
   1.225 @@ -1037,7 +1054,7 @@
   1.226    fix m n :: nat
   1.227    assume "n \<noteq> 0"
   1.228    then show "m * n div n = m"
   1.229 -    by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
   1.230 +    by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
   1.231  qed (simp_all add: unit_factor_nat_def)
   1.232  
   1.233  end
   1.234 @@ -1051,11 +1068,20 @@
   1.235  next
   1.236    fix m n q :: nat
   1.237    assume "m \<noteq> 0"
   1.238 -  then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
   1.239 -    using div_mult_mod_eq [of n q]
   1.240 -    by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
   1.241 -  then show "(m * n) div (m * q) = n div q"
   1.242 -    by (rule div_nat_unique)
   1.243 +  show "(m * n) div (m * q) = n div q"
   1.244 +  proof (cases "q = 0")
   1.245 +    case True
   1.246 +    then show ?thesis
   1.247 +      by simp
   1.248 +  next
   1.249 +    case False
   1.250 +    show ?thesis
   1.251 +    proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
   1.252 +      show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
   1.253 +        by (rule eucl_rel_natI)
   1.254 +          (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>)
   1.255 +    qed          
   1.256 +  qed
   1.257  qed
   1.258  
   1.259  lemma div_by_Suc_0 [simp]:
   1.260 @@ -1187,31 +1213,33 @@
   1.261  
   1.262  subsubsection \<open>Quotient and Remainder\<close>
   1.263  
   1.264 -lemma divmod_nat_rel_mult1_eq:
   1.265 -  "divmod_nat_rel b c (q, r)
   1.266 -   \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
   1.267 -by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
   1.268 -
   1.269  lemma div_mult1_eq:
   1.270    "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
   1.271 -by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
   1.272 -
   1.273 -lemma divmod_nat_rel_add1_eq:
   1.274 -  "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
   1.275 -   \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   1.276 -by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
   1.277 +  by (cases "c = 0")
   1.278 +     (auto simp add: algebra_simps distrib_left [symmetric]
   1.279 +     intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
   1.280 +
   1.281 +lemma eucl_rel_nat_add1_eq:
   1.282 +  "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
   1.283 +   \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
   1.284 +  by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
   1.285  
   1.286  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.287  lemma div_add1_eq:
   1.288 -  "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.289 -by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
   1.290 -
   1.291 -lemma divmod_nat_rel_mult2_eq:
   1.292 -  assumes "divmod_nat_rel a b (q, r)"
   1.293 -  shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
   1.294 -proof -
   1.295 -  { assume "r < b" and "0 < c"
   1.296 -    then have "b * (q mod c) + r < b * c"
   1.297 +  "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.298 +by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
   1.299 +
   1.300 +lemma eucl_rel_nat_mult2_eq:
   1.301 +  assumes "eucl_rel_nat a b (q, r)"
   1.302 +  shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
   1.303 +proof (cases "c = 0")
   1.304 +  case True
   1.305 +  with assms show ?thesis
   1.306 +    by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
   1.307 +next
   1.308 +  case False
   1.309 +  { assume "r < b"
   1.310 +    with False have "b * (q mod c) + r < b * c"
   1.311        apply (cut_tac m = q and n = c in mod_less_divisor)
   1.312        apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   1.313        apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
   1.314 @@ -1219,15 +1247,15 @@
   1.315        done
   1.316      then have "r + b * (q mod c) < b * c"
   1.317        by (simp add: ac_simps)
   1.318 -  } with assms show ?thesis
   1.319 -    by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
   1.320 +  } with assms False show ?thesis
   1.321 +    by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
   1.322  qed
   1.323  
   1.324  lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
   1.325 -by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
   1.326 +by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
   1.327  
   1.328  lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
   1.329 -by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
   1.330 +by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
   1.331  
   1.332  instantiation nat :: semiring_numeral_div
   1.333  begin
   1.334 @@ -1386,8 +1414,8 @@
   1.335    from A B show ?lhs ..
   1.336  next
   1.337    assume P: ?lhs
   1.338 -  then have "divmod_nat_rel m n (q, m - n * q)"
   1.339 -    unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
   1.340 +  then have "eucl_rel_nat m n (q, m - n * q)"
   1.341 +    by (auto intro: eucl_rel_natI simp add: ac_simps)
   1.342    then have "m div n = q"
   1.343      by (rule div_nat_unique)
   1.344    then show ?rhs by simp
   1.345 @@ -1673,9 +1701,19 @@
   1.346  context
   1.347  begin
   1.348  
   1.349 -definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
   1.350 -  where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
   1.351 -    (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
   1.352 +inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
   1.353 +  where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
   1.354 +  | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
   1.355 +  | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
   1.356 +      \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
   1.357 +
   1.358 +lemma eucl_rel_int_iff:    
   1.359 +  "eucl_rel_int k l (q, r) \<longleftrightarrow> 
   1.360 +    k = l * q + r \<and>
   1.361 +     (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
   1.362 +  by (cases "r = 0")
   1.363 +    (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
   1.364 +    simp add: ac_simps sgn_1_pos sgn_1_neg)
   1.365  
   1.366  lemma unique_quotient_lemma:
   1.367    "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
   1.368 @@ -1694,17 +1732,17 @@
   1.369    by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
   1.370  
   1.371  lemma unique_quotient:
   1.372 -  "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
   1.373 -apply (simp add: divmod_int_rel_def linorder_neq_iff split: if_split_asm)
   1.374 -apply (blast intro: order_antisym
   1.375 -             dest: order_eq_refl [THEN unique_quotient_lemma]
   1.376 -             order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   1.377 -done
   1.378 +  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
   1.379 +  apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
   1.380 +  apply (blast intro: order_antisym
   1.381 +    dest: order_eq_refl [THEN unique_quotient_lemma]
   1.382 +    order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
   1.383 +  done
   1.384  
   1.385  lemma unique_remainder:
   1.386 -  "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> r = r'"
   1.387 +  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
   1.388  apply (subgoal_tac "q = q'")
   1.389 - apply (simp add: divmod_int_rel_def)
   1.390 + apply (simp add: eucl_rel_int_iff)
   1.391  apply (blast intro: unique_quotient)
   1.392  done
   1.393  
   1.394 @@ -1733,12 +1771,12 @@
   1.395        then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
   1.396        else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
   1.397  
   1.398 -lemma divmod_int_rel:
   1.399 -  "divmod_int_rel k l (k div l, k mod l)"
   1.400 +lemma eucl_rel_int:
   1.401 +  "eucl_rel_int k l (k div l, k mod l)"
   1.402  proof (cases k rule: int_cases3)
   1.403    case zero
   1.404    then show ?thesis
   1.405 -    by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
   1.406 +    by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
   1.407  next
   1.408    case (pos n)
   1.409    then show ?thesis
   1.410 @@ -1746,7 +1784,7 @@
   1.411      by (cases l rule: int_cases3)
   1.412        (auto simp del: of_nat_mult of_nat_add
   1.413          simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   1.414 -        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
   1.415 +        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
   1.416  next
   1.417    case (neg n)
   1.418    then show ?thesis
   1.419 @@ -1754,29 +1792,29 @@
   1.420      by (cases l rule: int_cases3)
   1.421        (auto simp del: of_nat_mult of_nat_add
   1.422          simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   1.423 -        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
   1.424 +        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
   1.425  qed
   1.426  
   1.427  lemma divmod_int_unique:
   1.428 -  assumes "divmod_int_rel k l (q, r)"
   1.429 +  assumes "eucl_rel_int k l (q, r)"
   1.430    shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
   1.431 -  using assms divmod_int_rel [of k l]
   1.432 +  using assms eucl_rel_int [of k l]
   1.433    using unique_quotient [of k l] unique_remainder [of k l]
   1.434    by auto
   1.435  
   1.436  instance proof
   1.437    fix k l :: int
   1.438    show "k div l * l + k mod l = k"
   1.439 -    using divmod_int_rel [of k l]
   1.440 -    unfolding divmod_int_rel_def by (simp add: ac_simps)
   1.441 +    using eucl_rel_int [of k l]
   1.442 +    unfolding eucl_rel_int_iff by (simp add: ac_simps)
   1.443  next
   1.444    fix k :: int show "k div 0 = 0"
   1.445 -    by (rule div_int_unique, simp add: divmod_int_rel_def)
   1.446 +    by (rule div_int_unique, simp add: eucl_rel_int_iff)
   1.447  next
   1.448    fix k l :: int
   1.449    assume "l \<noteq> 0"
   1.450    then show "k * l div l = k"
   1.451 -    by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
   1.452 +    by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
   1.453  qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
   1.454  
   1.455  end
   1.456 @@ -1789,23 +1827,23 @@
   1.457  proof
   1.458    fix k l s :: int
   1.459    assume "l \<noteq> 0"
   1.460 -  then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
   1.461 -    using divmod_int_rel [of k l]
   1.462 -    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
   1.463 +  then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
   1.464 +    using eucl_rel_int [of k l]
   1.465 +    unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
   1.466    then show "(k + s * l) div l = s + k div l"
   1.467      by (rule div_int_unique)
   1.468  next
   1.469    fix k l s :: int
   1.470    assume "s \<noteq> 0"
   1.471 -  have "\<And>q r. divmod_int_rel k l (q, r)
   1.472 -    \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
   1.473 -    unfolding divmod_int_rel_def
   1.474 +  have "\<And>q r. eucl_rel_int k l (q, r)
   1.475 +    \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
   1.476 +    unfolding eucl_rel_int_iff
   1.477      by (rule linorder_cases [of 0 l])
   1.478        (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
   1.479        mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
   1.480        mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
   1.481 -  then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
   1.482 -    using divmod_int_rel [of k l] .
   1.483 +  then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
   1.484 +    using eucl_rel_int [of k l] .
   1.485    then show "(s * k) div (s * l) = k div l"
   1.486      by (rule div_int_unique)
   1.487  qed
   1.488 @@ -1839,15 +1877,15 @@
   1.489    by (simp add: modulo_int_def int_dvd_iff)
   1.490  
   1.491  lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   1.492 -  using divmod_int_rel [of a b]
   1.493 -  by (auto simp add: divmod_int_rel_def prod_eq_iff)
   1.494 +  using eucl_rel_int [of a b]
   1.495 +  by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   1.496  
   1.497  lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
   1.498     and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
   1.499  
   1.500  lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
   1.501 -  using divmod_int_rel [of a b]
   1.502 -  by (auto simp add: divmod_int_rel_def prod_eq_iff)
   1.503 +  using eucl_rel_int [of a b]
   1.504 +  by (auto simp add: eucl_rel_int_iff prod_eq_iff)
   1.505  
   1.506  lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
   1.507     and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
   1.508 @@ -1857,34 +1895,34 @@
   1.509  
   1.510  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
   1.511  apply (rule div_int_unique)
   1.512 -apply (auto simp add: divmod_int_rel_def)
   1.513 +apply (auto simp add: eucl_rel_int_iff)
   1.514  done
   1.515  
   1.516  lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
   1.517  apply (rule div_int_unique)
   1.518 -apply (auto simp add: divmod_int_rel_def)
   1.519 +apply (auto simp add: eucl_rel_int_iff)
   1.520  done
   1.521  
   1.522  lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
   1.523  apply (rule div_int_unique)
   1.524 -apply (auto simp add: divmod_int_rel_def)
   1.525 +apply (auto simp add: eucl_rel_int_iff)
   1.526  done
   1.527  
   1.528  (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
   1.529  
   1.530  lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
   1.531  apply (rule_tac q = 0 in mod_int_unique)
   1.532 -apply (auto simp add: divmod_int_rel_def)
   1.533 +apply (auto simp add: eucl_rel_int_iff)
   1.534  done
   1.535  
   1.536  lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
   1.537  apply (rule_tac q = 0 in mod_int_unique)
   1.538 -apply (auto simp add: divmod_int_rel_def)
   1.539 +apply (auto simp add: eucl_rel_int_iff)
   1.540  done
   1.541  
   1.542  lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
   1.543  apply (rule_tac q = "-1" in mod_int_unique)
   1.544 -apply (auto simp add: divmod_int_rel_def)
   1.545 +apply (auto simp add: eucl_rel_int_iff)
   1.546  done
   1.547  
   1.548  text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
   1.549 @@ -1893,22 +1931,22 @@
   1.550  subsubsection \<open>Laws for div and mod with Unary Minus\<close>
   1.551  
   1.552  lemma zminus1_lemma:
   1.553 -     "divmod_int_rel a b (q, r) ==> b \<noteq> 0
   1.554 -      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
   1.555 +     "eucl_rel_int a b (q, r) ==> b \<noteq> 0
   1.556 +      ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
   1.557                            if r=0 then 0 else b-r)"
   1.558 -by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
   1.559 +by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff right_diff_distrib)
   1.560  
   1.561  
   1.562  lemma zdiv_zminus1_eq_if:
   1.563       "b \<noteq> (0::int)
   1.564        ==> (-a) div b =
   1.565            (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
   1.566 -by (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN div_int_unique])
   1.567 +by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
   1.568  
   1.569  lemma zmod_zminus1_eq_if:
   1.570       "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
   1.571  apply (case_tac "b = 0", simp)
   1.572 -apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
   1.573 +apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
   1.574  done
   1.575  
   1.576  lemma zmod_zminus1_not_zero:
   1.577 @@ -2022,27 +2060,27 @@
   1.578  text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
   1.579  
   1.580  lemma zmult1_lemma:
   1.581 -     "[| divmod_int_rel b c (q, r) |]
   1.582 -      ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
   1.583 -by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
   1.584 +     "[| eucl_rel_int b c (q, r) |]
   1.585 +      ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
   1.586 +by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
   1.587  
   1.588  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   1.589  apply (case_tac "c = 0", simp)
   1.590 -apply (blast intro: divmod_int_rel [THEN zmult1_lemma, THEN div_int_unique])
   1.591 +apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
   1.592  done
   1.593  
   1.594  text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
   1.595  
   1.596  lemma zadd1_lemma:
   1.597 -     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
   1.598 -      ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   1.599 -by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
   1.600 +     "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
   1.601 +      ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
   1.602 +by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
   1.603  
   1.604  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.605  lemma zdiv_zadd1_eq:
   1.606       "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.607  apply (case_tac "c = 0", simp)
   1.608 -apply (blast intro: zadd1_lemma [OF divmod_int_rel divmod_int_rel] div_int_unique)
   1.609 +apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
   1.610  done
   1.611  
   1.612  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
   1.613 @@ -2095,9 +2133,9 @@
   1.614  apply simp
   1.615  done
   1.616  
   1.617 -lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
   1.618 -      ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
   1.619 -by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
   1.620 +lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
   1.621 +      ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
   1.622 +by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
   1.623                     zero_less_mult_iff distrib_left [symmetric]
   1.624                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
   1.625  
   1.626 @@ -2105,14 +2143,14 @@
   1.627    fixes a b c :: int
   1.628    shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
   1.629  apply (case_tac "b = 0", simp)
   1.630 -apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN div_int_unique])
   1.631 +apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
   1.632  done
   1.633  
   1.634  lemma zmod_zmult2_eq:
   1.635    fixes a b c :: int
   1.636    shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
   1.637  apply (case_tac "b = 0", simp)
   1.638 -apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN mod_int_unique])
   1.639 +apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
   1.640  done
   1.641  
   1.642  lemma div_pos_geq:
   1.643 @@ -2199,27 +2237,27 @@
   1.644  
   1.645  subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
   1.646  
   1.647 -lemma pos_divmod_int_rel_mult_2:
   1.648 +lemma pos_eucl_rel_int_mult_2:
   1.649    assumes "0 \<le> b"
   1.650 -  assumes "divmod_int_rel a b (q, r)"
   1.651 -  shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
   1.652 -  using assms unfolding divmod_int_rel_def by auto
   1.653 -
   1.654 -lemma neg_divmod_int_rel_mult_2:
   1.655 +  assumes "eucl_rel_int a b (q, r)"
   1.656 +  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
   1.657 +  using assms unfolding eucl_rel_int_iff by auto
   1.658 +
   1.659 +lemma neg_eucl_rel_int_mult_2:
   1.660    assumes "b \<le> 0"
   1.661 -  assumes "divmod_int_rel (a + 1) b (q, r)"
   1.662 -  shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
   1.663 -  using assms unfolding divmod_int_rel_def by auto
   1.664 +  assumes "eucl_rel_int (a + 1) b (q, r)"
   1.665 +  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
   1.666 +  using assms unfolding eucl_rel_int_iff by auto
   1.667  
   1.668  text\<open>computing div by shifting\<close>
   1.669  
   1.670  lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
   1.671 -  using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel]
   1.672 +  using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
   1.673    by (rule div_int_unique)
   1.674  
   1.675  lemma neg_zdiv_mult_2:
   1.676    assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
   1.677 -  using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel]
   1.678 +  using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
   1.679    by (rule div_int_unique)
   1.680  
   1.681  (* FIXME: add rules for negative numerals *)
   1.682 @@ -2240,14 +2278,14 @@
   1.683    fixes a b :: int
   1.684    assumes "0 \<le> a"
   1.685    shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
   1.686 -  using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
   1.687 +  using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   1.688    by (rule mod_int_unique)
   1.689  
   1.690  lemma neg_zmod_mult_2:
   1.691    fixes a b :: int
   1.692    assumes "a \<le> 0"
   1.693    shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
   1.694 -  using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
   1.695 +  using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   1.696    by (rule mod_int_unique)
   1.697  
   1.698  (* FIXME: add rules for negative numerals *)
   1.699 @@ -2452,19 +2490,19 @@
   1.700  text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
   1.701  
   1.702  lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
   1.703 -  by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
   1.704 +  by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
   1.705  
   1.706  lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
   1.707    by (rule div_int_unique [of a b q r],
   1.708 -    simp add: divmod_int_rel_def)
   1.709 +    simp add: eucl_rel_int_iff)
   1.710  
   1.711  lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
   1.712    by (rule mod_int_unique [of a b q r],
   1.713 -    simp add: divmod_int_rel_def)
   1.714 +    simp add: eucl_rel_int_iff)
   1.715  
   1.716  lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   1.717    by (rule mod_int_unique [of a b q r],
   1.718 -    simp add: divmod_int_rel_def)
   1.719 +    simp add: eucl_rel_int_iff)
   1.720  
   1.721  lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
   1.722  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
     2.1 --- a/src/HOL/Library/Polynomial.thy	Thu Dec 22 08:43:30 2016 +0100
     2.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Dec 22 10:42:08 2016 +0100
     2.3 @@ -1613,18 +1613,26 @@
     2.4  
     2.5  subsection \<open>Long division of polynomials\<close>
     2.6  
     2.7 -definition pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
     2.8 -where
     2.9 -  "pdivmod_rel x y q r \<longleftrightarrow>
    2.10 -    x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
    2.11 -
    2.12 -lemma pdivmod_rel_0:
    2.13 -  "pdivmod_rel 0 y 0 0"
    2.14 -  unfolding pdivmod_rel_def by simp
    2.15 -
    2.16 -lemma pdivmod_rel_by_0:
    2.17 -  "pdivmod_rel x 0 0 x"
    2.18 -  unfolding pdivmod_rel_def by simp
    2.19 +inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
    2.20 +  where eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
    2.21 +  | eucl_rel_poly_dividesI: "y \<noteq> 0 \<Longrightarrow> x = q * y \<Longrightarrow> eucl_rel_poly x y (q, 0)"
    2.22 +  | eucl_rel_poly_remainderI: "y \<noteq> 0 \<Longrightarrow> degree r < degree y
    2.23 +      \<Longrightarrow> x = q * y + r \<Longrightarrow> eucl_rel_poly x y (q, r)"
    2.24 +  
    2.25 +lemma eucl_rel_poly_iff:
    2.26 +  "eucl_rel_poly x y (q, r) \<longleftrightarrow>
    2.27 +    x = q * y + r \<and>
    2.28 +      (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
    2.29 +  by (auto elim: eucl_rel_poly.cases
    2.30 +    intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI)
    2.31 +  
    2.32 +lemma eucl_rel_poly_0:
    2.33 +  "eucl_rel_poly 0 y (0, 0)"
    2.34 +  unfolding eucl_rel_poly_iff by simp
    2.35 +
    2.36 +lemma eucl_rel_poly_by_0:
    2.37 +  "eucl_rel_poly x 0 (0, x)"
    2.38 +  unfolding eucl_rel_poly_iff by simp
    2.39  
    2.40  lemma eq_zero_or_degree_less:
    2.41    assumes "degree p \<le> n" and "coeff p n = 0"
    2.42 @@ -1650,15 +1658,15 @@
    2.43    then show ?thesis ..
    2.44  qed
    2.45  
    2.46 -lemma pdivmod_rel_pCons:
    2.47 -  assumes rel: "pdivmod_rel x y q r"
    2.48 +lemma eucl_rel_poly_pCons:
    2.49 +  assumes rel: "eucl_rel_poly x y (q, r)"
    2.50    assumes y: "y \<noteq> 0"
    2.51    assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
    2.52 -  shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
    2.53 -    (is "pdivmod_rel ?x y ?q ?r")
    2.54 +  shows "eucl_rel_poly (pCons a x) y (pCons b q, pCons a r - smult b y)"
    2.55 +    (is "eucl_rel_poly ?x y (?q, ?r)")
    2.56  proof -
    2.57    have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
    2.58 -    using assms unfolding pdivmod_rel_def by simp_all
    2.59 +    using assms unfolding eucl_rel_poly_iff by simp_all
    2.60  
    2.61    have 1: "?x = ?q * y + ?r"
    2.62      using b x by simp
    2.63 @@ -1678,31 +1686,31 @@
    2.64    qed
    2.65  
    2.66    from 1 2 show ?thesis
    2.67 -    unfolding pdivmod_rel_def
    2.68 +    unfolding eucl_rel_poly_iff
    2.69      using \<open>y \<noteq> 0\<close> by simp
    2.70  qed
    2.71  
    2.72 -lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
    2.73 +lemma eucl_rel_poly_exists: "\<exists>q r. eucl_rel_poly x y (q, r)"
    2.74  apply (cases "y = 0")
    2.75 -apply (fast intro!: pdivmod_rel_by_0)
    2.76 +apply (fast intro!: eucl_rel_poly_by_0)
    2.77  apply (induct x)
    2.78 -apply (fast intro!: pdivmod_rel_0)
    2.79 -apply (fast intro!: pdivmod_rel_pCons)
    2.80 +apply (fast intro!: eucl_rel_poly_0)
    2.81 +apply (fast intro!: eucl_rel_poly_pCons)
    2.82  done
    2.83  
    2.84 -lemma pdivmod_rel_unique:
    2.85 -  assumes 1: "pdivmod_rel x y q1 r1"
    2.86 -  assumes 2: "pdivmod_rel x y q2 r2"
    2.87 +lemma eucl_rel_poly_unique:
    2.88 +  assumes 1: "eucl_rel_poly x y (q1, r1)"
    2.89 +  assumes 2: "eucl_rel_poly x y (q2, r2)"
    2.90    shows "q1 = q2 \<and> r1 = r2"
    2.91  proof (cases "y = 0")
    2.92    assume "y = 0" with assms show ?thesis
    2.93 -    by (simp add: pdivmod_rel_def)
    2.94 +    by (simp add: eucl_rel_poly_iff)
    2.95  next
    2.96    assume [simp]: "y \<noteq> 0"
    2.97    from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
    2.98 -    unfolding pdivmod_rel_def by simp_all
    2.99 +    unfolding eucl_rel_poly_iff by simp_all
   2.100    from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
   2.101 -    unfolding pdivmod_rel_def by simp_all
   2.102 +    unfolding eucl_rel_poly_iff by simp_all
   2.103    from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
   2.104      by (simp add: algebra_simps)
   2.105    from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
   2.106 @@ -1723,15 +1731,15 @@
   2.107    qed
   2.108  qed
   2.109  
   2.110 -lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0"
   2.111 -by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0)
   2.112 -
   2.113 -lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
   2.114 -by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
   2.115 -
   2.116 -lemmas pdivmod_rel_unique_div = pdivmod_rel_unique [THEN conjunct1]
   2.117 -
   2.118 -lemmas pdivmod_rel_unique_mod = pdivmod_rel_unique [THEN conjunct2]
   2.119 +lemma eucl_rel_poly_0_iff: "eucl_rel_poly 0 y (q, r) \<longleftrightarrow> q = 0 \<and> r = 0"
   2.120 +by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_0)
   2.121 +
   2.122 +lemma eucl_rel_poly_by_0_iff: "eucl_rel_poly x 0 (q, r) \<longleftrightarrow> q = 0 \<and> r = x"
   2.123 +by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_by_0)
   2.124 +
   2.125 +lemmas eucl_rel_poly_unique_div = eucl_rel_poly_unique [THEN conjunct1]
   2.126 +
   2.127 +lemmas eucl_rel_poly_unique_mod = eucl_rel_poly_unique [THEN conjunct2]
   2.128  
   2.129  
   2.130  
   2.131 @@ -2236,8 +2244,8 @@
   2.132      if g = 0 then f
   2.133      else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g"
   2.134  
   2.135 -lemma pdivmod_rel: "pdivmod_rel (x::'a::field poly) y (x div y) (x mod y)"
   2.136 -  unfolding pdivmod_rel_def
   2.137 +lemma eucl_rel_poly: "eucl_rel_poly (x::'a::field poly) y (x div y, x mod y)"
   2.138 +  unfolding eucl_rel_poly_iff
   2.139  proof (intro conjI)
   2.140    show "x = x div y * y + x mod y"
   2.141    proof(cases "y = 0")
   2.142 @@ -2261,24 +2269,24 @@
   2.143  qed
   2.144  
   2.145  lemma div_poly_eq:
   2.146 -  "pdivmod_rel (x::'a::field poly) y q r \<Longrightarrow> x div y = q"
   2.147 -  by(rule pdivmod_rel_unique_div[OF pdivmod_rel])
   2.148 +  "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x div y = q"
   2.149 +  by(rule eucl_rel_poly_unique_div[OF eucl_rel_poly])
   2.150  
   2.151  lemma mod_poly_eq:
   2.152 -  "pdivmod_rel (x::'a::field poly) y q r \<Longrightarrow> x mod y = r"
   2.153 -  by (rule pdivmod_rel_unique_mod[OF pdivmod_rel])
   2.154 +  "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x mod y = r"
   2.155 +  by (rule eucl_rel_poly_unique_mod[OF eucl_rel_poly])
   2.156  
   2.157  instance
   2.158  proof
   2.159    fix x y :: "'a poly"
   2.160 -  from pdivmod_rel[of x y,unfolded pdivmod_rel_def]
   2.161 +  from eucl_rel_poly[of x y,unfolded eucl_rel_poly_iff]
   2.162    show "x div y * y + x mod y = x" by auto
   2.163  next
   2.164    fix x y z :: "'a poly"
   2.165    assume "y \<noteq> 0"
   2.166 -  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
   2.167 -    using pdivmod_rel [of x y]
   2.168 -    by (simp add: pdivmod_rel_def distrib_right)
   2.169 +  hence "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
   2.170 +    using eucl_rel_poly [of x y]
   2.171 +    by (simp add: eucl_rel_poly_iff distrib_right)
   2.172    thus "(x + z * y) div y = z + x div y"
   2.173      by (rule div_poly_eq)
   2.174  next
   2.175 @@ -2286,23 +2294,23 @@
   2.176    assume "x \<noteq> 0"
   2.177    show "(x * y) div (x * z) = y div z"
   2.178    proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
   2.179 -    have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
   2.180 -      by (rule pdivmod_rel_by_0)
   2.181 +    have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
   2.182 +      by (rule eucl_rel_poly_by_0)
   2.183      then have [simp]: "\<And>x::'a poly. x div 0 = 0"
   2.184        by (rule div_poly_eq)
   2.185 -    have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
   2.186 -      by (rule pdivmod_rel_0)
   2.187 +    have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
   2.188 +      by (rule eucl_rel_poly_0)
   2.189      then have [simp]: "\<And>x::'a poly. 0 div x = 0"
   2.190        by (rule div_poly_eq)
   2.191      case False then show ?thesis by auto
   2.192    next
   2.193      case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
   2.194      with \<open>x \<noteq> 0\<close>
   2.195 -    have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
   2.196 -      by (auto simp add: pdivmod_rel_def algebra_simps)
   2.197 +    have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
   2.198 +      by (auto simp add: eucl_rel_poly_iff algebra_simps)
   2.199          (rule classical, simp add: degree_mult_eq)
   2.200 -    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
   2.201 -    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
   2.202 +    moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
   2.203 +    ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
   2.204      then show ?thesis by (simp add: div_poly_eq)
   2.205    qed
   2.206  qed
   2.207 @@ -2311,35 +2319,35 @@
   2.208  
   2.209  lemma degree_mod_less:
   2.210    "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
   2.211 -  using pdivmod_rel [of x y]
   2.212 -  unfolding pdivmod_rel_def by simp
   2.213 +  using eucl_rel_poly [of x y]
   2.214 +  unfolding eucl_rel_poly_iff by simp
   2.215  
   2.216  lemma div_poly_less: "degree (x::'a::field poly) < degree y \<Longrightarrow> x div y = 0"
   2.217  proof -
   2.218    assume "degree x < degree y"
   2.219 -  hence "pdivmod_rel x y 0 x"
   2.220 -    by (simp add: pdivmod_rel_def)
   2.221 +  hence "eucl_rel_poly x y (0, x)"
   2.222 +    by (simp add: eucl_rel_poly_iff)
   2.223    thus "x div y = 0" by (rule div_poly_eq)
   2.224  qed
   2.225  
   2.226  lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
   2.227  proof -
   2.228    assume "degree x < degree y"
   2.229 -  hence "pdivmod_rel x y 0 x"
   2.230 -    by (simp add: pdivmod_rel_def)
   2.231 +  hence "eucl_rel_poly x y (0, x)"
   2.232 +    by (simp add: eucl_rel_poly_iff)
   2.233    thus "x mod y = x" by (rule mod_poly_eq)
   2.234  qed
   2.235  
   2.236 -lemma pdivmod_rel_smult_left:
   2.237 -  "pdivmod_rel x y q r
   2.238 -    \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
   2.239 -  unfolding pdivmod_rel_def by (simp add: smult_add_right)
   2.240 +lemma eucl_rel_poly_smult_left:
   2.241 +  "eucl_rel_poly x y (q, r)
   2.242 +    \<Longrightarrow> eucl_rel_poly (smult a x) y (smult a q, smult a r)"
   2.243 +  unfolding eucl_rel_poly_iff by (simp add: smult_add_right)
   2.244  
   2.245  lemma div_smult_left: "(smult (a::'a::field) x) div y = smult a (x div y)"
   2.246 -  by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
   2.247 +  by (rule div_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
   2.248  
   2.249  lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
   2.250 -  by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
   2.251 +  by (rule mod_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
   2.252  
   2.253  lemma poly_div_minus_left [simp]:
   2.254    fixes x y :: "'a::field poly"
   2.255 @@ -2351,23 +2359,23 @@
   2.256    shows "(- x) mod y = - (x mod y)"
   2.257    using mod_smult_left [of "- 1::'a"] by simp
   2.258  
   2.259 -lemma pdivmod_rel_add_left:
   2.260 -  assumes "pdivmod_rel x y q r"
   2.261 -  assumes "pdivmod_rel x' y q' r'"
   2.262 -  shows "pdivmod_rel (x + x') y (q + q') (r + r')"
   2.263 -  using assms unfolding pdivmod_rel_def
   2.264 +lemma eucl_rel_poly_add_left:
   2.265 +  assumes "eucl_rel_poly x y (q, r)"
   2.266 +  assumes "eucl_rel_poly x' y (q', r')"
   2.267 +  shows "eucl_rel_poly (x + x') y (q + q', r + r')"
   2.268 +  using assms unfolding eucl_rel_poly_iff
   2.269    by (auto simp add: algebra_simps degree_add_less)
   2.270  
   2.271  lemma poly_div_add_left:
   2.272    fixes x y z :: "'a::field poly"
   2.273    shows "(x + y) div z = x div z + y div z"
   2.274 -  using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
   2.275 +  using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
   2.276    by (rule div_poly_eq)
   2.277  
   2.278  lemma poly_mod_add_left:
   2.279    fixes x y z :: "'a::field poly"
   2.280    shows "(x + y) mod z = x mod z + y mod z"
   2.281 -  using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
   2.282 +  using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
   2.283    by (rule mod_poly_eq)
   2.284  
   2.285  lemma poly_div_diff_left:
   2.286 @@ -2380,17 +2388,17 @@
   2.287    shows "(x - y) mod z = x mod z - y mod z"
   2.288    by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
   2.289  
   2.290 -lemma pdivmod_rel_smult_right:
   2.291 -  "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
   2.292 -    \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
   2.293 -  unfolding pdivmod_rel_def by simp
   2.294 +lemma eucl_rel_poly_smult_right:
   2.295 +  "a \<noteq> 0 \<Longrightarrow> eucl_rel_poly x y (q, r)
   2.296 +    \<Longrightarrow> eucl_rel_poly x (smult a y) (smult (inverse a) q, r)"
   2.297 +  unfolding eucl_rel_poly_iff by simp
   2.298  
   2.299  lemma div_smult_right:
   2.300    "(a::'a::field) \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
   2.301 -  by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
   2.302 +  by (rule div_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
   2.303  
   2.304  lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
   2.305 -  by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
   2.306 +  by (rule mod_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
   2.307  
   2.308  lemma poly_div_minus_right [simp]:
   2.309    fixes x y :: "'a::field poly"
   2.310 @@ -2402,30 +2410,30 @@
   2.311    shows "x mod (- y) = x mod y"
   2.312    using mod_smult_right [of "- 1::'a"] by simp
   2.313  
   2.314 -lemma pdivmod_rel_mult:
   2.315 -  "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
   2.316 -    \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
   2.317 -apply (cases "z = 0", simp add: pdivmod_rel_def)
   2.318 -apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff)
   2.319 +lemma eucl_rel_poly_mult:
   2.320 +  "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly q z (q', r')
   2.321 +    \<Longrightarrow> eucl_rel_poly x (y * z) (q', y * r' + r)"
   2.322 +apply (cases "z = 0", simp add: eucl_rel_poly_iff)
   2.323 +apply (cases "y = 0", simp add: eucl_rel_poly_by_0_iff eucl_rel_poly_0_iff)
   2.324  apply (cases "r = 0")
   2.325  apply (cases "r' = 0")
   2.326 -apply (simp add: pdivmod_rel_def)
   2.327 -apply (simp add: pdivmod_rel_def field_simps degree_mult_eq)
   2.328 +apply (simp add: eucl_rel_poly_iff)
   2.329 +apply (simp add: eucl_rel_poly_iff field_simps degree_mult_eq)
   2.330  apply (cases "r' = 0")
   2.331 -apply (simp add: pdivmod_rel_def degree_mult_eq)
   2.332 -apply (simp add: pdivmod_rel_def field_simps)
   2.333 +apply (simp add: eucl_rel_poly_iff degree_mult_eq)
   2.334 +apply (simp add: eucl_rel_poly_iff field_simps)
   2.335  apply (simp add: degree_mult_eq degree_add_less)
   2.336  done
   2.337  
   2.338  lemma poly_div_mult_right:
   2.339    fixes x y z :: "'a::field poly"
   2.340    shows "x div (y * z) = (x div y) div z"
   2.341 -  by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
   2.342 +  by (rule div_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
   2.343  
   2.344  lemma poly_mod_mult_right:
   2.345    fixes x y z :: "'a::field poly"
   2.346    shows "x mod (y * z) = y * (x div y mod z) + x mod y"
   2.347 -  by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
   2.348 +  by (rule mod_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
   2.349  
   2.350  lemma mod_pCons:
   2.351    fixes a and x
   2.352 @@ -2434,7 +2442,7 @@
   2.353    shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
   2.354  unfolding b
   2.355  apply (rule mod_poly_eq)
   2.356 -apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
   2.357 +apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl])
   2.358  done
   2.359  
   2.360  definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
   2.361 @@ -2453,9 +2461,9 @@
   2.362          in (pCons b s, pCons a r - smult b q)))"
   2.363    apply (simp add: pdivmod_def Let_def, safe)
   2.364    apply (rule div_poly_eq)
   2.365 -  apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
   2.366 +  apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
   2.367    apply (rule mod_poly_eq)
   2.368 -  apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
   2.369 +  apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
   2.370    done
   2.371  
   2.372  lemma pdivmod_fold_coeffs:
   2.373 @@ -2700,8 +2708,8 @@
   2.374  (* *************** *)
   2.375  subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close>
   2.376  
   2.377 -lemma pdivmod_pdivmodrel: "pdivmod_rel p q r s = (pdivmod p q = (r, s))"
   2.378 -  by (metis pdivmod_def pdivmod_rel pdivmod_rel_unique prod.sel)
   2.379 +lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> pdivmod p q = (r, s)"
   2.380 +  by (metis pdivmod_def eucl_rel_poly eucl_rel_poly_unique)
   2.381  
   2.382  lemma pdivmod_via_pseudo_divmod: "pdivmod f g = (if g = 0 then (0,f) 
   2.383       else let 
   2.384 @@ -2720,7 +2728,7 @@
   2.385      unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto
   2.386    from pseudo_divmod[OF h0 p, unfolded h1] 
   2.387    have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h" by auto
   2.388 -  have "pdivmod_rel f h q r" unfolding pdivmod_rel_def using f r h0 by auto
   2.389 +  have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto
   2.390    hence "pdivmod f h = (q,r)" by (simp add: pdivmod_pdivmodrel)
   2.391    hence "pdivmod f g = (smult lc q, r)" 
   2.392      unfolding pdivmod_def h_def div_smult_right[OF lc] mod_smult_right[OF lc]