Fixed Coset.thy (proved theorem factorgroup_is_group).

--- 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 ("\<zero>\<index>")
   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
   a_inv :: "'a => 'a" ("\<ominus>\<index> _" [81] 80)
-  minus :: "['a, 'a] => 'a" (infixl "\<ominus>\<index>" 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 \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y = x \<oplus> \<ominus> y"
     and m_inv_def: "[| EX y. y \<in> carrier R & x \<otimes> y = \<one>; x \<in> carrier R |]
       ==> inv x = (THE y. y \<in> carrier R & x \<otimes> y = \<one>)"
     and l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
 
+text {* Derived operation. *}
+
+constdefs
+  minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
+  "[| x \<in> carrier R; y \<in> 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 {} = \<zero>"
-  by (simp add: finsum_def
-    abelian_monoid.finprod_empty [OF a_abelian_monoid])
-
-lemma (in cring) finsum_insert [simp]:
-  "[| finite F; a \<notin> F; f : F -> carrier R; f a \<in> carrier R |] ==>
-   finsum R f (insert a F) = f a \<oplus> 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. \<zero>) A = \<zero>"
-  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 \<in> 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 \<in> A -> carrier R; g \<in> B -> carrier R |] ==>
-     finsum R g (A Un B) \<oplus> finsum R g (A Int B) =
-     finsum R g A \<oplus> 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 \<in> A -> carrier R; g \<in> B -> carrier R |]
-   ==> finsum R g (A Un B) = finsum R g A \<oplus> 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 \<in> A -> carrier R; g \<in> A -> carrier R |] ==>
-   finsum R (%x. f x \<oplus> g x) A = (finsum R f A \<oplus> 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 \<in> {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 \<in> {..Suc n} -> carrier R ==>
-   finsum R f {..Suc n} = (f (Suc n) \<oplus> finsum R f {..n})"
-  by (simp add: finsum_def
-    abelian_monoid.finprod_Suc [OF a_abelian_monoid, simplified])
-
-lemma (in cring) finsum_Suc2:
-  "f \<in> {..Suc n} -> carrier R ==>
-   finsum R f {..Suc n} = (finsum R (%i. f (Suc i)) {..n} \<oplus> 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 \<oplus> g i) {..n::nat} =
-     finsum R f {..n} \<oplus> 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 \<in> 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 \<in> B -> carrier G"} cannot be shown.
    Adding @{thm [source] Pi_def} to the simpset is often useful. *}

--- 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 \<in> rcosets G H |] ==> set_inv G K \<in> 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 \<in> rcosets G H |] ==> set_inv G K \<in> 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 \<in> rcosets G H"
+lemma (in group) subgroup_in_rcosets:
+  "subgroup H G ==> H \<in> rcosets G H"
+proof -
+  assume sub: "subgroup H G"
+  have "r_coset G H \<one> = 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 \<in> 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) 

--- 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]