src/HOL/Algebra/Coset.thy
changeset 39910 10097e0a9dbd
parent 35849 b5522b51cb1e
child 40815 6e2d17cc0d1d
     1.1 --- a/src/HOL/Algebra/Coset.thy	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -924,9 +924,9 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -lemma (in group_hom) FactGroup_contents_mem:
     1.8 +lemma (in group_hom) FactGroup_the_elem_mem:
     1.9    assumes X: "X \<in> carrier (G Mod (kernel G H h))"
    1.10 -  shows "contents (h`X) \<in> carrier H"
    1.11 +  shows "the_elem (h`X) \<in> carrier H"
    1.12  proof -
    1.13    from X
    1.14    obtain g where g: "g \<in> carrier G" 
    1.15 @@ -937,8 +937,8 @@
    1.16  qed
    1.17  
    1.18  lemma (in group_hom) FactGroup_hom:
    1.19 -     "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
    1.20 -apply (simp add: hom_def FactGroup_contents_mem  normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
    1.21 +     "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
    1.22 +apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
    1.23  proof (intro ballI)
    1.24    fix X and X'
    1.25    assume X:  "X  \<in> carrier (G Mod kernel G H h)"
    1.26 @@ -955,7 +955,7 @@
    1.27      by (auto dest!: FactGroup_nonempty
    1.28               simp add: set_mult_def image_eq_UN 
    1.29                         subsetD [OF Xsub] subsetD [OF X'sub]) 
    1.30 -  thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
    1.31 +  thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
    1.32      by (simp add: all image_eq_UN FactGroup_nonempty X X')
    1.33  qed
    1.34  
    1.35 @@ -971,7 +971,7 @@
    1.36  done
    1.37  
    1.38  lemma (in group_hom) FactGroup_inj_on:
    1.39 -     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
    1.40 +     "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
    1.41  proof (simp add: inj_on_def, clarify) 
    1.42    fix X and X'
    1.43    assume X:  "X  \<in> carrier (G Mod kernel G H h)"
    1.44 @@ -983,7 +983,7 @@
    1.45      by (auto simp add: FactGroup_def RCOSETS_def)
    1.46    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
    1.47      by (force simp add: kernel_def r_coset_def image_def)+
    1.48 -  assume "contents (h ` X) = contents (h ` X')"
    1.49 +  assume "the_elem (h ` X) = the_elem (h ` X')"
    1.50    hence h: "h g = h g'"
    1.51      by (simp add: image_eq_UN all FactGroup_nonempty X X') 
    1.52    show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
    1.53 @@ -993,11 +993,11 @@
    1.54  homomorphism from the quotient group*}
    1.55  lemma (in group_hom) FactGroup_onto:
    1.56    assumes h: "h ` carrier G = carrier H"
    1.57 -  shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
    1.58 +  shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
    1.59  proof
    1.60 -  show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
    1.61 -    by (auto simp add: FactGroup_contents_mem)
    1.62 -  show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
    1.63 +  show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
    1.64 +    by (auto simp add: FactGroup_the_elem_mem)
    1.65 +  show "carrier H \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
    1.66    proof
    1.67      fix y
    1.68      assume y: "y \<in> carrier H"
    1.69 @@ -1005,7 +1005,7 @@
    1.70        by (blast elim: equalityE) 
    1.71      hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
    1.72        by (auto simp add: y kernel_def r_coset_def) 
    1.73 -    with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
    1.74 +    with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" 
    1.75        by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
    1.76    qed
    1.77  qed
    1.78 @@ -1015,7 +1015,7 @@
    1.79   quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
    1.80  theorem (in group_hom) FactGroup_iso:
    1.81    "h ` carrier G = carrier H
    1.82 -   \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
    1.83 +   \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
    1.84  by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
    1.85                FactGroup_onto) 
    1.86