SSL Cyclic_Group.thy

(* 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 [^] n)"
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)) = 1" by simp
    finally have "g [^] ?d = 1" 
      using le.prems(3) pow_eq_div2 by force
    { 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 = 1› 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) = 1"
    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: carrier_conv_generator inj_on_generator inj_on_imp_bij_betw)

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