Quelle Group.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Group.thy
    Author:     Clemens Ballarin, started 4 February 2003

Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
*)

theory Group
imports Complete_Lattice "HOL-Library.FuncSet"
begin

section \<open>Monoids and Groups\<close>

subsection \<open>Definitions\<close>

text \<open>
  Definitions follow \<^cite>\<open>"Jacobson:1985"\<close>.
\<close>

record 'a monoid = "'a partial_object" +
  mult    :: "['a, 'a] \ 'a" (infixl \\\\ 70)
  one     :: 'a (\\\\)

definition m_inv :: "('a, 'b) monoid_scheme => 'a => 'a"
  where "m_inv G x = (THE y. y \ carrier G \ x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> \ y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>)"

open_bundle m_inv_syntax
begin
notation m_inv  (\<open>(\<open>open_block notation=\<open>prefix inv\<close>\<close>inv\<index> _)\<close> [81] 80)
end

definition
  Units :: "_ => 'a set"
  \<comment> \<open>The set of invertible elements\<close>
  where "Units G = {y. y \ carrier G \ (\x \ carrier G. x \\<^bsub>G\<^esub> y = \\<^bsub>G\<^esub> \ y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub>)}"

locale monoid =
  fixes G (structure)
  assumes m_closed [intro, simp]:
         "\x \ carrier G; y \ carrier G\ \ x \ y \ carrier G"
      and m_assoc:
         "\x \ carrier G; y \ carrier G; z \ carrier G\
          \<Longrightarrow> (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
      and one_closed [intro, simp]: "\ \ carrier G"
      and l_one [simp]: "x \ carrier G \ \ \ x = x"
      and r_one [simp]: "x \ carrier G \ x \ \ = x"

lemma monoidI:
  fixes G (structure)
  assumes m_closed:
      "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"
    and one_closed: "\ \ carrier G"
    and m_assoc:
      "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    and l_one: "!!x. x \ carrier G ==> \ \ x = x"
    and r_one: "!!x. x \ carrier G ==> x \ \ = x"
  shows "monoid G"
  by (fast intro!: monoid.intro intro: assms)

lemma (in monoid) Units_closed [dest]:
  "x \ Units G ==> x \ carrier G"
  by (unfold Units_def) fast

lemma (in monoid) one_unique:
  assumes "u \ carrier G"
    and "\x. x \ carrier G \ u \ x = x"
  shows "u = \"
  using assms(2)[OF one_closed] r_one[OF assms(1)] by simp

lemma (in monoid) inv_unique:
  assumes eq: "y \ x = \" "x \ y' = \"
    and G: "x \ carrier G" "y \ carrier G" "y' \ carrier G"
  shows "y = y'"
proof -
  from G eq have "y = y \ (x \ y')" by simp
  also from G have "... = (y \ x) \ y'" by (simp add: m_assoc)
  also from G eq have "... = y'" by simp
  finally show ?thesis .
qed

lemma (in monoid) Units_m_closed [simp, intro]:
  assumes x: "x \ Units G" and y: "y \ Units G"
  shows "x \ y \ Units G"
proof -
  from x obtain x' where x: "x \ carrier G" "x' \ carrier G" and xinv: "x \ x' = \" "x' \ x = \"
    unfolding Units_def by fast
  from y obtain y' where y: "y \ carrier G" "y' \ carrier G" and yinv: "y \ y' = \" "y' \ y = \"
    unfolding Units_def by fast
  from x y xinv yinv have "y' \ (x' \ x) \ y = \" by simp
  moreover from x y xinv yinv have "x \ (y \ y') \ x' = \" by simp
  moreover note x y
  ultimately show ?thesis unfolding Units_def
    by simp (metis m_assoc m_closed)
qed

lemma (in monoid) Units_one_closed [intro, simp]:
  "\ \ Units G"
  by (unfold Units_def) auto

lemma (in monoid) Units_inv_closed [intro, simp]:
  "x \ Units G ==> inv x \ carrier G"
  apply (simp add: Units_def m_inv_def)
  by (metis (mono_tags, lifting) inv_unique the_equality)

lemma (in monoid) Units_l_inv_ex:
  "x \ Units G ==> \y \ carrier G. y \ x = \"
  by (unfold Units_def) auto

lemma (in monoid) Units_r_inv_ex:
  "x \ Units G ==> \y \ carrier G. x \ y = \"
  by (unfold Units_def) auto

lemma (in monoid) Units_l_inv [simp]:
  "x \ Units G ==> inv x \ x = \"
  apply (unfold Units_def m_inv_def, simp)
  by (metis (mono_tags, lifting) inv_unique the_equality)

lemma (in monoid) Units_r_inv [simp]:
  "x \ Units G ==> x \ inv x = \"
  by (metis (full_types) Units_closed Units_inv_closed Units_l_inv Units_r_inv_ex inv_unique)

lemma (in monoid) inv_one [simp]:
  "inv \ = \"
  by (metis Units_one_closed Units_r_inv l_one monoid.Units_inv_closed monoid_axioms)

lemma (in monoid) Units_inv_Units [intro, simp]:
  "x \ Units G ==> inv x \ Units G"
proof -
  assume x: "x \ Units G"
  show "inv x \ Units G"
    by (auto simp add: Units_def
      intro: Units_l_inv Units_r_inv x Units_closed [OF x])
qed

lemma (in monoid) Units_l_cancel [simp]:
  "[| x \ Units G; y \ carrier G; z \ carrier G |] ==>
   (x \<otimes> y = x \<otimes> z) = (y = z)"
proof
  assume eq: "x \ y = x \ z"
    and G: "x \ Units G" "y \ carrier G" "z \ carrier G"
  then have "(inv x \ x) \ y = (inv x \ x) \ z"
    by (simp add: m_assoc Units_closed del: Units_l_inv)
  with G show "y = z" by simp
next
  assume eq: "y = z"
    and G: "x \ Units G" "y \ carrier G" "z \ carrier G"
  then show "x \ y = x \ z" by simp
qed

lemma (in monoid) Units_inv_inv [simp]:
  "x \ Units G ==> inv (inv x) = x"
proof -
  assume x: "x \ Units G"
  then have "inv x \ inv (inv x) = inv x \ x" by simp
  with x show ?thesis by (simp add: Units_closed del: Units_l_inv Units_r_inv)
qed

lemma (in monoid) inv_inj_on_Units:
  "inj_on (m_inv G) (Units G)"
proof (rule inj_onI)
  fix x y
  assume G: "x \ Units G" "y \ Units G" and eq: "inv x = inv y"
  then have "inv (inv x) = inv (inv y)" by simp
  with G show "x = y" by simp
qed

lemma (in monoid) Units_inv_comm:
  assumes inv: "x \ y = \"
    and G: "x \ Units G" "y \ Units G"
  shows "y \ x = \"
proof -
  from G have "x \ y \ x = x \ \" by (auto simp add: inv Units_closed)
  with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
qed

lemma (in monoid) carrier_not_empty: "carrier G \ {}"
by auto

(* Jacobson defines submonoid here. *)
(* Jacobson defines the order of a monoid here. *)

subsection \<open>Groups\<close>

text \<open>
  A group is a monoid all of whose elements are invertible.
\<close>

locale group = monoid +
  assumes Units: "carrier G <= Units G"

lemma (in group) is_group [iff]: "group G" by (rule group_axioms)

lemma (in group) is_monoid [iff]: "monoid G"
  by (rule monoid_axioms)

theorem groupI:
  fixes G (structure)
  assumes m_closed [simp]:
      "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"
    and one_closed [simp]: "\ \ carrier G"
    and m_assoc:
      "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    and l_one [simp]: "!!x. x \ carrier G ==> \ \ x = x"
    and l_inv_ex: "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \"
  shows "group G"
proof -
  have l_cancel [simp]:
    "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
    (x \<otimes> y = x \<otimes> z) = (y = z)"
  proof
    fix x y z
    assume eq: "x \ y = x \ z"
      and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"
    with l_inv_ex obtain x_inv where xG: "x_inv \ carrier G"
      and l_inv: "x_inv \ x = \" by fast
    from G eq xG have "(x_inv \ x) \ y = (x_inv \ x) \ z"
      by (simp add: m_assoc)
    with G show "y = z" by (simp add: l_inv)
  next
    fix x y z
    assume eq: "y = z"
      and G: "x \ carrier G" "y \ carrier G" "z \ carrier G"
    then show "x \ y = x \ z" by simp
  qed
  have r_one:
    "!!x. x \ carrier G ==> x \ \ = x"
  proof -
    fix x
    assume x: "x \ carrier G"
    with l_inv_ex obtain x_inv where xG: "x_inv \ carrier G"
      and l_inv: "x_inv \ x = \" by fast
    from x xG have "x_inv \ (x \ \) = x_inv \ x"
      by (simp add: m_assoc [symmetric] l_inv)
    with x xG show "x \ \ = x" by simp
  qed
  have inv_ex:
    "\x. x \ carrier G \ \y \ carrier G. y \ x = \ \ x \ y = \"
  proof -
    fix x
    assume x: "x \ carrier G"
    with l_inv_ex obtain y where y: "y \ carrier G"
      and l_inv: "y \ x = \" by fast
    from x y have "y \ (x \ y) = y \ \"
      by (simp add: m_assoc [symmetric] l_inv r_one)
    with x y have r_inv: "x \ y = \"
      by simp
    from x y show "\y \ carrier G. y \ x = \ \ x \ y = \"
      by (fast intro: l_inv r_inv)
  qed
  then have carrier_subset_Units: "carrier G \ Units G"
    by (unfold Units_def) fast
  show ?thesis
    by standard (auto simp: r_one m_assoc carrier_subset_Units)
qed

lemma (in monoid) group_l_invI:
  assumes l_inv_ex:
    "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \"
  shows "group G"
  by (rule groupI) (auto intro: m_assoc l_inv_ex)

lemma (in group) Units_eq [simp]:
  "Units G = carrier G"
proof
  show "Units G \ carrier G" by fast
next
  show "carrier G \ Units G" by (rule Units)
qed

lemma (in group) inv_closed [intro, simp]:
  "x \ carrier G ==> inv x \ carrier G"
  using Units_inv_closed by simp

lemma (in group) l_inv_ex [simp]:
  "x \ carrier G ==> \y \ carrier G. y \ x = \"
  using Units_l_inv_ex by simp

lemma (in group) r_inv_ex [simp]:
  "x \ carrier G ==> \y \ carrier G. x \ y = \"
  using Units_r_inv_ex by simp

lemma (in group) l_inv [simp]:
  "x \ carrier G ==> inv x \ x = \"
  by simp

subsection \<open>Cancellation Laws and Basic Properties\<close>

lemma (in group) inv_eq_1_iff [simp]:
  assumes "x \ carrier G" shows "inv\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub> \ x = \\<^bsub>G\<^esub>"
proof -
  have "x = \" if "inv x = \"
  proof -
    have "inv x \ x = \"
      using assms l_inv by blast
    then show "x = \"
      using that assms by simp
  qed
  then show ?thesis
    by auto
qed

lemma (in group) r_inv [simp]:
  "x \ carrier G ==> x \ inv x = \"
  by simp

lemma (in group) right_cancel [simp]:
  "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
   (y \<otimes> x = z \<otimes> x) = (y = z)"
  by (metis inv_closed m_assoc r_inv r_one)

lemma (in group) inv_inv [simp]:
  "x \ carrier G ==> inv (inv x) = x"
  using Units_inv_inv by simp

lemma (in group) inv_inj:
  "inj_on (m_inv G) (carrier G)"
  using inv_inj_on_Units by simp

lemma (in group) inv_mult_group:
  "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv y \ inv x"
proof -
  assume G: "x \ carrier G" "y \ carrier G"
  then have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ y)"
    by (simp add: m_assoc) (simp add: m_assoc [symmetric])
  with G show ?thesis by (simp del: l_inv Units_l_inv)
qed

lemma (in group) inv_comm:
  "[| x \ y = \; x \ carrier G; y \ carrier G |] ==> y \ x = \"
  by (rule Units_inv_comm) auto

lemma (in group) inv_equality:
     "[|y \ x = \; x \ carrier G; y \ carrier G|] ==> inv x = y"
  using inv_unique r_inv by blast

lemma (in group) inv_solve_left:
  "\ a \ carrier G; b \ carrier G; c \ carrier G \ \ a = inv b \ c \ c = b \ a"
  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)

lemma (in group) inv_solve_left':
  "\ a \ carrier G; b \ carrier G; c \ carrier G \ \ inv b \ c = a \ c = b \ a"
  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)

lemma (in group) inv_solve_right:
  "\ a \ carrier G; b \ carrier G; c \ carrier G \ \ a = b \ inv c \ b = a \ c"
  by (metis inv_equality l_inv_ex l_one m_assoc r_inv)

lemma (in group) inv_solve_right':
  "\a \ carrier G; b \ carrier G; c \ carrier G\ \ b \ inv c = a \ b = a \ c"
  by (auto simp: m_assoc)


subsection \<open>Power\<close>

consts
  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr \<open>[^]\<index>\<close> 75)

overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
begin
  definition "nat_pow G a n = rec_nat \\<^bsub>G\<^esub> (%u b. b \\<^bsub>G\<^esub> a) n"
end

lemma (in monoid) nat_pow_closed [intro, simp]:
  "x \ carrier G ==> x [^] (n::nat) \ carrier G"
  by (induct n) (simp_all add: nat_pow_def)

lemma (in monoid) nat_pow_0 [simp]:
  "x [^] (0::nat) = \"
  by (simp add: nat_pow_def)

lemma (in monoid) nat_pow_Suc [simp]:
  "x [^] (Suc n) = x [^] n \ x"
  by (simp add: nat_pow_def)

lemma (in monoid) nat_pow_one [simp]:
  "\ [^] (n::nat) = \"
  by (induct n) simp_all

lemma (in monoid) nat_pow_mult:
  "x \ carrier G ==> x [^] (n::nat) \ x [^] m = x [^] (n + m)"
  by (induct m) (simp_all add: m_assoc [THEN sym])

lemma (in monoid) nat_pow_comm:
  "x \ carrier G \ (x [^] (n::nat)) \ (x [^] (m :: nat)) = (x [^] m) \ (x [^] n)"
  using nat_pow_mult[of x n m] nat_pow_mult[of x m n] by (simp add: add.commute)

lemma (in monoid) nat_pow_Suc2:
  "x \ carrier G \ x [^] (Suc n) = x \ (x [^] n)"
  using nat_pow_mult[of x 1 n] Suc_eq_plus1[of n]
  by (metis One_nat_def Suc_eq_plus1_left l_one nat.rec(1) nat_pow_Suc nat_pow_def)

lemma (in monoid) nat_pow_pow:
  "x \ carrier G ==> (x [^] n) [^] m = x [^] (n * m::nat)"
  by (induct m) (simp, simp add: nat_pow_mult add.commute)

lemma (in monoid) nat_pow_consistent:
  "x [^] (n :: nat) = x [^]\<^bsub>(G \ carrier := H \)\<^esub> n"
  unfolding nat_pow_def by simp

lemma nat_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::nat) = \\<^bsub>G\<^esub>"
  by (simp add: nat_pow_def)

lemma nat_pow_Suc [simp]: "x [^]\<^bsub>G\<^esub> (Suc n) = (x [^]\<^bsub>G\<^esub> n)\\<^bsub>G\<^esub> x"
  by (simp add: nat_pow_def)

lemma (in group) nat_pow_inv:
  assumes "x \ carrier G" shows "(inv x) [^] (i :: nat) = inv (x [^] i)"
proof (induction i)
  case 0 thus ?case by simp
next
  case (Suc i)
  have "(inv x) [^] Suc i = ((inv x) [^] i) \ inv x"
    by simp
  also have " ... = (inv (x [^] i)) \ inv x"
    by (simp add: Suc.IH Suc.prems)
  also have " ... = inv (x \ (x [^] i))"
    by (simp add: assms inv_mult_group)
  also have " ... = inv (x [^] (Suc i))"
    using assms nat_pow_Suc2 by auto
  finally show ?case .
qed

overloading int_pow == "pow :: [_, 'a, int] => 'a"
begin
  definition "int_pow G a z =
   (let p = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
end

lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
  by(simp add: int_pow_def nat_pow_def)

lemma pow_nat:
  assumes "i\0"
  shows "x [^]\<^bsub>G\<^esub> nat i = x [^]\<^bsub>G\<^esub> i"
proof (cases i rule: int_cases)
  case (nonneg n)
  then show ?thesis
    by (simp add: int_pow_int)
next
  case (neg n)
  then show ?thesis
    using assms by linarith
qed

lemma int_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::int) = \\<^bsub>G\<^esub>"
  by (simp add: int_pow_def)

lemma int_pow_def2: "a [^]\<^bsub>G\<^esub> z =
   (if z < 0 then inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> (nat (-z))) else a [^]\<^bsub>G\<^esub> (nat z))"
  by (simp add: int_pow_def nat_pow_def)

lemma (in group) int_pow_one [simp]:
  "\ [^] (z::int) = \"
  by (simp add: int_pow_def2)

lemma (in group) int_pow_closed [intro, simp]:
  "x \ carrier G ==> x [^] (i::int) \ carrier G"
  by (simp add: int_pow_def2)

lemma (in group) int_pow_1 [simp]:
  "x \ carrier G \ x [^] (1::int) = x"
  by (simp add: int_pow_def2)

lemma (in group) int_pow_neg:
  "x \ carrier G \ x [^] (-i::int) = inv (x [^] i)"
  by (simp add: int_pow_def2)

lemma (in group) int_pow_neg_int: "x \ carrier G \ x [^] -(int n) = inv (x [^] n)"
  by (simp add: int_pow_neg int_pow_int)

lemma (in group) int_pow_mult:
  assumes "x \ carrier G" shows "x [^] (i + j::int) = x [^] i \ x [^] j"
proof -
  have [simp]: "-i - j = -j - i" by simp
  show ?thesis
    by (auto simp: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult)
qed

lemma (in group) int_pow_inv:
  "x \ carrier G \ (inv x) [^] (i :: int) = inv (x [^] i)"
  by (metis int_pow_def2 nat_pow_inv)

lemma (in group) int_pow_pow:
  assumes "x \ carrier G"
  shows "(x [^] (n :: int)) [^] (m :: int) = x [^] (n * m :: int)"
proof (cases)
  assume n_ge: "n \ 0" thus ?thesis
  proof (cases)
    assume m_ge: "m \ 0" thus ?thesis
      using n_ge nat_pow_pow[OF assms, of "nat n" "nat m"] int_pow_def2 [where G=G]
      by (simp add: mult_less_0_iff nat_mult_distrib)
  next
    assume m_lt: "\ m \ 0"
    with n_ge show ?thesis
      apply (simp add: int_pow_def2 mult_less_0_iff)
      by (metis assms mult_minus_right n_ge nat_mult_distrib nat_pow_pow)
  qed
next
  assume n_lt: "\ n \ 0" thus ?thesis
  proof (cases)
    assume m_ge: "m \ 0"
    have "inv x [^] (nat m * nat (- n)) = inv x [^] nat (- (m * n))"
      by (metis (full_types) m_ge mult_minus_right nat_mult_distrib)
    with m_ge n_lt show ?thesis
      by (simp add: int_pow_def2 mult_less_0_iff assms mult.commute nat_pow_inv nat_pow_pow)
  next
    assume m_lt: "\ m \ 0" thus ?thesis
      using n_lt by (auto simp: int_pow_def2 mult_less_0_iff assms nat_mult_distrib_neg nat_pow_inv nat_pow_pow)
  qed
qed

lemma (in group) int_pow_diff:
  "x \ carrier G \ x [^] (n - m :: int) = x [^] n \ inv (x [^] m)"
  by(simp only: diff_conv_add_uminus int_pow_mult int_pow_neg)

lemma (in group) inj_on_multc: "c \ carrier G \ inj_on (\x. x \ c) (carrier G)"
  by(simp add: inj_on_def)

lemma (in group) inj_on_cmult: "c \ carrier G \ inj_on (\x. c \ x) (carrier G)"
  by(simp add: inj_on_def)

lemma (in monoid) group_commutes_pow:
  fixes n::nat
  shows "\x \ y = y \ x; x \ carrier G; y \ carrier G\ \ x [^] n \ y = y \ x [^] n"
  apply (induction n, auto)
  by (metis m_assoc nat_pow_closed)

lemma (in monoid) pow_mult_distrib:
  assumes eq: "x \ y = y \ x" and xy: "x \ carrier G" "y \ carrier G"
  shows "(x \ y) [^] (n::nat) = x [^] n \ y [^] n"
proof (induct n)
  case (Suc n)
  have "x \ (y [^] n \ y) = y [^] n \ x \ y"
    by (simp add: eq group_commutes_pow m_assoc xy)
  then show ?case
    using assms Suc.hyps m_assoc by auto
qed auto

lemma (in group) int_pow_mult_distrib:
  assumes eq: "x \ y = y \ x" and xy: "x \ carrier G" "y \ carrier G"
  shows "(x \ y) [^] (i::int) = x [^] i \ y [^] i"
proof (cases i rule: int_cases)
  case (nonneg n)
  then show ?thesis
    by (metis eq int_pow_int pow_mult_distrib xy)
next
  case (neg n)
  then show ?thesis
    unfolding neg
    apply (simp add: xy int_pow_neg_int del: of_nat_Suc)
    by (metis eq inv_mult_group local.nat_pow_Suc nat_pow_closed pow_mult_distrib xy)
qed

lemma (in group) pow_eq_div2:
  fixes m n :: nat
  assumes x_car: "x \ carrier G"
  assumes pow_eq: "x [^] m = x [^] n"
  shows "x [^] (m - n) = \"
proof (cases "m < n")
  case False
  have "\ \ x [^] m = x [^] m" by (simp add: x_car)
  also have "\ = x [^] (m - n) \ x [^] n"
    using False by (simp add: nat_pow_mult x_car)
  also have "\ = x [^] (m - n) \ x [^] m"
    by (simp add: pow_eq)
  finally show ?thesis
    by (metis nat_pow_closed one_closed right_cancel x_car)
qed simp

subsection \<open>Submonoids\<close>

locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  fixes H and G (structure)
  assumes subset: "H \ carrier G"
    and m_closed [intro, simp]: "\x \ H; y \ H\ \ x \ y \ H"
    and one_closed [simp]: "\ \ H"

lemma (in submonoid) is_submonoid: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  "submonoid H G" by (rule submonoid_axioms)

lemma (in submonoid) mem_carrier [simp]: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  "x \ H \ x \ carrier G"
  using subset by blast

lemma (in submonoid) submonoid_is_monoid [intro]: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  assumes "monoid G"
  shows "monoid (G\carrier := H\)"
proof -
  interpret monoid G by fact
  show ?thesis
    by (simp add: monoid_def m_assoc)
qed

lemma submonoid_nonempty: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  "~ submonoid {} G"
  by (blast dest: submonoid.one_closed)

lemma (in submonoid) finite_monoid_imp_card_positive: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  "finite (carrier G) ==> 0 < card H"
proof (rule classical)
  assume "finite (carrier G)" and a: "~ 0 < card H"
  then have "finite H" by (blast intro: finite_subset [OF subset])
  with is_submonoid a have "submonoid {} G" by simp
  with submonoid_nonempty show ?thesis by contradiction
qed

lemma (in monoid) monoid_incl_imp_submonoid : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  assumes "H \ carrier G"
and "monoid (G\carrier := H\)"
shows "submonoid H G"
proof (intro submonoid.intro[OF assms(1)])
  have ab_eq : "\ a b. a \ H \ b \ H \ a \\<^bsub>G\carrier := H\\<^esub> b = a \ b" using assms by simp
  have "\a b. a \ H \ b \ H \ a \ b \ carrier (G\carrier := H\) "
    using assms ab_eq unfolding group_def using monoid.m_closed by fastforce
  thus "\a b. a \ H \ b \ H \ a \ b \ H" by simp
  show "\ \ H " using monoid.one_closed[OF assms(2)] assms by simp
qed

lemma (in monoid) inv_unique': \<^marker>\contributor \Martin Baillon\\
  assumes "x \ carrier G" "y \ carrier G"
  shows "\ x \ y = \; y \ x = \ \ \ y = inv x"
proof -
  assume "x \ y = \" and l_inv: "y \ x = \"
  hence unit: "x \ Units G"
    using assms unfolding Units_def by auto
  show "y = inv x"
    using inv_unique[OF l_inv Units_r_inv[OF unit] assms Units_inv_closed[OF unit]] .
qed

lemma (in monoid) m_inv_monoid_consistent: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "x \ Units (G \ carrier := H \)" and "submonoid H G"
  shows "inv\<^bsub>(G \ carrier := H \)\<^esub> x = inv x"
proof -
  have monoid: "monoid (G \ carrier := H \)"
    using submonoid.submonoid_is_monoid[OF assms(2) monoid_axioms] .
  obtain y where y: "y \ H" "x \ y = \" "y \ x = \"
    using assms(1) unfolding Units_def by auto
  have x: "x \ H" and in_carrier: "x \ carrier G" "y \ carrier G"
    using y(1) submonoid.subset[OF assms(2)] assms(1) unfolding Units_def by auto
  show ?thesis
    using monoid.inv_unique'[OF monoid, of x y] x y
    using inv_unique'[OF in_carrier y(2-3)] by auto
qed

subsection \<open>Subgroups\<close>

locale subgroup =
  fixes H and G (structure)
  assumes subset: "H \ carrier G"
    and m_closed [intro, simp]: "\x \ H; y \ H\ \ x \ y \ H"
    and one_closed [simp]: "\ \ H"
    and m_inv_closed [intro,simp]: "x \ H \ inv x \ H"

lemma (in subgroup) is_subgroup:
  "subgroup H G" by (rule subgroup_axioms)

declare (in subgroup) group.intro [intro]

lemma (in subgroup) mem_carrier [simp]:
  "x \ H \ x \ carrier G"
  using subset by blast

lemma (in subgroup) subgroup_is_group [intro]:
  assumes "group G"
  shows "group (G\carrier := H\)"
proof -
  interpret group G by fact
  have "Group.monoid (G\carrier := H\)"
    by (simp add: monoid_axioms submonoid.intro submonoid.submonoid_is_monoid subset)
  then show ?thesis
    by (rule monoid.group_l_invI) (auto intro: l_inv mem_carrier)
qed

lemma (in group) triv_subgroup: "subgroup {\} G"
  by (auto simp: subgroup_def)

lemma subgroup_is_submonoid:
  assumes "subgroup H G" shows "submonoid H G"
  using assms by (auto intro: submonoid.intro simp add: subgroup_def)

lemma (in group) subgroup_Units:
  assumes "subgroup H G" shows "H \ Units (G \ carrier := H \)"
  using group.Units[OF subgroup.subgroup_is_group[OF assms group_axioms]] by simp

lemma (in group) m_inv_consistent [simp]:
  assumes "subgroup H G" "x \ H"
  shows "inv\<^bsub>(G \ carrier := H \)\<^esub> x = inv x"
  using assms m_inv_monoid_consistent[OF _ subgroup_is_submonoid] subgroup_Units[of H] by auto

lemma (in group) int_pow_consistent: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "subgroup H G" "x \ H"
  shows "x [^] (n :: int) = x [^]\<^bsub>(G \ carrier := H \)\<^esub> n"
proof (cases)
  assume ge: "n \ 0"
  hence "x [^] n = x [^] (nat n)"
    using int_pow_def2 [of G] by auto
  also have " ... = x [^]\<^bsub>(G \ carrier := H \)\<^esub> (nat n)"
    using nat_pow_consistent by simp
  also have " ... = x [^]\<^bsub>(G \ carrier := H \)\<^esub> n"
    by (metis ge int_nat_eq int_pow_int)
  finally show ?thesis .
next
  assume "\ n \ 0" hence lt: "n < 0" by simp
  hence "x [^] n = inv (x [^] (nat (- n)))"
    using int_pow_def2 [of G] by auto
  also have " ... = (inv x) [^] (nat (- n))"
    by (metis assms nat_pow_inv subgroup.mem_carrier)
  also have " ... = (inv\<^bsub>(G \ carrier := H \)\<^esub> x) [^]\<^bsub>(G \ carrier := H \)\<^esub> (nat (- n))"
    using m_inv_consistent[OF assms] nat_pow_consistent by auto
  also have " ... = inv\<^bsub>(G \ carrier := H \)\<^esub> (x [^]\<^bsub>(G \ carrier := H \)\<^esub> (nat (- n)))"
    using group.nat_pow_inv[OF subgroup.subgroup_is_group[OF assms(1) is_group]] assms(2) by auto
  also have " ... = x [^]\<^bsub>(G \ carrier := H \)\<^esub> n"
    by (simp add: int_pow_def2 lt)
  finally show ?thesis .
qed

text \<open>
  Since \<^term>\<open>H\<close> is nonempty, it contains some element \<^term>\<open>x\<close>.  Since
  it is closed under inverse, it contains \<open>inv x\<close>.  Since
  it is closed under product, it contains \<open>x \<otimes> inv x = \<one>\<close>.
\<close>

lemma (in group) one_in_subset:
  "\H \ carrier G; H \ {}; \a \ H. inv a \ H; \a\H. \b\H. a \ b \ H\
   \<Longrightarrow> \<one> \<in> H"
by force

text \<open>A characterization of subgroups: closed, non-empty subset.\<close>

lemma (in group) subgroupI:
  assumes subset: "H \ carrier G" and non_empty: "H \ {}"
    and inv: "!!a. a \ H \ inv a \ H"
    and mult: "!!a b. \a \ H; b \ H\ \ a \ b \ H"
  shows "subgroup H G"
proof (simp add: subgroup_def assms)
  show "\ \ H" by (rule one_in_subset) (auto simp only: assms)
qed

lemma (in group) subgroupE:
  assumes "subgroup H G"
  shows "H \ carrier G"
    and "H \ {}"
    and "\a. a \ H \ inv a \ H"
    and "\a b. \ a \ H; b \ H \ \ a \ b \ H"
  using assms unfolding subgroup_def[of H G] by auto

declare monoid.one_closed [iff] group.inv_closed [simp]
  monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp]

lemma subgroup_nonempty:
  "\ subgroup {} G"
  by (blast dest: subgroup.one_closed)

lemma (in subgroup) finite_imp_card_positive: "finite (carrier G) \ 0 < card H"
  using subset one_closed card_gt_0_iff finite_subset by blast

lemma (in subgroup) subgroup_is_submonoid : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  "submonoid H G"
  by (simp add: submonoid.intro subset)

lemma (in group) submonoid_subgroupI : \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  assumes "submonoid H G"
    and "\a. a \ H \ inv a \ H"
  shows "subgroup H G"
  by (metis assms subgroup_def submonoid_def)

lemma (in group) group_incl_imp_subgroup: \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
  assumes "H \ carrier G"
    and "group (G\carrier := H\)"
  shows "subgroup H G"
proof (intro submonoid_subgroupI[OF monoid_incl_imp_submonoid[OF assms(1)]])
  show "monoid (G\carrier := H\)" using group_def assms by blast
  have ab_eq : "\ a b. a \ H \ b \ H \ a \\<^bsub>G\carrier := H\\<^esub> b = a \ b" using assms by simp
  fix a  assume aH : "a \ H"
  have " inv\<^bsub>G\carrier := H\\<^esub> a \ carrier G"
    using assms aH group.inv_closed[OF assms(2)] by auto
  moreover have "\\<^bsub>G\carrier := H\\<^esub> = \" using assms monoid.one_closed ab_eq one_def by simp
  hence "a \\<^bsub>G\carrier := H\\<^esub> inv\<^bsub>G\carrier := H\\<^esub> a= \"
    using assms ab_eq aH  group.r_inv[OF assms(2)] by simp
  hence "a \ inv\<^bsub>G\carrier := H\\<^esub> a= \"
    using aH assms group.inv_closed[OF assms(2)] ab_eq by simp
  ultimately have "inv\<^bsub>G\carrier := H\\<^esub> a = inv a"
    by (metis aH assms(1) contra_subsetD group.inv_inv is_group local.inv_equality)
  moreover have "inv\<^bsub>G\carrier := H\\<^esub> a \ H"
    using aH group.inv_closed[OF assms(2)] by auto
  ultimately show "inv a \ H" by auto
qed

subsection \<open>Direct Products\<close>

definition
  DirProd :: "_ \ _ \ ('a \ 'b) monoid" (infixr \\\\ 80) where
  "G \\ H =
    \<lparr>carrier = carrier G \<times> carrier H,
     mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
     one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"

lemma DirProd_monoid:
  assumes "monoid G" and "monoid H"
  shows "monoid (G \\ H)"
proof -
  interpret G: monoid G by fact
  interpret H: monoid H by fact
  from assms
  show ?thesis by (unfold monoid_def DirProd_def, auto)
qed

text\<open>Does not use the previous result because it's easier just to use auto.\<close>
lemma DirProd_group:
  assumes "group G" and "group H"
  shows "group (G \\ H)"
proof -
  interpret G: group G by fact
  interpret H: group H by fact
  show ?thesis by (rule groupI)
     (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
           simp add: DirProd_def)
qed

lemma carrier_DirProd [simp]: "carrier (G \\ H) = carrier G \ carrier H"
  by (simp add: DirProd_def)

lemma one_DirProd [simp]: "\\<^bsub>G \\ H\<^esub> = (\\<^bsub>G\<^esub>, \\<^bsub>H\<^esub>)"
  by (simp add: DirProd_def)

lemma mult_DirProd [simp]: "(g, h) \\<^bsub>(G \\ H)\<^esub> (g', h') = (g \\<^bsub>G\<^esub> g', h \\<^bsub>H\<^esub> h')"
  by (simp add: DirProd_def)

lemma mult_DirProd': "x \\<^bsub>(G \\ H)\<^esub> y = (fst x \\<^bsub>G\<^esub> fst y, snd x \\<^bsub>H\<^esub> snd y)"
  by (subst mult_DirProd [symmetric]) simp

lemma DirProd_assoc: "(G \\ H \\ I) = (G \\ (H \\ I))"
  by auto

lemma inv_DirProd [simp]:
  assumes "group G" and "group H"
  assumes g: "g \ carrier G"
      and h: "h \ carrier H"
  shows "m_inv (G \\ H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
proof -
  interpret G: group G by fact
  interpret H: group H by fact
  interpret Prod: group "G \\ H"
    by (auto intro: DirProd_group group.intro group.axioms assms)
  show ?thesis by (simp add: Prod.inv_equality g h)
qed

lemma DirProd_subgroups :
  assumes "group G"
    and "subgroup H G"
    and "group K"
    and "subgroup I K"
  shows "subgroup (H \ I) (G \\ K)"
proof (intro group.group_incl_imp_subgroup[OF DirProd_group[OF assms(1)assms(3)]])
  have "H \ carrier G" "I \ carrier K" using subgroup.subset assms by blast+
  thus "(H \ I) \ carrier (G \\ K)" unfolding DirProd_def by auto
  have "Group.group ((G\carrier := H\) \\ (K\carrier := I\))"
    using DirProd_group[OF subgroup.subgroup_is_group[OF assms(2)assms(1)]
        subgroup.subgroup_is_group[OF assms(4)assms(3)]].
  moreover have "((G\carrier := H\) \\ (K\carrier := I\)) = ((G \\ K)\carrier := H \ I\)"
    unfolding DirProd_def using assms by simp
  ultimately show "Group.group ((G \\ K)\carrier := H \ I\)" by simp
qed

subsection \<open>Homomorphisms (mono and epi) and Isomorphisms\<close>

definition
  hom :: "_ => _ => ('a => 'b) set" where
  "hom G H =
    {h. h \<in> carrier G \<rightarrow> carrier H \<and>
      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"

lemma homI:
  "\\x. x \ carrier G \ h x \ carrier H;
    \<And>x y. \<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y\<rbrakk> \<Longrightarrow> h \<in> hom G H"
  by (auto simp: hom_def)

lemma hom_carrier: "h \ hom G H \ h ` carrier G \ carrier H"
  by (auto simp: hom_def)

lemma hom_in_carrier: "\h \ hom G H; x \ carrier G\ \ h x \ carrier H"
  by (auto simp: hom_def)

lemma hom_compose:
  "\ f \ hom G H; g \ hom H I \ \ g \ f \ hom G I"
  unfolding hom_def by (auto simp add: Pi_iff)

lemma (in group) hom_restrict:
  assumes "h \ hom G H" and "\g. g \ carrier G \ h g = t g" shows "t \ hom G H"
  using assms unfolding hom_def by (auto simp add: Pi_iff)

lemma (in group) hom_compose:
  "[|h \ hom G H; i \ hom H I|] ==> compose (carrier G) i h \ hom G I"
by (fastforce simp add: hom_def compose_def)

lemma (in group) restrict_hom_iff [simp]:
  "(\x. if x \ carrier G then f x else g x) \ hom G H \ f \ hom G H"
  by (simp add: hom_def Pi_iff)

definition iso :: "_ => _ => ('a => 'b) set"
  where "iso G H = {h. h \ hom G H \ bij_betw h (carrier G) (carrier H)}"

definition is_iso :: "_ \ _ \ bool" (infixr \\\ 60)
  where "G \ H = (iso G H \ {})"

definition mon where "mon G H = {f \ hom G H. inj_on f (carrier G)}"

definition epi where "epi G H = {f \ hom G H. f ` (carrier G) = carrier H}"

lemma isoI:
  "\h \ hom G H; bij_betw h (carrier G) (carrier H)\ \ h \ iso G H"
  by (auto simp: iso_def)

lemma is_isoI: "h \ iso G H \ G \ H"
  using is_iso_def by auto

lemma epi_iff_subset:
   "f \ epi G G' \ f \ hom G G' \ carrier G' \ f ` carrier G"
  by (auto simp: epi_def hom_def)

lemma iso_iff_mon_epi: "f \ iso G H \ f \ mon G H \ f \ epi G H"
  by (auto simp: iso_def mon_def epi_def bij_betw_def)

lemma iso_set_refl: "(\x. x) \ iso G G"
  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)

lemma id_iso: "id \ iso G G"
  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)

corollary iso_refl [simp]: "G \ G"
  using iso_set_refl unfolding is_iso_def by auto

lemma iso_iff:
   "h \ iso G H \ h \ hom G H \ h ` (carrier G) = carrier H \ inj_on h (carrier G)"
  by (auto simp: iso_def hom_def bij_betw_def)

lemma iso_imp_homomorphism:
   "h \ iso G H \ h \ hom G H"
  by (simp add: iso_iff)

lemma trivial_hom:
   "group H \ (\x. one H) \ hom G H"
  by (auto simp: hom_def Group.group_def)

lemma (in group) hom_eq:
  assumes "f \ hom G H" "\x. x \ carrier G \ f' x = f x"
  shows "f' \ hom G H"
  using assms by (auto simp: hom_def)

lemma (in group) iso_eq:
  assumes "f \ iso G H" "\x. x \ carrier G \ f' x = f x"
  shows "f' \ iso G H"
  using assms  by (fastforce simp: iso_def inj_on_def bij_betw_def hom_eq image_iff)

lemma (in group) iso_set_sym:
  assumes "h \ iso G H"
  shows "inv_into (carrier G) h \ iso H G"
proof -
  have h: "h \ hom G H" "bij_betw h (carrier G) (carrier H)"
    using assms by (auto simp add: iso_def bij_betw_inv_into)
  then have HG: "bij_betw (inv_into (carrier G) h) (carrier H) (carrier G)"
    by (simp add: bij_betw_inv_into)
  have "inv_into (carrier G) h \ hom H G"
    unfolding hom_def
  proof safe
    show *: "\x. x \ carrier H \ inv_into (carrier G) h x \ carrier G"
      by (meson HG bij_betwE)
    show "inv_into (carrier G) h (x \\<^bsub>H\<^esub> y) = inv_into (carrier G) h x \ inv_into (carrier G) h y"
      if "x \ carrier H" "y \ carrier H" for x y
    proof (rule inv_into_f_eq)
      show "inj_on h (carrier G)"
        using bij_betw_def h(2) by blast
      show "inv_into (carrier G) h x \ inv_into (carrier G) h y \ carrier G"
        by (simp add: * that)
      show "h (inv_into (carrier G) h x \ inv_into (carrier G) h y) = x \\<^bsub>H\<^esub> y"
        using h bij_betw_inv_into_right [of h] unfolding hom_def by (simp add: "*" that)
    qed
  qed
  then show ?thesis
    by (simp add: Group.iso_def bij_betw_inv_into h)
qed

corollary (in group) iso_sym: "G \ H \ H \ G"
  using iso_set_sym unfolding is_iso_def by auto

lemma iso_set_trans:
  "\h \ Group.iso G H; i \ Group.iso H I\ \ i \ h \ Group.iso G I"
  by (force simp: iso_def hom_compose intro: bij_betw_trans)

corollary iso_trans [trans]: "\G \ H ; H \ I\ \ G \ I"
  using iso_set_trans unfolding is_iso_def by blast

lemma iso_same_card: "G \ H \ card (carrier G) = card (carrier H)"
  using bij_betw_same_card  unfolding is_iso_def iso_def by auto

lemma iso_finite: "G \ H \ finite(carrier G) \ finite(carrier H)"
  by (auto simp: is_iso_def iso_def bij_betw_finite)

lemma mon_compose:
   "\f \ mon G H; g \ mon H K\ \ (g \ f) \ mon G K"
  by (auto simp: mon_def intro: hom_compose comp_inj_on inj_on_subset [OF _ hom_carrier])

lemma mon_compose_rev:
   "\f \ hom G H; g \ hom H K; (g \ f) \ mon G K\ \ f \ mon G H"
  using inj_on_imageI2 by (auto simp: mon_def)

lemma epi_compose:
   "\f \ epi G H; g \ epi H K\ \ (g \ f) \ epi G K"
  using hom_compose by (force simp: epi_def hom_compose simp flip: image_image)

lemma epi_compose_rev:
   "\f \ hom G H; g \ hom H K; (g \ f) \ epi G K\ \ g \ epi H K"
  by (fastforce simp: epi_def hom_def Pi_iff image_def set_eq_iff)

lemma iso_compose_rev:
   "\f \ hom G H; g \ hom H K; (g \ f) \ iso G K\ \ f \ mon G H \ g \ epi H K"
  unfolding iso_iff_mon_epi using mon_compose_rev epi_compose_rev by blast

lemma epi_iso_compose_rev:
  assumes "f \ epi G H" "g \ hom H K" "(g \ f) \ iso G K"
  shows "f \ iso G H \ g \ iso H K"
proof
  show "f \ iso G H"
    by (metis (no_types, lifting) assms epi_def iso_compose_rev iso_iff_mon_epi mem_Collect_eq)
  then have "f \ hom G H \ bij_betw f (carrier G) (carrier H)"
    using Group.iso_def \<open>f \<in> Group.iso G H\<close> by blast
  then have "bij_betw g (carrier H) (carrier K)"
    using Group.iso_def assms(3) bij_betw_comp_iff by blast
  then show "g \ iso H K"
    using Group.iso_def assms(2) by blast
qed

lemma mon_left_invertible:
   "\f \ hom G H; \x. x \ carrier G \ g(f x) = x\ \ f \ mon G H"
  by (simp add: mon_def inj_on_def) metis

lemma epi_right_invertible:
   "\g \ hom H G; f \ carrier G \ carrier H; \x. x \ carrier G \ g(f x) = x\ \ g \ epi H G"
  by (force simp: Pi_iff epi_iff_subset image_subset_iff_funcset subset_iff)

lemma (in monoid) hom_imp_img_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "h \ hom G H"
  shows "monoid (H \ carrier := h ` (carrier G), one := h \\<^bsub>G\<^esub> \)" (is "monoid ?h_img")
proof (rule monoidI)
  show "\\<^bsub>?h_img\<^esub> \ carrier ?h_img"
    by auto
next
  fix x y z assume "x \ carrier ?h_img" "y \ carrier ?h_img" "z \ carrier ?h_img"
  then obtain g1 g2 g3
    where g1: "g1 \ carrier G" "x = h g1"
      and g2: "g2 \ carrier G" "y = h g2"
      and g3: "g3 \ carrier G" "z = h g3"
    using image_iff[where ?f = h and ?A = "carrier G"] by auto
  have aux_lemma:
    "\a b. \ a \ carrier G; b \ carrier G \ \ h a \\<^bsub>(?h_img)\<^esub> h b = h (a \ b)"
    using assms unfolding hom_def by auto

  show "x \\<^bsub>(?h_img)\<^esub> \\<^bsub>(?h_img)\<^esub> = x"
    using aux_lemma[OF g1(1) one_closed] g1(2) r_one[OF g1(1)] by simp

  show "\\<^bsub>(?h_img)\<^esub> \\<^bsub>(?h_img)\<^esub> x = x"
    using aux_lemma[OF one_closed g1(1)] g1(2) l_one[OF g1(1)] by simp

  have "x \\<^bsub>(?h_img)\<^esub> y = h (g1 \ g2)"
    using aux_lemma g1 g2 by auto
  thus "x \\<^bsub>(?h_img)\<^esub> y \ carrier ?h_img"
    using g1(1) g2(1) by simp

  have "(x \\<^bsub>(?h_img)\<^esub> y) \\<^bsub>(?h_img)\<^esub> z = h ((g1 \ g2) \ g3)"
    using aux_lemma g1 g2 g3 by auto
  also have " ... = h (g1 \ (g2 \ g3))"
    using m_assoc[OF g1(1) g2(1) g3(1)] by simp
  also have " ... = x \\<^bsub>(?h_img)\<^esub> (y \\<^bsub>(?h_img)\<^esub> z)"
    using aux_lemma g1 g2 g3 by auto
  finally show "(x \\<^bsub>(?h_img)\<^esub> y) \\<^bsub>(?h_img)\<^esub> z = x \\<^bsub>(?h_img)\<^esub> (y \\<^bsub>(?h_img)\<^esub> z)" .
qed

lemma (in group) hom_imp_img_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "h \ hom G H"
  shows "group (H \ carrier := h ` (carrier G), one := h \\<^bsub>G\<^esub> \)" (is "group ?h_img")
proof -
  interpret monoid ?h_img
    using hom_imp_img_monoid[OF assms] .

  show ?thesis
  proof (unfold_locales)
    show "carrier ?h_img \ Units ?h_img"
    proof (auto simp add: Units_def)
      have aux_lemma:
        "\g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ h g1 \\<^bsub>H\<^esub> h g2 = h (g1 \ g2)"
        using assms unfolding hom_def by auto

      fix g1 assume g1: "g1 \ carrier G"
      thus "\g2 \ carrier G. (h g2) \\<^bsub>H\<^esub> (h g1) = h \ \ (h g1) \\<^bsub>H\<^esub> (h g2) = h \"
        using aux_lemma[OF g1 inv_closed[OF g1]]
              aux_lemma[OF inv_closed[OF g1] g1]
              inv_closed by auto
    qed
  qed
qed

lemma (in group) iso_imp_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "G \ H" and "monoid H"
  shows "group H"
proof -
  obtain \<phi> where phi: "\<phi> \<in> iso G H" "inv_into (carrier G) \<phi> \<in> iso H G"
    using iso_set_sym assms unfolding is_iso_def by blast
  define \<psi> where psi_def: "\<psi> = inv_into (carrier G) \<phi>"

  have surj: "\ ` (carrier G) = (carrier H)" "\ ` (carrier H) = (carrier G)"
   and inj: "inj_on \ (carrier G)" "inj_on \ (carrier H)"
   and phi_hom: "\g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ \ (g1 \ g2) = (\ g1) \\<^bsub>H\<^esub> (\ g2)"
   and psi_hom: "\h1 h2. \ h1 \ carrier H; h2 \ carrier H \ \ \ (h1 \\<^bsub>H\<^esub> h2) = (\ h1) \ (\ h2)"
   using phi psi_def unfolding iso_def bij_betw_def hom_def by auto

  have phi_one: "\ \ = \\<^bsub>H\<^esub>"
  proof -
    have "(\ \) \\<^bsub>H\<^esub> \\<^bsub>H\<^esub> = (\ \) \\<^bsub>H\<^esub> (\ \)"
      by (metis assms(2) image_eqI monoid.r_one one_closed phi_hom r_one surj(1))
    thus ?thesis
      by (metis (no_types, opaque_lifting) Units_eq Units_one_closed assms(2) f_inv_into_f imageI
          monoid.l_one monoid.one_closed phi_hom psi_def r_one surj)
  qed

  have "carrier H \ Units H"
  proof
    fix h assume h: "h \ carrier H"
    let ?inv_h = "\ (inv (\ h))"
    have "h \\<^bsub>H\<^esub> ?inv_h = \ (\ h) \\<^bsub>H\<^esub> ?inv_h"
      by (simp add: f_inv_into_f h psi_def surj(1))
    also have " ... = \ ((\ h) \ inv (\ h))"
      by (metis h imageI inv_closed phi_hom surj(2))
    also have " ... = \ \"
      by (simp add: h inv_into_into psi_def surj(1))
    finally have 1: "h \\<^bsub>H\<^esub> ?inv_h = \\<^bsub>H\<^esub>"
      using phi_one by simp

    have "?inv_h \\<^bsub>H\<^esub> h = ?inv_h \\<^bsub>H\<^esub> \ (\ h)"
      by (simp add: f_inv_into_f h psi_def surj(1))
    also have " ... = \ (inv (\ h) \ (\ h))"
      by (metis h imageI inv_closed phi_hom surj(2))
    also have " ... = \ \"
      by (simp add: h inv_into_into psi_def surj(1))
    finally have 2: "?inv_h \\<^bsub>H\<^esub> h = \\<^bsub>H\<^esub>"
      using phi_one by simp

    thus "h \ Units H" unfolding Units_def using 1 2 h surj by fastforce
  qed
  thus ?thesis unfolding group_def group_axioms_def using assms(2) by simp
qed

corollary (in group) iso_imp_img_group: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "h \ iso G H"
  shows "group (H \ one := h \ \)"
proof -
  let ?h_img = "H \ carrier := h ` (carrier G), one := h \ \"
  have "h \ iso G ?h_img"
    using assms unfolding iso_def hom_def bij_betw_def by auto
  hence "G \ ?h_img"
    unfolding is_iso_def by auto
  hence "group ?h_img"
    using iso_imp_group[of ?h_img] hom_imp_img_monoid[of h H] assms unfolding iso_def by simp
  moreover have "carrier H = carrier ?h_img"
    using assms unfolding iso_def bij_betw_def by simp
  hence "H \ one := h \ \ = ?h_img"
    by simp
  ultimately show ?thesis by simp
qed

subsubsection \<open>HOL Light's concept of an isomorphism pair\<close>

definition group_isomorphisms
  where
"group_isomorphisms G H f g \
        f \<in> hom G H \<and> g \<in> hom H G \<and>
        (\<forall>x \<in> carrier G. g(f x) = x) \<and>
        (\<forall>y \<in> carrier H. f(g y) = y)"

lemma group_isomorphisms_sym: "group_isomorphisms G H f g \ group_isomorphisms H G g f"
  by (auto simp: group_isomorphisms_def)

lemma group_isomorphisms_imp_iso: "group_isomorphisms G H f g \ f \ iso G H"
by (auto simp: iso_def inj_on_def image_def group_isomorphisms_def hom_def bij_betw_def Pi_iff, metis+)

lemma (in group) iso_iff_group_isomorphisms:
  "f \ iso G H \ (\g. group_isomorphisms G H f g)"
proof safe
  show "\g. group_isomorphisms G H f g" if "f \ Group.iso G H"
    unfolding group_isomorphisms_def
  proof (intro exI conjI)
    let ?g = "inv_into (carrier G) f"
    show "\x\carrier G. ?g (f x) = x"
      by (metis (no_types, lifting) Group.iso_def bij_betw_inv_into_left mem_Collect_eq that)
    show "\y\carrier H. f (?g y) = y"
      by (metis (no_types, lifting) Group.iso_def bij_betw_inv_into_right mem_Collect_eq that)
  qed (use Group.iso_def iso_set_sym that in \<open>blast+\<close>)
next
  fix g
  assume "group_isomorphisms G H f g"
  then show "f \ Group.iso G H"
    by (auto simp: iso_def group_isomorphisms_def hom_in_carrier intro: bij_betw_byWitness)
qed

subsubsection \<open>Involving direct products\<close>

lemma DirProd_commute_iso_set:
  shows "(\(x,y). (y,x)) \ iso (G \\ H) (H \\ G)"
  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)

corollary DirProd_commute_iso :
"(G \\ H) \ (H \\ G)"
  using DirProd_commute_iso_set unfolding is_iso_def by blast

lemma DirProd_assoc_iso_set:
  shows "(\(x,y,z). (x,(y,z))) \ iso (G \\ H \\ I) (G \\ (H \\ I))"
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)

lemma (in group) DirProd_iso_set_trans:
  assumes "g \ iso G G2"
    and "h \ iso H I"
  shows "(\(x,y). (g x, h y)) \ iso (G \\ H) (G2 \\ I)"
proof-
  have "(\(x,y). (g x, h y)) \ hom (G \\ H) (G2 \\ I)"
    using assms unfolding iso_def hom_def by auto
  moreover have " inj_on (\(x,y). (g x, h y)) (carrier (G \\ H))"
    using assms unfolding iso_def DirProd_def bij_betw_def inj_on_def by auto
  moreover have "(\(x, y). (g x, h y)) ` carrier (G \\ H) = carrier (G2 \\ I)"
    using assms unfolding iso_def bij_betw_def image_def DirProd_def by fastforce
  ultimately show "(\(x,y). (g x, h y)) \ iso (G \\ H) (G2 \\ I)"
    unfolding iso_def bij_betw_def by auto
qed

corollary (in group) DirProd_iso_trans :
  assumes "G \ G2" and "H \ I"
  shows "G \\ H \ G2 \\ I"
  using DirProd_iso_set_trans assms unfolding is_iso_def by blast

lemma hom_pairwise: "f \ hom G (DirProd H K) \ (fst \ f) \ hom G H \ (snd \ f) \ hom G K"
  apply (auto simp: hom_def mult_DirProd' dest: Pi_mem)
   apply (metis Product_Type.mem_Times_iff comp_eq_dest_lhs funcset_mem)
  by (metis mult_DirProd prod.collapse)

lemma hom_paired:
   "(\x. (f x,g x)) \ hom G (DirProd H K) \ f \ hom G H \ g \ hom G K"
  by (simp add: hom_pairwise o_def)

lemma hom_paired2:
  assumes "group G" "group H"
  shows "(\(x,y). (f x,g y)) \ hom (DirProd G H) (DirProd G' H') \ f \ hom G G' \ g \ hom H H'"
  using assms
  by (fastforce simp: hom_def Pi_def dest!: group.is_monoid)

lemma iso_paired2:
  assumes "group G" "group H"
  shows "(\(x,y). (f x,g y)) \ iso (DirProd G H) (DirProd G' H') \ f \ iso G G' \ g \ iso H H'"
  using assms
  by (fastforce simp add: iso_def inj_on_def bij_betw_def hom_paired2 image_paired_Times
      times_eq_iff group_def monoid.carrier_not_empty)

lemma hom_of_fst:
  assumes "group H"
  shows "(f \ fst) \ hom (DirProd G H) K \ f \ hom G K"
proof -
  interpret group H
    by (rule assms)
  show ?thesis
    using one_closed by (auto simp: hom_def Pi_def)
qed

lemma hom_of_snd:
  assumes "group G"
  shows "(f \ snd) \ hom (DirProd G H) K \ f \ hom H K"
proof -
  interpret group G
    by (rule assms)
  show ?thesis
    using one_closed by (auto simp: hom_def Pi_def)
qed

subsection\<open>The locale for a homomorphism between two groups\<close>

text\<open>Basis for homomorphism proofs: we assume two groups \<^term>\<open>G\<close> and
  \<^term>\<open>H\<close>, with a homomorphism \<^term>\<open>h\<close> between them\<close>
locale group_hom = G?: group G + H?: group H for G (structure) and H (structure) +
  fixes h
  assumes homh [simp]: "h \ hom G H"

declare group_hom.homh [simp]

lemma (in group_hom) hom_mult [simp]:
  "[| x \ carrier G; y \ carrier G |] ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y"
proof -
  assume "x \ carrier G" "y \ carrier G"
  with homh [unfolded hom_def] show ?thesis by simp
qed

lemma (in group_hom) hom_closed [simp]:
  "x \ carrier G ==> h x \ carrier H"
proof -
  assume "x \ carrier G"
  with homh [unfolded hom_def] show ?thesis by auto
qed

lemma (in group_hom) one_closed: "h \ \ carrier H"
  by simp

lemma (in group_hom) hom_one [simp]: "h \ = \\<^bsub>H\<^esub>"
proof -
  have "h \ \\<^bsub>H\<^esub> \\<^bsub>H\<^esub> = h \ \\<^bsub>H\<^esub> h \"
    by (simp add: hom_mult [symmetric] del: hom_mult)
  then show ?thesis
    by (metis H.Units_eq H.Units_l_cancel H.one_closed local.one_closed)
qed

lemma hom_one:
  assumes "h \ hom G H" "group G" "group H"
  shows "h (one G) = one H"
  apply (rule group_hom.hom_one)
  by (simp add: assms group_hom_axioms_def group_hom_def)

lemma hom_mult:
  "\h \ hom G H; x \ carrier G; y \ carrier G\ \ h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y"
  by (auto simp: hom_def)

lemma (in group_hom) inv_closed [simp]:
  "x \ carrier G ==> h (inv x) \ carrier H"
  by simp

lemma (in group_hom) hom_inv [simp]:
  assumes "x \ carrier G" shows "h (inv x) = inv\<^bsub>H\<^esub> (h x)"
proof -
  have "h x \\<^bsub>H\<^esub> h (inv x) = h x \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)"
    using assms by (simp flip: hom_mult)
  with assms show ?thesis by (simp del: H.r_inv H.Units_r_inv)
qed

lemma (in group) int_pow_is_hom: \<^marker>\<open>contributor \<open>Joachim Breitner\<close>\<close>
  "x \ carrier G \ (([^]) x) \ hom \ carrier = UNIV, mult = (+), one = 0::int \ G "
  unfolding hom_def by (simp add: int_pow_mult)

lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H" \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  apply (rule subgroupI)
  apply (auto simp add: image_subsetI)
  apply (metis G.inv_closed hom_inv image_iff)
  by (metis G.monoid_axioms hom_mult image_eqI monoid.m_closed)

lemma (in group_hom) subgroup_img_is_subgroup: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "subgroup I G"
  shows "subgroup (h ` I) H"
proof -
  have "h \ hom (G \ carrier := I \) H"
    using G.subgroupE[OF assms] subgroup.mem_carrier[OF assms] homh
    unfolding hom_def by auto
  hence "group_hom (G \ carrier := I \) H h"
    using subgroup.subgroup_is_group[OF assms G.is_group] is_group
    unfolding group_hom_def group_hom_axioms_def by simp
  thus ?thesis
    using group_hom.img_is_subgroup[of "G \ carrier := I \" H h] by simp
qed

lemma (in subgroup) iso_subgroup: \<^marker>\<open>contributor \<open>Jakob von Raumer\<close>\<close>
  assumes "group G" "group F"
  assumes "\ \ iso G F"
  shows "subgroup (\ ` H) F"
  by (metis assms Group.iso_iff group_hom.intro group_hom_axioms_def group_hom.subgroup_img_is_subgroup subgroup_axioms)

lemma (in group_hom) induced_group_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "subgroup I G"
  shows "group_hom (G \ carrier := I \) (H \ carrier := h ` I \) h"
proof -
  have "h \ hom (G \ carrier := I \) (H \ carrier := h ` I \)"
    using homh subgroup.mem_carrier[OF assms] unfolding hom_def by auto
  thus ?thesis
    unfolding group_hom_def group_hom_axioms_def
    using subgroup.subgroup_is_group[OF assms G.is_group]
          subgroup.subgroup_is_group[OF subgroup_img_is_subgroup[OF assms] is_group] by simp
qed

text \<open>An isomorphism restricts to an isomorphism of subgroups.\<close>

lemma iso_restrict:
  assumes "\ \ iso G F"
  assumes groups: "group G" "group F"
  assumes HG: "subgroup H G"
  shows "(restrict \ H) \ iso (G\carrier := H\) (F\carrier := \ ` H\)"
proof -
  have "\x y. \x \ H; y \ H; x \\<^bsub>G\<^esub> y \ H\ \ \ (x \\<^bsub>G\<^esub> y) = \ x \\<^bsub>F\<^esub> \ y"
    by (meson assms hom_mult iso_imp_homomorphism subgroup.mem_carrier)
  moreover have "\x y. \x \ H; y \ H; x \\<^bsub>G\<^esub> y \ H\ \ \ x \\<^bsub>F\<^esub> \ y = undefined"
    by (simp add: HG subgroup.m_closed)
  moreover have "\x y. \x \ H; y \ H; \ x = \ y\ \ x = y"
    by (smt (verit, ccfv_SIG) assms group.iso_iff_group_isomorphisms group_isomorphisms_def subgroup.mem_carrier)
  ultimately show ?thesis
    by (auto simp: iso_def hom_def bij_betw_def inj_on_def)
qed

lemma (in group) canonical_inj_is_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  assumes "subgroup H G"
  shows "group_hom (G \ carrier := H \) G id"
  unfolding group_hom_def group_hom_axioms_def hom_def
  using subgroup.subgroup_is_group[OF assms is_group]
        is_group subgroup.subset[OF assms] by auto

lemma (in group_hom) hom_nat_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  "x \ carrier G \ h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
  by (induction n) auto

lemma (in group_hom) hom_int_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
  "x \ carrier G \ h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
  using hom_nat_pow by (simp add: int_pow_def2)

lemma hom_nat_pow:
  "\h \ hom G H; x \ carrier G; group G; group H\ \ h (x [^]\<^bsub>G\<^esub> (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
  by (simp add: group_hom.hom_nat_pow group_hom_axioms_def group_hom_def)

lemma hom_int_pow:
  "\h \ hom G H; x \ carrier G; group G; group H\ \ h (x [^]\<^bsub>G\<^esub> (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
  by (simp add: group_hom.hom_int_pow group_hom_axioms.intro group_hom_def)

subsection \<open>Commutative Structures\<close>

text \<open>
  Naming convention: multiplicative structures that are commutative
  are called \emph{commutative}, additive structures are called
  \emph{Abelian}.
\<close>

locale comm_monoid = monoid +
  assumes m_comm: "\x \ carrier G; y \ carrier G\ \ x \ y = y \ x"

lemma (in comm_monoid) m_lcomm:
  "\x \ carrier G; y \ carrier G; z \ carrier G\ \
   x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
proof -
  assume xyz: "x \ carrier G" "y \ carrier G" "z \ carrier G"
  from xyz have "x \ (y \ z) = (x \ y) \ z" by (simp add: m_assoc)
  also from xyz have "... = (y \ x) \ z" by (simp add: m_comm)
  also from xyz have "... = y \ (x \ z)" by (simp add: m_assoc)
  finally show ?thesis .
qed

lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm

lemma comm_monoidI:
  fixes G (structure)
  assumes m_closed:
      "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"
    and one_closed: "\ \ carrier G"
    and m_assoc:
      "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    and l_one: "!!x. x \ carrier G ==> \ \ x = x"
    and m_comm:
      "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"
  shows "comm_monoid G"
  using l_one
    by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro
             intro: assms simp: m_closed one_closed m_comm)

lemma (in monoid) monoid_comm_monoidI:
  assumes m_comm:
      "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"
  shows "comm_monoid G"
  by (rule comm_monoidI) (auto intro: m_assoc m_comm)

lemma (in comm_monoid) submonoid_is_comm_monoid :
  assumes "submonoid H G"
  shows "comm_monoid (G\carrier := H\)"
proof (intro monoid.monoid_comm_monoidI)
  show "monoid (G\carrier := H\)"
    using submonoid.submonoid_is_monoid assms comm_monoid_axioms comm_monoid_def by blast
  show "\x y. x \ carrier (G\carrier := H\) \ y \ carrier (G\carrier := H\)
        \<Longrightarrow> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y = y \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x"
    by simp (meson assms m_comm submonoid.mem_carrier)
qed

locale comm_group = comm_monoid + group

lemma (in group) group_comm_groupI:
  assumes m_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"
  shows "comm_group G"
  by standard (simp_all add: m_comm)

lemma comm_groupI:
  fixes G (structure)
  assumes m_closed:
      "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y \ carrier G"
    and one_closed: "\ \ carrier G"
    and m_assoc:
      "!!x y z. [| x \ carrier G; y \ carrier G; z \ carrier G |] ==>
      (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
    and m_comm:
      "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x"
    and l_one: "!!x. x \ carrier G ==> \ \ x = x"
    and l_inv_ex: "!!x. x \ carrier G ==> \y \ carrier G. y \ x = \"
  shows "comm_group G"
  by (fast intro: group.group_comm_groupI groupI assms)

lemma comm_groupE:
  fixes G (structure)
  assumes "comm_group G"
  shows "\x y. \ x \ carrier G; y \ carrier G \ \ x \ y \ carrier G"
    and "\ \ carrier G"
    and "\x y z. \ x \ carrier G; y \ carrier G; z \ carrier G \ \ (x \ y) \ z = x \ (y \ z)"
    and "\x y. \ x \ carrier G; y \ carrier G \ \ x \ y = y \ x"
    and "\x. x \ carrier G \ \ \ x = x"
    and "\x. x \ carrier G \ \y \ carrier G. y \ x = \"
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.12 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.