imports Complex_Main More_Finite_Product UnivPoly

(* Title: HOL/Algebra/Multiplicative_Group.thy Author: Simon Wimmer Author: Lars Noschinski *) theory Multiplicative_Group imports Complex_Main Group More_Group More_Finite_Product Coset UnivPoly begin section {* Simplification Rules for Polynomials *} text_raw {* \label{sec:simp-rules} *} lemma (in ring_hom_cring) hom_sub[simp]: assumes "x ∈ carrier R" "y ∈ carrier R" shows "h (x ⊖ y) = h x ⊖⇘_{S⇙}h y" using assms by (simp add: R.minus_eq S.minus_eq) context UP_ring begin lemma deg_nzero_nzero: assumes deg_p_nzero: "deg R p ≠ 0" shows "p ≠ 𝟬⇘_{P⇙}" using deg_zero deg_p_nzero by auto lemma deg_add_eq: assumes c: "p ∈ carrier P" "q ∈ carrier P" assumes "deg R q ≠ deg R p" shows "deg R (p ⊕⇘_{P⇙}q) = max (deg R p) (deg R q)" proof - let ?m = "max (deg R p) (deg R q)" from assms have "coeff P p ?m = 𝟬 ⟷ coeff P q ?m ≠ 𝟬" by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1) then have "coeff P (p ⊕⇘_{P⇙}q) ?m ≠ 𝟬" using assms by auto then have "deg R (p ⊕⇘_{P⇙}q) ≥ ?m" using assms by (blast intro: deg_belowI) with deg_add[OF c] show ?thesis by arith qed lemma deg_minus_eq: assumes "p ∈ carrier P" "q ∈ carrier P" "deg R q ≠ deg R p" shows "deg R (p ⊖⇘_{P⇙}q) = max (deg R p) (deg R q)" using assms by (simp add: deg_add_eq a_minus_def) end context UP_cring begin lemma evalRR_add: assumes "p ∈ carrier P" "q ∈ carrier P" assumes x:"x ∈ carrier R" shows "eval R R id x (p ⊕⇘_{P⇙}q) = eval R R id x p ⊕ eval R R id x q" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemma evalRR_sub: assumes "p ∈ carrier P" "q ∈ carrier P" assumes x:"x ∈ carrier R" shows "eval R R id x (p ⊖⇘_{P⇙}q) = eval R R id x p ⊖ eval R R id x q" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemma evalRR_mult: assumes "p ∈ carrier P" "q ∈ carrier P" assumes x:"x ∈ carrier R" shows "eval R R id x (p ⊗⇘_{P⇙}q) = eval R R id x p ⊗ eval R R id x q" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemma evalRR_monom: assumes a: "a ∈ carrier R" and x: "x ∈ carrier R" shows "eval R R id x (monom P a d) = a ⊗ x (^) d" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp show ?thesis using assms by (simp add: eval_monom) qed lemma evalRR_one: assumes x: "x ∈ carrier R" shows "eval R R id x 𝟭⇘_{P⇙}= 𝟭" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemma carrier_evalRR: assumes x: "x ∈ carrier R" and "p ∈ carrier P" shows "eval R R id x p ∈ carrier R" proof - interpret UP_pre_univ_prop R R id by unfold_locales simp interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x]) show ?thesis using assms by simp qed lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR end section {* Properties of the Euler @{text φ}-function *} text_raw {* \label{sec:euler-phi} *} text{* In this section we prove that for every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds. *} lemma dvd_div_ge_1 : fixes a b :: nat assumes "a ≥ 1" "b dvd a" shows "a div b ≥ 1" proof - from ‹b dvd a› obtain c where "a = b * c" .. with ‹a ≥ 1› show ?thesis by simp qed lemma dvd_nat_bounds : fixes n p :: nat assumes "p > 0" "n dvd p" shows "n > 0 ∧ n ≤ p" using assms by (simp add: dvd_pos_nat dvd_imp_le) (* Deviates from the definition given in the library in number theory *) definition phi' :: "nat => nat" where "phi' m = card {x. 1 ≤ x ∧ x ≤ m ∧ gcd x m = 1}" notation (latex output) phi' ("φ _") lemma phi'_nonzero : assumes "m > 0" shows "phi' m > 0" proof - have "1 ∈ {x. 1 ≤ x ∧ x ≤ m ∧ gcd x m = 1}" using assms by simp hence "card {x. 1 ≤ x ∧ x ≤ m ∧ gcd x m = 1} > 0" by (auto simp: card_gt_0_iff) thus ?thesis unfolding phi'_def by simp qed lemma dvd_div_eq_1: fixes a b c :: nat assumes "c dvd a" "c dvd b" "a div c = b div c" shows "a = b" using assms dvd_mult_div_cancel[OF `c dvd a`] dvd_mult_div_cancel[OF `c dvd b`] by presburger lemma dvd_div_eq_2: fixes a b c :: nat assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b" shows "a = b" proof - have "a > 0" "a ≤ c" using dvd_nat_bounds[OF assms(1-2)] by auto have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce also have "… = b*(c div a)" using assms dvd_mult_div_cancel by fastforce finally show "a = b" using `c>0` dvd_div_ge_1[OF _ `a dvd c`] by fastforce qed lemma div_mult_mono: fixes a b c :: nat assumes "a > 0" "a≤d" shows "a * b div d ≤ b" proof - have "a*b div d ≤ b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger thus ?thesis using assms by force qed text{* We arrive at the main result of this section: For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds. The outline of the proof for this lemma is as follows: We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$. We analyze the reduced form $a/d = m/n$ for any of those fractions. We want to know how many fractions $m/n$ have the reduced form denominator $d$. The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$. Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. @{term "gcd a d = 1"}. This number is exactly @{term "phi' d"}. Finally, by counting the fractions $m/n$ according to their reduced form denominator, we get: @{term [display] "(∑d | d dvd n . phi' d) = n"}. To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$ \begin{itemize} \item the set of reduced form numerators @{term "{a. (1::nat) ≤ a ∧ a ≤ d ∧ coprime a d}"} \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$, i.e. the set @{term "{m ∈ {1::nat .. n}. n div gcd m n = d}"} \end{itemize} We show that @{term "λa. a*n div d"} with the inverse @{term "λa. a div gcd a n"} is a bijection between theses sets, thus yielding the equality @{term [display] "phi' d = card {m ∈ {1 .. n}. n div gcd m n = d}"} This gives us @{term [display] "(∑d | d dvd n . phi' d) = card (⋃d ∈ {d. d dvd n}. {m ∈ {1 .. n}. n div gcd m n = d})"} and by showing @{term "(⋃d ∈ {d. d dvd n}. {m ∈ {1::nat .. n}. n div gcd m n = d}) ⊇ {1 .. n}"} (this is our counting argument) the thesis follows. *} lemma sum_phi'_factors : fixes n :: nat assumes "n > 0" shows "(∑d | d dvd n. phi' d) = n" proof - { fix d assume "d dvd n" then obtain q where q: "n = d * q" .. have "card {a. 1 ≤ a ∧ a ≤ d ∧ coprime a d} = card {m ∈ {1 .. n}. n div gcd m n = d}" (is "card ?RF = card ?F") proof (rule card_bij_eq) { fix a b assume "a * n div d = b * n div d" hence "a * (n div d) = b * (n div d)" using dvd_div_mult[OF `d dvd n`] by (fastforce simp add: mult.commute) hence "a = b" using dvd_div_ge_1[OF _ `d dvd n`] `n>0` by (simp add: mult.commute nat_mult_eq_cancel1) } thus "inj_on (λa. a*n div d) ?RF" unfolding inj_on_def by blast { fix a assume a:"a∈?RF" hence "a * (n div d) ≥ 1" using `n>0` dvd_div_ge_1[OF _ `d dvd n`] by simp hence ge_1:"a * n div d ≥ 1" by (simp add: `d dvd n` div_mult_swap) have le_n:"a * n div d ≤ n" using div_mult_mono a by simp have "gcd (a * n div d) n = n div d * gcd a d" by (simp add: gcd_mult_distrib_nat q ac_simps) hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp hence "a * n div d ∈ ?F" using ge_1 le_n by (fastforce simp add: `d dvd n` dvd_mult_div_cancel) } thus "(λa. a*n div d) ` ?RF ⊆ ?F" by blast { fix m l assume A: "m ∈ ?F" "l ∈ ?F" "m div gcd m n = l div gcd l n" hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce } thus "inj_on (λa. a div gcd a n) ?F" unfolding inj_on_def by blast { fix m assume "m ∈ ?F" hence "m div gcd m n ∈ ?RF" using dvd_div_ge_1 by (fastforce simp add: div_le_mono div_gcd_coprime) } thus "(λa. a div gcd a n) ` ?F ⊆ ?RF" by blast qed force+ } hence phi'_eq:"⋀d. d dvd n ⟹ phi' d = card {m ∈ {1 .. n}. n div gcd m n = d}" unfolding phi'_def by presburger have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF `n>0`] by force have "(∑d | d dvd n. phi' d) = card (⋃d ∈ {d. d dvd n}. {m ∈ {1 .. n}. n div gcd m n = d})" using card_UN_disjoint[OF fin, of "(λd. {m ∈ {1 .. n}. n div gcd m n = d})"] phi'_eq by fastforce also have "(⋃d ∈ {d. d dvd n}. {m ∈ {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R") proof show "?L ⊇ ?R" proof fix m assume m: "m ∈ ?R" thus "m ∈ ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"] by (simp add: dvd_mult_div_cancel) qed qed fastforce finally show ?thesis by force qed section {* Order of an Element of a Group *} text_raw {* \label{sec:order-elem} *} context group begin lemma pow_eq_div2 : fixes m n :: nat assumes x_car: "x ∈ carrier G" assumes pow_eq: "x (^) m = x (^) n" shows "x (^) (m - n) = 𝟭" proof (cases "m < n") case False have "𝟭 ⊗ x (^) m = x (^) m" by (simp add: x_car) also have "… = x (^) (m - n) ⊗ x (^) n" using False by (simp add: nat_pow_mult x_car) also have "… = x (^) (m - n) ⊗ x (^) m" by (simp add: pow_eq) finally show ?thesis by (simp add: x_car) qed simp definition ord where "ord a = Min {d ∈ {1 .. order G} . a (^) d = 𝟭}" lemma assumes finite:"finite (carrier G)" assumes a:"a ∈ carrier G" shows ord_ge_1: "1 ≤ ord a" and ord_le_group_order: "ord a ≤ order G" and pow_ord_eq_1: "a (^) ord a = 𝟭" proof - have "¬inj_on (λx. a (^) x) {0 .. order G}" proof (rule notI) assume A: "inj_on (λx. a (^) x) {0 .. order G}" have "order G + 1 = card {0 .. order G}" by simp also have "… = card ((λx. a (^) x) ` {0 .. order G})" (is "_ = card ?S") using A by (simp add: card_image) also have "?S = {a (^) x | x. x ∈ {0 .. order G}}" by blast also have "… ⊆ carrier G" (is "?S ⊆ _") using a by blast then have "card ?S ≤ order G" unfolding order_def by (rule card_mono[OF finite]) finally show False by arith qed then obtain x y where x_y:"x ≠ y" "x ∈ {0 .. order G}" "y ∈ {0 .. order G}" "a (^) x = a (^) y" unfolding inj_on_def by blast obtain d where "1 ≤ d" "a (^) d = 𝟭" "d ≤ order G" proof cases assume "y < x" with x_y show ?thesis by (intro that[where d="x - y"]) (auto simp add: pow_eq_div2[OF a]) next assume "¬y < x" with x_y show ?thesis by (intro that[where d="y - x"]) (auto simp add: pow_eq_div2[OF a]) qed hence "ord a ∈ {d ∈ {1 .. order G} . a (^) d = 𝟭}" unfolding ord_def using Min_in[of "{d ∈ {1 .. order G} . a (^) d = 𝟭}"] by fastforce then show "1 ≤ ord a" and "ord a ≤ order G" and "a (^) ord a = 𝟭" by (auto simp: order_def) qed lemma finite_group_elem_finite_ord : assumes "finite (carrier G)" "x ∈ carrier G" shows "∃ d::nat. d ≥ 1 ∧ x (^) d = 𝟭" using assms ord_ge_1 pow_ord_eq_1 by auto lemma ord_min: assumes "finite (carrier G)" "1 ≤ d" "a ∈ carrier G" "a (^) d = 𝟭" shows "ord a ≤ d" proof - def Ord ≡ "{d ∈ {1..order G}. a (^) d = 𝟭}" have fin: "finite Ord" by (auto simp: Ord_def) have in_ord: "ord a ∈ Ord" using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def) then have "Ord ≠ {}" by auto show ?thesis proof (cases "d ≤ order G") case True then have "d ∈ Ord" using assms by (auto simp: Ord_def) with fin in_ord show ?thesis unfolding ord_def Ord_def[symmetric] by simp next case False then show ?thesis using in_ord by (simp add: Ord_def) qed qed lemma ord_inj : assumes finite: "finite (carrier G)" assumes a: "a ∈ carrier G" shows "inj_on (λ x . a (^) x) {0 .. ord a - 1}" proof (rule inj_onI, rule ccontr) fix x y assume A: "x ∈ {0 .. ord a - 1}" "y ∈ {0 .. ord a - 1}" "a (^) x= a (^) y" "x ≠ y" have "finite {d ∈ {1..order G}. a (^) d = 𝟭}" by auto { fix x y assume A: "x < y" "x ∈ {0 .. ord a - 1}" "y ∈ {0 .. ord a - 1}" "a (^) x = a (^) y" hence "y - x < ord a" by auto also have "… ≤ order G" using assms by (simp add: ord_le_group_order) finally have y_x_range:"y - x ∈ {1 .. order G}" using A by force have "a (^) (y-x) = 𝟭" using a A by (simp add: pow_eq_div2) hence y_x:"y - x ∈ {d ∈ {1.. order G}. a (^) d = 𝟭}" using y_x_range by blast have "min (y - x) (ord a) = ord a" using Min.in_idem[OF `finite {d ∈ {1 .. order G} . a (^) d = 𝟭}` y_x] ord_def by auto with `y - x < ord a` have False by linarith } note X = this { assume "x < y" with A X have False by blast } moreover { assume "x > y" with A X have False by metis } moreover { assume "x = y" then have False using A by auto} ultimately show False by fastforce qed lemma ord_inj' : assumes finite: "finite (carrier G)" assumes a: "a ∈ carrier G" shows "inj_on (λ x . a (^) x) {1 .. ord a}" proof (rule inj_onI, rule ccontr) fix x y :: nat assume A:"x ∈ {1 .. ord a}" "y ∈ {1 .. ord a}" "a (^) x = a (^) y" "x≠y" { assume "x < ord a" "y < ord a" hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce } moreover { assume "x = ord a" "y < ord a" hence "a (^) y = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto hence "y=0" using ord_inj[OF assms] `y < ord a` unfolding inj_on_def by force hence False using A by fastforce } moreover { assume "y = ord a" "x < ord a" hence "a (^) x = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto hence "x=0" using ord_inj[OF assms] `x < ord a` unfolding inj_on_def by force hence False using A by fastforce } ultimately show False using A by force qed lemma ord_elems : assumes "finite (carrier G)" "a ∈ carrier G" shows "{a(^)x | x. x ∈ (UNIV :: nat set)} = {a(^)x | x. x ∈ {0 .. ord a - 1}}" (is "?L = ?R") proof show "?R ⊆ ?L" by blast { fix y assume "y ∈ ?L" then obtain x::nat where x:"y = a(^)x" by auto def r ≡ "x mod ord a" then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger hence "y = (a(^)ord a)(^)q ⊗ a(^)r" using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow) hence "y = a(^)r" using assms by (simp add: pow_ord_eq_1) have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def) hence "r ∈ {0 .. ord a - 1}" by (force simp: r_def) hence "y ∈ {a(^)x | x. x ∈ {0 .. ord a - 1}}" using `y=a(^)r` by blast } thus "?L ⊆ ?R" by auto qed lemma ord_dvd_pow_eq_1 : assumes "finite (carrier G)" "a ∈ carrier G" "a (^) k = 𝟭" shows "ord a dvd k" proof - def r ≡ "k mod ord a" then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger hence "a(^)k = (a(^)ord a)(^)q ⊗ a(^)r" using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow) hence "a(^)k = a(^)r" using assms by (simp add: pow_ord_eq_1) hence "a(^)r = 𝟭" using assms(3) by simp have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def) hence "r = 0" using `a(^)r = 𝟭` ord_def[of a] ord_min[of r a] assms(1-2) by linarith thus ?thesis using q by simp qed lemma dvd_gcd : fixes a b :: nat obtains q where "a * (b div gcd a b) = b*q" proof have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add: div_mult_swap dvd_div_mult) also have "… = b * (a div gcd a b)" by simp finally show "a * (b div gcd a b) = b * (a div gcd a b) " . qed lemma ord_pow_dvd_ord_elem : assumes finite[simp]: "finite (carrier G)" assumes a[simp]:"a ∈ carrier G" shows "ord (a(^)n) = ord a div gcd n (ord a)" proof - have "(a(^)n) (^) ord a = (a (^) ord a) (^) n" by (simp add: mult.commute nat_pow_pow) hence "(a(^)n) (^) ord a = 𝟭" by (simp add: pow_ord_eq_1) obtain q where "n * (ord a div gcd n (ord a)) = ord a * q" by (rule dvd_gcd) hence "(a(^)n) (^) (ord a div gcd n (ord a)) = (a (^) ord a)(^)q" by (simp add : nat_pow_pow) hence pow_eq_1: "(a(^)n) (^) (ord a div gcd n (ord a)) = 𝟭" by (auto simp add : pow_ord_eq_1[of a]) have "ord a ≥ 1" using ord_ge_1 by simp have ge_1:"ord a div gcd n (ord a) ≥ 1" proof - have "gcd n (ord a) dvd ord a" by blast thus ?thesis by (rule dvd_div_ge_1[OF `ord a ≥ 1`]) qed have "ord a ≤ order G" by (simp add: ord_le_group_order) have "ord a div gcd n (ord a) ≤ order G" proof - have "ord a div gcd n (ord a) ≤ ord a" by simp thus ?thesis using `ord a ≤ order G` by linarith qed hence ord_gcd_elem:"ord a div gcd n (ord a) ∈ {d ∈ {1..order G}. (a(^)n) (^) d = 𝟭}" using ge_1 pow_eq_1 by force { fix d :: nat assume d_elem:"d ∈ {d ∈ {1..order G}. (a(^)n) (^) d = 𝟭}" assume d_lt:"d < ord a div gcd n (ord a)" hence pow_nd:"a(^)(n*d) = 𝟭" using d_elem by (simp add : nat_pow_pow) hence "ord a dvd n*d" using assms by (auto simp add : ord_dvd_pow_eq_1) then obtain q where "ord a * q = n*d" by (metis dvd_mult_div_cancel) hence prod_eq:"(ord a div gcd n (ord a)) * q = (n div gcd n (ord a)) * d" by (simp add: dvd_div_mult) have cp:"coprime (ord a div gcd n (ord a)) (n div gcd n (ord a))" proof - have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))" using div_gcd_coprime[of n "ord a"] ge_1 by fastforce thus ?thesis by (simp add: gcd.commute) qed have dvd_d:"(ord a div gcd n (ord a)) dvd d" proof - have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq by (metis dvd_triv_right mult.commute) hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))" by (simp add: mult.commute) thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce qed have "d > 0" using d_elem by simp hence "ord a div gcd n (ord a) ≤ d" using dvd_d by (simp add : Nat.dvd_imp_le) hence False using d_lt by simp } hence ord_gcd_min: "⋀ d . d ∈ {d ∈ {1..order G}. (a(^)n) (^) d = 𝟭} ⟹ d≥ord a div gcd n (ord a)" by fastforce have fin:"finite {d ∈ {1..order G}. (a(^)n) (^) d = 𝟭}" by auto thus ?thesis using Min_eqI[OF fin ord_gcd_min ord_gcd_elem] unfolding ord_def by simp qed lemma ord_1_eq_1 : assumes "finite (carrier G)" shows "ord 𝟭 = 1" using assms ord_ge_1 ord_min[of 1 𝟭] by force theorem lagrange_dvd: assumes "finite(carrier G)" "subgroup H G" shows "(card H) dvd (order G)" using assms by (simp add: lagrange[symmetric]) lemma element_generates_subgroup: assumes finite[simp]: "finite (carrier G)" assumes a[simp]: "a ∈ carrier G" shows "subgroup {a (^) i | i. i ∈ {0 .. ord a - 1}} G" proof show "{a(^)i | i. i ∈ {0 .. ord a - 1} } ⊆ carrier G" by auto next fix x y assume A: "x ∈ {a(^)i | i. i ∈ {0 .. ord a - 1}}" "y ∈ {a(^)i | i. i ∈ {0 .. ord a - 1}}" obtain i::nat where i:"x = a(^)i" and i2:"i ∈ UNIV" using A by auto obtain j::nat where j:"y = a(^)j" and j2:"j ∈ UNIV" using A by auto have "a(^)(i+j) ∈ {a(^)i | i. i ∈ {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto thus "x ⊗ y ∈ {a(^)i | i. i ∈ {0 .. ord a - 1}}" using i j a ord_elems assms by (auto simp add: nat_pow_mult) next show "𝟭 ∈ {a(^)i | i. i ∈ {0 .. ord a - 1}}" by force next fix x assume x: "x ∈ {a(^)i | i. i ∈ {0 .. ord a - 1}}" hence x_in_carrier: "x ∈ carrier G" by auto then obtain d::nat where d:"x (^) d = 𝟭" and "d≥1" using finite_group_elem_finite_ord by auto have inv_1:"x(^)(d - 1) ⊗ x = 𝟭" using `d≥1` d nat_pow_Suc[of x "d - 1"] by simp have elem:"x (^) (d - 1) ∈ {a(^)i | i. i ∈ {0 .. ord a - 1}}" proof - obtain i::nat where i:"x = a(^)i" using x by auto hence "x(^)(d - 1) ∈ {a(^)i | i. i ∈ (UNIV::nat set)}" by (auto simp add: nat_pow_pow) thus ?thesis using ord_elems[of a] by auto qed have inv:"inv x = x(^)(d - 1)" using inv_equality[OF inv_1] x_in_carrier by blast thus "inv x ∈ {a(^)i | i. i ∈ {0 .. ord a - 1}}" using elem inv by auto qed lemma ord_dvd_group_order : assumes finite[simp]: "finite (carrier G)" assumes a[simp]: "a ∈ carrier G" shows "ord a dvd order G" proof - have card_dvd:"card {a(^)i | i. i ∈ {0 .. ord a - 1}} dvd card (carrier G)" using lagrange_dvd element_generates_subgroup unfolding order_def by simp have "inj_on (λ i . a(^)i) {0..ord a - 1}" using ord_inj by simp hence cards_eq:"card ( (λ i . a(^)i) ` {0..ord a - 1}) = card {0..ord a - 1}" using card_image[of "λ i . a(^)i" "{0..ord a - 1}"] by auto have "(λ i . a(^)i) ` {0..ord a - 1} = {a(^)i | i. i ∈ {0..ord a - 1}}" by auto hence "card {a(^)i | i. i ∈ {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp also have "… = ord a" using ord_ge_1[of a] by simp finally show ?thesis using card_dvd by (simp add: order_def) qed end section {* Number of Roots of a Polynomial *} text_raw {* \label{sec:number-roots} *} definition mult_of :: "('a, 'b) ring_scheme ⇒ 'a monoid" where "mult_of R ≡ ⦇ carrier = carrier R - {𝟬⇘_{R⇙}}, mult = mult R, one = 𝟭⇘_{R⇙}⦈" lemma carrier_mult_of: "carrier (mult_of R) = carrier R - {𝟬⇘_{R⇙}}" by (simp add: mult_of_def) lemma mult_mult_of: "mult (mult_of R) = mult R" by (simp add: mult_of_def) lemma nat_pow_mult_of: "op (^)⇘_{mult_of R⇙}= (op (^)⇘_{R⇙}:: _ ⇒ nat ⇒ _)" by (simp add: mult_of_def fun_eq_iff nat_pow_def) lemma one_mult_of: "𝟭⇘_{mult_of R⇙}= 𝟭⇘_{R⇙}" by (simp add: mult_of_def) lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of context field begin lemma field_mult_group : shows "group (mult_of R)" apply (rule groupI) apply (auto simp: mult_of_simps m_assoc dest: integral) by (metis Diff_iff Units_inv_Units Units_l_inv field_Units singletonE) lemma finite_mult_of: "finite (carrier R) ⟹ finite (carrier (mult_of R))" by (auto simp: mult_of_simps) lemma order_mult_of: "finite (carrier R) ⟹ order (mult_of R) = order R - 1" unfolding order_def carrier_mult_of by (simp add: card.remove) end lemma (in monoid) Units_pow_closed : fixes d :: nat assumes "x ∈ Units G" shows "x (^) d ∈ Units G" by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow) lemma (in comm_monoid) is_monoid: shows "monoid G" by unfold_locales declare comm_monoid.is_monoid[intro?] lemma (in ring) r_right_minus_eq[simp]: assumes "a ∈ carrier R" "b ∈ carrier R" shows "a ⊖ b = 𝟬 ⟷ a = b" using assms by (metis a_minus_def add.inv_closed minus_equality r_neg) context UP_cring begin lemma is_UP_cring:"UP_cring R" by (unfold_locales) lemma is_UP_ring : shows "UP_ring R" by (unfold_locales) end context UP_domain begin lemma roots_bound: assumes f [simp]: "f ∈ carrier P" assumes f_not_zero: "f ≠ 𝟬⇘_{P⇙}" assumes finite: "finite (carrier R)" shows "finite {a ∈ carrier R . eval R R id a f = 𝟬} ∧ card {a ∈ carrier R . eval R R id a f = 𝟬} ≤ deg R f" using f f_not_zero proof (induction "deg R f" arbitrary: f) case 0 have "⋀x. eval R R id x f ≠ 𝟬" proof - fix x have "(⨁i∈{..deg R f}. id (coeff P f i) ⊗ x (^) i) ≠ 𝟬" using 0 lcoeff_nonzero_nonzero[where p = f] by simp thus "eval R R id x f ≠ 𝟬" using 0 unfolding eval_def P_def by simp qed then have *: "{a ∈ carrier R. eval R R (λa. a) a f = 𝟬} = {}" by (auto simp: id_def) show ?case by (simp add: *) next case (Suc x) show ?case proof (cases "∃ a ∈ carrier R . eval R R id a f = 𝟬") case True then obtain a where a_carrier[simp]: "a ∈ carrier R" and a_root:"eval R R id a f = 𝟬" by blast have R_not_triv: "carrier R ≠ {𝟬}" by (metis R.one_zeroI R.zero_not_one) obtain q where q:"(q ∈ carrier P)" and f:"f = (monom P 𝟭⇘_{R⇙}1 ⊖⇘_{ P⇙}monom P a 0) ⊗⇘_{P⇙}q ⊕⇘_{P⇙}monom P (eval R R id a f) 0" using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto hence lin_fac: "f = (monom P 𝟭⇘_{R⇙}1 ⊖⇘_{ P⇙}monom P a 0) ⊗⇘_{P⇙}q" using q by (simp add: a_root) have deg:"deg R (monom P 𝟭⇘_{R⇙}1 ⊖⇘_{ P⇙}monom P a 0) = 1" using a_carrier by (simp add: deg_minus_eq) hence mon_not_zero:"(monom P 𝟭⇘_{R⇙}1 ⊖⇘_{ P⇙}monom P a 0) ≠ 𝟬⇘_{P⇙}" by (fastforce simp del: r_right_minus_eq) have q_not_zero:"q ≠ 𝟬⇘_{P⇙}" using Suc by (auto simp add : lin_fac) hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q] by (simp add : lin_fac) hence q_IH:"finite {a ∈ carrier R . eval R R id a q = 𝟬} ∧ card {a ∈ carrier R . eval R R id a q = 𝟬} ≤ x" using Suc q q_not_zero by blast have subs:"{a ∈ carrier R . eval R R id a f = 𝟬} ⊆ {a ∈ carrier R . eval R R id a q = 𝟬} ∪ {a}" (is "?L ⊆ ?R ∪ {a}") using a_carrier `q ∈ _` by (auto simp: evalRR_simps lin_fac R.integral_iff) have "{a ∈ carrier R . eval R R id a f = 𝟬} ⊆ insert a {a ∈ carrier R . eval R R id a q = 𝟬}" using subs by auto hence "card {a ∈ carrier R . eval R R id a f = 𝟬} ≤ card (insert a {a ∈ carrier R . eval R R id a q = 𝟬})" using q_IH by (blast intro: card_mono) also have "… ≤ deg R f" using q_IH `Suc x = _` by (simp add: card_insert_if) finally show ?thesis using q_IH `Suc x = _` using finite by force next case False hence "card {a ∈ carrier R. eval R R id a f = 𝟬} = 0" using finite by auto also have "… ≤ deg R f" by simp finally show ?thesis using finite by auto qed qed end lemma (in domain) num_roots_le_deg : fixes p d :: nat assumes finite:"finite (carrier R)" assumes d_neq_zero : "d ≠ 0" shows "card {x ∈ carrier R. x (^) d = 𝟭} ≤ d" proof - let ?f = "monom (UP R) 𝟭⇘_{R⇙}d ⊖⇘_{ (UP R)⇙}monom (UP R) 𝟭⇘_{R⇙}0" have one_in_carrier:"𝟭 ∈ carrier R" by simp interpret R: UP_domain R "UP R" by (unfold_locales) have "deg R ?f = d" using d_neq_zero by (simp add: R.deg_minus_eq) hence f_not_zero:"?f ≠ 𝟬⇘_{UP R⇙}" using d_neq_zero by (auto simp add : R.deg_nzero_nzero) have roots_bound:"finite {a ∈ carrier R . eval R R id a ?f = 𝟬} ∧ card {a ∈ carrier R . eval R R id a ?f = 𝟬} ≤ deg R ?f" using finite by (intro R.roots_bound[OF _ f_not_zero]) simp have subs:"{x ∈ carrier R. x (^) d = 𝟭} ⊆ {a ∈ carrier R . eval R R id a ?f = 𝟬}" by (auto simp: R.evalRR_simps) then have "card {x ∈ carrier R. x (^) d = 𝟭} ≤ card {a ∈ carrier R. eval R R id a ?f = 𝟬}" using finite by (simp add : card_mono) thus ?thesis using `deg R ?f = d` roots_bound by linarith qed section {* The Multiplicative Group of a Field *} text_raw {* \label{sec:mult-group} *} text {* In this section we show that the multiplicative group of a finite field is generated by a single element, i.e. it is cyclic. The proof is inspired by the first proof given in the survey~\cite{conrad-cyclicity}. *} lemma (in group) pow_order_eq_1: assumes "finite (carrier G)" "x ∈ carrier G" shows "x (^) order G = 𝟭" using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one) (* XXX remove in AFP devel, replaced by div_eq_dividend_iff *) lemma nat_div_eq: "a ≠ 0 ⟹ (a :: nat) div b = a ⟷ b = 1" apply rule apply (cases "b = 0") apply simp_all apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3) done lemma (in group) assumes finite': "finite (carrier G)" assumes "a ∈ carrier G" shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a ⟷ coprime k (ord a)" (is "?L ⟷ ?R") proof assume A: ?L then show ?R using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem) next assume ?R then show ?L using ord_pow_dvd_ord_elem[OF assms, of k] by auto qed context field begin lemma num_elems_of_ord_eq_phi': assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)" and exists: "∃a∈carrier (mult_of R). group.ord (mult_of R) a = d" shows "card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d" proof - note mult_of_simps[simp] have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of) interpret G:group "mult_of R" rewrites "op (^)⇘_{mult_of R⇙}= (op (^) :: _ ⇒ nat ⇒ _)" and "𝟭⇘_{mult_of R⇙}= 𝟭" by (rule field_mult_group) simp_all from exists obtain a where a:"a ∈ carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d" by (auto simp add: card_gt_0_iff) have set_eq1:"{a(^)n| n. n ∈ {1 .. d}} = {x ∈ carrier (mult_of R). x (^) d = 𝟭}" proof (rule card_seteq) show "finite {x ∈ carrier (mult_of R). x (^) d = 𝟭}" using finite by auto show "{a(^)n| n. n ∈ {1 ..d}} ⊆ {x ∈ carrier (mult_of R). x(^)d = 𝟭}" proof fix x assume "x ∈ {a(^)n | n. n ∈ {1 .. d}}" then obtain n where n:"x = a(^)n ∧ n ∈ {1 .. d}" by auto have "x(^)d =(a(^)d)(^)n" using n a ord_a by (simp add:nat_pow_pow mult.commute) hence "x(^)d = 𝟭" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce thus "x ∈ {x ∈ carrier (mult_of R). x(^)d = 𝟭}" using G.nat_pow_closed[OF a] n by blast qed show "card {x ∈ carrier (mult_of R). x (^) d = 𝟭} ≤ card {a(^)n | n. n ∈ {1 .. d}}" proof - have *:"{a(^)n | n. n ∈ {1 .. d }} = ((λ n. a(^)n) ` {1 .. d})" by auto have "0 < order (mult_of R)" unfolding order_mult_of[OF finite] using card_mono[OF finite, of "{𝟬, 𝟭}"] by (simp add: order_def) have "card {x ∈ carrier (mult_of R). x (^) d = 𝟭} ≤ card {x ∈ carrier R. x (^) d = 𝟭}" using finite by (auto intro: card_mono) also have "… ≤ d" using `0 < order (mult_of R)` num_roots_le_deg[OF finite, of d] by (simp add : dvd_pos_nat[OF _ `d dvd order (mult_of R)`]) finally show ?thesis using G.ord_inj'[OF finite' a] ord_a * by (simp add: card_image) qed qed have set_eq2:"{x ∈ carrier (mult_of R) . group.ord (mult_of R) x = d} = (λ n . a(^)n) ` {n ∈ {1 .. d}. group.ord (mult_of R) (a(^)n) = d}" (is "?L = ?R") proof { fix x assume x:"x ∈ (carrier (mult_of R)) ∧ group.ord (mult_of R) x = d" hence "x ∈ {x ∈ carrier (mult_of R). x (^) d = 𝟭}" by (simp add: G.pow_ord_eq_1[OF finite', of x, symmetric]) then obtain n where n:"x = a(^)n ∧ n ∈ {1 .. d}" using set_eq1 by blast hence "x ∈ ?R" using x by fast } thus "?L ⊆ ?R" by blast show "?R ⊆ ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of) qed have "inj_on (λ n . a(^)n) {n ∈ {1 .. d}. group.ord (mult_of R) (a(^)n) = d}" using G.ord_inj'[OF finite' a, unfolded ord_a] unfolding inj_on_def by fast hence "card ((λn. a(^)n) ` {n ∈ {1 .. d}. group.ord (mult_of R) (a(^)n) = d}) = card {k ∈ {1 .. d}. group.ord (mult_of R) (a(^)k) = d}" using card_image by blast thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' `a ∈ _`, unfolded ord_a] by (simp add: phi'_def) qed end theorem (in field) finite_field_mult_group_has_gen : assumes finite:"finite (carrier R)" shows "∃ a ∈ carrier (mult_of R) . carrier (mult_of R) = {a(^)i | i::nat . i ∈ UNIV}" proof - note mult_of_simps[simp] have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of) interpret G: group "mult_of R" rewrites "op (^)⇘_{mult_of R⇙}= (op (^) :: _ ⇒ nat ⇒ _)" and "𝟭⇘_{mult_of R⇙}= 𝟭" by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def) let ?N = "λ x . card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = x}" have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{𝟬, 𝟭}"] by simp then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of) have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force have "(∑d | d dvd order (mult_of R). ?N d) = card (UN d:{d . d dvd order (mult_of R) }. {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d})" (is "_ = card ?U") using fin finite by (subst card_UN_disjoint) auto also have "?U = carrier (mult_of R)" proof { fix x assume x:"x ∈ carrier (mult_of R)" hence x':"x∈carrier (mult_of R)" by simp then have "group.ord (mult_of R) x dvd order (mult_of R)" using finite' G.ord_dvd_group_order[OF _ x'] by (simp add: order_mult_of) hence "x ∈ ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast } thus "carrier (mult_of R) ⊆ ?U" by blast qed auto also have "card ... = order (mult_of R)" using order_mult_of finite' by (simp add: order_def) finally have sum_Ns_eq: "(∑d | d dvd order (mult_of R). ?N d) = order (mult_of R)" . { fix d assume d:"d dvd order (mult_of R)" have "card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d} ≤ phi' d" proof cases assume "card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger next assume "card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d} ≠ 0" hence "∃a ∈ carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff) thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto qed } hence all_le:"⋀i. i ∈ {d. d dvd order (mult_of R) } ⟹ (λi. card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = i}) i ≤ (λi. phi' i) i" by fast hence le:"(∑i | i dvd order (mult_of R). ?N i) ≤ (∑i | i dvd order (mult_of R). phi' i)" using sum_mono[of "{d . d dvd order (mult_of R)}" "λi. card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger have "order (mult_of R) = (∑d | d dvd order (mult_of R). phi' d)" using * by (simp add: sum_phi'_factors) hence eq:"(∑i | i dvd order (mult_of R). ?N i) = (∑i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger have "⋀i. i ∈ {d. d dvd order (mult_of R) } ⟹ ?N i = (λi. phi' i) i" proof (rule ccontr) fix i assume i1:"i ∈ {d. d dvd order (mult_of R)}" and "?N i ≠ phi' i" hence "?N i = 0" using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff) moreover have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i]) ultimately have "?N i < phi' i" using phi'_nonzero by presburger hence "(∑i | i dvd order (mult_of R). ?N i) < (∑i | i dvd order (mult_of R). phi' i)" using sum_strict_mono_ex1[OF fin, of "?N" "λ i . phi' i"] i1 all_le by auto thus False using eq by force qed hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero) then obtain a where a:"a ∈ carrier (mult_of R)" and a_ord:"group.ord (mult_of R) a = order (mult_of R)" by (auto simp add: card_gt_0_iff) hence set_eq:"{a(^)i | i::nat. i ∈ UNIV} = (λx. a(^)x) ` {0 .. group.ord (mult_of R) a - 1}" using G.ord_elems[OF finite'] by auto have card_eq:"card ((λx. a(^)x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}" by (intro card_image G.ord_inj finite' a) hence "card ((λ x . a(^)x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}" using assms by (simp add: card_eq a_ord) hence card_R_minus_1:"card {a(^)i | i::nat. i ∈ UNIV} = order (mult_of R)" using * by (subst set_eq) auto have **:"{a(^)i | i::nat. i ∈ UNIV} ⊆ carrier (mult_of R)" using G.nat_pow_closed[OF a] by auto with _ have "carrier (mult_of R) = {a(^)i|i::nat. i ∈ UNIV}" by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I) thus ?thesis using a by blast qed end