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