diff -r ba2a92af88b4 -r 023b353911c5 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sat Jun 16 22:09:24 2018 +0200
+++ b/src/HOL/Algebra/Group.thy	Sun Jun 17 22:00:43 2018 +0100
@@ -136,10 +136,7 @@
 
 lemma (in monoid) Units_r_inv [simp]:
   "x \<in> Units G ==> x \<otimes> inv x = \<one>"
-  apply (unfold Units_def m_inv_def, auto)
-  apply (rule theI2, fast)
-   apply (fast intro: inv_unique, fast)
-  done
+  by (metis (full_types) Units_closed Units_inv_closed Units_l_inv Units_r_inv_ex inv_unique)
 
 lemma (in monoid) inv_one [simp]:
   "inv \<one> = \<one>"
@@ -503,10 +500,6 @@
   "x \<in> H \<Longrightarrow> x \<in> carrier G"
   using subset by blast
 
-lemma submonoid_imp_subset:
-  "submonoid H G \<Longrightarrow> H \<subseteq> carrier G"
-  by (rule submonoid.subset)
-
 lemma (in submonoid) submonoid_is_monoid [intro]:
   assumes "monoid G"
   shows "monoid (G\<lparr>carrier := H\<rparr>)"
@@ -516,15 +509,6 @@
     by (simp add: monoid_def m_assoc)
 qed
 
-lemma (in monoid) submonoidE:
-  assumes "submonoid H G"
-  shows "H \<subseteq> carrier G"
-    and "H \<noteq> {}"
-    and "\<And>a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
-  using assms submonoid_imp_subset apply blast
-  using assms submonoid_def apply auto[1]
-  by (simp add: assms submonoid.m_closed)+
-
 lemma submonoid_nonempty:
   "~ submonoid {} G"
   by (blast dest: submonoid.one_closed)
@@ -569,21 +553,15 @@
   "x \<in> H \<Longrightarrow> x \<in> carrier G"
   using subset by blast
 
-(*DELETE*)
-lemma subgroup_imp_subset:
-  "subgroup H G \<Longrightarrow> H \<subseteq> carrier G"
-  by (rule subgroup.subset)
-
 lemma (in subgroup) subgroup_is_group [intro]:
   assumes "group G"
   shows "group (G\<lparr>carrier := H\<rparr>)"
 proof -
   interpret group G by fact
-  show ?thesis
-    apply (rule monoid.group_l_invI)
-    apply (unfold_locales) [1]
-    apply (auto intro: m_assoc l_inv mem_carrier)
-    done
+  have "Group.monoid (G\<lparr>carrier := H\<rparr>)"
+    by (simp add: monoid_axioms submonoid.intro submonoid.submonoid_is_monoid subset)
+  then show ?thesis
+    by (rule monoid.group_l_invI) (auto intro: l_inv mem_carrier)
 qed
 
 lemma (in group) subgroup_inv_equality:
@@ -808,23 +786,42 @@
   using iso_set_refl unfolding is_iso_def by auto
 
 lemma (in group) iso_set_sym:
-     "h \<in> iso G H \<Longrightarrow> inv_into (carrier G) h \<in> (iso H G)"
-apply (simp add: iso_def bij_betw_inv_into)
-apply (subgoal_tac "inv_into (carrier G) h \<in> carrier H \<rightarrow> carrier G")
- prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_into])
-apply (simp add: hom_def bij_betw_def inv_into_f_eq f_inv_into_f Pi_def)
-done
+  assumes "h \<in> iso G H"
+  shows "inv_into (carrier G) h \<in> iso H G"
+proof -
+  have h: "h \<in> hom G H" "bij_betw h (carrier G) (carrier H)"
+    using assms by (auto simp add: iso_def bij_betw_inv_into)
+  then have HG: "bij_betw (inv_into (carrier G) h) (carrier H) (carrier G)"
+    by (simp add: bij_betw_inv_into)
+  have "inv_into (carrier G) h \<in> hom H G"
+    unfolding hom_def
+  proof safe
+    show *: "\<And>x. x \<in> carrier H \<Longrightarrow> inv_into (carrier G) h x \<in> carrier G"
+      by (meson HG bij_betwE)
+    show "inv_into (carrier G) h (x \<otimes>\<^bsub>H\<^esub> y) = inv_into (carrier G) h x \<otimes> inv_into (carrier G) h y"
+      if "x \<in> carrier H" "y \<in> carrier H" for x y
+    proof (rule inv_into_f_eq)
+      show "inj_on h (carrier G)"
+        using bij_betw_def h(2) by blast
+      show "inv_into (carrier G) h x \<otimes> inv_into (carrier G) h y \<in> carrier G"
+        by (simp add: * that)
+      show "h (inv_into (carrier G) h x \<otimes> inv_into (carrier G) h y) = x \<otimes>\<^bsub>H\<^esub> y"
+        using h bij_betw_inv_into_right [of h] unfolding hom_def by (simp add: "*" that)
+    qed
+  qed
+  then show ?thesis
+    by (simp add: Group.iso_def bij_betw_inv_into h)
+qed
 
-corollary (in group) iso_sym :
-"G \<cong> H \<Longrightarrow> H \<cong> G"
+
+corollary (in group) iso_sym: "G \<cong> H \<Longrightarrow> H \<cong> G"
   using iso_set_sym unfolding is_iso_def by auto
 
 lemma (in group) iso_set_trans:
      "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
 by (auto simp add: iso_def hom_compose bij_betw_compose)
 
-corollary (in group) iso_trans :
-"\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
+corollary (in group) iso_trans: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
   using iso_set_trans unfolding is_iso_def by blast
 
 (* Next four lemmas contributed by Paulo. *)
@@ -1143,15 +1140,6 @@
   shows "comm_monoid G"
   by (rule comm_monoidI) (auto intro: m_assoc m_comm)
 
-(*lemma (in comm_monoid) r_one [simp]:
-  "x \<in> carrier G ==> x \<otimes> \<one> = x"
-proof -
-  assume G: "x \<in> carrier G"
-  then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm)
-  also from G have "... = x" by simp
-  finally show ?thesis .
-qed*)
-
 lemma (in comm_monoid) nat_pow_distr:
   "[| x \<in> carrier G; y \<in> carrier G |] ==>
   (x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
@@ -1397,22 +1385,24 @@
     \<lparr>carrier = Units G, Group.monoid.mult = Group.monoid.mult G, one  = one G\<rparr>"
 
 lemma (in monoid) units_group: "group (units_of G)"
-  apply (unfold units_of_def)
-  apply (rule groupI)
-      apply auto
-   apply (subst m_assoc)
-      apply auto
-  apply (rule_tac x = "inv x" in bexI)
-   apply auto
-  done
+proof -
+  have "\<And>x y z. \<lbrakk>x \<in> Units G; y \<in> Units G; z \<in> Units G\<rbrakk> \<Longrightarrow> x \<otimes> y \<otimes> z = x \<otimes> (y \<otimes> z)"
+    by (simp add: Units_closed m_assoc)
+  moreover have "\<And>x. x \<in> Units G \<Longrightarrow> \<exists>y\<in>Units G. y \<otimes> x = \<one>"
+    using Units_l_inv by blast
+  ultimately show ?thesis
+    unfolding units_of_def
+    by (force intro!: groupI)
+qed
 
 lemma (in comm_monoid) units_comm_group: "comm_group (units_of G)"
-  apply (rule group.group_comm_groupI)
-   apply (rule units_group)
-  apply (insert comm_monoid_axioms)
-  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
-  apply auto
-  done
+proof -
+  have "\<And>x y. \<lbrakk>x \<in> carrier (units_of G); y \<in> carrier (units_of G)\<rbrakk>
+              \<Longrightarrow> x \<otimes>\<^bsub>units_of G\<^esub> y = y \<otimes>\<^bsub>units_of G\<^esub> x"
+    by (simp add: Units_closed m_comm units_of_def)
+  then show ?thesis
+    by (rule group.group_comm_groupI [OF units_group]) auto
+qed
 
 lemma units_of_carrier: "carrier (units_of G) = Units G"
   by (auto simp: units_of_def)
@@ -1423,39 +1413,14 @@
 lemma units_of_one: "one (units_of G) = one G"
   by (auto simp: units_of_def)
 
-lemma (in monoid) units_of_inv: "x \<in> Units G \<Longrightarrow> m_inv (units_of G) x = m_inv G x"
-  apply (rule sym)
-  apply (subst m_inv_def)
-  apply (rule the1_equality)
-   apply (rule ex_ex1I)
-    apply (subst (asm) Units_def)
-    apply auto
-     apply (erule inv_unique)
-        apply auto
-    apply (rule Units_closed)
-    apply (simp_all only: units_of_carrier [symmetric])
-    apply (insert units_group)
-    apply auto
-   apply (subst units_of_mult [symmetric])
-   apply (subst units_of_one [symmetric])
-   apply (erule group.r_inv, assumption)
-  apply (subst units_of_mult [symmetric])
-  apply (subst units_of_one [symmetric])
-  apply (erule group.l_inv, assumption)
-  done
-
-lemma (in group) inj_on_const_mult: "a \<in> carrier G \<Longrightarrow> inj_on (\<lambda>x. a \<otimes> x) (carrier G)"
-  unfolding inj_on_def by auto
+lemma (in monoid) units_of_inv: 
+  assumes "x \<in> Units G"
+  shows "m_inv (units_of G) x = m_inv G x"
+  by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one)
 
 lemma (in group) surj_const_mult: "a \<in> carrier G \<Longrightarrow> (\<lambda>x. a \<otimes> x) ` carrier G = carrier G"
   apply (auto simp add: image_def)
-  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
-  apply auto
-(* auto should get this. I suppose we need "comm_monoid_simprules"
-   for ac_simps rewriting. *)
-  apply (subst m_assoc [symmetric])
-  apply auto
-  done
+  by (metis inv_closed inv_solve_left m_closed)
 
 lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
   by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)