Theory Cyclic_Group

(* Title: Cyclic_Group.thy
  Author: Andreas Lochbihler, ETH Zurich *)

section ‹Cyclic groups›

theory Cyclic_Group imports
  "HOL-Algebra.Coset"
begin

record 'a cyclic_group = "'a monoid" + 
  generator :: 'a ("gı")

locale cyclic_group = group G
  for G :: "('a, 'b) cyclic_group_scheme" (structure)
  +
  assumes generator_closed [intro, simp]: "generator G  carrier G"
  and generator: "carrier G  range (λn :: nat. generator G [^]Gn)"
begin

lemma generatorE [elim?]:
  assumes "x  carrier G"
  obtains n :: nat where "x = generator G [^] n"
using generator assms by auto

lemma inj_on_generator: "inj_on (([^]) g) {..<order G}"
proof(rule inj_onI)
  fix n m
  assume "n  {..<order G}" "m  {..<order G}"
  hence n: "n < order G" and m: "m < order G" by simp_all
  moreover
  assume "g [^] n = g [^] m"
  ultimately show "n = m"
  proof(induction n m rule: linorder_wlog)
    case sym thus ?case by simp
  next
    case (le n m)
    let ?d = "m - n"
    have "g [^] (int m - int n) = g [^] int m  inv (g [^] int n)"
      by(simp add: int_pow_diff)
    also have "g [^] int m = g [^] int n" by(simp add: le.prems int_pow_int)
    also have "  inv (g [^] (int n)) = 𝟭" by simp
    finally have "g [^] ?d = 𝟭" using le.hyps by(simp add: of_nat_diff[symmetric] int_pow_int)
    { assume "n < m"
      have "carrier G  (λn. g [^] n) ` {..<?d}"
      proof
        fix x
        assume "x  carrier G"
        then obtain k :: nat where "x = g [^] k" ..
        also have " = (g [^] ?d) [^] (k div ?d)  g [^] (k mod ?d)"
          by(simp add: nat_pow_pow nat_pow_mult div_mult_mod_eq)
        also have " = g [^] (k mod ?d)"
          using g [^] ?d = 𝟭 by simp
        finally show "x  (λn. g [^] n) ` {..<?d}" using n < m by auto
      qed
      hence "order G  card ((λn. g [^] n) ` {..<?d})"
        by(simp add: order_def card_mono)
      also have "  card {..<?d}" by(rule card_image_le) simp
      also have " < order G" using m < order G by simp
      finally have False by simp }
    with n  m show "n = m" by(auto simp add: order.order_iff_strict)
  qed
qed

lemma finite_carrier: "finite (carrier G)" (* contributed by Dominique Unruh *)
proof -
  from generator obtain n :: nat where "g [^] n = inv g"
    by(metis generatorE generator_closed inv_closed)
  then have g1: "g [^] (Suc n) = 𝟭"
    by auto
  have mod: "g [^] m = g [^] (m mod Suc n)" for m
  proof -
    obtain k where "m mod Suc n + Suc n * k = m"
      using mod_mult_div_eq by blast
    then have "g [^] m = g [^] (m mod Suc n + Suc n * k)" by simp
    also have " = g [^] (m mod Suc n)"
      unfolding nat_pow_mult[symmetric, OF generator_closed] nat_pow_pow[symmetric, OF generator_closed] g1
      by simp
    finally show ?thesis .
  qed
  have "g [^] x  ([^]) g ` {..<Suc n}" for x :: nat by (subst mod) auto
  then have "range (([^]) g :: nat  _)  (([^]) g) ` {..<Suc n}" by auto
  then have "finite (range (([^]) g :: nat  _))" by(rule finite_surj[rotated]) simp
  with generator show ?thesis by(rule finite_subset)
qed

lemma carrier_conv_generator: "carrier G = (λn. g [^] n) ` {..<order G}"
proof -
  have "(λn. g [^] n) ` {..<order G}  carrier G" by auto
  moreover have "card ((λn. g [^] n) ` {..<order G})  order G"
    using inj_on_generator by(simp add: card_image)
  ultimately show ?thesis using finite_carrier 
    unfolding order_def by(rule card_seteq[symmetric, rotated])
qed

lemma bij_betw_generator_carrier:
  "bij_betw (λn :: nat. g [^] n) {..<order G} (carrier G)"
by(simp add: bij_betw_def inj_on_generator carrier_conv_generator)

lemma order_gt_0: "order G > 0"
  using order_gt_0_iff_finite by(simp add: finite_carrier)

end

lemma (in monoid) order_in_range_Suc: "order G  range Suc  finite (carrier G)"
by(cases "order G")(auto simp add: order_def carrier_not_empty intro: card_ge_0_finite)

end