Quelle Multiplicative_Group.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Multiplicative_Group.thy
    Author:     Simon Wimmer
    Author:     Lars Noschinski
*)

theory Multiplicative_Group
imports
  Complex_Main
  Group
  Coset
  UnivPoly
  Generated_Groups
  Elementary_Groups
begin

section \<open>Simplification Rules for Polynomials\<close>
text_raw \<open>\label{sec:simp-rules}\<close>

lemma (in ring_hom_cring) hom_sub[simp]:
  assumes "x \ carrier R" "y \ carrier R"
  shows "h (x \ y) = h x \\<^bsub>S\<^esub> h y"
  using assms by (simp add: R.minus_eq S.minus_eq)

context UP_ring begin

lemma deg_nzero_nzero:
  assumes deg_p_nzero: "deg R p \ 0"
  shows "p \ \\<^bsub>P\<^esub>"
  using deg_zero deg_p_nzero by auto

lemma deg_add_eq:
  assumes c: "p \ carrier P" "q \ carrier P"
  assumes "deg R q \ deg R p"
  shows "deg R (p \\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
proof -
  let ?m = "max (deg R p) (deg R q)"
  from assms have "coeff P p ?m = \ \ coeff P q ?m \ \"
    by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1)
  then have "coeff P (p \\<^bsub>P\<^esub> q) ?m \ \"
    using assms by auto
  then have "deg R (p \\<^bsub>P\<^esub> q) \ ?m"
    using assms by (blast intro: deg_belowI)
  with deg_add[OF c] show ?thesis by arith
qed

lemma deg_minus_eq:
  assumes "p \ carrier P" "q \ carrier P" "deg R q \ deg R p"
  shows "deg R (p \\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
  using assms by (simp add: deg_add_eq a_minus_def)

end

context UP_cring begin

lemma evalRR_add:
  assumes "p \ carrier P" "q \ carrier P"
  assumes x: "x \ carrier R"
  shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemma evalRR_sub:
  assumes "p \ carrier P" "q \ carrier P"
  assumes x: "x \ carrier R"
  shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemma evalRR_mult:
  assumes "p \ carrier P" "q \ carrier P"
  assumes x: "x \ carrier R"
  shows "eval R R id x (p \\<^bsub>P\<^esub> q) = eval R R id x p \ eval R R id x q"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemma evalRR_monom:
  assumes a: "a \ carrier R" and x: "x \ carrier R"
  shows "eval R R id x (monom P a d) = a \ x [^] d"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  show ?thesis using assms by (simp add: eval_monom)
qed

lemma evalRR_one:
  assumes x: "x \ carrier R"
  shows "eval R R id x \\<^bsub>P\<^esub> = \"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemma carrier_evalRR:
  assumes x: "x \ carrier R" and "p \ carrier P"
  shows "eval R R id x p \ carrier R"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR

end

section \<open>Properties of the Euler \<open>\<phi>\<close>-function\<close>
text_raw \<open>\label{sec:euler-phi}\<close>

text\<open>
  In this section we prove that for every positive natural number the equation
  $\sum_{d | n}^n \varphi(d) = n$ holds.
\<close>

lemma dvd_div_ge_1:
  fixes a b :: nat
  assumes "a \ 1" "b dvd a"
  shows "a div b \ 1"
proof -
  from \<open>b dvd a\<close> obtain c where "a = b * c" ..
  with \<open>a \<ge> 1\<close> show ?thesis by simp
qed

lemma dvd_nat_bounds:
fixes n p :: nat
assumes "p > 0" "n dvd p"
shows "n > 0 \ n \ p"
using assms by (simp add: dvd_pos_nat dvd_imp_le)

(* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of
   HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic
   dependency. *)
definition phi' :: "nat => nat"
  where "phi' m = card {x. 1 \ x \ x \ m \ coprime x m}"

notation (latex output)
  phi' (\\ _\)

lemma phi'_nonzero:
  assumes "m > 0"
  shows "phi' m > 0"
proof -
  have "1 \ {x. 1 \ x \ x \ m \ coprime x m}" using assms by simp
  hence "card {x. 1 \ x \ x \ m \ coprime x m} > 0" by (auto simp: card_gt_0_iff)
  thus ?thesis unfolding phi'_def by simp
qed

lemma dvd_div_eq_1:
  fixes a b c :: nat
  assumes "c dvd a" "c dvd b" "a div c = b div c"
  shows "a = b" using assms dvd_mult_div_cancel[OF \<open>c dvd a\<close>] dvd_mult_div_cancel[OF \<open>c dvd b\<close>]
                by presburger

lemma dvd_div_eq_2:
  fixes a b c :: nat
  assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b"
  shows "a = b"
  proof -
  have "a > 0" "a \ c" using dvd_nat_bounds[OF assms(1-2)] by auto
  have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce
  also have "\ = b*(c div a)" using assms dvd_mult_div_cancel by fastforce
  finally show "a = b" using \<open>c>0\<close> dvd_div_ge_1[OF _ \<open>a dvd c\<close>] by fastforce
qed

lemma div_mult_mono:
  fixes a b c :: nat
  assumes "a > 0" "a\d"
  shows "a * b div d \ b"
proof -
  have "a*b div d \ b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger
  thus ?thesis using assms by force
qed

text\<open>
  We arrive at the main result of this section:
  For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.

  The outline of the proof for this lemma is as follows:
  We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$.
  We analyze the reduced form $a/d = m/n$ for any of those fractions.
  We want to know how many fractions $m/n$ have the reduced form denominator $d$.
  The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$.
  Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. \<^term>\<open>gcd a d = 1\<close>.
  This number is exactly \<^term>\<open>phi' d\<close>.

  Finally, by counting the fractions $m/n$ according to their reduced form denominator,
  we get: @{term [display] "(\d | d dvd n . phi' d) = n"}.
  To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$
  \begin{itemize}
    \item the set of reduced form numerators \<^term>\<open>{a. (1::nat) \<le> a \<and> a \<le> d \<and> coprime a d}\<close>
    \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$,
      i.e. the set \<^term>\<open>{m \<in> {1::nat .. n}. n div gcd m n = d}\<close>
  \end{itemize}
  We show that \<^term>\<open>\<lambda>a. a*n div d\<close> with the inverse \<^term>\<open>\<lambda>a. a div gcd a n\<close> is
  a bijection between theses sets, thus yielding the equality
  @{term [display] "phi' d = card {m \ {1 .. n}. n div gcd m n = d}"}
  This gives us
  @{term [display] "(\d | d dvd n . phi' d)
          = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"}
  and by showing
  \<^term>\<open>(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}\<close>
  (this is our counting argument) the thesis follows.
\<close>
lemma sum_phi'_factors:
fixes n :: nat
assumes "n > 0"
shows "(\d | d dvd n. phi' d) = n"
proof -
  have "card {a. 1 \ a \ a \ d \ coprime a d} = card {m \ {1 .. n}. n div gcd m n = d}"
    (is "card ?RF = card ?F")
    if "d dvd n" for d
  proof (rule card_bij_eq)
    from that obtain q where q: "n = d * q" ..
    have "a = b" if "a * n div d = b * n div d" for a b
    proof -
      from that have "a * (n div d) = b * (n div d)"
        using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
      then show ?thesis using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
        by (simp add: mult.commute nat_mult_eq_cancel1)
    qed
    thus "inj_on (\a. a*n div d) ?RF" unfolding inj_on_def by blast
    have "a * n div d \ ?F" if a: "a\?RF" for a
    proof -
      from that have "a * (n div d) \ 1" using \n>0\ dvd_div_ge_1[OF _ \d dvd n\] by simp
      hence ge_1: "a * n div d \ 1" by (simp add: \d dvd n\ div_mult_swap)
      have le_n: "a * n div d \ n" using div_mult_mono a by simp
      have "gcd (a * n div d) n = n div d * gcd a d"
        by (simp add: gcd_mult_distrib_nat q ac_simps)
      hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
      then show ?thesis
        using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
    qed
    thus "(\a. a*n div d) ` ?RF \ ?F" by blast
    have "m = l" if A: "m \ ?F" "l \ ?F" "m div gcd m n = l div gcd l n" for m l
    proof -
      from that have "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
      then show ?thesis using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
    qed
    thus "inj_on (\a. a div gcd a n) ?F" unfolding inj_on_def by blast
    have "m div gcd m n \ ?RF" if "m \ ?F" for m
      using that dvd_div_ge_1  by (fastforce simp add: div_le_mono div_gcd_coprime)
    thus "(\a. a div gcd a n) ` ?F \ ?RF" by blast
  qed force+
  hence phi'_eq: "\d. d dvd n \ phi' d = card {m \ {1 .. n}. n div gcd m n = d}"
    unfolding phi'_def by presburger
  have fin: "finite {d. d dvd n}" using dvd_nat_bounds[OF \<open>n>0\<close>] by force
  have "(\d | d dvd n. phi' d)
                 = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
    using card_UN_disjoint[OF fin, of "(\d. {m \ {1 .. n}. n div gcd m n = d})"] phi'_eq
    by fastforce
  also have "(\d \ {d. d dvd n}. {m \ {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R")
  proof
    show "?L \ ?R"
    proof
      fix m assume m: "m \ ?R"
      thus "m \ ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
        by simp
    qed
  qed fastforce
  finally show ?thesis by force
qed

section \<open>Order of an Element of a Group\<close>
text_raw \<open>\label{sec:order-elem}\<close>

context group begin

definition (in group) ord :: "'a \ nat" where
  "ord x \ (@d. \n::nat. x [^] n = \ \ d dvd n)"

lemma (in group) pow_eq_id:
  assumes "x \ carrier G"
  shows "x [^] n = \ \ (ord x) dvd n"
proof (cases "\n::nat. pow G x n = one G \ n = 0")
  case True
  show ?thesis
    unfolding ord_def
    by (rule someI2 [where a=0]) (auto simp: True)
next
  case False
  define N where "N \ LEAST n::nat. x [^] n = \ \ n > 0"
  have N: "x [^] N = \ \ N > 0"
    using False
    apply (simp add: N_def)
    by (metis (mono_tags, lifting) LeastI)
  have eq0: "n = 0" if "x [^] n = \" "n < N" for n
    using N_def not_less_Least that by fastforce
  show ?thesis
    unfolding ord_def
  proof (rule someI2 [where a = N], rule allI)
    fix n :: "nat"
    show "(x [^] n = \) \ (N dvd n)"
    proof (cases "n = 0")
      case False
      show ?thesis
        unfolding dvd_def
      proof safe
        assume 1: "x [^] n = \"
        have "x [^] n = x [^] (n mod N + N * (n div N))"
          by simp
        also have "\ = x [^] (n mod N) \ x [^] (N * (n div N))"
          by (simp add: assms nat_pow_mult)
        also have "\ = x [^] (n mod N)"
          by (metis N assms l_cancel_one nat_pow_closed nat_pow_one nat_pow_pow)
        finally have "x [^] (n mod N) = \"
          by (simp add: "1")
        then have "n mod N = 0"
          using N eq0 mod_less_divisor by blast
        then show "\k. n = N * k"
          by blast
      next
        fix k :: "nat"
        assume "n = N * k"
        with N show "x [^] (N * k) = \"
          by (metis assms nat_pow_one nat_pow_pow)
      qed
    qed simp
  qed blast
qed

lemma (in group) pow_ord_eq_1 [simp]:
   "x \ carrier G \ x [^] ord x = \"
  by (simp add: pow_eq_id)

lemma (in group) int_pow_eq_id:
  assumes "x \ carrier G"
  shows "(pow G x i = one G \ int (ord x) dvd i)"
proof (cases i rule: int_cases2)
  case (nonneg n)
  then show ?thesis
    by (simp add: int_pow_int pow_eq_id assms)
next
  case (nonpos n)
  then have "x [^] i = inv (x [^] n)"
    by (simp add: assms int_pow_int int_pow_neg)
  then show ?thesis
    by (simp add: assms pow_eq_id nonpos)
qed

lemma (in group) int_pow_eq:
   "x \ carrier G \ (x [^] m = x [^] n) \ int (ord x) dvd (n - m)"
  apply (simp flip: int_pow_eq_id)
  by (metis int_pow_closed int_pow_diff inv_closed r_inv right_cancel)

lemma (in group) ord_eq_0:
   "x \ carrier G \ (ord x = 0 \ (\n::nat. n \ 0 \ x [^] n \ \))"
  by (auto simp: pow_eq_id)

lemma (in group) ord_unique:
   "x \ carrier G \ ord x = d \ (\n. pow G x n = one G \ d dvd n)"
  by (meson dvd_antisym dvd_refl pow_eq_id)

lemma (in group) ord_eq_1:
   "x \ carrier G \ (ord x = 1 \ x = \)"
  by (metis pow_eq_id nat_dvd_1_iff_1 nat_pow_eone)

lemma (in group) ord_id [simp]:
   "ord (one G) = 1"
  using ord_eq_1 by blast

lemma (in group) ord_inv [simp]:
   "x \ carrier G
        \<Longrightarrow> ord (m_inv G x) = ord x"
  by (simp add: ord_unique pow_eq_id nat_pow_inv)

lemma (in group) ord_pow:
  assumes "x \ carrier G" "k dvd ord x" "k \ 0"
  shows "ord (pow G x k) = ord x div k"
proof -
  have "(x [^] k) [^] (ord x div k) = \"
    using assms by (simp add: nat_pow_pow)
  moreover have "ord x dvd k * ord (x [^] k)"
    by (metis assms(1) pow_ord_eq_1 pow_eq_id nat_pow_closed nat_pow_pow)
  ultimately show ?thesis
    by (metis assms div_dvd_div dvd_antisym dvd_triv_left pow_eq_id nat_pow_closed nonzero_mult_div_cancel_left)
qed

lemma (in group) ord_mul_divides:
  assumes eq: "x \ y = y \ x" and xy: "x \ carrier G" "y \ carrier G"
  shows "ord (x \ y) dvd (ord x * ord y)"
apply (simp add: xy flip: pow_eq_id eq)
  by (metis dvd_triv_left dvd_triv_right eq pow_eq_id one_closed pow_mult_distrib r_one xy)

lemma (in comm_group) abelian_ord_mul_divides:
   "\x \ carrier G; y \ carrier G\
        \<Longrightarrow> ord (x \<otimes> y) dvd (ord x * ord y)"
  by (simp add: ord_mul_divides m_comm)

lemma ord_inj:
  assumes a: "a \ carrier G"
  shows "inj_on (\ x . a [^] x) {0 .. ord a - 1}"
proof -
  let ?M = "Max (ord ` carrier G)"
  have "finite {d \ {..?M}. a [^] d = \}" by auto

  have *: False if A: "x < y" "x \ {0 .. ord a - 1}" "y \ {0 .. ord a - 1}"
        "a [^] x = a [^] y" for x y
  proof -
    have "y - x < ord a" using that by auto
    moreover have "a [^] (y-x) = \" using a A by (simp add: pow_eq_div2)
    ultimately have "min (y - x) (ord a) = ord a"
      using A(1) a pow_eq_id by auto
    with \<open>y - x < ord a\<close> show False by linarith
  qed
  show ?thesis
    unfolding inj_on_def by (metis nat_neq_iff *)
qed

lemma ord_inj':
  assumes a: "a \ carrier G"
  shows "inj_on (\ x . a [^] x) {1 .. ord a}"
proof (rule inj_onI, rule ccontr)
  fix x y :: nat
  assume A: "x \ {1 .. ord a}" "y \ {1 .. ord a}" "a [^] x = a [^] y" "x\y"
  then consider "x < ord a" "y < ord a" | "x = ord a" "y < ord a" | "y = ord a" "x < ord a"
    by force
  then show False
  proof cases
    case 1
    then show ?thesis using ord_inj[OF assms] A unfolding inj_on_def by fastforce
  next
    case 2
    hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
    hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
    with A show ?thesis by fastforce
  next
    case 3
    hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
    hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
    with A show ?thesis by fastforce
  qed
qed

lemma (in group) ord_ge_1:
  assumes finite: "finite (carrier G)" and a: "a \ carrier G"
  shows "ord a \ 1"
proof -
  have "((\n::nat. a [^] n) ` {0<..}) \ carrier G"
    using a by blast
  then have "finite ((\n::nat. a [^] n) ` {0<..})"
    using finite_subset finite by auto
  then have "\ inj_on (\n::nat. a [^] n) {0<..}"
    using finite_imageD infinite_Ioi by blast
  then obtain i j::nat where "i \ j" "a [^] i = a [^] j"
    by (auto simp: inj_on_def)
  then have "\n::nat. n>0 \ a [^] n = \"
    by (metis a diffs0_imp_equal pow_eq_div2 neq0_conv)
  then have "ord a \ 0"
    by (simp add: ord_eq_0 [OF a])
  then show ?thesis
    by simp
qed

lemma ord_elems:
  assumes "finite (carrier G)" "a \ carrier G"
  shows "{a[^]x | x. x \ (UNIV :: nat set)} = {a[^]x | x. x \ {0 .. ord a - 1}}" (is "?L = ?R")
proof
  show "?R \ ?L" by blast
  have "y \ {a[^]x | x. x \ {0 .. ord a - 1}}" if "y \ ?L" for y
  proof -
    from that obtain x::nat where x: "y = a[^]x" by auto
    define r q where "r = x mod ord a" and "q = x div ord a"
    then have "x = q * ord a + r"
      by (simp add: div_mult_mod_eq)
    hence "y = (a[^]ord a)[^]q \ a[^]r"
      using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
    hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
    have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
    hence "r \ {0 .. ord a - 1}" by (force simp: r_def)
    thus ?thesis using \<open>y=a[^]r\<close> by blast
  qed
  thus "?L \ ?R" by auto
qed

lemma (in group)
  assumes "x \ carrier G"
  shows finite_cyclic_subgroup:
        "finite(carrier(subgroup_generated G {x})) \ (\n::nat. n \ 0 \ x [^] n = \)" (is "?fin \ ?nat1")
    and infinite_cyclic_subgroup:
        "infinite(carrier(subgroup_generated G {x})) \ (\m n::nat. x [^] m = x [^] n \ m = n)" (is "\ ?fin \ ?nateq")
    and finite_cyclic_subgroup_int:
        "finite(carrier(subgroup_generated G {x})) \ (\i::int. i \ 0 \ x [^] i = \)" (is "?fin \ ?int1")
    and infinite_cyclic_subgroup_int:
        "infinite(carrier(subgroup_generated G {x})) \ (\i j::int. x [^] i = x [^] j \ i = j)" (is "\ ?fin \ ?inteq")
proof -
  have 1: "\ ?fin" if ?nateq
  proof -
    have "infinite (range (\n::nat. x [^] n))"
      using that range_inj_infinite [of "(\n::nat. x [^] n)"] by (auto simp: inj_on_def)
    moreover have "range (\n::nat. x [^] n) \ range (\i::int. x [^] i)"
      apply clarify
      by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI)
    ultimately show ?thesis
      using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto
  qed
  have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat
    using eq [of "int m" "int n"]
    by (simp add: int_pow_int mn)
  have 3: ?nat1 if non: "\ ?inteq"
  proof -
    obtain i j::int where eq: "x [^] i = x [^] j" and "i \ j"
      using non by auto
    show ?thesis
    proof (cases i j rule: linorder_cases)
      case less
      then have [simp]: "x [^] (j - i) = \"
        by (simp add: eq assms int_pow_diff)
      show ?thesis
        using less by (rule_tac x="nat (j-i)" in exI) auto
    next
      case greater
      then have [simp]: "x [^] (i - j) = \"
        by (simp add: eq assms int_pow_diff)
      then show ?thesis
        using greater by (rule_tac x="nat (i-j)" in exI) auto
    qed (use \<open>i \<noteq> j\<close> in auto)
  qed
  have 4: "\i::int. (i \ 0) \ x [^] i = \" if "n \ 0" "x [^] n = \" for n::nat
    apply (rule_tac x="int n" in exI)
    by (simp add: int_pow_int that)
  have 5: "finite (carrier (subgroup_generated G {x}))" if "i \ 0" and 1: "x [^] i = \" for i::int
  proof -
    obtain n::nat where n: "n > 0" "x [^] n = \"
      using "1" "3" \<open>i \<noteq> 0\<close> by fastforce
    have "x [^] a \ ([^]) x ` {0..
    proof
      show "x [^] a = x [^] nat (a mod int n)"
        using n
        by simp (metis (no_types, lifting) assms dvd_minus_mod dvd_trans int_pow_eq int_pow_eq_id int_pow_int)
      show "nat (a mod int n) \ {0..
        using n by (simp add: nat_less_iff)
    qed
    then have "carrier (subgroup_generated G {x}) \ ([^]) x ` {0..
      using carrier_subgroup_generated_by_singleton [OF assms] by auto
    then show ?thesis
      using finite_surj by blast
  qed
  show "?fin \ ?nat1" "\ ?fin \ ?nateq" "?fin \ ?int1" "\ ?fin \ ?inteq"
    using 1 2 3 4 5 by meson+
qed

lemma (in group) finite_cyclic_subgroup_order:
   "x \ carrier G \ finite(carrier(subgroup_generated G {x})) \ ord x \ 0"
  by (simp add: finite_cyclic_subgroup ord_eq_0)

lemma (in group) infinite_cyclic_subgroup_order:
   "x \ carrier G \ infinite (carrier(subgroup_generated G {x})) \ ord x = 0"
  by (simp add: finite_cyclic_subgroup_order)

lemma generate_pow_on_finite_carrier: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "finite (carrier G)" and a: "a \ carrier G"
  shows "generate G { a } = { a [^] k | k. k \ (UNIV :: nat set) }"
proof
  show "{ a [^] k | k. k \ (UNIV :: nat set) } \ generate G { a }"
  proof
    fix b assume "b \ { a [^] k | k. k \ (UNIV :: nat set) }"
    then obtain k :: nat where "b = a [^] k" by blast
    hence "b = a [^] (int k)"
      by (simp add: int_pow_int)
    thus "b \ generate G { a }"
      unfolding generate_pow[OF a] by blast
  qed
next
  show "generate G { a } \ { a [^] k | k. k \ (UNIV :: nat set) }"
  proof
    fix b assume "b \ generate G { a }"
    then obtain k :: int where k: "b = a [^] k"
      unfolding generate_pow[OF a] by blast
    show "b \ { a [^] k | k. k \ (UNIV :: nat set) }"
    proof (cases "k < 0")
      assume "\ k < 0"
      hence "b = a [^] (nat k)"
        by (simp add: k)
      thus ?thesis by blast
    next
      assume "k < 0"
      hence b: "b = inv (a [^] (nat (- k)))"
        using k a by (auto simp: int_pow_neg)
      obtain m where m: "ord a * m \ nat (- k)"
        by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)
      hence "a [^] (ord a * m) = \"
        by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
      then obtain k' :: nat where "(a [^] (nat (- k))) \ (a [^] k') = \"
        using m a nat_le_iff_add nat_pow_mult by auto
      hence "b = a [^] k'"
        using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
      thus "b \ { a [^] k | k. k \ (UNIV :: nat set) }" by blast
    qed
  qed
qed

lemma ord_elems_inf_carrier:
assumes "a \ carrier G" "ord a \ 0"
shows "{a[^]x | x. x \ (UNIV :: nat set)} = {a[^]x | x. x \ {0 .. ord a - 1}}" (is "?L = ?R")
proof
  show "?R \ ?L" by blast
  have "y \ {a[^]x | x. x \ {0 .. ord a - 1}}" if "y \ ?L" for y
  proof -
    from that obtain x::nat where x: "y = a[^]x" by auto
    define r q where "r = x mod ord a" and "q = x div ord a"
    then have "x = q * ord a + r"
      by (simp add: div_mult_mod_eq)
    hence "y = (a[^]ord a)[^]q \ a[^]r"
      using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
    hence "y = a[^]r" using assms by simp
    have "r < ord a" using assms by (simp add: r_def)
    hence "r \ {0 .. ord a - 1}" by (force simp: r_def)
    then show ?thesis using \<open>y=a[^]r\<close> by blast
  qed
  thus "?L \ ?R" by auto
qed

lemma generate_pow_nat:
assumes a: "a \ carrier G" and "ord a \ 0"
shows "generate G { a } = { a [^] k | k. k \ (UNIV :: nat set) }"
proof
show "{ a [^] k | k. k \ (UNIV :: nat set) } \ generate G { a }"
proof
   fix b assume "b \ { a [^] k | k. k \ (UNIV :: nat set) }"
   then obtain k :: nat where "b = a [^] k" by blast
   hence "b = a [^] (int k)"
     by (simp add: int_pow_int)
   thus "b \ generate G { a }"
     unfolding generate_pow[OF a] by blast
qed
next
show "generate G { a } \ { a [^] k | k. k \ (UNIV :: nat set) }"
proof
   fix b assume "b \ generate G { a }"
   then obtain k :: int where k: "b = a [^] k"
     unfolding generate_pow[OF a] by blast
   show "b \ { a [^] k | k. k \ (UNIV :: nat set) }"
   proof (cases "k < 0")
     assume "\ k < 0"
     hence "b = a [^] (nat k)"
       by (simp add: k)
     thus ?thesis by blast
   next
     assume "k < 0"
     hence b: "b = inv (a [^] (nat (- k)))"
       using k a by (auto simp: int_pow_neg)
     obtain m where m: "ord a * m \ nat (- k)"
       by (metis assms(2) dvd_imp_le dvd_triv_right le_zero_eq mult_eq_0_iff not_gr_zero)
     hence "a [^] (ord a * m) = \"
       by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
     then obtain k' :: nat where "(a [^] (nat (- k))) \ (a [^] k') = \"
       using m a nat_le_iff_add nat_pow_mult by auto
     hence "b = a [^] k'"
       using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
     thus "b \ { a [^] k | k. k \ (UNIV :: nat set) }" by blast
   qed
qed
qed

lemma generate_pow_card:
  assumes a: "a \ carrier G"
  shows "ord a = card (generate G { a })"
proof (cases "ord a = 0")
  case True
  then have "infinite (carrier (subgroup_generated G {a}))"
    using infinite_cyclic_subgroup_order[OF a] by auto
  then have "infinite (generate G {a})"
    unfolding subgroup_generated_def
    using a by simp
  then show ?thesis
    using \<open>ord a = 0\<close> by auto
next
  case finite_subgroup: False
  then have "generate G { a } = (([^]) a) ` {0..ord a - 1}"
    using generate_pow_nat ord_elems_inf_carrier a by auto
  hence "card (generate G {a}) = card {0..ord a - 1}"
    using ord_inj[OF a] card_image by metis
  also have "... = ord a" using finite_subgroup by auto
  finally show ?thesis..
qed

lemma (in group) cyclic_order_is_ord:
assumes "g \ carrier G"
shows "ord g = order (subgroup_generated G {g})"
unfolding order_def subgroup_generated_def
using assms generate_pow_card by simp

lemma ord_dvd_group_order:
  assumes "a \ carrier G" shows "(ord a) dvd (order G)"
  using lagrange[OF generate_is_subgroup[of "{a}"]] assms
  unfolding generate_pow_card[OF assms]
  by (metis dvd_triv_right empty_subsetI insert_subset)

lemma (in group) pow_order_eq_1:
  assumes "a \ carrier G" shows "a [^] order G = \"
  using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)

lemma dvd_gcd:
  fixes a b :: nat
  obtains q where "a * (b div gcd a b) = b*q"
proof
  have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add:  div_mult_swap dvd_div_mult)
  also have "\ = b * (a div gcd a b)" by simp
  finally show "a * (b div gcd a b) = b * (a div gcd a b) " .
qed

lemma (in group) ord_le_group_order:
  assumes finite: "finite (carrier G)" and a: "a \ carrier G"
  shows "ord a \ order G"
  by (simp add: a dvd_imp_le local.finite ord_dvd_group_order order_gt_0_iff_finite)

lemma (in group) ord_pow_gen:
  assumes "x \ carrier G"
  shows "ord (pow G x k) = (if k = 0 then 1 else ord x div gcd (ord x) k)"
proof -
  have "ord (x [^] k) = ord x div gcd (ord x) k"
    if "0 < k"
  proof -
    have "(d dvd k * n) = (d div gcd (d) k dvd n)" for d n
      using that by (simp add: div_dvd_iff_mult gcd_mult_distrib_nat mult.commute)
    then show ?thesis
      using that by (auto simp add: assms ord_unique nat_pow_pow pow_eq_id)
  qed
  then show ?thesis by auto
qed

lemma (in group)
  assumes finite': "finite (carrier G)" "a \ carrier G"
  shows pow_ord_eq_ord_iff: "group.ord G (a [^] k) = ord a \ coprime k (ord a)" (is "?L \ ?R")
    using assms ord_ge_1 [OF assms]
    by (auto simp: div_eq_dividend_iff ord_pow_gen coprime_iff_gcd_eq_1 gcd.commute split: if_split_asm)

lemma element_generates_subgroup:
  assumes finite[simp]: "finite (carrier G)"
  assumes a[simp]: "a \ carrier G"
  shows "subgroup {a [^] i | i. i \ {0 .. ord a - 1}} G"
  using generate_is_subgroup[of "{ a }"] assms(2)
        generate_pow_on_finite_carrier[OF assms]
  unfolding ord_elems[OF assms] by auto

end

section \<open>Number of Roots of a Polynomial\<close>
text_raw \<open>\label{sec:number-roots}\<close>

definition mult_of :: "('a, 'b) ring_scheme \ 'a monoid" where
  "mult_of R \ \ carrier = carrier R - {\\<^bsub>R\<^esub>}, mult = mult R, one = \\<^bsub>R\<^esub>\"

lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {\\<^bsub>R\<^esub>}"
  by (simp add: mult_of_def)

lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
by (simp add: mult_of_def)

lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \ nat \ _)"
  by (simp add: mult_of_def fun_eq_iff nat_pow_def)

lemma one_mult_of [simp]: "\\<^bsub>mult_of R\<^esub> = \\<^bsub>R\<^esub>"
  by (simp add: mult_of_def)

lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of

context field
begin

lemma mult_of_is_Units: "mult_of R = units_of R"
  unfolding mult_of_def units_of_def using field_Units by auto

lemma m_inv_mult_of:
"\x. x \ carrier (mult_of R) \ m_inv (mult_of R) x = m_inv R x"
  using mult_of_is_Units units_of_inv unfolding units_of_def
  by simp

lemma (in field) field_mult_group: "group (mult_of R)"
  proof (rule groupI)
  show "\y\carrier (mult_of R). y \\<^bsub>mult_of R\<^esub> x = \\<^bsub>mult_of R\<^esub>"
    if "x \ carrier (mult_of R)" for x
    using group.l_inv_ex mult_of_is_Units that units_group by fastforce
qed (auto simp: m_assoc dest: integral)

lemma finite_mult_of: "finite (carrier R) \ finite (carrier (mult_of R))"
  by simp

lemma order_mult_of: "finite (carrier R) \ order (mult_of R) = order R - 1"
  unfolding order_def carrier_mult_of by (simp add: card.remove)

end

lemma (in monoid) Units_pow_closed :
  fixes d :: nat
  assumes "x \ Units G"
  shows "x [^] d \ Units G"
    by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)

lemma (in ring) r_right_minus_eq[simp]:
  assumes "a \ carrier R" "b \ carrier R"
  shows "a \ b = \ \ a = b"
  using assms by (metis a_minus_def add.inv_closed minus_equality r_neg)

context UP_cring begin

lemma is_UP_cring: "UP_cring R" by (unfold_locales)
lemma is_UP_ring:
  shows "UP_ring R" by (unfold_locales)

end

context UP_domain begin

lemma roots_bound:
  assumes f [simp]: "f \ carrier P"
  assumes f_not_zero: "f \ \\<^bsub>P\<^esub>"
  assumes finite: "finite (carrier R)"
  shows "finite {a \ carrier R . eval R R id a f = \} \
         card {a \<in> carrier R . eval R R id a f = \<zero>} \<le> deg R f" using f f_not_zero
proof (induction "deg R f" arbitrary: f)
  case 0
  have "\x. eval R R id x f \ \"
  proof -
    fix x
    have "(\i\{..deg R f}. id (coeff P f i) \ x [^] i) \ \"
      using 0 lcoeff_nonzero_nonzero[where p = f] by simp
    thus "eval R R id x f \ \" using 0 unfolding eval_def P_def by simp
  qed
  then have *: "{a \ carrier R. eval R R (\a. a) a f = \} = {}"
    by (auto simp: id_def)
  show ?case by (simp add: *)
next
  case (Suc x)
  show ?case
  proof (cases "\ a \ carrier R . eval R R id a f = \")
    case True
    then obtain a where a_carrier[simp]: "a \ carrier R" and a_root: "eval R R id a f = \" by blast
    have R_not_triv: "carrier R \ {\}"
      by (metis R.one_zeroI R.zero_not_one)
    obtain q  where q: "(q \ carrier P)" and
      f: "f = (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> monom P (eval R R id a f) 0"
     using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto
    hence lin_fac: "f = (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \\<^bsub>P\<^esub> q" using q by (simp add: a_root)
    have deg: "deg R (monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) = 1"
      using a_carrier by (simp add: deg_minus_eq)
    hence mon_not_zero: "(monom P \\<^bsub>R\<^esub> 1 \\<^bsub> P\<^esub> monom P a 0) \ \\<^bsub>P\<^esub>"
      by (fastforce simp del: r_right_minus_eq)
    have q_not_zero: "q \ \\<^bsub>P\<^esub>" using Suc by (auto simp add : lin_fac)
    hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q]
      by (simp add : lin_fac)
    hence q_IH: "finite {a \ carrier R . eval R R id a q = \}
                \<and> card {a \<in> carrier R . eval R R id a q = \<zero>} \<le> x" using Suc q q_not_zero by blast
    have subs: "{a \ carrier R . eval R R id a f = \}
                \<subseteq> {a \<in> carrier R . eval R R id a q = \<zero>} \<union> {a}" (is "?L \<subseteq> ?R \<union> {a}")
      using a_carrier \<open>q \<in> _\<close>
      by (auto simp: evalRR_simps lin_fac R.integral_iff)
    have "{a \ carrier R . eval R R id a f = \} \ insert a {a \ carrier R . eval R R id a q = \}"
     using subs by auto
    hence "card {a \ carrier R . eval R R id a f = \} \
           card (insert a {a \<in> carrier R . eval R R id a q = \<zero>})" using q_IH by (blast intro: card_mono)
    also have "\ \ deg R f" using q_IH \Suc x = _\
      by (simp add: card_insert_if)
    finally show ?thesis using q_IH \<open>Suc x = _\<close> using finite by force
  next
    case False
    hence "card {a \ carrier R. eval R R id a f = \} = 0" using finite by auto
    also have "\ \ deg R f" by simp
    finally show ?thesis using finite by auto
  qed
qed

end

lemma (in domain) num_roots_le_deg :
  fixes p d :: nat
  assumes finite: "finite (carrier R)"
  assumes d_neq_zero: "d \ 0"
  shows "card {x \ carrier R. x [^] d = \} \ d"
proof -
  let ?f = "monom (UP R) \\<^bsub>R\<^esub> d \\<^bsub> (UP R)\<^esub> monom (UP R) \\<^bsub>R\<^esub> 0"
  have one_in_carrier: "\ \ carrier R" by simp
  interpret R: UP_domain R "UP R" by (unfold_locales)
  have "deg R ?f = d"
    using d_neq_zero by (simp add: R.deg_minus_eq)
  hence f_not_zero: "?f \ \\<^bsub>UP R\<^esub>" using d_neq_zero by (auto simp add : R.deg_nzero_nzero)
  have roots_bound: "finite {a \ carrier R . eval R R id a ?f = \} \
                    card {a \<in> carrier R . eval R R id a ?f = \<zero>} \<le> deg R ?f"
                    using finite by (intro R.roots_bound[OF _ f_not_zero]) simp
  have subs: "{x \ carrier R. x [^] d = \} \ {a \ carrier R . eval R R id a ?f = \}"
    by (auto simp: R.evalRR_simps)
  then have "card {x \ carrier R. x [^] d = \} \
        card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)
  thus ?thesis using \<open>deg R ?f = d\<close> roots_bound by linarith
qed

section \<open>The Multiplicative Group of a Field\<close>
text_raw \<open>\label{sec:mult-group}\<close>

text \<open>
  In this section we show that the multiplicative group of a finite field
  is generated by a single element, i.e. it is cyclic. The proof is inspired
  by the first proof given in the survey~\<^cite>\<open>"conrad-cyclicity"\<close>.
\<close>

context field begin

lemma num_elems_of_ord_eq_phi':
  assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)"
      and exists: "\a\carrier (mult_of R). group.ord (mult_of R) a = d"
  shows "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d"
proof -
  note mult_of_simps[simp]
  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)

  interpret G:group "mult_of R" rewrites "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \ nat \ _)" and "\\<^bsub>mult_of R\<^esub> = \"
    by (rule field_mult_group) simp_all

  from exists
  obtain a where a: "a \ carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"
    by (auto simp add: card_gt_0_iff)

  have set_eq1: "{a[^]n| n. n \ {1 .. d}} = {x \ carrier (mult_of R). x [^] d = \}"
  proof (rule card_seteq)
    show "finite {x \ carrier (mult_of R). x [^] d = \}" using finite by auto

    show "{a[^]n| n. n \ {1 ..d}} \ {x \ carrier (mult_of R). x[^]d = \}"
    proof
      fix x assume "x \ {a[^]n | n. n \ {1 .. d}}"
      then obtain n where n: "x = a[^]n \ n \ {1 .. d}" by auto
      have "x[^]d =(a[^]d)[^]n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
      hence "x[^]d = \" using ord_a G.pow_ord_eq_1[OF a] by fastforce
      thus "x \ {x \ carrier (mult_of R). x[^]d = \}" using G.nat_pow_closed[OF a] n by blast
    qed

    show "card {x \ carrier (mult_of R). x [^] d = \} \ card {a[^]n | n. n \ {1 .. d}}"
    proof -
      have *: "{a[^]n | n. n \ {1 .. d }} = ((\ n. a[^]n) ` {1 .. d})" by auto
      have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]
        using card_mono[OF finite, of "{\, \}"] by (simp add: order_def)
      have "card {x \ carrier (mult_of R). x [^] d = \} \ card {x \ carrier R. x [^] d = \}"
        using finite by (auto intro: card_mono)
      also have "\ \ d" using \0 < order (mult_of R)\ num_roots_le_deg[OF finite, of d]
        by (simp add : dvd_pos_nat[OF _ \<open>d dvd order (mult_of R)\<close>])
      finally show ?thesis using G.ord_inj'[OF a] ord_a * by (simp add: card_image)
    qed
  qed

  have set_eq2: "{x \ carrier (mult_of R) . group.ord (mult_of R) x = d}
                = (\<lambda> n . a[^]n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R")
  proof
    have "x \ ?R" if x: "x \ (carrier (mult_of R)) \ group.ord (mult_of R) x = d" for x
    proof -
      from that have "x \ {x \ carrier (mult_of R). x [^] d = \}"
        by (simp add: G.pow_ord_eq_1[of x, symmetric])
      then obtain n where n: "x = a[^]n \ n \ {1 .. d}" using set_eq1 by blast
      then show ?thesis using x by fast
    qed
    thus "?L \ ?R" by blast
    show "?R \ ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
  qed
  have "inj_on (\ n . a[^]n) {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}"
    using G.ord_inj'[OF a, unfolded ord_a] unfolding inj_on_def by fast
  hence "card ((\n. a[^]n) ` {n \ {1 .. d}. group.ord (mult_of R) (a[^]n) = d})
         = card {k \<in> {1 .. d}. group.ord (mult_of R) (a[^]k) = d}"
         using card_image by blast
  thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' \a \ _\, unfolded ord_a]
    by (simp add: phi'_def)
qed

end

theorem (in field) finite_field_mult_group_has_gen :
  assumes finite: "finite (carrier R)"
  shows "\ a \ carrier (mult_of R) . carrier (mult_of R) = {a[^]i | i::nat . i \ UNIV}"
proof -
  note mult_of_simps[simp]
  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)

  interpret G: group "mult_of R" rewrites
      "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \ nat \ _)" and "\\<^bsub>mult_of R\<^esub> = \"
    by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)

  let ?N = "\ x . card {a \ carrier (mult_of R). group.ord (mult_of R) a = x}"
  have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{\, \}"] by simp
  then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of)
  have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force

  have "(\d | d dvd order (mult_of R). ?N d)
      = card (UN d:{d . d dvd order (mult_of R) }. {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = d})"
      (is "_ = card ?U")
    using fin finite by (subst card_UN_disjoint) auto
  also have "?U = carrier (mult_of R)"
  proof
    have "x \ ?U" if x: "x \ carrier (mult_of R)" for x
    proof -
      from that have x': "x\carrier (mult_of R)" by simp
      then have "group.ord (mult_of R) x dvd order (mult_of R)"
        using G.ord_dvd_group_order by blast
      then show ?thesis
        using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
    qed
    thus "carrier (mult_of R) \ ?U" by blast
  qed auto
  also have "card ... = order (mult_of R)"
    using order_mult_of finite' by (simp add: order_def)
  finally have sum_Ns_eq: "(\d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .

  have "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} \ phi' d"
    if d: "d dvd order (mult_of R)" for d
  proof (cases "card {a \ carrier (mult_of R). group.ord (mult_of R) a = d} = 0")
    case True
    thus ?thesis by presburger
  next
    case False
    hence "\a \ carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
    thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
  qed
  hence all_le: "\i. i \ {d. d dvd order (mult_of R) }
        \<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
  hence le: "(\i | i dvd order (mult_of R). ?N i)
            \<le> (\<Sum>i | i dvd order (mult_of R). phi' i)"
            using sum_mono[of "{d . d dvd order (mult_of R)}"
                  "\i. card {a \ carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger
  have "order (mult_of R) = (\d | d dvd order (mult_of R). phi' d)" using *
    by (simp add: sum_phi'_factors)
  hence eq: "(\i | i dvd order (mult_of R). ?N i)
          = (\<Sum>i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger
  have "\i. i \ {d. d dvd order (mult_of R) } \ ?N i = (\i. phi' i) i"
  proof (rule ccontr)
    fix i
    assume i1: "i \ {d. d dvd order (mult_of R)}" and "?N i \ phi' i"
    hence "?N i = 0"
      using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff)
    moreover  have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i])
    ultimately have "?N i < phi' i" using phi'_nonzero by presburger
    hence "(\i | i dvd order (mult_of R). ?N i)
         < (\<Sum>i | i dvd order (mult_of R). phi' i)"
      using sum_strict_mono_ex1[OF fin, of "?N" "\ i . phi' i"]
            i1 all_le by auto
    thus False using eq by force
  qed
  hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)
  then obtain a where a: "a \ carrier (mult_of R)" and a_ord: "group.ord (mult_of R) a = order (mult_of R)"
    by (auto simp add: card_gt_0_iff)
  hence set_eq: "{a[^]i | i::nat. i \ UNIV} = (\x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}"
    using G.ord_elems[OF finite'] by auto
  have card_eq: "card ((\x. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}"
    by (intro card_image G.ord_inj finite' a)
  hence "card ((\ x . a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"
    using assms by (simp add: card_eq a_ord)
  hence card_R_minus_1: "card {a[^]i | i::nat. i \ UNIV} = order (mult_of R)"
    using * by (subst set_eq) auto
  have **: "{a[^]i | i::nat. i \ UNIV} \ carrier (mult_of R)"
    using G.nat_pow_closed[OF a] by auto
  with _ have "carrier (mult_of R) = {a[^]i|i::nat. i \ UNIV}"
    by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)
  thus ?thesis using a by blast
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.