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