Quelle Left_Coset.thy Sprache: Isabelle

theory Left_Coset
imports Coset

(*This instance of Coset.thy but for left cosets is due to Jonas Rädle and has been imported
  from the AFP entry Orbit_Stabiliser. *)

begin

definition
  LCOSETS  :: "[_, 'a set] \ ('a set)set"
    (\<open>(\<open>open_block notation=\<open>prefix lcosets\<close>\<close>lcosets\<index> _)\<close> [81] 80)
  where "lcosets\<^bsub>G\<^esub> H = (\a\carrier G. {a <#\<^bsub>G\<^esub> H})"

definition
  LFactGroup :: "[('a,'b) monoid_scheme, 'a set] \ ('a set) monoid" (infixl \LMod\ 65)
    \<comment> \<open>Actually defined for groups rather than monoids\<close>
   where "LFactGroup G H = \carrier = lcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\"

lemma (in group) lcos_self: "[| x \ carrier G; subgroup H G |] ==> x \ x <# H"
  by (simp add: group_l_invI subgroup.lcos_module_rev subgroup.one_closed)

text \<open>Elements of a left coset are in the carrier\<close>
lemma (in subgroup) elemlcos_carrier:
  assumes "group G" "a \ carrier G" "a' \ a <# H"
  shows "a' \ carrier G"
  by (meson assms group.l_coset_carrier subgroup_axioms)

text \<open>Step one for lemma \<open>rcos_module\<close>\<close>
lemma (in subgroup) lcos_module_imp:
  assumes "group G"
  assumes xcarr: "x \ carrier G"
      and x'cos: "x' \<in> x <# H"
  shows "(inv x \ x') \ H"
proof -
  interpret group G by fact
  obtain h
    where hH: "h \ H" and x': "x' = x \ h" and hcarr: "h \ carrier G"
    using assms by (auto simp: l_coset_def)
  have "(inv x) \ x' = (inv x) \ (x \ h)"
    by (simp add: x')
  have "\ = (x \ inv x) \ h"
    by (metis hcarr inv_closed inv_inv l_inv m_assoc xcarr)
  also have "\ = h"
    by (simp add: hcarr xcarr)
  finally have "(inv x) \ x' = h"
    using x' by metis
  then show "(inv x) \ x' \ H"
    using hH by force
qed

text \<open>Left cosets are subsets of the carrier.\<close>
lemma (in subgroup) lcosets_carrier:
  assumes "group G"
  assumes XH: "X \ lcosets H"
  shows "X \ carrier G"
proof -
  interpret group G by fact
  show "X \ carrier G"
    using XH l_coset_subset_G subset by (auto simp: LCOSETS_def)
qed

lemma (in group) lcosets_part_G:
  assumes "subgroup H G"
  shows "\(lcosets H) = carrier G"
proof -
  interpret subgroup H G by fact
  show ?thesis
  proof
    show "\ (lcosets H) \ carrier G"
      by (force simp add: LCOSETS_def l_coset_def)
    show "carrier G \ \ (lcosets H)"
      by (auto simp add: LCOSETS_def intro: lcos_self assms)
  qed
qed

lemma (in group) lcosets_subset_PowG:
     "subgroup H G \ lcosets H \ Pow(carrier G)"
  using lcosets_part_G subset_Pow_Union by blast

lemma (in group) lcos_disjoint:
  assumes "subgroup H G"
  assumes p: "a \ lcosets H" "b \ lcosets H" "a\b"
  shows "a \ b = {}"
proof -
  interpret subgroup H G by fact
  show ?thesis
    using p l_repr_independence subgroup_axioms unfolding LCOSETS_def disjoint_iff
    by blast
qed

text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
lemma (in group) inj_on_f':
    "\H \ carrier G; a \ carrier G\ \ inj_on (\y. y \ inv a) (a <# H)"
  by (simp add: inj_on_g l_coset_subset_G)

lemma (in group) inj_on_f'':
    "\H \ carrier G; a \ carrier G\ \ inj_on (\y. inv a \ y) (a <# H)"
  by (meson inj_on_cmult inv_closed l_coset_subset_G inj_on_subset)

lemma (in group) inj_on_g':
    "\H \ carrier G; a \ carrier G\ \ inj_on (\y. a \ y) H"
  using inj_on_cmult inj_on_subset by blast

lemma (in group) l_card_cosets_equal:
  assumes "c \ lcosets H" and H: "H \ carrier G" and fin: "finite(carrier G)"
  shows "card H = card c"
proof -
  obtain x where x: "x \ carrier G" and c: "c = x <# H"
    using assms by (auto simp add: LCOSETS_def)
  have "inj_on ((\) x) H"
    by (simp add: H group.inj_on_g' x)
  moreover
  have "(\) x ` H \ x <# H"
    by (force simp add: m_assoc subsetD l_coset_def)
  moreover
  have "inj_on ((\) (inv x)) (x <# H)"
    by (simp add: H group.inj_on_f'' x)
  moreover
  have "\h. h \ H \ inv x \ (x \ h) \ H"
    by (metis H in_mono inv_solve_left m_closed x)
  then have "(\) (inv x) ` (x <# H) \ H"
    by (auto simp: l_coset_def)
  ultimately show ?thesis
    by (metis H fin c card_bij_eq finite_imageD finite_subset)
qed

theorem (in group) l_lagrange:
  assumes "finite(carrier G)" "subgroup H G"
  shows "card(lcosets H) * card(H) = order(G)"
proof -
  have "card H * card (lcosets H) = card (\ (lcosets H))"
    using card_partition
    by (metis (no_types, lifting) assms finite_UnionD l_card_cosets_equal lcos_disjoint lcosets_part_G subgroup.subset)
  then show ?thesis
    by (simp add: assms(2) lcosets_part_G mult.commute order_def)
qed

end

quality100%

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