src/HOL/Divides.thy

   with \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
   show ?case
     by simp
 qed
 
-lemma euclidean_relation_intI' [case_names by0 pos neg]:
-  \<open>(k div l, k mod l) = (q, r)\<close>
-    if \<open>l = 0 \<Longrightarrow> q = 0 \<and> r = k\<close>
-    and \<open>l > 0 \<Longrightarrow> 0 \<le> r \<and> r < l \<and> k = q * l + r\<close>
-    and \<open>l < 0 \<Longrightarrow> l < r \<and> r \<le> 0 \<and> k = q * l + r\<close> for k l q r :: int
-  by (cases l \<open>0::int\<close> rule: linorder_cases)
-    (auto dest: that)
-
 
 subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
 
 lemma div_pos_geq:
   fixes k l :: int

 lemma pos_zdiv_mult_2: \<open>(1 + 2 * b) div (2 * a) = b div a\<close> (is ?Q)
   and pos_zmod_mult_2: \<open>(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)\<close> (is ?R)
   if \<open>0 \<le> a\<close> for a b :: int
 proof -
   have \<open>((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = (b div a, 1 + 2 * (b mod a))\<close>
-  proof (cases \<open>2 * a\<close> \<open>b div a\<close> \<open>1 + 2 * (b mod a)\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI')
+  proof (cases \<open>2 * a\<close> \<open>b div a\<close> \<open>1 + 2 * (b mod a)\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI)
     case by0
     then show ?case
       by simp
   next
-    case pos
-    then have \<open>a > 0\<close>
+    case divides
+    have \<open>even (2 * a)\<close>
+      by simp
+    then have \<open>even (1 + 2 * b)\<close>
+      using \<open>2 * a dvd 1 + 2 * b\<close> by (rule dvd_trans)
+    then show ?case
+      by simp
+  next
+    case euclidean_relation
+    with that have \<open>a > 0\<close>
       by simp
     moreover have \<open>b mod a < a\<close>
       using \<open>a > 0\<close> by simp
     then have \<open>1 + 2 * (b mod a) < 2 * a\<close>
       by simp
     moreover have \<open>2 * (b mod a) + a * (2 * (b div a)) = 2 * (b div a * a + b mod a)\<close>
       by (simp only: algebra_simps)
+    moreover have \<open>0 \<le> 2 * (b mod a)\<close>
+      using \<open>a > 0\<close> by simp
     ultimately show ?case
       by (simp add: algebra_simps)
-  next
-    case neg
-    with that show ?case
-      by simp
   qed
   then show ?Q and ?R
     by simp_all
 qed
 
 lemma neg_zdiv_mult_2: \<open>(1 + 2 * b) div (2 * a) = (b + 1) div a\<close> (is ?Q)
   and neg_zmod_mult_2: \<open>(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1\<close> (is ?R)
   if \<open>a \<le> 0\<close> for a b :: int
 proof -
   have \<open>((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = ((b + 1) div a, 2 * ((b + 1) mod a) - 1)\<close>
-  proof (cases \<open>2 * a\<close> \<open>(b + 1) div a\<close> \<open>2 * ((b + 1) mod a) - 1\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI')
+  proof (cases \<open>2 * a\<close> \<open>(b + 1) div a\<close> \<open>2 * ((b + 1) mod a) - 1\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI)
     case by0
     then show ?case
       by simp
   next
-    case pos
-    with that show ?case
+    case divides
+    have \<open>even (2 * a)\<close>
+      by simp
+    then have \<open>even (1 + 2 * b)\<close>
+      using \<open>2 * a dvd 1 + 2 * b\<close> by (rule dvd_trans)
+    then show ?case
       by simp
   next
-    case neg
-    then have \<open>a < 0\<close>
+    case euclidean_relation
+    with that have \<open>a < 0\<close>
       by simp
     moreover have \<open>(b + 1) mod a > a\<close>
       using \<open>a < 0\<close> by simp
     then have \<open>2 * ((b + 1) mod a) > 1 + 2 * a\<close>
       by simp

       by simp
     moreover have \<open>2 * ((1 + b) mod a) + a * (2 * ((1 + b) div a)) =
       2 * ((1 + b) div a * a + (1 + b) mod a)\<close>
       by (simp only: algebra_simps)
     ultimately show ?case
-      by (simp add: algebra_simps)
+      by (simp add: algebra_simps sgn_mult abs_mult)
   qed
   then show ?Q and ?R
     by simp_all
 qed