summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Manuel Eberl <eberlm@in.tum.de> |

Fri, 08 Jan 2021 19:52:10 +0100 | |

changeset 73109 | 783406dd051e |

parent 73108 | 981a383610df |

child 73110 | c87ca43ebd3b |

some algebra material for HOL: characteristic of a ring, algebraic integers

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