# HG changeset patch
# User paulson
# Date 1528291630 -3600
# Node ID cada19e0c6c7a60af8a71d167ed8147c9f07660c
# Parent  194fa3d2d6a4d01f9f3cde59125c466c525216be# Parent  0b71d08528f0599685d89b94b78d66d81363a273
merged

diff -r 194fa3d2d6a4 -r cada19e0c6c7 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed Jun 06 14:23:13 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Jun 06 14:27:10 2018 +0100
@@ -50,14 +50,6 @@
 
 subsection \<open>Products of Units in Monoids\<close>
 
-lemma (in monoid) Units_m_closed[simp, intro]:
-  assumes h1unit: "h1 \<in> Units G"
-    and h2unit: "h2 \<in> Units G"
-  shows "h1 \<otimes> h2 \<in> Units G"
-  unfolding Units_def
-  using assms
-  by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)
-
 lemma (in monoid) prod_unit_l:
   assumes abunit[simp]: "a \<otimes> b \<in> Units G"
     and aunit[simp]: "a \<in> Units G"
diff -r 194fa3d2d6a4 -r cada19e0c6c7 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Jun 06 14:23:13 2018 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed Jun 06 14:27:10 2018 +0100
@@ -324,39 +324,19 @@
 
 lemma (in group) l_inv [simp]:
   "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
-  using Units_l_inv by simp
+  by simp
 
 
 subsection \<open>Cancellation Laws and Basic Properties\<close>
 
-lemma (in group) l_cancel [simp]:
-  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
-   (x \<otimes> y = x \<otimes> z) = (y = z)"
-  using Units_l_inv by simp
-
 lemma (in group) r_inv [simp]:
   "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
-proof -
-  assume x: "x \<in> carrier G"
-  then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
-    by (simp add: m_assoc [symmetric])
-  with x show ?thesis by (simp del: r_one)
-qed
+  by simp
 
-lemma (in group) r_cancel [simp]:
+lemma (in group) right_cancel [simp]:
   "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    (y \<otimes> x = z \<otimes> x) = (y = z)"
-proof
-  assume eq: "y \<otimes> x = z \<otimes> x"
-    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
-  then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
-    by (simp add: m_assoc [symmetric] del: r_inv Units_r_inv)
-  with G show "y = z" by simp
-next
-  assume eq: "y = z"
-    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
-  then show "y \<otimes> x = z \<otimes> x" by simp
-qed
+  by (metis inv_closed m_assoc r_inv r_one)
 
 lemma (in group) inv_one [simp]:
   "inv \<one> = \<one>"
@@ -389,11 +369,7 @@
 
 lemma (in group) inv_equality:
      "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
-apply (simp add: m_inv_def)
-apply (rule the_equality)
- apply (simp add: inv_comm [of y x])
-apply (rule r_cancel [THEN iffD1], auto)
-done
+  using inv_unique r_inv by blast
 
 (* Contributed by Joachim Breitner *)
 lemma (in group) inv_solve_left:
diff -r 194fa3d2d6a4 -r cada19e0c6c7 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Wed Jun 06 14:23:13 2018 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Wed Jun 06 14:27:10 2018 +0100
@@ -4,7 +4,7 @@
 *)
 
 theory IntRing
-imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
+imports "HOL-Computational_Algebra.Primes" QuotRing Lattice 
 begin
 
 section \<open>The Ring of Integers\<close>
@@ -229,7 +229,7 @@
   by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
 
 lemma prime_primeideal:
-  assumes prime: "prime p"
+  assumes prime: "Factorial_Ring.prime p"
   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
 apply (rule primeidealI)
    apply (rule int.genideal_ideal, simp)
@@ -404,7 +404,7 @@
   done
 
 lemma ZFact_prime_is_domain:
-  assumes pprime: "prime p"
+  assumes pprime: "Factorial_Ring.prime p"
   shows "domain (ZFact p)"
   apply (unfold ZFact_def)
   apply (rule primeideal.quotient_is_domain)
diff -r 194fa3d2d6a4 -r cada19e0c6c7 src/HOL/Algebra/More_Group.thy
--- a/src/HOL/Algebra/More_Group.thy	Wed Jun 06 14:23:13 2018 +0200
+++ b/src/HOL/Algebra/More_Group.thy	Wed Jun 06 14:27:10 2018 +0100
@@ -81,31 +81,16 @@
   done
 
 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"
-  apply auto
-  apply (subst l_cancel [symmetric])
-     prefer 4
-     apply (erule ssubst)
-     apply auto
-  done
+  by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
 
 lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
-  apply auto
-  apply (subst r_cancel [symmetric])
-     prefer 4
-     apply (erule ssubst)
-     apply auto
-  done
+  by (metis monoid.l_one monoid_axioms one_closed right_cancel)
 
-(* Is there a better way to do this? *)
 lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
-  apply (subst eq_commute)
-  apply simp
-  done
+  using l_cancel_one by fastforce
 
 lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
-  apply (subst eq_commute)
-  apply simp
-  done
+  using r_cancel_one by fastforce
 
 (* This should be generalized to arbitrary groups, not just commutative
    ones, using Lagrange's theorem. *)
diff -r 194fa3d2d6a4 -r cada19e0c6c7 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Jun 06 14:23:13 2018 +0200
+++ b/src/HOL/Algebra/Ring.thy	Wed Jun 06 14:27:10 2018 +0100
@@ -184,8 +184,6 @@
   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
   by (simp add: a_minus_def)
 
-lemmas a_l_cancel = add.l_cancel
-lemmas a_r_cancel = add.r_cancel
 lemmas l_neg = add.l_inv [simp del]
 lemmas r_neg = add.r_inv [simp del]
 lemmas minus_zero = add.inv_one
diff -r 194fa3d2d6a4 -r cada19e0c6c7 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Wed Jun 06 14:23:13 2018 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Wed Jun 06 14:27:10 2018 +0100
@@ -79,7 +79,7 @@
   show ?thesis
   proof
     show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
-      by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1)
+      by (simp add: H_def inj_on_def m1)
     show "restrict ((\<otimes>) m1) H \<in> H \<rightarrow> M1"
     proof (rule restrictI)
       fix z