# HG changeset patch
# User haftmann
# Date 1664874754 0
# Node ID 4111c94657b4fc5404bf01c18be57750ea789c9f
# Parent  6ab4bb7cb8b2cb6d85c564b75fa29cef0aace417
slightly less abusive proof pattern

diff -r 6ab4bb7cb8b2 -r 4111c94657b4 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 02 18:22:49 2022 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Tue Oct 04 09:12:34 2022 +0000
@@ -3985,9 +3985,9 @@
       by simp
   next
     case False
-    then show ?thesis
-      by (cases y \<open>smult a (x div y)\<close> \<open>smult a (x mod y)\<close> \<open>smult a x\<close> rule: euclidean_relation_polyI)
-        (simp_all add: dvd_smult_iff degree_mod_less_degree flip: smult_add_right)
+    show ?thesis
+      by (rule euclidean_relation_polyI)
+        (use False in \<open>simp_all add: dvd_smult_iff degree_mod_less_degree flip: smult_add_right\<close>)
   qed
   then show ?Q and ?R
     by simp_all
@@ -4006,7 +4006,7 @@
   for x y z :: \<open>'a::field poly\<close>
 proof -
   have \<open>((x + y) div z, (x + y) mod z) = (x div z + y div z, x mod z + y mod z)\<close>
-  proof (cases z \<open>x div z + y div z\<close> \<open>x mod z + y mod z\<close> \<open>x + y\<close> rule: euclidean_relation_polyI)
+  proof (induction rule: euclidean_relation_polyI)
     case by0
     then show ?case by simp
   next
@@ -4045,7 +4045,7 @@
   and mod_smult_right: \<open>x mod smult a y = (if a = 0 then x else x mod y)\<close> (is ?R)
 proof -
   have \<open>(x div smult a y, x mod smult a y) = (smult (inverse a) (x div y), (if a = 0 then x else x mod y))\<close>
-  proof (cases \<open>smult a y\<close> \<open>smult (inverse a) (x div y)\<close> \<open>(if a = 0 then x else x mod y)\<close> x rule: euclidean_relation_polyI)
+  proof (induction rule: euclidean_relation_polyI)
     case by0
     then show ?case by auto
   next
@@ -4077,7 +4077,7 @@
   for x y z :: \<open>'a::field poly\<close>
 proof -
   have \<open>(x div (y * z), x mod (y * z)) = ((x div y) div z, y * (x div y mod z) + x mod y)\<close>
-  proof (cases \<open>y * z\<close> \<open>(x div y) div z\<close> \<open>y * (x div y mod z) + x mod y\<close> x rule: euclidean_relation_polyI)
+  proof (induction rule: euclidean_relation_polyI)
     case by0
     then show ?case by auto
   next
@@ -4143,7 +4143,7 @@
     define b where \<open>b = coeff (pCons a (p mod q)) (degree q) / lead_coeff q\<close>
     have \<open>(pCons a p div q, pCons a p mod q) =
       (pCons b (p div q), (pCons a (p mod q) - smult b q))\<close> (is \<open>_ = (?q, ?r)\<close>)
-    proof (cases q ?q ?r \<open>pCons a p\<close> rule: euclidean_relation_polyI)
+    proof (induction rule: euclidean_relation_polyI)
       case by0
       with \<open>q \<noteq> 0\<close> show ?case by simp
     next
diff -r 6ab4bb7cb8b2 -r 4111c94657b4 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sun Oct 02 18:22:49 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy	Tue Oct 04 09:12:34 2022 +0000
@@ -672,7 +672,7 @@
   fix a b c
   assume \<open>b \<noteq> 0\<close>
   have \<open>((a + c * b) div b, (a + c * b) mod b) = (c + a div b, a mod b)\<close>
-  proof (cases b \<open>c + a div b\<close> \<open>a mod b\<close> \<open>a + c * b\<close> rule: euclidean_relationI)
+  proof (induction rule: euclidean_relationI)
     case by0
     with \<open>b \<noteq> 0\<close>
     show ?case
@@ -698,7 +698,7 @@
   fix a b c
   assume \<open>c \<noteq> 0\<close>
   have \<open>((c * a) div (c * b), (c * a) mod (c * b)) = (a div b, c * (a mod b))\<close>
-  proof (cases \<open>c * b\<close> \<open>a div b\<close> \<open>c * (a mod b)\<close> \<open>c * a\<close> rule: euclidean_relationI)
+  proof (induction rule: euclidean_relationI)
     case by0
     with \<open>c \<noteq> 0\<close> show ?case
       by simp
@@ -745,7 +745,7 @@
   next
     assume \<open>euclidean_size a < euclidean_size b\<close>
     have \<open>(a div b, a mod b) = (0, a)\<close>
-    proof (cases b 0 a a rule: euclidean_relationI)
+    proof (induction rule: euclidean_relationI)
       case by0
       show ?case
         by simp
@@ -783,7 +783,7 @@
       by (simp add: algebra_simps)
   qed
   have \<open>((a * b) div c, (a * b) mod c) = (a * (b div c) + a * (b mod c) div c, (a * b) mod c)\<close>
-  proof (cases c \<open>a * (b div c) + a * (b mod c) div c\<close> \<open>(a * b) mod c\<close> \<open>a * b\<close> rule: euclidean_relationI)
+  proof (induction rule: euclidean_relationI)
     case by0
     then show ?case by simp
   next
@@ -817,7 +817,7 @@
       by (simp add: mod_mult_div_eq)
   qed
   have \<open>((a + b) div c, (a + b) mod c) = (a div c + b div c + (a mod c + b mod c) div c, (a + b) mod c)\<close>
-  proof (cases c \<open>a div c + b div c + (a mod c + b mod c) div c\<close> \<open>(a + b) mod c\<close> \<open>a + b\<close> rule: euclidean_relationI)
+  proof (induction rule: euclidean_relationI)
     case by0
     then show ?case
       by simp
@@ -978,7 +978,7 @@
   \<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_relation_natI)
+  proof (induction rule: euclidean_relation_natI)
     case by0
     with that show ?case
       by simp
@@ -1004,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_relation_natI)
+  proof (induction rule: euclidean_relation_natI)
     case by0
     with that show ?case
       by simp
@@ -1268,7 +1268,7 @@
   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_relation_natI)
+  proof (induction rule: euclidean_relation_natI)
     case by0
     then show ?case
       by auto
@@ -1948,7 +1948,7 @@
     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)
+proof (induction rule: euclidean_relationI)
   case by0
   then show ?case
     by (rule by0')
@@ -2274,7 +2274,7 @@
   from that have \<open>l < 0\<close>
     by simp
   have \<open>(k div l, k mod l) = (- 1, k + l)\<close>
-  proof (cases l \<open>- 1 :: int\<close> \<open>k + l\<close> k rule: euclidean_relation_intI)
+  proof (induction rule: euclidean_relation_intI)
     case by0
     with \<open>l < 0\<close> show ?case
       by simp
@@ -2316,9 +2316,9 @@
     and int_mod_pos_eq:
       \<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_relation_intI)
-      (auto simp add: ac_simps dvd_add_left_iff sgn_1_pos le_less dest: zdvd_imp_le)
+  have \<open>(a div b, a mod b) = (q, r)\<close>
+    by (induction rule: euclidean_relation_intI)
+      (use assms in \<open>auto simp add: ac_simps dvd_add_left_iff sgn_1_pos le_less dest: zdvd_imp_le\<close>)
   then show ?Q and ?R
     by simp_all
 qed
@@ -2868,7 +2868,7 @@
   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 (induction rule: euclidean_relation_intI)
     case by0
     then show ?case
       by simp
@@ -2908,7 +2908,7 @@
   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 (induction rule: euclidean_relation_intI)
     case by0
     then show ?case
       by simp