Theory Group_Extras

text ‹Authors: Anthony Bordg and Lawrence Paulson›

theory Group_Extras
  imports Main
          "Jacobson_Basic_Algebra.Group_Theory"
          "Set_Extras"

begin

section ‹Fold operator with a subdomain›

inductive_set
  foldSetD :: "['a set, 'b ⇒ 'a ⇒ 'a, 'a] ⇒ ('b set * 'a) set"
  for D :: "'a set" and f :: "'b ⇒ 'a ⇒ 'a" and e :: 'a
  where
    emptyI [intro]: "e ∈ D ⟹ ({}, e) ∈ foldSetD D f e"
  | insertI [intro]: "⟦x ∉ A; f x y ∈ D; (A, y) ∈ foldSetD D f e⟧ ⟹
                      (insert x A, f x y) ∈ foldSetD D f e"

inductive_cases empty_foldSetDE [elim!]: "({}, x) ∈ foldSetD D f e"

definition
  foldD :: "['a set, 'b ⇒ 'a ⇒ 'a, 'a, 'b set] ⇒ 'a"
  where "foldD D f e A = (THE x. (A, x) ∈ foldSetD D f e)"

lemma foldSetD_closed: "(A, z) ∈ foldSetD D f e ⟹ z ∈ D"
  by (erule foldSetD.cases) auto

lemma Diff1_foldSetD:
  "⟦(A - {x}, y) ∈ foldSetD D f e; x ∈ A; f x y ∈ D⟧ ⟹
   (A, f x y) ∈ foldSetD D f e"
  by (metis Diff_insert_absorb foldSetD.insertI mk_disjoint_insert)

lemma foldSetD_imp_finite [simp]: "(A, x) ∈ foldSetD D f e ⟹ finite A"
  by (induct set: foldSetD) auto

lemma finite_imp_foldSetD:
  "⟦finite A; e ∈ D; ⋀x y. ⟦x ∈ A; y ∈ D⟧ ⟹ f x y ∈ D⟧
    ⟹ ∃x. (A, x) ∈ foldSetD D f e"
proof (induct set: finite)
  case empty then show ?case by auto
next
  case (insert x F)
  then obtain y where y: "(F, y) ∈ foldSetD D f e" by auto
  with insert have "y ∈ D" by (auto dest: foldSetD_closed)
  with y and insert have "(insert x F, f x y) ∈ foldSetD D f e"
    by (intro foldSetD.intros) auto
  then show ?case ..
qed

lemma foldSetD_backwards:
  assumes "A ≠ {}" "(A, z) ∈ foldSetD D f e"
  shows "∃x y. x ∈ A ∧ (A - { x }, y) ∈ foldSetD D f e ∧ z = f x y"
  using assms(2) by (cases) (simp add: assms(1), metis Diff_insert_absorb insertI1)

subsection ‹Left-Commutative Operations›

locale LCD =
  fixes B :: "'b set"
  and D :: "'a set"
  and f :: "'b ⇒ 'a ⇒ 'a"    (infixl ‹⋅› 70)
  assumes left_commute:
    "⟦x ∈ B; y ∈ B; z ∈ D⟧ ⟹ x ⋅ (y ⋅ z) = y ⋅ (x ⋅ z)"
  and f_closed [simp, intro!]: "!!x y. ⟦x ∈ B; y ∈ D⟧ ⟹ f x y ∈ D"

lemma (in LCD) foldSetD_closed [dest]: "(A, z) ∈ foldSetD D f e ⟹ z ∈ D"
  by (erule foldSetD.cases) auto

lemma (in LCD) Diff1_foldSetD:
  "⟦(A - {x}, y) ∈ foldSetD D f e; x ∈ A; A ⊆ B⟧ ⟹
  (A, f x y) ∈ foldSetD D f e"
  by (meson Diff1_foldSetD f_closed local.foldSetD_closed subsetCE)

lemma (in LCD) finite_imp_foldSetD:
  "⟦finite A; A ⊆ B; e ∈ D⟧ ⟹ ∃x. (A, x) ∈ foldSetD D f e"
proof (induct set: finite)
  case empty then show ?case by auto
next
  case (insert x F)
  then obtain y where y: "(F, y) ∈ foldSetD D f e" by auto
  with insert have "y ∈ D" by auto
  with y and insert have "(insert x F, f x y) ∈ foldSetD D f e"
    by (intro foldSetD.intros) auto
  then show ?case ..
qed


lemma (in LCD) foldSetD_determ_aux:
  assumes "e ∈ D" and A: "card A < n" "A ⊆ B" "(A, x) ∈ foldSetD D f e" "(A, y) ∈ foldSetD D f e"
  shows "y = x"
  using A
proof (induction n arbitrary: A x y)
  case 0
  then show ?case
    by auto
next
  case (Suc n)
  then consider "card A = n" | "card A < n"
    by linarith
  then show ?case
  proof cases
    case 1
    show ?thesis
      using foldSetD.cases [OF ‹(A,x) ∈ foldSetD D (⋅) e›]
    proof cases
      case 1
      then show ?thesis
        using ‹(A,y) ∈ foldSetD D (⋅) e› by auto
    next
      case (2 x' A' y')
      note A' = this
      show ?thesis
        using foldSetD.cases [OF ‹(A,y) ∈ foldSetD D (⋅) e›]
      proof cases
        case 1
        then show ?thesis
          using ‹(A,x) ∈ foldSetD D (⋅) e› by auto
      next
        case (2 x'' A'' y'')
        note A'' = this
        show ?thesis
        proof (cases "x' = x''")
          case True
          show ?thesis
          proof (cases "y' = y''")
            case True
            then show ?thesis
              using A' A'' ‹x' = x''› by (blast elim!: equalityE)
          next
            case False
            then show ?thesis
              using A' A'' ‹x' = x''›
              by (metis ‹card A = n› Suc.IH Suc.prems(2) card_insert_disjoint foldSetD_imp_finite insert_eq_iff insert_subset lessI)
          qed
        next
          case False
          then have *: "A' - {x''} = A'' - {x'}" "x'' ∈ A'" "x' ∈ A''"
            using A' A'' by fastforce+
          then have "A' = insert x'' A'' - {x'}"
            using ‹x' ∉ A'› by blast
          then have card: "card A' ≤ card A''"
            using A' A'' * by (metis card_Suc_Diff1 eq_refl foldSetD_imp_finite)
          obtain u where u: "(A' - {x''}, u) ∈ foldSetD D (⋅) e"
            using finite_imp_foldSetD [of "A' - {x''}"] A' Diff_insert ‹A ⊆ B› ‹e ∈ D› by fastforce
          have "y' = f x'' u"
            using Diff1_foldSetD [OF u] ‹x'' ∈ A'› ‹card A = n› A' Suc.IH ‹A ⊆ B› by auto
          then have "(A'' - {x'}, u) ∈ foldSetD D f e"
            using "*"(1) u by auto
          then have "y'' = f x' u"
            using A'' by (metis * ‹card A = n› A'(1) Diff1_foldSetD Suc.IH ‹A ⊆ B›
                card card_Suc_Diff1 card_insert_disjoint foldSetD_imp_finite insert_subset le_imp_less_Suc)
          then show ?thesis
            using A' A''
            by (metis ‹A ⊆ B› ‹y' = x'' ⋅ u› insert_subset left_commute local.foldSetD_closed u)
        qed
      qed
    qed
  next
    case 2 with Suc show ?thesis by blast
  qed
qed

lemma (in LCD) foldSetD_determ:
  "⟦(A, x) ∈ foldSetD D f e; (A, y) ∈ foldSetD D f e; e ∈ D; A ⊆ B⟧
  ⟹ y = x"
  by (blast intro: foldSetD_determ_aux [rule_format])

lemma (in LCD) foldD_equality:
  "⟦(A, y) ∈ foldSetD D f e; e ∈ D; A ⊆ B⟧ ⟹ foldD D f e A = y"
  by (unfold foldD_def) (blast intro: foldSetD_determ)

lemma foldD_empty [simp]:
  "e ∈ D ⟹ foldD D f e {} = e"
  by (unfold foldD_def) blast

lemma (in LCD) foldD_insert_aux:
  "⟦x ∉ A; x ∈ B; e ∈ D; A ⊆ B⟧
    ⟹ ((insert x A, v) ∈ foldSetD D f e) ⟷ (∃y. (A, y) ∈ foldSetD D f e ∧ v = f x y)"
  apply auto
  by (metis Diff_insert_absorb f_closed finite_Diff foldSetD.insertI foldSetD_determ foldSetD_imp_finite insert_subset local.finite_imp_foldSetD local.foldSetD_closed)

lemma (in LCD) foldD_insert:
  assumes "finite A" "x ∉ A" "x ∈ B" "e ∈ D" "A ⊆ B"
  shows "foldD D f e (insert x A) = f x (foldD D f e A)"
proof -
  have "(THE v. ∃y. (A, y) ∈ foldSetD D (⋅) e ∧ v = x ⋅ y) = x ⋅ (THE y. (A, y) ∈ foldSetD D (⋅) e)"
    by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in ‹metis+›)
  then show ?thesis
    unfolding foldD_def using assms by (simp add: foldD_insert_aux)
qed

lemma (in LCD) foldD_closed [simp]:
  "⟦finite A; e ∈ D; A ⊆ B⟧ ⟹ foldD D f e A ∈ D"
proof (induct set: finite)
  case empty then show ?case by simp
next
  case insert then show ?case by (simp add: foldD_insert)
qed

lemma (in LCD) foldD_commute:
  "⟦finite A; x ∈ B; e ∈ D; A ⊆ B⟧ ⟹
   f x (foldD D f e A) = foldD D f (f x e) A"
  by (induct set: finite) (auto simp add: left_commute foldD_insert)

lemma Int_mono2:
  "⟦A ⊆ C; B ⊆ C⟧ ⟹ A Int B ⊆ C"
  by blast

lemma (in LCD) foldD_nest_Un_Int:
  "⟦finite A; finite C; e ∈ D; A ⊆ B; C ⊆ B⟧ ⟹
   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
proof (induction set: finite)
  case (insert x F)
  then show ?case
    by (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb Int_mono2)
qed simp

lemma (in LCD) foldD_nest_Un_disjoint:
  "⟦finite A; finite B; A Int B = {}; e ∈ D; A ⊆ B; C ⊆ B⟧
    ⟹ foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
  by (simp add: foldD_nest_Un_Int)

― ‹Delete rules to do with ‹foldSetD› relation.›

declare foldSetD_imp_finite [simp del]
  empty_foldSetDE [rule del]
  foldSetD.intros [rule del]
declare (in LCD)
  foldSetD_closed [rule del]

section ‹Monoids›

lemma comp_monoid_morphisms:
  assumes "monoid_homomorphism η A multA oneA B multB oneB" and
          "monoid_homomorphism θ B multB oneB C multC oneC"
shows "monoid_homomorphism (θ ∘ η ↓ A) A multA oneA C multC oneC"
proof-
  have "map (θ ∘ η ↓ A) A C" using assms comp_maps by (metis monoid_homomorphism.axioms(1))
  moreover have "(θ ∘ η ↓ A) oneA = oneC"
    using assms
    by (metis compose_eq monoid.unit_closed monoid_homomorphism.axioms(2) monoid_homomorphism.commutes_with_unit)
  moreover have "(θ ∘ η ↓ A) (multA x y) = multC ((θ ∘ η ↓ A) x) ((θ ∘ η ↓ A) y)"
      if "x ∈ A" "y ∈ A" for x y
    using that assms monoid_homomorphism.commutes_with_composition
    by (smt compose_eq map.map_closed monoid.composition_closed monoid_homomorphism.axioms)
  ultimately show ?thesis
    using monoid_homomorphism_def assms comp_maps by (smt monoid_homomorphism_axioms.intro)
qed

text ‹Commutative Monoids›

text ‹
  We enter a more restrictive context, with ‹f :: 'a ⇒ 'a ⇒ 'a›
  instead of ‹'b ⇒ 'a ⇒ 'a›.
›

locale ACeD =
  fixes D :: "'a set"
    and f :: "'a ⇒ 'a ⇒ 'a"    (infixl ‹⋅› 70)
    and e :: 'a
  assumes ident [simp]: "x ∈ D ⟹ x ⋅ e = x"
    and commute: "⟦x ∈ D; y ∈ D⟧ ⟹ x ⋅ y = y ⋅ x"
    and assoc: "⟦x ∈ D; y ∈ D; z ∈ D⟧ ⟹ (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
    and e_closed [simp]: "e ∈ D"
    and f_closed [simp]: "⟦x ∈ D; y ∈ D⟧ ⟹ x ⋅ y ∈ D"

lemma (in ACeD) left_commute:
  "⟦x ∈ D; y ∈ D; z ∈ D⟧ ⟹ x ⋅ (y ⋅ z) = y ⋅ (x ⋅ z)"
proof -
  assume D: "x ∈ D" "y ∈ D" "z ∈ D"
  then have "x ⋅ (y ⋅ z) = (y ⋅ z) ⋅ x" by (simp add: commute)
  also from D have "... = y ⋅ (z ⋅ x)" by (simp add: assoc)
  also from D have "z ⋅ x = x ⋅ z" by (simp add: commute)
  finally show ?thesis .
qed

lemmas (in ACeD) AC = assoc commute left_commute

lemma (in ACeD) left_ident [simp]: "x ∈ D ⟹ e ⋅ x = x"
proof -
  assume "x ∈ D"
  then have "x ⋅ e = x" by (rule ident)
  with ‹x ∈ D› show ?thesis by (simp add: commute)
qed

lemma (in ACeD) foldD_Un_Int:
  "⟦finite A; finite B; A ⊆ D; B ⊆ D⟧ ⟹
    foldD D f e A ⋅ foldD D f e B =
    foldD D f e (A Un B) ⋅ foldD D f e (A Int B)"
proof (induction set: finite)
  case empty
  then show ?case
    by(simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
next
  case (insert x F)
  then show ?case
    by(simp add: AC insert_absorb Int_insert_left Int_mono2
                 LCD.foldD_insert [OF LCD.intro [of D]]
                 LCD.foldD_closed [OF LCD.intro [of D]])
qed

lemma (in ACeD) foldD_Un_disjoint:
  "⟦finite A; finite B; A Int B = {}; A ⊆ D; B ⊆ D⟧ ⟹
    foldD D f e (A Un B) = foldD D f e A ⋅ foldD D f e B"
  by (simp add: foldD_Un_Int
    left_commute LCD.foldD_closed [OF LCD.intro [of D]])


subsection ‹Finite Products›

context monoid
begin

definition finprod:: "'b set => ('b => 'a) ⇒ 'a"
  where "finprod I f ≡ if finite I then foldD M (composition ∘ f) 𝟭 I else 𝟭"

end (* monoid *)


section ‹Groups›

lemma comp_group_morphisms:
  assumes "group_homomorphism η A multA oneA B multB oneB" and
"group_homomorphism θ B multB oneB C multC oneC"
shows "group_homomorphism (θ ∘ η ↓ A) A multA oneA C multC oneC"
  using assms group_homomorphism_def comp_monoid_morphisms by metis

subsection ‹Subgroup Generated by a Subset›

context group
begin

inductive_set generate :: "'a set ⇒ 'a set"
  for H where
    unit:  "𝟭 ∈ generate H"
  | incl: "a ∈ H ⟹ a ∈ generate H"
  | inv:  "a ∈ H ⟹ inverse a ∈ generate H"
  | mult:  "a ∈ generate H ⟹ b ∈ generate H ⟹ a ⋅ b ∈ generate H"

lemma generate_into_G: "a ∈ generate (G ∩ H) ⟹ a ∈ G"
  by (induction rule: generate.induct) auto


definition subgroup_generated :: "'a set ⇒ 'a set"
  where "subgroup_generated S = generate (G ∩ S)"

lemma inverse_in_subgroup_generated: "a ∈ subgroup_generated H ⟹ inverse a ∈ subgroup_generated H"
  unfolding subgroup_generated_def
proof (induction rule: generate.induct)
  case (mult a b)
  then show ?case
    by (simp add: generate.mult generate_into_G inverse_composition_commute)
qed (auto simp add: generate.unit generate.incl generate.inv)

lemma subgroup_generated_is_monoid:
  fixes H
  shows "Group_Theory.monoid (subgroup_generated H) (⋅) 𝟭"
  unfolding subgroup_generated_def
proof qed (auto simp: generate.unit generate.mult associative generate_into_G)

lemma subgroup_generated_is_subset:
  fixes H
  shows "subgroup_generated H ⊆ G"
    using generate_into_G subgroup_generated_def by blast

lemma subgroup_generated_is_subgroup:
  fixes H
  shows "subgroup (subgroup_generated H) G (⋅) 𝟭"
proof
  show "subgroup_generated H ⊆ G"
    by (simp add: subgroup_generated_is_subset)
  show "a ⋅ b ∈ subgroup_generated H"
    if "a ∈ subgroup_generated H" "b ∈ subgroup_generated H" for a b
    using that by (meson monoid.composition_closed subgroup_generated_is_monoid)
  show "a ⋅ b ⋅ c = a ⋅ (b ⋅ c)"
    if "a ∈ subgroup_generated H" "b ∈ subgroup_generated H" "c ∈ subgroup_generated H"
    for a b c
    using that by (meson monoid.associative subgroup_generated_is_monoid)
  show "monoid.invertible (subgroup_generated H) (⋅) 𝟭 u"
    if "u ∈ subgroup_generated H" for u
  proof (rule monoid.invertibleI )
    show "Group_Theory.monoid (subgroup_generated H) (⋅) 𝟭"
      by (simp add: subgroup_generated_is_monoid)
    show "u ⋅ local.inverse u = 𝟭" "local.inverse u ⋅ u = 𝟭" "u ∈ subgroup_generated H"
      using ‹subgroup_generated H ⊆ G› that by auto
    show "local.inverse u ∈ subgroup_generated H"
      using inverse_in_subgroup_generated that by blast
  qed
qed (auto simp: generate_into_G generate.unit subgroup_generated_def)


end (* group *)


section ‹Abelian Groups›

context abelian_group
begin

definition minus:: "'a ⇒ 'a ⇒ 'a" (infixl ‹‐› 70)
  where "x ‐ y ≡ x ⋅ inverse y "

definition finsum:: "'b set ⇒ ('b ⇒ 'a) ⇒ 'a"
  where "finsum I f ≡ finprod I f"

(* A notation "∑i∈I. f i" should be introduced for a sum of a family of elements of an abelian group *)

end (* abelian_group*)

end