diff -r 4b367da119ed -r 2976a4a3b126 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Jul 25 22:33:04 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy	Sat Jul 28 16:06:36 2018 +0100
@@ -440,45 +440,36 @@
   shows "N \<lhd> G"
   using assms normal_inv_iff by blast
 
-corollary (in group) normal_invE:
-  assumes "N \<lhd> G"
-  shows "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
-  using assms normal_inv_iff apply blast
-  by (simp add: assms normal.inv_op_closed2)
-
-
-lemma (in group) one_is_normal :
-   "{\<one>} \<lhd> G"
-proof(intro normal_invI )
+lemma (in group) one_is_normal: "{\<one>} \<lhd> G"
+proof(intro normal_invI)
   show "subgroup {\<one>} G"
     by (simp add: subgroup_def)
-  show "\<And>x h. x \<in> carrier G \<Longrightarrow> h \<in> {\<one>} \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> {\<one>}" by simp
-qed
+qed simp
 
 
 subsection\<open>More Properties of Left Cosets\<close>
 
 lemma (in group) l_repr_independence:
-  assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
+  assumes "y \<in> x <# H" "x \<in> carrier G" and HG: "subgroup H G"
   shows "x <# H = y <# H"
 proof -
   obtain h' where h': "h' \<in> H" "y = x \<otimes> h'"
     using assms(1) unfolding l_coset_def by blast
   hence "x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)" if "h \<in> H" for h
   proof -
-    have f3: "h' \<in> carrier G"
-      by (meson assms(3) h'(1) subgroup.mem_carrier)
-    have f4: "h \<in> carrier G"
-      by (meson assms(3) subgroup.mem_carrier that)
-    then show ?thesis
-      by (metis assms(2) f3 h'(2) inv_closed inv_solve_right m_assoc m_closed)
+    have "h' \<in> carrier G"
+      by (meson HG h'(1) subgroup.mem_carrier)
+    moreover have "h \<in> carrier G"
+      by (meson HG subgroup.mem_carrier that)
+    ultimately show ?thesis
+      by (metis assms(2) h'(2) inv_closed inv_solve_right m_assoc m_closed)
   qed
-  hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
-    unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def)
-  moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
-    using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
-  hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
-    unfolding l_coset_def using subgroup.m_closed[OF assms(3) h'(1)] by blast
+  hence "\<And>xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
+    unfolding l_coset_def by (metis (no_types, lifting) UN_iff HG h'(1) subgroup_def)
+  moreover have "\<And>h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
+    using h' by (meson assms(2) HG m_assoc subgroup.mem_carrier)
+  hence "\<And>yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
+    unfolding l_coset_def using subgroup.m_closed[OF HG h'(1)] by blast
   ultimately show ?thesis by blast
 qed
 
@@ -655,8 +646,8 @@
   shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
 proof -
   interpret subgroup H G by fact
-  from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
-    apply blast by (simp add: inv_solve_left m_assoc)
+  from p show ?thesis 
+    by (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"]) (auto simp: inv_solve_left m_assoc)
 qed
 
 lemma (in group) rcos_disjoint:
@@ -666,9 +657,8 @@
 proof -
   interpret subgroup H G by fact
   from p show ?thesis
-    apply (simp add: RCOSETS_def r_coset_def)
-    apply (blast intro: rcos_equation assms sym)
-    done
+    unfolding RCOSETS_def r_coset_def
+    by (blast intro: rcos_equation assms sym)
 qed
 
 
@@ -761,26 +751,26 @@
 proof -
   interpret subgroup H G by fact
   show ?thesis
-    apply (rule equalityI)
-    apply (force simp add: RCOSETS_def r_coset_def)
-    apply (auto simp add: RCOSETS_def intro: rcos_self assms)
-    done
+    unfolding RCOSETS_def r_coset_def by auto
 qed
 
 lemma (in group) cosets_finite:
      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
-apply (auto simp add: RCOSETS_def)
-apply (simp add: r_coset_subset_G [THEN finite_subset])
-done
+  unfolding RCOSETS_def
+  by (auto simp add: r_coset_subset_G [THEN finite_subset])
 
 text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
 lemma (in group) inj_on_f:
-    "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
-apply (rule inj_onI)
-apply (subgoal_tac "x \<in> carrier G \<and> y \<in> carrier G")
- prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
-apply (simp add: subsetD)
-done
+  assumes "H \<subseteq> carrier G" and a: "a \<in> carrier G"
+  shows "inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
+proof 
+  fix x y
+  assume "x \<in> H #> a" "y \<in> H #> a" and xy: "x \<otimes> inv a = y \<otimes> inv a"
+  then have "x \<in> carrier G" "y \<in> carrier G"
+    using assms r_coset_subset_G by blast+
+  with xy a show "x = y"
+    by auto
+qed
 
 lemma (in group) inj_on_g:
     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
@@ -827,16 +817,17 @@
   using rcosets_part_G by auto
 
 proposition (in group) lagrange_finite:
-     "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
-      \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
-apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
-apply (subst mult.commute)
-apply (rule card_partition)
-   apply (simp add: rcosets_subset_PowG [THEN finite_subset])
-  apply (simp add: rcosets_part_G)
-  apply (simp add: card_rcosets_equal subgroup.subset)
-apply (simp add: rcos_disjoint)
-done
+  assumes "finite(carrier G)" and HG: "subgroup H G"
+  shows "card(rcosets H) * card(H) = order(G)"
+proof -
+  have "card H * card (rcosets H) = card (\<Union>(rcosets H))"
+  proof (rule card_partition)
+    show "\<And>c1 c2. \<lbrakk>c1 \<in> rcosets H; c2 \<in> rcosets H; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> c1 \<inter> c2 = {}"
+      using HG rcos_disjoint by auto
+  qed (auto simp: assms finite_UnionD rcosets_part_G card_rcosets_equal subgroup.subset)
+  then show ?thesis
+    by (simp add: HG mult.commute order_def rcosets_part_G)
+qed
 
 theorem (in group) lagrange:
   assumes "subgroup H G"
@@ -844,29 +835,29 @@
 proof (cases "finite (carrier G)")
   case True thus ?thesis using lagrange_finite assms by simp
 next
-  case False note inf_G = this
+  case False 
   thus ?thesis
   proof (cases "finite H")
-    case False thus ?thesis using inf_G  by (simp add: order_def)
+    case False thus ?thesis using \<open>infinite (carrier G)\<close>  by (simp add: order_def)
   next
-    case True note finite_H = this
+    case True 
     have "infinite (rcosets H)"
-    proof (rule ccontr)
-      assume "\<not> infinite (rcosets H)"
+    proof 
+      assume "finite (rcosets H)"
       hence finite_rcos: "finite (rcosets H)" by simp
       hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
-        using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
+        using card_Union_disjoint[of "rcosets H"] \<open>finite H\<close> rcos_disjoint[OF assms(1)]
               rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
       hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
         by (simp add: assms order_def rcosets_part_G)
       hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
         using card_rcosets_equal by (simp add: assms subgroup.subset)
       hence "order G = (card H) * (card (rcosets H))" by simp
-      hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
+      hence "order G \<noteq> 0" using finite_rcos \<open>finite H\<close> assms ex_in_conv
                                 rcosets_part_G subgroup.one_closed by fastforce
-      thus False using inf_G order_gt_0_iff_finite by blast
+      thus False using \<open>infinite (carrier G)\<close> order_gt_0_iff_finite by blast
     qed
-    thus ?thesis using inf_G by (simp add: order_def)
+    thus ?thesis using \<open>infinite (carrier G)\<close> by (simp add: order_def)
   qed
 qed
 
@@ -908,8 +899,8 @@
 
 theorem (in normal) factorgroup_is_group:
   "group (G Mod H)"
-apply (simp add: FactGroup_def)
-apply (rule groupI)
+  unfolding FactGroup_def
+  apply (rule groupI)
     apply (simp add: setmult_closed)
    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
   apply (simp add: restrictI setmult_closed rcosets_assoc)
@@ -922,10 +913,20 @@
   by (simp add: FactGroup_def)
 
 lemma (in normal) inv_FactGroup:
-     "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
-apply (rule group.inv_equality [OF factorgroup_is_group])
-apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
-done
+  assumes "X \<in> carrier (G Mod H)"
+  shows "inv\<^bsub>G Mod H\<^esub> X = set_inv X"
+proof -
+  have X: "X \<in> rcosets H"
+    using assms by (simp add: FactGroup_def)
+  moreover have "set_inv X <#> X = H"
+    using X by (simp add: normal.rcosets_inv_mult_group_eq normal_axioms)
+  moreover have "Group.group (G Mod H)"
+    using normal.factorgroup_is_group normal_axioms by blast
+  moreover have "set_inv X \<in> rcosets H"
+    by (simp add: \<open>X \<in> rcosets H\<close> setinv_closed)
+  ultimately show ?thesis
+    by (simp add: FactGroup_def group.inv_equality)
+qed
 
 text\<open>The coset map is a homomorphism from @{term G} to the quotient group
   @{term "G Mod H"}\<close>
@@ -945,15 +946,13 @@
   where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"
 
 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
-apply (rule subgroup.intro)
-apply (auto simp add: kernel_def group.intro is_group)
-done
+  by (auto simp add: kernel_def group.intro is_group intro: subgroup.intro)
 
 text\<open>The kernel of a homomorphism is a normal subgroup\<close>
 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
-apply (simp add: G.normal_inv_iff subgroup_kernel)
-apply (simp add: kernel_def)
-done
+  apply (simp only: G.normal_inv_iff subgroup_kernel)
+  apply (simp add: kernel_def)
+  done
 
 lemma (in group_hom) FactGroup_nonempty:
   assumes X: "X \<in> carrier (G Mod kernel G H h)"
@@ -982,37 +981,40 @@
 
 lemma (in group_hom) FactGroup_hom:
      "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
-apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
-proof (intro ballI)
-  fix X and X'
-  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
-     and X': "X' \<in> carrier (G Mod kernel G H h)"
-  then
-  obtain g and g'
-           where "g \<in> carrier G" and "g' \<in> carrier G"
-             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
-    by (auto simp add: FactGroup_def RCOSETS_def)
-  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
-    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
-    by (force simp add: kernel_def r_coset_def image_def)+
-  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
-    by (auto dest!: FactGroup_nonempty intro!: image_eqI
-             simp add: set_mult_def
-                       subsetD [OF Xsub] subsetD [OF X'sub])
-  then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
-    by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
+proof -
+  have "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
+    if X: "X  \<in> carrier (G Mod kernel G H h)" and X': "X' \<in> carrier (G Mod kernel G H h)" for X X'
+  proof -
+    obtain g and g'
+      where "g \<in> carrier G" and "g' \<in> carrier G"
+        and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
+      using X X' by (auto simp add: FactGroup_def RCOSETS_def)
+    hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
+      and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
+      by (force simp add: kernel_def r_coset_def image_def)+
+    hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
+      by (auto dest!: FactGroup_nonempty intro!: image_eqI
+          simp add: set_mult_def
+          subsetD [OF Xsub] subsetD [OF X'sub])
+    then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
+      by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
+  qed
+  then show ?thesis
+    by (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
 qed
 
 
 text\<open>Lemma for the following injectivity result\<close>
 lemma (in group_hom) FactGroup_subset:
-     "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
-      \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
-apply (clarsimp simp add: kernel_def r_coset_def)
-apply (rename_tac y)
-apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
-apply (simp add: G.m_assoc)
-done
+  assumes "g \<in> carrier G" "g' \<in> carrier G" "h g = h g'"
+  shows "kernel G H h #> g \<subseteq> kernel G H h #> g'"
+  unfolding kernel_def r_coset_def
+proof clarsimp
+  fix y 
+  assume "y \<in> carrier G" "h y = \<one>\<^bsub>H\<^esub>"
+  with assms show "\<exists>x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub> \<and> y \<otimes> g = x \<otimes> g'"
+    by (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) (auto simp: G.m_assoc)
+qed
 
 lemma (in group_hom) FactGroup_inj_on:
      "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
@@ -1113,13 +1115,13 @@
     from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
       unfolding DirProd_def by fastforce
     hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
-      using normal_imp_subgroup subgroup.subset assms apply blast+.
+      using normal_imp_subgroup subgroup.subset assms by blast+
     have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
       using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
     hence "x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x = (x1 \<otimes> h1 \<otimes> inv x1,x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)"
       using h1h2 x1x2 h1h2GK by auto
     moreover have "x1 \<otimes> h1 \<otimes> inv x1 \<in> H" "x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2 \<in> N"
-      using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto.
+      using assms x1x2 h1h2 assms by (simp_all add: normal.inv_op_closed2)
     hence "(x1 \<otimes> h1 \<otimes> inv x1, x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)\<in> H \<times> N" by auto
     ultimately show " x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x \<in> H \<times> N" by auto
   qed
@@ -1133,7 +1135,7 @@
 
 proof-
   have R :"(\<lambda>(X, Y). X \<times> Y) \<in> carrier (G Mod H) \<times> carrier (K Mod N) \<rightarrow> carrier (G \<times>\<times> K Mod H \<times> N)"
-    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
+    unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def by force
   moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
                 \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) =  x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)"
     unfolding set_mult_def by force
@@ -1143,8 +1145,14 @@
     by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
   moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) =
                                      carrier (G \<times>\<times> K Mod H \<times> N)"
-    unfolding image_def  apply auto using R apply force
-    unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
+  proof -
+    have 1: "\<And>x a b. \<lbrakk>a \<in> carrier (G Mod H); b \<in> carrier (K Mod N)\<rbrakk> \<Longrightarrow> a \<times> b \<in> carrier (G \<times>\<times> K Mod H \<times> N)"
+      using R by force
+    have 2: "\<And>z. z \<in> carrier (G \<times>\<times> K Mod H \<times> N) \<Longrightarrow> \<exists>x\<in>carrier (G Mod H). \<exists>y\<in>carrier (K Mod N). z = x \<times> y"
+      unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
+    show ?thesis
+      unfolding image_def by (auto simp: intro: 1 2)
+  qed
   ultimately show ?thesis
     unfolding iso_def hom_def bij_betw_def inj_on_def by simp
 qed
@@ -1262,7 +1270,7 @@
       have hH:"h\<in>carrier(GH)"
         using hHK HK_def GH_def by auto
       have  "(\<forall>x\<in>carrier (GH). \<forall>h\<in>H1.  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1)"
-        using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
+        using assms GH_def normal.inv_op_closed2 by fastforce
       hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
         using  xH H1K_def p2 by blast
       have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
@@ -1275,7 +1283,6 @@
   qed
 qed
 
-
 lemma (in group) normal_inter_subgroup:
   assumes "subgroup H G"
     and "N \<lhd> G"
@@ -1288,8 +1295,8 @@
   ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
     using normal_inter[of K H N] assms(1) by blast
   moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
-  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
+  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)"
+ by auto
 qed
 
-
 end