src/HOL/Algebra/Multiplicative_Group.thy
 author haftmann Sat May 12 22:20:46 2018 +0200 (21 months ago ago) changeset 68157 057d5b4ce47e parent 67399 eab6ce8368fa child 68432 c183a6a69f2d permissions -rw-r--r--
removed some non-essential rules
     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   More_Group

    11   More_Finite_Product

    12   Coset

    13   UnivPoly

    14 begin

    15

    16 section \<open>Simplification Rules for Polynomials\<close>

    17 text_raw \<open>\label{sec:simp-rules}\<close>

    18

    19 lemma (in ring_hom_cring) hom_sub[simp]:

    20   assumes "x \<in> carrier R" "y \<in> carrier R"

    21   shows "h (x \<ominus> y) = h x \<ominus>\<^bsub>S\<^esub> h y"

    22   using assms by (simp add: R.minus_eq S.minus_eq)

    23

    24 context UP_ring begin

    25

    26 lemma deg_nzero_nzero:

    27   assumes deg_p_nzero: "deg R p \<noteq> 0"

    28   shows "p \<noteq> \<zero>\<^bsub>P\<^esub>"

    29   using deg_zero deg_p_nzero by auto

    30

    31 lemma deg_add_eq:

    32   assumes c: "p \<in> carrier P" "q \<in> carrier P"

    33   assumes "deg R q \<noteq> deg R p"

    34   shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"

    35 proof -

    36   let ?m = "max (deg R p) (deg R q)"

    37   from assms have "coeff P p ?m = \<zero> \<longleftrightarrow> coeff P q ?m \<noteq> \<zero>"

    38     by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1)

    39   then have "coeff P (p \<oplus>\<^bsub>P\<^esub> q) ?m \<noteq> \<zero>"

    40     using assms by auto

    41   then have "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<ge> ?m"

    42     using assms by (blast intro: deg_belowI)

    43   with deg_add[OF c] show ?thesis by arith

    44 qed

    45

    46 lemma deg_minus_eq:

    47   assumes "p \<in> carrier P" "q \<in> carrier P" "deg R q \<noteq> deg R p"

    48   shows "deg R (p \<ominus>\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"

    49   using assms by (simp add: deg_add_eq a_minus_def)

    50

    51 end

    52

    53 context UP_cring begin

    54

    55 lemma evalRR_add:

    56   assumes "p \<in> carrier P" "q \<in> carrier P"

    57   assumes x:"x \<in> carrier R"

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

    59 proof -

    60   interpret UP_pre_univ_prop R R id by unfold_locales simp

    61   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])

    62   show ?thesis using assms by simp

    63 qed

    64

    65 lemma evalRR_sub:

    66   assumes "p \<in> carrier P" "q \<in> carrier P"

    67   assumes x:"x \<in> carrier R"

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

    69 proof -

    70   interpret UP_pre_univ_prop R R id by unfold_locales simp

    71   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])

    72   show ?thesis using assms by simp

    73 qed

    74

    75 lemma evalRR_mult:

    76   assumes "p \<in> carrier P" "q \<in> carrier P"

    77   assumes x:"x \<in> carrier R"

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

    79 proof -

    80   interpret UP_pre_univ_prop R R id by unfold_locales simp

    81   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])

    82   show ?thesis using assms by simp

    83 qed

    84

    85 lemma evalRR_monom:

    86   assumes a: "a \<in> carrier R" and x: "x \<in> carrier R"

    87   shows "eval R R id x (monom P a d) = a \<otimes> x [^] d"

    88 proof -

    89   interpret UP_pre_univ_prop R R id by unfold_locales simp

    90   show ?thesis using assms by (simp add: eval_monom)

    91 qed

    92

    93 lemma evalRR_one:

    94   assumes x: "x \<in> carrier R"

    95   shows "eval R R id x \<one>\<^bsub>P\<^esub> = \<one>"

    96 proof -

    97   interpret UP_pre_univ_prop R R id by unfold_locales simp

    98   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])

    99   show ?thesis using assms by simp

   100 qed

   101

   102 lemma carrier_evalRR:

   103   assumes x: "x \<in> carrier R" and "p \<in> carrier P"

   104   shows "eval R R id x p \<in> carrier R"

   105 proof -

   106   interpret UP_pre_univ_prop R R id by unfold_locales simp

   107   interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])

   108   show ?thesis using assms by simp

   109 qed

   110

   111 lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR

   112

   113 end

   114

   115

   116

   117 section \<open>Properties of the Euler \<open>\<phi>\<close>-function\<close>

   118 text_raw \<open>\label{sec:euler-phi}\<close>

   119

   120 text\<open>

   121   In this section we prove that for every positive natural number the equation

   122   $\sum_{d | n}^n \varphi(d) = n$ holds.

   123 \<close>

   124

   125 lemma dvd_div_ge_1 :

   126   fixes a b :: nat

   127   assumes "a \<ge> 1" "b dvd a"

   128   shows "a div b \<ge> 1"

   129 proof -

   130   from \<open>b dvd a\<close> obtain c where "a = b * c" ..

   131   with \<open>a \<ge> 1\<close> show ?thesis by simp

   132 qed

   133

   134 lemma dvd_nat_bounds :

   135  fixes n p :: nat

   136  assumes "p > 0" "n dvd p"

   137  shows "n > 0 \<and> n \<le> p"

   138  using assms by (simp add: dvd_pos_nat dvd_imp_le)

   139

   140 (* Deviates from the definition given in the library in number theory *)

   141 definition phi' :: "nat => nat"

   142   where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"

   143

   144 notation (latex output)

   145   phi' ("\<phi> _")

   146

   147 lemma phi'_nonzero :

   148   assumes "m > 0"

   149   shows "phi' m > 0"

   150 proof -

   151   have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" using assms by simp

   152   hence "card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m} > 0" by (auto simp: card_gt_0_iff)

   153   thus ?thesis unfolding phi'_def by simp

   154 qed

   155

   156 lemma dvd_div_eq_1:

   157   fixes a b c :: nat

   158   assumes "c dvd a" "c dvd b" "a div c = b div c"

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

   160                 by presburger

   161

   162 lemma dvd_div_eq_2:

   163   fixes a b c :: nat

   164   assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b"

   165   shows "a = b"

   166   proof -

   167   have "a > 0" "a \<le> c" using dvd_nat_bounds[OF assms(1-2)] by auto

   168   have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce

   169   also have "\<dots> = b*(c div a)" using assms dvd_mult_div_cancel by fastforce

   170   finally show "a = b" using \<open>c>0\<close> dvd_div_ge_1[OF _ \<open>a dvd c\<close>] by fastforce

   171 qed

   172

   173 lemma div_mult_mono:

   174   fixes a b c :: nat

   175   assumes "a > 0" "a\<le>d"

   176   shows "a * b div d \<le> b"

   177 proof -

   178   have "a*b div d \<le> b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger

   179   thus ?thesis using assms by force

   180 qed

   181

   182 text\<open>

   183   We arrive at the main result of this section:

   184   For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.

   185

   186   The outline of the proof for this lemma is as follows:

   187   We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$.

   188   We analyze the reduced form $a/d = m/n$ for any of those fractions.

   189   We want to know how many fractions $m/n$ have the reduced form denominator $d$.

   190   The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$.

   191   Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. @{term "gcd a d = 1"}.

   192   This number is exactly @{term "phi' d"}.

   193

   194   Finally, by counting the fractions $m/n$ according to their reduced form denominator,

   195   we get: @{term [display] "(\<Sum>d | d dvd n . phi' d) = n"}.

   196   To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$

   197   \begin{itemize}

   198     \item the set of reduced form numerators @{term "{a. (1::nat) \<le> a \<and> a \<le> d \<and> coprime a d}"}

   199     \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$,

   200       i.e. the set @{term "{m \<in> {1::nat .. n}. n div gcd m n = d}"}

   201   \end{itemize}

   202   We show that @{term "\<lambda>a. a*n div d"} with the inverse @{term "\<lambda>a. a div gcd a n"} is

   203   a bijection between theses sets, thus yielding the equality

   204   @{term [display] "phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"}

   205   This gives us

   206   @{term [display] "(\<Sum>d | d dvd n . phi' d)

   207           = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"}

   208   and by showing

   209   @{term "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}"}

   210   (this is our counting argument) the thesis follows.

   211 \<close>

   212 lemma sum_phi'_factors :

   213  fixes n :: nat

   214  assumes "n > 0"

   215  shows "(\<Sum>d | d dvd n. phi' d) = n"

   216 proof -

   217   { fix d assume "d dvd n" then obtain q where q: "n = d * q" ..

   218     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}"

   219          (is "card ?RF = card ?F")

   220     proof (rule card_bij_eq)

   221       { fix a b assume "a * n div d = b * n div d"

   222         hence "a * (n div d) = b * (n div d)"

   223           using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)

   224         hence "a = b" using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>

   225           by (simp add: mult.commute nat_mult_eq_cancel1)

   226       } thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast

   227       { fix a assume a:"a\<in>?RF"

   228         hence "a * (n div d) \<ge> 1" using \<open>n>0\<close> dvd_div_ge_1[OF _ \<open>d dvd n\<close>] by simp

   229         hence ge_1:"a * n div d \<ge> 1" by (simp add: \<open>d dvd n\<close> div_mult_swap)

   230         have le_n:"a * n div d \<le> n" using div_mult_mono a by simp

   231         have "gcd (a * n div d) n = n div d * gcd a d"

   232           by (simp add: gcd_mult_distrib_nat q ac_simps)

   233         hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp

   234         hence "a * n div d \<in> ?F"

   235           using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)

   236       } thus "(\<lambda>a. a*n div d)  ?RF \<subseteq> ?F" by blast

   237       { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"

   238         hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce

   239         hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce

   240       } thus "inj_on (\<lambda>a. a div gcd a n) ?F" unfolding inj_on_def by blast

   241       { fix m assume "m \<in> ?F"

   242         hence "m div gcd m n \<in> ?RF" using dvd_div_ge_1

   243           by (fastforce simp add: div_le_mono div_gcd_coprime)

   244       } thus "(\<lambda>a. a div gcd a n)  ?F \<subseteq> ?RF" by blast

   245     qed force+

   246   } hence phi'_eq:"\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"

   247       unfolding phi'_def by presburger

   248   have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF \<open>n>0\<close>] by force

   249   have "(\<Sum>d | d dvd n. phi' d)

   250                  = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"

   251     using card_UN_disjoint[OF fin, of "(\<lambda>d. {m \<in> {1 .. n}. n div gcd m n = d})"] phi'_eq

   252     by fastforce

   253   also have "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R")

   254   proof

   255     show "?L \<supseteq> ?R"

   256     proof

   257       fix m assume m: "m \<in> ?R"

   258       thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]

   259         by simp

   260     qed

   261   qed fastforce

   262   finally show ?thesis by force

   263 qed

   264

   265 section \<open>Order of an Element of a Group\<close>

   266 text_raw \<open>\label{sec:order-elem}\<close>

   267

   268

   269 context group begin

   270

   271 lemma pow_eq_div2 :

   272   fixes m n :: nat

   273   assumes x_car: "x \<in> carrier G"

   274   assumes pow_eq: "x [^] m = x [^] n"

   275   shows "x [^] (m - n) = \<one>"

   276 proof (cases "m < n")

   277   case False

   278   have "\<one> \<otimes> x [^] m = x [^] m" by (simp add: x_car)

   279   also have "\<dots> = x [^] (m - n) \<otimes> x [^] n"

   280     using False by (simp add: nat_pow_mult x_car)

   281   also have "\<dots> = x [^] (m - n) \<otimes> x [^] m"

   282     by (simp add: pow_eq)

   283   finally show ?thesis by (simp add: x_car)

   284 qed simp

   285

   286 definition ord where "ord a = Min {d \<in> {1 .. order G} . a [^] d = \<one>}"

   287

   288 lemma

   289   assumes finite:"finite (carrier G)"

   290   assumes a:"a \<in> carrier G"

   291   shows ord_ge_1: "1 \<le> ord a" and ord_le_group_order: "ord a \<le> order G"

   292     and pow_ord_eq_1: "a [^] ord a = \<one>"

   293 proof -

   294   have "\<not>inj_on (\<lambda>x. a [^] x) {0 .. order G}"

   295   proof (rule notI)

   296     assume A: "inj_on (\<lambda>x. a [^] x) {0 .. order G}"

   297     have "order G + 1 = card {0 .. order G}" by simp

   298     also have "\<dots> = card ((\<lambda>x. a [^] x)  {0 .. order G})" (is "_ = card ?S")

   299       using A by (simp add: card_image)

   300     also have "?S = {a [^] x | x. x \<in> {0 .. order G}}" by blast

   301     also have "\<dots> \<subseteq> carrier G" (is "?S \<subseteq> _") using a by blast

   302     then have "card ?S \<le> order G" unfolding order_def

   303       by (rule card_mono[OF finite])

   304     finally show False by arith

   305   qed

   306

   307   then obtain x y where x_y:"x \<noteq> y" "x \<in> {0 .. order G}" "y \<in> {0 .. order G}"

   308                         "a [^] x = a [^] y" unfolding inj_on_def by blast

   309   obtain d where "1 \<le> d" "a [^] d = \<one>" "d \<le> order G"

   310   proof cases

   311     assume "y < x" with x_y show ?thesis

   312       by (intro that[where d="x - y"]) (auto simp add: pow_eq_div2[OF a])

   313   next

   314     assume "\<not>y < x" with x_y show ?thesis

   315       by (intro that[where d="y - x"]) (auto simp add: pow_eq_div2[OF a])

   316   qed

   317   hence "ord a \<in> {d \<in> {1 .. order G} . a [^] d = \<one>}"

   318     unfolding ord_def using Min_in[of "{d \<in> {1 .. order G} . a [^] d = \<one>}"]

   319     by fastforce

   320   then show "1 \<le> ord a" and "ord a \<le> order G" and "a [^] ord a = \<one>"

   321     by (auto simp: order_def)

   322 qed

   323

   324 lemma finite_group_elem_finite_ord :

   325   assumes "finite (carrier G)" "x \<in> carrier G"

   326   shows "\<exists> d::nat. d \<ge> 1 \<and> x [^] d = \<one>"

   327   using assms ord_ge_1 pow_ord_eq_1 by auto

   328

   329 lemma ord_min:

   330   assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a [^] d = \<one>" shows "ord a \<le> d"

   331 proof -

   332   define Ord where "Ord = {d \<in> {1..order G}. a [^] d = \<one>}"

   333   have fin: "finite Ord" by (auto simp: Ord_def)

   334   have in_ord: "ord a \<in> Ord"

   335     using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)

   336   then have "Ord \<noteq> {}" by auto

   337

   338   show ?thesis

   339   proof (cases "d \<le> order G")

   340     case True

   341     then have "d \<in> Ord" using assms by (auto simp: Ord_def)

   342     with fin in_ord show ?thesis

   343       unfolding ord_def Ord_def[symmetric] by simp

   344   next

   345     case False

   346     then show ?thesis using in_ord by (simp add: Ord_def)

   347   qed

   348 qed

   349

   350 lemma ord_inj :

   351   assumes finite: "finite (carrier G)"

   352   assumes a: "a \<in> carrier G"

   353   shows "inj_on (\<lambda> x . a [^] x) {0 .. ord a - 1}"

   354 proof (rule inj_onI, rule ccontr)

   355   fix x y assume A: "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}" "a [^] x= a [^] y" "x \<noteq> y"

   356

   357   have "finite {d \<in> {1..order G}. a [^] d = \<one>}" by auto

   358

   359   { fix x y assume A: "x < y" "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}"

   360         "a [^] x = a [^] y"

   361     hence "y - x < ord a" by auto

   362     also have "\<dots> \<le> order G" using assms by (simp add: ord_le_group_order)

   363     finally have y_x_range:"y - x \<in> {1 .. order G}" using A by force

   364     have "a [^] (y-x) = \<one>" using a A by (simp add: pow_eq_div2)

   365

   366     hence y_x:"y - x \<in> {d \<in> {1.. order G}. a [^] d = \<one>}" using y_x_range by blast

   367     have "min (y - x) (ord a) = ord a"

   368       using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a [^] d = \<one>}\<close> y_x] ord_def by auto

   369     with \<open>y - x < ord a\<close> have False by linarith

   370   }

   371   note X = this

   372

   373   { assume "x < y" with A X have False by blast }

   374   moreover

   375   { assume "x > y" with A X  have False by metis }

   376   moreover

   377   { assume "x = y" then have False using A by auto}

   378   ultimately

   379   show False by fastforce

   380 qed

   381

   382 lemma ord_inj' :

   383   assumes finite: "finite (carrier G)"

   384   assumes a: "a \<in> carrier G"

   385   shows "inj_on (\<lambda> x . a [^] x) {1 .. ord a}"

   386 proof (rule inj_onI, rule ccontr)

   387   fix x y :: nat

   388   assume A:"x \<in> {1 .. ord a}" "y \<in> {1 .. ord a}" "a [^] x = a [^] y" "x\<noteq>y"

   389   { assume "x < ord a" "y < ord a"

   390     hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce

   391   }

   392   moreover

   393   { assume "x = ord a" "y < ord a"

   394     hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1[OF assms] A by auto

   395     hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force

   396     hence False using A by fastforce

   397   }

   398   moreover

   399   { assume "y = ord a" "x < ord a"

   400     hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1[OF assms] A by auto

   401     hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force

   402     hence False using A by fastforce

   403   }

   404   ultimately show False using A  by force

   405 qed

   406

   407 lemma ord_elems :

   408   assumes "finite (carrier G)" "a \<in> carrier G"

   409   shows "{a[^]x | x. x \<in> (UNIV :: nat set)} = {a[^]x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")

   410 proof

   411   show "?R \<subseteq> ?L" by blast

   412   { fix y assume "y \<in> ?L"

   413     then obtain x::nat where x:"y = a[^]x" by auto

   414     define r q where "r = x mod ord a" and "q = x div ord a"

   415     then have "x = q * ord a + r"

   416       by (simp add: div_mult_mod_eq)

   417     hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"

   418       using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)

   419     hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)

   420     have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)

   421     hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)

   422     hence "y \<in> {a[^]x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a[^]r\<close> by blast

   423   }

   424   thus "?L \<subseteq> ?R" by auto

   425 qed

   426

   427 lemma ord_dvd_pow_eq_1 :

   428   assumes "finite (carrier G)" "a \<in> carrier G" "a [^] k = \<one>"

   429   shows "ord a dvd k"

   430 proof -

   431   define r where "r = k mod ord a"

   432

   433   define r q where "r = k mod ord a" and "q = k div ord a"

   434   then have q: "k = q * ord a + r"

   435     by (simp add: div_mult_mod_eq)

   436   hence "a[^]k = (a[^]ord a)[^]q \<otimes> a[^]r"

   437       using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)

   438   hence "a[^]k = a[^]r" using assms by (simp add: pow_ord_eq_1)

   439   hence "a[^]r = \<one>" using assms(3) by simp

   440   have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)

   441   hence "r = 0" using \<open>a[^]r = \<one>\<close> ord_def[of a] ord_min[of r a] assms(1-2) by linarith

   442   thus ?thesis using q by simp

   443 qed

   444

   445 lemma dvd_gcd :

   446   fixes a b :: nat

   447   obtains q where "a * (b div gcd a b) = b*q"

   448 proof

   449   have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add:  div_mult_swap dvd_div_mult)

   450   also have "\<dots> = b * (a div gcd a b)" by simp

   451   finally show "a * (b div gcd a b) = b * (a div gcd a b) " .

   452 qed

   453

   454 lemma ord_pow_dvd_ord_elem :

   455   assumes finite[simp]: "finite (carrier G)"

   456   assumes a[simp]:"a \<in> carrier G"

   457   shows "ord (a[^]n) = ord a div gcd n (ord a)"

   458 proof -

   459   have "(a[^]n) [^] ord a = (a [^] ord a) [^] n"

   460     by (simp add: mult.commute nat_pow_pow)

   461   hence "(a[^]n) [^] ord a = \<one>" by (simp add: pow_ord_eq_1)

   462   obtain q where "n * (ord a div gcd n (ord a)) = ord a * q" by (rule dvd_gcd)

   463   hence "(a[^]n) [^] (ord a div gcd n (ord a)) = (a [^] ord a)[^]q"  by (simp add : nat_pow_pow)

   464   hence pow_eq_1: "(a[^]n) [^] (ord a div gcd n (ord a)) = \<one>"

   465      by (auto simp add : pow_ord_eq_1[of a])

   466   have "ord a \<ge> 1" using ord_ge_1 by simp

   467   have ge_1:"ord a div gcd n (ord a) \<ge> 1"

   468   proof -

   469     have "gcd n (ord a) dvd ord a" by blast

   470     thus ?thesis by (rule dvd_div_ge_1[OF \<open>ord a \<ge> 1\<close>])

   471   qed

   472   have "ord a \<le> order G" by (simp add: ord_le_group_order)

   473   have "ord a div gcd n (ord a) \<le> order G"

   474   proof -

   475     have "ord a div gcd n (ord a) \<le> ord a" by simp

   476     thus ?thesis using \<open>ord a \<le> order G\<close> by linarith

   477   qed

   478   hence ord_gcd_elem:"ord a div gcd n (ord a) \<in> {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}"

   479     using ge_1 pow_eq_1 by force

   480   { fix d :: nat

   481     assume d_elem:"d \<in> {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}"

   482     assume d_lt:"d < ord a div gcd n (ord a)"

   483     hence pow_nd:"a[^](n*d)  = \<one>" using d_elem

   484       by (simp add : nat_pow_pow)

   485     hence "ord a dvd n*d" using assms by (auto simp add : ord_dvd_pow_eq_1)

   486     then obtain q where "ord a * q = n*d" by (metis dvd_mult_div_cancel)

   487     hence prod_eq:"(ord a div gcd n (ord a)) * q = (n div gcd n (ord a)) * d"

   488       by (simp add: dvd_div_mult)

   489     have cp:"coprime (ord a div gcd n (ord a)) (n div gcd n (ord a))"

   490     proof -

   491       have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"

   492         using div_gcd_coprime[of n "ord a"] ge_1 by fastforce

   493       thus ?thesis by (simp add: ac_simps)

   494     qed

   495     have dvd_d:"(ord a div gcd n (ord a)) dvd d"

   496     proof -

   497       have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq

   498         by (metis dvd_triv_right mult.commute)

   499       hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"

   500         by (simp add: mult.commute)

   501       then show ?thesis

   502         using cp by (simp add: coprime_dvd_mult_left_iff)

   503     qed

   504     have "d > 0" using d_elem by simp

   505     hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)

   506     hence False using d_lt by simp

   507   } hence ord_gcd_min: "\<And> d . d \<in> {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}

   508                         \<Longrightarrow> d\<ge>ord a div gcd n (ord a)" by fastforce

   509   have fin:"finite {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}" by auto

   510   thus ?thesis using Min_eqI[OF fin ord_gcd_min ord_gcd_elem]

   511     unfolding ord_def by simp

   512 qed

   513

   514 lemma ord_1_eq_1 :

   515   assumes "finite (carrier G)"

   516   shows "ord \<one> = 1"

   517  using assms ord_ge_1 ord_min[of 1 \<one>] by force

   518

   519 theorem lagrange_dvd:

   520  assumes "finite(carrier G)" "subgroup H G" shows "(card H) dvd (order G)"

   521  using assms by (simp add: lagrange[symmetric])

   522

   523 lemma element_generates_subgroup:

   524   assumes finite[simp]: "finite (carrier G)"

   525   assumes a[simp]: "a \<in> carrier G"

   526   shows "subgroup {a [^] i | i. i \<in> {0 .. ord a - 1}} G"

   527 proof

   528   show "{a[^]i | i. i \<in> {0 .. ord a - 1} } \<subseteq> carrier G" by auto

   529 next

   530   fix x y

   531   assume A: "x \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" "y \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"

   532   obtain i::nat where i:"x = a[^]i" and i2:"i \<in> UNIV" using A by auto

   533   obtain j::nat where j:"y = a[^]j" and j2:"j \<in> UNIV" using A by auto

   534   have "a[^](i+j) \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto

   535   thus "x \<otimes> y \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"

   536     using i j a ord_elems assms by (auto simp add: nat_pow_mult)

   537 next

   538   show "\<one> \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" by force

   539 next

   540   fix x assume x: "x \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"

   541   hence x_in_carrier: "x \<in> carrier G" by auto

   542   then obtain d::nat where d:"x [^] d = \<one>" and "d\<ge>1"

   543     using finite_group_elem_finite_ord by auto

   544   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

   545   have elem:"x [^] (d - 1) \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}"

   546   proof -

   547     obtain i::nat where i:"x = a[^]i" using x by auto

   548     hence "x[^](d - 1) \<in> {a[^]i | i. i \<in> (UNIV::nat set)}" by (auto simp add: nat_pow_pow)

   549     thus ?thesis using ord_elems[of a] by auto

   550   qed

   551   have inv:"inv x = x[^](d - 1)" using inv_equality[OF inv_1] x_in_carrier by blast

   552   thus "inv x \<in> {a[^]i | i. i \<in> {0 .. ord a - 1}}" using elem inv by auto

   553 qed

   554

   555 lemma ord_dvd_group_order :

   556   assumes finite[simp]: "finite (carrier G)"

   557   assumes a[simp]: "a \<in> carrier G"

   558   shows "ord a dvd order G"

   559 proof -

   560   have card_dvd:"card {a[^]i | i. i \<in> {0 .. ord a - 1}} dvd card (carrier G)"

   561     using lagrange_dvd element_generates_subgroup unfolding order_def by simp

   562   have "inj_on (\<lambda> i . a[^]i) {0..ord a - 1}" using ord_inj by simp

   563   hence cards_eq:"card ( (\<lambda> i . a[^]i)  {0..ord a - 1}) = card {0..ord a - 1}"

   564     using card_image[of "\<lambda> i . a[^]i" "{0..ord a - 1}"] by auto

   565   have "(\<lambda> i . a[^]i)  {0..ord a - 1} = {a[^]i | i. i \<in> {0..ord a - 1}}" by auto

   566   hence "card {a[^]i | i. i \<in> {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp

   567   also have "\<dots> = ord a" using ord_ge_1[of a] by simp

   568   finally show ?thesis using card_dvd by (simp add: order_def)

   569 qed

   570

   571 end

   572

   573

   574 section \<open>Number of Roots of a Polynomial\<close>

   575 text_raw \<open>\label{sec:number-roots}\<close>

   576

   577

   578 definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where

   579   "mult_of R \<equiv> \<lparr> carrier = carrier R - {\<zero>\<^bsub>R\<^esub>}, mult = mult R, one = \<one>\<^bsub>R\<^esub>\<rparr>"

   580

   581 lemma carrier_mult_of: "carrier (mult_of R) = carrier R - {\<zero>\<^bsub>R\<^esub>}"

   582   by (simp add: mult_of_def)

   583

   584 lemma mult_mult_of: "mult (mult_of R) = mult R"

   585  by (simp add: mult_of_def)

   586

   587 lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"

   588   by (simp add: mult_of_def fun_eq_iff nat_pow_def)

   589

   590 lemma one_mult_of: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"

   591   by (simp add: mult_of_def)

   592

   593 lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of

   594

   595 context field begin

   596

   597 lemma field_mult_group :

   598   shows "group (mult_of R)"

   599   apply (rule groupI)

   600   apply (auto simp: mult_of_simps m_assoc dest: integral)

   601   by (metis Diff_iff Units_inv_Units Units_l_inv field_Units singletonE)

   602

   603 lemma finite_mult_of: "finite (carrier R) \<Longrightarrow> finite (carrier (mult_of R))"

   604   by (auto simp: mult_of_simps)

   605

   606 lemma order_mult_of: "finite (carrier R) \<Longrightarrow> order (mult_of R) = order R - 1"

   607   unfolding order_def carrier_mult_of by (simp add: card.remove)

   608

   609 end

   610

   611

   612

   613 lemma (in monoid) Units_pow_closed :

   614   fixes d :: nat

   615   assumes "x \<in> Units G"

   616   shows "x [^] d \<in> Units G"

   617     by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)

   618

   619 lemma (in comm_monoid) is_monoid:

   620   shows "monoid G" by unfold_locales

   621

   622 declare comm_monoid.is_monoid[intro?]

   623

   624 lemma (in ring) r_right_minus_eq[simp]:

   625   assumes "a \<in> carrier R" "b \<in> carrier R"

   626   shows "a \<ominus> b = \<zero> \<longleftrightarrow> a = b"

   627   using assms by (metis a_minus_def add.inv_closed minus_equality r_neg)

   628

   629 context UP_cring begin

   630

   631 lemma is_UP_cring:"UP_cring R" by (unfold_locales)

   632 lemma is_UP_ring :

   633   shows "UP_ring R" by (unfold_locales)

   634

   635 end

   636

   637 context UP_domain begin

   638

   639

   640 lemma roots_bound:

   641   assumes f [simp]: "f \<in> carrier P"

   642   assumes f_not_zero: "f \<noteq> \<zero>\<^bsub>P\<^esub>"

   643   assumes finite: "finite (carrier R)"

   644   shows "finite {a \<in> carrier R . eval R R id a f = \<zero>} \<and>

   645          card {a \<in> carrier R . eval R R id a f = \<zero>} \<le> deg R f" using f f_not_zero

   646 proof (induction "deg R f" arbitrary: f)

   647   case 0

   648   have "\<And>x. eval R R id x f \<noteq> \<zero>"

   649   proof -

   650     fix x

   651     have "(\<Oplus>i\<in>{..deg R f}. id (coeff P f i) \<otimes> x [^] i) \<noteq> \<zero>"

   652       using 0 lcoeff_nonzero_nonzero[where p = f] by simp

   653     thus "eval R R id x f \<noteq> \<zero>" using 0 unfolding eval_def P_def by simp

   654   qed

   655   then have *: "{a \<in> carrier R. eval R R (\<lambda>a. a) a f = \<zero>} = {}"

   656     by (auto simp: id_def)

   657   show ?case by (simp add: *)

   658 next

   659   case (Suc x)

   660   show ?case

   661   proof (cases "\<exists> a \<in> carrier R . eval R R id a f = \<zero>")

   662     case True

   663     then obtain a where a_carrier[simp]: "a \<in> carrier R" and a_root:"eval R R id a f = \<zero>" by blast

   664     have R_not_triv: "carrier R \<noteq> {\<zero>}"

   665       by (metis R.one_zeroI R.zero_not_one)

   666     obtain q  where q:"(q \<in> carrier P)" and

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

   668      using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto

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

   670     have deg:"deg R (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) = 1"

   671       using a_carrier by (simp add: deg_minus_eq)

   672     hence mon_not_zero:"(monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) \<noteq> \<zero>\<^bsub>P\<^esub>"

   673       by (fastforce simp del: r_right_minus_eq)

   674     have q_not_zero:"q \<noteq> \<zero>\<^bsub>P\<^esub>" using Suc by (auto simp add : lin_fac)

   675     hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q]

   676       by (simp add : lin_fac)

   677     hence q_IH:"finite {a \<in> carrier R . eval R R id a q = \<zero>}

   678                 \<and> card {a \<in> carrier R . eval R R id a q = \<zero>} \<le> x" using Suc q q_not_zero by blast

   679     have subs:"{a \<in> carrier R . eval R R id a f = \<zero>}

   680                 \<subseteq> {a \<in> carrier R . eval R R id a q = \<zero>} \<union> {a}" (is "?L \<subseteq> ?R \<union> {a}")

   681       using a_carrier \<open>q \<in> _\<close>

   682       by (auto simp: evalRR_simps lin_fac R.integral_iff)

   683     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>}"

   684      using subs by auto

   685     hence "card {a \<in> carrier R . eval R R id a f = \<zero>} \<le>

   686            card (insert a {a \<in> carrier R . eval R R id a q = \<zero>})" using q_IH by (blast intro: card_mono)

   687     also have "\<dots> \<le> deg R f" using q_IH \<open>Suc x = _\<close>

   688       by (simp add: card_insert_if)

   689     finally show ?thesis using q_IH \<open>Suc x = _\<close> using finite by force

   690   next

   691     case False

   692     hence "card {a \<in> carrier R. eval R R id a f = \<zero>} = 0" using finite by auto

   693     also have "\<dots> \<le>  deg R f" by simp

   694     finally show ?thesis using finite by auto

   695   qed

   696 qed

   697

   698 end

   699

   700 lemma (in domain) num_roots_le_deg :

   701   fixes p d :: nat

   702   assumes finite:"finite (carrier R)"

   703   assumes d_neq_zero : "d \<noteq> 0"

   704   shows "card {x \<in> carrier R. x [^] d = \<one>} \<le> d"

   705 proof -

   706   let ?f = "monom (UP R) \<one>\<^bsub>R\<^esub> d \<ominus>\<^bsub> (UP R)\<^esub> monom (UP R) \<one>\<^bsub>R\<^esub> 0"

   707   have one_in_carrier:"\<one> \<in> carrier R" by simp

   708   interpret R: UP_domain R "UP R" by (unfold_locales)

   709   have "deg R ?f = d"

   710     using d_neq_zero by (simp add: R.deg_minus_eq)

   711   hence f_not_zero:"?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using  d_neq_zero by (auto simp add : R.deg_nzero_nzero)

   712   have roots_bound:"finite {a \<in> carrier R . eval R R id a ?f = \<zero>} \<and>

   713                     card {a \<in> carrier R . eval R R id a ?f = \<zero>} \<le> deg R ?f"

   714                     using finite by (intro R.roots_bound[OF _ f_not_zero]) simp

   715   have subs:"{x \<in> carrier R. x [^] d = \<one>} \<subseteq> {a \<in> carrier R . eval R R id a ?f = \<zero>}"

   716     by (auto simp: R.evalRR_simps)

   717   then have "card {x \<in> carrier R. x [^] d = \<one>} \<le>

   718         card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)

   719   thus ?thesis using \<open>deg R ?f = d\<close> roots_bound by linarith

   720 qed

   721

   722

   723

   724 section \<open>The Multiplicative Group of a Field\<close>

   725 text_raw \<open>\label{sec:mult-group}\<close>

   726

   727

   728 text \<open>

   729   In this section we show that the multiplicative group of a finite field

   730   is generated by a single element, i.e. it is cyclic. The proof is inspired

   731   by the first proof given in the survey~@{cite "conrad-cyclicity"}.

   732 \<close>

   733

   734 lemma (in group) pow_order_eq_1:

   735   assumes "finite (carrier G)" "x \<in> carrier G" shows "x [^] order G = \<one>"

   736   using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)

   737

   738 (* XXX remove in AFP devel, replaced by div_eq_dividend_iff *)

   739 lemma nat_div_eq: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"

   740   apply rule

   741   apply (cases "b = 0")

   742   apply simp_all

   743   apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)

   744   done

   745

   746 lemma (in group)

   747   assumes finite': "finite (carrier G)"

   748   assumes "a \<in> carrier G"

   749   shows pow_ord_eq_ord_iff: "group.ord G (a [^] k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")

   750 proof

   751   assume A: ?L then show ?R

   752     using assms ord_ge_1 [OF assms]

   753     by (auto simp: nat_div_eq ord_pow_dvd_ord_elem coprime_iff_gcd_eq_1)

   754 next

   755   assume ?R then show ?L

   756     using ord_pow_dvd_ord_elem[OF assms, of k] by auto

   757 qed

   758

   759 context field begin

   760

   761 lemma num_elems_of_ord_eq_phi':

   762   assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)"

   763       and exists: "\<exists>a\<in>carrier (mult_of R). group.ord (mult_of R) a = d"

   764   shows "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d"

   765 proof -

   766   note mult_of_simps[simp]

   767   have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)

   768

   769   interpret G:group "mult_of R" rewrites "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"

   770     by (rule field_mult_group) simp_all

   771

   772   from exists

   773   obtain a where a:"a \<in> carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"

   774     by (auto simp add: card_gt_0_iff)

   775

   776   have set_eq1:"{a[^]n| n. n \<in> {1 .. d}} = {x \<in> carrier (mult_of R). x [^] d = \<one>}"

   777   proof (rule card_seteq)

   778     show "finite {x \<in> carrier (mult_of R). x [^] d = \<one>}" using finite by auto

   779

   780     show "{a[^]n| n. n \<in> {1 ..d}} \<subseteq> {x \<in> carrier (mult_of R). x[^]d = \<one>}"

   781     proof

   782       fix x assume "x \<in> {a[^]n | n. n \<in> {1 .. d}}"

   783       then obtain n where n:"x = a[^]n \<and> n \<in> {1 .. d}" by auto

   784       have "x[^]d =(a[^]d)[^]n" using n a ord_a by (simp add:nat_pow_pow mult.commute)

   785       hence "x[^]d = \<one>" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce

   786       thus "x \<in> {x \<in> carrier (mult_of R). x[^]d = \<one>}" using G.nat_pow_closed[OF a] n by blast

   787     qed

   788

   789     show "card {x \<in> carrier (mult_of R). x [^] d = \<one>} \<le> card {a[^]n | n. n \<in> {1 .. d}}"

   790     proof -

   791       have *:"{a[^]n | n. n \<in> {1 .. d }} = ((\<lambda> n. a[^]n)  {1 .. d})" by auto

   792       have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]

   793         using card_mono[OF finite, of "{\<zero>, \<one>}"] by (simp add: order_def)

   794       have "card {x \<in> carrier (mult_of R). x [^] d = \<one>} \<le> card {x \<in> carrier R. x [^] d = \<one>}"

   795         using finite by (auto intro: card_mono)

   796       also have "\<dots> \<le> d" using \<open>0 < order (mult_of R)\<close> num_roots_le_deg[OF finite, of d]

   797         by (simp add : dvd_pos_nat[OF _ \<open>d dvd order (mult_of R)\<close>])

   798       finally show ?thesis using G.ord_inj'[OF finite' a] ord_a * by (simp add: card_image)

   799     qed

   800   qed

   801

   802   have set_eq2:"{x \<in> carrier (mult_of R) . group.ord (mult_of R) x = d}

   803                 = (\<lambda> n . a[^]n)  {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R")

   804   proof

   805     { fix x assume x:"x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d"

   806       hence "x \<in> {x \<in> carrier (mult_of R). x [^] d = \<one>}"

   807         by (simp add: G.pow_ord_eq_1[OF finite', of x, symmetric])

   808       then obtain n where n:"x = a[^]n \<and> n \<in> {1 .. d}" using set_eq1 by blast

   809       hence "x \<in> ?R" using x by fast

   810     } thus "?L \<subseteq> ?R" by blast

   811     show "?R \<subseteq> ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)

   812   qed

   813   have "inj_on (\<lambda> n . a[^]n) {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}"

   814     using G.ord_inj'[OF finite' a, unfolded ord_a] unfolding inj_on_def by fast

   815   hence "card ((\<lambda>n. a[^]n)  {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d})

   816          = card {k \<in> {1 .. d}. group.ord (mult_of R) (a[^]k) = d}"

   817          using card_image by blast

   818   thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' \<open>a \<in> _\<close>, unfolded ord_a]

   819     by (simp add: phi'_def)

   820 qed

   821

   822 end

   823

   824

   825 theorem (in field) finite_field_mult_group_has_gen :

   826   assumes finite:"finite (carrier R)"

   827   shows "\<exists> a \<in> carrier (mult_of R) . carrier (mult_of R) = {a[^]i | i::nat . i \<in> UNIV}"

   828 proof -

   829   note mult_of_simps[simp]

   830   have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)

   831

   832   interpret G: group "mult_of R" rewrites

   833       "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"

   834     by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)

   835

   836   let ?N = "\<lambda> x . card {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = x}"

   837   have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{\<zero>, \<one>}"] by simp

   838   then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of)

   839   have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force

   840

   841   have "(\<Sum>d | d dvd order (mult_of R). ?N d)

   842       = card (UN d:{d . d dvd order (mult_of R) }. {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = d})"

   843       (is "_ = card ?U")

   844     using fin finite by (subst card_UN_disjoint) auto

   845   also have "?U = carrier (mult_of R)"

   846   proof

   847     { fix x assume x:"x \<in> carrier (mult_of R)"

   848       hence x':"x\<in>carrier (mult_of R)" by simp

   849       then have "group.ord (mult_of R) x dvd order (mult_of R)"

   850           using finite' G.ord_dvd_group_order[OF _ x'] by (simp add: order_mult_of)

   851       hence "x \<in> ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast

   852     } thus "carrier (mult_of R) \<subseteq> ?U" by blast

   853   qed auto

   854   also have "card ... = order (mult_of R)"

   855     using order_mult_of finite' by (simp add: order_def)

   856   finally have sum_Ns_eq: "(\<Sum>d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .

   857

   858   { fix d assume d:"d dvd order (mult_of R)"

   859     have "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<le> phi' d"

   860     proof cases

   861       assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger

   862       next

   863       assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<noteq> 0"

   864       hence "\<exists>a \<in> carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)

   865       thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto

   866     qed

   867   }

   868   hence all_le:"\<And>i. i \<in> {d. d dvd order (mult_of R) }

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

   870   hence le:"(\<Sum>i | i dvd order (mult_of R). ?N i)

   871             \<le> (\<Sum>i | i dvd order (mult_of R). phi' i)"

   872             using sum_mono[of "{d .  d dvd order (mult_of R)}"

   873                   "\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger

   874   have "order (mult_of R) = (\<Sum>d | d dvd order (mult_of R). phi' d)" using *

   875     by (simp add: sum_phi'_factors)

   876   hence eq:"(\<Sum>i | i dvd order (mult_of R). ?N i)

   877           = (\<Sum>i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger

   878   have "\<And>i. i \<in> {d. d dvd order (mult_of R) } \<Longrightarrow> ?N i = (\<lambda>i. phi' i) i"

   879   proof (rule ccontr)

   880     fix i

   881     assume i1:"i \<in> {d. d dvd order (mult_of R)}" and "?N i \<noteq> phi' i"

   882     hence "?N i = 0"

   883       using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff)

   884     moreover  have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i])

   885     ultimately have "?N i < phi' i" using phi'_nonzero by presburger

   886     hence "(\<Sum>i | i dvd order (mult_of R). ?N i)

   887          < (\<Sum>i | i dvd order (mult_of R). phi' i)"

   888       using sum_strict_mono_ex1[OF fin, of "?N" "\<lambda> i . phi' i"]

   889             i1 all_le by auto

   890     thus False using eq by force

   891   qed

   892   hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)

   893   then obtain a where a:"a \<in> carrier (mult_of R)" and a_ord:"group.ord (mult_of R) a = order (mult_of R)"

   894     by (auto simp add: card_gt_0_iff)

   895   hence set_eq:"{a[^]i | i::nat. i \<in> UNIV} = (\<lambda>x. a[^]x)  {0 .. group.ord (mult_of R) a - 1}"

   896     using G.ord_elems[OF finite'] by auto

   897   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}"

   898     by (intro card_image G.ord_inj finite' a)

   899   hence "card ((\<lambda> x . a[^]x)  {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"

   900     using assms by (simp add: card_eq a_ord)

   901   hence card_R_minus_1:"card {a[^]i | i::nat. i \<in> UNIV} =  order (mult_of R)"

   902     using * by (subst set_eq) auto

   903   have **:"{a[^]i | i::nat. i \<in> UNIV} \<subseteq> carrier (mult_of R)"

   904     using G.nat_pow_closed[OF a] by auto

   905   with _ have "carrier (mult_of R) = {a[^]i|i::nat. i \<in> UNIV}"

   906     by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)

   907   thus ?thesis using a by blast

   908 qed

   909

   910 end
`