# HG changeset patch # User ballarin # Date 1049206114 -7200 # Node ID 6676ac2527fa8763120308ae99a096150f7233cb # Parent 16f424af58a2a2b0bc453d4519fff207a8f0ec99 Fixed Coset.thy (proved theorem factorgroup_is_group). diff -r 16f424af58a2 -r 6676ac2527fa src/HOL/Algebra/CRing.thy --- a/src/HOL/Algebra/CRing.thy Mon Mar 31 12:29:54 2003 +0200 +++ b/src/HOL/Algebra/CRing.thy Tue Apr 01 16:08:34 2003 +0200 @@ -16,17 +16,21 @@ zero :: 'a ("\\") add :: "['a, 'a] => 'a" (infixl "\\" 65) a_inv :: "'a => 'a" ("\\ _" [81] 80) - minus :: "['a, 'a] => 'a" (infixl "\\" 65) locale cring = abelian_monoid R + assumes a_abelian_group: "abelian_group (| carrier = carrier R, mult = add R, one = zero R, m_inv = a_inv R |)" - and minus_def: "[| x \ carrier R; y \ carrier R |] ==> x \ y = x \ \ y" and m_inv_def: "[| EX y. y \ carrier R & x \ y = \; x \ carrier R |] ==> inv x = (THE y. y \ carrier R & x \ y = \)" and l_distr: "[| x \ carrier R; y \ carrier R; z \ carrier R |] ==> (x \ y) \ z = x \ z \ y \ z" +text {* Derived operation. *} + +constdefs + minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\\" 65) + "[| x \ carrier R; y \ carrier R |] ==> minus R x y == add R x (a_inv R y)" + (* -- {* Definition of derived operations *} @@ -289,8 +293,8 @@ abelian_monoid.finprod_multf [OF a_abelian_monoid, folded finsum_def, simplified group_record_simps] -lemmas (in cring) finsum_cong = - abelian_monoid.finprod_cong [OF a_abelian_monoid, folded finsum_def, +lemmas (in cring) finsum_cong' = + abelian_monoid.finprod_cong' [OF a_abelian_monoid, folded finsum_def, simplified group_record_simps] lemmas (in cring) finsum_0 [simp] = @@ -309,93 +313,10 @@ abelian_monoid.finprod_mult [OF a_abelian_monoid, folded finsum_def, simplified group_record_simps] -lemmas (in cring) finsum_cong' [cong] = - abelian_monoid.finprod_cong' [OF a_abelian_monoid, folded finsum_def, +lemmas (in cring) finsum_cong = + abelian_monoid.finprod_cong [OF a_abelian_monoid, folded finsum_def, simplified group_record_simps] -(* -lemma (in cring) finsum_empty [simp]: - "finsum R f {} = \" - by (simp add: finsum_def - abelian_monoid.finprod_empty [OF a_abelian_monoid]) - -lemma (in cring) finsum_insert [simp]: - "[| finite F; a \ F; f : F -> carrier R; f a \ carrier R |] ==> - finsum R f (insert a F) = f a \ finsum R f F" - by (simp add: finsum_def - abelian_monoid.finprod_insert [OF a_abelian_monoid]) - -lemma (in cring) finsum_zero: - "finite A ==> finsum R (%i. \) A = \" - by (simp add: finsum_def - abelian_monoid.finprod_one [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_closed [simp]: - "[| finite A; f : A -> carrier R |] ==> finsum R f A \ carrier R" - by (simp only: finsum_def - abelian_monoid.finprod_closed [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_Un_Int: - "[| finite A; finite B; g \ A -> carrier R; g \ B -> carrier R |] ==> - finsum R g (A Un B) \ finsum R g (A Int B) = - finsum R g A \ finsum R g B" - by (simp only: finsum_def - abelian_monoid.finprod_Un_Int [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_Un_disjoint: - "[| finite A; finite B; A Int B = {}; - g \ A -> carrier R; g \ B -> carrier R |] - ==> finsum R g (A Un B) = finsum R g A \ finsum R g B" - by (simp only: finsum_def - abelian_monoid.finprod_Un_disjoint [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_addf: - "[| finite A; f \ A -> carrier R; g \ A -> carrier R |] ==> - finsum R (%x. f x \ g x) A = (finsum R f A \ finsum R g A)" - by (simp only: finsum_def - abelian_monoid.finprod_multf [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_cong: - "[| A = B; g : B -> carrier R; - !!i. i : B ==> f i = g i |] ==> finsum R f A = finsum R g B" - apply (simp only: finsum_def) - apply (rule abelian_monoid.finprod_cong [OF a_abelian_monoid, simplified]) - apply simp_all - done - -lemma (in cring) finsum_0 [simp]: - "f \ {0::nat} -> carrier R ==> finsum R f {..0} = f 0" - by (simp add: finsum_def - abelian_monoid.finprod_0 [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_Suc [simp]: - "f \ {..Suc n} -> carrier R ==> - finsum R f {..Suc n} = (f (Suc n) \ finsum R f {..n})" - by (simp add: finsum_def - abelian_monoid.finprod_Suc [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_Suc2: - "f \ {..Suc n} -> carrier R ==> - finsum R f {..Suc n} = (finsum R (%i. f (Suc i)) {..n} \ f 0)" - by (simp only: finsum_def - abelian_monoid.finprod_Suc2 [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_add [simp]: - "[| f : {..n} -> carrier R; g : {..n} -> carrier R |] ==> - finsum R (%i. f i \ g i) {..n::nat} = - finsum R f {..n} \ finsum R g {..n}" - by (simp only: finsum_def - abelian_monoid.finprod_mult [OF a_abelian_monoid, simplified]) - -lemma (in cring) finsum_cong' [cong]: - "[| A = B; !!i. i : B ==> f i = g i; - g \ B -> carrier R = True |] ==> finsum R f A = finsum R g B" - apply (simp only: finsum_def) - apply (rule abelian_monoid.finprod_cong' [OF a_abelian_monoid, simplified]) - apply simp_all - done -*) - text {*Usually, if this rule causes a failed congruence proof error, the reason is that the premise @{text "g \ B -> carrier G"} cannot be shown. Adding @{thm [source] Pi_def} to the simpset is often useful. *} diff -r 16f424af58a2 -r 6676ac2527fa src/HOL/Algebra/Coset.thy --- a/src/HOL/Algebra/Coset.thy Mon Mar 31 12:29:54 2003 +0200 +++ b/src/HOL/Algebra/Coset.thy Tue Apr 01 16:08:34 2003 +0200 @@ -40,6 +40,13 @@ and lcos_def: "x <# H == l_coset G x H" and setmult_def: "H <#> K == set_mult G H K" +text {* + Locale @{term coset} provides only syntax. + Logically, groups are cosets. +*} +lemma (in group) is_coset: + "coset G" + .. text{*Lemmas useful for Sylow's Theorem*} @@ -413,7 +420,15 @@ by (auto simp add: normal_imp_subgroup [THEN subgroup.subset] rcos_sum setrcos_eq) +lemma (in group) setinv_closed: + "[| H <| G; K \ rcosets G H |] ==> set_inv G K \ rcosets G H" +by (auto simp add: normal_imp_subgroup + subgroup.subset coset.rcos_inv [OF is_coset] + coset.setrcos_eq [OF is_coset]) + (* +The old version is no longer valid: "group G" has to be an explicit premise. + lemma setinv_closed: "[| H <| G; K \ rcosets G H |] ==> set_inv G K \ rcosets G H" by (auto simp add: normal_imp_subgroup @@ -426,8 +441,20 @@ by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup subgroup.subset m_assoc) -(*?? -lemma subgroup_in_rcosets: "subgroup H G ==> H \ rcosets G H" +lemma (in group) subgroup_in_rcosets: + "subgroup H G ==> H \ rcosets G H" +proof - + assume sub: "subgroup H G" + have "r_coset G H \ = H" + by (rule coset.coset_join2) + (auto intro: sub subgroup.one_closed is_coset) + then show ?thesis + by (auto simp add: coset.setrcos_eq [OF is_coset]) +qed + +(* +lemma subgroup_in_rcosets: + "subgroup H G ==> H \ rcosets G H" apply (frule subgroup_imp_coset) apply (frule subgroup_imp_group) apply (simp add: coset.setrcos_eq) @@ -442,6 +469,33 @@ by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup subgroup.subset) +lemma (in group) factorgroup_is_magma: + "H <| G ==> magma (G Mod H)" + by rule (simp add: FactGroup_def coset.setmult_closed [OF is_coset]) + +lemma (in group) factorgroup_semigroup_axioms: + "H <| G ==> semigroup_axioms (G Mod H)" + by rule (simp add: FactGroup_def coset.setrcos_assoc [OF is_coset] + coset.setmult_closed [OF is_coset]) + +theorem (in group) factorgroup_is_group: + "H <| G ==> group (G Mod H)" +apply (insert is_coset) +apply (simp add: FactGroup_def) +apply (rule group.intro) + apply (rule magma.intro) + apply (simp add: coset.setmult_closed) + apply (rule semigroup_axioms.intro) + apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc) + apply (rule l_one.intro) + apply (simp add: normal_imp_subgroup subgroup_in_rcosets) + apply (simp add: normal_imp_subgroup + subgroup_in_rcosets coset.setrcos_mult_eq) +apply (rule group_axioms.intro) + apply (simp add: restrictI setinv_closed) +apply (simp add: setinv_closed coset.setrcos_inv_mult_group_eq) +done + (*???????????????? theorem factorgroup_is_group: "H <| G ==> group (G Mod H)" apply (frule normal_imp_coset) diff -r 16f424af58a2 -r 6676ac2527fa src/HOL/Algebra/Summation.thy --- a/src/HOL/Algebra/Summation.thy Mon Mar 31 12:29:54 2003 +0200 +++ b/src/HOL/Algebra/Summation.thy Tue Apr 01 16:08:34 2003 +0200 @@ -416,7 +416,7 @@ by (simp add: insert fA fa gA ga fgA fga ac finprod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff) qed -lemma (in abelian_monoid) finprod_cong: +lemma (in abelian_monoid) finprod_cong': "[| A = B; g : B -> carrier G; !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B" proof - @@ -457,14 +457,17 @@ qed qed -lemma (in abelian_monoid) finprod_cong' [cong]: +lemma (in abelian_monoid) finprod_cong: "[| A = B; !!i. i : B ==> f i = g i; g : B -> carrier G = True |] ==> finprod G f A = finprod G g B" - by (rule finprod_cong) fast+ + by (rule finprod_cong') fast+ text {*Usually, if this rule causes a failed congruence proof error, - the reason is that the premise @{text "g : B -> carrier G"} cannot be shown. - Adding @{thm [source] Pi_def} to the simpset is often useful. *} + the reason is that the premise @{text "g : B -> carrier G"} cannot be shown. + Adding @{thm [source] Pi_def} to the simpset is often useful. + For this reason, @{thm [source] abelian_monoid.finprod_cong} + is not added to the simpset by default. +*} declare funcsetI [rule del] funcset_mem [rule del]