--- 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
--- 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