# HG changeset patch
# User haftmann
# Date 1663072237 0
# Node ID e7497a1de8b97eb9ac888a5120fa9915d01cb68f
# Parent  19837257fd895a68be454b56b3041451f70cd890
more concise instance-specific rules on euclidean relation

diff -r 19837257fd89 -r e7497a1de8b9 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Sep 13 18:56:48 2022 +0100
+++ b/src/HOL/Divides.thy	Tue Sep 13 12:30:37 2022 +0000
@@ -262,8 +262,8 @@
       \<open>a mod b = r\<close> (is ?R)
 proof -
   from assms have \<open>(a div b, a mod b) = (q, r)\<close>
-    by (cases b q r a rule: euclidean_relationI)
-      (auto simp add: division_segment_int_def ac_simps dvd_add_left_iff dest: zdvd_imp_le)
+    by (cases b q r a rule: euclidean_relation_intI)
+      (auto simp add: ac_simps dvd_add_left_iff sgn_1_pos le_less dest: zdvd_imp_le)
   then show ?Q and ?R
     by simp_all
 qed
@@ -400,34 +400,6 @@
 qed
 
 
-subsubsection \<open>Uniqueness rules\<close>
-
-lemma euclidean_relation_intI [case_names by0 divides euclidean_relation]:
-  \<open>(k div l, k mod l) = (q, r)\<close>
-    if by0': \<open>l = 0 \<Longrightarrow> q = 0 \<and> r = k\<close>
-    and divides': \<open>l \<noteq> 0 \<Longrightarrow> l dvd k \<Longrightarrow> r = 0 \<and> k = q * l\<close>
-    and euclidean_relation': \<open>l \<noteq> 0 \<Longrightarrow> \<not> l dvd k \<Longrightarrow> sgn r = sgn l
-      \<and> \<bar>r\<bar> < \<bar>l\<bar> \<and> k = q * l + r\<close> for k l :: int
-proof (cases l q r k rule: euclidean_relationI)
-  case by0
-  then show ?case
-    by (rule by0')
-next
-  case divides
-  then show ?case
-    by (rule divides')
-next
-  case euclidean_relation
-  with euclidean_relation' have \<open>sgn r = sgn l\<close> \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
-    by simp_all
-  from \<open>sgn r = sgn l\<close> \<open>l \<noteq> 0\<close> have \<open>division_segment r = division_segment l\<close>
-    by (simp add: division_segment_int_def sgn_if split: if_splits)
-  with \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
-  show ?case
-    by simp
-qed
-
-
 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
 
 lemma div_pos_geq:
diff -r 19837257fd89 -r e7497a1de8b9 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Tue Sep 13 18:56:48 2022 +0100
+++ b/src/HOL/Euclidean_Division.thy	Tue Sep 13 12:30:37 2022 +0000
@@ -967,20 +967,27 @@
 
 end
 
+lemma euclidean_relation_natI [case_names by0 divides euclidean_relation]:
+  \<open>(m div n, m mod n) = (q, r)\<close>
+    if by0: \<open>n = 0 \<Longrightarrow> q = 0 \<and> r = m\<close>
+    and divides: \<open>n > 0 \<Longrightarrow> n dvd m \<Longrightarrow> r = 0 \<and> m = q * n\<close>
+    and euclidean_relation: \<open>n > 0 \<Longrightarrow> \<not> n dvd m \<Longrightarrow> r < n \<and> m = q * n + r\<close> for m n q r :: nat
+  by (rule euclidean_relationI) (use that in simp_all)
+
 lemma div_nat_eqI:
   \<open>m div n = q\<close> if \<open>n * q \<le> m\<close> and \<open>m < n * Suc q\<close> for m n q :: nat
 proof -
   have \<open>(m div n, m mod n) = (q, m - n * q)\<close>
-  proof (cases n q \<open>m - n * q\<close>  m rule: euclidean_relationI)
+  proof (cases n q \<open>m - n * q\<close>  m rule: euclidean_relation_natI)
     case by0
     with that show ?case
       by simp
   next
     case divides
     from \<open>n dvd m\<close> obtain s where \<open>m = n * s\<close> ..
-    with \<open>n \<noteq> 0\<close> that have \<open>s < Suc q\<close>
+    with \<open>n > 0\<close> that have \<open>s < Suc q\<close>
       by (simp only: mult_less_cancel1)
-    with \<open>m = n * s\<close> \<open>n \<noteq> 0\<close> that have \<open>q = s\<close>
+    with \<open>m = n * s\<close> \<open>n > 0\<close> that have \<open>q = s\<close>
       by simp
     with \<open>m = n * s\<close> show ?case
       by (simp add: ac_simps)
@@ -997,7 +1004,7 @@
   \<open>m mod n = r\<close> if \<open>r < n\<close> and \<open>r \<le> m\<close> and \<open>n dvd m - r\<close> for m n r :: nat
 proof -
   have \<open>(m div n, m mod n) = ((m - r) div n, r)\<close>
-  proof (cases n \<open>(m - r) div n\<close> r  m rule: euclidean_relationI)
+  proof (cases n \<open>(m - r) div n\<close> r  m rule: euclidean_relation_natI)
     case by0
     with that show ?case
       by simp
@@ -1010,9 +1017,9 @@
       by (simp add: dvd_add_right_iff)
     then have \<open>n \<le> n - r\<close>
       by (rule dvd_imp_le) (use \<open>r < n\<close> in simp)
-    with \<open>n \<noteq> 0\<close> have \<open>r = 0\<close>
+    with \<open>n > 0\<close> have \<open>r = 0\<close>
       by simp
-    with \<open>n \<noteq> 0\<close> that show ?case
+    with \<open>n > 0\<close> that show ?case
       by simp
   next
     case euclidean_relation
@@ -1261,14 +1268,14 @@
   for m n q :: nat
 proof -
   have \<open>(m div (n * q), m mod (n * q)) = ((m div n) div q, n * (m div n mod q) + m mod n)\<close>
-  proof (cases \<open>n * q\<close> \<open>(m div n) div q\<close> \<open>n * (m div n mod q) + m mod n\<close> m rule: euclidean_relationI)
+  proof (cases \<open>n * q\<close> \<open>(m div n) div q\<close> \<open>n * (m div n mod q) + m mod n\<close> m rule: euclidean_relation_natI)
     case by0
     then show ?case
       by auto
   next
     case divides
     from \<open>n * q dvd m\<close> obtain t where \<open>m = n * q * t\<close> ..
-    with \<open>n * q \<noteq> 0\<close> show ?case
+    with \<open>n * q > 0\<close> show ?case
       by (simp add: algebra_simps)
   next
     case euclidean_relation
@@ -1812,6 +1819,31 @@
 
 end
 
+lemma euclidean_relation_intI [case_names by0 divides euclidean_relation]:
+  \<open>(k div l, k mod l) = (q, r)\<close>
+    if by0': \<open>l = 0 \<Longrightarrow> q = 0 \<and> r = k\<close>
+    and divides': \<open>l \<noteq> 0 \<Longrightarrow> l dvd k \<Longrightarrow> r = 0 \<and> k = q * l\<close>
+    and euclidean_relation': \<open>l \<noteq> 0 \<Longrightarrow> \<not> l dvd k \<Longrightarrow> sgn r = sgn l
+      \<and> \<bar>r\<bar> < \<bar>l\<bar> \<and> k = q * l + r\<close> for k l :: int
+proof (cases l q r k rule: euclidean_relationI)
+  case by0
+  then show ?case
+    by (rule by0')
+next
+  case divides
+  then show ?case
+    by (rule divides')
+next
+  case euclidean_relation
+  with euclidean_relation' have \<open>sgn r = sgn l\<close> \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
+    by simp_all
+  from \<open>sgn r = sgn l\<close> \<open>l \<noteq> 0\<close> have \<open>division_segment r = division_segment l\<close>
+    by (simp add: division_segment_int_def sgn_if split: if_splits)
+  with \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
+  show ?case
+    by simp
+qed
+
 
 subsection \<open>Special case: euclidean rings containing the natural numbers\<close>