src/HOL/Algebra/Coset.thy
changeset 15120 f0359f75682e
parent 14963 d584e32f7d46
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Algebra/Coset.thy	Fri Aug 06 16:54:26 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Aug 06 16:55:14 2004 +0200
     1.3 @@ -153,13 +153,13 @@
     1.4    proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
     1.5      fix x
     1.6      assume x: "x \<in> carrier G"
     1.7 -    show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) = (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
     1.8 +    show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
     1.9      proof
    1.10 -      show "(\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
    1.11 +      show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
    1.12        proof clarify
    1.13          fix n
    1.14          assume n: "n \<in> N" 
    1.15 -        show "n \<otimes> x \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h})"
    1.16 +        show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
    1.17          proof 
    1.18            from closed [of "inv x"]
    1.19            show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
    1.20 @@ -168,11 +168,11 @@
    1.21          qed
    1.22        qed
    1.23      next
    1.24 -      show "(\<Union>\<^bsub>h\<in>N\<^esub> {x \<otimes> h}) \<subseteq> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
    1.25 +      show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
    1.26        proof clarify
    1.27          fix n
    1.28          assume n: "n \<in> N" 
    1.29 -        show "x \<otimes> n \<in> (\<Union>\<^bsub>h\<in>N\<^esub> {h \<otimes> x})"
    1.30 +        show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
    1.31          proof 
    1.32            show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
    1.33            show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
    1.34 @@ -261,7 +261,7 @@
    1.35  proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
    1.36    fix h
    1.37    assume "h \<in> H"
    1.38 -  show "inv x \<otimes> inv h \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {j \<otimes> inv x})"
    1.39 +  show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
    1.40    proof
    1.41      show "inv x \<otimes> inv h \<otimes> x \<in> H"
    1.42        by (simp add: inv_op_closed1 prems)
    1.43 @@ -271,7 +271,7 @@
    1.44  next
    1.45    fix h
    1.46    assume "h \<in> H"
    1.47 -  show "h \<otimes> inv x \<in> (\<Union>\<^bsub>j\<in>H\<^esub> {inv x \<otimes> inv j})"
    1.48 +  show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
    1.49    proof
    1.50      show "x \<otimes> inv h \<otimes> inv x \<in> H"
    1.51        by (simp add: inv_op_closed2 prems)
    1.52 @@ -651,7 +651,7 @@
    1.53      assume y: "y \<in> carrier H"
    1.54      with h obtain g where g: "g \<in> carrier G" "h g = y"
    1.55        by (blast elim: equalityE); 
    1.56 -    hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}" 
    1.57 +    hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
    1.58        by (auto simp add: y kernel_def r_coset_def) 
    1.59      with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 
    1.60        by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)