# HG changeset patch # User paulson # Date 1528816152 -3600 # Node ID ff61cbfb3f2d185b0de85a5629d222f9ab547085 # Parent 46beee72fb66065283acc9efcf06c4ecffd59a30# Parent 43055b016688ab7f60bc50611bd19d4248172b82 merged diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Tue Jun 12 16:21:52 2018 +0200 +++ b/src/HOL/Algebra/AbelCoset.thy Tue Jun 12 16:09:12 2018 +0100 @@ -17,45 +17,42 @@ definition a_r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "+>\" 60) - where "a_r_coset G = r_coset \carrier = carrier G, mult = add G, one = zero G\" + where "a_r_coset G = r_coset (add_monoid G)" definition a_l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "<+\" 60) - where "a_l_coset G = l_coset \carrier = carrier G, mult = add G, one = zero G\" + where "a_l_coset G = l_coset (add_monoid G)" definition A_RCOSETS :: "[_, 'a set] \ ('a set)set" ("a'_rcosets\ _" [81] 80) - where "A_RCOSETS G H = RCOSETS \carrier = carrier G, mult = add G, one = zero G\ H" + where "A_RCOSETS G H = RCOSETS (add_monoid G) H" definition set_add :: "[_, 'a set ,'a set] \ 'a set" (infixl "<+>\" 60) - where "set_add G = set_mult \carrier = carrier G, mult = add G, one = zero G\" + where "set_add G = set_mult (add_monoid G)" definition A_SET_INV :: "[_,'a set] \ 'a set" ("a'_set'_inv\ _" [81] 80) - where "A_SET_INV G H = SET_INV \carrier = carrier G, mult = add G, one = zero G\ H" + where "A_SET_INV G H = SET_INV (add_monoid G) H" definition a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \ ('a*'a)set" ("racong\") - where "a_r_congruent G = r_congruent \carrier = carrier G, mult = add G, one = zero G\" + where "a_r_congruent G = r_congruent (add_monoid G)" definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \ ('a set) monoid" (infixl "A'_Mod" 65) \ \Actually defined for groups rather than monoids\ - where "A_FactGroup G H = FactGroup \carrier = carrier G, mult = add G, one = zero G\ H" + where "A_FactGroup G H = FactGroup (add_monoid G) H" definition a_kernel :: "('a, 'm) ring_scheme \ ('b, 'n) ring_scheme \ ('a \ 'b) \ 'a set" \ \the kernel of a homomorphism (additive)\ - where "a_kernel G H h = - kernel \carrier = carrier G, mult = add G, one = zero G\ - \carrier = carrier H, mult = add H, one = zero H\ h" + where "a_kernel G H h = kernel (add_monoid G) (add_monoid H) h" locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H for G (structure) and H (structure) + fixes h - assumes a_group_hom: "group_hom \carrier = carrier G, mult = add G, one = zero G\ - \carrier = carrier H, mult = add H, one = zero H\ h" + assumes a_group_hom: "group_hom (add_monoid G) (add_monoid H) h" lemmas a_r_coset_defs = a_r_coset_def r_coset_def @@ -63,8 +60,7 @@ lemma a_r_coset_def': fixes G (structure) shows "H +> a \ \h\H. {h \ a}" -unfolding a_r_coset_defs -by simp + unfolding a_r_coset_defs by simp lemmas a_l_coset_defs = a_l_coset_def l_coset_def @@ -72,8 +68,7 @@ lemma a_l_coset_def': fixes G (structure) shows "a <+ H \ \h\H. {a \ h}" -unfolding a_l_coset_defs -by simp + unfolding a_l_coset_defs by simp lemmas A_RCOSETS_defs = A_RCOSETS_def RCOSETS_def @@ -81,8 +76,7 @@ lemma A_RCOSETS_def': fixes G (structure) shows "a_rcosets H \ \a\carrier G. {H +> a}" -unfolding A_RCOSETS_defs -by (fold a_r_coset_def, simp) + unfolding A_RCOSETS_defs by (fold a_r_coset_def, simp) lemmas set_add_defs = set_add_def set_mult_def @@ -90,8 +84,7 @@ lemma set_add_def': fixes G (structure) shows "H <+> K \ \h\H. \k\K. {h \ k}" -unfolding set_add_defs -by simp + unfolding set_add_defs by simp lemmas A_SET_INV_defs = A_SET_INV_def SET_INV_def @@ -99,18 +92,53 @@ lemma A_SET_INV_def': fixes G (structure) shows "a_set_inv H \ \h\H. {\ h}" -unfolding A_SET_INV_defs -by (fold a_inv_def) + unfolding A_SET_INV_defs by (fold a_inv_def) subsubsection \Cosets\ +sublocale abelian_group < + add: group "(add_monoid G)" + rewrites "carrier (add_monoid G) = carrier G" + and " mult (add_monoid G) = add G" + and " one (add_monoid G) = zero G" + and " m_inv (add_monoid G) = a_inv G" + and "finprod (add_monoid G) = finsum G" + and "r_coset (add_monoid G) = a_r_coset G" + and "l_coset (add_monoid G) = a_l_coset G" + and "(\a k. pow (add_monoid G) a k) = (\a k. add_pow G k a)" + by (rule a_group) + (auto simp: m_inv_def a_inv_def finsum_def a_r_coset_def a_l_coset_def add_pow_def) + +context abelian_group +begin + +thm add.coset_mult_assoc +lemmas a_repr_independence' = add.repr_independence + +(* +lemmas a_coset_add_assoc = add.coset_mult_assoc +lemmas a_coset_add_zero [simp] = add.coset_mult_one +lemmas a_coset_add_inv1 = add.coset_mult_inv1 +lemmas a_coset_add_inv2 = add.coset_mult_inv2 +lemmas a_coset_join1 = add.coset_join1 +lemmas a_coset_join2 = add.coset_join2 +lemmas a_solve_equation = add.solve_equation +lemmas a_repr_independence = add.repr_independence +lemmas a_rcosI = add.rcosI +lemmas a_rcosetsI = add.rcosetsI +*) + +end + lemma (in abelian_group) a_coset_add_assoc: "[| M \ carrier G; g \ carrier G; h \ carrier G |] ==> (M +> g) +> h = M +> (g \ h)" by (rule group.coset_mult_assoc [OF a_group, folded a_r_coset_def, simplified monoid_record_simps]) +thm abelian_group.a_coset_add_assoc + lemma (in abelian_group) a_coset_add_zero [simp]: "M \ carrier G ==> M +> \ = M" by (rule group.coset_mult_one [OF a_group, @@ -129,22 +157,22 @@ folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) lemma (in abelian_group) a_coset_join1: - "[| H +> x = H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> x \ H" + "[| H +> x = H; x \ carrier G; subgroup H (add_monoid G) |] ==> x \ H" by (rule group.coset_join1 [OF a_group, folded a_r_coset_def, simplified monoid_record_simps]) lemma (in abelian_group) a_solve_equation: - "\subgroup H \carrier = carrier G, mult = add G, one = zero G\; x \ H; y \ H\ \ \h\H. y = h \ x" + "\subgroup H (add_monoid G); x \ H; y \ H\ \ \h\H. y = h \ x" by (rule group.solve_equation [OF a_group, folded a_r_coset_def, simplified monoid_record_simps]) lemma (in abelian_group) a_repr_independence: - "\y \ H +> x; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ \ \ H +> x = H +> y" -by (rule group.repr_independence [OF a_group, - folded a_r_coset_def, simplified monoid_record_simps]) + "\ y \ H +> x; x \ carrier G; subgroup H (add_monoid G) \ \ + H +> x = H +> y" + using a_repr_independence' by (simp add: a_r_coset_def) lemma (in abelian_group) a_coset_join2: - "\x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\; x\H\ \ H +> x = H" + "\x \ carrier G; subgroup H (add_monoid G); x\H\ \ H +> x = H" by (rule group.coset_join2 [OF a_group, folded a_r_coset_def, simplified monoid_record_simps]) @@ -167,23 +195,15 @@ lemma (in abelian_group) a_transpose_inv: "[| x \ y = z; x \ carrier G; y \ carrier G; z \ carrier G |] ==> (\ x) \ z = y" -by (rule group.transpose_inv [OF a_group, - folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) + using r_neg1 by blast -(* ---"duplicate" -lemma (in abelian_group) a_rcos_self: - "[| x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> x \ H +> x" -by (rule group.rcos_self [OF a_group, - folded a_r_coset_def, simplified monoid_record_simps]) -*) subsubsection \Subgroups\ locale additive_subgroup = fixes H and G (structure) - assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + assumes a_subgroup: "subgroup H (add_monoid G)" lemma (in additive_subgroup) is_additive_subgroup: shows "additive_subgroup H G" @@ -191,7 +211,7 @@ lemma additive_subgroupI: fixes G (structure) - assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + assumes a_subgroup: "subgroup H (add_monoid G)" shows "additive_subgroup H G" by (rule additive_subgroup.intro) (rule a_subgroup) @@ -221,18 +241,18 @@ text \Every subgroup of an \abelian_group\ is normal\ locale abelian_subgroup = additive_subgroup + abelian_group G + - assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\" + assumes a_normal: "normal H (add_monoid G)" lemma (in abelian_subgroup) is_abelian_subgroup: shows "abelian_subgroup H G" by (rule abelian_subgroup_axioms) lemma abelian_subgroupI: - assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\" + assumes a_normal: "normal H (add_monoid G)" and a_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \\<^bsub>G\<^esub> y = y \\<^bsub>G\<^esub> x" shows "abelian_subgroup H G" proof - - interpret normal "H" "\carrier = carrier G, mult = add G, one = zero G\" + interpret normal "H" "(add_monoid G)" by (rule a_normal) show "abelian_subgroup H G" @@ -241,13 +261,13 @@ lemma abelian_subgroupI2: fixes G (structure) - assumes a_comm_group: "comm_group \carrier = carrier G, mult = add G, one = zero G\" - and a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + assumes a_comm_group: "comm_group (add_monoid G)" + and a_subgroup: "subgroup H (add_monoid G)" shows "abelian_subgroup H G" proof - - interpret comm_group "\carrier = carrier G, mult = add G, one = zero G\" + interpret comm_group "(add_monoid G)" by (rule a_comm_group) - interpret subgroup "H" "\carrier = carrier G, mult = add G, one = zero G\" + interpret subgroup "H" "(add_monoid G)" by (rule a_subgroup) show "abelian_subgroup H G" @@ -264,13 +284,10 @@ lemma abelian_subgroupI3: fixes G (structure) - assumes asg: "additive_subgroup H G" - and ag: "abelian_group G" + assumes "additive_subgroup H G" + and "abelian_group G" shows "abelian_subgroup H G" -apply (rule abelian_subgroupI2) - apply (rule abelian_group.a_comm_group[OF ag]) -apply (rule additive_subgroup.a_subgroup[OF asg]) -done + using assms abelian_subgroupI2 abelian_group.a_comm_group additive_subgroup_def by blast lemma (in abelian_subgroup) a_coset_eq: "(\x \ carrier G. H +> x = x <+ H)" @@ -289,15 +306,14 @@ text\Alternative characterization of normal subgroups\ lemma (in abelian_group) a_normal_inv_iff: - "(N \ \carrier = carrier G, mult = add G, one = zero G\) = - (subgroup N \carrier = carrier G, mult = add G, one = zero G\ \ (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))" + "(N \ (add_monoid G)) = + (subgroup N (add_monoid G) & (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))" (is "_ = ?rhs") by (rule group.normal_inv_iff [OF a_group, folded a_inv_def, simplified monoid_record_simps]) lemma (in abelian_group) a_lcos_m_assoc: - "[| M \ carrier G; g \ carrier G; h \ carrier G |] - ==> g <+ (h <+ M) = (g \ h) <+ M" + "\ M \ carrier G; g \ carrier G; h \ carrier G \ \ g <+ (h <+ M) = (g \ h) <+ M" by (rule group.lcos_m_assoc [OF a_group, folded a_l_coset_def, simplified monoid_record_simps]) @@ -308,33 +324,28 @@ lemma (in abelian_group) a_l_coset_subset_G: - "[| H \ carrier G; x \ carrier G |] ==> x <+ H \ carrier G" + "\ H \ carrier G; x \ carrier G \ \ x <+ H \ carrier G" by (rule group.l_coset_subset_G [OF a_group, folded a_l_coset_def, simplified monoid_record_simps]) lemma (in abelian_group) a_l_coset_swap: - "\y \ x <+ H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\\ \ x \ y <+ H" + "\y \ x <+ H; x \ carrier G; subgroup H (add_monoid G)\ \ x \ y <+ H" by (rule group.l_coset_swap [OF a_group, folded a_l_coset_def, simplified monoid_record_simps]) lemma (in abelian_group) a_l_coset_carrier: - "[| y \ x <+ H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> y \ carrier G" + "[| y \ x <+ H; x \ carrier G; subgroup H (add_monoid G) |] ==> y \ carrier G" by (rule group.l_coset_carrier [OF a_group, folded a_l_coset_def, simplified monoid_record_simps]) lemma (in abelian_group) a_l_repr_imp_subset: - assumes y: "y \ x <+ H" and x: "x \ carrier G" and sb: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + assumes "y \ x <+ H" "x \ carrier G" "subgroup H (add_monoid G)" shows "y <+ H \ x <+ H" -apply (rule group.l_repr_imp_subset [OF a_group, - folded a_l_coset_def, simplified monoid_record_simps]) -apply (rule y) -apply (rule x) -apply (rule sb) -done + by (metis (full_types) a_l_coset_defs(1) add.l_repr_independence assms set_eq_subset) lemma (in abelian_group) a_l_repr_independence: - assumes y: "y \ x <+ H" and x: "x \ carrier G" and sb: "subgroup H \carrier = carrier G, mult = add G, one = zero G\" + assumes y: "y \ x <+ H" and x: "x \ carrier G" and sb: "subgroup H (add_monoid G)" shows "x <+ H = y <+ H" apply (rule group.l_repr_independence [OF a_group, folded a_l_coset_def, simplified monoid_record_simps]) @@ -348,7 +359,7 @@ by (rule group.setmult_subset_G [OF a_group, folded set_add_def, simplified monoid_record_simps]) -lemma (in abelian_group) subgroup_add_id: "subgroup H \carrier = carrier G, mult = add G, one = zero G\ \ H <+> H = H" +lemma (in abelian_group) subgroup_add_id: "subgroup H (add_monoid G) \ H <+> H = H" by (rule group.subgroup_mult_id [OF a_group, folded set_add_def, simplified monoid_record_simps]) @@ -427,8 +438,7 @@ lemma (in abelian_group) a_card_cosets_equal: "\c \ a_rcosets H; H \ carrier G; finite(carrier G)\ \ card c = card H" -by (rule group.card_cosets_equal [OF a_group, - folded A_RCOSETS_def, simplified monoid_record_simps]) + by (simp add: A_RCOSETS_defs(1) add.card_rcosets_equal) lemma (in abelian_group) rcosets_subset_PowG: "additive_subgroup H G \ a_rcosets H \ Pow(carrier G)" @@ -509,7 +519,7 @@ text\The coset map is a homomorphism from @{term G} to the quotient group @{term "G Mod H"}\ lemma (in abelian_subgroup) a_r_coset_hom_A_Mod: - "(\a. H +> a) \ hom \carrier = carrier G, mult = add G, one = zero G\ (G A_Mod H)" + "(\a. H +> a) \ hom (add_monoid G) (G A_Mod H)" by (rule normal.r_coset_hom_Mod [OF a_normal, folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps]) @@ -535,8 +545,8 @@ lemma abelian_group_homI: assumes "abelian_group G" assumes "abelian_group H" - assumes a_group_hom: "group_hom \carrier = carrier G, mult = add G, one = zero G\ - \carrier = carrier H, mult = add H, one = zero H\ h" + assumes a_group_hom: "group_hom (add_monoid G) + (add_monoid H) h" shows "abelian_group_hom G H h" proof - interpret G: abelian_group G by fact @@ -614,7 +624,7 @@ lemma (in abelian_group_hom) A_FactGroup_hom: "(\X. the_elem (h`X)) \ hom (G A_Mod (a_kernel G H h)) - \carrier = carrier H, mult = add H, one = zero H\" + (add_monoid H)" by (rule group_hom.FactGroup_hom[OF a_group_hom, folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) @@ -633,13 +643,16 @@ text\If @{term h} is a homomorphism from @{term G} onto @{term H}, then the quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\ -theorem (in abelian_group_hom) A_FactGroup_iso: +theorem (in abelian_group_hom) A_FactGroup_iso_set: "h ` carrier G = carrier H - \ (\X. the_elem (h`X)) \ (G A_Mod (a_kernel G H h)) \ - \carrier = carrier H, mult = add H, one = zero H\" -by (rule group_hom.FactGroup_iso[OF a_group_hom, + \ (\X. the_elem (h`X)) \ iso (G A_Mod (a_kernel G H h)) (add_monoid H)" +by (rule group_hom.FactGroup_iso_set[OF a_group_hom, folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) +corollary (in abelian_group_hom) A_FactGroup_iso : + "h ` carrier G = carrier H + \ (G A_Mod (a_kernel G H h)) \ (add_monoid H)" + using A_FactGroup_iso_set unfolding is_iso_def by auto subsubsection \Cosets\ diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Tue Jun 12 16:21:52 2018 +0200 +++ b/src/HOL/Algebra/Congruence.thy Tue Jun 12 16:09:12 2018 +0100 @@ -43,6 +43,10 @@ where "class_of\<^bsub>S\<^esub> x = {y \ carrier S. x .=\<^bsub>S\<^esub> y}" definition + eq_classes :: "_ \ ('a set) set" ("classes\") + where "classes\<^bsub>S\<^esub> = {class_of\<^bsub>S\<^esub> x | x. x \ carrier S}" + +definition eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\") where "closure_of\<^bsub>S\<^esub> A = {y \ carrier S. y .\\<^bsub>S\<^esub> A}" @@ -69,235 +73,148 @@ and trans [trans]: "\ x .= y; y .= z; x \ carrier S; y \ carrier S; z \ carrier S \ \ x .= z" +lemma equivalenceI: + fixes P :: "'a \ 'a \ bool" and E :: "'a set" + assumes refl: "\x. \ x \ E \ \ P x x" + and sym: "\x y. \ x \ E; y \ E \ \ P x y \ P y x" + and trans: "\x y z. \ x \ E; y \ E; z \ E \ \ P x y \ P y z \ P x z" + shows "equivalence \ carrier = E, eq = P \" + unfolding equivalence_def using assms + by (metis eq_object.select_convs(1) partial_object.select_convs(1)) + +locale partition = + fixes A :: "'a set" and B :: "('a set) set" + assumes unique_class: "\a. a \ A \ \!b \ B. a \ b" + and incl: "\b. b \ B \ b \ A" + +lemma equivalence_subset: + assumes "equivalence L" "A \ carrier L" + shows "equivalence (L\ carrier := A \)" +proof - + interpret L: equivalence L + by (simp add: assms) + show ?thesis + by (unfold_locales, simp_all add: L.sym assms rev_subsetD, meson L.trans assms(2) contra_subsetD) +qed + + (* Lemmas by Stephan Hohe *) lemma elemI: fixes R (structure) - assumes "a' \ A" and "a .= a'" + assumes "a' \ A" "a .= a'" shows "a .\ A" -unfolding elem_def -using assms -by fast + unfolding elem_def using assms by auto lemma (in equivalence) elem_exact: - assumes "a \ carrier S" and "a \ A" + assumes "a \ carrier S" "a \ A" shows "a .\ A" -using assms -by (fast intro: elemI) + unfolding elem_def using assms by auto lemma elemE: fixes S (structure) assumes "a .\ A" and "\a'. \a' \ A; a .= a'\ \ P" shows "P" -using assms -unfolding elem_def -by fast + using assms unfolding elem_def by auto lemma (in equivalence) elem_cong_l [trans]: - assumes cong: "a' .= a" - and a: "a .\ A" - and carr: "a \ carrier S" "a' \ carrier S" - and Acarr: "A \ carrier S" + assumes "a \ carrier S" "a' \ carrier S" "A \ carrier S" + and "a' .= a" "a .\ A" shows "a' .\ A" -using a -apply (elim elemE, intro elemI) -proof assumption - fix b - assume bA: "b \ A" - note [simp] = carr bA[THEN subsetD[OF Acarr]] - note cong - also assume "a .= b" - finally show "a' .= b" by simp -qed + using assms by (meson elem_def trans subsetCE) lemma (in equivalence) elem_subsetD: - assumes "A \ B" - and aA: "a .\ A" + assumes "A \ B" "a .\ A" shows "a .\ B" -using assms -by (fast intro: elemI elim: elemE dest: subsetD) + using assms by (fast intro: elemI elim: elemE dest: subsetD) lemma (in equivalence) mem_imp_elem [simp, intro]: - "\ x \ A; x \ carrier S \ \ x .\ A" - unfolding elem_def by blast + assumes "x \ carrier S" + shows "x \ A \ x .\ A" + using assms unfolding elem_def by blast lemma set_eqI: fixes R (structure) - assumes ltr: "\a. a \ A \ a .\ B" - and rtl: "\b. b \ B \ b .\ A" + assumes "\a. a \ A \ a .\ B" + and "\b. b \ B \ b .\ A" shows "A {.=} B" -unfolding set_eq_def -by (fast intro: ltr rtl) + using assms unfolding set_eq_def by auto lemma set_eqI2: fixes R (structure) - assumes ltr: "\a b. a \ A \ \b\B. a .= b" - and rtl: "\b. b \ B \ \a\A. b .= a" + assumes "\a. a \ A \ \b \ B. a .= b" + and "\b. b \ B \ \a \ A. b .= a" shows "A {.=} B" - by (intro set_eqI, unfold elem_def) (fast intro: ltr rtl)+ + using assms by (simp add: set_eqI elem_def) lemma set_eqD1: fixes R (structure) - assumes AA': "A {.=} A'" - and "a \ A" + assumes "A {.=} A'" and "a \ A" shows "\a'\A'. a .= a'" -using assms -unfolding set_eq_def elem_def -by fast + using assms by (simp add: set_eq_def elem_def) lemma set_eqD2: fixes R (structure) - assumes AA': "A {.=} A'" - and "a' \ A'" + assumes "A {.=} A'" and "a' \ A'" shows "\a\A. a' .= a" -using assms -unfolding set_eq_def elem_def -by fast + using assms by (simp add: set_eq_def elem_def) lemma set_eqE: fixes R (structure) - assumes AB: "A {.=} B" - and r: "\\a\A. a .\ B; \b\B. b .\ A\ \ P" + assumes "A {.=} B" + and "\ \a \ A. a .\ B; \b \ B. b .\ A \ \ P" shows "P" -using AB -unfolding set_eq_def -by (blast dest: r) + using assms unfolding set_eq_def by blast lemma set_eqE2: fixes R (structure) - assumes AB: "A {.=} B" - and r: "\\a\A. (\b\B. a .= b); \b\B. (\a\A. b .= a)\ \ P" + assumes "A {.=} B" + and "\ \a \ A. \b \ B. a .= b; \b \ B. \a \ A. b .= a \ \ P" shows "P" -using AB -unfolding set_eq_def elem_def -by (blast dest: r) + using assms unfolding set_eq_def by (simp add: elem_def) lemma set_eqE': fixes R (structure) - assumes AB: "A {.=} B" - and aA: "a \ A" and bB: "b \ B" - and r: "\a' b'. \a' \ A; b .= a'; b' \ B; a .= b'\ \ P" + assumes "A {.=} B" "a \ A" "b \ B" + and "\a' b'. \ a' \ A; b' \ B \ \ b .= a' \ a .= b' \ P" shows "P" -proof - - from AB aA - have "\b'\B. a .= b'" by (rule set_eqD1) - from this obtain b' - where b': "b' \ B" "a .= b'" by auto - - from AB bB - have "\a'\A. b .= a'" by (rule set_eqD2) - from this obtain a' - where a': "a' \ A" "b .= a'" by auto - - from a' b' - show "P" by (rule r) -qed + using assms by (meson set_eqE2) lemma (in equivalence) eq_elem_cong_r [trans]: - assumes a: "a .\ A" - and cong: "A {.=} A'" - and carr: "a \ carrier S" - and Carr: "A \ carrier S" "A' \ carrier S" - shows "a .\ A'" -using a cong -proof (elim elemE set_eqE) - fix b - assume bA: "b \ A" - and inA': "\b\A. b .\ A'" - note [simp] = carr Carr Carr[THEN subsetD] bA - assume "a .= b" - also from bA inA' - have "b .\ A'" by fast - finally - show "a .\ A'" by simp -qed + assumes "A \ carrier S" "A' \ carrier S" "A {.=} A'" + shows "\ a \ carrier S \ \ a .\ A \ a .\ A'" + using assms by (meson elemE elem_cong_l set_eqE subset_eq) lemma (in equivalence) set_eq_sym [sym]: - assumes "A {.=} B" - shows "B {.=} A" -using assms -unfolding set_eq_def elem_def -by fast + assumes "A \ carrier S" "B \ carrier S" + shows "A {.=} B \ B {.=} A" + using assms unfolding set_eq_def elem_def by auto lemma (in equivalence) equal_set_eq_trans [trans]: - assumes AB: "A = B" and BC: "B {.=} C" - shows "A {.=} C" - using AB BC by simp + "\ A = B; B {.=} C \ \ A {.=} C" + by simp lemma (in equivalence) set_eq_equal_trans [trans]: - assumes AB: "A {.=} B" and BC: "B = C" - shows "A {.=} C" - using AB BC by simp + "\ A {.=} B; B = C \ \ A {.=} C" + by simp -lemma (in equivalence) set_eq_trans [trans]: - assumes AB: "A {.=} B" and BC: "B {.=} C" - and carr: "A \ carrier S" "B \ carrier S" "C \ carrier S" +lemma (in equivalence) set_eq_trans_aux: + assumes "A \ carrier S" "B \ carrier S" "C \ carrier S" + and "A {.=} B" "B {.=} C" + shows "\a. a \ A \ a .\ C" + using assms by (simp add: eq_elem_cong_r subset_iff) + +corollary (in equivalence) set_eq_trans [trans]: + assumes "A \ carrier S" "B \ carrier S" "C \ carrier S" + and "A {.=} B" " B {.=} C" shows "A {.=} C" proof (intro set_eqI) - fix a - assume aA: "a \ A" - with carr have "a \ carrier S" by fast - note [simp] = carr this - - from aA - have "a .\ A" by (simp add: elem_exact) - also note AB - also note BC - finally - show "a .\ C" by simp + show "\a. a \ A \ a .\ C" using set_eq_trans_aux assms by blast next - fix c - assume cC: "c \ C" - with carr have "c \ carrier S" by fast - note [simp] = carr this - - from cC - have "c .\ C" by (simp add: elem_exact) - also note BC[symmetric] - also note AB[symmetric] - finally - show "c .\ A" by simp + show "\b. b \ C \ b .\ A" using set_eq_trans_aux set_eq_sym assms by blast qed -lemma (in equivalence) set_eq_insert_aux: - assumes x: "x .= x'" - and carr: "x \ carrier S" "x' \ carrier S" "A \ carrier S" - shows "\a \ (insert x A). a .\ (insert x' A)" -proof - fix a - show "a \ insert x A \ a .\ insert x' A" - proof cases - assume "a \ A" - thus "a .\ insert x' A" - using carr(3) by blast - next - assume "a \ insert x A" "a \ A" - hence "a = x" - by blast - thus "a .\ insert x' A" - by (meson x elemI insertI1) - qed -qed - -lemma (in equivalence) set_eq_insert: - assumes x: "x .= x'" - and carr: "x \ carrier S" "x' \ carrier S" "A \ carrier S" - shows "insert x A {.=} insert x' A" -proof- - have "(\a \ (insert x A). a .\ (insert x' A)) \ - (\a \ (insert x' A). a .\ (insert x A))" - using set_eq_insert_aux carr x sym by blast - thus "insert x A {.=} insert x' A" - using set_eq_def by blast -qed - -lemma (in equivalence) set_eq_pairI: - assumes xx': "x .= x'" - and carr: "x \ carrier S" "x' \ carrier S" "y \ carrier S" - shows "{x, y} {.=} {x', y}" - using assms set_eq_insert by simp - lemma (in equivalence) is_closedI: assumes closed: "\x y. \x .= y; x \ A; y \ carrier S\ \ y \ A" and S: "A \ carrier S" @@ -307,29 +224,28 @@ by (blast dest: closed sym) lemma (in equivalence) closure_of_eq: - "\x .= x'; A \ carrier S; x \ closure_of A; x' \ carrier S\ \ x' \ closure_of A" - unfolding eq_closure_of_def elem_def - by (blast intro: trans sym) + assumes "A \ carrier S" "x \ closure_of A" + shows "\ x' \ carrier S; x .= x' \ \ x' \ closure_of A" + using assms elem_cong_l sym unfolding eq_closure_of_def by blast lemma (in equivalence) is_closed_eq [dest]: - "\x .= x'; x \ A; is_closed A; x \ carrier S; x' \ carrier S\ \ x' \ A" - unfolding eq_is_closed_def - using closure_of_eq [where A = A] - by simp + assumes "is_closed A" "x \ A" + shows "\ x .= x'; x' \ carrier S \ \ x' \ A" + using assms closure_of_eq [where A = A] unfolding eq_is_closed_def by simp -lemma (in equivalence) is_closed_eq_rev [dest]: - "\x .= x'; x' \ A; is_closed A; x \ carrier S; x' \ carrier S\ \ x \ A" - by (meson subsetD eq_is_closed_def is_closed_eq sym) +corollary (in equivalence) is_closed_eq_rev [dest]: + assumes "is_closed A" "x' \ A" + shows "\ x .= x'; x \ carrier S \ \ x \ A" + using sym is_closed_eq assms by (meson contra_subsetD eq_is_closed_def) lemma closure_of_closed [simp, intro]: fixes S (structure) shows "closure_of A \ carrier S" -unfolding eq_closure_of_def -by fast + unfolding eq_closure_of_def by auto lemma closure_of_memI: fixes S (structure) - assumes "a .\ A" and "a \ carrier S" + assumes "a .\ A" "a \ carrier S" shows "a \ closure_of A" by (simp add: assms eq_closure_of_def) @@ -351,67 +267,193 @@ assumes "a \ closure_of A" and "\a'. \a \ carrier S; a' \ A; a .= a'\ \ P" shows "P" - by (meson closure_of_memE elemE assms) + using assms by (meson closure_of_memE elemE) + + +(* Lemmas by Paulo Emílio de Vilhena *) + +lemma (in partition) equivalence_from_partition: + "equivalence \ carrier = A, eq = (\x y. y \ (THE b. b \ B \ x \ b))\" + unfolding partition_def equivalence_def +proof (auto) + let ?f = "\x. THE b. b \ B \ x \ b" + show "\x. x \ A \ x \ ?f x" + using unique_class by (metis (mono_tags, lifting) theI') + show "\x y. \ x \ A; y \ A \ \ y \ ?f x \ x \ ?f y" + using unique_class by (metis (mono_tags, lifting) the_equality) + show "\x y z. \ x \ A; y \ A; z \ A \ \ y \ ?f x \ z \ ?f y \ z \ ?f x" + using unique_class by (metis (mono_tags, lifting) the_equality) +qed + +lemma (in partition) partition_coverture: "\B = A" + by (meson Sup_le_iff UnionI unique_class incl subsetI subset_antisym) + +lemma (in partition) disjoint_union: + assumes "b1 \ B" "b2 \ B" + and "b1 \ b2 \ {}" + shows "b1 = b2" +proof (rule ccontr) + assume "b1 \ b2" + obtain a where "a \ A" "a \ b1" "a \ b2" + using assms(2-3) incl by blast + thus False using unique_class \b1 \ b2\ assms(1) assms(2) by blast +qed + +lemma partitionI: + fixes A :: "'a set" and B :: "('a set) set" + assumes "\B = A" + and "\b1 b2. \ b1 \ B; b2 \ B \ \ b1 \ b2 \ {} \ b1 = b2" + shows "partition A B" +proof + show "\a. a \ A \ \!b. b \ B \ a \ b" + proof (rule ccontr) + fix a assume "a \ A" "\!b. b \ B \ a \ b" + then obtain b1 b2 where "b1 \ B" "a \ b1" + and "b2 \ B" "a \ b2" "b1 \ b2" using assms(1) by blast + thus False using assms(2) by blast + qed +next + show "\b. b \ B \ b \ A" using assms(1) by blast +qed + +lemma (in partition) remove_elem: + assumes "b \ B" + shows "partition (A - b) (B - {b})" +proof + show "\a. a \ A - b \ \!b'. b' \ B - {b} \ a \ b'" + using unique_class by fastforce +next + show "\b'. b' \ B - {b} \ b' \ A - b" + using assms unique_class incl partition_axioms partition_coverture by fastforce +qed + +lemma disjoint_sum: + "\ finite B; finite A; partition A B\ \ (\b\B. \a\b. f a) = (\a\A. f a)" +proof (induct arbitrary: A set: finite) + case empty thus ?case using partition.unique_class by fastforce +next + case (insert b B') + have "(\b\(insert b B'). \a\b. f a) = (\a\b. f a) + (\b\B'. \a\b. f a)" + by (simp add: insert.hyps(1) insert.hyps(2)) + also have "... = (\a\b. f a) + (\a\(A - b). f a)" + using partition.remove_elem[of A "insert b B'" b] insert.hyps insert.prems + by (metis Diff_insert_absorb finite_Diff insert_iff) + finally show "(\b\(insert b B'). \a\b. f a) = (\a\A. f a)" + using partition.remove_elem[of A "insert b B'" b] insert.prems + by (metis add.commute insert_iff partition.incl sum.subset_diff) +qed + +lemma (in partition) disjoint_sum: + assumes "finite A" + shows "(\b\B. \a\b. f a) = (\a\A. f a)" +proof - + have "finite B" + by (simp add: assms finite_UnionD partition_coverture) + thus ?thesis using disjoint_sum assms partition_axioms by blast +qed + +lemma (in equivalence) set_eq_insert_aux: + assumes "A \ carrier S" + and "x \ carrier S" "x' \ carrier S" "x .= x'" + and "y \ insert x A" + shows "y .\ insert x' A" + by (metis assms(1) assms(4) assms(5) contra_subsetD elemI elem_exact insert_iff) + +corollary (in equivalence) set_eq_insert: + assumes "A \ carrier S" + and "x \ carrier S" "x' \ carrier S" "x .= x'" + shows "insert x A {.=} insert x' A" + by (meson set_eqI assms set_eq_insert_aux sym equivalence_axioms) + +lemma (in equivalence) set_eq_pairI: + assumes xx': "x .= x'" + and carr: "x \ carrier S" "x' \ carrier S" "y \ carrier S" + shows "{x, y} {.=} {x', y}" + using assms set_eq_insert by simp lemma (in equivalence) closure_inclusion: assumes "A \ B" shows "closure_of A \ closure_of B" - unfolding eq_closure_of_def -proof - fix x - assume "x \ {y \ carrier S. y .\ A}" - hence "x \ carrier S \ x .\ A" - by blast - hence "x \ carrier S \ x .\ B" - using assms elem_subsetD by blast - thus "x \ {y \ carrier S. y .\ B}" - by simp -qed + unfolding eq_closure_of_def using assms elem_subsetD by auto lemma (in equivalence) classes_small: assumes "is_closed B" and "A \ B" shows "closure_of A \ B" -proof- - have "closure_of A \ closure_of B" - using closure_inclusion assms by simp - thus "closure_of A \ B" - using assms(1) eq_is_closed_def by fastforce -qed + by (metis assms closure_inclusion eq_is_closed_def) lemma (in equivalence) classes_eq: assumes "A \ carrier S" shows "A {.=} closure_of A" -using assms -by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE) + using assms by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE) lemma (in equivalence) complete_classes: - assumes c: "is_closed A" + assumes "is_closed A" shows "A = closure_of A" using assms by (simp add: eq_is_closed_def) -lemma (in equivalence) closure_idemp_weak: +lemma (in equivalence) closure_idem_weak: "closure_of (closure_of A) {.=} closure_of A" by (simp add: classes_eq set_eq_sym) -lemma (in equivalence) closure_idemp_strong: +lemma (in equivalence) closure_idem_strong: assumes "A \ carrier S" shows "closure_of (closure_of A) = closure_of A" using assms closure_of_eq complete_classes is_closedI by auto -lemma (in equivalence) complete_classes2: +lemma (in equivalence) classes_consistent: assumes "A \ carrier S" shows "is_closed (closure_of A)" - using closure_idemp_strong by (simp add: assms eq_is_closed_def) + using closure_idem_strong by (simp add: assms eq_is_closed_def) + +lemma (in equivalence) classes_coverture: + "\classes = carrier S" +proof + show "\classes \ carrier S" + unfolding eq_classes_def eq_class_of_def by blast +next + show "carrier S \ \classes" unfolding eq_classes_def eq_class_of_def + proof + fix x assume "x \ carrier S" + hence "x \ {y \ carrier S. x .= y}" using refl by simp + thus "x \ \{{y \ carrier S. x .= y} |x. x \ carrier S}" by blast + qed +qed -lemma equivalence_subset: - assumes "equivalence L" "A \ carrier L" - shows "equivalence (L\ carrier := A \)" +lemma (in equivalence) disjoint_union: + assumes "class1 \ classes" "class2 \ classes" + and "class1 \ class2 \ {}" + shows "class1 = class2" proof - - interpret L: equivalence L - by (simp add: assms) - show ?thesis - by (unfold_locales, simp_all add: L.sym assms rev_subsetD, meson L.trans assms(2) contra_subsetD) + obtain x y where x: "x \ carrier S" "class1 = class_of x" + and y: "y \ carrier S" "class2 = class_of y" + using assms(1-2) unfolding eq_classes_def by blast + obtain z where z: "z \ carrier S" "z \ class1 \ class2" + using assms classes_coverture by fastforce + hence "x .= z \ y .= z" using x y unfolding eq_class_of_def by blast + hence "x .= y" using x y z trans sym by meson + hence "class_of x = class_of y" + unfolding eq_class_of_def using local.sym trans x y by blast + thus ?thesis using x y by simp +qed + +lemma (in equivalence) partition_from_equivalence: + "partition (carrier S) classes" +proof (intro partitionI) + show "\classes = carrier S" using classes_coverture by simp +next + show "\class1 class2. \ class1 \ classes; class2 \ classes \ \ + class1 \ class2 \ {} \ class1 = class2" + using disjoint_union by simp +qed + +lemma (in equivalence) disjoint_sum: + assumes "finite (carrier S)" + shows "(\c\classes. \x\c. f x) = (\x\(carrier S). f x)" +proof - + have "finite classes" + unfolding eq_classes_def using assms by auto + thus ?thesis using disjoint_sum assms partition_from_equivalence by blast qed end diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Tue Jun 12 16:21:52 2018 +0200 +++ b/src/HOL/Algebra/Coset.thy Tue Jun 12 16:09:12 2018 +0100 @@ -38,346 +38,325 @@ normal_rel :: "['a set, ('a, 'b) monoid_scheme] \ bool" (infixl "\" 60) where "H \ G \ normal H G" +(* ************************************************************************** *) +(* Next two lemmas contributed by Martin Baillon. *) + +lemma l_coset_eq_set_mult: + fixes G (structure) + shows "x <# H = {x} <#> H" + unfolding l_coset_def set_mult_def by simp + +lemma r_coset_eq_set_mult: + fixes G (structure) + shows "H #> x = H <#> {x}" + unfolding r_coset_def set_mult_def by simp + +(* ************************************************************************** *) + + +(* ************************************************************************** *) +(* Next five lemmas contributed by Paulo Emílio de Vilhena. *) + +lemma (in subgroup) rcosets_not_empty: + assumes "R \ rcosets H" + shows "R \ {}" +proof - + obtain g where "g \ carrier G" "R = H #> g" + using assms unfolding RCOSETS_def by blast + hence "\ \ g \ R" + using one_closed unfolding r_coset_def by blast + thus ?thesis by blast +qed + +lemma (in group) diff_neutralizes: + assumes "subgroup H G" "R \ rcosets H" + shows "\r1 r2. \ r1 \ R; r2 \ R \ \ r1 \ (inv r2) \ H" +proof - + fix r1 r2 assume r1: "r1 \ R" and r2: "r2 \ R" + obtain g where g: "g \ carrier G" "R = H #> g" + using assms unfolding RCOSETS_def by blast + then obtain h1 h2 where h1: "h1 \ H" "r1 = h1 \ g" + and h2: "h2 \ H" "r2 = h2 \ g" + using r1 r2 unfolding r_coset_def by blast + hence "r1 \ (inv r2) = (h1 \ g) \ ((inv g) \ (inv h2))" + using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce + also have " ... = (h1 \ (g \ inv g) \ inv h2)" + using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc + monoid_axioms subgroup.mem_carrier by smt + finally have "r1 \ inv r2 = h1 \ inv h2" + using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce + thus "r1 \ inv r2 \ H" by (metis assms(1) h1(1) h2(1) subgroup_def) +qed + + +subsection \Stable Operations for Subgroups\ + +lemma (in group) subgroup_set_mult_equality[simp]: + assumes "subgroup H G" "I \ H" "J \ H" + shows "I <#>\<^bsub>G \ carrier := H \\<^esub> J = I <#> J" + unfolding set_mult_def subgroup_mult_equality[OF assms(1)] by auto + +lemma (in group) subgroup_rcos_equality[simp]: + assumes "subgroup H G" "I \ H" "h \ H" + shows "I #>\<^bsub>G \ carrier := H \\<^esub> h = I #> h" + using subgroup_set_mult_equality by (simp add: r_coset_eq_set_mult assms) + +lemma (in group) subgroup_lcos_equality[simp]: + assumes "subgroup H G" "I \ H" "h \ H" + shows "h <#\<^bsub>G \ carrier := H \\<^esub> I = h <# I" + using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms) + +(* ************************************************************************** *) + + +subsection \Basic Properties of set_mult\ + +lemma (in group) setmult_subset_G: + assumes "H \ carrier G" "K \ carrier G" + shows "H <#> K \ carrier G" using assms + by (auto simp add: set_mult_def subsetD) + +lemma (in monoid) set_mult_closed: + assumes "H \ carrier G" "K \ carrier G" + shows "H <#> K \ carrier G" + using assms by (auto simp add: set_mult_def subsetD) + +(* ************************************************************************** *) +(* Next lemma contributed by Martin Baillon. *) + +lemma (in group) set_mult_assoc: + assumes "M \ carrier G" "H \ carrier G" "K \ carrier G" + shows "(M <#> H) <#> K = M <#> (H <#> K)" +proof + show "(M <#> H) <#> K \ M <#> (H <#> K)" + proof + fix x assume "x \ (M <#> H) <#> K" + then obtain m h k where x: "m \ M" "h \ H" "k \ K" "x = (m \ h) \ k" + unfolding set_mult_def by blast + hence "x = m \ (h \ k)" + using assms m_assoc by blast + thus "x \ M <#> (H <#> K)" + unfolding set_mult_def using x by blast + qed +next + show "M <#> (H <#> K) \ (M <#> H) <#> K" + proof + fix x assume "x \ M <#> (H <#> K)" + then obtain m h k where x: "m \ M" "h \ H" "k \ K" "x = m \ (h \ k)" + unfolding set_mult_def by blast + hence "x = (m \ h) \ k" + using assms m_assoc rev_subsetD by metis + thus "x \ (M <#> H) <#> K" + unfolding set_mult_def using x by blast + qed +qed + +(* ************************************************************************** *) + subsection \Basic Properties of Cosets\ lemma (in group) coset_mult_assoc: - "[| M \ carrier G; g \ carrier G; h \ carrier G |] - ==> (M #> g) #> h = M #> (g \ h)" -by (force simp add: r_coset_def m_assoc) + assumes "M \ carrier G" "g \ carrier G" "h \ carrier G" + shows "(M #> g) #> h = M #> (g \ h)" + using assms by (force simp add: r_coset_def m_assoc) + +lemma (in group) coset_assoc: + assumes "x \ carrier G" "y \ carrier G" "H \ carrier G" + shows "x <# (H #> y) = (x <# H) #> y" + using set_mult_assoc[of "{x}" H "{y}"] + by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult assms) lemma (in group) coset_mult_one [simp]: "M \ carrier G ==> M #> \ = M" by (force simp add: r_coset_def) lemma (in group) coset_mult_inv1: - "[| M #> (x \ (inv y)) = M; x \ carrier G ; y \ carrier G; - M \ carrier G |] ==> M #> x = M #> y" -apply (erule subst [of concl: "%z. M #> x = z #> y"]) -apply (simp add: coset_mult_assoc m_assoc) -done + assumes "M #> (x \ (inv y)) = M" + and "x \ carrier G" "y \ carrier G" "M \ carrier G" + shows "M #> x = M #> y" using assms + by (metis coset_mult_assoc group.inv_solve_right is_group subgroup_def subgroup_self) lemma (in group) coset_mult_inv2: - "[| M #> x = M #> y; x \ carrier G; y \ carrier G; M \ carrier G |] - ==> M #> (x \ (inv y)) = M " -apply (simp add: coset_mult_assoc [symmetric]) -apply (simp add: coset_mult_assoc) -done + assumes "M #> x = M #> y" + and "x \ carrier G" "y \ carrier G" "M \ carrier G" + shows "M #> (x \ (inv y)) = M " using assms + by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv) lemma (in group) coset_join1: - "[| H #> x = H; x \ carrier G; subgroup H G |] ==> x \ H" -apply (erule subst) -apply (simp add: r_coset_def) -apply (blast intro: l_one subgroup.one_closed sym) -done + assumes "H #> x = H" + and "x \ carrier G" "subgroup H G" + shows "x \ H" + using assms r_coset_def l_one subgroup.one_closed sym by fastforce lemma (in group) solve_equation: - "\subgroup H G; x \ H; y \ H\ \ \h\H. y = h \ x" -apply (rule bexI [of _ "y \ (inv x)"]) -apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc - subgroup.subset [THEN subsetD]) -done + assumes "subgroup H G" "x \ H" "y \ H" + shows "\h \ H. y = h \ x" +proof - + have "y = (y \ (inv x)) \ x" using assms + by (simp add: m_assoc subgroup.mem_carrier) + moreover have "y \ (inv x) \ H" using assms + by (simp add: subgroup_def) + ultimately show ?thesis by blast +qed lemma (in group) repr_independence: - "\y \ H #> x; x \ carrier G; subgroup H G\ \ H #> x = H #> y" + assumes "y \ H #> x" "x \ carrier G" "subgroup H G" + shows "H #> x = H #> y" using assms by (auto simp add: r_coset_def m_assoc [symmetric] subgroup.subset [THEN subsetD] subgroup.m_closed solve_equation) lemma (in group) coset_join2: - "\x \ carrier G; subgroup H G; x\H\ \ H #> x = H" + assumes "x \ carrier G" "subgroup H G" "x \ H" + shows "H #> x = H" using assms \ \Alternative proof is to put @{term "x=\"} in \repr_independence\.\ by (force simp add: subgroup.m_closed r_coset_def solve_equation) +lemma (in group) coset_join3: + assumes "x \ carrier G" "subgroup H G" "x \ H" + shows "x <# H = H" +proof + have "\h. h \ H \ x \ h \ H" using assms + by (simp add: subgroup.m_closed) + thus "x <# H \ H" unfolding l_coset_def by blast +next + have "\h. h \ H \ x \ ((inv x) \ h) = h" + by (smt assms inv_closed l_one m_assoc r_inv subgroup.mem_carrier) + moreover have "\h. h \ H \ (inv x) \ h \ H" + by (simp add: assms subgroup.m_closed subgroup.m_inv_closed) + ultimately show "H \ x <# H" unfolding l_coset_def by blast +qed + lemma (in monoid) r_coset_subset_G: - "[| H \ carrier G; x \ carrier G |] ==> H #> x \ carrier G" + "\ H \ carrier G; x \ carrier G \ \ H #> x \ carrier G" by (auto simp add: r_coset_def) lemma (in group) rcosI: - "[| h \ H; H \ carrier G; x \ carrier G|] ==> h \ x \ H #> x" + "\ h \ H; H \ carrier G; x \ carrier G \ \ h \ x \ H #> x" by (auto simp add: r_coset_def) lemma (in group) rcosetsI: "\H \ carrier G; x \ carrier G\ \ H #> x \ rcosets H" by (auto simp add: RCOSETS_def) -text\Really needed?\ -lemma (in group) transpose_inv: - "[| x \ y = z; x \ carrier G; y \ carrier G; z \ carrier G |] - ==> (inv x) \ z = y" -by (force simp add: m_assoc [symmetric]) - -lemma (in group) rcos_self: "[| x \ carrier G; subgroup H G |] ==> x \ H #> x" -apply (simp add: r_coset_def) -apply (blast intro: sym l_one subgroup.subset [THEN subsetD] - subgroup.one_closed) -done +lemma (in group) rcos_self: + "\ x \ carrier G; subgroup H G \ \ x \ H #> x" + by (metis l_one rcosI subgroup_def) text (in group) \Opposite of @{thm [source] "repr_independence"}\ lemma (in group) repr_independenceD: - assumes "subgroup H G" - assumes ycarr: "y \ carrier G" - and repr: "H #> x = H #> y" + assumes "subgroup H G" "y \ carrier G" + and "H #> x = H #> y" shows "y \ H #> x" -proof - - interpret subgroup H G by fact - show ?thesis apply (subst repr) - apply (intro rcos_self) - apply (rule ycarr) - apply (rule is_subgroup) - done -qed + using assms by (simp add: rcos_self) text \Elements of a right coset are in the carrier\ lemma (in subgroup) elemrcos_carrier: - assumes "group G" - assumes acarr: "a \ carrier G" - and a': "a' \ H #> a" + assumes "group G" "a \ carrier G" + and "a' \ H #> a" shows "a' \ carrier G" -proof - - interpret group G by fact - from subset and acarr - have "H #> a \ carrier G" by (rule r_coset_subset_G) - from this and a' - show "a' \ carrier G" - by fast -qed + by (meson assms group.is_monoid monoid.r_coset_subset_G subset subsetCE) lemma (in subgroup) rcos_const: - assumes "group G" - assumes hH: "h \ H" + assumes "group G" "h \ H" shows "H #> h = H" -proof - - interpret group G by fact - show ?thesis apply (unfold r_coset_def) - apply rule - apply rule - apply clarsimp - apply (intro subgroup.m_closed) - apply (rule is_subgroup) - apply assumption - apply (rule hH) - apply rule - apply simp - proof - - fix h' - assume h'H: "h' \ H" - note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier] - from carr - have a: "h' = (h' \ inv h) \ h" by (simp add: m_assoc) - from h'H hH - have "h' \ inv h \ H" by simp - from this and a - show "\x\H. h' = x \ h" by fast - qed -qed + using group.coset_join2[OF assms(1), of h H] + by (simp add: assms(2) subgroup_axioms) -text \Step one for lemma \rcos_module\\ lemma (in subgroup) rcos_module_imp: - assumes "group G" - assumes xcarr: "x \ carrier G" - and x'cos: "x' \ H #> x" + assumes "group G" "x \ carrier G" + and "x' \ H #> x" shows "(x' \ inv x) \ H" proof - - interpret group G by fact - from xcarr x'cos - have x'carr: "x' \ carrier G" - by (rule elemrcos_carrier[OF is_group]) - from xcarr - have ixcarr: "inv x \ carrier G" - by simp - from x'cos - have "\h\H. x' = h \ x" - unfolding r_coset_def - by fast - from this - obtain h - where hH: "h \ H" - and x': "x' = h \ x" - by auto - from hH and subset - have hcarr: "h \ carrier G" by fast - note carr = xcarr x'carr hcarr - from x' and carr - have "x' \ (inv x) = (h \ x) \ (inv x)" by fast - also from carr - have "\ = h \ (x \ inv x)" by (simp add: m_assoc) - also from carr - have "\ = h \ \" by simp - also from carr - have "\ = h" by simp - finally - have "x' \ (inv x) = h" by simp - from hH this - show "x' \ (inv x) \ H" by simp + obtain h where h: "h \ H" "x' = h \ x" + using assms(3) unfolding r_coset_def by blast + hence "x' \ inv x = h" + by (metis assms elemrcos_carrier group.inv_solve_right mem_carrier) + thus ?thesis using h by blast qed -text \Step two for lemma \rcos_module\\ lemma (in subgroup) rcos_module_rev: - assumes "group G" - assumes carr: "x \ carrier G" "x' \ carrier G" - and xixH: "(x' \ inv x) \ H" + assumes "group G" "x \ carrier G" "x' \ carrier G" + and "(x' \ inv x) \ H" shows "x' \ H #> x" proof - - interpret group G by fact - from xixH - have "\h\H. x' \ (inv x) = h" by fast - from this - obtain h - where hH: "h \ H" - and hsym: "x' \ (inv x) = h" - by fast - from hH subset have hcarr: "h \ carrier G" by simp - note carr = carr hcarr - from hsym[symmetric] have "h \ x = x' \ (inv x) \ x" by fast - also from carr - have "\ = x' \ ((inv x) \ x)" by (simp add: m_assoc) - also from carr - have "\ = x' \ \" by simp - also from carr - have "\ = x'" by simp - finally - have "h \ x = x'" by simp - from this[symmetric] and hH - show "x' \ H #> x" - unfolding r_coset_def - by fast + obtain h where h: "h \ H" "x' \ inv x = h" + using assms(4) unfolding r_coset_def by blast + hence "x' = h \ x" + by (metis assms group.inv_solve_right mem_carrier) + thus ?thesis using h unfolding r_coset_def by blast qed text \Module property of right cosets\ lemma (in subgroup) rcos_module: - assumes "group G" - assumes carr: "x \ carrier G" "x' \ carrier G" + assumes "group G" "x \ carrier G" "x' \ carrier G" shows "(x' \ H #> x) = (x' \ inv x \ H)" -proof - - interpret group G by fact - show ?thesis proof assume "x' \ H #> x" - from this and carr - show "x' \ inv x \ H" - by (intro rcos_module_imp[OF is_group]) - next - assume "x' \ inv x \ H" - from this and carr - show "x' \ H #> x" - by (intro rcos_module_rev[OF is_group]) - qed -qed + using rcos_module_rev rcos_module_imp assms by blast text \Right cosets are subsets of the carrier.\ lemma (in subgroup) rcosets_carrier: - assumes "group G" - assumes XH: "X \ rcosets H" + assumes "group G" "X \ rcosets H" shows "X \ carrier G" -proof - - interpret group G by fact - from XH have "\x\ carrier G. X = H #> x" - unfolding RCOSETS_def - by fast - from this - obtain x - where xcarr: "x\ carrier G" - and X: "X = H #> x" - by fast - from subset and xcarr - show "X \ carrier G" - unfolding X - by (rule r_coset_subset_G) -qed + using assms elemrcos_carrier singletonD + subset_eq unfolding RCOSETS_def by force + text \Multiplication of general subsets\ -lemma (in monoid) set_mult_closed: - assumes Acarr: "A \ carrier G" - and Bcarr: "B \ carrier G" - shows "A <#> B \ carrier G" -apply rule apply (simp add: set_mult_def, clarsimp) -proof - - fix a b - assume "a \ A" - from this and Acarr - have acarr: "a \ carrier G" by fast - - assume "b \ B" - from this and Bcarr - have bcarr: "b \ carrier G" by fast - - from acarr bcarr - show "a \ b \ carrier G" by (rule m_closed) -qed lemma (in comm_group) mult_subgroups: - assumes subH: "subgroup H G" - and subK: "subgroup K G" + assumes "subgroup H G" and "subgroup K G" shows "subgroup (H <#> K) G" -apply (rule subgroup.intro) - apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK]) - apply (simp add: set_mult_def) apply clarsimp defer 1 - apply (simp add: set_mult_def) defer 1 - apply (simp add: set_mult_def, clarsimp) defer 1 -proof - - fix ha hb ka kb - assume haH: "ha \ H" and hbH: "hb \ H" and kaK: "ka \ K" and kbK: "kb \ K" - note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]] - kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]] - from carr - have "(ha \ ka) \ (hb \ kb) = ha \ (ka \ hb) \ kb" by (simp add: m_assoc) - also from carr - have "\ = ha \ (hb \ ka) \ kb" by (simp add: m_comm) - also from carr - have "\ = (ha \ hb) \ (ka \ kb)" by (simp add: m_assoc) - finally - have eq: "(ha \ ka) \ (hb \ kb) = (ha \ hb) \ (ka \ kb)" . - - from haH hbH have hH: "ha \ hb \ H" by (simp add: subgroup.m_closed[OF subH]) - from kaK kbK have kK: "ka \ kb \ K" by (simp add: subgroup.m_closed[OF subK]) - - from hH and kK and eq - show "\h'\H. \k'\K. (ha \ ka) \ (hb \ kb) = h' \ k'" by fast +proof (rule subgroup.intro) + show "H <#> K \ carrier G" + by (simp add: setmult_subset_G assms subgroup_imp_subset) +next + have "\ \ \ \ H <#> K" + unfolding set_mult_def using assms subgroup.one_closed by blast + thus "\ \ H <#> K" by simp next - have "\ = \ \ \" by simp - from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this - show "\h\H. \k\K. \ = h \ k" by fast + show "\x. x \ H <#> K \ inv x \ H <#> K" + proof - + fix x assume "x \ H <#> K" + then obtain h k where hk: "h \ H" "k \ K" "x = h \ k" + unfolding set_mult_def by blast + hence "inv x = (inv k) \ (inv h)" + by (meson inv_mult_group assms subgroup.mem_carrier) + hence "inv x = (inv h) \ (inv k)" + by (metis hk inv_mult assms subgroup.mem_carrier) + thus "inv x \ H <#> K" + unfolding set_mult_def using hk assms + by (metis (no_types, lifting) UN_iff singletonI subgroup_def) + qed next - fix h k - assume hH: "h \ H" - and kK: "k \ K" - - from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]] - have "inv (h \ k) = inv h \ inv k" by (simp add: inv_mult_group m_comm) - - from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this - show "\ha\H. \ka\K. inv (h \ k) = ha \ ka" by fast + show "\x y. x \ H <#> K \ y \ H <#> K \ x \ y \ H <#> K" + proof - + fix x y assume "x \ H <#> K" "y \ H <#> K" + then obtain h1 k1 h2 k2 where h1k1: "h1 \ H" "k1 \ K" "x = h1 \ k1" + and h2k2: "h2 \ H" "k2 \ K" "y = h2 \ k2" + unfolding set_mult_def by blast + hence "x \ y = (h1 \ k1) \ (h2 \ k2)" by simp + also have " ... = h1 \ (k1 \ h2) \ k2" + by (smt h1k1 h2k2 m_assoc m_closed assms subgroup.mem_carrier) + also have " ... = h1 \ (h2 \ k1) \ k2" + by (metis (no_types, hide_lams) assms m_comm h1k1(2) h2k2(1) subgroup.mem_carrier) + finally have "x \ y = (h1 \ h2) \ (k1 \ k2)" + by (smt assms h1k1 h2k2 m_assoc monoid.m_closed monoid_axioms subgroup.mem_carrier) + thus "x \ y \ H <#> K" unfolding set_mult_def + using subgroup.m_closed[OF assms(1) h1k1(1) h2k2(1)] + subgroup.m_closed[OF assms(2) h1k1(2) h2k2(2)] by blast + qed qed lemma (in subgroup) lcos_module_rev: - assumes "group G" - assumes carr: "x \ carrier G" "x' \ carrier G" - and xixH: "(inv x \ x') \ H" + assumes "group G" "x \ carrier G" "x' \ carrier G" + and "(inv x \ x') \ H" shows "x' \ x <# H" proof - - interpret group G by fact - from xixH - have "\h\H. (inv x) \ x' = h" by fast - from this - obtain h - where hH: "h \ H" - and hsym: "(inv x) \ x' = h" - by fast - - from hH subset have hcarr: "h \ carrier G" by simp - note carr = carr hcarr - from hsym[symmetric] have "x \ h = x \ ((inv x) \ x')" by fast - also from carr - have "\ = (x \ (inv x)) \ x'" by (simp add: m_assoc[symmetric]) - also from carr - have "\ = \ \ x'" by simp - also from carr - have "\ = x'" by simp - finally - have "x \ h = x'" by simp - - from this[symmetric] and hH - show "x' \ x <# H" - unfolding l_coset_def - by fast + obtain h where h: "h \ H" "inv x \ x' = h" + using assms(4) unfolding l_coset_def by blast + hence "x' = x \ h" + by (metis assms group.inv_solve_left mem_carrier) + thus ?thesis using h unfolding l_coset_def by blast qed @@ -391,21 +370,21 @@ by (simp add: normal_def normal_axioms_def is_group) lemma (in normal) inv_op_closed1: - "\x \ carrier G; h \ H\ \ (inv x) \ h \ x \ H" -apply (insert coset_eq) -apply (auto simp add: l_coset_def r_coset_def) -apply (drule bspec, assumption) -apply (drule equalityD1 [THEN subsetD], blast, clarify) -apply (simp add: m_assoc) -apply (simp add: m_assoc [symmetric]) -done + assumes "x \ carrier G" and "h \ H" + shows "(inv x) \ h \ x \ H" +proof - + have "h \ x \ x <# H" + using assms coset_eq assms(1) unfolding r_coset_def by blast + then obtain h' where "h' \ H" "h \ x = x \ h'" + unfolding l_coset_def by blast + thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier) +qed lemma (in normal) inv_op_closed2: - "\x \ carrier G; h \ H\ \ x \ h \ (inv x) \ H" -apply (subgoal_tac "inv (inv x) \ h \ (inv x) \ H") -apply (simp add: ) -apply (blast intro: inv_op_closed1) -done + assumes "x \ carrier G" and "h \ H" + shows "x \ h \ (inv x) \ H" + using assms inv_op_closed1 by (metis inv_closed inv_inv) + text\Alternative characterization of normal subgroups\ lemma (in group) normal_inv_iff: @@ -455,74 +434,81 @@ qed qed +corollary (in group) normal_invI: + assumes "subgroup N G" and "\x h. \ x \ carrier G; h \ N \ \ x \ h \ inv x \ N" + shows "N \ G" + using assms normal_inv_iff by blast -subsection\More Properties of Cosets\ +corollary (in group) normal_invE: + assumes "N \ G" + shows "subgroup N G" and "\x h. \ x \ carrier G; h \ N \ \ x \ h \ inv x \ N" + using assms normal_inv_iff apply blast + by (simp add: assms normal.inv_op_closed2) + + +lemma (in group) one_is_normal : + "{\} \ G" +proof(intro normal_invI ) + show "subgroup {\} G" + by (simp add: subgroup_def) + show "\x h. x \ carrier G \ h \ {\} \ x \ h \ inv x \ {\}" by simp +qed + + +subsection\More Properties of Left Cosets\ + +lemma (in group) l_repr_independence: + assumes "y \ x <# H" "x \ carrier G" "subgroup H G" + shows "x <# H = y <# H" +proof - + obtain h' where h': "h' \ H" "y = x \ h'" + using assms(1) unfolding l_coset_def by blast + hence "\ h. h \ H \ x \ h = y \ ((inv h') \ h)" + by (smt assms(2-3) inv_closed inv_solve_right m_assoc m_closed subgroup.mem_carrier) + hence "\ xh. xh \ x <# H \ xh \ y <# H" + unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def) + moreover have "\ h. h \ H \ y \ h = x \ (h' \ h)" + using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier) + hence "\ yh. yh \ y <# H \ yh \ x <# H" + unfolding l_coset_def using subgroup.m_closed[OF assms(3) h'(1)] by blast + ultimately show ?thesis by blast +qed lemma (in group) lcos_m_assoc: - "[| M \ carrier G; g \ carrier G; h \ carrier G |] - ==> g <# (h <# M) = (g \ h) <# M" + "\ M \ carrier G; g \ carrier G; h \ carrier G \ \ g <# (h <# M) = (g \ h) <# M" by (force simp add: l_coset_def m_assoc) -lemma (in group) lcos_mult_one: "M \ carrier G ==> \ <# M = M" +lemma (in group) lcos_mult_one: "M \ carrier G \ \ <# M = M" by (force simp add: l_coset_def) lemma (in group) l_coset_subset_G: - "[| H \ carrier G; x \ carrier G |] ==> x <# H \ carrier G" + "\ H \ carrier G; x \ carrier G \ \ x <# H \ carrier G" by (auto simp add: l_coset_def subsetD) -lemma (in group) l_coset_swap: - "\y \ x <# H; x \ carrier G; subgroup H G\ \ x \ y <# H" -proof (simp add: l_coset_def) - assume "\h\H. y = x \ h" - and x: "x \ carrier G" - and sb: "subgroup H G" - then obtain h' where h': "h' \ H \ x \ h' = y" by blast - show "\h\H. x = y \ h" - proof - show "x = y \ inv h'" using h' x sb - by (auto simp add: m_assoc subgroup.subset [THEN subsetD]) - show "inv h' \ H" using h' sb - by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed) - qed -qed - lemma (in group) l_coset_carrier: - "[| y \ x <# H; x \ carrier G; subgroup H G |] ==> y \ carrier G" -by (auto simp add: l_coset_def m_assoc - subgroup.subset [THEN subsetD] subgroup.m_closed) + "\ y \ x <# H; x \ carrier G; subgroup H G \ \ y \ carrier G" + by (auto simp add: l_coset_def m_assoc subgroup.subset [THEN subsetD] subgroup.m_closed) -lemma (in group) l_repr_imp_subset: - assumes y: "y \ x <# H" and x: "x \ carrier G" and sb: "subgroup H G" - shows "y <# H \ x <# H" -proof - - from y - obtain h' where "h' \ H" "x \ h' = y" by (auto simp add: l_coset_def) - thus ?thesis using x sb - by (auto simp add: l_coset_def m_assoc - subgroup.subset [THEN subsetD] subgroup.m_closed) -qed +lemma (in group) l_coset_swap: + assumes "y \ x <# H" "x \ carrier G" "subgroup H G" + shows "x \ y <# H" + using assms(2) l_repr_independence[OF assms] subgroup.one_closed[OF assms(3)] + unfolding l_coset_def by fastforce -lemma (in group) l_repr_independence: - assumes y: "y \ x <# H" and x: "x \ carrier G" and sb: "subgroup H G" - shows "x <# H = y <# H" +lemma (in group) subgroup_mult_id: + assumes "subgroup H G" + shows "H <#> H = H" proof - show "x <# H \ y <# H" - by (rule l_repr_imp_subset, - (blast intro: l_coset_swap l_coset_carrier y x sb)+) - show "y <# H \ x <# H" by (rule l_repr_imp_subset [OF y x sb]) + show "H <#> H \ H" + unfolding set_mult_def using subgroup.m_closed[OF assms] by (simp add: UN_subset_iff) + show "H \ H <#> H" + proof + fix x assume x: "x \ H" thus "x \ H <#> H" unfolding set_mult_def + using subgroup.m_closed[OF assms subgroup.one_closed[OF assms] x] subgroup.one_closed[OF assms] + by (smt UN_iff assms coset_join3 l_coset_def subgroup.mem_carrier) + qed qed -lemma (in group) setmult_subset_G: - "\H \ carrier G; K \ carrier G\ \ H <#> K \ carrier G" -by (auto simp add: set_mult_def subsetD) - -lemma (in group) subgroup_mult_id: "subgroup H G \ H <#> H = H" -apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def) -apply (rule_tac x = x in bexI) -apply (rule bexI [of _ "\"]) -apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD]) -done - subsubsection \Set of Inverses of an \r_coset\.\ @@ -552,20 +538,21 @@ subsubsection \Theorems for \<#>\ with \#>\ or \<#\.\ lemma (in group) setmult_rcos_assoc: - "\H \ carrier G; K \ carrier G; x \ carrier G\ - \ H <#> (K #> x) = (H <#> K) #> x" -by (force simp add: r_coset_def set_mult_def m_assoc) + "\H \ carrier G; K \ carrier G; x \ carrier G\ \ + H <#> (K #> x) = (H <#> K) #> x" + using set_mult_assoc[of H K "{x}"] by (simp add: r_coset_eq_set_mult) lemma (in group) rcos_assoc_lcos: - "\H \ carrier G; K \ carrier G; x \ carrier G\ - \ (H #> x) <#> K = H <#> (x <# K)" -by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc) + "\H \ carrier G; K \ carrier G; x \ carrier G\ \ + (H #> x) <#> K = H <#> (x <# K)" + using set_mult_assoc[of H "{x}" K] + by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult) lemma (in normal) rcos_mult_step1: - "\x \ carrier G; y \ carrier G\ - \ (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y" -by (simp add: setmult_rcos_assoc subset - r_coset_subset_G l_coset_subset_G rcos_assoc_lcos) + "\x \ carrier G; y \ carrier G\ \ + (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y" + by (simp add: setmult_rcos_assoc r_coset_subset_G + subset l_coset_subset_G rcos_assoc_lcos) lemma (in normal) rcos_mult_step2: "\x \ carrier G; y \ carrier G\ @@ -645,7 +632,7 @@ lemma (in subgroup) l_coset_eq_rcong: assumes "group G" assumes a: "a \ carrier G" - shows "a <# H = rcong H `` {a}" + shows "a <# H = (rcong H) `` {a}" proof - interpret group G by fact show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) @@ -661,9 +648,7 @@ proof - interpret subgroup H G by fact from p show ?thesis apply (rule_tac UN_I [of "hb \ ((inv ha) \ h)"]) - apply (simp add: ) - apply (simp add: m_assoc transpose_inv) - done + apply blast by (simp add: inv_solve_left m_assoc) qed lemma (in group) rcos_disjoint: @@ -793,28 +778,47 @@ "\H \ carrier G; a \ carrier G\ \ inj_on (\y. y \ a) H" by (force simp add: inj_on_def subsetD) +(* ************************************************************************** *) + lemma (in group) card_cosets_equal: - "\c \ rcosets H; H \ carrier G; finite(carrier G)\ - \ card c = card H" -apply (auto simp add: RCOSETS_def) -apply (rule card_bij_eq) - apply (rule inj_on_f, assumption+) - apply (force simp add: m_assoc subsetD r_coset_def) - apply (rule inj_on_g, assumption+) - apply (force simp add: m_assoc subsetD r_coset_def) - txt\The sets @{term "H #> a"} and @{term "H"} are finite.\ - apply (simp add: r_coset_subset_G [THEN finite_subset]) -apply (blast intro: finite_subset) -done + assumes "R \ rcosets H" "H \ carrier G" + shows "\f. bij_betw f H R" +proof - + obtain g where g: "g \ carrier G" "R = H #> g" + using assms(1) unfolding RCOSETS_def by blast + + let ?f = "\h. h \ g" + have "\r. r \ R \ \h \ H. ?f h = r" + proof - + fix r assume "r \ R" + then obtain h where "h \ H" "r = h \ g" + using g unfolding r_coset_def by blast + thus "\h \ H. ?f h = r" by blast + qed + hence "R \ ?f ` H" by blast + moreover have "?f ` H \ R" + using g unfolding r_coset_def by blast + ultimately show ?thesis using inj_on_g unfolding bij_betw_def + using assms(2) g(1) by auto +qed + +corollary (in group) card_rcosets_equal: + assumes "R \ rcosets H" "H \ carrier G" + shows "card H = card R" + using card_cosets_equal assms bij_betw_same_card by blast + +corollary (in group) rcosets_finite: + assumes "R \ rcosets H" "H \ carrier G" "finite H" + shows "finite R" + using card_cosets_equal assms bij_betw_finite is_group by blast + +(* ************************************************************************** *) lemma (in group) rcosets_subset_PowG: "subgroup H G \ rcosets H \ Pow(carrier G)" -apply (simp add: RCOSETS_def) -apply (blast dest: r_coset_subset_G subgroup.subset) -done + using rcosets_part_G by auto - -theorem (in group) lagrange: +proposition (in group) lagrange_finite: "\finite(carrier G); subgroup H G\ \ card(rcosets H) * card(H) = order(G)" apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric]) @@ -822,10 +826,42 @@ apply (rule card_partition) apply (simp add: rcosets_subset_PowG [THEN finite_subset]) apply (simp add: rcosets_part_G) - apply (simp add: card_cosets_equal subgroup.subset) + apply (simp add: card_rcosets_equal subgroup_imp_subset) apply (simp add: rcos_disjoint) done +theorem (in group) lagrange: + assumes "subgroup H G" + shows "card (rcosets H) * card H = order G" +proof (cases "finite (carrier G)") + case True thus ?thesis using lagrange_finite assms by simp +next + case False note inf_G = this + thus ?thesis + proof (cases "finite H") + case False thus ?thesis using inf_G by (simp add: order_def) + next + case True note finite_H = this + have "infinite (rcosets H)" + proof (rule ccontr) + assume "\ infinite (rcosets H)" + hence finite_rcos: "finite (rcosets H)" by simp + hence "card (\(rcosets H)) = (\R\(rcosets H). card R)" + using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)] + rcosets_finite[where ?H = H] by (simp add: assms subgroup_imp_subset) + hence "order G = (\R\(rcosets H). card R)" + by (simp add: assms order_def rcosets_part_G) + hence "order G = (\R\(rcosets H). card H)" + using card_rcosets_equal by (simp add: assms subgroup_imp_subset) + hence "order G = (card H) * (card (rcosets H))" by simp + hence "order G \ 0" using finite_rcos finite_H assms ex_in_conv + rcosets_part_G subgroup.one_closed by fastforce + thus False using inf_G order_gt_0_iff_finite by blast + qed + thus ?thesis using inf_G by (simp add: order_def) + qed +qed + subsection \Quotient Groups: Factorization of a Group\ @@ -845,7 +881,7 @@ lemma (in normal) rcosets_assoc: "\M1 \ rcosets H; M2 \ rcosets H; M3 \ rcosets H\ \ M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)" -by (auto simp add: RCOSETS_def rcos_sum m_assoc) + by (simp add: group.set_mult_assoc is_group rcosets_carrier) lemma (in subgroup) subgroup_in_rcosets: assumes "group G" @@ -1016,10 +1052,111 @@ text\If @{term h} is a homomorphism from @{term G} onto @{term H}, then the quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\ -theorem (in group_hom) FactGroup_iso: +theorem (in group_hom) FactGroup_iso_set: "h ` carrier G = carrier H - \ (\X. the_elem (h`X)) \ (G Mod (kernel G H h)) \ H" + \ (\X. the_elem (h`X)) \ iso (G Mod (kernel G H h)) H" by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def FactGroup_onto) +corollary (in group_hom) FactGroup_iso : + "h ` carrier G = carrier H + \ (G Mod (kernel G H h))\ H" + using FactGroup_iso_set unfolding is_iso_def by auto + + +(* Next two lemmas contributed by Paulo Emílio de Vilhena. *) + +lemma (in group_hom) trivial_hom_iff: + "(h ` (carrier G) = { \\<^bsub>H\<^esub> }) = (kernel G H h = carrier G)" + unfolding kernel_def using one_closed by force + +lemma (in group_hom) trivial_ker_imp_inj: + assumes "kernel G H h = { \ }" + shows "inj_on h (carrier G)" +proof (rule inj_onI) + fix g1 g2 assume A: "g1 \ carrier G" "g2 \ carrier G" "h g1 = h g2" + hence "h (g1 \ (inv g2)) = \\<^bsub>H\<^esub>" by simp + hence "g1 \ (inv g2) = \" + using A assms unfolding kernel_def by blast + thus "g1 = g2" + using A G.inv_equality G.inv_inv by blast +qed + + +(* Next subsection contributed by Martin Baillon. *) + +subsection \Theorems about Factor Groups and Direct product\ + + +lemma (in group) DirProd_normal : + assumes "group K" + and "H \ G" + and "N \ K" + shows "H \ N \ G \\ K" +proof (intro group.normal_invI[OF DirProd_group[OF group_axioms assms(1)]]) + show sub : "subgroup (H \ N) (G \\ K)" + using DirProd_subgroups[OF group_axioms normal_imp_subgroup[OF assms(2)]assms(1) + normal_imp_subgroup[OF assms(3)]]. + show "\x h. x \ carrier (G\\K) \ h \ H\N \ x \\<^bsub>G\\K\<^esub> h \\<^bsub>G\\K\<^esub> inv\<^bsub>G\\K\<^esub> x \ H\N" + proof- + fix x h assume xGK : "x \ carrier (G \\ K)" and hHN : " h \ H \ N" + hence hGK : "h \ carrier (G \\ K)" using subgroup_imp_subset[OF sub] by auto + from xGK obtain x1 x2 where x1x2 :"x1 \ carrier G" "x2 \ carrier K" "x = (x1,x2)" + unfolding DirProd_def by fastforce + from hHN obtain h1 h2 where h1h2 : "h1 \ H" "h2 \ N" "h = (h1,h2)" + unfolding DirProd_def by fastforce + hence h1h2GK : "h1 \ carrier G" "h2 \ carrier K" + using normal_imp_subgroup subgroup_imp_subset assms apply blast+. + have "inv\<^bsub>G \\ K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)" + using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto + hence "x \\<^bsub>G \\ K\<^esub> h \\<^bsub>G \\ K\<^esub> inv\<^bsub>G \\ K\<^esub> x = (x1 \ h1 \ inv x1,x2 \\<^bsub>K\<^esub> h2 \\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)" + using h1h2 x1x2 h1h2GK by auto + moreover have "x1 \ h1 \ inv x1 \ H" "x2 \\<^bsub>K\<^esub> h2 \\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2 \ N" + using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto. + hence "(x1 \ h1 \ inv x1, x2 \\<^bsub>K\<^esub> h2 \\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)\ H \ N" by auto + ultimately show " x \\<^bsub>G \\ K\<^esub> h \\<^bsub>G \\ K\<^esub> inv\<^bsub>G \\ K\<^esub> x \ H \ N" by auto + qed +qed + +lemma (in group) FactGroup_DirProd_multiplication_iso_set : + assumes "group K" + and "H \ G" + and "N \ K" + shows "(\ (X, Y). X \ Y) \ iso ((G Mod H) \\ (K Mod N)) (G \\ K Mod H \ N)" + +proof- + have R :"(\(X, Y). X \ Y) \ carrier (G Mod H) \ carrier (K Mod N) \ carrier (G \\ K Mod H \ N)" + unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast + moreover have "(\x\carrier (G Mod H). \y\carrier (K Mod N). \xa\carrier (G Mod H). + \ya\carrier (K Mod N). (x <#> xa) \ (y <#>\<^bsub>K\<^esub> ya) = x \ y <#>\<^bsub>G \\ K\<^esub> xa \ ya)" + unfolding set_mult_def apply auto apply blast+. + moreover have "(\x\carrier (G Mod H). \y\carrier (K Mod N). \xa\carrier (G Mod H). + \ya\carrier (K Mod N). x \ y = xa \ ya \ x = xa \ y = ya)" + unfolding FactGroup_def using times_eq_iff subgroup.rcosets_not_empty + by (metis assms(2) assms(3) normal_def partial_object.select_convs(1)) + moreover have "(\(X, Y). X \ Y) ` (carrier (G Mod H) \ carrier (K Mod N)) = + carrier (G \\ K Mod H \ N)" + unfolding image_def apply auto using R apply force + unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def apply auto apply force. + ultimately show ?thesis + unfolding iso_def hom_def bij_betw_def inj_on_def by simp +qed + +corollary (in group) FactGroup_DirProd_multiplication_iso_1 : + assumes "group K" + and "H \ G" + and "N \ K" + shows " ((G Mod H) \\ (K Mod N)) \ (G \\ K Mod H \ N)" + unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto + +corollary (in group) FactGroup_DirProd_multiplication_iso_2 : + assumes "group K" + and "H \ G" + and "N \ K" + shows "(G \\ K Mod H \ N) \ ((G Mod H) \\ (K Mod N))" + using FactGroup_DirProd_multiplication_iso_1 group.iso_sym assms + DirProd_group[OF normal.factorgroup_is_group normal.factorgroup_is_group] + by blast + + end diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Tue Jun 12 16:21:52 2018 +0200 +++ b/src/HOL/Algebra/Group.thy Tue Jun 12 16:09:12 2018 +0100 @@ -75,6 +75,12 @@ "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" @@ -86,7 +92,7 @@ finally show ?thesis . qed -lemma (in monoid) Units_m_closed [intro, simp]: +lemma (in monoid) Units_m_closed [simp, intro]: assumes x: "x \ Units G" and y: "y \ Units G" shows "x \ y \ Units G" proof - @@ -215,10 +221,23 @@ "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 + (* Jacobson defines submonoid here. *) (* Jacobson defines the order of a monoid here. *) @@ -416,6 +435,57 @@ by (auto simp add: int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult ) qed +lemma (in group) nat_pow_inv: + "x \ carrier G \ (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))" + using inv_mult_group[OF Suc.prems nat_pow_closed[OF Suc.prems, of i]] by simp + also have " ... = inv (x [^] (Suc i))" + using Suc.prems nat_pow_Suc2 by auto + finally show ?case . +qed + +lemma (in group) int_pow_inv: + "x \ carrier G \ (inv x) [^] (i :: int) = inv (x [^] i)" + by (simp add: nat_pow_inv int_pow_def2) + +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 + by (simp add: mult_less_0_iff nat_mult_distrib) + next + assume m_lt: "\ m \ 0" thus ?thesis + using n_ge int_pow_def2 nat_pow_pow[OF assms, of "nat n" "nat (- m)"] + by (smt assms group.int_pow_neg is_group mult_minus_right nat_mult_distrib split_mult_neg_le) + qed +next + assume n_lt: "\ n \ 0" thus ?thesis + proof (cases) + assume m_ge: "m \ 0" thus ?thesis + using n_lt nat_pow_pow[OF assms, of "nat (- n)" "nat m"] + nat_pow_inv[of "x [^] nat (- n)" "nat m"] int_pow_def2 + by (smt assms group.int_pow_closed group.int_pow_neg is_group mult_minus_right + mult_nonpos_nonpos nat_mult_distrib_neg) + next + assume m_lt: "\ m \ 0" thus ?thesis + using n_lt nat_pow_pow[OF assms, of "nat (- n)" "nat (- m)"] + nat_pow_inv[of "x [^] nat (- n)" "nat (- m)"] int_pow_def2 + by (smt assms inv_inv mult_nonpos_nonpos nat_mult_distrib_neg nat_pow_closed) + 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) @@ -426,6 +496,70 @@ lemma (in group) inj_on_cmult: "c \ carrier G \ inj_on (\x. c \ x) (carrier G)" by(simp add: inj_on_def) +(*Following subsection contributed by Martin Baillon*) +subsection \Submonoids\ + +locale submonoid = + 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: + "submonoid H G" by (rule submonoid_axioms) + +lemma (in submonoid) mem_carrier [simp]: + "x \ H \ x \ carrier G" + using subset by blast + +lemma submonoid_imp_subset: + "submonoid H G \ H \ carrier G" + by (rule submonoid.subset) + +lemma (in submonoid) submonoid_is_monoid [intro]: + 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 (in monoid) submonoidE: + assumes "submonoid H G" + shows "H \ carrier G" + and "H \ {}" + and "\a b. \a \ H; b \ H\ \ a \ b \ H" + using assms submonoid_imp_subset apply blast + using assms submonoid_def apply auto[1] + by (simp add: assms submonoid.m_closed)+ + +lemma submonoid_nonempty: + "~ submonoid {} G" + by (blast dest: submonoid.one_closed) + +lemma (in submonoid) finite_monoid_imp_card_positive: + "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 : + 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 + subsection \Subgroups\ locale subgroup = @@ -460,6 +594,40 @@ done qed +lemma (in group) m_inv_consistent: + assumes "subgroup H G" "x \ H" + shows "inv x = inv\<^bsub>(G \ carrier := H \)\<^esub> x" + unfolding m_inv_def apply auto + using subgroup.m_inv_closed[OF assms] inv_equality + by (metis (no_types, hide_lams) assms subgroup.mem_carrier) + +lemma (in group) int_pow_consistent: (* by Paulo *) + 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 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" + using group.int_pow_def2[OF subgroup.subgroup_is_group[OF assms(1) is_group]] ge by auto + finally show ?thesis . +next + assume "\ n \ 0" hence lt: "n < 0" by simp + hence "x [^] n = inv (x [^] (nat (- n)))" + using int_pow_def2 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" + using group.int_pow_def2[OF subgroup.subgroup_is_group[OF assms(1) is_group]] lt by auto + finally show ?thesis . +qed + text \ Since @{term H} is nonempty, it contains some element @{term x}. Since it is closed under inverse, it contains \inv x\. Since @@ -482,6 +650,17 @@ 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 subgroup_imp_subset apply blast + using assms subgroup_def apply auto[1] + by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)+ + declare monoid.one_closed [iff] group.inv_closed [simp] monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp] @@ -498,12 +677,44 @@ with subgroup_nonempty show ?thesis by contradiction qed +(*Following 3 lemmas contributed by Martin Baillon*) + +lemma (in subgroup) subgroup_is_submonoid : + "submonoid H G" + by (simp add: submonoid.intro subset) + +lemma (in group) submonoid_subgroupI : + 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: + 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 (smt 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 + (* lemma (in monoid) Units_subgroup: "subgroup (Units G) G" *) - subsection \Direct Products\ definition @@ -548,6 +759,10 @@ "(g, h) \\<^bsub>(G \\ H)\<^esub> (g', h') = (g \\<^bsub>G\<^esub> g', h \\<^bsub>H\<^esub> h')" by (simp add: DirProd_def) +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" @@ -561,6 +776,22 @@ 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_imp_subset assms apply 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 apply simp. + ultimately show "Group.group ((G \\ K)\carrier := H \ I\)" by simp +qed subsection \Homomorphisms and Isomorphisms\ @@ -575,31 +806,203 @@ by (fastforce simp add: hom_def compose_def) definition - iso :: "_ => _ => ('a => 'b) set" (infixr "\" 60) - where "G \ H = {h. h \ hom G H \ bij_betw h (carrier G) (carrier H)}" + 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 \ {})" -lemma iso_refl: "(\x. x) \ G \ G" -by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_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 (in group) iso_sym: - "h \ G \ H \ inv_into (carrier G) h \ H \ G" +corollary iso_refl : "G \ G" + using iso_set_refl unfolding is_iso_def by auto + +lemma (in group) iso_set_sym: + "h \ iso G H \ inv_into (carrier G) h \ (iso H G)" apply (simp add: iso_def bij_betw_inv_into) apply (subgoal_tac "inv_into (carrier G) h \ carrier H \ carrier G") prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into]) apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def) done -lemma (in group) iso_trans: - "[|h \ G \ H; i \ H \ I|] ==> (compose (carrier G) i h) \ G \ I" +corollary (in group) iso_sym : +"G \ H \ H \ G" + using iso_set_sym unfolding is_iso_def by auto + +lemma (in group) iso_set_trans: + "[|h \ iso G H; i \ iso H I|] ==> (compose (carrier G) i h) \ iso G I" by (auto simp add: iso_def hom_compose bij_betw_compose) -lemma DirProd_commute_iso: - shows "(\(x,y). (y,x)) \ (G \\ H) \ (H \\ G)" +corollary (in group) iso_trans : +"\G \ H ; H \ I\ \ G \ I" + using iso_set_trans unfolding is_iso_def by blast + +(* Next four lemmas contributed by Paulo Emílio de Vilhena. *) + +lemma (in monoid) hom_imp_img_monoid: + 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: + 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: + assumes "G \ H" and "monoid H" + shows "group H" +proof - + obtain \ where phi: "\ \ iso G H" "inv_into (carrier G) \ \ iso H G" + using iso_set_sym assms unfolding is_iso_def by blast + define \ where psi_def: "\ = inv_into (carrier G) \" + + from 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 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, hide_lams) 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: + 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 + +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 DirProd_assoc_iso: - shows "(\(x,y,z). (x,(y,z))) \ (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 text\Basis for homomorphism proofs: we assume two groups @{term G} and @@ -655,6 +1058,56 @@ "x \ carrier G \ (([^]) x) \ hom \ carrier = UNIV, mult = (+), one = 0::int \ G " unfolding hom_def by (simp add: int_pow_mult) +(* Next six lemmas contributed by Paulo Emílio de Vilhena. *) + +lemma (in group_hom) img_is_subgroup: "subgroup (h ` (carrier G)) H" + apply (rule subgroupI) + apply (auto simp add: image_subsetI) + apply (metis (no_types, hide_lams) G.inv_closed hom_inv image_iff) + apply (smt G.monoid_axioms hom_mult image_iff monoid.m_closed) + done + +lemma (in group_hom) subgroup_img_is_subgroup: + 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 group_hom) induced_group_hom: + 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 + +lemma (in group) canonical_inj_is_hom: + 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_imp_subset[OF assms] by auto + +lemma (in group_hom) nat_pow_hom: + "x \ carrier G \ h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n" + by (induction n) auto + +lemma (in group_hom) int_pow_hom: + "x \ carrier G \ h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n" + using int_pow_def2 nat_pow_hom by (simp add: G.int_pow_def2) + subsection \Commutative Structures\ @@ -716,6 +1169,18 @@ (x \ y) [^] (n::nat) = x [^] n \ y [^] n" by (induct n) (simp, simp add: m_ac) +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\) + \ x \\<^bsub>G\carrier := H\\<^esub> y = y \\<^bsub>G\carrier := H\\<^esub> x" apply simp + using assms comm_monoid_axioms_def submonoid.mem_carrier + by (metis m_comm) +qed + locale comm_group = comm_monoid + group lemma (in group) group_comm_groupI: @@ -739,10 +1204,83 @@ 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 = \" + apply (simp_all add: group.axioms assms comm_group.axioms comm_monoid.m_comm comm_monoid.m_ac(1)) + by (simp_all add: Group.group.axioms(1) assms comm_group.axioms(2) monoid.m_closed group.r_inv_ex) + lemma (in comm_group) inv_mult: "[| x \ carrier G; y \ carrier G |] ==> inv (x \ y) = inv x \ inv y" by (simp add: m_ac inv_mult_group) +(* Next three lemmas contributed by Paulo Emílio de Vilhena. *) + +lemma (in comm_monoid) hom_imp_img_comm_monoid: + assumes "h \ hom G H" + shows "comm_monoid (H \ carrier := h ` (carrier G), one := h \\<^bsub>G\<^esub> \)" (is "comm_monoid ?h_img") +proof (rule monoid.monoid_comm_monoidI) + show "monoid ?h_img" + using hom_imp_img_monoid[OF assms] . +next + fix x y assume "x \ carrier ?h_img" "y \ carrier ?h_img" + then obtain g1 g2 + where g1: "g1 \ carrier G" "x = h g1" + and g2: "g2 \ carrier G" "y = h g2" + by auto + have "x \\<^bsub>(?h_img)\<^esub> y = h (g1 \ g2)" + using g1 g2 assms unfolding hom_def by auto + also have " ... = h (g2 \ g1)" + using m_comm[OF g1(1) g2(1)] by simp + also have " ... = y \\<^bsub>(?h_img)\<^esub> x" + using g1 g2 assms unfolding hom_def by auto + finally show "x \\<^bsub>(?h_img)\<^esub> y = y \\<^bsub>(?h_img)\<^esub> x" . +qed + +lemma (in comm_group) iso_imp_img_comm_group: + assumes "h \ iso G H" + shows "comm_group (H \ one := h \\<^bsub>G\<^esub> \)" +proof - + let ?h_img = "H \ carrier := h ` (carrier G), one := h \ \" + have "comm_monoid ?h_img" + using hom_imp_img_comm_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 have "comm_monoid (H \ one := h \\<^bsub>G\<^esub> \)" + by simp + thus ?thesis + unfolding comm_group_def using iso_imp_img_group[OF assms] by simp +qed + +lemma (in comm_group) iso_imp_comm_group: + assumes "G \ H" "monoid H" + shows "comm_group H" +proof - + obtain h where h: "h \ iso G H" + using assms(1) unfolding is_iso_def by auto + hence comm_gr: "comm_group (H \ one := h \ \)" + using iso_imp_img_comm_group[of h H] by simp + hence "\x. x \ carrier H \ h \ \\<^bsub>H\<^esub> x = x" + using monoid.l_one[of "H \ one := h \ \"] unfolding comm_group_def comm_monoid_def by simp + moreover have "h \ \ carrier H" + using h one_closed unfolding iso_def hom_def by auto + ultimately have "h \ = \\<^bsub>H\<^esub>" + using monoid.one_unique[OF assms(2), of "h \"] by simp + hence "H = H \ one := h \ \" + by simp + thus ?thesis + using comm_gr by simp +qed + + subsection \The Lattice of Subgroups of a Group\ @@ -773,6 +1311,10 @@ apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+) done +lemma (in group) subgroup_mult_equality: + "\ subgroup H G; h1 \ H; h2 \ H \ \ h1 \\<^bsub>G \ carrier := H \\<^esub> h2 = h1 \ h2" + unfolding subgroup_def by simp + theorem (in group) subgroups_Inter: assumes subgr: "(\H. H \ A \ subgroup H G)" and not_empty: "A \ {}" @@ -793,6 +1335,11 @@ show "x \ y \ \A" by blast qed +lemma (in group) subgroups_Inter_pair : + assumes "subgroup I G" + and "subgroup J G" + shows "subgroup (I\J) G" using subgroups_Inter[ where ?A = "{I,J}"] assms by auto + theorem (in group) subgroups_complete_lattice: "complete_lattice \carrier = {H. subgroup H G}, eq = (=), le = (\)\" (is "complete_lattice ?L") diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/Group_Action.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Group_Action.thy Tue Jun 12 16:09:12 2018 +0100 @@ -0,0 +1,927 @@ +(* ************************************************************************** *) +(* Title: Group_Action.thy *) +(* Author: Paulo Emílio de Vilhena *) +(* ************************************************************************** *) + +theory Group_Action +imports Bij Coset Congruence + +begin + +section \Group Actions\ + +locale group_action = + fixes G (structure) and E and \ + assumes group_hom: "group_hom G (BijGroup E) \" + +definition + orbit :: "[_, 'a \ 'b \ 'b, 'b] \ 'b set" + where "orbit G \ x = {(\ g) x | g. g \ carrier G}" + +definition + orbits :: "[_, 'b set, 'a \ 'b \ 'b] \ ('b set) set" + where "orbits G E \ = {orbit G \ x | x. x \ E}" + +definition + stabilizer :: "[_, 'a \ 'b \ 'b, 'b] \ 'a set" + where "stabilizer G \ x = {g \ carrier G. (\ g) x = x}" + +definition + invariants :: "['b set, 'a \ 'b \ 'b, 'a] \ 'b set" + where "invariants E \ g = {x \ E. (\ g) x = x}" + +definition + normalizer :: "[_, 'a set] \ 'a set" + where "normalizer G H = + stabilizer G (\g. \H \ {H. H \ carrier G}. g <#\<^bsub>G\<^esub> H #>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> g)) H" + +locale faithful_action = group_action + + assumes faithful: "inj_on \ (carrier G)" + +locale transitive_action = group_action + + assumes unique_orbit: "\ x \ E; y \ E \ \ \g \ carrier G. (\ g) x = y" + + + +subsection \Prelimineries\ + +text \Some simple lemmas to make group action's properties more explicit\ + +lemma (in group_action) id_eq_one: "(\x \ E. x) = \ \" + by (metis BijGroup_def group_hom group_hom.hom_one select_convs(2)) + +lemma (in group_action) bij_prop0: + "\ g. g \ carrier G \ (\ g) \ Bij E" + by (metis BijGroup_def group_hom group_hom.hom_closed partial_object.select_convs(1)) + +lemma (in group_action) surj_prop: + "\ g. g \ carrier G \ (\ g) ` E = E" + using bij_prop0 by (simp add: Bij_def bij_betw_def) + +lemma (in group_action) inj_prop: + "\ g. g \ carrier G \ inj_on (\ g) E" + using bij_prop0 by (simp add: Bij_def bij_betw_def) + +lemma (in group_action) bij_prop1: + "\ g y. \ g \ carrier G; y \ E \ \ \!x \ E. (\ g) x = y" +proof - + fix g y assume "g \ carrier G" "y \ E" + hence "\x \ E. (\ g) x = y" + using surj_prop by force + moreover have "\ x1 x2. \ x1 \ E; x2 \ E \ \ (\ g) x1 = (\ g) x2 \ x1 = x2" + using inj_prop by (meson \g \ carrier G\ inj_on_eq_iff) + ultimately show "\!x \ E. (\ g) x = y" + by blast +qed + +lemma (in group_action) composition_rule: + assumes "x \ E" "g1 \ carrier G" "g2 \ carrier G" + shows "\ (g1 \ g2) x = (\ g1) (\ g2 x)" +proof - + have "\ (g1 \ g2) x = ((\ g1) \\<^bsub>BijGroup E\<^esub> (\ g2)) x" + using assms(2) assms(3) group_hom group_hom.hom_mult by fastforce + also have " ... = (compose E (\ g1) (\ g2)) x" + unfolding BijGroup_def by (simp add: assms bij_prop0) + finally show "\ (g1 \ g2) x = (\ g1) (\ g2 x)" + by (simp add: assms(1) compose_eq) +qed + +lemma (in group_action) element_image: + assumes "g \ carrier G" and "x \ E" and "(\ g) x = y" + shows "y \ E" + using surj_prop assms by blast + + + +subsection \Orbits\ + +text\We prove here that orbits form an equivalence relation\ + +lemma (in group_action) orbit_sym_aux: + assumes "g \ carrier G" + and "x \ E" + and "(\ g) x = y" + shows "(\ (inv g)) y = x" +proof - + interpret group G + using group_hom group_hom.axioms(1) by auto + have "y \ E" + using element_image assms by simp + have "inv g \ carrier G" + by (simp add: assms(1)) + + have "(\ (inv g)) y = (\ (inv g)) ((\ g) x)" + using assms(3) by simp + also have " ... = compose E (\ (inv g)) (\ g) x" + by (simp add: assms(2) compose_eq) + also have " ... = ((\ (inv g)) \\<^bsub>BijGroup E\<^esub> (\ g)) x" + by (simp add: BijGroup_def assms(1) bij_prop0) + also have " ... = (\ ((inv g) \ g)) x" + by (metis \inv g \ carrier G\ assms(1) group_hom group_hom.hom_mult) + finally show "(\ (inv g)) y = x" + by (metis assms(1) assms(2) id_eq_one l_inv restrict_apply) +qed + +lemma (in group_action) orbit_refl: + "x \ E \ x \ orbit G \ x" +proof - + assume "x \ E" hence "(\ \) x = x" + using id_eq_one by (metis restrict_apply') + thus "x \ orbit G \ x" unfolding orbit_def + using group.is_monoid group_hom group_hom.axioms(1) by force +qed + +lemma (in group_action) orbit_sym: + assumes "x \ E" and "y \ E" and "y \ orbit G \ x" + shows "x \ orbit G \ y" +proof - + have "\ g \ carrier G. (\ g) x = y" + by (smt assms(3) mem_Collect_eq orbit_def) + then obtain g where g: "g \ carrier G \ (\ g) x = y" by blast + hence "(\ (inv g)) y = x" + using orbit_sym_aux by (simp add: assms(1)) + thus ?thesis + using g group_hom group_hom.axioms(1) orbit_def by fastforce +qed + +lemma (in group_action) orbit_trans: + assumes "x \ E" "y \ E" "z \ E" + and "y \ orbit G \ x" "z \ orbit G \ y" + shows "z \ orbit G \ x" +proof - + interpret group G + using group_hom group_hom.axioms(1) by auto + + have "\ g1 \ carrier G. (\ g1) x = y" + by (smt assms mem_Collect_eq orbit_def) + then obtain g1 where g1: "g1 \ carrier G \ (\ g1) x = y" by blast + + have "\ g2 \ carrier G. (\ g2) y = z" + by (smt assms mem_Collect_eq orbit_def) + then obtain g2 where g2: "g2 \ carrier G \ (\ g2) y = z" by blast + + have "(\ (g2 \ g1)) x = ((\ g2) \\<^bsub>BijGroup E\<^esub> (\ g1)) x" + using g1 g2 group_hom group_hom.hom_mult by fastforce + also have " ... = (\ g2) ((\ g1) x)" + using composition_rule assms(1) calculation g1 g2 by auto + finally have "(\ (g2 \ g1)) x = z" + by (simp add: g1 g2) + thus ?thesis + using g1 g2 orbit_def by force +qed + +lemma (in group_action) orbits_as_classes: + "classes\<^bsub>\ carrier = E, eq = \x. \y. y \ orbit G \ x \\<^esub> = orbits G E \" + unfolding eq_classes_def eq_class_of_def orbits_def apply simp +proof - + have "\x. x \ E \ {y \ E. y \ orbit G \ x} = orbit G \ x" + by (smt Collect_cong element_image mem_Collect_eq orbit_def) + thus "{{y \ E. y \ orbit G \ x} |x. x \ E} = {orbit G \ x |x. x \ E}" by blast +qed + +theorem (in group_action) orbit_partition: + "partition E (orbits G E \)" +proof - + have "equivalence \ carrier = E, eq = \x. \y. y \ orbit G \ x \" + unfolding equivalence_def apply simp + using orbit_refl orbit_sym orbit_trans by blast + thus ?thesis using equivalence.partition_from_equivalence orbits_as_classes by fastforce +qed + +corollary (in group_action) orbits_coverture: + "\ (orbits G E \) = E" + using partition.partition_coverture[OF orbit_partition] by simp + +corollary (in group_action) disjoint_union: + assumes "orb1 \ (orbits G E \)" "orb2 \ (orbits G E \)" + shows "(orb1 = orb2) \ (orb1 \ orb2) = {}" + using partition.disjoint_union[OF orbit_partition] assms by auto + +corollary (in group_action) disjoint_sum: + assumes "finite E" + shows "(\orb\(orbits G E \). \x\orb. f x) = (\x\E. f x)" + using partition.disjoint_sum[OF orbit_partition] assms by auto + + +subsubsection \Transitive Actions\ + +text \Transitive actions have only one orbit\ + +lemma (in transitive_action) all_equivalent: + "\ x \ E; y \ E \ \ x .=\<^bsub>\carrier = E, eq = \x y. y \ orbit G \ x\\<^esub> y" +proof - + assume "x \ E" "y \ E" + hence "\ g \ carrier G. (\ g) x = y" + using unique_orbit by blast + hence "y \ orbit G \ x" + using orbit_def by fastforce + thus "x .=\<^bsub>\carrier = E, eq = \x y. y \ orbit G \ x\\<^esub> y" by simp +qed + +proposition (in transitive_action) one_orbit: + assumes "E \ {}" + shows "card (orbits G E \) = 1" +proof - + have "orbits G E \ \ {}" + using assms orbits_coverture by auto + moreover have "\ orb1 orb2. \ orb1 \ (orbits G E \); orb2 \ (orbits G E \) \ \ orb1 = orb2" + proof - + fix orb1 orb2 assume orb1: "orb1 \ (orbits G E \)" + and orb2: "orb2 \ (orbits G E \)" + then obtain x y where x: "orb1 = orbit G \ x" and x_E: "x \ E" + and y: "orb2 = orbit G \ y" and y_E: "y \ E" + unfolding orbits_def by blast + hence "x \ orbit G \ y" using all_equivalent by auto + hence "orb1 \ orb2 \ {}" using x y x_E orbit_refl by auto + thus "orb1 = orb2" using disjoint_union[of orb1 orb2] orb1 orb2 by auto + qed + ultimately show "card (orbits G E \) = 1" + by (meson is_singletonI' is_singleton_altdef) +qed + + + +subsection \Stabilizers\ + +text \We show that stabilizers are subgroups from the acting group\ + +lemma (in group_action) stabilizer_subset: + "stabilizer G \ x \ carrier G" + by (metis (no_types, lifting) mem_Collect_eq stabilizer_def subsetI) + +lemma (in group_action) stabilizer_m_closed: + assumes "x \ E" "g1 \ (stabilizer G \ x)" "g2 \ (stabilizer G \ x)" + shows "(g1 \ g2) \ (stabilizer G \ x)" +proof - + interpret group G + using group_hom group_hom.axioms(1) by auto + + have "\ g1 x = x" + using assms stabilizer_def by fastforce + moreover have "\ g2 x = x" + using assms stabilizer_def by fastforce + moreover have g1: "g1 \ carrier G" + by (meson assms contra_subsetD stabilizer_subset) + moreover have g2: "g2 \ carrier G" + by (meson assms contra_subsetD stabilizer_subset) + ultimately have "\ (g1 \ g2) x = x" + using composition_rule assms by simp + + thus ?thesis + by (simp add: g1 g2 stabilizer_def) +qed + +lemma (in group_action) stabilizer_one_closed: + assumes "x \ E" + shows "\ \ (stabilizer G \ x)" +proof - + have "\ \ x = x" + by (metis assms id_eq_one restrict_apply') + thus ?thesis + using group_def group_hom group_hom.axioms(1) stabilizer_def by fastforce +qed + +lemma (in group_action) stabilizer_m_inv_closed: + assumes "x \ E" "g \ (stabilizer G \ x)" + shows "(inv g) \ (stabilizer G \ x)" +proof - + interpret group G + using group_hom group_hom.axioms(1) by auto + + have "\ g x = x" + using assms(2) stabilizer_def by fastforce + moreover have g: "g \ carrier G" + using assms(2) stabilizer_subset by blast + moreover have inv_g: "inv g \ carrier G" + by (simp add: g) + ultimately have "\ (inv g) x = x" + using assms(1) orbit_sym_aux by blast + + thus ?thesis by (simp add: inv_g stabilizer_def) +qed + +theorem (in group_action) stabilizer_subgroup: + assumes "x \ E" + shows "subgroup (stabilizer G \ x) G" + unfolding subgroup_def + using stabilizer_subset stabilizer_m_closed stabilizer_one_closed + stabilizer_m_inv_closed assms by simp + + + +subsection \The Orbit-Stabilizer Theorem\ + +text \In this subsection, we prove the Orbit-Stabilizer theorem. + Our approach is to show the existence of a bijection between + "rcosets (stabilizer G \ x)" and "orbit G \ x". Then we use + Lagrange's theorem to find the cardinal of the first set.\ + +subsubsection \Rcosets - Supporting Lemmas\ + +corollary (in group_action) stab_rcosets_not_empty: + assumes "x \ E" "R \ rcosets (stabilizer G \ x)" + shows "R \ {}" + using subgroup.rcosets_not_empty[OF stabilizer_subgroup[OF assms(1)] assms(2)] by simp + +corollary (in group_action) diff_stabilizes: + assumes "x \ E" "R \ rcosets (stabilizer G \ x)" + shows "\g1 g2. \ g1 \ R; g2 \ R \ \ g1 \ (inv g2) \ stabilizer G \ x" + using group.diff_neutralizes[of G "stabilizer G \ x" R] stabilizer_subgroup[OF assms(1)] + assms(2) group_hom group_hom.axioms(1) by blast + + +subsubsection \Bijection Between Rcosets and an Orbit - Definition and Supporting Lemmas\ + +(* This definition could be easier if lcosets were available, and it's indeed a considerable + modification at Coset theory, since we could derive it easily from the definition of rcosets + following the same idea we use here: f: rcosets \ lcosets, s.t. f R = (\g. inv g) ` R + is a bijection. *) + +definition + orb_stab_fun :: "[_, ('a \ 'b \ 'b), 'a set, 'b] \ 'b" + where "orb_stab_fun G \ R x = (\ (inv\<^bsub>G\<^esub> (SOME h. h \ R))) x" + +lemma (in group_action) orbit_stab_fun_is_well_defined0: + assumes "x \ E" "R \ rcosets (stabilizer G \ x)" + shows "\g1 g2. \ g1 \ R; g2 \ R \ \ (\ (inv g1)) x = (\ (inv g2)) x" +proof - + fix g1 g2 assume g1: "g1 \ R" and g2: "g2 \ R" + have R_carr: "R \ carrier G" + using subgroup.rcosets_carrier[OF stabilizer_subgroup[OF assms(1)]] + assms(2) group_hom group_hom.axioms(1) by auto + from R_carr have g1_carr: "g1 \ carrier G" using g1 by blast + from R_carr have g2_carr: "g2 \ carrier G" using g2 by blast + + have "g1 \ (inv g2) \ stabilizer G \ x" + using diff_stabilizes[of x R g1 g2] assms g1 g2 by blast + hence "\ (g1 \ (inv g2)) x = x" + by (simp add: stabilizer_def) + hence "(\ (inv g1)) x = (\ (inv g1)) (\ (g1 \ (inv g2)) x)" by simp + also have " ... = \ ((inv g1) \ (g1 \ (inv g2))) x" + using group_def assms(1) composition_rule g1_carr g2_carr + group_hom group_hom.axioms(1) monoid.m_closed by fastforce + also have " ... = \ (((inv g1) \ g1) \ (inv g2)) x" + using group_def g1_carr g2_carr group_hom group_hom.axioms(1) monoid.m_assoc by fastforce + finally show "(\ (inv g1)) x = (\ (inv g2)) x" + using group_def g1_carr g2_carr group.l_inv group_hom group_hom.axioms(1) by fastforce +qed + +lemma (in group_action) orbit_stab_fun_is_well_defined1: + assumes "x \ E" "R \ rcosets (stabilizer G \ x)" + shows "\g. g \ R \ (\ (inv (SOME h. h \ R))) x = (\ (inv g)) x" + by (meson assms orbit_stab_fun_is_well_defined0 someI_ex) + +lemma (in group_action) orbit_stab_fun_is_inj: + assumes "x \ E" + and "R1 \ rcosets (stabilizer G \ x)" + and "R2 \ rcosets (stabilizer G \ x)" + and "\ (inv (SOME h. h \ R1)) x = \ (inv (SOME h. h \ R2)) x" + shows "R1 = R2" +proof - + have "(\g1. g1 \ R1) \ (\g2. g2 \ R2)" + using assms(1-3) stab_rcosets_not_empty by auto + then obtain g1 g2 where g1: "g1 \ R1" and g2: "g2 \ R2" by blast + hence g12_carr: "g1 \ carrier G \ g2 \ carrier G" + using subgroup.rcosets_carrier assms(1-3) group_hom + group_hom.axioms(1) stabilizer_subgroup by blast + + then obtain r1 r2 where r1: "r1 \ carrier G" "R1 = (stabilizer G \ x) #> r1" + and r2: "r2 \ carrier G" "R2 = (stabilizer G \ x) #> r2" + using assms(1-3) unfolding RCOSETS_def by blast + then obtain s1 s2 where s1: "s1 \ (stabilizer G \ x)" "g1 = s1 \ r1" + and s2: "s2 \ (stabilizer G \ x)" "g2 = s2 \ r2" + using g1 g2 unfolding r_coset_def by blast + + have "\ (inv g1) x = \ (inv (SOME h. h \ R1)) x" + using orbit_stab_fun_is_well_defined1[OF assms(1) assms(2) g1] by simp + also have " ... = \ (inv (SOME h. h \ R2)) x" + using assms(4) by simp + finally have "\ (inv g1) x = \ (inv g2) x" + using orbit_stab_fun_is_well_defined1[OF assms(1) assms(3) g2] by simp + + hence "\ g2 (\ (inv g1) x) = \ g2 (\ (inv g2) x)" by simp + also have " ... = \ (g2 \ (inv g2)) x" + using assms(1) composition_rule g12_carr group_hom group_hom.axioms(1) by fastforce + finally have "\ g2 (\ (inv g1) x) = x" + using g12_carr assms(1) group.r_inv group_hom group_hom.axioms(1) + id_eq_one restrict_apply by metis + hence "\ (g2 \ (inv g1)) x = x" + using assms(1) composition_rule g12_carr group_hom group_hom.axioms(1) by fastforce + hence "g2 \ (inv g1) \ (stabilizer G \ x)" + using g12_carr group.subgroup_self group_hom group_hom.axioms(1) + mem_Collect_eq stabilizer_def subgroup_def by (metis (mono_tags, lifting)) + then obtain s where s: "s \ (stabilizer G \ x)" "s = g2 \ (inv g1)" by blast + + let ?h = "s \ g1" + have "?h = s \ (s1 \ r1)" by (simp add: s1) + hence "?h = (s \ s1) \ r1" + using stabilizer_subgroup[OF assms(1)] group_def group_hom + group_hom.axioms(1) monoid.m_assoc r1 s s1 subgroup.mem_carrier by fastforce + hence inR1: "?h \ (stabilizer G \ x) #> r1" unfolding r_coset_def + using stabilizer_subgroup[OF assms(1)] assms(1) s s1 stabilizer_m_closed by auto + + have "?h = g2" using s stabilizer_subgroup[OF assms(1)] g12_carr group.inv_solve_right + group_hom group_hom.axioms(1) subgroup.mem_carrier by metis + hence inR2: "?h \ (stabilizer G \ x) #> r2" + using g2 r2 by blast + + have "R1 \ R2 \ {}" using inR1 inR2 r1 r2 by blast + thus ?thesis using stabilizer_subgroup group.rcos_disjoint[of G "stabilizer G \ x" R1 R2] + assms group_hom group_hom.axioms(1) by blast +qed + +lemma (in group_action) orbit_stab_fun_is_surj: + assumes "x \ E" "y \ orbit G \ x" + shows "\R \ rcosets (stabilizer G \ x). \ (inv (SOME h. h \ R)) x = y" +proof - + have "\g \ carrier G. (\ g) x = y" + using assms(2) unfolding orbit_def by blast + then obtain g where g: "g \ carrier G \ (\ g) x = y" by blast + + let ?R = "(stabilizer G \ x) #> (inv g)" + have R: "?R \ rcosets (stabilizer G \ x)" + unfolding RCOSETS_def using g group_hom group_hom.axioms(1) by fastforce + moreover have "\ \ (inv g) \ ?R" + unfolding r_coset_def using assms(1) stabilizer_one_closed by auto + ultimately have "\ (inv (SOME h. h \ ?R)) x = \ (inv (\ \ (inv g))) x" + using orbit_stab_fun_is_well_defined1[OF assms(1)] by simp + also have " ... = (\ g) x" + using group_def g group_hom group_hom.axioms(1) monoid.l_one by fastforce + finally have "\ (inv (SOME h. h \ ?R)) x = y" + using g by simp + thus ?thesis using R by blast +qed + +proposition (in group_action) orbit_stab_fun_is_bij: + assumes "x \ E" + shows "bij_betw (\R. (\ (inv (SOME h. h \ R))) x) (rcosets (stabilizer G \ x)) (orbit G \ x)" + unfolding bij_betw_def +proof + show "inj_on (\R. \ (inv (SOME h. h \ R)) x) (rcosets stabilizer G \ x)" + using orbit_stab_fun_is_inj[OF assms(1)] by (simp add: inj_on_def) +next + have "\R. R \ (rcosets stabilizer G \ x) \ \ (inv (SOME h. h \ R)) x \ orbit G \ x " + proof - + fix R assume R: "R \ (rcosets stabilizer G \ x)" + then obtain g where g: "g \ R" + using assms stab_rcosets_not_empty by auto + hence "\ (inv (SOME h. h \ R)) x = \ (inv g) x" + using R assms orbit_stab_fun_is_well_defined1 by blast + thus "\ (inv (SOME h. h \ R)) x \ orbit G \ x" unfolding orbit_def + using subgroup.rcosets_carrier group_hom group_hom.axioms(1) + g R assms stabilizer_subgroup by fastforce + qed + moreover have "orbit G \ x \ (\R. \ (inv (SOME h. h \ R)) x) ` (rcosets stabilizer G \ x)" + using assms orbit_stab_fun_is_surj by fastforce + ultimately show "(\R. \ (inv (SOME h. h \ R)) x) ` (rcosets stabilizer G \ x) = orbit G \ x " + using assms set_eq_subset by blast +qed + + +subsubsection \The Theorem\ + +theorem (in group_action) orbit_stabilizer_theorem: + assumes "x \ E" + shows "card (orbit G \ x) * card (stabilizer G \ x) = order G" +proof - + have "card (rcosets stabilizer G \ x) = card (orbit G \ x)" + using orbit_stab_fun_is_bij[OF assms(1)] bij_betw_same_card by blast + moreover have "card (rcosets stabilizer G \ x) * card (stabilizer G \ x) = order G" + using stabilizer_subgroup assms group.lagrange group_hom group_hom.axioms(1) by blast + ultimately show ?thesis by auto +qed + + + +subsection \The Burnside's Lemma\ + +subsubsection \Sums and Cardinals\ + +lemma card_as_sums: + assumes "A = {x \ B. P x}" "finite B" + shows "card A = (\x\B. (if P x then 1 else 0))" +proof - + have "A \ B" using assms(1) by blast + have "card A = (\x\A. 1)" by simp + also have " ... = (\x\A. (if P x then 1 else 0))" + by (simp add: assms(1)) + also have " ... = (\x\A. (if P x then 1 else 0)) + (\x\(B - A). (if P x then 1 else 0))" + using assms(1) by auto + finally show "card A = (\x\B. (if P x then 1 else 0))" + using \A \ B\ add.commute assms(2) sum.subset_diff by metis +qed + +lemma sum_invertion: + "\ finite A; finite B \ \ (\x\A. \y\B. f x y) = (\y\B. \x\A. f x y)" +proof (induct set: finite) + case empty thus ?case by simp +next + case (insert x A') + have "(\x\insert x A'. \y\B. f x y) = (\y\B. f x y) + (\x\A'. \y\B. f x y)" + by (simp add: insert.hyps) + also have " ... = (\y\B. f x y) + (\y\B. \x\A'. f x y)" + using insert.hyps by (simp add: insert.prems) + also have " ... = (\y\B. (f x y) + (\x\A'. f x y))" + by (simp add: sum.distrib) + finally have "(\x\insert x A'. \y\B. f x y) = (\y\B. \x\insert x A'. f x y)" + using sum.swap by blast + thus ?case by simp +qed + +lemma (in group_action) card_stablizer_sum: + assumes "finite (carrier G)" "orb \ (orbits G E \)" + shows "(\x \ orb. card (stabilizer G \ x)) = order G" +proof - + obtain x where x:"x \ E" and orb:"orb = orbit G \ x" + using assms(2) unfolding orbits_def by blast + have "\y. y \ orb \ card (stabilizer G \ x) = card (stabilizer G \ y)" + proof - + fix y assume "y \ orb" + hence y: "y \ E \ y \ orbit G \ x" + using x orb assms(2) orbits_coverture by auto + hence same_orbit: "(orbit G \ x) = (orbit G \ y)" + using disjoint_union[of "orbit G \ x" "orbit G \ y"] orbit_refl x + unfolding orbits_def by auto + have "card (orbit G \ x) * card (stabilizer G \ x) = + card (orbit G \ y) * card (stabilizer G \ y)" + using y assms(1) x orbit_stabilizer_theorem by simp + hence "card (orbit G \ x) * card (stabilizer G \ x) = + card (orbit G \ x) * card (stabilizer G \ y)" using same_orbit by simp + moreover have "orbit G \ x \ {} \ finite (orbit G \ x)" + using y orbit_def[of G \ x] assms(1) by auto + hence "card (orbit G \ x) > 0" + by (simp add: card_gt_0_iff) + ultimately show "card (stabilizer G \ x) = card (stabilizer G \ y)" by auto + qed + hence "(\x \ orb. card (stabilizer G \ x)) = (\y \ orb. card (stabilizer G \ x))" by auto + also have " ... = card (stabilizer G \ x) * (\y \ orb. 1)" by simp + also have " ... = card (stabilizer G \ x) * card (orbit G \ x)" + using orb by auto + finally show "(\x \ orb. card (stabilizer G \ x)) = order G" + by (metis mult.commute orbit_stabilizer_theorem x) +qed + + +subsubsection \The Lemma\ + +theorem (in group_action) burnside: + assumes "finite (carrier G)" "finite E" + shows "card (orbits G E \) * order G = (\g \ carrier G. card(invariants E \ g))" +proof - + have "(\g \ carrier G. card(invariants E \ g)) = + (\g \ carrier G. \x \ E. (if (\ g) x = x then 1 else 0))" + by (simp add: assms(2) card_as_sums invariants_def) + also have " ... = (\x \ E. \g \ carrier G. (if (\ g) x = x then 1 else 0))" + using sum_invertion[where ?f = "\ g x. (if (\ g) x = x then 1 else 0)"] assms by auto + also have " ... = (\x \ E. card (stabilizer G \ x))" + by (simp add: assms(1) card_as_sums stabilizer_def) + also have " ... = (\orbit \ (orbits G E \). \x \ orbit. card (stabilizer G \ x))" + using disjoint_sum orbits_coverture assms(2) by metis + also have " ... = (\orbit \ (orbits G E \). order G)" + by (simp add: assms(1) card_stablizer_sum) + finally have "(\g \ carrier G. card(invariants E \ g)) = card (orbits G E \) * order G" by simp + thus ?thesis by simp +qed + + + +subsection \Action by Conjugation\ + + +subsubsection \Action Over Itself\ + +text \A Group Acts by Conjugation Over Itself\ + +lemma (in group) conjugation_is_inj: + assumes "g \ carrier G" "h1 \ carrier G" "h2 \ carrier G" + and "g \ h1 \ (inv g) = g \ h2 \ (inv g)" + shows "h1 = h2" + using assms by auto + +lemma (in group) conjugation_is_surj: + assumes "g \ carrier G" "h \ carrier G" + shows "g \ ((inv g) \ h \ g) \ (inv g) = h" + using assms m_assoc inv_closed inv_inv m_closed monoid_axioms r_inv r_one + by metis + +lemma (in group) conjugation_is_bij: + assumes "g \ carrier G" + shows "bij_betw (\h \ carrier G. g \ h \ (inv g)) (carrier G) (carrier G)" + (is "bij_betw ?\ (carrier G) (carrier G)") + unfolding bij_betw_def +proof + show "inj_on ?\ (carrier G)" + using conjugation_is_inj by (simp add: assms inj_on_def) +next + have S: "\ h. h \ carrier G \ (inv g) \ h \ g \ carrier G" + using assms by blast + have "\ h. h \ carrier G \ ?\ ((inv g) \ h \ g) = h" + using assms by (simp add: conjugation_is_surj) + hence "carrier G \ ?\ ` carrier G" + using S image_iff by fastforce + moreover have "\ h. h \ carrier G \ ?\ h \ carrier G" + using assms by simp + hence "?\ ` carrier G \ carrier G" by blast + ultimately show "?\ ` carrier G = carrier G" by blast +qed + +lemma(in group) conjugation_is_hom: + "(\g. \h \ carrier G. g \ h \ inv g) \ hom G (BijGroup (carrier G))" + unfolding hom_def +proof - + let ?\ = "\g. \h. g \ h \ inv g" + let ?\ = "\g. restrict (?\ g) (carrier G)" + + (* First, we prove that ?\: G \ Bij(G) is well defined *) + have Step0: "\ g. g \ carrier G \ (?\ g) \ Bij (carrier G)" + using Bij_def conjugation_is_bij by fastforce + hence Step1: "?\: carrier G \ carrier (BijGroup (carrier G))" + unfolding BijGroup_def by simp + + (* Second, we prove that ?\ is a homomorphism *) + have "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + (\ h. h \ carrier G \ ?\ (g1 \ g2) h = (?\ g1) ((?\ g2) h))" + proof - + fix g1 g2 h assume g1: "g1 \ carrier G" and g2: "g2 \ carrier G" and h: "h \ carrier G" + have "inv (g1 \ g2) = (inv g2) \ (inv g1)" + using g1 g2 by (simp add: inv_mult_group) + thus "?\ (g1 \ g2) h = (?\ g1) ((?\ g2) h)" + by (simp add: g1 g2 h m_assoc) + qed + hence "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + (\ h \ carrier G. ?\ (g1 \ g2) h) = (\ h \ carrier G. (?\ g1) ((?\ g2) h))" by auto + hence Step2: "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + ?\ (g1 \ g2) = (?\ g1) \\<^bsub>BijGroup (carrier G)\<^esub> (?\ g2)" + unfolding BijGroup_def by (simp add: Step0 compose_def) + + (* Finally, we combine both results to prove the lemma *) + thus "?\ \ {h: carrier G \ carrier (BijGroup (carrier G)). + (\x \ carrier G. \y \ carrier G. h (x \ y) = h x \\<^bsub>BijGroup (carrier G)\<^esub> h y)}" + using Step1 Step2 by auto +qed + +theorem (in group) action_by_conjugation: + "group_action G (carrier G) (\g. (\h \ carrier G. g \ h \ (inv g)))" + unfolding group_action_def group_hom_def using conjugation_is_hom + by (simp add: group_BijGroup group_hom_axioms.intro is_group) + + +subsubsection \Action Over The Set of Subgroups\ + +text \A Group Acts by Conjugation Over The Set of Subgroups\ + +lemma (in group) subgroup_conjugation_is_inj_aux: + assumes "g \ carrier G" "H1 \ carrier G" "H2 \ carrier G" + and "g <# H1 #> (inv g) = g <# H2 #> (inv g)" + shows "H1 \ H2" +proof + fix h1 assume h1: "h1 \ H1" + hence "g \ h1 \ (inv g) \ g <# H1 #> (inv g)" + unfolding l_coset_def r_coset_def using assms by blast + hence "g \ h1 \ (inv g) \ g <# H2 #> (inv g)" + using assms by auto + hence "\h2 \ H2. g \ h1 \ (inv g) = g \ h2 \ (inv g)" + unfolding l_coset_def r_coset_def by blast + then obtain h2 where "h2 \ H2 \ g \ h1 \ (inv g) = g \ h2 \ (inv g)" by blast + thus "h1 \ H2" + using assms conjugation_is_inj h1 by blast +qed + +lemma (in group) subgroup_conjugation_is_inj: + assumes "g \ carrier G" "H1 \ carrier G" "H2 \ carrier G" + and "g <# H1 #> (inv g) = g <# H2 #> (inv g)" + shows "H1 = H2" + using subgroup_conjugation_is_inj_aux assms set_eq_subset by metis + +lemma (in group) subgroup_conjugation_is_surj0: + assumes "g \ carrier G" "H \ carrier G" + shows "g <# ((inv g) <# H #> g) #> (inv g) = H" + using coset_assoc assms coset_mult_assoc l_coset_subset_G lcos_m_assoc + by (simp add: lcos_mult_one) + +lemma (in group) subgroup_conjugation_is_surj1: + assumes "g \ carrier G" "subgroup H G" + shows "subgroup ((inv g) <# H #> g) G" +proof + show "\ \ inv g <# H #> g" + proof - + have "\ \ H" by (simp add: assms(2) subgroup.one_closed) + hence "inv g \ \ \ g \ inv g <# H #> g" + unfolding l_coset_def r_coset_def by blast + thus "\ \ inv g <# H #> g" using assms by simp + qed +next + show "inv g <# H #> g \ carrier G" + proof + fix x assume "x \ inv g <# H #> g" + hence "\h \ H. x = (inv g) \ h \ g" + unfolding r_coset_def l_coset_def by blast + hence "\h \ (carrier G). x = (inv g) \ h \ g" + by (meson assms subgroup.mem_carrier) + thus "x \ carrier G" using assms by blast + qed +next + show " \ x y. \ x \ inv g <# H #> g; y \ inv g <# H #> g \ \ x \ y \ inv g <# H #> g" + proof - + fix x y assume "x \ inv g <# H #> g" "y \ inv g <# H #> g" + hence "\ h1 \ H. \ h2 \ H. x = (inv g) \ h1 \ g \ y = (inv g) \ h2 \ g" + unfolding l_coset_def r_coset_def by blast + hence "\ h1 \ H. \ h2 \ H. x \ y = ((inv g) \ h1 \ g) \ ((inv g) \ h2 \ g)" by blast + hence "\ h1 \ H. \ h2 \ H. x \ y = ((inv g) \ (h1 \ h2) \ g)" + using assms is_group inv_closed l_one m_assoc m_closed + monoid_axioms r_inv subgroup.mem_carrier by smt + hence "\ h \ H. x \ y = (inv g) \ h \ g" + by (meson assms(2) subgroup_def) + thus "x \ y \ inv g <# H #> g" + unfolding l_coset_def r_coset_def by blast + qed +next + show "\x. x \ inv g <# H #> g \ inv x \ inv g <# H #> g" + proof - + fix x assume "x \ inv g <# H #> g" + hence "\h \ H. x = (inv g) \ h \ g" + unfolding r_coset_def l_coset_def by blast + then obtain h where h: "h \ H \ x = (inv g) \ h \ g" by blast + hence "x \ (inv g) \ (inv h) \ g = \" + using assms inv_closed m_assoc m_closed monoid_axioms + r_inv r_one subgroup.mem_carrier by smt + hence "inv x = (inv g) \ (inv h) \ g" + using assms h inv_closed inv_inv inv_mult_group m_assoc + m_closed monoid_axioms subgroup.mem_carrier by smt + moreover have "inv h \ H" + by (simp add: assms h subgroup.m_inv_closed) + ultimately show "inv x \ inv g <# H #> g" unfolding r_coset_def l_coset_def by blast + qed +qed + +lemma (in group) subgroup_conjugation_is_surj2: + assumes "g \ carrier G" "subgroup H G" + shows "subgroup (g <# H #> (inv g)) G" + using subgroup_conjugation_is_surj1 by (metis assms inv_closed inv_inv) + +lemma (in group) subgroup_conjugation_is_bij: + assumes "g \ carrier G" + shows "bij_betw (\H \ {H. subgroup H G}. g <# H #> (inv g)) {H. subgroup H G} {H. subgroup H G}" + (is "bij_betw ?\ {H. subgroup H G} {H. subgroup H G}") + unfolding bij_betw_def +proof + show "inj_on ?\ {H. subgroup H G}" + using subgroup_conjugation_is_inj assms inj_on_def subgroup_imp_subset + by (metis (mono_tags, lifting) inj_on_restrict_eq mem_Collect_eq) +next + have "\H. H \ {H. subgroup H G} \ ?\ ((inv g) <# H #> g) = H" + by (simp add: assms subgroup_imp_subset subgroup_conjugation_is_surj0 + subgroup_conjugation_is_surj1 is_group) + hence "\H. H \ {H. subgroup H G} \ \H' \ {H. subgroup H G}. ?\ H' = H" + using assms subgroup_conjugation_is_surj1 by fastforce + thus "?\ ` {H. subgroup H G} = {H. subgroup H G}" + using subgroup_conjugation_is_surj2 assms by auto +qed + +lemma (in group) subgroup_conjugation_is_hom: + "(\g. \H \ {H. subgroup H G}. g <# H #> (inv g)) \ hom G (BijGroup {H. subgroup H G})" + unfolding hom_def +proof - + (* We follow the exact same structure of conjugation_is_hom's proof *) + let ?\ = "\g. \H. g <# H #> (inv g)" + let ?\ = "\g. restrict (?\ g) {H. subgroup H G}" + + have Step0: "\ g. g \ carrier G \ (?\ g) \ Bij {H. subgroup H G}" + using Bij_def subgroup_conjugation_is_bij by fastforce + hence Step1: "?\: carrier G \ carrier (BijGroup {H. subgroup H G})" + unfolding BijGroup_def by simp + + have "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + (\ H. H \ {H. subgroup H G} \ ?\ (g1 \ g2) H = (?\ g1) ((?\ g2) H))" + proof - + fix g1 g2 H assume g1: "g1 \ carrier G" and g2: "g2 \ carrier G" and H': "H \ {H. subgroup H G}" + hence H: "subgroup H G" by simp + have "(?\ g1) ((?\ g2) H) = g1 <# (g2 <# H #> (inv g2)) #> (inv g1)" + by (simp add: H g2 subgroup_conjugation_is_surj2) + also have " ... = g1 <# (g2 <# H) #> ((inv g2) \ (inv g1))" + by (simp add: H coset_mult_assoc g1 g2 group.coset_assoc + is_group l_coset_subset_G subgroup_imp_subset) + also have " ... = g1 <# (g2 <# H) #> inv (g1 \ g2)" + using g1 g2 by (simp add: inv_mult_group) + finally have "(?\ g1) ((?\ g2) H) = ?\ (g1 \ g2) H" + by (simp add: H g1 g2 lcos_m_assoc subgroup_imp_subset) + thus "?\ (g1 \ g2) H = (?\ g1) ((?\ g2) H)" by auto + qed + hence "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + (\H \ {H. subgroup H G}. ?\ (g1 \ g2) H) = (\H \ {H. subgroup H G}. (?\ g1) ((?\ g2) H))" + by (meson restrict_ext) + hence Step2: "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + ?\ (g1 \ g2) = (?\ g1) \\<^bsub>BijGroup {H. subgroup H G}\<^esub> (?\ g2)" + unfolding BijGroup_def by (simp add: Step0 compose_def) + + show "?\ \ {h: carrier G \ carrier (BijGroup {H. subgroup H G}). + \x\carrier G. \y\carrier G. h (x \ y) = h x \\<^bsub>BijGroup {H. subgroup H G}\<^esub> h y}" + using Step1 Step2 by auto +qed + +theorem (in group) action_by_conjugation_on_subgroups_set: + "group_action G {H. subgroup H G} (\g. \H \ {H. subgroup H G}. g <# H #> (inv g))" + unfolding group_action_def group_hom_def using subgroup_conjugation_is_hom + by (simp add: group_BijGroup group_hom_axioms.intro is_group) + + +subsubsection \Action Over The Power Set\ + +text \A Group Acts by Conjugation Over The Power Set\ + +lemma (in group) subset_conjugation_is_bij: + assumes "g \ carrier G" + shows "bij_betw (\H \ {H. H \ carrier G}. g <# H #> (inv g)) {H. H \ carrier G} {H. H \ carrier G}" + (is "bij_betw ?\ {H. H \ carrier G} {H. H \ carrier G}") + unfolding bij_betw_def +proof + show "inj_on ?\ {H. H \ carrier G}" + using subgroup_conjugation_is_inj assms inj_on_def + by (metis (mono_tags, lifting) inj_on_restrict_eq mem_Collect_eq) +next + have "\H. H \ {H. H \ carrier G} \ ?\ ((inv g) <# H #> g) = H" + by (simp add: assms l_coset_subset_G r_coset_subset_G subgroup_conjugation_is_surj0) + hence "\H. H \ {H. H \ carrier G} \ \H' \ {H. H \ carrier G}. ?\ H' = H" + by (metis assms l_coset_subset_G mem_Collect_eq r_coset_subset_G subgroup_def subgroup_self) + hence "{H. H \ carrier G} \ ?\ ` {H. H \ carrier G}" by blast + moreover have "?\ ` {H. H \ carrier G} \ {H. H \ carrier G}" + by (smt assms image_subsetI inv_closed l_coset_subset_G + mem_Collect_eq r_coset_subset_G restrict_apply') + ultimately show "?\ ` {H. H \ carrier G} = {H. H \ carrier G}" by simp +qed + +lemma (in group) subset_conjugation_is_hom: + "(\g. \H \ {H. H \ carrier G}. g <# H #> (inv g)) \ hom G (BijGroup {H. H \ carrier G})" + unfolding hom_def +proof - + (* We follow the exact same structure of conjugation_is_hom's proof *) + let ?\ = "\g. \H. g <# H #> (inv g)" + let ?\ = "\g. restrict (?\ g) {H. H \ carrier G}" + + have Step0: "\ g. g \ carrier G \ (?\ g) \ Bij {H. H \ carrier G}" + using Bij_def subset_conjugation_is_bij by fastforce + hence Step1: "?\: carrier G \ carrier (BijGroup {H. H \ carrier G})" + unfolding BijGroup_def by simp + + have "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + (\ H. H \ {H. H \ carrier G} \ ?\ (g1 \ g2) H = (?\ g1) ((?\ g2) H))" + proof - + fix g1 g2 H assume g1: "g1 \ carrier G" and g2: "g2 \ carrier G" and H: "H \ {H. H \ carrier G}" + hence "(?\ g1) ((?\ g2) H) = g1 <# (g2 <# H #> (inv g2)) #> (inv g1)" + using l_coset_subset_G r_coset_subset_G by auto + also have " ... = g1 <# (g2 <# H) #> ((inv g2) \ (inv g1))" + using H coset_assoc coset_mult_assoc g1 g2 l_coset_subset_G by auto + also have " ... = g1 <# (g2 <# H) #> inv (g1 \ g2)" + using g1 g2 by (simp add: inv_mult_group) + finally have "(?\ g1) ((?\ g2) H) = ?\ (g1 \ g2) H" + using H g1 g2 lcos_m_assoc by force + thus "?\ (g1 \ g2) H = (?\ g1) ((?\ g2) H)" by auto + qed + hence "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + (\H \ {H. H \ carrier G}. ?\ (g1 \ g2) H) = (\H \ {H. H \ carrier G}. (?\ g1) ((?\ g2) H))" + by (meson restrict_ext) + hence Step2: "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \ + ?\ (g1 \ g2) = (?\ g1) \\<^bsub>BijGroup {H. H \ carrier G}\<^esub> (?\ g2)" + unfolding BijGroup_def by (simp add: Step0 compose_def) + + show "?\ \ {h: carrier G \ carrier (BijGroup {H. H \ carrier G}). + \x\carrier G. \y\carrier G. h (x \ y) = h x \\<^bsub>BijGroup {H. H \ carrier G}\<^esub> h y}" + using Step1 Step2 by auto +qed + +theorem (in group) action_by_conjugation_on_power_set: + "group_action G {H. H \ carrier G} (\g. \H \ {H. H \ carrier G}. g <# H #> (inv g))" + unfolding group_action_def group_hom_def using subset_conjugation_is_hom + by (simp add: group_BijGroup group_hom_axioms.intro is_group) + +corollary (in group) normalizer_imp_subgroup: + assumes "H \ carrier G" + shows "subgroup (normalizer G H) G" + unfolding normalizer_def + using group_action.stabilizer_subgroup[OF action_by_conjugation_on_power_set] assms by auto + + +subsection \Subgroup of an Acting Group\ + +text \A Subgroup of an Acting Group Induces an Action\ + +lemma (in group_action) induced_homomorphism: + assumes "subgroup H G" + shows "\ \ hom (G \carrier := H\) (BijGroup E)" + unfolding hom_def apply simp +proof - + have S0: "H \ carrier G" by (meson assms subgroup_def) + hence "\: H \ carrier (BijGroup E)" + by (simp add: BijGroup_def bij_prop0 subset_eq) + thus "\: H \ carrier (BijGroup E) \ (\x \ H. \y \ H. \ (x \ y) = \ x \\<^bsub>BijGroup E\<^esub> \ y)" + by (simp add: S0 group_hom group_hom.hom_mult set_rev_mp) +qed + +theorem (in group_action) induced_action: + assumes "subgroup H G" + shows "group_action (G \carrier := H\) E \" + unfolding group_action_def group_hom_def + using induced_homomorphism assms group.subgroup_imp_group group_BijGroup + group_hom group_hom.axioms(1) group_hom_axioms_def by blast + +end \ No newline at end of file diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/Ideal.thy --- a/src/HOL/Algebra/Ideal.thy Tue Jun 12 16:21:52 2018 +0200 +++ b/src/HOL/Algebra/Ideal.thy Tue Jun 12 16:09:12 2018 +0100 @@ -29,7 +29,7 @@ lemma idealI: fixes R (structure) assumes "ring R" - assumes a_subgroup: "subgroup I \carrier = carrier R, mult = add R, one = zero R\" + assumes a_subgroup: "subgroup I (add_monoid R)" and I_l_closed: "\a x. \a \ I; x \ carrier R\ \ x \ a \ I" and I_r_closed: "\a x. \a \ I; x \ carrier R\ \ a \ x \ I" shows "ideal I R" @@ -708,10 +708,7 @@ qed corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\} R" - apply rule - apply (erule domain.zeroprimeideal) - apply (erule zeroprimeideal_domainI) - done + using domain.zeroprimeideal zeroprimeideal_domainI by blast subsection \Maximal Ideals\ @@ -963,9 +960,6 @@ qed lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\} R = field R" - apply rule - apply (erule zeromaximalideal_fieldI) - apply (erule field.zeromaximalideal) - done + using field.zeromaximalideal zeromaximalideal_fieldI by blast end diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Tue Jun 12 16:21:52 2018 +0200 +++ b/src/HOL/Algebra/Ring.thy Tue Jun 12 16:09:12 2018 +0100 @@ -13,79 +13,101 @@ record 'a ring = "'a monoid" + zero :: 'a ("\\") - add :: "['a, 'a] => 'a" (infixl "\\" 65) + add :: "['a, 'a] \ 'a" (infixl "\\" 65) + +abbreviation + add_monoid :: "('a, 'm) ring_scheme \ ('a, 'm) monoid_scheme" + where "add_monoid R \ \ carrier = carrier R, mult = add R, one = zero R, \ = (undefined :: 'm) \" text \Derived operations.\ definition - a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\\ _" [81] 80) - where "a_inv R = m_inv \carrier = carrier R, mult = add R, one = zero R\" + a_inv :: "[('a, 'm) ring_scheme, 'a ] \ 'a" ("\\ _" [81] 80) + where "a_inv R = m_inv (add_monoid R)" + definition a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" ("(_ \\ _)" [65,66] 65) - where "[| x \ carrier R; y \ carrier R |] ==> x \\<^bsub>R\<^esub> y = x \\<^bsub>R\<^esub> (\\<^bsub>R\<^esub> y)" + where "\ x \ carrier R; y \ carrier R \ \ x \\<^bsub>R\<^esub> y = x \\<^bsub>R\<^esub> (\\<^bsub>R\<^esub> y)" + +definition + add_pow :: "[_, ('b :: semiring_1), 'a] \ 'a" ("[_] \\ _" [81, 81] 80) + where "add_pow R k a = pow (add_monoid R) a k" locale abelian_monoid = fixes G (structure) assumes a_comm_monoid: - "comm_monoid \carrier = carrier G, mult = add G, one = zero G\" + "comm_monoid (add_monoid G)" definition - finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where - "finsum G = finprod \carrier = carrier G, mult = add G, one = zero G\" + finsum :: "[('b, 'm) ring_scheme, 'a \ 'b, 'a set] \ 'b" where + "finsum G = finprod (add_monoid G)" syntax - "_finsum" :: "index => idt => 'a set => 'b => 'b" + "_finsum" :: "index \ idt \ 'a set \ 'b \ 'b" ("(3\__\_. _)" [1000, 0, 51, 10] 10) translations - "\\<^bsub>G\<^esub>i\A. b" \ "CONST finsum G (%i. b) A" + "\\<^bsub>G\<^esub>i\A. b" \ "CONST finsum G (\i. b) A" \ \Beware of argument permutation!\ locale abelian_group = abelian_monoid + assumes a_comm_group: - "comm_group \carrier = carrier G, mult = add G, one = zero G\" + "comm_group (add_monoid G)" subsection \Basic Properties\ lemma abelian_monoidI: fixes R (structure) - assumes a_closed: - "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y \ carrier R" - and zero_closed: "\ \ carrier R" - and a_assoc: - "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] ==> - (x \ y) \ z = x \ (y \ z)" - and l_zero: "!!x. x \ carrier R ==> \ \ x = x" - and a_comm: - "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y = y \ x" + assumes "\x y. \ x \ carrier R; y \ carrier R \ \ x \ y \ carrier R" + and "\ \ carrier R" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ (y \ z)" + and "\x. x \ carrier R \ \ \ x = x" + and "\x y. \ x \ carrier R; y \ carrier R \ \ x \ y = y \ x" shows "abelian_monoid R" by (auto intro!: abelian_monoid.intro comm_monoidI intro: assms) +lemma abelian_monoidE: + fixes R (structure) + assumes "abelian_monoid R" + shows "\x y. \ x \ carrier R; y \ carrier R \ \ x \ y \ carrier R" + and "\ \ carrier R" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ (y \ z)" + and "\x. x \ carrier R \ \ \ x = x" + and "\x y. \ x \ carrier R; y \ carrier R \ \ x \ y = y \ x" + using assms unfolding abelian_monoid_def comm_monoid_def comm_monoid_axioms_def monoid_def by auto + lemma abelian_groupI: fixes R (structure) - assumes a_closed: - "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y \ carrier R" - and zero_closed: "zero R \ carrier R" - and a_assoc: - "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] ==> - (x \ y) \ z = x \ (y \ z)" - and a_comm: - "!!x y. [| x \ carrier R; y \ carrier R |] ==> x \ y = y \ x" - and l_zero: "!!x. x \ carrier R ==> \ \ x = x" - and l_inv_ex: "\x. x \ carrier R \ \y \ carrier R. y \ x = \" + assumes "\x y. \ x \ carrier R; y \ carrier R \ \ x \ y \ carrier R" + and "\ \ carrier R" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ (y \ z)" + and "\x y. \ x \ carrier R; y \ carrier R \ \ x \ y = y \ x" + and "\x. x \ carrier R \ \ \ x = x" + and "\x. x \ carrier R \ \y \ carrier R. y \ x = \" shows "abelian_group R" by (auto intro!: abelian_group.intro abelian_monoidI abelian_group_axioms.intro comm_monoidI comm_groupI intro: assms) +lemma abelian_groupE: + fixes R (structure) + assumes "abelian_group R" + shows "\x y. \ x \ carrier R; y \ carrier R \ \ x \ y \ carrier R" + and "\ \ carrier R" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ (y \ z)" + and "\x y. \ x \ carrier R; y \ carrier R \ \ x \ y = y \ x" + and "\x. x \ carrier R \ \ \ x = x" + and "\x. x \ carrier R \ \y \ carrier R. y \ x = \" + using abelian_group.a_comm_group assms comm_groupE by fastforce+ + lemma (in abelian_monoid) a_monoid: - "monoid \carrier = carrier G, mult = add G, one = zero G\" + "monoid (add_monoid G)" by (rule comm_monoid.axioms, rule a_comm_monoid) lemma (in abelian_group) a_group: - "group \carrier = carrier G, mult = add G, one = zero G\" + "group (add_monoid G)" by (simp add: group_def a_monoid) (simp add: comm_group.axioms group.axioms a_comm_group) @@ -94,13 +116,15 @@ text \Transfer facts from multiplicative structures via interpretation.\ sublocale abelian_monoid < - add: monoid "\carrier = carrier G, mult = add G, one = zero G\" - rewrites "carrier \carrier = carrier G, mult = add G, one = zero G\ = carrier G" - and "mult \carrier = carrier G, mult = add G, one = zero G\ = add G" - and "one \carrier = carrier G, mult = add G, one = zero G\ = zero G" - by (rule a_monoid) auto + add: monoid "(add_monoid G)" + rewrites "carrier (add_monoid G) = carrier G" + and "mult (add_monoid G) = add G" + and "one (add_monoid G) = zero G" + and "(\a k. pow (add_monoid G) a k) = (\a k. add_pow G k a)" + by (rule a_monoid) (auto simp add: add_pow_def) -context abelian_monoid begin +context abelian_monoid +begin lemmas a_closed = add.m_closed lemmas zero_closed = add.one_closed @@ -112,12 +136,13 @@ end sublocale abelian_monoid < - add: comm_monoid "\carrier = carrier G, mult = add G, one = zero G\" - rewrites "carrier \carrier = carrier G, mult = add G, one = zero G\ = carrier G" - and "mult \carrier = carrier G, mult = add G, one = zero G\ = add G" - and "one \carrier = carrier G, mult = add G, one = zero G\ = zero G" - and "finprod \carrier = carrier G, mult = add G, one = zero G\ = finsum G" - by (rule a_comm_monoid) (auto simp: finsum_def) + add: comm_monoid "(add_monoid G)" + rewrites "carrier (add_monoid G) = carrier G" + and "mult (add_monoid G) = add G" + and "one (add_monoid G) = zero G" + and "finprod (add_monoid G) = finsum G" + and "pow (add_monoid G) = (\a k. add_pow G k a)" + by (rule a_comm_monoid) (auto simp: finsum_def add_pow_def) context abelian_monoid begin @@ -168,12 +193,13 @@ end sublocale abelian_group < - add: group "\carrier = carrier G, mult = add G, one = zero G\" - rewrites "carrier \carrier = carrier G, mult = add G, one = zero G\ = carrier G" - and "mult \carrier = carrier G, mult = add G, one = zero G\ = add G" - and "one \carrier = carrier G, mult = add G, one = zero G\ = zero G" - and "m_inv \carrier = carrier G, mult = add G, one = zero G\ = a_inv G" - by (rule a_group) (auto simp: m_inv_def a_inv_def) + add: group "(add_monoid G)" + rewrites "carrier (add_monoid G) = carrier G" + and "mult (add_monoid G) = add G" + and "one (add_monoid G) = zero G" + and "m_inv (add_monoid G) = a_inv G" + and "pow (add_monoid G) = (\a k. add_pow G k a)" + by (rule a_group) (auto simp: m_inv_def a_inv_def add_pow_def) context abelian_group begin @@ -194,13 +220,14 @@ end sublocale abelian_group < - add: comm_group "\carrier = carrier G, mult = add G, one = zero G\" - rewrites "carrier \carrier = carrier G, mult = add G, one = zero G\ = carrier G" - and "mult \carrier = carrier G, mult = add G, one = zero G\ = add G" - and "one \carrier = carrier G, mult = add G, one = zero G\ = zero G" - and "m_inv \carrier = carrier G, mult = add G, one = zero G\ = a_inv G" - and "finprod \carrier = carrier G, mult = add G, one = zero G\ = finsum G" - by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def) + add: comm_group "(add_monoid G)" + rewrites "carrier (add_monoid G) = carrier G" + and "mult (add_monoid G) = add G" + and "one (add_monoid G) = zero G" + and "m_inv (add_monoid G) = a_inv G" + and "finprod (add_monoid G) = finsum G" + and "pow (add_monoid G) = (\a k. add_pow G k a)" + by (rule a_comm_group) (auto simp: m_inv_def a_inv_def finsum_def add_pow_def) lemmas (in abelian_group) minus_add = add.inv_mult @@ -208,10 +235,10 @@ lemma comm_group_abelian_groupI: fixes G (structure) - assumes cg: "comm_group \carrier = carrier G, mult = add G, one = zero G\" + assumes cg: "comm_group (add_monoid G)" shows "abelian_group G" proof - - interpret comm_group "\carrier = carrier G, mult = add G, one = zero G\" + interpret comm_group "(add_monoid G)" by (rule cg) show "abelian_group G" .. qed @@ -219,26 +246,21 @@ subsection \Rings: Basic Definitions\ -locale semiring = abelian_monoid R + monoid R for R (structure) + - assumes l_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> (x \ y) \ z = x \ z \ y \ z" - and r_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> z \ (x \ y) = z \ x \ z \ y" - and l_null[simp]: "x \ carrier R ==> \ \ x = \" - and r_null[simp]: "x \ carrier R ==> x \ \ = \" +locale semiring = abelian_monoid (* for add *) R + monoid (* for mult *) R for R (structure) + + assumes l_distr: "\ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ z \ y \ z" + and r_distr: "\ x \ carrier R; y \ carrier R; z \ carrier R \ \ z \ (x \ y) = z \ x \ z \ y" + and l_null[simp]: "x \ carrier R \ \ \ x = \" + and r_null[simp]: "x \ carrier R \ x \ \ = \" -locale ring = abelian_group R + monoid R for R (structure) + - assumes "[| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> (x \ y) \ z = x \ z \ y \ z" - and "[| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> z \ (x \ y) = z \ x \ z \ y" +locale ring = abelian_group (* for add *) R + monoid (* for mult *) R for R (structure) + + assumes "\ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ z \ y \ z" + and "\ x \ carrier R; y \ carrier R; z \ carrier R \ \ z \ (x \ y) = z \ x \ z \ y" -locale cring = ring + comm_monoid R +locale cring = ring + comm_monoid (* for mult *) R locale "domain" = cring + assumes one_not_zero [simp]: "\ \ \" - and integral: "[| a \ b = \; a \ carrier R; b \ carrier R |] ==> - a = \ \ b = \" + and integral: "\ a \ b = \; a \ carrier R; b \ carrier R \ \ a = \ \ b = \" locale field = "domain" + assumes field_Units: "Units R = carrier R - {\}" @@ -248,16 +270,23 @@ lemma ringI: fixes R (structure) - assumes abelian_group: "abelian_group R" - and monoid: "monoid R" - and l_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> (x \ y) \ z = x \ z \ y \ z" - and r_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> z \ (x \ y) = z \ x \ z \ y" + assumes "abelian_group R" + and "monoid R" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ z \ y \ z" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ z \ (x \ y) = z \ x \ z \ y" shows "ring R" by (auto intro: ring.intro abelian_group.axioms ring_axioms.intro assms) +lemma ringE: + fixes R (structure) + assumes "ring R" + shows "abelian_group R" + and "monoid R" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ z \ y \ z" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ z \ (x \ y) = z \ x \ z \ y" + using assms unfolding ring_def ring_axioms_def by auto + context ring begin lemma is_abelian_group: "abelian_group R" .. @@ -269,15 +298,15 @@ by (rule ring_axioms) end - +thm monoid_record_simps lemmas ring_record_simps = monoid_record_simps ring.simps lemma cringI: fixes R (structure) assumes abelian_group: "abelian_group R" and comm_monoid: "comm_monoid R" - and l_distr: "!!x y z. [| x \ carrier R; y \ carrier R; z \ carrier R |] - ==> (x \ y) \ z = x \ z \ y \ z" + and l_distr: "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ + (x \ y) \ z = x \ z \ y \ z" shows "cring R" proof (intro cring.intro ring.intro) show "ring_axioms R" @@ -300,20 +329,35 @@ qed (auto intro: cring.intro abelian_group.axioms comm_monoid.axioms ring_axioms.intro assms) +lemma cringE: + fixes R (structure) + assumes "cring R" + shows "comm_monoid R" + and "\x y z. \ x \ carrier R; y \ carrier R; z \ carrier R \ \ (x \ y) \ z = x \ z \ y \ z" + using assms cring_def apply auto by (simp add: assms cring.axioms(1) ringE(3)) + (* lemma (in cring) is_comm_monoid: "comm_monoid R" by (auto intro!: comm_monoidI m_assoc m_comm) *) - lemma (in cring) is_cring: "cring R" by (rule cring_axioms) subsubsection \Normaliser for Rings\ +lemma (in abelian_group) r_neg1: + "\ x \ carrier G; y \ carrier G \ \ (\ x) \ (x \ y) = y" +proof - + assume G: "x \ carrier G" "y \ carrier G" + then have "(\ x \ x) \ y = y" + by (simp only: l_neg l_zero) + with G show ?thesis by (simp add: a_ac) +qed + lemma (in abelian_group) r_neg2: - "[| x \ carrier G; y \ carrier G |] ==> x \ (\ x \ y) = y" + "\ x \ carrier G; y \ carrier G \ \ x \ ((\ x) \ y) = y" proof - assume G: "x \ carrier G" "y \ carrier G" then have "(x \ \ x) \ y = y" @@ -322,15 +366,6 @@ by (simp add: a_ac) qed -lemma (in abelian_group) r_neg1: - "[| x \ carrier G; y \ carrier G |] ==> \ x \ (x \ y) = y" -proof - - assume G: "x \ carrier G" "y \ carrier G" - then have "(\ x \ x) \ y = y" - by (simp only: l_neg l_zero) - with G show ?thesis by (simp add: a_ac) -qed - context ring begin text \ @@ -358,7 +393,7 @@ qed lemma l_minus: - "[| x \ carrier R; y \ carrier R |] ==> \ x \ y = \ (x \ y)" + "\ x \ carrier R; y \ carrier R \ \ (\ x) \ y = \ (x \ y)" proof - assume R: "x \ carrier R" "y \ carrier R" then have "(\ x) \ y \ x \ y = (\ x \ x) \ y" by (simp add: l_distr) @@ -369,7 +404,7 @@ qed lemma r_minus: - "[| x \ carrier R; y \ carrier R |] ==> x \ \ y = \ (x \ y)" + "\ x \ carrier R; y \ carrier R \ \ x \ (\ y) = \ (x \ y)" proof - assume R: "x \ carrier R" "y \ carrier R" then have "x \ (\ y) \ x \ y = x \ (\ y \ y)" by (simp add: r_distr) @@ -382,12 +417,13 @@ end lemma (in abelian_group) minus_eq: - "[| x \ carrier G; y \ carrier G |] ==> x \ y = x \ \ y" + "\ x \ carrier G; y \ carrier G \ \ x \ y = x \ (\ y)" by (simp only: a_minus_def) text \Setup algebra method: compute distributive normal form in locale contexts\ + ML_file "ringsimp.ML" attribute_setup algebra = \ @@ -467,7 +503,7 @@ fixes R (structure) and S (structure) assumes "ring R" "cring S" assumes RS: "a \ carrier R" "b \ carrier R" "c \ carrier S" "d \ carrier S" - shows "a \ \ (a \ \ b) = b \ c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c" + shows "a \ (\ (a \ (\ b))) = b \ c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c" proof - interpret ring R by fact interpret cring S by fact @@ -488,8 +524,8 @@ subsubsection \Sums over Finite Sets\ lemma (in semiring) finsum_ldistr: - "[| finite A; a \ carrier R; f \ A \ carrier R |] ==> - finsum R f A \ a = finsum R (%i. f i \ a) A" + "\ finite A; a \ carrier R; f: A \ carrier R \ \ + (\ i \ A. (f i)) \ a = (\ i \ A. ((f i) \ a))" proof (induct set: finite) case empty then show ?case by simp next @@ -497,25 +533,87 @@ qed lemma (in semiring) finsum_rdistr: - "[| finite A; a \ carrier R; f \ A \ carrier R |] ==> - a \ finsum R f A = finsum R (%i. a \ f i) A" + "\ finite A; a \ carrier R; f: A \ carrier R \ \ + a \ (\ i \ A. (f i)) = (\ i \ A. (a \ (f i)))" proof (induct set: finite) case empty then show ?case by simp next case (insert x F) then show ?case by (simp add: Pi_def r_distr) qed +(* ************************************************************************** *) +(* Contributed by Paulo E. de Vilhena. *) + +text \A quick detour\ + +lemma add_pow_int_ge: "(k :: int) \ 0 \ [ k ] \\<^bsub>R\<^esub> a = [ nat k ] \\<^bsub>R\<^esub> a" + by (simp add: add_pow_def int_pow_def nat_pow_def) + +lemma add_pow_int_lt: "(k :: int) < 0 \ [ k ] \\<^bsub>R\<^esub> a = \\<^bsub>R\<^esub> ([ nat (- k) ] \\<^bsub>R\<^esub> a)" + by (simp add: int_pow_def nat_pow_def a_inv_def add_pow_def) + +corollary (in semiring) add_pow_ldistr: + assumes "a \ carrier R" "b \ carrier R" + shows "([(k :: nat)] \ a) \ b = [k] \ (a \ b)" +proof - + have "([k] \ a) \ b = (\ i \ {..< k}. a) \ b" + using add.finprod_const[OF assms(1), of "{.. i \ {..< k}. (a \ b))" + using finsum_ldistr[of "{..x. a"] assms by simp + also have " ... = [k] \ (a \ b)" + using add.finprod_const[of "a \ b" "{.. carrier R" "b \ carrier R" + shows "a \ ([(k :: nat)] \ b) = [k] \ (a \ b)" +proof - + have "a \ ([k] \ b) = a \ (\ i \ {..< k}. b)" + using add.finprod_const[OF assms(2), of "{.. i \ {..< k}. (a \ b))" + using finsum_rdistr[of "{..x. b"] assms by simp + also have " ... = [k] \ (a \ b)" + using add.finprod_const[of "a \ b" "{.. carrier R" "b \ carrier R" + shows "([(k :: int)] \ a) \ b = [k] \ (a \ b)" +proof (cases "k \ 0") + case True thus ?thesis + using add_pow_int_ge[of k R] add_pow_ldistr[OF assms] by auto +next + case False thus ?thesis + using add_pow_int_lt[of k R a] add_pow_int_lt[of k R "a \ b"] + add_pow_ldistr[OF assms, of "nat (- k)"] assms l_minus by auto +qed + +lemma (in ring) add_pow_rdistr_int: + assumes "a \ carrier R" "b \ carrier R" + shows "a \ ([(k :: int)] \ b) = [k] \ (a \ b)" +proof (cases "k \ 0") + case True thus ?thesis + using add_pow_int_ge[of k R] add_pow_rdistr[OF assms] by auto +next + case False thus ?thesis + using add_pow_int_lt[of k R b] add_pow_int_lt[of k R "a \ b"] + add_pow_rdistr[OF assms, of "nat (- k)"] assms r_minus by auto +qed +(* ************************************************************************** *) + subsection \Integral Domains\ context "domain" begin -lemma zero_not_one [simp]: - "\ \ \" +lemma zero_not_one [simp]: "\ \ \" by (rule not_sym) simp lemma integral_iff: (* not by default a simp rule! *) - "[| a \ carrier R; b \ carrier R |] ==> (a \ b = \) = (a = \ \ b = \)" + "\ a \ carrier R; b \ carrier R \ \ (a \ b = \) = (a = \ \ b = \)" proof assume "a \ carrier R" "b \ carrier R" "a \ b = \" then show "a = \ \ b = \" by (simp add: integral) @@ -556,6 +654,7 @@ text \Field would not need to be derived from domain, the properties for domain follow from the assumptions of field\ + lemma (in cring) cring_fieldI: assumes field_Units: "Units R = carrier R - {\}" shows "field R" @@ -614,49 +713,62 @@ lemma ring_hom_memI: fixes R (structure) and S (structure) - assumes hom_closed: "!!x. x \ carrier R ==> h x \ carrier S" - and hom_mult: "!!x y. [| x \ carrier R; y \ carrier R |] ==> - h (x \ y) = h x \\<^bsub>S\<^esub> h y" - and hom_add: "!!x y. [| x \ carrier R; y \ carrier R |] ==> - h (x \ y) = h x \\<^bsub>S\<^esub> h y" - and hom_one: "h \ = \\<^bsub>S\<^esub>" + assumes "\x. x \ carrier R \ h x \ carrier S" + and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and "h \ = \\<^bsub>S\<^esub>" shows "h \ ring_hom R S" by (auto simp add: ring_hom_def assms Pi_def) +lemma ring_hom_memE: + fixes R (structure) and S (structure) + assumes "h \ ring_hom R S" + shows "\x. x \ carrier R \ h x \ carrier S" + and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" + and "h \ = \\<^bsub>S\<^esub>" + using assms unfolding ring_hom_def by auto + lemma ring_hom_closed: - "[| h \ ring_hom R S; x \ carrier R |] ==> h x \ carrier S" + "\ h \ ring_hom R S; x \ carrier R \ \ h x \ carrier S" by (auto simp add: ring_hom_def funcset_mem) lemma ring_hom_mult: fixes R (structure) and S (structure) - shows - "[| h \ ring_hom R S; x \ carrier R; y \ carrier R |] ==> - h (x \ y) = h x \\<^bsub>S\<^esub> h y" + shows "\ h \ ring_hom R S; x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" by (simp add: ring_hom_def) lemma ring_hom_add: fixes R (structure) and S (structure) - shows - "[| h \ ring_hom R S; x \ carrier R; y \ carrier R |] ==> - h (x \ y) = h x \\<^bsub>S\<^esub> h y" + shows "\ h \ ring_hom R S; x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y" by (simp add: ring_hom_def) lemma ring_hom_one: fixes R (structure) and S (structure) - shows "h \ ring_hom R S ==> h \ = \\<^bsub>S\<^esub>" + shows "h \ ring_hom R S \ h \ = \\<^bsub>S\<^esub>" by (simp add: ring_hom_def) -locale ring_hom_cring = R?: cring R + S?: cring S - for R (structure) and S (structure) + - fixes h +lemma ring_hom_zero: + fixes R (structure) and S (structure) + assumes "h \ ring_hom R S" "ring R" "ring S" + shows "h \ = \\<^bsub>S\<^esub>" +proof - + have "h \ = h \ \\<^bsub>S\<^esub> h \" + using ring_hom_add[OF assms(1), of \ \] assms(2) + by (simp add: ring.ring_simprules(2) ring.ring_simprules(15)) + thus ?thesis + by (metis abelian_group.l_neg assms ring.is_abelian_group ring.ring_simprules(18) ring.ring_simprules(2) ring_hom_closed) +qed + +locale ring_hom_cring = + R?: cring R + S?: cring S for R (structure) and S (structure) + fixes h assumes homh [simp, intro]: "h \ ring_hom R S" notes hom_closed [simp, intro] = ring_hom_closed [OF homh] and hom_mult [simp] = ring_hom_mult [OF homh] and hom_add [simp] = ring_hom_add [OF homh] and hom_one [simp] = ring_hom_one [OF homh] -lemma (in ring_hom_cring) hom_zero [simp]: - "h \ = \\<^bsub>S\<^esub>" +lemma (in ring_hom_cring) hom_zero [simp]: "h \ = \\<^bsub>S\<^esub>" proof - have "h \ \\<^bsub>S\<^esub> h \ = h \ \\<^bsub>S\<^esub> \\<^bsub>S\<^esub>" by (simp add: hom_add [symmetric] del: hom_add) @@ -664,7 +776,7 @@ qed lemma (in ring_hom_cring) hom_a_inv [simp]: - "x \ carrier R ==> h (\ x) = \\<^bsub>S\<^esub> h x" + "x \ carrier R \ h (\ x) = \\<^bsub>S\<^esub> h x" proof - assume R: "x \ carrier R" then have "h x \\<^bsub>S\<^esub> h (\ x) = h x \\<^bsub>S\<^esub> (\\<^bsub>S\<^esub> h x)" @@ -673,19 +785,24 @@ qed lemma (in ring_hom_cring) hom_finsum [simp]: - "f \ A \ carrier R \ - h (finsum R f A) = finsum S (h \ f) A" - by (induct A rule: infinite_finite_induct, auto simp: Pi_def) + assumes "f: A \ carrier R" + shows "h (\ i \ A. f i) = (\\<^bsub>S\<^esub> i \ A. (h o f) i)" + using assms by (induct A rule: infinite_finite_induct, auto simp: Pi_def) lemma (in ring_hom_cring) hom_finprod: - "f \ A \ carrier R \ - h (finprod R f A) = finprod S (h \ f) A" - by (induct A rule: infinite_finite_induct, auto simp: Pi_def) + assumes "f: A \ carrier R" + shows "h (\ i \ A. f i) = (\\<^bsub>S\<^esub> i \ A. (h o f) i)" + using assms by (induct A rule: infinite_finite_induct, auto simp: Pi_def) declare ring_hom_cring.hom_finprod [simp] -lemma id_ring_hom [simp]: - "id \ ring_hom R R" +lemma id_ring_hom [simp]: "id \ ring_hom R R" by (auto intro!: ring_hom_memI) +(* Next lemma contributed by Paulo Emílio de Vilhena. *) + +lemma ring_hom_trans: + "\ f \ ring_hom R S; g \ ring_hom S T \ \ g \ f \ ring_hom R T" + by (rule ring_hom_memI) (auto simp add: ring_hom_closed ring_hom_mult ring_hom_add ring_hom_one) + end diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/Sylow.thy --- a/src/HOL/Algebra/Sylow.thy Tue Jun 12 16:21:52 2018 +0200 +++ b/src/HOL/Algebra/Sylow.thy Tue Jun 12 16:09:12 2018 +0100 @@ -189,7 +189,7 @@ using rcosetGM1g_subset_G finite_G M1_subset_G cosets_finite rcosetsI by blast lemma M1_cardeq_rcosetGM1g: "g \ carrier G \ card (M1 #> g) = card M1" - by (simp add: card_cosets_equal rcosetsI) + by (metis M1_subset_G card_rcosets_equal rcosetsI) lemma M1_RelM_rcosetGM1g: "g \ carrier G \ (M1, M1 #> g) \ RelM" apply (simp add: RelM_def calM_def card_M1) diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/Algebra/Zassenhaus.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/Zassenhaus.thy Tue Jun 12 16:09:12 2018 +0100 @@ -0,0 +1,846 @@ +theory Zassenhaus + imports Coset Group_Action +begin + +subsection "fundamental lemmas" + + +text "Lemmas about subgroups" + + +(*A subgroup included in another subgroup is a subgroup of the subgroup*) +lemma (in group) subgroup_incl : + assumes "subgroup I G" + and "subgroup J G" + and "I\J" + shows "subgroup I (G\carrier:=J\)"using assms subgroup_inv_equality + by (auto simp add: subgroup_def) + +(*A subgroup of a subgroup is a subgroup of the group*) +lemma (in group) incl_subgroup : + assumes "subgroup J G" + and "subgroup I (G\carrier:=J\)" + shows "subgroup I G" unfolding subgroup_def +proof + have H1: "I \ carrier (G\carrier:=J\)" using assms(2) subgroup_imp_subset by blast + also have H2: "...\J" by simp + also have "...\(carrier G)" by (simp add: assms(1) subgroup_imp_subset) + finally have H: "I \ carrier G" by simp + have "(\x y. \x \ I ; y \ I\ \ x \ y \ I)" using assms(2) by (auto simp add: subgroup_def) + thus "I \ carrier G \ (\x y. x \ I \ y \ I \ x \ y \ I)" using H by blast + have K: "\ \ I" using assms(2) by (auto simp add: subgroup_def) + have "(\x. x \ I \ inv x \ I)" using assms subgroup.m_inv_closed H + by (metis H1 H2 subgroup_inv_equality subsetCE) + thus "\ \ I \ (\x. x \ I \ inv x \ I)" using K by blast +qed + + +text "Lemmas about set_mult" + + +lemma (in group) set_mult_same_law : + assumes "subgroup H G" +and "K1 \ H" +and "K2 \ H" +shows "K1<#>\<^bsub>(G\carrier:=H\)\<^esub>K2 = K1<#>K2" +proof + show "K1 <#>\<^bsub>G\carrier := H\\<^esub> K2 \ K1 <#> K2" + proof + fix h assume Hyph : "h\K1<#>\<^bsub>G\carrier := H\\<^esub>K2" + then obtain k1 k2 where Hyp : "k1\K1 \ k2\K2 \ k1\\<^bsub>G\carrier := H\\<^esub>k2 = h" + unfolding set_mult_def by blast + hence "k1\H" using assms by blast + moreover have "k2\H" using Hyp assms by blast + ultimately have EGAL : "k1 \\<^bsub>G\carrier := H\\<^esub> k2 = k1 \\<^bsub>G\<^esub> k2" by simp + have "k1 \\<^bsub>G\<^esub> k2 \ K1<#>K2" unfolding set_mult_def using Hyp by blast + hence "k1 \\<^bsub>G\carrier := H\\<^esub> k2 \ K1<#>K2" using EGAL by auto + thus "h \ K1<#>K2 " using Hyp by blast + qed + show "K1 <#> K2 \ K1 <#>\<^bsub>G\carrier := H\\<^esub> K2" + proof + fix h assume Hyph : "h\K1<#>K2" + then obtain k1 k2 where Hyp : "k1\K1 \ k2\K2 \ k1\k2 = h" unfolding set_mult_def by blast + hence k1H: "k1\H" using assms by blast + have k2H: "k2\H" using Hyp assms by blast + have EGAL : "k1 \\<^bsub>G\carrier := H\\<^esub> k2 = k1 \\<^bsub>G\<^esub> k2" using k1H k2H by simp + have "k1 \\<^bsub>G\carrier := H\\<^esub> k2 \ K1<#>\<^bsub>G\carrier := H\\<^esub>K2" unfolding set_mult_def using Hyp by blast + hence "k1 \ k2 \ K1<#>\<^bsub>G\carrier := H\\<^esub>K2" using EGAL by auto + thus "h \ K1<#>\<^bsub>G\carrier := H\\<^esub>K2 " using Hyp by blast + qed +qed + + +(*A group multiplied by a subgroup stays the same*) +lemma (in group) set_mult_carrier_idem : + assumes "subgroup H G" + shows "(carrier G)<#>H = carrier G" +proof + show "(carrier G)<#>H \ carrier G" unfolding set_mult_def using subgroup_imp_subset assms by blast +next + have " (carrier G) #> \ = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp + moreover have "(carrier G) #> \ \ (carrier G) <#> H" unfolding set_mult_def r_coset_def + using assms subgroup.one_closed[OF assms] by blast + ultimately show "carrier G \ (carrier G) <#> H" by simp +qed + +(*Same lemma as above, but everything is included in a subgroup*) +lemma (in group) set_mult_subgroup_idem : + assumes "subgroup H G" + and "subgroup N (G\carrier:=H\)" + shows "H<#>N = H" + using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup_imp_subset assms + by (metis monoid.cases_scheme order_refl partial_object.simps(1) + partial_object.update_convs(1) set_mult_same_law) + +(*A normal subgroup is commutative with set_mult*) +lemma (in group) commut_normal : + assumes "subgroup H G" + and "N\G" + shows "H<#>N = N<#>H" +proof- + have aux1 : "{H <#> N} = {\h\H. h <# N }" unfolding set_mult_def l_coset_def by auto + also have "... = {\h\H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce + moreover have aux2 : "{N <#> H} = {\h\H. N #> h }"unfolding set_mult_def r_coset_def by auto + ultimately show "H<#>N = N<#>H" by simp +qed + +(*Same lemma as above, but everything is included in a subgroup*) +lemma (in group) commut_normal_subgroup : + assumes "subgroup H G" + and "N\(G\carrier:=H\)" + and "subgroup K (G\carrier:=H\)" + shows "K<#>N = N<#>K" +proof- + have "N \ carrier (G\carrier := H\)" using assms normal_imp_subgroup subgroup_imp_subset by blast + hence NH : "N \ H" by simp + have "K \ carrier(G\carrier := H\)" using subgroup_imp_subset assms by blast + hence KH : "K \ H" by simp + have Egal : "K <#>\<^bsub>G\carrier := H\\<^esub> N = N <#>\<^bsub>G\carrier := H\\<^esub> K" + using group.commut_normal[where ?G = "G\carrier :=H\", of K N,OF subgroup_imp_group[OF assms(1)] + assms(3) assms(2)] by auto + also have "... = N <#> K" using set_mult_same_law[of H N K, OF assms(1) NH KH] by auto + moreover have "K <#>\<^bsub>G\carrier := H\\<^esub> N = K <#> N" + using set_mult_same_law[of H K N, OF assms(1) KH NH] by auto + ultimately show "K<#>N = N<#>K" by auto +qed + + + +text "Lemmas about intersection and normal subgroups" + + + +lemma (in group) normal_inter: + assumes "subgroup H G" + and "subgroup K G" + and "H1\G\carrier := H\" + shows " (H1\K)\(G\carrier:= (H\K)\)" +proof- + define HK and H1K and GH and GHK + where "HK = H\K" and "H1K=H1\K" and "GH =G\carrier := H\" and "GHK = (G\carrier:= (H\K)\)" + show "H1K\GHK" + proof (intro group.normal_invI[of GHK H1K]) + show "Group.group GHK" + using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast + + next + have H1K_incl:"subgroup H1K (G\carrier:= (H\K)\)" + proof(intro subgroup_incl) + show "subgroup H1K G" + using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast + next + show "subgroup (H\K) G" using HK_def subgroups_Inter_pair assms by auto + next + have "H1 \ (carrier (G\carrier:=H\))" + using assms(3) normal_imp_subgroup subgroup_imp_subset by blast + also have "... \ H" by simp + thus "H1K \H\K" + using H1K_def calculation by auto + qed + thus "subgroup H1K GHK" using GHK_def by simp + + next + show "\ x h. x\carrier GHK \ h\H1K \ x \\<^bsub>GHK\<^esub> h \\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x\ H1K" + proof- + have invHK: "\y\HK\ \ inv\<^bsub>GHK\<^esub> y = inv\<^bsub>GH\<^esub> y" + using subgroup_inv_equality assms HK_def GH_def GHK_def subgroups_Inter_pair by simp + have multHK : "\x\HK;y\HK\ \ x \\<^bsub>(G\carrier:=HK\)\<^esub> y = x \ y" + using HK_def by simp + fix x assume p: "x\carrier GHK" + fix h assume p2 : "h:H1K" + have "carrier(GHK)\HK" + using GHK_def HK_def by simp + hence xHK:"x\HK" using p by auto + hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x" + using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp + have "H1\carrier(GH)" + using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast + hence hHK:"h\HK" + using p2 H1K_def HK_def GH_def by auto + hence xhx_egal : "x \\<^bsub>GHK\<^esub> h \\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub>x = x \\<^bsub>GH\<^esub> h \\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x" + using invx invHK multHK GHK_def GH_def by auto + have xH:"x\carrier(GH)" + using xHK HK_def GH_def by auto + have hH:"h\carrier(GH)" + using hHK HK_def GH_def by auto + have "(\x\carrier (GH). \h\H1. x \\<^bsub>GH\<^esub> h \\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \ H1)" + using assms normal_invE GH_def normal.inv_op_closed2 by fastforce + hence INCL_1 : "x \\<^bsub>GH\<^esub> h \\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \ H1" + using xH H1K_def p2 by blast + have " x \\<^bsub>GH\<^esub> h \\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \ HK" + using assms HK_def subgroups_Inter_pair hHK xHK + by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl) + hence " x \\<^bsub>GH\<^esub> h \\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \ K" using HK_def by simp + hence " x \\<^bsub>GH\<^esub> h \\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \ H1K" using INCL_1 H1K_def by auto + thus "x \\<^bsub>GHK\<^esub> h \\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \ H1K" using xhx_egal by simp + qed + qed +qed + + +lemma (in group) normal_inter_subgroup : + assumes "subgroup H G" + and "N \ G" + shows "(N\H) \ (G\carrier := H\)" +proof - + define K where "K = carrier G" + have "G\carrier := K\ = G" using K_def by auto + moreover have "subgroup K G" using K_def subgroup_self by blast + moreover have "normal N (G \carrier :=K\)" using assms K_def by simp + ultimately have "N \ H \ G\carrier := K \ H\" + using normal_inter[of K H N] assms(1) by blast + moreover have "K \ H = H" using K_def assms subgroup_imp_subset by blast + ultimately show "normal (N\H) (G\carrier := H\)" by auto +qed + + + +text \Lemmas about normalizer\ + + +lemma (in group) subgroup_in_normalizer: + assumes "subgroup H G" + shows "normal H (G\carrier:= (normalizer G H)\)" +proof(intro group.normal_invI) + show "Group.group (G\carrier := normalizer G H\)" + by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup_imp_subset) + have K:"H \ (normalizer G H)" unfolding normalizer_def + proof + fix x assume xH: "x \ H" + from xH have xG : "x \ carrier G" using subgroup_imp_subset assms by auto + have "x <# H = H" + by (metis \x \ H\ assms group.lcos_mult_one is_group + l_repr_independence one_closed subgroup_imp_subset) + moreover have "H #> inv x = H" + by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed) + ultimately have "x <# H #> (inv x) = H" by simp + thus " x \ stabilizer G (\g. \H\{H. H \ carrier G}. g <# H #> inv g) H" + using assms xG subgroup_imp_subset unfolding stabilizer_def by auto + qed + thus "subgroup H (G\carrier:= (normalizer G H)\)" + using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup_imp_subset) + show " \x h. x \ carrier (G\carrier := normalizer G H\) \ h \ H \ + x \\<^bsub>G\carrier := normalizer G H\\<^esub> h + \\<^bsub>G\carrier := normalizer G H\\<^esub> inv\<^bsub>G\carrier := normalizer G H\\<^esub> x \ H" + proof- + fix x h assume xnorm : "x \ carrier (G\carrier := normalizer G H\)" and hH : "h \ H" + have xnormalizer:"x \ normalizer G H" using xnorm by simp + moreover have hnormalizer:"h \ normalizer G H" using hH K by auto + ultimately have "x \\<^bsub>G\carrier := normalizer G H\\<^esub> h = x \ h" by simp + moreover have " inv\<^bsub>G\carrier := normalizer G H\\<^esub> x = inv x" + using xnormalizer + by (simp add: assms normalizer_imp_subgroup subgroup_imp_subset subgroup_inv_equality) + ultimately have xhxegal: "x \\<^bsub>G\carrier := normalizer G H\\<^esub> h + \\<^bsub>G\carrier := normalizer G H\\<^esub> inv\<^bsub>G\carrier := normalizer G H\\<^esub> x + = x \h \ inv x" + using hnormalizer by simp + have "x \h \ inv x \ (x <# H #> inv x)" + unfolding l_coset_def r_coset_def using hH by auto + moreover have "x <# H #> inv x = H" + using xnormalizer assms subgroup_imp_subset[OF assms] + unfolding normalizer_def stabilizer_def by auto + ultimately have "x \h \ inv x \ H" by simp + thus " x \\<^bsub>G\carrier := normalizer G H\\<^esub> h + \\<^bsub>G\carrier := normalizer G H\\<^esub> inv\<^bsub>G\carrier := normalizer G H\\<^esub> x \ H" + using xhxegal hH xnorm by simp + qed +qed + + +lemma (in group) normal_imp_subgroup_normalizer : + assumes "subgroup H G" +and "N \ (G\carrier := H\)" +shows "subgroup H (G\carrier := normalizer G N\)" +proof- + have N_carrierG : "N \ carrier(G)" + using assms normal_imp_subgroup subgroup_imp_subset + by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1)) + {have "H \ normalizer G N" unfolding normalizer_def stabilizer_def + proof + fix x assume xH : "x \ H" + hence xcarrierG : "x \ carrier(G)" using assms subgroup_imp_subset by auto + have " N #> x = x <# N" using assms xH + unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto + hence "x <# N #> inv x =(N #> x) #> inv x" + by simp + also have "... = N #> \" + using assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp + finally have "x <# N #> inv x = N" by (simp add: N_carrierG) + thus "x \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) N = N}" + using xcarrierG by (simp add : N_carrierG) + qed} + thus "subgroup H (G\carrier := normalizer G N\)" + using subgroup_incl[OF assms(1) normalizer_imp_subgroup] + assms normal_imp_subgroup subgroup_imp_subset + by (metis group.incl_subgroup is_group) +qed + + +subsection \Second Isomorphism Theorem\ + + +lemma (in group) mult_norm_subgroup : + assumes "normal N G" + and "subgroup H G" + shows "subgroup (N<#>H) G" unfolding subgroup_def +proof- + have A :"N <#> H \ carrier G" + using assms setmult_subset_G by (simp add: normal_imp_subgroup subgroup_imp_subset) + + have B :"\ x y. \x \ (N <#> H); y \ (N <#> H)\ \ (x \ y) \ (N<#>H)" + proof- + fix x y assume B1a: "x \ (N <#> H)" and B1b: "y \ (N <#> H)" + obtain n1 h1 where B2:"n1 \ N \ h1 \ H \ n1\h1 = x" + using set_mult_def B1a by (metis (no_types, lifting) UN_E singletonD) + obtain n2 h2 where B3:"n2 \ N \ h2 \ H \ n2\h2 = y" + using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD) + have "N #> h1 = h1 <# N" + using normalI B2 assms normal.coset_eq subgroup_imp_subset by blast + hence "h1\n2 \ N #> h1" + using B2 B3 assms l_coset_def by fastforce + from this obtain y2 where y2_def:"y2 \ N" and y2_prop:"y2\h1 = h1\n2" + using singletonD by (metis (no_types, lifting) UN_E r_coset_def) + have " x\y = n1 \ y2 \ h1 \ h2" using y2_def B2 B3 + by (smt assms y2_prop m_assoc m_closed normal_imp_subgroup subgroup.mem_carrier) + moreover have B4 :"n1 \ y2 \N" + using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def) + moreover have "h1 \ h2 \H" using B2 B3 assms by (simp add: subgroup.m_closed) + hence "(n1 \ y2) \ (h1 \ h2) \(N<#>H) " + using B4 unfolding set_mult_def by auto + hence "n1 \ y2 \ h1 \ h2 \(N<#>H)" + using m_assoc B2 B3 assms normal_imp_subgroup by (metis B4 subgroup.mem_carrier) + ultimately show "x \ y \ N <#> H" by auto + qed + have C :"\ x. x\(N<#>H) \ (inv x)\(N<#>H)" + + proof- + fix x assume C1 : "x \ (N<#>H)" + obtain n h where C2:"n \ N \ h \ H \ n\h = x" + using set_mult_def C1 by (metis (no_types, lifting) UN_E singletonD) + have C3 :"inv(n\h) = inv(h)\inv(n)" + by (meson C2 assms inv_mult_group normal_imp_subgroup subgroup.mem_carrier) + hence "... \h \ N" + using assms C2 + by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier) + hence C4:"(inv h \ inv n \ h) \ inv h \ (N<#>H)" + using C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto + have "inv h \ inv n \ h \ inv h = inv h \ inv n" + using subgroup_imp_subset[OF assms(2)] + by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE) + thus "inv(x)\N<#>H" using C4 C2 C3 by simp + qed + + have D : "\ \ N <#> H" + proof- + have D1 : "\ \ N" + using assms by (simp add: normal_def subgroup.one_closed) + have D2 :"\ \ H" + using assms by (simp add: subgroup.one_closed) + thus "\ \ (N <#> H)" + using set_mult_def D1 assms by fastforce + qed + thus "(N <#> H \ carrier G \ (\x y. x \ N <#> H \ y \ N <#> H \ x \ y \ N <#> H)) \ + \ \ N <#> H \ (\x. x \ N <#> H \ inv x \ N <#> H)" using A B C D assms by blast +qed + + +lemma (in group) mult_norm_sub_in_sub : + assumes "normal N (G\carrier:=K\)" + assumes "subgroup H (G\carrier:=K\)" + assumes "subgroup K G" + shows "subgroup (N<#>H) (G\carrier:=K\)" +proof- + have Hyp:"subgroup (N <#>\<^bsub>G\carrier := K\\<^esub> H) (G\carrier := K\)" + using group.mult_norm_subgroup[where ?G = "G\carrier := K\"] assms subgroup_imp_group by auto + have "H \ carrier(G\carrier := K\)" using assms subgroup_imp_subset by blast + also have "... \ K" by simp + finally have Incl1:"H \ K" by simp + have "N \ carrier(G\carrier := K\)" using assms normal_imp_subgroup subgroup_imp_subset by blast + also have "... \ K" by simp + finally have Incl2:"N \ K" by simp + have "(N <#>\<^bsub>G\carrier := K\\<^esub> H) = (N <#> H)" + using set_mult_same_law[of K] assms Incl1 Incl2 by simp + thus "subgroup (N<#>H) (G\carrier:=K\)" using Hyp by auto +qed + + +lemma (in group) subgroup_of_normal_set_mult : + assumes "normal N G" +and "subgroup H G" +shows "subgroup H (G\carrier := N <#> H\)" +proof- + have "\ \ N" using normal_imp_subgroup assms(1) subgroup_def by blast + hence "\ <# H \ N <#> H" unfolding set_mult_def l_coset_def by blast + hence H_incl : "H \ N <#> H" + by (metis assms(2) lcos_mult_one subgroup_def) + show "subgroup H (G\carrier := N <#> H\)" + using subgroup_incl[OF assms(2) mult_norm_subgroup[OF assms(1) assms(2)] H_incl] . +qed + + +lemma (in group) normal_in_normal_set_mult : + assumes "normal N G" +and "subgroup H G" +shows "normal N (G\carrier := N <#> H\)" +proof- + have "\ \ H" using assms(2) subgroup_def by blast + hence "N #> \ \ N <#> H" unfolding set_mult_def r_coset_def by blast + hence N_incl : "N \ N <#> H" + by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def) + thus "normal N (G\carrier := N <#> H\)" + using normal_inter_subgroup[OF mult_norm_subgroup[OF assms] assms(1)] + by (simp add : inf_absorb1) +qed + + +proposition (in group) weak_snd_iso_thme : + assumes "subgroup H G" + and "N\G" + shows "(G\carrier := N<#>H\ Mod N \ G\carrier:=H\ Mod (N\H))" +proof- + define f where "f = (#>) N" + have GroupNH : "Group.group (G\carrier := N<#>H\)" + using subgroup_imp_group assms mult_norm_subgroup by simp + have HcarrierNH :"H \ carrier(G\carrier := N<#>H\)" + using assms subgroup_of_normal_set_mult subgroup_imp_subset by blast + hence HNH :"H \ N<#>H" by simp + have op_hom : "f \ hom (G\carrier := H\) (G\carrier := N <#> H\ Mod N)" unfolding hom_def + proof + have "\x . x \ carrier (G\carrier :=H\) \ + (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N x \ carrier (G\carrier := N <#> H\ Mod N)" + proof- + fix x assume "x \ carrier (G\carrier :=H\)" + hence xH : "x \ H" by simp + hence "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N x \ rcosets\<^bsub>G\carrier := N <#> H\\<^esub> N" + using HcarrierNH RCOSETS_def[where ?G = "G\carrier := N <#> H\"] by blast + thus "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N x \ carrier (G\carrier := N <#> H\ Mod N)" + unfolding FactGroup_def by simp + qed + hence "(#>\<^bsub>G\carrier := N <#> H\\<^esub>) N \ carrier (G\carrier :=H\) \ + carrier (G\carrier := N <#> H\ Mod N)" by auto + hence "f \ carrier (G\carrier :=H\) \ carrier (G\carrier := N <#> H\ Mod N)" + unfolding r_coset_def f_def by simp + moreover have "\x y. x\carrier (G\carrier := H\) \ y\carrier (G\carrier := H\) \ + f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y)" + proof- + fix x y assume "x\carrier (G\carrier := H\)" "y\carrier (G\carrier := H\)" + hence xHyH :"x \ H" "y \ H" by auto + have Nxeq :"N #>\<^bsub>G\carrier := N<#>H\\<^esub> x = N #>x" unfolding r_coset_def by simp + have Nyeq :"N #>\<^bsub>G\carrier := N<#>H\\<^esub> y = N #>y" unfolding r_coset_def by simp + + have "x \\<^bsub>G\carrier := H\\<^esub> y =x \\<^bsub>G\carrier := N<#>H\\<^esub> y" by simp + hence "N #>\<^bsub>G\carrier := N<#>H\\<^esub> x \\<^bsub>G\carrier := H\\<^esub> y + = N #>\<^bsub>G\carrier := N<#>H\\<^esub> x \\<^bsub>G\carrier := N<#>H\\<^esub> y" by simp + also have "... = (N #>\<^bsub>G\carrier := N<#>H\\<^esub> x) <#>\<^bsub>G\carrier := N<#>H\\<^esub> + (N #>\<^bsub>G\carrier := N<#>H\\<^esub> y)" + using normal.rcos_sum[OF normal_in_normal_set_mult[OF assms(2) assms(1)], of x y] + xHyH assms HcarrierNH by auto + finally show "f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y)" + unfolding FactGroup_def r_coset_def f_def using Nxeq Nyeq by auto + qed + hence "(\x\carrier (G\carrier := H\). \y\carrier (G\carrier := H\). + f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y))" by blast + ultimately show " f \ carrier (G\carrier := H\) \ carrier (G\carrier := N <#> H\ Mod N) \ + (\x\carrier (G\carrier := H\). \y\carrier (G\carrier := H\). + f (x \\<^bsub>G\carrier := H\\<^esub> y) = f(x) \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub> f(y))" + by auto + qed + hence homomorphism : "group_hom (G\carrier := H\) (G\carrier := N <#> H\ Mod N) f" + unfolding group_hom_def group_hom_axioms_def using subgroup_imp_group[OF assms(1)] + normal.factorgroup_is_group[OF normal_in_normal_set_mult[OF assms(2) assms(1)]] by auto + moreover have im_f : "(f ` carrier(G\carrier:=H\)) = carrier(G\carrier := N <#> H\ Mod N)" + proof + show "f ` carrier (G\carrier := H\) \ carrier (G\carrier := N <#> H\ Mod N)" + using op_hom unfolding hom_def using funcset_image by blast + next + show "carrier (G\carrier := N <#> H\ Mod N) \ f ` carrier (G\carrier := H\)" + proof + fix x assume p : " x \ carrier (G\carrier := N <#> H\ Mod N)" + hence "x \ \{y. \x\carrier (G\carrier := N <#> H\). y = {N #>\<^bsub>G\carrier := N <#> H\\<^esub> x}}" + unfolding FactGroup_def RCOSETS_def by auto + hence hyp :"\y. \h\carrier (G\carrier := N <#> H\). y = {N #>\<^bsub>G\carrier := N <#> H\\<^esub> h} \ x \ y" + using Union_iff by blast + from hyp obtain nh where nhNH:"nh \carrier (G\carrier := N <#> H\)" + and "x \ {N #>\<^bsub>G\carrier := N <#> H\\<^esub> nh}" + by blast + hence K: "x = (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N nh" by simp + have "nh \ N <#> H" using nhNH by simp + from this obtain n h where nN : "n \ N" and hH : " h \ H" and nhnh: "n \ h = nh" + unfolding set_mult_def by blast + have "x = (#>\<^bsub>G\carrier := N <#> H\\<^esub>) N (n \ h)" using K nhnh by simp + hence "x = (#>) N (n \ h)" using K nhnh unfolding r_coset_def by auto + also have "... = (N #> n) #>h" + using coset_mult_assoc hH nN assms subgroup_imp_subset normal_imp_subgroup + by (metis subgroup.mem_carrier) + finally have "x = (#>) N h" + using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier) + thus "x \ f ` carrier (G\carrier := H\)" using hH unfolding f_def by simp + qed + qed + moreover have ker_f :"kernel (G\carrier := H\) (G\carrier := N<#>H\ Mod N) f = N\H" + unfolding kernel_def f_def + proof- + have "{x \ carrier (G\carrier := H\). N #> x = \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub>} = + {x \ carrier (G\carrier := H\). N #> x = N}" unfolding FactGroup_def by simp + also have "... = {x \ carrier (G\carrier := H\). x \ N}" + using coset_join1 + by (metis (no_types, lifting) assms group.subgroup_self incl_subgroup is_group + normal_imp_subgroup subgroup.mem_carrier subgroup.rcos_const subgroup_imp_group) + also have "... =N \ (carrier(G\carrier := H\))" by auto + finally show "{x \ carrier (G\carrier := H\). N#>x = \\<^bsub>G\carrier := N <#> H\ Mod N\<^esub>} = N \ H" + by simp + qed + ultimately have "(G\carrier := H\ Mod N \ H) \ (G\carrier := N <#> H\ Mod N)" + using group_hom.FactGroup_iso[OF homomorphism im_f] by auto + hence "G\carrier := N <#> H\ Mod N \ G\carrier := H\ Mod N \ H" + by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_inter_subgroup) + thus "G\carrier := N <#> H\ Mod N \ G\carrier := H\ Mod N \ H" by auto +qed + + +theorem (in group) snd_iso_thme : + assumes "subgroup H G" + and "subgroup N G" + and "subgroup H (G\carrier:= (normalizer G N)\)" + shows "(G\carrier:= N<#>H\ Mod N) \ (G\carrier:= H\ Mod (H\N))" +proof- + have "G\carrier := normalizer G N, carrier := H\ + = G\carrier := H\" by simp + hence "G\carrier := normalizer G N, carrier := H\ Mod N \ H = + G\carrier := H\ Mod N \ H" by auto + moreover have "G\carrier := normalizer G N, + carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ = + G\carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\" by simp + hence "G\carrier := normalizer G N, + carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N = + G\carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N" by auto + hence "G\carrier := normalizer G N, + carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ + G\carrier := normalizer G N, carrier := H\ Mod N \ H = + (G\carrier:= N<#>H\ Mod N) \ + G\carrier := normalizer G N, carrier := H\ Mod N \ H" + using set_mult_same_law[OF normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H] + subgroup_imp_subset[OF assms(3)] + subgroup_imp_subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]] + by simp + ultimately have "G\carrier := normalizer G N, + carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ + G\carrier := normalizer G N, carrier := H\ Mod N \ H = + (G\carrier:= N<#>H\ Mod N) \ G\carrier := H\ Mod N \ H" by auto + moreover have "G\carrier := normalizer G N, + carrier := N <#>\<^bsub>G\carrier := normalizer G N\\<^esub> H\ Mod N \ + G\carrier := normalizer G N, carrier := H\ Mod N \ H" + using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF + subgroup_imp_subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]] + by simp + moreover have "H\N = N\H" using assms by auto + ultimately show "(G\carrier:= N<#>H\ Mod N) \ G\carrier := H\ Mod H \ N" by auto +qed + + +corollary (in group) snd_iso_thme_recip : + assumes "subgroup H G" + and "subgroup N G" + and "subgroup H (G\carrier:= (normalizer G N)\)" + shows "(G\carrier:= H<#>N\ Mod N) \ (G\carrier:= H\ Mod (H\N))" + by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup_imp_subset + normalizer_imp_subgroup snd_iso_thme) + + +subsection\The Zassenhaus Lemma\ + + +lemma (in group) distinc : + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" + and "K1\G\carrier:=K\" + shows "subgroup (H\K) (G\carrier:=(normalizer G (H1<#>(H\K1))) \)" +proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]]) + show "subgroup (normalizer G (H1 <#> H \ K1)) G" + using normalizer_imp_subgroup assms normal_imp_subgroup subgroup_imp_subset + by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair) +next + show "H \ K \ normalizer G (H1 <#> H \ K1)" unfolding normalizer_def stabilizer_def + proof + fix x assume xHK : "x \ H \ K" + hence xG : "{x} \ carrier G" "{inv x} \ carrier G" + using subgroup_imp_subset assms inv_closed xHK by auto + have allG : "H \ carrier G" "K \ carrier G" "H1 \ carrier G" "K1 \ carrier G" + using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+ . + have HK1_normal: "H\K1 \ (G\carrier := H \ K\)" using normal_inter[OF assms(3)assms(1)assms(4)] + by (simp add : inf_commute) + have "H \ K \ normalizer G (H \ K1)" + using subgroup_imp_subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF + assms(1)assms(3)]HK1_normal]] by auto + hence "x <# (H \ K1) #> inv x = (H \ K1)" + using xHK subgroup_imp_subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3) + normal_imp_subgroup[OF assms(4)]]]] + unfolding normalizer_def stabilizer_def by auto + moreover have "H \ normalizer G H1" + using subgroup_imp_subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto + hence "x <# H1 #> inv x = H1" + using xHK subgroup_imp_subset[OF incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]] + unfolding normalizer_def stabilizer_def by auto + ultimately have "H1 <#> H \ K1 = (x <# H1 #> inv x) <#> (x <# H \ K1 #> inv x)" by auto + also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H \ K1 <#> {inv x})" + by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult) + also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#> (H \ K1 <#> {inv x})" + by (smt Int_lower1 allG xG set_mult_assoc subset_trans setmult_subset_G) + also have "... = ({x} <#> H1 <#> {\}) <#> (H \ K1 <#> {inv x})" + using allG xG coset_mult_assoc by (simp add: r_coset_eq_set_mult setmult_subset_G) + also have "... =({x} <#> H1) <#> (H \ K1 <#> {inv x})" + using coset_mult_one r_coset_eq_set_mult[of G H1 \] set_mult_assoc[OF xG(1) allG(3)] allG + by auto + also have "... = {x} <#> (H1 <#> H \ K1) <#> {inv x}" + using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2) + finally have "H1 <#> H \ K1 = x <# (H1 <#> H \ K1) #> inv x" + using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult) + thus "x \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) (H1 <#> H \ K1) + = H1 <#> H \ K1}" + using xG allG setmult_subset_G[OF allG(3), where ?K = "H\K1"] xHK + by auto + qed +qed + +lemma (in group) preliminary1 : + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" + and "K1\G\carrier:=K\" + shows " (H\K) \ (H1<#>(H\K1)) = (H1\K)<#>(H\K1)" +proof + have all_inclG : "H \ carrier G" "H1 \ carrier G" "K \ carrier G" "K1 \ carrier G" + using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+. + show "H \ K \ (H1 <#> H \ K1) \ H1 \ K <#> H \ K1" + proof + fix x assume x_def : "x \ (H \ K) \ (H1 <#> (H \ K1))" + from x_def have x_incl : "x \ H" "x \ K" "x \ (H1 <#> (H \ K1))" by auto + then obtain h1 hk1 where h1hk1_def : "h1 \ H1" "hk1 \ H \ K1" "h1 \ hk1 = x" + using assms unfolding set_mult_def by blast + hence "hk1 \ H \ K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(4)]] by auto + hence "inv hk1 \ H \ K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto + moreover have "h1 \ hk1 \ H \ K" using x_incl h1hk1_def by auto + ultimately have "h1 \ hk1 \ inv hk1 \ H \ K" + using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto + hence "h1 \ H \ K" using h1hk1_def assms subgroup_imp_subset incl_subgroup normal_imp_subgroup + by (metis Int_iff contra_subsetD inv_solve_right m_closed) + hence "h1 \ H1 \ H \ K" using h1hk1_def by auto + hence "h1 \ H1 \ K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(2)]] by auto + hence "h1 \ hk1 \ (H1\K)<#>(H\K1)" + using h1hk1_def unfolding set_mult_def by auto + thus " x \ (H1\K)<#>(H\K1)" using h1hk1_def x_def by auto + qed + show "H1 \ K <#> H \ K1 \ H \ K \ (H1 <#> H \ K1)" + proof- + have "H1 \ K \ H \ K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(2)]] by auto + moreover have "H \ K1 \ H \ K" + using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(4)]] by auto + ultimately have "H1 \ K <#> H \ K1 \ H \ K" unfolding set_mult_def + using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast + moreover have "H1 \ K \ H1" by auto + hence "H1 \ K <#> H \ K1 \ (H1 <#> H \ K1)" unfolding set_mult_def by auto + ultimately show "H1 \ K <#> H \ K1 \ H \ K \ (H1 <#> H \ K1)" by auto + qed +qed + +lemma (in group) preliminary2 : + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" + and "K1\G\carrier:=K\" + shows "(H1<#>(H\K1)) \ G\carrier:=(H1<#>(H\K))\" +proof- + have all_inclG : "H \ carrier G" "H1 \ carrier G" "K \ carrier G" "K1 \ carrier G" + using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+. + have subH1:"subgroup (H1 <#> H \ K) (G\carrier := H\)" + using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)] + assms(1)]] assms by auto + have "Group.group (G\carrier:=(H1<#>(H\K))\)" + using subgroup_imp_group[OF incl_subgroup[OF assms(1) subH1]]. + moreover have subH2 : "subgroup (H1 <#> H \ K1) (G\carrier := H\)" + using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF + assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto + hence "(H\K1) \ (H\K)" + using assms subgroup_imp_subset normal_imp_subgroup monoid.cases_scheme + by (metis inf.mono partial_object.simps(1) partial_object.update_convs(1) subset_refl) + hence incl:"(H1<#>(H\K1)) \ H1<#>(H\K)" using assms subgroup_imp_subset normal_imp_subgroup + unfolding set_mult_def by blast + hence "subgroup (H1 <#> H \ K1) (G\carrier := (H1<#>(H\K))\)" + using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1) + subH1]] normal_imp_subgroup subgroup_imp_subset unfolding set_mult_def by blast + moreover have " (\ x. x\carrier (G\carrier := H1 <#> H \ K\) \ + H1 <#> H\K1 #>\<^bsub>G\carrier := H1 <#> H\K\\<^esub> x = x <#\<^bsub>G\carrier := H1 <#> H\K\\<^esub> (H1 <#> H\K1))" + proof- + fix x assume "x \carrier (G\carrier := H1 <#> H \ K\)" + hence x_def : "x \ H1 <#> H \ K" by simp + from this obtain h1 hk where h1hk_def :"h1 \ H1" "hk \ H \ K" "h1 \ hk = x" + unfolding set_mult_def by blast + have xH : "x \ H" using subgroup_imp_subset[OF subH1] using x_def by auto + hence allG : "h1 \ carrier G" "hk \ carrier G" "x \ carrier G" + using assms subgroup_imp_subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+. + hence "x <#\<^bsub>G\carrier := H1 <#> H\K\\<^esub> (H1 <#> H\K1) =h1 \ hk <# (H1 <#> H\K1)" + using set_mult_same_law subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def) + also have "... = h1 <# (hk <# (H1 <#> H\K1))" + using lcos_m_assoc[OF subgroup_imp_subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)] + by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup_imp_subset) + also have "... = h1 <# (hk <# H1 <#> H\K1)" + using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1) + also have "... = h1 <# (hk <# H1 #> \ <#> H\K1 #> \)" + using coset_mult_one allG all_inclG l_coset_subset_G + by (smt inf_le2 setmult_subset_G subset_trans) + also have "... = h1 <# (hk <# H1 #> inv hk #> hk <#> H\K1 #> inv hk #> hk)" + using all_inclG allG coset_mult_assoc l_coset_subset_G + by (simp add: inf.coboundedI1 setmult_subset_G) + finally have "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = + h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\K1 #> inv hk) #> hk)" + using rcos_assoc_lcos allG all_inclG + by (smt inf_le1 inv_closed l_coset_subset_G r_coset_subset_G setmult_rcos_assoc subset_trans) + moreover have "H \ normalizer G H1" + using assms h1hk_def subgroup_imp_subset[OF normal_imp_subgroup_normalizer] by simp + hence "\g. g \ H \ g \ {g \ carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) H1 = H1}" + using all_inclG assms unfolding normalizer_def stabilizer_def by auto + hence "\g. g \ H \ g <# H1 #> inv g = H1" using all_inclG by simp + hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp + moreover have "H\K \ normalizer G (H\K1)" + using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair + subgroup_imp_subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute) + hence "\g. g\H\K \ g\{g\carrier G. (\H\{H. H \ carrier G}. g <# H #> inv g) (H\K1) = H\K1}" + using all_inclG assms unfolding normalizer_def stabilizer_def by auto + hence "\g. g \ H\K \ g <# (H\K1) #> inv g = H\K1" + using subgroup_imp_subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF + assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto + hence "(hk <# H\K1 #> inv hk) = H\K1" using h1hk_def by simp + ultimately have "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = h1 <#(H1 <#> (H \ K1)#> hk)" + by auto + also have "... = h1 <# H1 <#> ((H \ K1)#> hk)" + using set_mult_assoc[where ?M = "{h1}" and ?H = "H1" and ?K = "(H \ K1)#> hk"] allG all_inclG + by (simp add: l_coset_eq_set_mult inf.coboundedI2 r_coset_subset_G setmult_rcos_assoc) + also have "... = H1 <#> ((H \ K1)#> hk)" + using coset_join3 allG incl_subgroup[OF assms(1)normal_imp_subgroup[OF assms(2)]] h1hk_def + by auto + finally have eq1 : "x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1) = H1 <#> (H \ K1) #> hk" + by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc) + have "H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x = H1 <#> H \ K1 #> (h1 \ hk)" + using set_mult_same_law subgroup_imp_subset xH h1hk_def by (simp add: r_coset_def) + also have "... = H1 <#> H \ K1 #> h1 #> hk" + using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G) + also have"... = H \ K1 <#> H1 #> h1 #> hk" + using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF + assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp + also have "... = H \ K1 <#> H1 #> hk" + using coset_join2[OF allG(1)incl_subgroup[OF assms(1)normal_imp_subgroup] + h1hk_def(1)] all_inclG allG assms by (metis inf.coboundedI2 setmult_rcos_assoc) + finally have "H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x =H1 <#> H \ K1 #> hk" + using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF + assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp + thus " H1 <#> H \ K1 #>\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> x = + x <#\<^bsub>G\carrier := H1 <#> H \ K\\<^esub> (H1 <#> H \ K1)" using eq1 by simp + qed + ultimately show "H1 <#> H \ K1 \ G\carrier := H1 <#> H \ K\" + unfolding normal_def normal_axioms_def by auto +qed + + +proposition (in group) Zassenhaus_1 : + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" + and "K1\G\carrier:=K\" + shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>H\K1)) \ (G\carrier:= (H\K)\ Mod ((H1\K)<#>(H\K1)))" +proof- + define N and N1 where "N = (H\K)" and "N1 =H1<#>(H\K1)" + have normal_N_N1 : "subgroup N (G\carrier:=(normalizer G N1)\)" + by (simp add: N1_def N_def assms distinc normal_imp_subgroup) + have Hp:"(G\carrier:= N<#>N1\ Mod N1) \ (G\carrier:= N\ Mod (N\N1))" + by (metis N1_def N_def assms incl_subgroup inf_le1 mult_norm_sub_in_sub + normal_N_N1 normal_imp_subgroup snd_iso_thme_recip subgroup_incl subgroups_Inter_pair) + have H_simp: "N<#>N1 = H1<#> (H\K)" + proof- + have H1_incl_G : "H1 \ carrier G" + using assms normal_imp_subgroup incl_subgroup subgroup_imp_subset by blast + have K1_incl_G :"K1 \ carrier G" + using assms normal_imp_subgroup incl_subgroup subgroup_imp_subset by blast + have "N<#>N1= (H\K)<#> (H1<#>(H\K1))" by (auto simp add: N_def N1_def) + also have "... = ((H\K)<#>H1) <#>(H\K1)" + using set_mult_assoc[where ?M = "H\K"] K1_incl_G H1_incl_G assms + by (simp add: inf.coboundedI2 subgroup_imp_subset) + also have "... = (H1<#>(H\K))<#>(H\K1)" + using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto + also have "... = H1 <#> ((H\K)<#>(H\K1))" + using set_mult_assoc K1_incl_G H1_incl_G assms + by (simp add: inf.coboundedI2 subgroup_imp_subset) + also have " ((H\K)<#>(H\K1)) = (H\K)" + proof (intro set_mult_subgroup_idem[where ?H = "H\K" and ?N="H\K1", + OF subgroups_Inter_pair[OF assms(1) assms(3)]]) + show "subgroup (H \ K1) (G\carrier := H \ K\)" + using subgroup_incl[where ?I = "H\K1" and ?J = "H\K",OF subgroups_Inter_pair[OF assms(1) + incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms + normal_imp_subgroup by (metis inf_commute normal_inter) + qed + hence " H1 <#> ((H\K)<#>(H\K1)) = H1 <#> ((H\K))" + by simp + thus "N <#> N1 = H1 <#> H \ K" + by (simp add: calculation) + qed + + have "N\N1 = (H1\K)<#>(H\K1)" + using preliminary1 assms N_def N1_def by simp + thus "(G\carrier:= H1 <#> (H\K)\ Mod N1) \ (G\carrier:= N\ Mod ((H1\K)<#>(H\K1)))" + using H_simp Hp by auto +qed + + +theorem (in group) Zassenhaus : + assumes "subgroup H G" + and "H1\G\carrier := H\" + and "subgroup K G" + and "K1\G\carrier:=K\" + shows "(G\carrier:= H1 <#> (H\K)\ Mod (H1<#>(H\K1))) \ + (G\carrier:= K1 <#> (H\K)\ Mod (K1<#>(K\H1)))" +proof- + define Gmod1 Gmod2 Gmod3 Gmod4 + where "Gmod1 = (G\carrier:= H1 <#> (H\K)\ Mod (H1<#>(H\K1))) " + and "Gmod2 = (G\carrier:= K1 <#> (K\H)\ Mod (K1<#>(K\H1)))" + and "Gmod3 = (G\carrier:= (H\K)\ Mod ((H1\K)<#>(H\K1)))" + and "Gmod4 = (G\carrier:= (K\H)\ Mod ((K1\H)<#>(K\H1)))" + have Hyp : "Gmod1 \ Gmod3" "Gmod2 \ Gmod4" + using Zassenhaus_1 assms Gmod1_def Gmod2_def Gmod3_def Gmod4_def by auto + have Hp : "Gmod3 = G\carrier:= (K\H)\ Mod ((K\H1)<#>(K1\H))" + by (simp add: Gmod3_def inf_commute) + have "(K\H1)<#>(K1\H) = (K1\H)<#>(K\H1)" + proof (intro commut_normal_subgroup[OF subgroups_Inter_pair[OF assms(1)assms(3)]]) + show "K1 \ H \ G\carrier := H \ K\" + using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute) + next + show "subgroup (K \ H1) (G\carrier := H \ K\)" + using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter) + qed + hence "Gmod3 = Gmod4" using Hp Gmod4_def by simp + hence "Gmod1 \ Gmod2" + using group.iso_sym group.iso_trans Hyp normal.factorgroup_is_group + by (metis assms Gmod1_def Gmod2_def preliminary2) + thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute) +qed + +end diff -r 46beee72fb66 -r ff61cbfb3f2d src/HOL/ROOT --- a/src/HOL/ROOT Tue Jun 12 16:21:52 2018 +0200 +++ b/src/HOL/ROOT Tue Jun 12 16:09:12 2018 +0100 @@ -302,6 +302,8 @@ More_Group More_Finite_Product Multiplicative_Group + Zassenhaus (* The Zassenhaus lemma *) + (* Rings *) Divisibility (* Rings *)