# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1610131930 -3600
# Node ID 783406dd051ed851c09621f093d793aba3e5f96f
# Parent  981a383610df89c6a9b0c8605e92785f7ff9c217
some algebra material for HOL: characteristic of a ring, algebraic integers

diff -r 981a383610df -r 783406dd051e src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Fri Jan 08 19:53:44 2021 +0100
+++ b/src/HOL/Complex.thy	Fri Jan 08 19:52:10 2021 +0100
@@ -586,6 +586,12 @@
 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * \<i>"
   by (simp add: complex_eq_iff)
 
+lemma Ints_cnj [intro]: "x \<in> \<int> \<Longrightarrow> cnj x \<in> \<int>"
+  by (auto elim!: Ints_cases)
+
+lemma cnj_in_Ints_iff [simp]: "cnj x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
+  using Ints_cnj[of x] Ints_cnj[of "cnj x"] by auto
+
 lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
   by (simp add: complex_eq_iff power2_eq_square)
 
diff -r 981a383610df -r 783406dd051e src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Jan 08 19:53:44 2021 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Jan 08 19:52:10 2021 +0100
@@ -1389,6 +1389,14 @@
   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum)
 
+lemma degree_prod_eq_sum_degree:
+  fixes A :: "'a set"
+  and f :: "'a \<Rightarrow> 'b::idom poly"
+  assumes f0: "\<forall>i\<in>A. f i \<noteq> 0"
+  shows "degree (\<Prod>i\<in>A. (f i)) = (\<Sum>i\<in>A. degree (f i))"
+  using assms
+  by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq)
+
 lemma degree_mult_eq_0:
   "degree (p * q) = 0 \<longleftrightarrow> p = 0 \<or> q = 0 \<or> (p \<noteq> 0 \<and> q \<noteq> 0 \<and> degree p = 0 \<and> degree q = 0)"
   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
@@ -1454,6 +1462,10 @@
   for p q :: "'a::{comm_semiring_0, semiring_no_zero_divisors} poly"
   by (cases "p = 0 \<or> q = 0") (auto simp: coeff_mult_degree_sum degree_mult_eq)
 
+lemma lead_coeff_prod: "lead_coeff (prod f A) = (\<Prod>x\<in>A. lead_coeff (f x))"
+  for f :: "'a \<Rightarrow> 'b::{comm_semiring_1, semiring_no_zero_divisors} poly"
+  by (induction A rule: infinite_finite_induct) (auto simp: lead_coeff_mult)
+
 lemma lead_coeff_smult: "lead_coeff (smult c p) = c * lead_coeff p"
   for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
 proof -
@@ -2147,6 +2159,46 @@
 qed
 
 
+subsection \<open>Closure properties of coefficients\<close>
+
+
+context
+  fixes R :: "'a :: comm_semiring_1 set"
+  assumes R_0: "0 \<in> R"
+  assumes R_plus: "\<And>x y. x \<in> R \<Longrightarrow> y \<in> R \<Longrightarrow> x + y \<in> R"
+  assumes R_mult: "\<And>x y. x \<in> R \<Longrightarrow> y \<in> R \<Longrightarrow> x * y \<in> R"
+begin
+
+lemma coeff_mult_semiring_closed:
+  assumes "\<And>i. coeff p i \<in> R" "\<And>i. coeff q i \<in> R"
+  shows   "coeff (p * q) i \<in> R"
+proof -
+  have R_sum: "sum f A \<in> R" if "\<And>x. x \<in> A \<Longrightarrow> f x \<in> R" for A and f :: "nat \<Rightarrow> 'a"
+    using that by (induction A rule: infinite_finite_induct) (auto intro: R_0 R_plus)
+  show ?thesis
+    unfolding coeff_mult by (auto intro!: R_sum R_mult assms)
+qed
+
+lemma coeff_pcompose_semiring_closed:
+  assumes "\<And>i. coeff p i \<in> R" "\<And>i. coeff q i \<in> R"
+  shows   "coeff (pcompose p q) i \<in> R"
+  using assms(1)
+proof (induction p arbitrary: i)
+  case (pCons a p i)
+  have [simp]: "a \<in> R"
+    using pCons.prems[of 0] by auto
+  have "coeff p i \<in> R" for i
+    using pCons.prems[of "Suc i"] by auto
+  hence "coeff (p \<circ>\<^sub>p q) i \<in> R" for i
+    using pCons.prems by (intro pCons.IH)
+  thus ?case
+    by (auto simp: pcompose_pCons coeff_pCons split: nat.splits
+             intro!: assms R_plus coeff_mult_semiring_closed)
+qed auto
+
+end
+
+
 subsection \<open>Shifting polynomials\<close>
 
 definition poly_shift :: "nat \<Rightarrow> 'a::zero poly \<Rightarrow> 'a poly"
@@ -2463,7 +2515,8 @@
 next
   case (Suc n)
   then show ?thesis
-    by (metis coeff_0 coeff_pderiv degree_0 leading_coeff_0_iff mult_eq_0_iff nat.distinct(1) of_nat_eq_0_iff)    
+    using coeff_0 coeff_pderiv degree_0 leading_coeff_0_iff mult_eq_0_iff nat.distinct(1) of_nat_eq_0_iff
+    by (metis coeff_0 coeff_pderiv degree_0 leading_coeff_0_iff mult_eq_0_iff nat.distinct(1) of_nat_eq_0_iff)
 qed
 
 lemma degree_pderiv: "degree (pderiv p) = degree p - 1"
@@ -2868,6 +2921,264 @@
 qed
 
 
+subsection \<open>Algebraic integers\<close>
+
+inductive algebraic_int :: "'a :: field \<Rightarrow> bool" where
+  "\<lbrakk>lead_coeff p = 1; \<forall>i. coeff p i \<in> \<int>; poly p x = 0\<rbrakk> \<Longrightarrow> algebraic_int x"
+
+lemma algebraic_int_altdef_ipoly:
+  fixes x :: "'a :: field_char_0"
+  shows "algebraic_int x \<longleftrightarrow> (\<exists>p. poly (map_poly of_int p) x = 0 \<and> lead_coeff p = 1)"
+proof
+  assume "algebraic_int x"
+  then obtain p where p: "lead_coeff p = 1" "\<forall>i. coeff p i \<in> \<int>" "poly p x = 0"
+    by (auto elim: algebraic_int.cases)
+  define the_int where "the_int = (\<lambda>x::'a. THE r. x = of_int r)"
+  define p' where "p' = map_poly the_int p"
+  have of_int_the_int: "of_int (the_int x) = x" if "x \<in> \<int>" for x
+    unfolding the_int_def by (rule sym, rule theI') (insert that, auto simp: Ints_def)
+  have the_int_0_iff: "the_int x = 0 \<longleftrightarrow> x = 0" if "x \<in> \<int>" for x
+    using of_int_the_int[OF that] by auto
+  have [simp]: "the_int 0 = 0"
+    by (subst the_int_0_iff) auto
+  have "map_poly of_int p' = map_poly (of_int \<circ> the_int) p"
+    by (simp add: p'_def map_poly_map_poly)
+  also from p of_int_the_int have "\<dots> = p"
+    by (subst poly_eq_iff) (auto simp: coeff_map_poly)
+  finally have p_p': "map_poly of_int p' = p" .
+
+  show "(\<exists>p. poly (map_poly of_int p) x = 0 \<and> lead_coeff p = 1)"
+  proof (intro exI conjI notI)
+    from p show "poly (map_poly of_int p') x = 0" by (simp add: p_p')
+  next
+    show "lead_coeff p' = 1"
+      using p by (simp flip: p_p' add: degree_map_poly coeff_map_poly)
+  qed
+next
+  assume "\<exists>p. poly (map_poly of_int p) x = 0 \<and> lead_coeff p = 1"
+  then obtain p where p: "poly (map_poly of_int p) x = 0" "lead_coeff p = 1"
+    by auto
+  define p' where "p' = (map_poly of_int p :: 'a poly)"
+  from p have "lead_coeff p' = 1" "poly p' x = 0" "\<forall>i. coeff p' i \<in> \<int>"
+    by (auto simp: p'_def coeff_map_poly degree_map_poly)
+  thus "algebraic_int x"
+    by (intro algebraic_int.intros)
+qed
+
+theorem rational_algebraic_int_is_int:
+  assumes "algebraic_int x" and "x \<in> \<rat>"
+  shows   "x \<in> \<int>"
+proof -
+  from assms(2) obtain a b where ab: "b > 0" "Rings.coprime a b" and x_eq: "x = of_int a / of_int b"
+    by (auto elim: Rats_cases')
+  from \<open>b > 0\<close> have [simp]: "b \<noteq> 0"
+    by auto
+  from assms(1) obtain p
+    where p: "lead_coeff p = 1" "\<forall>i. coeff p i \<in> \<int>" "poly p x = 0"
+    by (auto simp: algebraic_int.simps)
+
+  define q :: "'a poly" where "q = [:-of_int a, of_int b:]"
+  have "poly q x = 0" "q \<noteq> 0" "\<forall>i. coeff q i \<in> \<int>"
+    by (auto simp: x_eq q_def coeff_pCons split: nat.splits)
+  define n where "n = degree p"
+  have "n > 0"
+    using p by (intro Nat.gr0I) (auto simp: n_def elim!: degree_eq_zeroE)
+  have "(\<Sum>i<n. coeff p i * of_int (a ^ i * b ^ (n - i - 1))) \<in> \<int>"
+    using p by auto
+  then obtain R where R: "of_int R = (\<Sum>i<n. coeff p i * of_int (a ^ i * b ^ (n - i - 1)))"
+    by (auto simp: Ints_def)
+  have [simp]: "coeff p n = 1"
+    using p by (auto simp: n_def)
+
+  have "0 = poly p x * of_int b ^ n"
+    using p by simp
+  also have "\<dots> = (\<Sum>i\<le>n. coeff p i * x ^ i * of_int b ^ n)"
+    by (simp add: poly_altdef n_def sum_distrib_right)
+  also have "\<dots> = (\<Sum>i\<le>n. coeff p i * of_int (a ^ i * b ^ (n - i)))"
+    by (intro sum.cong) (auto simp: x_eq field_simps simp flip: power_add)
+  also have "{..n} = insert n {..<n}"
+    using \<open>n > 0\<close> by auto
+  also have "(\<Sum>i\<in>\<dots>. coeff p i * of_int (a ^ i * b ^ (n - i))) =
+               coeff p n * of_int (a ^ n) + (\<Sum>i<n. coeff p i * of_int (a ^ i * b ^ (n - i)))"
+    by (subst sum.insert) auto
+  also have "(\<Sum>i<n. coeff p i * of_int (a ^ i * b ^ (n - i))) =
+             (\<Sum>i<n. coeff p i * of_int (a ^ i * b * b ^ (n - i - 1)))"
+    by (intro sum.cong) (auto simp flip: power_add power_Suc simp: Suc_diff_Suc)
+  also have "\<dots> = of_int (b * R)"
+    by (simp add: R sum_distrib_left sum_distrib_right mult_ac)
+  finally have "of_int (a ^ n) = (-of_int (b * R) :: 'a)"
+    by (auto simp: add_eq_0_iff)
+  hence "a ^ n = -b * R"
+    by (simp flip: of_int_mult of_int_power of_int_minus)
+  hence "b dvd a ^ n"
+    by simp
+  with \<open>Rings.coprime a b\<close> have "b dvd 1"
+    by (meson coprime_power_left_iff dvd_refl not_coprimeI)
+  with x_eq and \<open>b > 0\<close> show ?thesis
+    by auto
+qed
+
+lemma algebraic_int_imp_algebraic [dest]: "algebraic_int x \<Longrightarrow> algebraic x"
+  by (auto simp: algebraic_int.simps algebraic_def)
+
+lemma int_imp_algebraic_int:
+  assumes "x \<in> \<int>"
+  shows   "algebraic_int x"
+proof
+  show "\<forall>i. coeff [:-x, 1:] i \<in> \<int>"
+    using assms by (auto simp: coeff_pCons split: nat.splits)
+qed auto
+
+lemma algebraic_int_0 [simp, intro]: "algebraic_int 0"
+  and algebraic_int_1 [simp, intro]: "algebraic_int 1"
+  and algebraic_int_numeral [simp, intro]: "algebraic_int (numeral n)"
+  and algebraic_int_of_nat [simp, intro]: "algebraic_int (of_nat k)"
+  and algebraic_int_of_int [simp, intro]: "algebraic_int (of_int k)"
+  by (simp_all add: int_imp_algebraic_int)
+
+lemma algebraic_int_ii [simp, intro]: "algebraic_int \<i>"
+proof
+  show "poly [:1, 0, 1:] \<i> = 0"
+    by simp
+qed (auto simp: coeff_pCons split: nat.splits)
+
+lemma algebraic_int_minus [intro]:
+  assumes "algebraic_int x"
+  shows   "algebraic_int (-x)"
+proof -
+  from assms obtain p where p: "lead_coeff p = 1" "\<forall>i. coeff p i \<in> \<int>" "poly p x = 0"
+    by (auto simp: algebraic_int.simps)
+  define s where "s = (if even (degree p) then 1 else -1 :: 'a)"
+
+  define q where "q = Polynomial.smult s (pcompose p [:0, -1:])"
+  have "lead_coeff q = s * lead_coeff (pcompose p [:0, -1:])"
+    by (simp add: q_def)
+  also have "lead_coeff (pcompose p [:0, -1:]) = lead_coeff p * (- 1) ^ degree p"
+    by (subst lead_coeff_comp) auto
+  finally have "poly q (-x) = 0" and "lead_coeff q = 1"
+    using p by (auto simp: q_def poly_pcompose s_def)
+  moreover have "coeff q i \<in> \<int>" for i
+  proof -
+    have "coeff (pcompose p [:0, -1:]) i \<in> \<int>"
+      using p by (intro coeff_pcompose_semiring_closed) (auto simp: coeff_pCons split: nat.splits)
+    thus ?thesis by (simp add: q_def s_def)
+  qed
+  ultimately show ?thesis
+    by (auto simp: algebraic_int.simps)
+qed
+
+lemma algebraic_int_minus_iff [simp]:
+  "algebraic_int (-x) \<longleftrightarrow> algebraic_int (x :: 'a :: field_char_0)"
+  using algebraic_int_minus[of x] algebraic_int_minus[of "-x"] by auto
+
+lemma algebraic_int_inverse [intro]:
+  assumes "poly p x = 0" and "\<forall>i. coeff p i \<in> \<int>" and "coeff p 0 = 1"
+  shows   "algebraic_int (inverse x)"
+proof
+  from assms have [simp]: "x \<noteq> 0"
+    by (auto simp: poly_0_coeff_0)
+  show "poly (reflect_poly p) (inverse x) = 0"
+    using assms by (simp add: poly_reflect_poly_nz)
+qed (use assms in \<open>auto simp: coeff_reflect_poly\<close>)
+
+lemma algebraic_int_root:
+  assumes "algebraic_int y" 
+      and "poly p x = y" and "\<forall>i. coeff p i \<in> \<int>" and "lead_coeff p = 1" and "degree p > 0"
+  shows   "algebraic_int x"
+proof -
+  from assms obtain q where q: "poly q y = 0" "\<forall>i. coeff q i \<in> \<int>" "lead_coeff q = 1"
+    by (auto simp: algebraic_int.simps)
+  show ?thesis
+  proof
+    from assms q show "lead_coeff (pcompose q p) = 1"
+      by (subst lead_coeff_comp) auto
+    from assms q show "\<forall>i. coeff (pcompose q p) i \<in> \<int>"
+      by (intro allI coeff_pcompose_semiring_closed) auto
+    show "poly (pcompose q p) x = 0"
+      using assms q by (simp add: poly_pcompose)
+  qed
+qed
+
+lemma algebraic_int_abs_real [simp]:
+  "algebraic_int \<bar>x :: real\<bar> \<longleftrightarrow> algebraic_int x"
+  by (auto simp: abs_if)
+
+lemma algebraic_int_nth_root_real [intro]:
+  assumes "algebraic_int x"
+  shows   "algebraic_int (root n x)"
+proof (cases "n = 0")
+  case False
+  show ?thesis
+  proof (rule algebraic_int_root)
+    show "poly (monom 1 n) (root n x) = (if even n then \<bar>x\<bar> else x)"
+      using sgn_power_root[of n x] False
+      by (auto simp add: poly_monom sgn_if split: if_splits)
+  qed (use False assms in \<open>auto simp: degree_monom_eq\<close>)
+qed auto
+
+lemma algebraic_int_sqrt [intro]: "algebraic_int x \<Longrightarrow> algebraic_int (sqrt x)"
+  by (auto simp: sqrt_def)
+
+lemma algebraic_int_csqrt [intro]: "algebraic_int x \<Longrightarrow> algebraic_int (csqrt x)"
+  by (rule algebraic_int_root[where p = "monom 1 2"])
+     (auto simp: poly_monom degree_monom_eq)
+
+lemma poly_map_poly_cnj [simp]: "poly (map_poly cnj p) x = cnj (poly p (cnj x))"
+  by (induction p) (auto simp: map_poly_pCons)
+
+lemma algebraic_int_cnj [intro]:
+  assumes "algebraic_int x"
+  shows   "algebraic_int (cnj x)"
+proof -
+  from assms obtain p where p: "lead_coeff p = 1" "\<forall>i. coeff p i \<in> \<int>" "poly p x = 0"
+    by (auto simp: algebraic_int.simps)
+  show ?thesis
+  proof
+    show "poly (map_poly cnj p) (cnj x) = 0"
+      using p by simp
+    show "lead_coeff (map_poly cnj p) = 1"
+      using p by (simp add: coeff_map_poly degree_map_poly)
+    show "\<forall>i. coeff (map_poly cnj p) i \<in> \<int>"
+      using p by (auto simp: coeff_map_poly)
+  qed
+qed
+
+lemma algebraic_int_cnj_iff [simp]: "algebraic_int (cnj x) \<longleftrightarrow> algebraic_int x"
+  using algebraic_int_cnj[of x] algebraic_int_cnj[of "cnj x"] by auto
+
+lemma algebraic_int_of_real [intro]:
+  assumes "algebraic_int x"
+  shows   "algebraic_int (of_real x)"
+proof -
+  from assms obtain p where p: "poly p x = 0" "\<forall>i. coeff p i \<in> \<int>" "lead_coeff p = 1"
+    by (auto simp: algebraic_int.simps)
+  show "algebraic_int (of_real x :: 'a)"
+  proof
+    have "poly (map_poly of_real p) (of_real x) = (of_real (poly p x) :: 'a)"
+      by (induction p) (auto simp: map_poly_pCons)
+    thus "poly (map_poly of_real p) (of_real x) = (0 :: 'a)"
+      using p by simp
+  qed (use p in \<open>auto simp: coeff_map_poly degree_map_poly\<close>)
+qed
+
+lemma algebraic_int_of_real_iff [simp]:
+  "algebraic_int (of_real x :: 'a :: {field_char_0, real_algebra_1}) \<longleftrightarrow> algebraic_int x"
+proof
+  assume "algebraic_int (of_real x :: 'a)"
+  then obtain p
+    where p: "poly (map_poly of_int p) (of_real x :: 'a) = 0" "lead_coeff p = 1"
+    by (auto simp: algebraic_int_altdef_ipoly)
+  show "algebraic_int x"
+    unfolding algebraic_int_altdef_ipoly
+  proof (intro exI[of _ p] conjI)
+    have "of_real (poly (map_poly real_of_int p) x) = poly (map_poly of_int p) (of_real x :: 'a)"
+      by (induction p) (auto simp: map_poly_pCons)
+    also note p(1)
+    finally show "poly (map_poly real_of_int p) x = 0" by simp
+  qed (use p in auto)
+qed auto
+
+
 subsection \<open>Division of polynomials\<close>
 
 subsubsection \<open>Division in general\<close>
diff -r 981a383610df -r 783406dd051e src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Jan 08 19:53:44 2021 +0100
+++ b/src/HOL/GCD.thy	Fri Jan 08 19:52:10 2021 +0100
@@ -2780,8 +2780,146 @@
   for x y :: nat
   by (fact gcd_nat.absorb2)
 
+lemma Gcd_in:
+  fixes A :: "nat set"
+  assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> gcd a b \<in> A"
+  assumes "A \<noteq> {}"
+  shows   "Gcd A \<in> A"
+proof (cases "A = {0}")
+  case False
+  with assms obtain x where "x \<in> A" "x > 0"
+    by auto
+  thus "Gcd A \<in> A"
+  proof (induction x rule: less_induct)
+    case (less x)
+    show ?case
+    proof (cases "x = Gcd A")
+      case False
+      have "\<exists>y\<in>A. \<not>x dvd y"
+        using False less.prems by (metis Gcd_dvd Gcd_greatest_nat gcd_nat.asym)
+      then obtain y where y: "y \<in> A" "\<not>x dvd y"
+        by blast
+      have "gcd x y \<in> A"
+        by (rule assms(1)) (use \<open>x \<in> A\<close> y in auto)
+      moreover have "gcd x y < x"
+        using \<open>x > 0\<close> y by (metis gcd_dvd1 gcd_dvd2 nat_dvd_not_less nat_neq_iff)
+      moreover have "gcd x y > 0"
+        using \<open>x > 0\<close> by auto
+      ultimately show ?thesis using less.IH by blast
+    qed (use less in auto)
+  qed
+qed auto
+
+lemma bezout_gcd_nat':
+  fixes a b :: nat
+  shows "\<exists>x y. b * y \<le> a * x \<and> a * x - b * y = gcd a b \<or> a * y \<le> b * x \<and> b * x - a * y = gcd a b"
+  using bezout_nat[of a b]
+  by (metis add_diff_cancel_left' diff_zero gcd.commute gcd_0_nat
+            le_add_same_cancel1 mult.right_neutral zero_le)
+
 lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
 lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
 lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
 
+
+subsection \<open>Characteristic of a semiring\<close>
+
+definition (in semiring_1) semiring_char :: "'a itself \<Rightarrow> nat" 
+  where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
+
+context semiring_1
+begin
+
+context
+  fixes CHAR :: nat
+  defines "CHAR \<equiv> semiring_char (Pure.type :: 'a itself)"
+begin
+
+lemma of_nat_CHAR [simp]: "of_nat CHAR = (0 :: 'a)"
+proof -
+  have "CHAR \<in> {n. of_nat n = (0::'a)}"
+    unfolding CHAR_def semiring_char_def
+  proof (rule Gcd_in, clarify)
+    fix a b :: nat
+    assume *: "of_nat a = (0 :: 'a)" "of_nat b = (0 :: 'a)"
+    show "of_nat (gcd a b) = (0 :: 'a)"
+    proof (cases "a = 0")
+      case False
+      with bezout_nat obtain x y where "a * x = b * y + gcd a b"
+        by blast
+      hence "of_nat (a * x) = (of_nat (b * y + gcd a b) :: 'a)"
+        by (rule arg_cong)
+      thus "of_nat (gcd a b) = (0 :: 'a)"
+        using * by simp
+    qed (use * in auto)
+  next
+    have "of_nat 0 = (0 :: 'a)"
+      by simp
+    thus "{n. of_nat n = (0 :: 'a)} \<noteq> {}"
+      by blast
+  qed
+  thus ?thesis
+    by simp
+qed
+
+lemma of_nat_eq_0_iff_char_dvd: "of_nat n = (0 :: 'a) \<longleftrightarrow> CHAR dvd n"
+proof
+  assume "of_nat n = (0 :: 'a)"
+  thus "CHAR dvd n"
+    unfolding CHAR_def semiring_char_def by (intro Gcd_dvd) auto
+next
+  assume "CHAR dvd n"
+  then obtain m where "n = CHAR * m"
+    by auto
+  thus "of_nat n = (0 :: 'a)"
+    by simp
+qed
+
+lemma CHAR_eqI:
+  assumes "of_nat c = (0 :: 'a)"
+  assumes "\<And>x. of_nat x = (0 :: 'a) \<Longrightarrow> c dvd x"
+  shows   "CHAR = c"
+  using assms by (intro dvd_antisym) (auto simp: of_nat_eq_0_iff_char_dvd)
+
+lemma CHAR_eq0_iff: "CHAR = 0 \<longleftrightarrow> (\<forall>n>0. of_nat n \<noteq> (0::'a))"
+  by (auto simp: of_nat_eq_0_iff_char_dvd)
+
+lemma CHAR_pos_iff: "CHAR > 0 \<longleftrightarrow> (\<exists>n>0. of_nat n = (0::'a))"
+  using CHAR_eq0_iff neq0_conv by blast
+
+lemma CHAR_eq_posI:
+  assumes "c > 0" "of_nat c = (0 :: 'a)" "\<And>x. x > 0 \<Longrightarrow> x < c \<Longrightarrow> of_nat x \<noteq> (0 :: 'a)"
+  shows   "CHAR = c"
+proof (rule antisym)
+  from assms have "CHAR > 0"
+    by (auto simp: CHAR_pos_iff)
+  from assms(3)[OF this] show "CHAR \<ge> c"
+    by force
+next
+  have "CHAR dvd c"
+    using assms by (auto simp: of_nat_eq_0_iff_char_dvd)
+  thus "CHAR \<le> c"
+    using \<open>c > 0\<close> by (intro dvd_imp_le) auto
+qed
+
 end
+end
+
+lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char (Pure.type :: 'a itself) = 0"
+  by (simp add: CHAR_eq0_iff)
+
+
+(* nicer notation *)
+
+syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))")
+
+translations "CHAR('t)" => "CONST semiring_char (CONST Pure.type :: 't itself)"
+
+print_translation \<open>
+  let
+    fun char_type_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] =
+      Syntax.const \<^syntax_const>\<open>_type_char\<close> $ Syntax_Phases.term_of_typ ctxt T
+  in [(\<^const_syntax>\<open>semiring_char\<close>, char_type_tr')] end
+\<close>
+
+end
diff -r 981a383610df -r 783406dd051e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Jan 08 19:53:44 2021 +0100
+++ b/src/HOL/Int.thy	Fri Jan 08 19:52:10 2021 +0100
@@ -957,6 +957,12 @@
 
 end
 
+lemma Ints_sum [intro]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<int>) \<Longrightarrow> sum f A \<in> \<int>"
+  by (induction A rule: infinite_finite_induct) auto
+
+lemma Ints_prod [intro]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<int>) \<Longrightarrow> prod f A \<in> \<int>"
+  by (induction A rule: infinite_finite_induct) auto
+
 lemma (in linordered_idom) Ints_abs [simp]:
   shows "a \<in> \<int> \<Longrightarrow> abs a \<in> \<int>"
   by (auto simp: abs_if)
diff -r 981a383610df -r 783406dd051e src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Fri Jan 08 19:53:44 2021 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Jan 08 19:52:10 2021 +0100
@@ -223,6 +223,30 @@
   "(\<And>z. \<lbrakk>0 \<le> z; z < n\<rbrakk> \<Longrightarrow> P (of_int z)) \<Longrightarrow> P (x::'a)"
 by (cases x rule: cases) simp
 
+lemma UNIV_eq: "(UNIV :: 'a set) = Abs ` {0..<n}"
+  using type type_definition.univ by blast
+
+lemma CARD_eq: "CARD('a) = nat n"
+proof -
+  have "CARD('a) = card (Abs ` {0..<n})"
+    by (simp add: UNIV_eq)
+  also have "inj_on Abs {0..<n}"
+    by (metis Abs_inverse inj_onI)
+  hence "card (Abs ` {0..<n}) = nat n"
+    using size1 by (subst card_image) auto
+  finally show ?thesis .
+qed
+
+lemma CHAR_eq [simp]: "CHAR('a) = CARD('a)"
+proof (rule CHAR_eqI)
+  show "of_nat (CARD('a)) = (0 :: 'a)"
+    by (simp add: CARD_eq of_nat_eq zero_def)
+next
+  fix n assume "of_nat n = (0 :: 'a)"
+  thus "CARD('a) dvd n"
+    by (metis CARD_eq Rep_0 Rep_Abs_mod Rep_le_n mod_0_imp_dvd nat_dvd_iff of_nat_eq)
+qed
+
 end
 
 
@@ -574,6 +598,7 @@
 
 lemma "CARD(0) = 0" by simp
 lemma "CARD(17) = 17" by simp
+lemma "CHAR(23) = 23" by simp
 lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp
 
 end
diff -r 981a383610df -r 783406dd051e src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Jan 08 19:53:44 2021 +0100
+++ b/src/HOL/Rat.thy	Fri Jan 08 19:52:10 2021 +0100
@@ -815,6 +815,20 @@
   then show thesis ..
 qed
 
+lemma Rats_cases':
+  assumes "(x :: 'a :: field_char_0) \<in> \<rat>"
+  obtains a b where "b > 0" "coprime a b" "x = of_int a / of_int b"
+proof -
+  from assms obtain r where "x = of_rat r"
+    by (auto simp: Rats_def)
+  obtain a b where quot: "quotient_of r = (a,b)" by force
+  have "b > 0" using quotient_of_denom_pos[OF quot] .
+  moreover have "coprime a b" using quotient_of_coprime[OF quot] .
+  moreover have "x = of_int a / of_int b" unfolding \<open>x = of_rat r\<close>
+      quotient_of_div[OF quot] by (simp add: of_rat_divide)
+  ultimately show ?thesis using that by blast
+qed
+
 lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
   by (simp add: Rats_def)
 
diff -r 981a383610df -r 783406dd051e src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 19:53:44 2021 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 19:52:10 2021 +0100
@@ -358,6 +358,23 @@
      power_int b w = x"
   by (metis of_real_power_int of_real_eq_iff)
 
+lemma of_real_in_Ints_iff [simp]: "of_real x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
+proof safe
+  fix x assume "(of_real x :: 'a) \<in> \<int>"
+  then obtain n where "(of_real x :: 'a) = of_int n"
+    by (auto simp: Ints_def)
+  also have "of_int n = of_real (real_of_int n)"
+    by simp
+  finally have "x = real_of_int n"
+    by (subst (asm) of_real_eq_iff)
+  thus "x \<in> \<int>"
+    by auto
+qed (auto simp: Ints_def)
+
+lemma Ints_of_real [intro]: "x \<in> \<int> \<Longrightarrow> of_real x \<in> \<int>"
+  by simp
+
+
 text \<open>Every real algebra has characteristic zero.\<close>
 instance real_algebra_1 < ring_char_0
 proof