# HG changeset patch # User Manuel Eberl # Date 1712237381 -7200 # Node ID 173548e4d5d04b81e2a034a9303a264563a7097b # Parent e2174bf626b8e39e68bde82b84c96abad48ae61a moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory diff -r e2174bf626b8 -r 173548e4d5d0 CONTRIBUTORS --- a/CONTRIBUTORS Thu Apr 04 11:40:45 2024 +0200 +++ b/CONTRIBUTORS Thu Apr 04 15:29:41 2024 +0200 @@ -6,6 +6,11 @@ Contributions to Isabelle2024 ----------------------------- +* Αpril 2024: Manuel Eberl, Katharina Kreuzer + Some material on finite fields and the characteristic of a ring in HOL, + HOL-Computational_Algebra, and HOL-Number_Theory. + Also a type constructor for the algebraic closure of a field. + * March 2024: Manuel Eberl Weierstraß Factorization Theorem in HOL-Complex_Analysis. diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Algebra/Algebra.thy --- a/src/HOL/Algebra/Algebra.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Algebra/Algebra.thy Thu Apr 04 15:29:41 2024 +0200 @@ -5,4 +5,5 @@ Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure Left_Coset SimpleGroups SndIsomorphismGrp begin + end diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Algebra/Algebraic_Closure_Type.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Algebraic_Closure_Type.thy Thu Apr 04 15:29:41 2024 +0200 @@ -0,0 +1,625 @@ +(* + File: Algebra/Algebraic_Closure_Type.thy + Authors: Katharina Kreuzer (TU München) + Manuel Eberl (University of Innsbruck) + + A type definition for the algebraic closure of fields. +*) + +theory Algebraic_Closure_Type +imports + Algebraic_Closure + "HOL-Computational_Algebra.Computational_Algebra" + "HOL-Computational_Algebra.Field_as_Ring" +begin + + +definition (in ring_1) ring_of_type_algebra :: "'a ring" + where "ring_of_type_algebra = \ + carrier = UNIV, monoid.mult = (\x y. x * y), + one = 1, + ring.zero = 0, + add = (\ x y. x + y) \" + +lemma (in comm_ring_1) ring_from_type_algebra [intro]: + "ring (ring_of_type_algebra :: 'a ring)" +proof - + have "\y. x + y = 0" for x :: 'a + using add.right_inverse by blast + thus ?thesis + unfolding ring_of_type_algebra_def using add.right_inverse + by unfold_locales (auto simp:algebra_simps Units_def) +qed + +lemma (in comm_ring_1) cring_from_type_algebra [intro]: + "cring (ring_of_type_algebra :: 'a ring)" +proof - + have "\y. x + y = 0" for x :: 'a + using add.right_inverse by blast + thus ?thesis + unfolding ring_of_type_algebra_def using add.right_inverse + by unfold_locales (auto simp:algebra_simps Units_def) +qed + +lemma (in Fields.field) field_from_type_algebra [intro]: + "field (ring_of_type_algebra :: 'a ring)" +proof - + have "\y. x + y = 0" for x :: 'a + using add.right_inverse by blast + + moreover have "x \ 0 \ \y. x * y = 1" for x :: 'a + by (rule exI[of _ "inverse x"]) auto + + ultimately show ?thesis + unfolding ring_of_type_algebra_def using add.right_inverse + by unfold_locales (auto simp:algebra_simps Units_def) +qed + + + +subsection \Definition\ + +typedef (overloaded) 'a :: field alg_closure = + "carrier (field.alg_closure (ring_of_type_algebra :: 'a :: field ring))" +proof - + define K where "K \ (ring_of_type_algebra :: 'a ring)" + define L where "L \ field.alg_closure K" + + interpret K: field K + unfolding K_def by rule + + interpret algebraic_closure L "range K.indexed_const" + proof - + have *: "carrier K = UNIV" + by (auto simp: K_def ring_of_type_algebra_def) + show "algebraic_closure L (range K.indexed_const)" + unfolding * [symmetric] L_def by (rule K.alg_closureE) + qed + + show "\x. x \ carrier L" + using zero_closed by blast +qed + +setup_lifting type_definition_alg_closure + +instantiation alg_closure :: (field) field +begin + +context + fixes L K + defines "K \ (ring_of_type_algebra :: 'a :: field ring)" + defines "L \ field.alg_closure K" +begin + +interpretation K: field K + unfolding K_def by rule + +interpretation algebraic_closure L "range K.indexed_const" +proof - + have *: "carrier K = UNIV" + by (auto simp: K_def ring_of_type_algebra_def) + show "algebraic_closure L (range K.indexed_const)" + unfolding * [symmetric] L_def by (rule K.alg_closureE) +qed + +lift_definition zero_alg_closure :: "'a alg_closure" is "ring.zero L" + by (fold K_def, fold L_def) (rule ring_simprules) + +lift_definition one_alg_closure :: "'a alg_closure" is "monoid.one L" + by (fold K_def, fold L_def) (rule ring_simprules) + +lift_definition plus_alg_closure :: "'a alg_closure \ 'a alg_closure \ 'a alg_closure" + is "ring.add L" + by (fold K_def, fold L_def) (rule ring_simprules) + +lift_definition minus_alg_closure :: "'a alg_closure \ 'a alg_closure \ 'a alg_closure" + is "a_minus L" + by (fold K_def, fold L_def) (rule ring_simprules) + +lift_definition times_alg_closure :: "'a alg_closure \ 'a alg_closure \ 'a alg_closure" + is "monoid.mult L" + by (fold K_def, fold L_def) (rule ring_simprules) + +lift_definition uminus_alg_closure :: "'a alg_closure \ 'a alg_closure" + is "a_inv L" + by (fold K_def, fold L_def) (rule ring_simprules) + +lift_definition inverse_alg_closure :: "'a alg_closure \ 'a alg_closure" + is "\x. if x = ring.zero L then ring.zero L else m_inv L x" + by (fold K_def, fold L_def) (auto simp: field_Units) + +lift_definition divide_alg_closure :: "'a alg_closure \ 'a alg_closure \ 'a alg_closure" + is "\x y. if y = ring.zero L then ring.zero L else monoid.mult L x (m_inv L y)" + by (fold K_def, fold L_def) (auto simp: field_Units) + +end + +instance proof - + define K where "K \ (ring_of_type_algebra :: 'a ring)" + define L where "L \ field.alg_closure K" + + interpret K: field K + unfolding K_def by rule + + interpret algebraic_closure L "range K.indexed_const" + proof - + have *: "carrier K = UNIV" + by (auto simp: K_def ring_of_type_algebra_def) + show "algebraic_closure L (range K.indexed_const)" + unfolding * [symmetric] L_def by (rule K.alg_closureE) + qed + + show "OFCLASS('a alg_closure, field_class)" + proof (standard, goal_cases) + case 1 + show ?case + by (transfer, fold K_def, fold L_def) (rule m_assoc) + next + case 2 + show ?case + by (transfer, fold K_def, fold L_def) (rule m_comm) + next + case 3 + show ?case + by (transfer, fold K_def, fold L_def) (rule l_one) + next + case 4 + show ?case + by (transfer, fold K_def, fold L_def) (rule a_assoc) + next + case 5 + show ?case + by (transfer, fold K_def, fold L_def) (rule a_comm) + next + case 6 + show ?case + by (transfer, fold K_def, fold L_def) (rule l_zero) + next + case 7 + show ?case + by (transfer, fold K_def, fold L_def) (rule ring_simprules) + next + case 8 + show ?case + by (transfer, fold K_def, fold L_def) (rule ring_simprules) + next + case 9 + show ?case + by (transfer, fold K_def, fold L_def) (rule ring_simprules) + next + case 10 + show ?case + by (transfer, fold K_def, fold L_def) (rule zero_not_one) + next + case 11 + thus ?case + by (transfer, fold K_def, fold L_def) (auto simp: field_Units) + next + case 12 + thus ?case + by (transfer, fold K_def, fold L_def) auto + next + case 13 + thus ?case + by transfer auto + qed +qed + +end + + + +subsection \The algebraic closure is algebraically closed\ + +instance alg_closure :: (field) alg_closed_field +proof + define K where "K \ (ring_of_type_algebra :: 'a ring)" + define L where "L \ field.alg_closure K" + + interpret K: field K + unfolding K_def by rule + + interpret algebraic_closure L "range K.indexed_const" + proof - + have *: "carrier K = UNIV" + by (auto simp: K_def ring_of_type_algebra_def) + show "algebraic_closure L (range K.indexed_const)" + unfolding * [symmetric] L_def by (rule K.alg_closureE) + qed + + have [simp]: "Rep_alg_closure x \ carrier L" for x + using Rep_alg_closure[of x] by (simp only: L_def K_def) + + have [simp]: "Rep_alg_closure x = Rep_alg_closure y \ x = y" for x y + by (simp add: Rep_alg_closure_inject) + have [simp]: "Rep_alg_closure x = \\<^bsub>L\<^esub> \ x = 0" for x + proof - + have "Rep_alg_closure x = Rep_alg_closure 0 \ x = 0" + by simp + also have "Rep_alg_closure 0 = \\<^bsub>L\<^esub>" + by (simp add: zero_alg_closure.rep_eq L_def K_def) + finally show ?thesis . + qed + + have [simp]: "Rep_alg_closure (x ^ n) = Rep_alg_closure x [^]\<^bsub>L\<^esub> n" + for x :: "'a alg_closure" and n + by (induction n) + (auto simp: one_alg_closure.rep_eq times_alg_closure.rep_eq m_comm + simp flip: L_def K_def) + have [simp]: "Rep_alg_closure (Abs_alg_closure x) = x" if "x \ carrier L" for x + using that unfolding L_def K_def by (rule Abs_alg_closure_inverse) + + show "\x. poly p x = 0" if p: "Polynomial.lead_coeff p = 1" "Polynomial.degree p > 0" + for p :: "'a alg_closure poly" + proof - + define P where "P = rev (map Rep_alg_closure (Polynomial.coeffs p))" + have deg: "Polynomials.degree P = Polynomial.degree p" + by (auto simp: P_def degree_eq_length_coeffs) + have carrier_P: "P \ carrier (poly_ring L)" + by (auto simp: univ_poly_def polynomial_def P_def hd_map hd_rev last_map + last_coeffs_eq_coeff_degree) + hence "splitted P" + using roots_over_carrier by blast + hence "roots P \ {#}" + unfolding splitted_def using deg p by auto + then obtain x where "x \# roots P" + by blast + hence x: "is_root P x" + using roots_mem_iff_is_root[OF carrier_P] by auto + hence [simp]: "x \ carrier L" + by (auto simp: is_root_def) + define x' where "x' = Abs_alg_closure x" + define xs where "xs = rev (coeffs p)" + + have "cr_alg_closure (eval (map Rep_alg_closure xs) x) (poly (Poly (rev xs)) x')" + by (induction xs) + (auto simp flip: K_def L_def simp: cr_alg_closure_def + zero_alg_closure.rep_eq plus_alg_closure.rep_eq + times_alg_closure.rep_eq Poly_append poly_monom + a_comm m_comm x'_def) + also have "map Rep_alg_closure xs = P" + by (simp add: xs_def P_def rev_map) + also have "Poly (rev xs) = p" + by (simp add: xs_def) + finally have "poly p x' = 0" + using x by (auto simp: is_root_def cr_alg_closure_def) + thus "\x. poly p x = 0" .. + qed +qed + + + +subsection \Converting between the base field and the closure\ + +context + fixes L K + defines "K \ (ring_of_type_algebra :: 'a :: field ring)" + defines "L \ field.alg_closure K" +begin + +interpretation K: field K + unfolding K_def by rule + +interpretation algebraic_closure L "range K.indexed_const" +proof - + have *: "carrier K = UNIV" + by (auto simp: K_def ring_of_type_algebra_def) + show "algebraic_closure L (range K.indexed_const)" + unfolding * [symmetric] L_def by (rule K.alg_closureE) +qed + +lemma alg_closure_hom: "K.indexed_const \ Ring.ring_hom K L" + unfolding L_def using K.alg_closureE(2) . + +lift_definition%important to_ac :: "'a :: field \ 'a alg_closure" + is "ring.indexed_const K" + by (fold K_def, fold L_def) (use mem_carrier in blast) + +lemma to_ac_0 [simp]: "to_ac (0 :: 'a) = 0" +proof - + have "to_ac (\\<^bsub>K\<^esub>) = 0" + proof (transfer fixing: K, fold K_def, fold L_def) + show "K.indexed_const \\<^bsub>K\<^esub> = \\<^bsub>L\<^esub>" + using Ring.ring_hom_zero[OF alg_closure_hom] K.ring_axioms is_ring + by simp + qed + thus ?thesis + by (simp add: K_def ring_of_type_algebra_def) +qed + +lemma to_ac_1 [simp]: "to_ac (1 :: 'a) = 1" +proof - + have "to_ac (\\<^bsub>K\<^esub>) = 1" + proof (transfer fixing: K, fold K_def, fold L_def) + show "K.indexed_const \\<^bsub>K\<^esub> = \\<^bsub>L\<^esub>" + using Ring.ring_hom_one[OF alg_closure_hom] K.ring_axioms is_ring + by simp + qed + thus ?thesis + by (simp add: K_def ring_of_type_algebra_def) +qed + +lemma to_ac_add [simp]: "to_ac (x + y :: 'a) = to_ac x + to_ac y" +proof - + have "to_ac (x \\<^bsub>K\<^esub> y) = to_ac x + to_ac y" + proof (transfer fixing: K x y, fold K_def, fold L_def) + show "K.indexed_const (x \\<^bsub>K\<^esub> y) = K.indexed_const x \\<^bsub>L\<^esub> K.indexed_const y" + using Ring.ring_hom_add[OF alg_closure_hom, of x y] K.ring_axioms is_ring + by (simp add: K_def ring_of_type_algebra_def) + qed + thus ?thesis + by (simp add: K_def ring_of_type_algebra_def) +qed + +lemma to_ac_minus [simp]: "to_ac (-x :: 'a) = -to_ac x" + using to_ac_add to_ac_0 add_eq_0_iff by metis + +lemma to_ac_diff [simp]: "to_ac (x - y :: 'a) = to_ac x - to_ac y" + using to_ac_add[of x "-y"] by simp + +lemma to_ac_mult [simp]: "to_ac (x * y :: 'a) = to_ac x * to_ac y" +proof - + have "to_ac (x \\<^bsub>K\<^esub> y) = to_ac x * to_ac y" + proof (transfer fixing: K x y, fold K_def, fold L_def) + show "K.indexed_const (x \\<^bsub>K\<^esub> y) = K.indexed_const x \\<^bsub>L\<^esub> K.indexed_const y" + using Ring.ring_hom_mult[OF alg_closure_hom, of x y] K.ring_axioms is_ring + by (simp add: K_def ring_of_type_algebra_def) + qed + thus ?thesis + by (simp add: K_def ring_of_type_algebra_def) +qed + +lemma to_ac_inverse [simp]: "to_ac (inverse x :: 'a) = inverse (to_ac x)" + using to_ac_mult[of x "inverse x"] to_ac_1 to_ac_0 + by (metis divide_self_if field_class.field_divide_inverse field_class.field_inverse_zero inverse_unique) + +lemma to_ac_divide [simp]: "to_ac (x / y :: 'a) = to_ac x / to_ac y" + using to_ac_mult[of x "inverse y"] to_ac_inverse[of y] + by (simp add: field_class.field_divide_inverse) + +lemma to_ac_power [simp]: "to_ac (x ^ n) = to_ac x ^ n" + by (induction n) auto + +lemma to_ac_of_nat [simp]: "to_ac (of_nat n) = of_nat n" + by (induction n) auto + +lemma to_ac_of_int [simp]: "to_ac (of_int n) = of_int n" + by (induction n) auto + +lemma to_ac_numeral [simp]: "to_ac (numeral n) = numeral n" + using to_ac_of_nat[of "numeral n"] by (simp del: to_ac_of_nat) + +lemma to_ac_sum: "to_ac (\x\A. f x) = (\x\A. to_ac (f x))" + by (induction A rule: infinite_finite_induct) auto + +lemma to_ac_prod: "to_ac (\x\A. f x) = (\x\A. to_ac (f x))" + by (induction A rule: infinite_finite_induct) auto + +lemma to_ac_sum_list: "to_ac (sum_list xs) = (\x\xs. to_ac x)" + by (induction xs) auto + +lemma to_ac_prod_list: "to_ac (prod_list xs) = (\x\xs. to_ac x)" + by (induction xs) auto + +lemma to_ac_sum_mset: "to_ac (sum_mset xs) = (\x\#xs. to_ac x)" + by (induction xs) auto + +lemma to_ac_prod_mset: "to_ac (prod_mset xs) = (\x\#xs. to_ac x)" + by (induction xs) auto + +end + +lemma (in ring) indexed_const_eq_iff [simp]: + "indexed_const x = (indexed_const y :: 'c multiset \ 'a) \ x = y" +proof + assume "indexed_const x = (indexed_const y :: 'c multiset \ 'a)" + hence "indexed_const x ({#} :: 'c multiset) = indexed_const y ({#} :: 'c multiset)" + by metis + thus "x = y" + by (simp add: indexed_const_def) +qed auto + +lemma inj_to_ac: "inj to_ac" + by (transfer, intro injI, subst (asm) ring.indexed_const_eq_iff) auto + +lemma to_ac_eq_iff [simp]: "to_ac x = to_ac y \ x = y" + using inj_to_ac by (auto simp: inj_on_def) + +lemma to_ac_eq_0_iff [simp]: "to_ac x = 0 \ x = 0" + and to_ac_eq_0_iff' [simp]: "0 = to_ac x \ x = 0" + and to_ac_eq_1_iff [simp]: "to_ac x = 1 \ x = 1" + and to_ac_eq_1_iff' [simp]: "1 = to_ac x \ x = 1" + using to_ac_eq_iff to_ac_0 to_ac_1 by metis+ + + +definition of_ac :: "'a :: field alg_closure \ 'a" where + "of_ac x = (if x \ range to_ac then inv_into UNIV to_ac x else 0)" + +lemma of_ac_eqI: "to_ac x = y \ of_ac y = x" + unfolding of_ac_def by (meson inj_to_ac inv_f_f range_eqI) + +lemma of_ac_0 [simp]: "of_ac 0 = 0" + and of_ac_1 [simp]: "of_ac 1 = 1" + by (rule of_ac_eqI; simp; fail)+ + +lemma of_ac_to_ac [simp]: "of_ac (to_ac x) = x" + by (rule of_ac_eqI) auto + +lemma to_ac_of_ac: "x \ range to_ac \ to_ac (of_ac x) = x" + by auto + + +lemma CHAR_alg_closure [simp]: + "CHAR('a :: field alg_closure) = CHAR('a)" +proof (rule CHAR_eqI) + show "of_nat CHAR('a) = (0 :: 'a alg_closure)" + by (metis of_nat_CHAR to_ac_0 to_ac_of_nat) +next + show "CHAR('a) dvd n" if "of_nat n = (0 :: 'a alg_closure)" for n + using that by (metis of_nat_eq_0_iff_char_dvd to_ac_eq_0_iff' to_ac_of_nat) +qed + +instance alg_closure :: (field_char_0) field_char_0 +proof + show "inj (of_nat :: nat \ 'a alg_closure)" + by (metis injD inj_of_nat inj_on_def inj_to_ac to_ac_of_nat) +qed + + +bundle alg_closure_syntax +begin +notation to_ac ("_\" [1000] 999) +notation of_ac ("_\" [1000] 999) +end + + +bundle alg_closure_syntax' +begin +notation (output) to_ac ("_") +notation (output) of_ac ("_") +end + + +subsection \The algebraic closure is an algebraic extension\ + +text \ + The algebraic closure is an algebraic extension, i.e.\ every element in it is + a root of some non-zero polynomial in the base field. +\ +theorem alg_closure_algebraic: + fixes x :: "'a :: field alg_closure" + obtains p :: "'a poly" where "p \ 0" "poly (map_poly to_ac p) x = 0" +proof - + define K where "K \ (ring_of_type_algebra :: 'a ring)" + define L where "L \ field.alg_closure K" + + interpret K: field K + unfolding K_def by rule + + interpret algebraic_closure L "range K.indexed_const" + proof - + have *: "carrier K = UNIV" + by (auto simp: K_def ring_of_type_algebra_def) + show "algebraic_closure L (range K.indexed_const)" + unfolding * [symmetric] L_def by (rule K.alg_closureE) + qed + + let ?K = "range K.indexed_const" + have sr: "subring ?K L" + by (rule subring_axioms) + define x' where "x' = Rep_alg_closure x" + have "x' \ carrier L" + unfolding x'_def L_def K_def by (rule Rep_alg_closure) + hence alg: "(algebraic over range K.indexed_const) x'" + using algebraic_extension by blast + then obtain p where p: "p \ carrier (?K[X]\<^bsub>L\<^esub>)" "p \ []" "eval p x' = \\<^bsub>L\<^esub>" + using algebraicE[OF sr \x' \ carrier L\ alg] by blast + + have [simp]: "Rep_alg_closure x \ carrier L" for x + using Rep_alg_closure[of x] by (simp only: L_def K_def) + have [simp]: "Abs_alg_closure x = 0 \ x = \\<^bsub>L\<^esub>" if "x \ carrier L" for x + using that unfolding L_def K_def + by (metis Abs_alg_closure_inverse zero_alg_closure.rep_eq zero_alg_closure_def) + have [simp]: "Rep_alg_closure (x ^ n) = Rep_alg_closure x [^]\<^bsub>L\<^esub> n" + for x :: "'a alg_closure" and n + by (induction n) + (auto simp: one_alg_closure.rep_eq times_alg_closure.rep_eq m_comm + simp flip: L_def K_def) + have [simp]: "Rep_alg_closure (Abs_alg_closure x) = x" if "x \ carrier L" for x + using that unfolding L_def K_def by (rule Abs_alg_closure_inverse) + have [simp]: "Rep_alg_closure x = \\<^bsub>L\<^esub> \ x = 0" for x + by (metis K_def L_def Rep_alg_closure_inverse zero_alg_closure.rep_eq) + + define p' where "p' = Poly (map Abs_alg_closure (rev p))" + have "p' \ 0" + proof + assume "p' = 0" + then obtain n where n: "map Abs_alg_closure (rev p) = replicate n 0" + by (auto simp: p'_def Poly_eq_0) + with \p \ []\ have "n > 0" + by (auto intro!: Nat.gr0I) + have "last (map Abs_alg_closure (rev p)) = 0" + using \n > 0\ by (subst n) auto + moreover have "Polynomials.lead_coeff p \ \\<^bsub>L\<^esub>" "Polynomials.lead_coeff p \ carrier L" + using p \p \ []\ local.subset + by (fastforce simp: polynomial_def univ_poly_def)+ + ultimately show False + using \p \ []\ by (auto simp: last_map last_rev) + qed + + have "set p \ carrier L" + using local.subset p by (auto simp: univ_poly_def polynomial_def) + hence "cr_alg_closure (eval p x') (poly p' x)" + unfolding p'_def + by (induction p) + (auto simp flip: K_def L_def simp: cr_alg_closure_def + zero_alg_closure.rep_eq plus_alg_closure.rep_eq + times_alg_closure.rep_eq Poly_append poly_monom + a_comm m_comm x'_def) + hence "poly p' x = 0" + using p by (auto simp: cr_alg_closure_def x'_def) + + have coeff_p': "Polynomial.coeff p' i \ range to_ac" for i + proof (cases "i \ length p") + case False + have "Polynomial.coeff p' i = Abs_alg_closure (rev p ! i)" + unfolding p'_def using False + by (auto simp: nth_default_def) + moreover have "rev p ! i \ ?K" + using p(1) False by (auto simp: univ_poly_def polynomial_def rev_nth) + ultimately show ?thesis + unfolding to_ac.abs_eq K_def by fastforce + qed (auto simp: p'_def nth_default_def) + + + define p'' where "p'' = map_poly of_ac p'" + have p'_eq: "p' = map_poly to_ac p''" + by (rule poly_eqI) (auto simp: coeff_map_poly p''_def to_ac_of_ac[OF coeff_p']) + + show ?thesis + proof (rule that) + show "p'' \ 0" + using \p' \ 0\ by (auto simp: p'_eq) + next + show "poly (map_poly to_ac p'') x = 0" + using \poly p' x = 0\ by (simp add: p'_eq) + qed +qed + + +instantiation alg_closure :: (field) + "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}" +begin + +definition [simp]: "normalize_alg_closure = (normalize_field :: 'a alg_closure \ _)" +definition [simp]: "unit_factor_alg_closure = (unit_factor_field :: 'a alg_closure \ _)" +definition [simp]: "modulo_alg_closure = (mod_field :: 'a alg_closure \ _)" +definition [simp]: "euclidean_size_alg_closure = (euclidean_size_field :: 'a alg_closure \ _)" +definition [simp]: "division_segment (x :: 'a alg_closure) = 1" + +instance + by standard + (simp_all add: dvd_field_iff field_split_simps split: if_splits) + +end + +instantiation alg_closure :: (field) euclidean_ring_gcd +begin + +definition gcd_alg_closure :: "'a alg_closure \ 'a alg_closure \ 'a alg_closure" where + "gcd_alg_closure = Euclidean_Algorithm.gcd" +definition lcm_alg_closure :: "'a alg_closure \ 'a alg_closure \ 'a alg_closure" where + "lcm_alg_closure = Euclidean_Algorithm.lcm" +definition Gcd_alg_closure :: "'a alg_closure set \ 'a alg_closure" where + "Gcd_alg_closure = Euclidean_Algorithm.Gcd" +definition Lcm_alg_closure :: "'a alg_closure set \ 'a alg_closure" where + "Lcm_alg_closure = Euclidean_Algorithm.Lcm" + +instance by standard (simp_all add: gcd_alg_closure_def lcm_alg_closure_def Gcd_alg_closure_def Lcm_alg_closure_def) + +end + +instance alg_closure :: (field) semiring_gcd_mult_normalize + .. + +end \ No newline at end of file diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Computational_Algebra/Euclidean_Algorithm.thy --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy Thu Apr 04 15:29:41 2024 +0200 @@ -675,4 +675,31 @@ instance int :: normalization_euclidean_semiring_multiplicative .. +lemma (in idom) prime_CHAR_semidom: + assumes "CHAR('a) > 0" + shows "prime CHAR('a)" +proof - + have False if ab: "a \ 1" "b \ 1" "CHAR('a) = a * b" for a b + proof - + from assms ab have "a > 0" "b > 0" + by (auto intro!: Nat.gr0I) + have "of_nat (a * b) = (0 :: 'a)" + using ab by (metis of_nat_CHAR) + also have "of_nat (a * b) = (of_nat a :: 'a) * of_nat b" + by simp + finally have "of_nat a * of_nat b = (0 :: 'a)" . + moreover have "of_nat a * of_nat b \ (0 :: 'a)" + using ab \a > 0\ \b > 0\ + by (intro no_zero_divisors) (auto simp: of_nat_eq_0_iff_char_dvd) + ultimately show False + by contradiction + qed + moreover have "CHAR('a) > 1" + using assms CHAR_not_1' by linarith + ultimately have "prime_elem CHAR('a)" + by (intro irreducible_imp_prime_elem) (auto simp: Factorial_Ring.irreducible_def) + thus ?thesis + by (auto simp: prime_def) +qed + end diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Computational_Algebra/Factorial_Ring.thy --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Thu Apr 04 15:29:41 2024 +0200 @@ -51,6 +51,59 @@ by auto qed (use assms in \auto simp: irreducible_def\) +lemma irreducible_multD: + assumes l: "irreducible (a*b)" + shows "a dvd 1 \ irreducible b \ b dvd 1 \ irreducible a" +proof- + have *: "irreducible b" if l: "irreducible (a*b)" and a: "a dvd 1" for a b :: 'a + proof (rule irreducibleI) + show "\(b dvd 1)" + proof + assume "b dvd 1" + hence "a * b dvd 1 * 1" + using \a dvd 1\ by (intro mult_dvd_mono) auto + with l show False + by (auto simp: irreducible_def) + qed + next + fix x y assume "b = x * y" + have "a * x dvd 1 \ y dvd 1" + using l by (rule irreducibleD) (use \b = x * y\ in \auto simp: mult_ac\) + thus "x dvd 1 \ y dvd 1" + by auto + qed (use l a in auto) + + from irreducibleD[OF assms refl] have "a dvd 1 \ b dvd 1" + by (auto simp: irreducible_def) + with *[of a b] *[of b a] l show ?thesis + by (auto simp: mult.commute) +qed + +lemma irreducible_power_iff [simp]: + "irreducible (p ^ n) \ irreducible p \ n = 1" +proof + assume *: "irreducible (p ^ n)" + have "irreducible p" + using * by (induction n) (auto dest!: irreducible_multD) + hence [simp]: "\p dvd 1" + using * by (auto simp: irreducible_def) + + consider "n = 0" | "n = 1" | "n > 1" + by linarith + thus "irreducible p \ n = 1" + proof cases + assume "n > 1" + hence "p ^ n = p * p ^ (n - 1)" + by (cases n) auto + with * \\ p dvd 1\ have "p ^ (n - 1) dvd 1" + using irreducible_multD[of p "p ^ (n - 1)"] by auto + with \\p dvd 1\ and \n > 1\ have False + by (meson dvd_power dvd_trans zero_less_diff) + thus ?thesis .. + qed (use * in auto) +qed auto + + definition prime_elem :: "'a \ bool" where "prime_elem p \ p \ 0 \ \p dvd 1 \ (\a b. p dvd (a * b) \ p dvd a \ p dvd b)" @@ -2172,7 +2225,7 @@ with assms show False by auto qed -text \Now a string of results due to Jakub Kądziołka\ +text \Now a string of results due to Maya Kądziołka\ lemma multiplicity_dvd_iff_dvd: assumes "x \ 0" diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Thu Apr 04 15:29:41 2024 +0200 @@ -30,7 +30,7 @@ lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI] -lemma expand_fls_eq: "f = g \ (\n. f $$ n = g $$ n)" +lemma fls_eq_iff: "f = g \ (\n. f $$ n = g $$ n)" by (simp add: fls_nth_inject[symmetric] fun_eq_iff) lemma nth_Abs_fls [simp]: "\\<^sub>\n. f (- int n) = 0 \ Abs_fls f $$ n = f n" @@ -136,9 +136,15 @@ lemma fls_const_nonzero: "c \ 0 \ fls_const c \ 0" using fls_nonzeroI[of "fls_const c" 0] by simp +lemma fls_const_eq_0_iff [simp]: "fls_const c = 0 \ c = 0" + by (auto simp: fls_eq_iff) + lemma fls_const_1 [simp]: "fls_const 1 = 1" unfolding fls_const_def one_fls_def .. +lemma fls_const_eq_1_iff [simp]: "fls_const c = 1 \ c = 1" + by (auto simp: fls_eq_iff) + lift_definition fls_X :: "'a::{zero,one} fls" is "\n. if n = 1 then 1 else 0" by simp @@ -1683,6 +1689,18 @@ instance fls :: (idom) idom .. +lemma semiring_char_fls [simp]: "CHAR('a :: comm_semiring_1 fls) = CHAR('a)" + by (rule CHAR_eqI) (auto simp: fls_of_nat of_nat_eq_0_iff_char_dvd fls_const_nonzero) + +instance fls :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char + by (rule semiring_prime_charI) auto +instance fls :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char + by standard +instance fls :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char + by standard +instance fls :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char + by standard + subsubsection \Powers\ @@ -2908,6 +2926,9 @@ instance fls :: (field) field by (standard, simp_all add: field_simps) +instance fls :: ("{field_prime_char,comm_semiring_1}") field_prime_char + by (rule field_prime_charI') auto + subsubsection \Division\ diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Computational_Algebra/Formal_Power_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Apr 04 15:29:41 2024 +0200 @@ -10,6 +10,7 @@ imports Complex_Main Euclidean_Algorithm + Primes begin @@ -537,7 +538,6 @@ instance fps :: (semiring_1_cancel) semiring_1_cancel .. - lemma fps_square_nth: "(f^2) $ n = (\k\n. f $ k * f $ (n - k))" by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost) @@ -562,9 +562,15 @@ lemma fps_const_nonzero_eq_nonzero: "c \ 0 \ fps_const c \ 0" using fps_nonzeroI[of "fps_const c" 0] by simp +lemma fps_const_eq_0_iff [simp]: "fps_const c = 0 \ c = 0" + by (auto simp: fps_eq_iff) + lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1" by (simp add: fps_ext) +lemma fps_const_eq_1_iff [simp]: "fps_const c = 1 \ c = 1" + by (auto simp: fps_eq_iff) + lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0" by (cases "c = 0") (auto intro!: subdegreeI) @@ -681,6 +687,25 @@ instance fps :: (idom) idom .. +lemma fps_of_nat: "fps_const (of_nat c) = of_nat c" + by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add) + +lemma fps_of_int: "fps_const (of_int c) = of_int c" + by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] + del: fps_const_minus fps_const_neg) + +lemma semiring_char_fps [simp]: "CHAR('a :: comm_semiring_1 fps) = CHAR('a)" + by (rule CHAR_eqI) (auto simp flip: fps_of_nat simp: of_nat_eq_0_iff_char_dvd) + +instance fps :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char + by (rule semiring_prime_charI) auto +instance fps :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char + by standard +instance fps :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char + by standard +instance fps :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char + by standard + lemma fps_numeral_fps_const: "numeral k = fps_const (numeral k)" by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1 fps_const_add [symmetric]) @@ -699,13 +724,6 @@ lemma subdegree_numeral [simp]: "subdegree (numeral n) = 0" by (simp add: numeral_fps_const) -lemma fps_of_nat: "fps_const (of_nat c) = of_nat c" - by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add) - -lemma fps_of_int: "fps_const (of_int c) = of_int c" - by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] - del: fps_const_minus fps_const_neg) - lemma fps_nth_of_nat [simp]: "(of_nat c) $ n = (if n=0 then of_nat c else 0)" by (simp add: fps_of_nat[symmetric]) diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Thu Apr 04 15:29:41 2024 +0200 @@ -12,7 +12,7 @@ Complex_Main "HOL-Library.More_List" "HOL-Library.Infinite_Set" - Factorial_Ring + Primes begin context semidom_modulo @@ -1533,6 +1533,18 @@ instance poly :: ("{ring_char_0, comm_ring_1}") ring_char_0 by standard (auto simp add: of_nat_poly intro: injI) +lemma semiring_char_poly [simp]: "CHAR('a :: comm_semiring_1 poly) = CHAR('a)" + by (rule CHAR_eqI) (auto simp: of_nat_poly of_nat_eq_0_iff_char_dvd) + +instance poly :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char + by (rule semiring_prime_charI) auto +instance poly :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char + by standard +instance poly :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char + by standard +instance poly :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char + by standard + lemma degree_mult_eq: "p \ 0 \ q \ 0 \ degree (p * q) = degree p + degree q" 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) @@ -5940,6 +5952,18 @@ finally show "\x. (\k\n. f k * x ^ k) = 0" .. qed +lemma (in alg_closed_field) nth_root_exists: + assumes "n > 0" + shows "\y. y ^ n = (x :: 'a)" +proof - + define f where "f = (\i. if i = 0 then -x else if i = n then 1 else 0)" + have "\x. (\k\n. f k * x ^ k) = 0" + by (rule alg_closed) (use assms in \auto simp: f_def\) + also have "(\x. \k\n. f k * x ^ k) = (\x. \k\{0,n}. f k * x ^ k)" + by (intro ext sum.mono_neutral_right) (auto simp: f_def) + finally show "\y. y ^ n = x" + using assms by (simp add: f_def) +qed text \ We can now prove by induction that every polynomial of degree \n\ splits into a product of diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Computational_Algebra/Polynomial_Factorial.thy --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Thu Apr 04 15:29:41 2024 +0200 @@ -632,6 +632,8 @@ semiring_gcd_mult_normalize}") euclidean_ring_gcd by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard +instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd, + semiring_gcd_mult_normalize}") factorial_semiring_multiplicative .. subsection \Polynomial GCD\ diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Computational_Algebra/Primes.thy --- a/src/HOL/Computational_Algebra/Primes.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Computational_Algebra/Primes.thy Thu Apr 04 15:29:41 2024 +0200 @@ -797,6 +797,231 @@ by (auto simp add: prime_dvd_mult_iff) qed +lemma (in ring_1) minus_power_prime_CHAR: + assumes "p = CHAR('a)" "prime p" + shows "(-x :: 'a) ^ p = -(x ^ p)" +proof (cases "p = 2") + case False + have "prime p" + using assms by blast + hence "odd p" + using prime_imp_coprime assms False coprime_right_2_iff_odd gcd_nat.strict_iff_not by blast + thus ?thesis + by simp +qed (use assms in \auto simp: uminus_CHAR_2\) + + +subsection \Rings and fields with prime characteristic\ + +text \ + We introduce some type classes for rings and fields with prime characteristic. +\ + +class semiring_prime_char = semiring_1 + + assumes prime_char_aux: "\n. prime n \ of_nat n = (0 :: 'a)" +begin + +lemma CHAR_pos [intro, simp]: "CHAR('a) > 0" + using local.CHAR_pos_iff local.prime_char_aux prime_gt_0_nat by blast + +lemma CHAR_nonzero [simp]: "CHAR('a) \ 0" + using CHAR_pos by auto + +lemma CHAR_prime [intro, simp]: "prime CHAR('a)" + by (metis (mono_tags, lifting) gcd_nat.order_iff_strict local.of_nat_1 local.of_nat_eq_0_iff_char_dvd + local.one_neq_zero local.prime_char_aux prime_nat_iff) + +end + +lemma semiring_prime_charI [intro?]: + "prime CHAR('a :: semiring_1) \ OFCLASS('a, semiring_prime_char_class)" + by standard auto + +lemma idom_prime_charI [intro?]: + assumes "CHAR('a :: idom) > 0" + shows "OFCLASS('a, semiring_prime_char_class)" +proof + show "prime CHAR('a)" + using assms prime_CHAR_semidom by blast +qed + +class comm_semiring_prime_char = comm_semiring_1 + semiring_prime_char +class comm_ring_prime_char = comm_ring_1 + semiring_prime_char +begin +subclass comm_semiring_prime_char .. +end +class idom_prime_char = idom + semiring_prime_char +begin +subclass comm_ring_prime_char .. +end + +class field_prime_char = field + + assumes pos_char_exists: "\n>0. of_nat n = (0 :: 'a)" +begin +subclass idom_prime_char + apply standard + using pos_char_exists local.CHAR_pos_iff local.of_nat_CHAR local.prime_CHAR_semidom by blast +end + +lemma field_prime_charI [intro?]: + "n > 0 \ of_nat n = (0 :: 'a :: field) \ OFCLASS('a, field_prime_char_class)" + by standard auto + +lemma field_prime_charI' [intro?]: + "CHAR('a :: field) > 0 \ OFCLASS('a, field_prime_char_class)" + by standard auto + + +subsection \Finite fields\ + +class finite_field = field_prime_char + finite + +lemma finite_fieldI [intro?]: + assumes "finite (UNIV :: 'a :: field set)" + shows "OFCLASS('a, finite_field_class)" +proof standard + show "\n>0. of_nat n = (0 :: 'a)" + using assms prime_CHAR_semidom[where ?'a = 'a] finite_imp_CHAR_pos[OF assms] + by (intro exI[of _ "CHAR('a)"]) auto +qed fact+ + +text \ + On a finite field with \n\ elements, taking the \n\-th power of an element + is the identity. This is an obvious consequence of the fact that the multiplicative group of + the field is a finite group of order \n - 1\, so \x^n = 1\ for any non-zero \x\. + + Note that this result is sharp in the sense that the multiplicative group of a + finite field is cyclic, i.e.\ it contains an element of order \n - 1\. + (We don't prove this here.) +\ +lemma finite_field_power_card_eq_same: + fixes x :: "'a :: finite_field" + shows "x ^ card (UNIV :: 'a set) = x" +proof (cases "x = 0") + case False + have "x * (\y\UNIV-{0}. x * y) = x * x ^ (card (UNIV :: 'a set) - 1) * \(UNIV-{0})" + by (simp add: prod.distrib mult_ac) + also have "x * x ^ (card (UNIV :: 'a set) - 1) = x ^ Suc (card (UNIV :: 'a set) - 1)" + by (subst power_Suc) auto + also have "Suc (card (UNIV :: 'a set) - 1) = card (UNIV :: 'a set)" + using finite_UNIV_card_ge_0[where ?'a = 'a] by simp + also have "(\y\UNIV-{0}. x * y) = (\y\UNIV-{0}. y)" + by (rule prod.reindex_bij_witness[of _ "\y. y / x" "\y. x * y"]) (use False in auto) + finally show ?thesis + by simp +qed (use finite_UNIV_card_ge_0[where ?'a = 'a] in auto) + +lemma finite_field_power_card_power_eq_same: + fixes x :: "'a :: finite_field" + assumes "m = card (UNIV :: 'a set) ^ n" + shows "x ^ m = x" + unfolding assms + by (induction n) (simp_all add: finite_field_power_card_eq_same power_mult) + +class enum_finite_field = finite_field + + fixes enum_finite_field :: "nat \ 'a" + assumes enum_finite_field: "enum_finite_field ` {.. + To get rid of the pending sort hypotheses, we prove that the field with 2 elements is indeed + a finite field. +\ +typedef gf2 = "{0, 1 :: nat}" + by auto + +setup_lifting type_definition_gf2 + +instantiation gf2 :: field +begin +lift_definition zero_gf2 :: "gf2" is "0" by auto +lift_definition one_gf2 :: "gf2" is "1" by auto +lift_definition uminus_gf2 :: "gf2 \ gf2" is "\x. x" . +lift_definition plus_gf2 :: "gf2 \ gf2 \ gf2" is "\x y. if x = y then 0 else 1" by auto +lift_definition minus_gf2 :: "gf2 \ gf2 \ gf2" is "\x y. if x = y then 0 else 1" by auto +lift_definition times_gf2 :: "gf2 \ gf2 \ gf2" is "\x y. x * y" by auto +lift_definition inverse_gf2 :: "gf2 \ gf2" is "\x. x" . +lift_definition divide_gf2 :: "gf2 \ gf2 \ gf2" is "\x y. x * y" by auto + +instance + by standard (transfer; fastforce)+ + +end + +instance gf2 :: finite_field +proof + interpret type_definition Rep_gf2 Abs_gf2 "{0, 1 :: nat}" + by (rule type_definition_gf2) + show "finite (UNIV :: gf2 set)" + by (metis Abs_image finite.emptyI finite.insertI finite_imageI) +qed + + +subsection \The Freshman's Dream in rings of prime characteristic\ + +lemma (in comm_semiring_1) freshmans_dream: + fixes x y :: 'a and n :: nat + assumes "prime CHAR('a)" + assumes n_def: "n = CHAR('a)" + shows "(x + y) ^ n = x ^ n + y ^ n" +proof - + interpret comm_semiring_prime_char + by standard (auto intro!: exI[of _ "CHAR('a)"] assms) + have "n > 0" + unfolding n_def by simp + have "(x + y) ^ n = (\k\n. of_nat (n choose k) * x ^ k * y ^ (n - k))" + by (rule binomial_ring) + also have "\ = (\k\{0,n}. of_nat (n choose k) * x ^ k * y ^ (n - k))" + proof (intro sum.mono_neutral_right ballI) + fix k assume "k \ {..n} - {0, n}" + hence k: "k > 0" "k < n" + by auto + have "CHAR('a) dvd (n choose k)" + unfolding n_def + by (rule dvd_choose_prime) (use k in \auto simp: n_def\) + hence "of_nat (n choose k) = (0 :: 'a)" + using of_nat_eq_0_iff_char_dvd by blast + thus "of_nat (n choose k) * x ^ k * y ^ (n - k) = 0" + by simp + qed auto + finally show ?thesis + using \n > 0\ by (simp add: add_ac) +qed + +lemma (in comm_semiring_1) freshmans_dream': + assumes [simp]: "prime CHAR('a)" and "m = CHAR('a) ^ n" + shows "(x + y :: 'a) ^ m = x ^ m + y ^ m" + unfolding assms(2) +proof (induction n) + case (Suc n) + have "(x + y) ^ (CHAR('a) ^ n * CHAR('a)) = ((x + y) ^ (CHAR('a) ^ n)) ^ CHAR('a)" + by (rule power_mult) + thus ?case + by (simp add: Suc.IH freshmans_dream Groups.mult_ac flip: power_mult) +qed auto + +lemma (in comm_semiring_1) freshmans_dream_sum: + fixes f :: "'b \ 'a" + assumes "prime CHAR('a)" and "n = CHAR('a)" + shows "sum f A ^ n = sum (\i. f i ^ n) A" + using assms + by (induct A rule: infinite_finite_induct) + (auto simp add: power_0_left freshmans_dream) + +lemma (in comm_semiring_1) freshmans_dream_sum': + fixes f :: "'b \ 'a" + assumes "prime CHAR('a)" "m = CHAR('a) ^ n" + shows "sum f A ^ m = sum (\i. f i ^ m) A" + using assms + by (induction A rule: infinite_finite_induct) + (auto simp: freshmans_dream' power_0_left) + + (* TODO Legacy names *) lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat] diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/GCD.thy Thu Apr 04 15:29:41 2024 +0200 @@ -2949,4 +2949,98 @@ lemma (in idom) CHAR_not_1' [simp]: "CHAR('a) \ Suc 0" using local.of_nat_CHAR by fastforce +lemma (in ring_1) uminus_CHAR_2: + assumes "CHAR('a) = 2" + shows "-(x :: 'a) = x" +proof - + have "x + x = 2 * x" + by (simp add: mult_2) + also have "2 = (0 :: 'a)" + using assms local.of_nat_CHAR by auto + finally show ?thesis + by (simp add: add_eq_0_iff2) +qed + +lemma (in ring_1) minus_CHAR_2: + assumes "CHAR('a) = 2" + shows "(x - y :: 'a) = x + y" +proof - + have "x - y = x + (-y)" + by simp + also have "-y = y" + by (rule uminus_CHAR_2) fact + finally show ?thesis . +qed + +lemma (in semiring_1_cancel) of_nat_eq_iff_char_dvd: + assumes "m < n" + shows "of_nat m = (of_nat n :: 'a) \ CHAR('a) dvd (n - m)" +proof + assume *: "of_nat m = (of_nat n :: 'a)" + have "of_nat n = (of_nat m + of_nat (n - m) :: 'a)" + using assms by (metis le_add_diff_inverse local.of_nat_add nless_le) + hence "of_nat (n - m) = (0 :: 'a)" + by (simp add: *) + thus "CHAR('a) dvd (n - m)" + by (simp add: of_nat_eq_0_iff_char_dvd) +next + assume "CHAR('a) dvd (n - m)" + hence "of_nat (n - m) = (0 :: 'a)" + by (simp add: of_nat_eq_0_iff_char_dvd) + hence "of_nat m = (of_nat m + of_nat (n - m) :: 'a)" + by simp + also have "\ = of_nat n" + using assms by (metis le_add_diff_inverse local.of_nat_add nless_le) + finally show "of_nat m = (of_nat n :: 'a)" . +qed + +lemma (in ring_1) of_int_eq_0_iff_char_dvd: + "(of_int n = (0 :: 'a)) = (int CHAR('a) dvd n)" +proof (cases "n \ 0") + case True + hence "(of_int n = (0 :: 'a)) \ (of_nat (nat n)) = (0 :: 'a)" + by auto + also have "\ \ CHAR('a) dvd nat n" + by (subst of_nat_eq_0_iff_char_dvd) auto + also have "\ \ int CHAR('a) dvd n" + using True by presburger + finally show ?thesis . +next + case False + hence "(of_int n = (0 :: 'a)) \ -(of_nat (nat (-n))) = (0 :: 'a)" + by auto + also have "\ \ CHAR('a) dvd nat (-n)" + by (auto simp: of_nat_eq_0_iff_char_dvd) + also have "\ \ int CHAR('a) dvd n" + using False dvd_nat_abs_iff[of "CHAR('a)" n] by simp + finally show ?thesis . +qed + +lemma (in semiring_1_cancel) finite_imp_CHAR_pos: + assumes "finite (UNIV :: 'a set)" + shows "CHAR('a) > 0" +proof - + have "\n\UNIV. infinite {m \ UNIV. of_nat m = (of_nat n :: 'a)}" + proof (rule pigeonhole_infinite) + show "infinite (UNIV :: nat set)" + by simp + show "finite (range (of_nat :: nat \ 'a))" + by (rule finite_subset[OF _ assms]) auto + qed + then obtain n :: nat where "infinite {m \ UNIV. of_nat m = (of_nat n :: 'a)}" + by blast + hence "\({m \ UNIV. of_nat m = (of_nat n :: 'a)} \ {n})" + by (intro notI) (use finite_subset in blast) + then obtain m where "m \ n" "of_nat m = (of_nat n :: 'a)" + by blast + thus ?thesis + proof (induction m n rule: linorder_wlog) + case (le m n) + hence "CHAR('a) dvd (n - m)" + using of_nat_eq_iff_char_dvd[of m n] by auto + thus ?thesis + using le by (intro Nat.gr0I) auto + qed (simp_all add: eq_commute) +qed + end diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Number_Theory/Cong.thy --- a/src/HOL/Number_Theory/Cong.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Number_Theory/Cong.thy Thu Apr 04 15:29:41 2024 +0200 @@ -747,4 +747,29 @@ by blast qed +lemma (in semiring_1_cancel) of_nat_eq_iff_cong_CHAR: + "of_nat x = (of_nat y :: 'a) \ [x = y] (mod CHAR('a))" +proof (induction x y rule: linorder_wlog) + case (le x y) + define z where "z = y - x" + have [simp]: "y = x + z" + using le by (auto simp: z_def) + have "(CHAR('a) dvd z) = [x = x + z] (mod CHAR('a))" + by (metis \y = x + z\ cong_def le mod_eq_dvd_iff_nat z_def) + thus ?case + by (simp add: of_nat_eq_0_iff_char_dvd) +qed (simp add: eq_commute cong_sym_eq) + +lemma (in ring_1) of_int_eq_iff_cong_CHAR: + "of_int x = (of_int y :: 'a) \ [x = y] (mod int CHAR('a))" +proof - + have "of_int x = (of_int y :: 'a) \ of_int (x - y) = (0 :: 'a)" + by auto + also have "\ \ (int CHAR('a) dvd x - y)" + by (rule of_int_eq_0_iff_char_dvd) + also have "\ \ [x = y] (mod int CHAR('a))" + by (simp add: cong_iff_dvd_diff) + finally show ?thesis . +qed + end diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/Number_Theory/Residues.thy --- a/src/HOL/Number_Theory/Residues.thy Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/Number_Theory/Residues.thy Thu Apr 04 15:29:41 2024 +0200 @@ -14,6 +14,66 @@ Totient begin +lemma (in ring_1) CHAR_dvd_CARD: "CHAR('a) dvd card (UNIV :: 'a set)" +proof (cases "card (UNIV :: 'a set) = 0") + case False + hence [intro]: "CHAR('a) > 0" + by (simp add: card_eq_0_iff finite_imp_CHAR_pos) + define G where "G = \ carrier = (UNIV :: 'a set), monoid.mult = (+), one = (0 :: 'a) \" + define H where "H = (of_nat ` {.. carrier G" + show "\y\carrier G. y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>" + by (intro bexI[of _ "-x"]) (auto simp: G_def) + qed (auto simp: G_def add_ac) + + interpret subgroup H G + proof + show "\\<^bsub>G\<^esub> \ H" + using False unfolding G_def H_def by force + next + fix x y :: 'a + assume "x \ H" "y \ H" + then obtain x' y' where [simp]: "x = of_nat x'" "y = of_nat y'" + by (auto simp: H_def) + have "x + y = of_nat ((x' + y') mod CHAR('a))" + by (auto simp flip: of_nat_add simp: of_nat_eq_iff_cong_CHAR) + moreover have "(x' + y') mod CHAR('a) < CHAR('a)" + using H_def \y \ H\ by fastforce + ultimately show "x \\<^bsub>G\<^esub> y \ H" + by (auto simp: H_def G_def intro!: imageI) + next + fix x :: 'a + assume x: "x \ H" + then obtain x' where [simp]: "x = of_nat x'" and x': "x' < CHAR('a)" + by (auto simp: H_def) + have "CHAR('a) dvd x' + (CHAR('a) - x') mod CHAR('a)" + using mod_eq_0_iff_dvd mod_if x' by fastforce + hence "x + of_nat ((CHAR('a) - x') mod CHAR('a)) = 0" + by (auto simp flip: of_nat_add simp: of_nat_eq_0_iff_char_dvd) + moreover from this have "inv\<^bsub>G\<^esub> x = of_nat ((CHAR('a) - x') mod CHAR('a))" + by (intro inv_equality) (auto simp: G_def add_ac) + moreover have "of_nat ((CHAR('a) - x') mod CHAR('a)) \ H" + unfolding H_def using \CHAR('a) > 0\ by (intro imageI) auto + ultimately show "inv\<^bsub>G\<^esub> x \ H" by force + qed (auto simp: G_def H_def) + + have "card H dvd card (rcosets\<^bsub>G\<^esub> H) * card H" + by simp + also have "card (rcosets\<^bsub>G\<^esub> H) * card H = Coset.order G" + proof (rule lagrange_finite) + show "finite (carrier G)" + using False card_ge_0_finite by (auto simp: G_def) + qed (fact is_subgroup) + finally have "card H dvd card (UNIV :: 'a set)" + by (simp add: Coset.order_def G_def) + also have "card H = card {.. int \ bool" where "QuadRes p a = (\y. ([y^2 = a] (mod p)))" diff -r e2174bf626b8 -r 173548e4d5d0 src/HOL/ROOT --- a/src/HOL/ROOT Thu Apr 04 11:40:45 2024 +0200 +++ b/src/HOL/ROOT Thu Apr 04 15:29:41 2024 +0200 @@ -436,6 +436,7 @@ Divisibility (* Rings *) IntRing (* Ideals and residue classes *) UnivPoly (* Polynomials *) + Algebraic_Closure_Type (* Main theory *) Algebra document_files "root.bib" "root.tex"