author wenzelm Mon Mar 17 22:34:23 2008 +0100 (2008-03-17) changeset 26310 f8a7fac36e13 parent 26309 fb52fe23acc4 child 26311 81a0fc28b0de
only one version of group.rcos_self;
 src/HOL/Algebra/AbelCoset.thy file | annotate | diff | revisions src/HOL/Algebra/Coset.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Mon Mar 17 20:51:23 2008 +0100
1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Mon Mar 17 22:34:23 2008 +0100
1.3 @@ -413,7 +413,7 @@
1.4
1.5  lemma (in abelian_subgroup) a_rcos_self:
1.6    shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x"
1.7 -by (rule group.rcos_self [OF a_group a_subgroup,
1.8 +by (rule group.rcos_self [OF a_group _ a_subgroup,
1.9      folded a_r_coset_def, simplified monoid_record_simps])
1.10
1.11  lemma (in abelian_subgroup) a_rcosets_part_G:
```
```     2.1 --- a/src/HOL/Algebra/Coset.thy	Mon Mar 17 20:51:23 2008 +0100
2.2 +++ b/src/HOL/Algebra/Coset.thy	Mon Mar 17 22:34:23 2008 +0100
2.3 @@ -369,7 +369,7 @@
2.4    by (simp add: normal_def subgroup_def)
2.5
2.6  lemma (in group) normalI:
2.7 -  "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
2.8 +  "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
2.9    by (simp add: normal_def normal_axioms_def prems)
2.10
2.11  lemma (in normal) inv_op_closed1:
2.12 @@ -385,7 +385,7 @@
2.13  lemma (in normal) inv_op_closed2:
2.14       "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H"
2.15  apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H")
2.18  apply (blast intro: inv_op_closed1)
2.19  done
2.20
2.21 @@ -640,7 +640,7 @@
2.22          h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
2.23        \<Longrightarrow> hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
2.24  apply (rule UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
2.27  apply (simp add: m_assoc transpose_inv)
2.28  done
2.29
2.30 @@ -731,14 +731,6 @@
2.31    order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
2.32    "order S \<equiv> card (carrier S)"
2.33
2.34 -lemma (in group) rcos_self:
2.35 -  includes subgroup
2.36 -  shows "x \<in> carrier G \<Longrightarrow> x \<in> H #> x"
2.38 -apply (rule_tac x="\<one>" in bexI)
2.39 -apply (auto simp add: );
2.40 -done
2.41 -
2.42  lemma (in group) rcosets_part_G:
2.43    includes subgroup
2.44    shows "\<Union>(rcosets H) = carrier G"
2.45 @@ -873,7 +865,7 @@
2.46    kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>
2.47               ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
2.48      --{*the kernel of a homomorphism*}
2.49 -  "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
2.50 +  "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
2.51
2.52  lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
2.53  apply (rule subgroup.intro)
2.54 @@ -939,10 +931,10 @@
2.55  lemma (in group_hom) FactGroup_subset:
2.56       "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
2.57        \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
2.58 -apply (clarsimp simp add: kernel_def r_coset_def image_def);
2.59 +apply (clarsimp simp add: kernel_def r_coset_def image_def)
2.60  apply (rename_tac y)
2.61  apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)