src/HOL/Algebra/Multiplicative_Group.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (20 months ago) changeset 67003 49850a679c2c parent 66500 ba94aeb02fbc child 67051 e7e54a0b9197 permissions -rw-r--r--
more robust sorted_entries;
 haftmann@65416  1 (* Title: HOL/Algebra/Multiplicative_Group.thy  haftmann@65416  2  Author: Simon Wimmer  haftmann@65416  3  Author: Lars Noschinski  haftmann@65416  4 *)  haftmann@65416  5 haftmann@65416  6 theory Multiplicative_Group  haftmann@65416  7 imports  haftmann@65416  8  Complex_Main  haftmann@65416  9  Group  haftmann@65416  10  More_Group  haftmann@65416  11  More_Finite_Product  haftmann@65416  12  Coset  haftmann@65416  13  UnivPoly  haftmann@65416  14 begin  haftmann@65416  15 haftmann@65416  16 section {* Simplification Rules for Polynomials *}  haftmann@65416  17 text_raw {* \label{sec:simp-rules} *}  haftmann@65416  18 haftmann@65416  19 lemma (in ring_hom_cring) hom_sub[simp]:  haftmann@65416  20  assumes "x \ carrier R" "y \ carrier R"  haftmann@65416  21  shows "h (x \ y) = h x \\<^bsub>S\<^esub> h y"  haftmann@65416  22  using assms by (simp add: R.minus_eq S.minus_eq)  haftmann@65416  23 haftmann@65416  24 context UP_ring begin  haftmann@65416  25 haftmann@65416  26 lemma deg_nzero_nzero:  haftmann@65416  27  assumes deg_p_nzero: "deg R p \ 0"  haftmann@65416  28  shows "p \ \\<^bsub>P\<^esub>"  haftmann@65416  29  using deg_zero deg_p_nzero by auto  haftmann@65416  30 haftmann@65416  31 lemma deg_add_eq:  haftmann@65416  32  assumes c: "p \ carrier P" "q \ carrier P"  haftmann@65416  33  assumes "deg R q \ deg R p"  haftmann@65416  34  shows "deg R (p \\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"  haftmann@65416  35 proof -  haftmann@65416  36  let ?m = "max (deg R p) (deg R q)"  haftmann@65416  37  from assms have "coeff P p ?m = \ \ coeff P q ?m \ \"  haftmann@65416  38  by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1)  haftmann@65416  39  then have "coeff P (p \\<^bsub>P\<^esub> q) ?m \ \"  haftmann@65416  40  using assms by auto  haftmann@65416  41  then have "deg R (p \\<^bsub>P\<^esub> q) \ ?m"  haftmann@65416  42  using assms by (blast intro: deg_belowI)  haftmann@65416  43  with deg_add[OF c] show ?thesis by arith  haftmann@65416  44 qed  haftmann@65416  45 haftmann@65416  46 lemma deg_minus_eq:  haftmann@65416  47  assumes "p \ carrier P" "q \ carrier P" "deg R q \ deg R p"  haftmann@65416  48  shows "deg R (p \\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"  haftmann@65416  49  using assms by (simp add: deg_add_eq a_minus_def)  haftmann@65416  50 haftmann@65416  51 end  haftmann@65416  52 haftmann@65416  53 context UP_cring begin  haftmann@65416  54 haftmann@65416  55 lemma evalRR_add:  haftmann@65416  56  assumes "p \ carrier P" "q \ carrier P"  haftmann@65416  57  assumes x:"x \ carrier R"  haftmann@65416  58  shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"  haftmann@65416  59 proof -  haftmann@65416  60  interpret UP_pre_univ_prop R R id by unfold_locales simp  haftmann@65416  61  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])  haftmann@65416  62  show ?thesis using assms by simp  haftmann@65416  63 qed  haftmann@65416  64 haftmann@65416  65 lemma evalRR_sub:  haftmann@65416  66  assumes "p \ carrier P" "q \ carrier P"  haftmann@65416  67  assumes x:"x \ carrier R"  haftmann@65416  68  shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"  haftmann@65416  69 proof -  haftmann@65416  70  interpret UP_pre_univ_prop R R id by unfold_locales simp  haftmann@65416  71  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])  haftmann@65416  72  show ?thesis using assms by simp  haftmann@65416  73 qed  haftmann@65416  74 haftmann@65416  75 lemma evalRR_mult:  haftmann@65416  76  assumes "p \ carrier P" "q \ carrier P"  haftmann@65416  77  assumes x:"x \ carrier R"  haftmann@65416  78  shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"  haftmann@65416  79 proof -  haftmann@65416  80  interpret UP_pre_univ_prop R R id by unfold_locales simp  haftmann@65416  81  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])  haftmann@65416  82  show ?thesis using assms by simp  haftmann@65416  83 qed  haftmann@65416  84 haftmann@65416  85 lemma evalRR_monom:  haftmann@65416  86  assumes a: "a \ carrier R" and x: "x \ carrier R"  haftmann@65416  87  shows "eval R R id x (monom P a d) = a \ x (^) d"  haftmann@65416  88 proof -  haftmann@65416  89  interpret UP_pre_univ_prop R R id by unfold_locales simp  haftmann@65416  90  show ?thesis using assms by (simp add: eval_monom)  haftmann@65416  91 qed  haftmann@65416  92 haftmann@65416  93 lemma evalRR_one:  haftmann@65416  94  assumes x: "x \ carrier R"  haftmann@65416  95  shows "eval R R id x \\<^bsub>P\<^esub> = \"  haftmann@65416  96 proof -  haftmann@65416  97  interpret UP_pre_univ_prop R R id by unfold_locales simp  haftmann@65416  98  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])  haftmann@65416  99  show ?thesis using assms by simp  haftmann@65416  100 qed  haftmann@65416  101 haftmann@65416  102 lemma carrier_evalRR:  haftmann@65416  103  assumes x: "x \ carrier R" and "p \ carrier P"  haftmann@65416  104  shows "eval R R id x p \ carrier R"  haftmann@65416  105 proof -  haftmann@65416  106  interpret UP_pre_univ_prop R R id by unfold_locales simp  haftmann@65416  107  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])  haftmann@65416  108  show ?thesis using assms by simp  haftmann@65416  109 qed  haftmann@65416  110 haftmann@65416  111 lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR  haftmann@65416  112 haftmann@65416  113 end  haftmann@65416  114 haftmann@65416  115 haftmann@65416  116 haftmann@65416  117 section {* Properties of the Euler @{text \}-function *}  haftmann@65416  118 text_raw {* \label{sec:euler-phi} *}  haftmann@65416  119 haftmann@65416  120 text{*  haftmann@65416  121  In this section we prove that for every positive natural number the equation  haftmann@65416  122  $\sum_{d | n}^n \varphi(d) = n$ holds.  haftmann@65416  123 *}  haftmann@65416  124 haftmann@65416  125 lemma dvd_div_ge_1 :  haftmann@65416  126  fixes a b :: nat  haftmann@65416  127  assumes "a \ 1" "b dvd a"  haftmann@65416  128  shows "a div b \ 1"  haftmann@65416  129 proof -  haftmann@65416  130  from \b dvd a\ obtain c where "a = b * c" ..  haftmann@65416  131  with \a \ 1\ show ?thesis by simp  haftmann@65416  132 qed  haftmann@65416  133 haftmann@65416  134 lemma dvd_nat_bounds :  haftmann@65416  135  fixes n p :: nat  haftmann@65416  136  assumes "p > 0" "n dvd p"  haftmann@65416  137  shows "n > 0 \ n \ p"  haftmann@65416  138  using assms by (simp add: dvd_pos_nat dvd_imp_le)  haftmann@65416  139 haftmann@65416  140 (* Deviates from the definition given in the library in number theory *)  haftmann@65416  141 definition phi' :: "nat => nat"  haftmann@65416  142  where "phi' m = card {x. 1 \ x \ x \ m \ gcd x m = 1}"  haftmann@65416  143 haftmann@66500  144 notation (latex output)  haftmann@65416  145  phi' ("\ _")  haftmann@65416  146 haftmann@65416  147 lemma phi'_nonzero :  haftmann@65416  148  assumes "m > 0"  haftmann@65416  149  shows "phi' m > 0"  haftmann@65416  150 proof -  haftmann@65416  151  have "1 \ {x. 1 \ x \ x \ m \ gcd x m = 1}" using assms by simp  haftmann@65416  152  hence "card {x. 1 \ x \ x \ m \ gcd x m = 1} > 0" by (auto simp: card_gt_0_iff)  haftmann@65416  153  thus ?thesis unfolding phi'_def by simp  haftmann@65416  154 qed  haftmann@65416  155 haftmann@65416  156 lemma dvd_div_eq_1:  haftmann@65416  157  fixes a b c :: nat  haftmann@65416  158  assumes "c dvd a" "c dvd b" "a div c = b div c"  haftmann@65416  159  shows "a = b" using assms dvd_mult_div_cancel[OF c dvd a] dvd_mult_div_cancel[OF c dvd b]  haftmann@65416  160  by presburger  haftmann@65416  161 haftmann@65416  162 lemma dvd_div_eq_2:  haftmann@65416  163  fixes a b c :: nat  haftmann@65416  164  assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b"  haftmann@65416  165  shows "a = b"  haftmann@65416  166  proof -  haftmann@65416  167  have "a > 0" "a \ c" using dvd_nat_bounds[OF assms(1-2)] by auto  haftmann@65416  168  have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce  haftmann@65416  169  also have "\ = b*(c div a)" using assms dvd_mult_div_cancel by fastforce  haftmann@65416  170  finally show "a = b" using c>0 dvd_div_ge_1[OF _ a dvd c] by fastforce  haftmann@65416  171 qed  haftmann@65416  172 haftmann@65416  173 lemma div_mult_mono:  haftmann@65416  174  fixes a b c :: nat  haftmann@65416  175  assumes "a > 0" "a\d"  haftmann@65416  176  shows "a * b div d \ b"  haftmann@65416  177 proof -  haftmann@65416  178  have "a*b div d \ b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger  haftmann@65416  179  thus ?thesis using assms by force  haftmann@65416  180 qed  haftmann@65416  181 haftmann@65416  182 text{*  haftmann@65416  183  We arrive at the main result of this section:  haftmann@65416  184  For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.  haftmann@65416  185 haftmann@65416  186  The outline of the proof for this lemma is as follows:  haftmann@65416  187  We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$.  haftmann@65416  188  We analyze the reduced form $a/d = m/n$ for any of those fractions.  haftmann@65416  189  We want to know how many fractions $m/n$ have the reduced form denominator $d$.  haftmann@65416  190  The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$.  haftmann@65416  191  Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. @{term "gcd a d = 1"}.  haftmann@65416  192  This number is exactly @{term "phi' d"}.  haftmann@65416  193 haftmann@65416  194  Finally, by counting the fractions $m/n$ according to their reduced form denominator,  haftmann@65416  195  we get: @{term [display] "(\d | d dvd n . phi' d) = n"}.  haftmann@65416  196  To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$  haftmann@65416  197  \begin{itemize}  haftmann@65416  198  \item the set of reduced form numerators @{term "{a. (1::nat) \ a \ a \ d \ coprime a d}"}  haftmann@65416  199  \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$,  haftmann@65416  200  i.e. the set @{term "{m \ {1::nat .. n}. n div gcd m n = d}"}  haftmann@65416  201  \end{itemize}  haftmann@65416  202  We show that @{term "\a. a*n div d"} with the inverse @{term "\a. a div gcd a n"} is  haftmann@65416  203  a bijection between theses sets, thus yielding the equality  haftmann@65416  204  @{term [display] "phi' d = card {m \ {1 .. n}. n div gcd m n = d}"}  haftmann@65416  205  This gives us  haftmann@65416  206  @{term [display] "(\d | d dvd n . phi' d)  haftmann@65416  207  = card (\d \ {d. d dvd n}. {m \ {1 .. n}. n div gcd m n = d})"}  haftmann@65416  208  and by showing  haftmann@65416  209  @{term "(\d \ {d. d dvd n}. {m \ {1::nat .. n}. n div gcd m n = d}) \ {1 .. n}"}  haftmann@65416  210  (this is our counting argument) the thesis follows.  haftmann@65416  211 *}  haftmann@65416  212 lemma sum_phi'_factors :  haftmann@65416  213  fixes n :: nat  haftmann@65416  214  assumes "n > 0"  haftmann@65416  215  shows "(\d | d dvd n. phi' d) = n"  haftmann@65416  216 proof -  haftmann@65416  217  { fix d assume "d dvd n" then obtain q where q: "n = d * q" ..  haftmann@65416  218  have "card {a. 1 \ a \ a \ d \ coprime a d} = card {m \ {1 .. n}. n div gcd m n = d}"  haftmann@65416  219  (is "card ?RF = card ?F")  haftmann@65416  220  proof (rule card_bij_eq)  haftmann@65416  221  { fix a b assume "a * n div d = b * n div d"  haftmann@65416  222  hence "a * (n div d) = b * (n div d)"  haftmann@65416  223  using dvd_div_mult[OF d dvd n] by (fastforce simp add: mult.commute)  haftmann@65416  224  hence "a = b" using dvd_div_ge_1[OF _ d dvd n] n>0  haftmann@65416  225  by (simp add: mult.commute nat_mult_eq_cancel1)  haftmann@65416  226  } thus "inj_on (\a. a*n div d) ?RF" unfolding inj_on_def by blast  haftmann@65416  227  { fix a assume a:"a\?RF"  haftmann@65416  228  hence "a * (n div d) \ 1" using n>0 dvd_div_ge_1[OF _ d dvd n] by simp  haftmann@65416  229  hence ge_1:"a * n div d \ 1" by (simp add: d dvd n div_mult_swap)  haftmann@65416  230  have le_n:"a * n div d \ n" using div_mult_mono a by simp  haftmann@65416  231  have "gcd (a * n div d) n = n div d * gcd a d"  haftmann@65416  232  by (simp add: gcd_mult_distrib_nat q ac_simps)  haftmann@65416  233  hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp  haftmann@65416  234  hence "a * n div d \ ?F"  haftmann@65416  235  using ge_1 le_n by (fastforce simp add: d dvd n dvd_mult_div_cancel)  haftmann@65416  236  } thus "(\a. a*n div d)  ?RF \ ?F" by blast  haftmann@65416  237  { fix m l assume A: "m \ ?F" "l \ ?F" "m div gcd m n = l div gcd l n"  haftmann@65416  238  hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce  haftmann@65416  239  hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce  haftmann@65416  240  } thus "inj_on (\a. a div gcd a n) ?F" unfolding inj_on_def by blast  haftmann@65416  241  { fix m assume "m \ ?F"  haftmann@65416  242  hence "m div gcd m n \ ?RF" using dvd_div_ge_1  haftmann@65416  243  by (fastforce simp add: div_le_mono div_gcd_coprime)  haftmann@65416  244  } thus "(\a. a div gcd a n)  ?F \ ?RF" by blast  haftmann@65416  245  qed force+  haftmann@65416  246  } hence phi'_eq:"\d. d dvd n \ phi' d = card {m \ {1 .. n}. n div gcd m n = d}"  haftmann@65416  247  unfolding phi'_def by presburger  haftmann@65416  248  have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF n>0] by force  haftmann@65416  249  have "(\d | d dvd n. phi' d)  haftmann@65416  250  = card (\d \ {d. d dvd n}. {m \ {1 .. n}. n div gcd m n = d})"  haftmann@65416  251  using card_UN_disjoint[OF fin, of "(\d. {m \ {1 .. n}. n div gcd m n = d})"] phi'_eq  haftmann@65416  252  by fastforce  haftmann@65416  253  also have "(\d \ {d. d dvd n}. {m \ {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R")  haftmann@65416  254  proof  haftmann@65416  255  show "?L \ ?R"  haftmann@65416  256  proof  haftmann@65416  257  fix m assume m: "m \ ?R"  haftmann@65416  258  thus "m \ ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]  haftmann@65416  259  by (simp add: dvd_mult_div_cancel)  haftmann@65416  260  qed  haftmann@65416  261  qed fastforce  haftmann@65416  262  finally show ?thesis by force  haftmann@65416  263 qed  haftmann@65416  264 haftmann@65416  265 section {* Order of an Element of a Group *}  haftmann@65416  266 text_raw {* \label{sec:order-elem} *}  haftmann@65416  267 haftmann@65416  268 haftmann@65416  269 context group begin  haftmann@65416  270 haftmann@65416  271 lemma pow_eq_div2 :  haftmann@65416  272  fixes m n :: nat  haftmann@65416  273  assumes x_car: "x \ carrier G"  haftmann@65416  274  assumes pow_eq: "x (^) m = x (^) n"  haftmann@65416  275  shows "x (^) (m - n) = \"  haftmann@65416  276 proof (cases "m < n")  haftmann@65416  277  case False  haftmann@65416  278  have "\ \ x (^) m = x (^) m" by (simp add: x_car)  haftmann@65416  279  also have "\ = x (^) (m - n) \ x (^) n"  haftmann@65416  280  using False by (simp add: nat_pow_mult x_car)  haftmann@65416  281  also have "\ = x (^) (m - n) \ x (^) m"  haftmann@65416  282  by (simp add: pow_eq)  haftmann@65416  283  finally show ?thesis by (simp add: x_car)  haftmann@65416  284 qed simp  haftmann@65416  285 haftmann@65416  286 definition ord where "ord a = Min {d \ {1 .. order G} . a (^) d = \}"  haftmann@65416  287 haftmann@65416  288 lemma  haftmann@65416  289  assumes finite:"finite (carrier G)"  haftmann@65416  290  assumes a:"a \ carrier G"  haftmann@65416  291  shows ord_ge_1: "1 \ ord a" and ord_le_group_order: "ord a \ order G"  haftmann@65416  292  and pow_ord_eq_1: "a (^) ord a = \"  haftmann@65416  293 proof -  haftmann@65416  294  have "\inj_on (\x. a (^) x) {0 .. order G}"  haftmann@65416  295  proof (rule notI)  haftmann@65416  296  assume A: "inj_on (\x. a (^) x) {0 .. order G}"  haftmann@65416  297  have "order G + 1 = card {0 .. order G}" by simp  haftmann@65416  298  also have "\ = card ((\x. a (^) x)  {0 .. order G})" (is "_ = card ?S")  haftmann@65416  299  using A by (simp add: card_image)  haftmann@65416  300  also have "?S = {a (^) x | x. x \ {0 .. order G}}" by blast  haftmann@65416  301  also have "\ \ carrier G" (is "?S \ _") using a by blast  haftmann@65416  302  then have "card ?S \ order G" unfolding order_def  haftmann@65416  303  by (rule card_mono[OF finite])  haftmann@65416  304  finally show False by arith  haftmann@65416  305  qed  haftmann@65416  306 haftmann@65416  307  then obtain x y where x_y:"x \ y" "x \ {0 .. order G}" "y \ {0 .. order G}"  haftmann@65416  308  "a (^) x = a (^) y" unfolding inj_on_def by blast  haftmann@65416  309  obtain d where "1 \ d" "a (^) d = \" "d \ order G"  haftmann@65416  310  proof cases  haftmann@65416  311  assume "y < x" with x_y show ?thesis  haftmann@65416  312  by (intro that[where d="x - y"]) (auto simp add: pow_eq_div2[OF a])  haftmann@65416  313  next  haftmann@65416  314  assume "\y < x" with x_y show ?thesis  haftmann@65416  315  by (intro that[where d="y - x"]) (auto simp add: pow_eq_div2[OF a])  haftmann@65416  316  qed  haftmann@65416  317  hence "ord a \ {d \ {1 .. order G} . a (^) d = \}"  haftmann@65416  318  unfolding ord_def using Min_in[of "{d \ {1 .. order G} . a (^) d = \}"]  haftmann@65416  319  by fastforce  haftmann@65416  320  then show "1 \ ord a" and "ord a \ order G" and "a (^) ord a = \"  haftmann@65416  321  by (auto simp: order_def)  haftmann@65416  322 qed  haftmann@65416  323 haftmann@65416  324 lemma finite_group_elem_finite_ord :  haftmann@65416  325  assumes "finite (carrier G)" "x \ carrier G"  haftmann@65416  326  shows "\ d::nat. d \ 1 \ x (^) d = \"  haftmann@65416  327  using assms ord_ge_1 pow_ord_eq_1 by auto  haftmann@65416  328 haftmann@65416  329 lemma ord_min:  haftmann@65416  330  assumes "finite (carrier G)" "1 \ d" "a \ carrier G" "a (^) d = \" shows "ord a \ d"  haftmann@65416  331 proof -  haftmann@65416  332  def Ord \ "{d \ {1..order G}. a (^) d = \}"  haftmann@65416  333  have fin: "finite Ord" by (auto simp: Ord_def)  haftmann@65416  334  have in_ord: "ord a \ Ord"  haftmann@65416  335  using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)  haftmann@65416  336  then have "Ord \ {}" by auto  haftmann@65416  337 haftmann@65416  338  show ?thesis  haftmann@65416  339  proof (cases "d \ order G")  haftmann@65416  340  case True  haftmann@65416  341  then have "d \ Ord" using assms by (auto simp: Ord_def)  haftmann@65416  342  with fin in_ord show ?thesis  haftmann@65416  343  unfolding ord_def Ord_def[symmetric] by simp  haftmann@65416  344  next  haftmann@65416  345  case False  haftmann@65416  346  then show ?thesis using in_ord by (simp add: Ord_def)  haftmann@65416  347  qed  haftmann@65416  348 qed  haftmann@65416  349 haftmann@65416  350 lemma ord_inj :  haftmann@65416  351  assumes finite: "finite (carrier G)"  haftmann@65416  352  assumes a: "a \ carrier G"  haftmann@65416  353  shows "inj_on (\ x . a (^) x) {0 .. ord a - 1}"  haftmann@65416  354 proof (rule inj_onI, rule ccontr)  haftmann@65416  355  fix x y assume A: "x \ {0 .. ord a - 1}" "y \ {0 .. ord a - 1}" "a (^) x= a (^) y" "x \ y"  haftmann@65416  356 haftmann@65416  357  have "finite {d \ {1..order G}. a (^) d = \}" by auto  haftmann@65416  358 haftmann@65416  359  { fix x y assume A: "x < y" "x \ {0 .. ord a - 1}" "y \ {0 .. ord a - 1}"  haftmann@65416  360  "a (^) x = a (^) y"  haftmann@65416  361  hence "y - x < ord a" by auto  haftmann@65416  362  also have "\ \ order G" using assms by (simp add: ord_le_group_order)  haftmann@65416  363  finally have y_x_range:"y - x \ {1 .. order G}" using A by force  haftmann@65416  364  have "a (^) (y-x) = \" using a A by (simp add: pow_eq_div2)  haftmann@65416  365 haftmann@65416  366  hence y_x:"y - x \ {d \ {1.. order G}. a (^) d = \}" using y_x_range by blast  haftmann@65416  367  have "min (y - x) (ord a) = ord a"  haftmann@65416  368  using Min.in_idem[OF finite {d \ {1 .. order G} . a (^) d = \} y_x] ord_def by auto  haftmann@65416  369  with y - x < ord a have False by linarith  haftmann@65416  370  }  haftmann@65416  371  note X = this  haftmann@65416  372 haftmann@65416  373  { assume "x < y" with A X have False by blast }  haftmann@65416  374  moreover  haftmann@65416  375  { assume "x > y" with A X have False by metis }  haftmann@65416  376  moreover  haftmann@65416  377  { assume "x = y" then have False using A by auto}  haftmann@65416  378  ultimately  haftmann@65416  379  show False by fastforce  haftmann@65416  380 qed  haftmann@65416  381 haftmann@65416  382 lemma ord_inj' :  haftmann@65416  383  assumes finite: "finite (carrier G)"  haftmann@65416  384  assumes a: "a \ carrier G"  haftmann@65416  385  shows "inj_on (\ x . a (^) x) {1 .. ord a}"  haftmann@65416  386 proof (rule inj_onI, rule ccontr)  haftmann@65416  387  fix x y :: nat  haftmann@65416  388  assume A:"x \ {1 .. ord a}" "y \ {1 .. ord a}" "a (^) x = a (^) y" "x\y"  haftmann@65416  389  { assume "x < ord a" "y < ord a"  haftmann@65416  390  hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce  haftmann@65416  391  }  haftmann@65416  392  moreover  haftmann@65416  393  { assume "x = ord a" "y < ord a"  haftmann@65416  394  hence "a (^) y = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto  haftmann@65416  395  hence "y=0" using ord_inj[OF assms] y < ord a unfolding inj_on_def by force  haftmann@65416  396  hence False using A by fastforce  haftmann@65416  397  }  haftmann@65416  398  moreover  haftmann@65416  399  { assume "y = ord a" "x < ord a"  haftmann@65416  400  hence "a (^) x = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto  haftmann@65416  401  hence "x=0" using ord_inj[OF assms] x < ord a unfolding inj_on_def by force  haftmann@65416  402  hence False using A by fastforce  haftmann@65416  403  }  haftmann@65416  404  ultimately show False using A by force  haftmann@65416  405 qed  haftmann@65416  406 haftmann@65416  407 lemma ord_elems :  haftmann@65416  408  assumes "finite (carrier G)" "a \ carrier G"  haftmann@65416  409  shows "{a(^)x | x. x \ (UNIV :: nat set)} = {a(^)x | x. x \ {0 .. ord a - 1}}" (is "?L = ?R")  haftmann@65416  410 proof  haftmann@65416  411  show "?R \ ?L" by blast  haftmann@65416  412  { fix y assume "y \ ?L"  haftmann@65416  413  then obtain x::nat where x:"y = a(^)x" by auto  haftmann@65416  414  def r \ "x mod ord a"  haftmann@65416  415  then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger  haftmann@65416  416  hence "y = (a(^)ord a)(^)q \ a(^)r"  haftmann@65416  417  using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)  haftmann@65416  418  hence "y = a(^)r" using assms by (simp add: pow_ord_eq_1)  haftmann@65416  419  have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)  haftmann@65416  420  hence "r \ {0 .. ord a - 1}" by (force simp: r_def)  haftmann@65416  421  hence "y \ {a(^)x | x. x \ {0 .. ord a - 1}}" using y=a(^)r by blast  haftmann@65416  422  }  haftmann@65416  423  thus "?L \ ?R" by auto  haftmann@65416  424 qed  haftmann@65416  425 haftmann@65416  426 lemma ord_dvd_pow_eq_1 :  haftmann@65416  427  assumes "finite (carrier G)" "a \ carrier G" "a (^) k = \"  haftmann@65416  428  shows "ord a dvd k"  haftmann@65416  429 proof -  haftmann@65416  430  def r \ "k mod ord a"  haftmann@65416  431  then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger  haftmann@65416  432  hence "a(^)k = (a(^)ord a)(^)q \ a(^)r"  haftmann@65416  433  using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)  haftmann@65416  434  hence "a(^)k = a(^)r" using assms by (simp add: pow_ord_eq_1)  haftmann@65416  435  hence "a(^)r = \" using assms(3) by simp  haftmann@65416  436  have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)  haftmann@65416  437  hence "r = 0" using a(^)r = \ ord_def[of a] ord_min[of r a] assms(1-2) by linarith  haftmann@65416  438  thus ?thesis using q by simp  haftmann@65416  439 qed  haftmann@65416  440 haftmann@65416  441 lemma dvd_gcd :  haftmann@65416  442  fixes a b :: nat  haftmann@65416  443  obtains q where "a * (b div gcd a b) = b*q"  haftmann@65416  444 proof  haftmann@65416  445  have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add: div_mult_swap dvd_div_mult)  haftmann@65416  446  also have "\ = b * (a div gcd a b)" by simp  haftmann@65416  447  finally show "a * (b div gcd a b) = b * (a div gcd a b) " .  haftmann@65416  448 qed  haftmann@65416  449 haftmann@65416  450 lemma ord_pow_dvd_ord_elem :  haftmann@65416  451  assumes finite[simp]: "finite (carrier G)"  haftmann@65416  452  assumes a[simp]:"a \ carrier G"  haftmann@65416  453  shows "ord (a(^)n) = ord a div gcd n (ord a)"  haftmann@65416  454 proof -  haftmann@65416  455  have "(a(^)n) (^) ord a = (a (^) ord a) (^) n"  haftmann@65416  456  by (simp add: mult.commute nat_pow_pow)  haftmann@65416  457  hence "(a(^)n) (^) ord a = \" by (simp add: pow_ord_eq_1)  haftmann@65416  458  obtain q where "n * (ord a div gcd n (ord a)) = ord a * q" by (rule dvd_gcd)  haftmann@65416  459  hence "(a(^)n) (^) (ord a div gcd n (ord a)) = (a (^) ord a)(^)q" by (simp add : nat_pow_pow)  haftmann@65416  460  hence pow_eq_1: "(a(^)n) (^) (ord a div gcd n (ord a)) = \"  haftmann@65416  461  by (auto simp add : pow_ord_eq_1[of a])  haftmann@65416  462  have "ord a \ 1" using ord_ge_1 by simp  haftmann@65416  463  have ge_1:"ord a div gcd n (ord a) \ 1"  haftmann@65416  464  proof -  haftmann@65416  465  have "gcd n (ord a) dvd ord a" by blast  haftmann@65416  466  thus ?thesis by (rule dvd_div_ge_1[OF ord a \ 1])  haftmann@65416  467  qed  haftmann@65416  468  have "ord a \ order G" by (simp add: ord_le_group_order)  haftmann@65416  469  have "ord a div gcd n (ord a) \ order G"  haftmann@65416  470  proof -  haftmann@65416  471  have "ord a div gcd n (ord a) \ ord a" by simp  haftmann@65416  472  thus ?thesis using ord a \ order G by linarith  haftmann@65416  473  qed  haftmann@65416  474  hence ord_gcd_elem:"ord a div gcd n (ord a) \ {d \ {1..order G}. (a(^)n) (^) d = \}"  haftmann@65416  475  using ge_1 pow_eq_1 by force  haftmann@65416  476  { fix d :: nat  haftmann@65416  477  assume d_elem:"d \ {d \ {1..order G}. (a(^)n) (^) d = \}"  haftmann@65416  478  assume d_lt:"d < ord a div gcd n (ord a)"  haftmann@65416  479  hence pow_nd:"a(^)(n*d) = \" using d_elem  haftmann@65416  480  by (simp add : nat_pow_pow)  haftmann@65416  481  hence "ord a dvd n*d" using assms by (auto simp add : ord_dvd_pow_eq_1)  haftmann@65416  482  then obtain q where "ord a * q = n*d" by (metis dvd_mult_div_cancel)  haftmann@65416  483  hence prod_eq:"(ord a div gcd n (ord a)) * q = (n div gcd n (ord a)) * d"  haftmann@65416  484  by (simp add: dvd_div_mult)  haftmann@65416  485  have cp:"coprime (ord a div gcd n (ord a)) (n div gcd n (ord a))"  haftmann@65416  486  proof -  haftmann@65416  487  have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"  haftmann@65416  488  using div_gcd_coprime[of n "ord a"] ge_1 by fastforce  haftmann@65416  489  thus ?thesis by (simp add: gcd.commute)  haftmann@65416  490  qed  haftmann@65416  491  have dvd_d:"(ord a div gcd n (ord a)) dvd d"  haftmann@65416  492  proof -  haftmann@65416  493  have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq  haftmann@65416  494  by (metis dvd_triv_right mult.commute)  haftmann@65416  495  hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"  haftmann@65416  496  by (simp add: mult.commute)  haftmann@65416  497  thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce  haftmann@65416  498  qed  haftmann@65416  499  have "d > 0" using d_elem by simp  haftmann@65416  500  hence "ord a div gcd n (ord a) \ d" using dvd_d by (simp add : Nat.dvd_imp_le)  haftmann@65416  501  hence False using d_lt by simp  haftmann@65416  502  } hence ord_gcd_min: "\ d . d \ {d \ {1..order G}. (a(^)n) (^) d = \}  haftmann@65416  503  \ d\ord a div gcd n (ord a)" by fastforce  haftmann@65416  504  have fin:"finite {d \ {1..order G}. (a(^)n) (^) d = \}" by auto  haftmann@65416  505  thus ?thesis using Min_eqI[OF fin ord_gcd_min ord_gcd_elem]  haftmann@65416  506  unfolding ord_def by simp  haftmann@65416  507 qed  haftmann@65416  508 haftmann@65416  509 lemma ord_1_eq_1 :  haftmann@65416  510  assumes "finite (carrier G)"  haftmann@65416  511  shows "ord \ = 1"  haftmann@65416  512  using assms ord_ge_1 ord_min[of 1 \] by force  haftmann@65416  513 haftmann@65416  514 theorem lagrange_dvd:  haftmann@65416  515  assumes "finite(carrier G)" "subgroup H G" shows "(card H) dvd (order G)"  haftmann@65416  516  using assms by (simp add: lagrange[symmetric])  haftmann@65416  517 haftmann@65416  518 lemma element_generates_subgroup:  haftmann@65416  519  assumes finite[simp]: "finite (carrier G)"  haftmann@65416  520  assumes a[simp]: "a \ carrier G"  haftmann@65416  521  shows "subgroup {a (^) i | i. i \ {0 .. ord a - 1}} G"  haftmann@65416  522 proof  haftmann@65416  523  show "{a(^)i | i. i \ {0 .. ord a - 1} } \ carrier G" by auto  haftmann@65416  524 next  haftmann@65416  525  fix x y  haftmann@65416  526  assume A: "x \ {a(^)i | i. i \ {0 .. ord a - 1}}" "y \ {a(^)i | i. i \ {0 .. ord a - 1}}"  haftmann@65416  527  obtain i::nat where i:"x = a(^)i" and i2:"i \ UNIV" using A by auto  haftmann@65416  528  obtain j::nat where j:"y = a(^)j" and j2:"j \ UNIV" using A by auto  haftmann@65416  529  have "a(^)(i+j) \ {a(^)i | i. i \ {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto  haftmann@65416  530  thus "x \ y \ {a(^)i | i. i \ {0 .. ord a - 1}}"  haftmann@65416  531  using i j a ord_elems assms by (auto simp add: nat_pow_mult)  haftmann@65416  532 next  haftmann@65416  533  show "\ \ {a(^)i | i. i \ {0 .. ord a - 1}}" by force  haftmann@65416  534 next  haftmann@65416  535  fix x assume x: "x \ {a(^)i | i. i \ {0 .. ord a - 1}}"  haftmann@65416  536  hence x_in_carrier: "x \ carrier G" by auto  haftmann@65416  537  then obtain d::nat where d:"x (^) d = \" and "d\1"  haftmann@65416  538  using finite_group_elem_finite_ord by auto  haftmann@65416  539  have inv_1:"x(^)(d - 1) \ x = \" using d\1 d nat_pow_Suc[of x "d - 1"] by simp  haftmann@65416  540  have elem:"x (^) (d - 1) \ {a(^)i | i. i \ {0 .. ord a - 1}}"  haftmann@65416  541  proof -  haftmann@65416  542  obtain i::nat where i:"x = a(^)i" using x by auto  haftmann@65416  543  hence "x(^)(d - 1) \ {a(^)i | i. i \ (UNIV::nat set)}" by (auto simp add: nat_pow_pow)  haftmann@65416  544  thus ?thesis using ord_elems[of a] by auto  haftmann@65416  545  qed  haftmann@65416  546  have inv:"inv x = x(^)(d - 1)" using inv_equality[OF inv_1] x_in_carrier by blast  haftmann@65416  547  thus "inv x \ {a(^)i | i. i \ {0 .. ord a - 1}}" using elem inv by auto  haftmann@65416  548 qed  haftmann@65416  549 haftmann@65416  550 lemma ord_dvd_group_order :  haftmann@65416  551  assumes finite[simp]: "finite (carrier G)"  haftmann@65416  552  assumes a[simp]: "a \ carrier G"  haftmann@65416  553  shows "ord a dvd order G"  haftmann@65416  554 proof -  haftmann@65416  555  have card_dvd:"card {a(^)i | i. i \ {0 .. ord a - 1}} dvd card (carrier G)"  haftmann@65416  556  using lagrange_dvd element_generates_subgroup unfolding order_def by simp  haftmann@65416  557  have "inj_on (\ i . a(^)i) {0..ord a - 1}" using ord_inj by simp  haftmann@65416  558  hence cards_eq:"card ( (\ i . a(^)i)  {0..ord a - 1}) = card {0..ord a - 1}"  haftmann@65416  559  using card_image[of "\ i . a(^)i" "{0..ord a - 1}"] by auto  haftmann@65416  560  have "(\ i . a(^)i)  {0..ord a - 1} = {a(^)i | i. i \ {0..ord a - 1}}" by auto  haftmann@65416  561  hence "card {a(^)i | i. i \ {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp  haftmann@65416  562  also have "\ = ord a" using ord_ge_1[of a] by simp  haftmann@65416  563  finally show ?thesis using card_dvd by (simp add: order_def)  haftmann@65416  564 qed  haftmann@65416  565 haftmann@65416  566 end  haftmann@65416  567 haftmann@65416  568 haftmann@65416  569 section {* Number of Roots of a Polynomial *}  haftmann@65416  570 text_raw {* \label{sec:number-roots} *}  haftmann@65416  571 haftmann@65416  572 haftmann@65416  573 definition mult_of :: "('a, 'b) ring_scheme \ 'a monoid" where  haftmann@65416  574  "mult_of R \ \ carrier = carrier R - {\\<^bsub>R\<^esub>}, mult = mult R, one = \\<^bsub>R\<^esub>\"  haftmann@65416  575 haftmann@65416  576 lemma carrier_mult_of: "carrier (mult_of R) = carrier R - {\\<^bsub>R\<^esub>}"  haftmann@65416  577  by (simp add: mult_of_def)  haftmann@65416  578 haftmann@65416  579 lemma mult_mult_of: "mult (mult_of R) = mult R"  haftmann@65416  580  by (simp add: mult_of_def)  haftmann@65416  581 haftmann@65416  582 lemma nat_pow_mult_of: "op (^)\<^bsub>mult_of R\<^esub> = (op (^)\<^bsub>R\<^esub> :: _ \ nat \ _)"  haftmann@65416  583  by (simp add: mult_of_def fun_eq_iff nat_pow_def)  haftmann@65416  584 haftmann@65416  585 lemma one_mult_of: "\\<^bsub>mult_of R\<^esub> = \\<^bsub>R\<^esub>"  haftmann@65416  586  by (simp add: mult_of_def)  haftmann@65416  587 haftmann@65416  588 lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of  haftmann@65416  589 haftmann@65416  590 context field begin  haftmann@65416  591 haftmann@65416  592 lemma field_mult_group :  haftmann@65416  593  shows "group (mult_of R)"  haftmann@65416  594  apply (rule groupI)  haftmann@65416  595  apply (auto simp: mult_of_simps m_assoc dest: integral)  haftmann@65416  596  by (metis Diff_iff Units_inv_Units Units_l_inv field_Units singletonE)  haftmann@65416  597 haftmann@65416  598 lemma finite_mult_of: "finite (carrier R) \ finite (carrier (mult_of R))"  haftmann@65416  599  by (auto simp: mult_of_simps)  haftmann@65416  600 haftmann@65416  601 lemma order_mult_of: "finite (carrier R) \ order (mult_of R) = order R - 1"  haftmann@65416  602  unfolding order_def carrier_mult_of by (simp add: card.remove)  haftmann@65416  603 haftmann@65416  604 end  haftmann@65416  605 haftmann@65416  606 haftmann@65416  607 haftmann@65416  608 lemma (in monoid) Units_pow_closed :  haftmann@65416  609  fixes d :: nat  haftmann@65416  610  assumes "x \ Units G"  haftmann@65416  611  shows "x (^) d \ Units G"  haftmann@65416  612  by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)  haftmann@65416  613 haftmann@65416  614 lemma (in comm_monoid) is_monoid:  haftmann@65416  615  shows "monoid G" by unfold_locales  haftmann@65416  616 haftmann@65416  617 declare comm_monoid.is_monoid[intro?]  haftmann@65416  618 haftmann@65416  619 lemma (in ring) r_right_minus_eq[simp]:  haftmann@65416  620  assumes "a \ carrier R" "b \ carrier R"  haftmann@65416  621  shows "a \ b = \ \ a = b"  haftmann@65416  622  using assms by (metis a_minus_def add.inv_closed minus_equality r_neg)  haftmann@65416  623 haftmann@65416  624 context UP_cring begin  haftmann@65416  625 haftmann@65416  626 lemma is_UP_cring:"UP_cring R" by (unfold_locales)  haftmann@65416  627 lemma is_UP_ring :  haftmann@65416  628  shows "UP_ring R" by (unfold_locales)  haftmann@65416  629 haftmann@65416  630 end  haftmann@65416  631 haftmann@65416  632 context UP_domain begin  haftmann@65416  633 haftmann@65416  634 haftmann@65416  635 lemma roots_bound:  haftmann@65416  636  assumes f [simp]: "f \ carrier P"  haftmann@65416  637  assumes f_not_zero: "f \ \\<^bsub>P\<^esub>"  haftmann@65416  638  assumes finite: "finite (carrier R)"  haftmann@65416  639  shows "finite {a \ carrier R . eval R R id a f = \} \  haftmann@65416  640  card {a \ carrier R . eval R R id a f = \} \ deg R f" using f f_not_zero  haftmann@65416  641 proof (induction "deg R f" arbitrary: f)  haftmann@65416  642  case 0  haftmann@65416  643  have "\x. eval R R id x f \ \"  haftmann@65416  644  proof -  haftmann@65416  645  fix x  haftmann@65416  646  have "(\i\{..deg R f}. id (coeff P f i) \ x (^) i) \ \"  haftmann@65416  647  using 0 lcoeff_nonzero_nonzero[where p = f] by simp  haftmann@65416  648  thus "eval R R id x f \ \" using 0 unfolding eval_def P_def by simp  haftmann@65416  649  qed  haftmann@65416  650  then have *: "{a \ carrier R. eval R R (\a. a) a f = \} = {}"  haftmann@65416  651  by (auto simp: id_def)  haftmann@65416  652  show ?case by (simp add: *)  haftmann@65416  653 next  haftmann@65416  654  case (Suc x)  haftmann@65416  655  show ?case  haftmann@65416  656  proof (cases "\ a \ carrier R . eval R R id a f = \")  haftmann@65416  657  case True  haftmann@65416  658  then obtain a where a_carrier[simp]: "a \ carrier R" and a_root:"eval R R id a f = \" by blast  haftmann@65416  659  have R_not_triv: "carrier R \ {\}"  haftmann@65416  660  by (metis R.one_zeroI R.zero_not_one)  haftmann@65416  661  obtain q where q:"(q \ carrier P)" and  haftmann@65416  662  f:"f = (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> monom P (eval R R id a f) 0"  haftmann@65416  663  using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto  haftmann@65416  664  hence lin_fac: "f = (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \\<^bsub>P\<^esub> q" using q by (simp add: a_root)  haftmann@65416  665  have deg:"deg R (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) = 1"  haftmann@65416  666  using a_carrier by (simp add: deg_minus_eq)  haftmann@65416  667  hence mon_not_zero:"(monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \ \\<^bsub>P\<^esub>"  haftmann@65416  668  by (fastforce simp del: r_right_minus_eq)  haftmann@65416  669  have q_not_zero:"q \ \\<^bsub>P\<^esub>" using Suc by (auto simp add : lin_fac)  haftmann@65416  670  hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q]  haftmann@65416  671  by (simp add : lin_fac)  haftmann@65416  672  hence q_IH:"finite {a \ carrier R . eval R R id a q = \}  haftmann@65416  673  \ card {a \ carrier R . eval R R id a q = \} \ x" using Suc q q_not_zero by blast  haftmann@65416  674  have subs:"{a \ carrier R . eval R R id a f = \}  haftmann@65416  675  \ {a \ carrier R . eval R R id a q = \} \ {a}" (is "?L \ ?R \ {a}")  haftmann@65416  676  using a_carrier q \ _  haftmann@65416  677  by (auto simp: evalRR_simps lin_fac R.integral_iff)  haftmann@65416  678  have "{a \ carrier R . eval R R id a f = \} \ insert a {a \ carrier R . eval R R id a q = \}"  haftmann@65416  679  using subs by auto  haftmann@65416  680  hence "card {a \ carrier R . eval R R id a f = \} \  haftmann@65416  681  card (insert a {a \ carrier R . eval R R id a q = \})" using q_IH by (blast intro: card_mono)  haftmann@65416  682  also have "\ \ deg R f" using q_IH Suc x = _  haftmann@65416  683  by (simp add: card_insert_if)  haftmann@65416  684  finally show ?thesis using q_IH Suc x = _ using finite by force  haftmann@65416  685  next  haftmann@65416  686  case False  haftmann@65416  687  hence "card {a \ carrier R. eval R R id a f = \} = 0" using finite by auto  haftmann@65416  688  also have "\ \ deg R f" by simp  haftmann@65416  689  finally show ?thesis using finite by auto  haftmann@65416  690  qed  haftmann@65416  691 qed  haftmann@65416  692 haftmann@65416  693 end  haftmann@65416  694 haftmann@65416  695 lemma (in domain) num_roots_le_deg :  haftmann@65416  696  fixes p d :: nat  haftmann@65416  697  assumes finite:"finite (carrier R)"  haftmann@65416  698  assumes d_neq_zero : "d \ 0"  haftmann@65416  699  shows "card {x \ carrier R. x (^) d = \} \ d"  haftmann@65416  700 proof -  haftmann@65416  701  let ?f = "monom (UP R) \\<^bsub>R\<^esub> d \\<^bsub> (UP R)\<^esub> monom (UP R) \\<^bsub>R\<^esub> 0"  haftmann@65416  702  have one_in_carrier:"\ \ carrier R" by simp  haftmann@65416  703  interpret R: UP_domain R "UP R" by (unfold_locales)  haftmann@65416  704  have "deg R ?f = d"  haftmann@65416  705  using d_neq_zero by (simp add: R.deg_minus_eq)  haftmann@65416  706  hence f_not_zero:"?f \ \\<^bsub>UP R\<^esub>" using d_neq_zero by (auto simp add : R.deg_nzero_nzero)  haftmann@65416  707  have roots_bound:"finite {a \ carrier R . eval R R id a ?f = \} \  haftmann@65416  708  card {a \ carrier R . eval R R id a ?f = \} \ deg R ?f"  haftmann@65416  709  using finite by (intro R.roots_bound[OF _ f_not_zero]) simp  haftmann@65416  710  have subs:"{x \ carrier R. x (^) d = \} \ {a \ carrier R . eval R R id a ?f = \}"  haftmann@65416  711  by (auto simp: R.evalRR_simps)  haftmann@65416  712  then have "card {x \ carrier R. x (^) d = \} \  haftmann@65416  713  card {a \ carrier R. eval R R id a ?f = \}" using finite by (simp add : card_mono)  haftmann@65416  714  thus ?thesis using deg R ?f = d roots_bound by linarith  haftmann@65416  715 qed  haftmann@65416  716 haftmann@65416  717 haftmann@65416  718 haftmann@65416  719 section {* The Multiplicative Group of a Field *}  haftmann@65416  720 text_raw {* \label{sec:mult-group} *}  haftmann@65416  721 haftmann@65416  722 haftmann@65416  723 text {*  haftmann@65416  724  In this section we show that the multiplicative group of a finite field  haftmann@65416  725  is generated by a single element, i.e. it is cyclic. The proof is inspired  haftmann@65416  726  by the first proof given in the survey~\cite{conrad-cyclicity}.  haftmann@65416  727 *}  haftmann@65416  728 haftmann@65416  729 lemma (in group) pow_order_eq_1:  haftmann@65416  730  assumes "finite (carrier G)" "x \ carrier G" shows "x (^) order G = \"  haftmann@65416  731  using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)  haftmann@65416  732 haftmann@65416  733 (* XXX remove in AFP devel, replaced by div_eq_dividend_iff *)  haftmann@65416  734 lemma nat_div_eq: "a \ 0 \ (a :: nat) div b = a \ b = 1"  haftmann@65416  735  apply rule  haftmann@65416  736  apply (cases "b = 0")  haftmann@65416  737  apply simp_all  haftmann@65416  738  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)  haftmann@65416  739  done  haftmann@65416  740 haftmann@65416  741 lemma (in group)  haftmann@65416  742  assumes finite': "finite (carrier G)"  haftmann@65416  743  assumes "a \ carrier G"  haftmann@65416  744  shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \ coprime k (ord a)" (is "?L \ ?R")  haftmann@65416  745 proof  haftmann@65416  746  assume A: ?L then show ?R  haftmann@65416  747  using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem)  haftmann@65416  748 next  haftmann@65416  749  assume ?R then show ?L  haftmann@65416  750  using ord_pow_dvd_ord_elem[OF assms, of k] by auto  haftmann@65416  751 qed  haftmann@65416  752 haftmann@65416  753 context field begin  haftmann@65416  754 haftmann@65416  755 lemma num_elems_of_ord_eq_phi':  haftmann@65416  756  assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)"  haftmann@65416  757  and exists: "\a\carrier (mult_of R). group.ord (mult_of R) a = d"  haftmann@65416  758  shows "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d"  haftmann@65416  759 proof -  haftmann@65416  760  note mult_of_simps[simp]  haftmann@65416  761  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)  haftmann@65416  762 haftmann@65416  763  interpret G:group "mult_of R" rewrites "op (^)\<^bsub>mult_of R\<^esub> = (op (^) :: _ \ nat \ _)" and "\\<^bsub>mult_of R\<^esub> = \"  haftmann@65416  764  by (rule field_mult_group) simp_all  haftmann@65416  765 haftmann@65416  766  from exists  haftmann@65416  767  obtain a where a:"a \ carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"  haftmann@65416  768  by (auto simp add: card_gt_0_iff)  haftmann@65416  769 haftmann@65416  770  have set_eq1:"{a(^)n| n. n \ {1 .. d}} = {x \ carrier (mult_of R). x (^) d = \}"  haftmann@65416  771  proof (rule card_seteq)  haftmann@65416  772  show "finite {x \ carrier (mult_of R). x (^) d = \}" using finite by auto  haftmann@65416  773 haftmann@65416  774  show "{a(^)n| n. n \ {1 ..d}} \ {x \ carrier (mult_of R). x(^)d = \}"  haftmann@65416  775  proof  haftmann@65416  776  fix x assume "x \ {a(^)n | n. n \ {1 .. d}}"  haftmann@65416  777  then obtain n where n:"x = a(^)n \ n \ {1 .. d}" by auto  haftmann@65416  778  have "x(^)d =(a(^)d)(^)n" using n a ord_a by (simp add:nat_pow_pow mult.commute)  haftmann@65416  779  hence "x(^)d = \" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce  haftmann@65416  780  thus "x \ {x \ carrier (mult_of R). x(^)d = \}" using G.nat_pow_closed[OF a] n by blast  haftmann@65416  781  qed  haftmann@65416  782 haftmann@65416  783  show "card {x \ carrier (mult_of R). x (^) d = \} \ card {a(^)n | n. n \ {1 .. d}}"  haftmann@65416  784  proof -  haftmann@65416  785  have *:"{a(^)n | n. n \ {1 .. d }} = ((\ n. a(^)n)  {1 .. d})" by auto  haftmann@65416  786  have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]  haftmann@65416  787  using card_mono[OF finite, of "{\, \}"] by (simp add: order_def)  haftmann@65416  788  have "card {x \ carrier (mult_of R). x (^) d = \} \ card {x \ carrier R. x (^) d = \}"  haftmann@65416  789  using finite by (auto intro: card_mono)  haftmann@65416  790  also have "\ \ d" using 0 < order (mult_of R) num_roots_le_deg[OF finite, of d]  haftmann@65416  791  by (simp add : dvd_pos_nat[OF _ d dvd order (mult_of R)])  haftmann@65416  792  finally show ?thesis using G.ord_inj'[OF finite' a] ord_a * by (simp add: card_image)  haftmann@65416  793  qed  haftmann@65416  794  qed  haftmann@65416  795 haftmann@65416  796  have set_eq2:"{x \ carrier (mult_of R) . group.ord (mult_of R) x = d}  haftmann@65416  797  = (\ n . a(^)n)  {n \ {1 .. d}. group.ord (mult_of R) (a(^)n) = d}" (is "?L = ?R")  haftmann@65416  798  proof  haftmann@65416  799  { fix x assume x:"x \ (carrier (mult_of R)) \ group.ord (mult_of R) x = d"  haftmann@65416  800  hence "x \ {x \ carrier (mult_of R). x (^) d = \}"  haftmann@65416  801  by (simp add: G.pow_ord_eq_1[OF finite', of x, symmetric])  haftmann@65416  802  then obtain n where n:"x = a(^)n \ n \ {1 .. d}" using set_eq1 by blast  haftmann@65416  803  hence "x \ ?R" using x by fast  haftmann@65416  804  } thus "?L \ ?R" by blast  haftmann@65416  805  show "?R \ ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)  haftmann@65416  806  qed  haftmann@65416  807  have "inj_on (\ n . a(^)n) {n \ {1 .. d}. group.ord (mult_of R) (a(^)n) = d}"  haftmann@65416  808  using G.ord_inj'[OF finite' a, unfolded ord_a] unfolding inj_on_def by fast  haftmann@65416  809  hence "card ((\n. a(^)n)  {n \ {1 .. d}. group.ord (mult_of R) (a(^)n) = d})  haftmann@65416  810  = card {k \ {1 .. d}. group.ord (mult_of R) (a(^)k) = d}"  haftmann@65416  811  using card_image by blast  haftmann@65416  812  thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' a \ _, unfolded ord_a]  haftmann@65416  813  by (simp add: phi'_def)  haftmann@65416  814 qed  haftmann@65416  815 haftmann@65416  816 end  haftmann@65416  817 haftmann@65416  818 haftmann@65416  819 theorem (in field) finite_field_mult_group_has_gen :  haftmann@65416  820  assumes finite:"finite (carrier R)"  haftmann@65416  821  shows "\ a \ carrier (mult_of R) . carrier (mult_of R) = {a(^)i | i::nat . i \ UNIV}"  haftmann@65416  822 proof -  haftmann@65416  823  note mult_of_simps[simp]  haftmann@65416  824  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)  haftmann@65416  825 haftmann@65416  826  interpret G: group "mult_of R" rewrites  haftmann@65416  827  "op (^)\<^bsub>mult_of R\<^esub> = (op (^) :: _ \ nat \ _)" and "\\<^bsub>mult_of R\<^esub> = \"  haftmann@65416  828  by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)  haftmann@65416  829 haftmann@65416  830  let ?N = "\ x . card {a \ carrier (mult_of R). group.ord (mult_of R) a = x}"  haftmann@65416  831  have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{\, \}"] by simp  haftmann@65416  832  then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of)  haftmann@65416  833  have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force  haftmann@65416  834 haftmann@65416  835  have "(\d | d dvd order (mult_of R). ?N d)  haftmann@65416  836  = card (UN d:{d . d dvd order (mult_of R) }. {a \ carrier (mult_of R). group.ord (mult_of R) a = d})"  haftmann@65416  837  (is "_ = card ?U")  haftmann@65416  838  using fin finite by (subst card_UN_disjoint) auto  haftmann@65416  839  also have "?U = carrier (mult_of R)"  haftmann@65416  840  proof  haftmann@65416  841  { fix x assume x:"x \ carrier (mult_of R)"  haftmann@65416  842  hence x':"x\carrier (mult_of R)" by simp  haftmann@65416  843  then have "group.ord (mult_of R) x dvd order (mult_of R)"  haftmann@65416  844  using finite' G.ord_dvd_group_order[OF _ x'] by (simp add: order_mult_of)  haftmann@65416  845  hence "x \ ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast  haftmann@65416  846  } thus "carrier (mult_of R) \ ?U" by blast  haftmann@65416  847  qed auto  haftmann@65416  848  also have "card ... = order (mult_of R)"  haftmann@65416  849  using order_mult_of finite' by (simp add: order_def)  haftmann@65416  850  finally have sum_Ns_eq: "(\d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .  haftmann@65416  851 haftmann@65416  852  { fix d assume d:"d dvd order (mult_of R)"  haftmann@65416  853  have "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} \ phi' d"  haftmann@65416  854  proof cases  haftmann@65416  855  assume "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger  haftmann@65416  856  next  haftmann@65416  857  assume "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} \ 0"  haftmann@65416  858  hence "\a \ carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)  haftmann@65416  859  thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto  haftmann@65416  860  qed  haftmann@65416  861  }  haftmann@65416  862  hence all_le:"\i. i \ {d. d dvd order (mult_of R) }  haftmann@65416  863  \ (\i. card {a \ carrier (mult_of R). group.ord (mult_of R) a = i}) i \ (\i. phi' i) i" by fast  haftmann@65416  864  hence le:"(\i | i dvd order (mult_of R). ?N i)  haftmann@65416  865  \ (\i | i dvd order (mult_of R). phi' i)"  haftmann@65416  866  using sum_mono[of "{d . d dvd order (mult_of R)}"  haftmann@65416  867  "\i. card {a \ carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger  haftmann@65416  868  have "order (mult_of R) = (\d | d dvd order (mult_of R). phi' d)" using *  haftmann@65416  869  by (simp add: sum_phi'_factors)  haftmann@65416  870  hence eq:"(\i | i dvd order (mult_of R). ?N i)  haftmann@65416  871  = (\i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger  haftmann@65416  872  have "\i. i \ {d. d dvd order (mult_of R) } \ ?N i = (\i. phi' i) i"  haftmann@65416  873  proof (rule ccontr)  haftmann@65416  874  fix i  haftmann@65416  875  assume i1:"i \ {d. d dvd order (mult_of R)}" and "?N i \ phi' i"  haftmann@65416  876  hence "?N i = 0"  haftmann@65416  877  using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff)  haftmann@65416  878  moreover have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i])  haftmann@65416  879  ultimately have "?N i < phi' i" using phi'_nonzero by presburger  haftmann@65416  880  hence "(\i | i dvd order (mult_of R). ?N i)  haftmann@65416  881  < (\i | i dvd order (mult_of R). phi' i)"  haftmann@65416  882  using sum_strict_mono_ex1[OF fin, of "?N" "\ i . phi' i"]  haftmann@65416  883  i1 all_le by auto  haftmann@65416  884  thus False using eq by force  haftmann@65416  885  qed  haftmann@65416  886  hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)  haftmann@65416  887  then obtain a where a:"a \ carrier (mult_of R)" and a_ord:"group.ord (mult_of R) a = order (mult_of R)"  haftmann@65416  888  by (auto simp add: card_gt_0_iff)  haftmann@65416  889  hence set_eq:"{a(^)i | i::nat. i \ UNIV} = (\x. a(^)x)  {0 .. group.ord (mult_of R) a - 1}"  haftmann@65416  890  using G.ord_elems[OF finite'] by auto  haftmann@65416  891  have card_eq:"card ((\x. a(^)x)  {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}"  haftmann@65416  892  by (intro card_image G.ord_inj finite' a)  haftmann@65416  893  hence "card ((\ x . a(^)x)  {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"  haftmann@65416  894  using assms by (simp add: card_eq a_ord)  haftmann@65416  895  hence card_R_minus_1:"card {a(^)i | i::nat. i \ UNIV} = order (mult_of R)"  haftmann@65416  896  using * by (subst set_eq) auto  haftmann@65416  897  have **:"{a(^)i | i::nat. i \ UNIV} \ carrier (mult_of R)"  haftmann@65416  898  using G.nat_pow_closed[OF a] by auto  haftmann@65416  899  with _ have "carrier (mult_of R) = {a(^)i|i::nat. i \ UNIV}"  haftmann@65416  900  by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)  haftmann@65416  901  thus ?thesis using a by blast  haftmann@65416  902 qed  haftmann@65416  903 haftmann@65416  904 end `