only one version of group.rcos_self;
authorwenzelm
Mon Mar 17 22:34:23 2008 +0100 (2008-03-17)
changeset 26310f8a7fac36e13
parent 26309 fb52fe23acc4
child 26311 81a0fc28b0de
only one version of group.rcos_self;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Coset.thy
     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.16 -apply (simp add: ); 
    2.17 +apply (simp add: ) 
    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.25 -apply (simp add: ); 
    2.26 +apply (simp add: ) 
    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.37 -apply (simp add: r_coset_def)
    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) 
    2.62 -apply (simp add: G.m_assoc); 
    2.63 +apply (simp add: G.m_assoc) 
    2.64  done
    2.65  
    2.66  lemma (in group_hom) FactGroup_inj_on:
    2.67 @@ -977,7 +969,7 @@
    2.68      fix y
    2.69      assume y: "y \<in> carrier H"
    2.70      with h obtain g where g: "g \<in> carrier G" "h g = y"
    2.71 -      by (blast elim: equalityE); 
    2.72 +      by (blast elim: equalityE) 
    2.73      hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
    2.74        by (auto simp add: y kernel_def r_coset_def) 
    2.75      with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"