# HG changeset patch
# User haftmann
# Date 1482399728 -3600
# Node ID 255741c5f862ad1a062ca88e3178824c6fac12c2
# Parent  5bd30359e46e7df973fb9af00fe528feb7415e20
more uniform div/mod relations

diff -r 5bd30359e46e -r 255741c5f862 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Dec 22 08:43:30 2016 +0100
+++ b/src/HOL/Divides.thy	Thu Dec 22 10:42:08 2016 +0100
@@ -828,18 +828,18 @@
   @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
 \<close>
 
-definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
-  "divmod_nat_rel m n qr \<longleftrightarrow>
-    m = fst qr * n + snd qr \<and>
-      (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)"
-
-text \<open>@{const divmod_nat_rel} is total:\<close>
-
-qualified lemma divmod_nat_rel_ex:
-  obtains q r where "divmod_nat_rel m n (q, r)"
+inductive eucl_rel_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool"
+  where eucl_rel_nat_by0: "eucl_rel_nat m 0 (0, m)"
+  | eucl_rel_natI: "r < n \<Longrightarrow> m = q * n + r \<Longrightarrow> eucl_rel_nat m n (q, r)"
+
+text \<open>@{const eucl_rel_nat} is total:\<close>
+
+qualified lemma eucl_rel_nat_ex:
+  obtains q r where "eucl_rel_nat m n (q, r)"
 proof (cases "n = 0")
-  case True  with that show thesis
-    by (auto simp add: divmod_nat_rel_def)
+  case True
+  with that eucl_rel_nat_by0 show thesis
+    by blast
 next
   case False
   have "\<exists>q r. m = q * n + r \<and> r < n"
@@ -864,74 +864,92 @@
       with \<open>n \<noteq> 0\<close> show ?thesis by blast
     qed
   qed
-  with that show thesis
-    using \<open>n \<noteq> 0\<close> by (auto simp add: divmod_nat_rel_def)
+  with that \<open>n \<noteq> 0\<close> eucl_rel_natI show thesis
+    by blast
 qed
 
-text \<open>@{const divmod_nat_rel} is injective:\<close>
-
-qualified lemma divmod_nat_rel_unique:
-  assumes "divmod_nat_rel m n qr"
-    and "divmod_nat_rel m n qr'"
-  shows "qr = qr'"
+text \<open>@{const eucl_rel_nat} is injective:\<close>
+
+qualified lemma eucl_rel_nat_unique_div:
+  assumes "eucl_rel_nat m n (q, r)"
+    and "eucl_rel_nat m n (q', r')"
+  shows "q = q'"
 proof (cases "n = 0")
   case True with assms show ?thesis
-    by (cases qr, cases qr')
-      (simp add: divmod_nat_rel_def)
+    by (auto elim: eucl_rel_nat.cases)
 next
   case False
-  have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
-  apply (rule leI)
-  apply (subst less_iff_Suc_add)
-  apply (auto simp add: add_mult_distrib)
-  done
-  from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
-    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
-  with assms have "snd qr = snd qr'"
-    by (simp add: divmod_nat_rel_def)
-  with * show ?thesis by (cases qr, cases qr') simp
+  have *: "q' \<le> q" if "q' * n + r' = q * n + r" "r < n" for q r q' r' :: nat
+  proof (rule ccontr)
+    assume "\<not> q' \<le> q"
+    then have "q < q'"
+      by (simp add: not_le)
+    with that show False
+      by (auto simp add: less_iff_Suc_add algebra_simps)
+  qed
+  from \<open>n \<noteq> 0\<close> assms show ?thesis
+    by (auto intro: order_antisym elim: eucl_rel_nat.cases dest: * sym split: if_splits)
+qed
+
+qualified lemma eucl_rel_nat_unique_mod:
+  assumes "eucl_rel_nat m n (q, r)"
+    and "eucl_rel_nat m n (q', r')"
+  shows "r = r'"
+proof -
+  from assms have "q' = q"
+    by (auto intro: eucl_rel_nat_unique_div)
+  with assms show ?thesis
+    by (auto elim!: eucl_rel_nat.cases)
 qed
 
 text \<open>
   We instantiate divisibility on the natural numbers by
-  means of @{const divmod_nat_rel}:
+  means of @{const eucl_rel_nat}:
 \<close>
 
 qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
-  "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
-
-qualified lemma divmod_nat_rel_divmod_nat:
-  "divmod_nat_rel m n (divmod_nat m n)"
+  "divmod_nat m n = (THE qr. eucl_rel_nat m n qr)"
+
+qualified lemma eucl_rel_nat_divmod_nat:
+  "eucl_rel_nat m n (divmod_nat m n)"
 proof -
-  from divmod_nat_rel_ex
-    obtain qr where rel: "divmod_nat_rel m n qr" .
+  from eucl_rel_nat_ex
+    obtain q r where rel: "eucl_rel_nat m n (q, r)" .
   then show ?thesis
-  by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
+    by (auto simp add: divmod_nat_def intro: theI
+      elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
 qed
 
 qualified lemma divmod_nat_unique:
-  assumes "divmod_nat_rel m n qr"
-  shows "divmod_nat m n = qr"
-  using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
-
-qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
-  by (simp add: divmod_nat_unique divmod_nat_rel_def)
-
-qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
-  by (simp add: divmod_nat_unique divmod_nat_rel_def)
-
-qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
-  by (simp add: divmod_nat_unique divmod_nat_rel_def)
+  "divmod_nat m n = (q, r)" if "eucl_rel_nat m n (q, r)"
+  using that
+  by (auto simp add: divmod_nat_def intro: eucl_rel_nat_divmod_nat elim: eucl_rel_nat_unique_div eucl_rel_nat_unique_mod)
+
+qualified lemma divmod_nat_zero:
+  "divmod_nat m 0 = (0, m)"
+  by (rule divmod_nat_unique) (fact eucl_rel_nat_by0)
+
+qualified lemma divmod_nat_zero_left:
+  "divmod_nat 0 n = (0, 0)"
+  by (rule divmod_nat_unique) 
+    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
+
+qualified lemma divmod_nat_base:
+  "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
+  by (rule divmod_nat_unique) 
+    (cases n, auto intro: eucl_rel_nat_by0 eucl_rel_natI)
 
 qualified lemma divmod_nat_step:
   assumes "0 < n" and "n \<le> m"
-  shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
+  shows "divmod_nat m n =
+    (Suc (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
 proof (rule divmod_nat_unique)
-  have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
-    by (fact divmod_nat_rel_divmod_nat)
-  then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
-    unfolding divmod_nat_rel_def using assms
-      by (auto split: if_splits simp add: algebra_simps)
+  have "eucl_rel_nat (m - n) n (divmod_nat (m - n) n)"
+    by (fact eucl_rel_nat_divmod_nat)
+  then show "eucl_rel_nat m n (Suc
+    (fst (divmod_nat (m - n) n)), snd (divmod_nat (m - n) n))"
+    using assms
+      by (auto split: if_splits intro: eucl_rel_natI elim!: eucl_rel_nat.cases simp add: algebra_simps)
 qed
 
 end
@@ -969,19 +987,19 @@
   by (simp add: prod_eq_iff)
 
 lemma div_nat_unique:
-  assumes "divmod_nat_rel m n (q, r)"
+  assumes "eucl_rel_nat m n (q, r)"
   shows "m div n = q"
   using assms
   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
 
 lemma mod_nat_unique:
-  assumes "divmod_nat_rel m n (q, r)"
+  assumes "eucl_rel_nat m n (q, r)"
   shows "m mod n = r"
   using assms
   by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
 
-lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
-  using Divides.divmod_nat_rel_divmod_nat
+lemma eucl_rel_nat: "eucl_rel_nat m n (m div n, m mod n)"
+  using Divides.eucl_rel_nat_divmod_nat
   by (simp add: divmod_nat_div_mod)
 
 text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
@@ -1014,22 +1032,21 @@
   fixes m n :: nat
   assumes "n > 0"
   shows "m mod n < n"
-  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
-  by (auto split: if_splits)
+  using assms eucl_rel_nat [of m n]
+    by (auto elim: eucl_rel_nat.cases)
 
 lemma mod_le_divisor [simp]:
   fixes m n :: nat
   assumes "n > 0"
   shows "m mod n \<le> n"
-proof (rule less_imp_le)
-  from assms show "m mod n < n"
-    by simp
-qed
+  using assms eucl_rel_nat [of m n]
+    by (auto elim: eucl_rel_nat.cases)
 
 instance proof
   fix m n :: nat
   show "m div n * n + m mod n = m"
-    using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
+    using eucl_rel_nat [of m n]
+    by (auto elim: eucl_rel_nat.cases)
 next
   fix n :: nat show "n div 0 = 0"
     by (simp add: div_nat_def Divides.divmod_nat_zero)
@@ -1037,7 +1054,7 @@
   fix m n :: nat
   assume "n \<noteq> 0"
   then show "m * n div n = m"
-    by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
+    by (auto intro!: eucl_rel_natI div_nat_unique [of _ _ _ 0])
 qed (simp_all add: unit_factor_nat_def)
 
 end
@@ -1051,11 +1068,20 @@
 next
   fix m n q :: nat
   assume "m \<noteq> 0"
-  then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
-    using div_mult_mod_eq [of n q]
-    by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
-  then show "(m * n) div (m * q) = n div q"
-    by (rule div_nat_unique)
+  show "(m * n) div (m * q) = n div q"
+  proof (cases "q = 0")
+    case True
+    then show ?thesis
+      by simp
+  next
+    case False
+    show ?thesis
+    proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
+      show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
+        by (rule eucl_rel_natI)
+          (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>)
+    qed          
+  qed
 qed
 
 lemma div_by_Suc_0 [simp]:
@@ -1187,31 +1213,33 @@
 
 subsubsection \<open>Quotient and Remainder\<close>
 
-lemma divmod_nat_rel_mult1_eq:
-  "divmod_nat_rel b c (q, r)
-   \<Longrightarrow> divmod_nat_rel (a * b) c (a * q + a * r div c, a * r mod c)"
-by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
-
 lemma div_mult1_eq:
   "(a * b) div c = a * (b div c) + a * (b mod c) div (c::nat)"
-by (blast intro: divmod_nat_rel_mult1_eq [THEN div_nat_unique] divmod_nat_rel)
-
-lemma divmod_nat_rel_add1_eq:
-  "divmod_nat_rel a c (aq, ar) \<Longrightarrow> divmod_nat_rel b c (bq, br)
-   \<Longrightarrow> divmod_nat_rel (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
-by (auto simp add: split_ifs divmod_nat_rel_def algebra_simps)
+  by (cases "c = 0")
+     (auto simp add: algebra_simps distrib_left [symmetric]
+     intro!: div_nat_unique [of _ _ _ "(a * (b mod c)) mod c"] eucl_rel_natI)
+
+lemma eucl_rel_nat_add1_eq:
+  "eucl_rel_nat a c (aq, ar) \<Longrightarrow> eucl_rel_nat b c (bq, br)
+   \<Longrightarrow> eucl_rel_nat (a + b) c (aq + bq + (ar + br) div c, (ar + br) mod c)"
+  by (auto simp add: split_ifs algebra_simps elim!: eucl_rel_nat.cases intro: eucl_rel_nat_by0 eucl_rel_natI)
 
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma div_add1_eq:
-  "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
-by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
-
-lemma divmod_nat_rel_mult2_eq:
-  assumes "divmod_nat_rel a b (q, r)"
-  shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
-proof -
-  { assume "r < b" and "0 < c"
-    then have "b * (q mod c) + r < b * c"
+  "(a + b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
+by (blast intro: eucl_rel_nat_add1_eq [THEN div_nat_unique] eucl_rel_nat)
+
+lemma eucl_rel_nat_mult2_eq:
+  assumes "eucl_rel_nat a b (q, r)"
+  shows "eucl_rel_nat a (b * c) (q div c, b *(q mod c) + r)"
+proof (cases "c = 0")
+  case True
+  with assms show ?thesis
+    by (auto intro: eucl_rel_nat_by0 elim!: eucl_rel_nat.cases simp add: ac_simps)
+next
+  case False
+  { assume "r < b"
+    with False have "b * (q mod c) + r < b * c"
       apply (cut_tac m = q and n = c in mod_less_divisor)
       apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
       apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
@@ -1219,15 +1247,15 @@
       done
     then have "r + b * (q mod c) < b * c"
       by (simp add: ac_simps)
-  } with assms show ?thesis
-    by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
+  } with assms False show ?thesis
+    by (auto simp add: algebra_simps add_mult_distrib2 [symmetric] elim!: eucl_rel_nat.cases intro: eucl_rel_nat.intros)
 qed
 
 lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
-by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
+by (force simp add: eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN div_nat_unique])
 
 lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
-by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
+by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
 
 instantiation nat :: semiring_numeral_div
 begin
@@ -1386,8 +1414,8 @@
   from A B show ?lhs ..
 next
   assume P: ?lhs
-  then have "divmod_nat_rel m n (q, m - n * q)"
-    unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
+  then have "eucl_rel_nat m n (q, m - n * q)"
+    by (auto intro: eucl_rel_natI simp add: ac_simps)
   then have "m div n = q"
     by (rule div_nat_unique)
   then show ?rhs by simp
@@ -1673,9 +1701,19 @@
 context
 begin
 
-definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
-  where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
-    (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
+inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
+  where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
+  | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
+  | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
+      \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
+
+lemma eucl_rel_int_iff:    
+  "eucl_rel_int k l (q, r) \<longleftrightarrow> 
+    k = l * q + r \<and>
+     (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
+  by (cases "r = 0")
+    (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
+    simp add: ac_simps sgn_1_pos sgn_1_neg)
 
 lemma unique_quotient_lemma:
   "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
@@ -1694,17 +1732,17 @@
   by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
 
 lemma unique_quotient:
-  "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
-apply (simp add: divmod_int_rel_def linorder_neq_iff split: if_split_asm)
-apply (blast intro: order_antisym
-             dest: order_eq_refl [THEN unique_quotient_lemma]
-             order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
-done
+  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
+  apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
+  apply (blast intro: order_antisym
+    dest: order_eq_refl [THEN unique_quotient_lemma]
+    order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
+  done
 
 lemma unique_remainder:
-  "divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> r = r'"
+  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
 apply (subgoal_tac "q = q'")
- apply (simp add: divmod_int_rel_def)
+ apply (simp add: eucl_rel_int_iff)
 apply (blast intro: unique_quotient)
 done
 
@@ -1733,12 +1771,12 @@
       then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
       else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
 
-lemma divmod_int_rel:
-  "divmod_int_rel k l (k div l, k mod l)"
+lemma eucl_rel_int:
+  "eucl_rel_int k l (k div l, k mod l)"
 proof (cases k rule: int_cases3)
   case zero
   then show ?thesis
-    by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
+    by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
 next
   case (pos n)
   then show ?thesis
@@ -1746,7 +1784,7 @@
     by (cases l rule: int_cases3)
       (auto simp del: of_nat_mult of_nat_add
         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
+        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
 next
   case (neg n)
   then show ?thesis
@@ -1754,29 +1792,29 @@
     by (cases l rule: int_cases3)
       (auto simp del: of_nat_mult of_nat_add
         simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
+        eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
 qed
 
 lemma divmod_int_unique:
-  assumes "divmod_int_rel k l (q, r)"
+  assumes "eucl_rel_int k l (q, r)"
   shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
-  using assms divmod_int_rel [of k l]
+  using assms eucl_rel_int [of k l]
   using unique_quotient [of k l] unique_remainder [of k l]
   by auto
 
 instance proof
   fix k l :: int
   show "k div l * l + k mod l = k"
-    using divmod_int_rel [of k l]
-    unfolding divmod_int_rel_def by (simp add: ac_simps)
+    using eucl_rel_int [of k l]
+    unfolding eucl_rel_int_iff by (simp add: ac_simps)
 next
   fix k :: int show "k div 0 = 0"
-    by (rule div_int_unique, simp add: divmod_int_rel_def)
+    by (rule div_int_unique, simp add: eucl_rel_int_iff)
 next
   fix k l :: int
   assume "l \<noteq> 0"
   then show "k * l div l = k"
-    by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
+    by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
 qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
 
 end
@@ -1789,23 +1827,23 @@
 proof
   fix k l s :: int
   assume "l \<noteq> 0"
-  then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
-    using divmod_int_rel [of k l]
-    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
+  then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
+    using eucl_rel_int [of k l]
+    unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
   then show "(k + s * l) div l = s + k div l"
     by (rule div_int_unique)
 next
   fix k l s :: int
   assume "s \<noteq> 0"
-  have "\<And>q r. divmod_int_rel k l (q, r)
-    \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
-    unfolding divmod_int_rel_def
+  have "\<And>q r. eucl_rel_int k l (q, r)
+    \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
+    unfolding eucl_rel_int_iff
     by (rule linorder_cases [of 0 l])
       (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
       mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
-  then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
-    using divmod_int_rel [of k l] .
+  then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
+    using eucl_rel_int [of k l] .
   then show "(s * k) div (s * l) = k div l"
     by (rule div_int_unique)
 qed
@@ -1839,15 +1877,15 @@
   by (simp add: modulo_int_def int_dvd_iff)
 
 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
-  using divmod_int_rel [of a b]
-  by (auto simp add: divmod_int_rel_def prod_eq_iff)
+  using eucl_rel_int [of a b]
+  by (auto simp add: eucl_rel_int_iff prod_eq_iff)
 
 lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
    and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
 
 lemma neg_mod_conj: "b < (0::int) \<Longrightarrow> a mod b \<le> 0 \<and> b < a mod b"
-  using divmod_int_rel [of a b]
-  by (auto simp add: divmod_int_rel_def prod_eq_iff)
+  using eucl_rel_int [of a b]
+  by (auto simp add: eucl_rel_int_iff prod_eq_iff)
 
 lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
    and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
@@ -1857,34 +1895,34 @@
 
 lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
 apply (rule div_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
 done
 
 lemma div_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a div b = 0"
 apply (rule div_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
 done
 
 lemma div_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a div b = -1"
 apply (rule div_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
 done
 
 (*There is no div_neg_pos_trivial because  0 div b = 0 would supersede it*)
 
 lemma mod_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a mod b = a"
 apply (rule_tac q = 0 in mod_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
 done
 
 lemma mod_neg_neg_trivial: "[| a \<le> (0::int);  b < a |] ==> a mod b = a"
 apply (rule_tac q = 0 in mod_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
 done
 
 lemma mod_pos_neg_trivial: "[| (0::int) < a;  a+b \<le> 0 |] ==> a mod b = a+b"
 apply (rule_tac q = "-1" in mod_int_unique)
-apply (auto simp add: divmod_int_rel_def)
+apply (auto simp add: eucl_rel_int_iff)
 done
 
 text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
@@ -1893,22 +1931,22 @@
 subsubsection \<open>Laws for div and mod with Unary Minus\<close>
 
 lemma zminus1_lemma:
-     "divmod_int_rel a b (q, r) ==> b \<noteq> 0
-      ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,
+     "eucl_rel_int a b (q, r) ==> b \<noteq> 0
+      ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
                           if r=0 then 0 else b-r)"
-by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
+by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff right_diff_distrib)
 
 
 lemma zdiv_zminus1_eq_if:
      "b \<noteq> (0::int)
       ==> (-a) div b =
           (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-by (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN div_int_unique])
+by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
 
 lemma zmod_zminus1_eq_if:
      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
 apply (case_tac "b = 0", simp)
-apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
+apply (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
 done
 
 lemma zmod_zminus1_not_zero:
@@ -2022,27 +2060,27 @@
 text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close>
 
 lemma zmult1_lemma:
-     "[| divmod_int_rel b c (q, r) |]
-      ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
-by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left ac_simps)
+     "[| eucl_rel_int b c (q, r) |]
+      ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)"
+by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps)
 
 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
 apply (case_tac "c = 0", simp)
-apply (blast intro: divmod_int_rel [THEN zmult1_lemma, THEN div_int_unique])
+apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique])
 done
 
 text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close>
 
 lemma zadd1_lemma:
-     "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]
-      ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
-by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
+     "[| eucl_rel_int a c (aq, ar);  eucl_rel_int b c (bq, br) |]
+      ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
+by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left)
 
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma zdiv_zadd1_eq:
      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
 apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF divmod_int_rel divmod_int_rel] div_int_unique)
+apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique)
 done
 
 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
@@ -2095,9 +2133,9 @@
 apply simp
 done
 
-lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]
-      ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
-by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
+lemma zmult2_lemma: "[| eucl_rel_int a b (q, r); 0 < c |]
+      ==> eucl_rel_int a (b * c) (q div c, b*(q mod c) + r)"
+by (auto simp add: mult.assoc eucl_rel_int_iff linorder_neq_iff
                    zero_less_mult_iff distrib_left [symmetric]
                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
 
@@ -2105,14 +2143,14 @@
   fixes a b c :: int
   shows "0 \<le> c \<Longrightarrow> a div (b * c) = (a div b) div c"
 apply (case_tac "b = 0", simp)
-apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN div_int_unique])
+apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN div_int_unique])
 done
 
 lemma zmod_zmult2_eq:
   fixes a b c :: int
   shows "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
 apply (case_tac "b = 0", simp)
-apply (force simp add: le_less divmod_int_rel [THEN zmult2_lemma, THEN mod_int_unique])
+apply (force simp add: le_less eucl_rel_int [THEN zmult2_lemma, THEN mod_int_unique])
 done
 
 lemma div_pos_geq:
@@ -2199,27 +2237,27 @@
 
 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
 
-lemma pos_divmod_int_rel_mult_2:
+lemma pos_eucl_rel_int_mult_2:
   assumes "0 \<le> b"
-  assumes "divmod_int_rel a b (q, r)"
-  shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
-  using assms unfolding divmod_int_rel_def by auto
-
-lemma neg_divmod_int_rel_mult_2:
+  assumes "eucl_rel_int a b (q, r)"
+  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
+  using assms unfolding eucl_rel_int_iff by auto
+
+lemma neg_eucl_rel_int_mult_2:
   assumes "b \<le> 0"
-  assumes "divmod_int_rel (a + 1) b (q, r)"
-  shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
-  using assms unfolding divmod_int_rel_def by auto
+  assumes "eucl_rel_int (a + 1) b (q, r)"
+  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
+  using assms unfolding eucl_rel_int_iff by auto
 
 text\<open>computing div by shifting\<close>
 
 lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
-  using pos_divmod_int_rel_mult_2 [OF _ divmod_int_rel]
+  using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
   by (rule div_int_unique)
 
 lemma neg_zdiv_mult_2:
   assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
-  using neg_divmod_int_rel_mult_2 [OF A divmod_int_rel]
+  using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
   by (rule div_int_unique)
 
 (* FIXME: add rules for negative numerals *)
@@ -2240,14 +2278,14 @@
   fixes a b :: int
   assumes "0 \<le> a"
   shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
-  using pos_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
+  using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   by (rule mod_int_unique)
 
 lemma neg_zmod_mult_2:
   fixes a b :: int
   assumes "a \<le> 0"
   shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
-  using neg_divmod_int_rel_mult_2 [OF assms divmod_int_rel]
+  using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
   by (rule mod_int_unique)
 
 (* FIXME: add rules for negative numerals *)
@@ -2452,19 +2490,19 @@
 text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
 
 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
-  by (rule div_int_unique [of a b q r]) (simp add: divmod_int_rel_def)
+  by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
 
 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
   by (rule div_int_unique [of a b q r],
-    simp add: divmod_int_rel_def)
+    simp add: eucl_rel_int_iff)
 
 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
   by (rule mod_int_unique [of a b q r],
-    simp add: divmod_int_rel_def)
+    simp add: eucl_rel_int_iff)
 
 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
   by (rule mod_int_unique [of a b q r],
-    simp add: divmod_int_rel_def)
+    simp add: eucl_rel_int_iff)
 
 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
diff -r 5bd30359e46e -r 255741c5f862 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Dec 22 08:43:30 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Thu Dec 22 10:42:08 2016 +0100
@@ -1613,18 +1613,26 @@
 
 subsection \<open>Long division of polynomials\<close>
 
-definition pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
-where
-  "pdivmod_rel x y q r \<longleftrightarrow>
-    x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
-
-lemma pdivmod_rel_0:
-  "pdivmod_rel 0 y 0 0"
-  unfolding pdivmod_rel_def by simp
-
-lemma pdivmod_rel_by_0:
-  "pdivmod_rel x 0 0 x"
-  unfolding pdivmod_rel_def by simp
+inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
+  where eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
+  | eucl_rel_poly_dividesI: "y \<noteq> 0 \<Longrightarrow> x = q * y \<Longrightarrow> eucl_rel_poly x y (q, 0)"
+  | eucl_rel_poly_remainderI: "y \<noteq> 0 \<Longrightarrow> degree r < degree y
+      \<Longrightarrow> x = q * y + r \<Longrightarrow> eucl_rel_poly x y (q, r)"
+  
+lemma eucl_rel_poly_iff:
+  "eucl_rel_poly x y (q, r) \<longleftrightarrow>
+    x = q * y + r \<and>
+      (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"
+  by (auto elim: eucl_rel_poly.cases
+    intro: eucl_rel_poly_by0 eucl_rel_poly_dividesI eucl_rel_poly_remainderI)
+  
+lemma eucl_rel_poly_0:
+  "eucl_rel_poly 0 y (0, 0)"
+  unfolding eucl_rel_poly_iff by simp
+
+lemma eucl_rel_poly_by_0:
+  "eucl_rel_poly x 0 (0, x)"
+  unfolding eucl_rel_poly_iff by simp
 
 lemma eq_zero_or_degree_less:
   assumes "degree p \<le> n" and "coeff p n = 0"
@@ -1650,15 +1658,15 @@
   then show ?thesis ..
 qed
 
-lemma pdivmod_rel_pCons:
-  assumes rel: "pdivmod_rel x y q r"
+lemma eucl_rel_poly_pCons:
+  assumes rel: "eucl_rel_poly x y (q, r)"
   assumes y: "y \<noteq> 0"
   assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
-  shows "pdivmod_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
-    (is "pdivmod_rel ?x y ?q ?r")
+  shows "eucl_rel_poly (pCons a x) y (pCons b q, pCons a r - smult b y)"
+    (is "eucl_rel_poly ?x y (?q, ?r)")
 proof -
   have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
-    using assms unfolding pdivmod_rel_def by simp_all
+    using assms unfolding eucl_rel_poly_iff by simp_all
 
   have 1: "?x = ?q * y + ?r"
     using b x by simp
@@ -1678,31 +1686,31 @@
   qed
 
   from 1 2 show ?thesis
-    unfolding pdivmod_rel_def
+    unfolding eucl_rel_poly_iff
     using \<open>y \<noteq> 0\<close> by simp
 qed
 
-lemma pdivmod_rel_exists: "\<exists>q r. pdivmod_rel x y q r"
+lemma eucl_rel_poly_exists: "\<exists>q r. eucl_rel_poly x y (q, r)"
 apply (cases "y = 0")
-apply (fast intro!: pdivmod_rel_by_0)
+apply (fast intro!: eucl_rel_poly_by_0)
 apply (induct x)
-apply (fast intro!: pdivmod_rel_0)
-apply (fast intro!: pdivmod_rel_pCons)
+apply (fast intro!: eucl_rel_poly_0)
+apply (fast intro!: eucl_rel_poly_pCons)
 done
 
-lemma pdivmod_rel_unique:
-  assumes 1: "pdivmod_rel x y q1 r1"
-  assumes 2: "pdivmod_rel x y q2 r2"
+lemma eucl_rel_poly_unique:
+  assumes 1: "eucl_rel_poly x y (q1, r1)"
+  assumes 2: "eucl_rel_poly x y (q2, r2)"
   shows "q1 = q2 \<and> r1 = r2"
 proof (cases "y = 0")
   assume "y = 0" with assms show ?thesis
-    by (simp add: pdivmod_rel_def)
+    by (simp add: eucl_rel_poly_iff)
 next
   assume [simp]: "y \<noteq> 0"
   from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
-    unfolding pdivmod_rel_def by simp_all
+    unfolding eucl_rel_poly_iff by simp_all
   from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
-    unfolding pdivmod_rel_def by simp_all
+    unfolding eucl_rel_poly_iff by simp_all
   from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
     by (simp add: algebra_simps)
   from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
@@ -1723,15 +1731,15 @@
   qed
 qed
 
-lemma pdivmod_rel_0_iff: "pdivmod_rel 0 y q r \<longleftrightarrow> q = 0 \<and> r = 0"
-by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_0)
-
-lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
-by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
-
-lemmas pdivmod_rel_unique_div = pdivmod_rel_unique [THEN conjunct1]
-
-lemmas pdivmod_rel_unique_mod = pdivmod_rel_unique [THEN conjunct2]
+lemma eucl_rel_poly_0_iff: "eucl_rel_poly 0 y (q, r) \<longleftrightarrow> q = 0 \<and> r = 0"
+by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_0)
+
+lemma eucl_rel_poly_by_0_iff: "eucl_rel_poly x 0 (q, r) \<longleftrightarrow> q = 0 \<and> r = x"
+by (auto dest: eucl_rel_poly_unique intro: eucl_rel_poly_by_0)
+
+lemmas eucl_rel_poly_unique_div = eucl_rel_poly_unique [THEN conjunct1]
+
+lemmas eucl_rel_poly_unique_mod = eucl_rel_poly_unique [THEN conjunct2]
 
 
 
@@ -2236,8 +2244,8 @@
     if g = 0 then f
     else pseudo_mod (smult ((1/coeff g (degree g)) ^ (Suc (degree f) - degree g)) f) g"
 
-lemma pdivmod_rel: "pdivmod_rel (x::'a::field poly) y (x div y) (x mod y)"
-  unfolding pdivmod_rel_def
+lemma eucl_rel_poly: "eucl_rel_poly (x::'a::field poly) y (x div y, x mod y)"
+  unfolding eucl_rel_poly_iff
 proof (intro conjI)
   show "x = x div y * y + x mod y"
   proof(cases "y = 0")
@@ -2261,24 +2269,24 @@
 qed
 
 lemma div_poly_eq:
-  "pdivmod_rel (x::'a::field poly) y q r \<Longrightarrow> x div y = q"
-  by(rule pdivmod_rel_unique_div[OF pdivmod_rel])
+  "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x div y = q"
+  by(rule eucl_rel_poly_unique_div[OF eucl_rel_poly])
 
 lemma mod_poly_eq:
-  "pdivmod_rel (x::'a::field poly) y q r \<Longrightarrow> x mod y = r"
-  by (rule pdivmod_rel_unique_mod[OF pdivmod_rel])
+  "eucl_rel_poly (x::'a::field poly) y (q, r) \<Longrightarrow> x mod y = r"
+  by (rule eucl_rel_poly_unique_mod[OF eucl_rel_poly])
 
 instance
 proof
   fix x y :: "'a poly"
-  from pdivmod_rel[of x y,unfolded pdivmod_rel_def]
+  from eucl_rel_poly[of x y,unfolded eucl_rel_poly_iff]
   show "x div y * y + x mod y = x" by auto
 next
   fix x y z :: "'a poly"
   assume "y \<noteq> 0"
-  hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
-    using pdivmod_rel [of x y]
-    by (simp add: pdivmod_rel_def distrib_right)
+  hence "eucl_rel_poly (x + z * y) y (z + x div y, x mod y)"
+    using eucl_rel_poly [of x y]
+    by (simp add: eucl_rel_poly_iff distrib_right)
   thus "(x + z * y) div y = z + x div y"
     by (rule div_poly_eq)
 next
@@ -2286,23 +2294,23 @@
   assume "x \<noteq> 0"
   show "(x * y) div (x * z) = y div z"
   proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
-    have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
-      by (rule pdivmod_rel_by_0)
+    have "\<And>x::'a poly. eucl_rel_poly x 0 (0, x)"
+      by (rule eucl_rel_poly_by_0)
     then have [simp]: "\<And>x::'a poly. x div 0 = 0"
       by (rule div_poly_eq)
-    have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
-      by (rule pdivmod_rel_0)
+    have "\<And>x::'a poly. eucl_rel_poly 0 x (0, 0)"
+      by (rule eucl_rel_poly_0)
     then have [simp]: "\<And>x::'a poly. 0 div x = 0"
       by (rule div_poly_eq)
     case False then show ?thesis by auto
   next
     case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
     with \<open>x \<noteq> 0\<close>
-    have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
-      by (auto simp add: pdivmod_rel_def algebra_simps)
+    have "\<And>q r. eucl_rel_poly y z (q, r) \<Longrightarrow> eucl_rel_poly (x * y) (x * z) (q, x * r)"
+      by (auto simp add: eucl_rel_poly_iff algebra_simps)
         (rule classical, simp add: degree_mult_eq)
-    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
-    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
+    moreover from eucl_rel_poly have "eucl_rel_poly y z (y div z, y mod z)" .
+    ultimately have "eucl_rel_poly (x * y) (x * z) (y div z, x * (y mod z))" .
     then show ?thesis by (simp add: div_poly_eq)
   qed
 qed
@@ -2311,35 +2319,35 @@
 
 lemma degree_mod_less:
   "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
-  using pdivmod_rel [of x y]
-  unfolding pdivmod_rel_def by simp
+  using eucl_rel_poly [of x y]
+  unfolding eucl_rel_poly_iff by simp
 
 lemma div_poly_less: "degree (x::'a::field poly) < degree y \<Longrightarrow> x div y = 0"
 proof -
   assume "degree x < degree y"
-  hence "pdivmod_rel x y 0 x"
-    by (simp add: pdivmod_rel_def)
+  hence "eucl_rel_poly x y (0, x)"
+    by (simp add: eucl_rel_poly_iff)
   thus "x div y = 0" by (rule div_poly_eq)
 qed
 
 lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
 proof -
   assume "degree x < degree y"
-  hence "pdivmod_rel x y 0 x"
-    by (simp add: pdivmod_rel_def)
+  hence "eucl_rel_poly x y (0, x)"
+    by (simp add: eucl_rel_poly_iff)
   thus "x mod y = x" by (rule mod_poly_eq)
 qed
 
-lemma pdivmod_rel_smult_left:
-  "pdivmod_rel x y q r
-    \<Longrightarrow> pdivmod_rel (smult a x) y (smult a q) (smult a r)"
-  unfolding pdivmod_rel_def by (simp add: smult_add_right)
+lemma eucl_rel_poly_smult_left:
+  "eucl_rel_poly x y (q, r)
+    \<Longrightarrow> eucl_rel_poly (smult a x) y (smult a q, smult a r)"
+  unfolding eucl_rel_poly_iff by (simp add: smult_add_right)
 
 lemma div_smult_left: "(smult (a::'a::field) x) div y = smult a (x div y)"
-  by (rule div_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
+  by (rule div_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
 
 lemma mod_smult_left: "(smult a x) mod y = smult a (x mod y)"
-  by (rule mod_poly_eq, rule pdivmod_rel_smult_left, rule pdivmod_rel)
+  by (rule mod_poly_eq, rule eucl_rel_poly_smult_left, rule eucl_rel_poly)
 
 lemma poly_div_minus_left [simp]:
   fixes x y :: "'a::field poly"
@@ -2351,23 +2359,23 @@
   shows "(- x) mod y = - (x mod y)"
   using mod_smult_left [of "- 1::'a"] by simp
 
-lemma pdivmod_rel_add_left:
-  assumes "pdivmod_rel x y q r"
-  assumes "pdivmod_rel x' y q' r'"
-  shows "pdivmod_rel (x + x') y (q + q') (r + r')"
-  using assms unfolding pdivmod_rel_def
+lemma eucl_rel_poly_add_left:
+  assumes "eucl_rel_poly x y (q, r)"
+  assumes "eucl_rel_poly x' y (q', r')"
+  shows "eucl_rel_poly (x + x') y (q + q', r + r')"
+  using assms unfolding eucl_rel_poly_iff
   by (auto simp add: algebra_simps degree_add_less)
 
 lemma poly_div_add_left:
   fixes x y z :: "'a::field poly"
   shows "(x + y) div z = x div z + y div z"
-  using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
+  using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
   by (rule div_poly_eq)
 
 lemma poly_mod_add_left:
   fixes x y z :: "'a::field poly"
   shows "(x + y) mod z = x mod z + y mod z"
-  using pdivmod_rel_add_left [OF pdivmod_rel pdivmod_rel]
+  using eucl_rel_poly_add_left [OF eucl_rel_poly eucl_rel_poly]
   by (rule mod_poly_eq)
 
 lemma poly_div_diff_left:
@@ -2380,17 +2388,17 @@
   shows "(x - y) mod z = x mod z - y mod z"
   by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
 
-lemma pdivmod_rel_smult_right:
-  "\<lbrakk>a \<noteq> 0; pdivmod_rel x y q r\<rbrakk>
-    \<Longrightarrow> pdivmod_rel x (smult a y) (smult (inverse a) q) r"
-  unfolding pdivmod_rel_def by simp
+lemma eucl_rel_poly_smult_right:
+  "a \<noteq> 0 \<Longrightarrow> eucl_rel_poly x y (q, r)
+    \<Longrightarrow> eucl_rel_poly x (smult a y) (smult (inverse a) q, r)"
+  unfolding eucl_rel_poly_iff by simp
 
 lemma div_smult_right:
   "(a::'a::field) \<noteq> 0 \<Longrightarrow> x div (smult a y) = smult (inverse a) (x div y)"
-  by (rule div_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
+  by (rule div_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
 
 lemma mod_smult_right: "a \<noteq> 0 \<Longrightarrow> x mod (smult a y) = x mod y"
-  by (rule mod_poly_eq, erule pdivmod_rel_smult_right, rule pdivmod_rel)
+  by (rule mod_poly_eq, erule eucl_rel_poly_smult_right, rule eucl_rel_poly)
 
 lemma poly_div_minus_right [simp]:
   fixes x y :: "'a::field poly"
@@ -2402,30 +2410,30 @@
   shows "x mod (- y) = x mod y"
   using mod_smult_right [of "- 1::'a"] by simp
 
-lemma pdivmod_rel_mult:
-  "\<lbrakk>pdivmod_rel x y q r; pdivmod_rel q z q' r'\<rbrakk>
-    \<Longrightarrow> pdivmod_rel x (y * z) q' (y * r' + r)"
-apply (cases "z = 0", simp add: pdivmod_rel_def)
-apply (cases "y = 0", simp add: pdivmod_rel_by_0_iff pdivmod_rel_0_iff)
+lemma eucl_rel_poly_mult:
+  "eucl_rel_poly x y (q, r) \<Longrightarrow> eucl_rel_poly q z (q', r')
+    \<Longrightarrow> eucl_rel_poly x (y * z) (q', y * r' + r)"
+apply (cases "z = 0", simp add: eucl_rel_poly_iff)
+apply (cases "y = 0", simp add: eucl_rel_poly_by_0_iff eucl_rel_poly_0_iff)
 apply (cases "r = 0")
 apply (cases "r' = 0")
-apply (simp add: pdivmod_rel_def)
-apply (simp add: pdivmod_rel_def field_simps degree_mult_eq)
+apply (simp add: eucl_rel_poly_iff)
+apply (simp add: eucl_rel_poly_iff field_simps degree_mult_eq)
 apply (cases "r' = 0")
-apply (simp add: pdivmod_rel_def degree_mult_eq)
-apply (simp add: pdivmod_rel_def field_simps)
+apply (simp add: eucl_rel_poly_iff degree_mult_eq)
+apply (simp add: eucl_rel_poly_iff field_simps)
 apply (simp add: degree_mult_eq degree_add_less)
 done
 
 lemma poly_div_mult_right:
   fixes x y z :: "'a::field poly"
   shows "x div (y * z) = (x div y) div z"
-  by (rule div_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
+  by (rule div_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
 
 lemma poly_mod_mult_right:
   fixes x y z :: "'a::field poly"
   shows "x mod (y * z) = y * (x div y mod z) + x mod y"
-  by (rule mod_poly_eq, rule pdivmod_rel_mult, (rule pdivmod_rel)+)
+  by (rule mod_poly_eq, rule eucl_rel_poly_mult, (rule eucl_rel_poly)+)
 
 lemma mod_pCons:
   fixes a and x
@@ -2434,7 +2442,7 @@
   shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
 unfolding b
 apply (rule mod_poly_eq)
-apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl])
+apply (rule eucl_rel_poly_pCons [OF eucl_rel_poly y refl])
 done
 
 definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly"
@@ -2453,9 +2461,9 @@
         in (pCons b s, pCons a r - smult b q)))"
   apply (simp add: pdivmod_def Let_def, safe)
   apply (rule div_poly_eq)
-  apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
+  apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
   apply (rule mod_poly_eq)
-  apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
+  apply (erule eucl_rel_poly_pCons [OF eucl_rel_poly _ refl])
   done
 
 lemma pdivmod_fold_coeffs:
@@ -2700,8 +2708,8 @@
 (* *************** *)
 subsubsection \<open>Improved Code-Equations for Polynomial (Pseudo) Division\<close>
 
-lemma pdivmod_pdivmodrel: "pdivmod_rel p q r s = (pdivmod p q = (r, s))"
-  by (metis pdivmod_def pdivmod_rel pdivmod_rel_unique prod.sel)
+lemma pdivmod_pdivmodrel: "eucl_rel_poly p q (r, s) \<longleftrightarrow> pdivmod p q = (r, s)"
+  by (metis pdivmod_def eucl_rel_poly eucl_rel_poly_unique)
 
 lemma pdivmod_via_pseudo_divmod: "pdivmod f g = (if g = 0 then (0,f) 
      else let 
@@ -2720,7 +2728,7 @@
     unfolding Let_def h_def[symmetric] lc_def[symmetric] p by auto
   from pseudo_divmod[OF h0 p, unfolded h1] 
   have f: "f = h * q + r" and r: "r = 0 \<or> degree r < degree h" by auto
-  have "pdivmod_rel f h q r" unfolding pdivmod_rel_def using f r h0 by auto
+  have "eucl_rel_poly f h (q, r)" unfolding eucl_rel_poly_iff using f r h0 by auto
   hence "pdivmod f h = (q,r)" by (simp add: pdivmod_pdivmodrel)
   hence "pdivmod f g = (smult lc q, r)" 
     unfolding pdivmod_def h_def div_smult_right[OF lc] mod_smult_right[OF lc]