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