--- a/src/HOL/Algebra/Divisibility.thy Tue Jun 05 16:35:52 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Wed Jun 06 14:25:53 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"
--- a/src/HOL/Algebra/Group.thy Tue Jun 05 16:35:52 2018 +0200
+++ b/src/HOL/Algebra/Group.thy Wed Jun 06 14:25:53 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:
--- a/src/HOL/Algebra/IntRing.thy Tue Jun 05 16:35:52 2018 +0200
+++ b/src/HOL/Algebra/IntRing.thy Wed Jun 06 14:25:53 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)
--- a/src/HOL/Algebra/More_Group.thy Tue Jun 05 16:35:52 2018 +0200
+++ b/src/HOL/Algebra/More_Group.thy Wed Jun 06 14:25:53 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. *)
--- a/src/HOL/Algebra/Ring.thy Tue Jun 05 16:35:52 2018 +0200
+++ b/src/HOL/Algebra/Ring.thy Wed Jun 06 14:25:53 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
--- a/src/HOL/Algebra/Sylow.thy Tue Jun 05 16:35:52 2018 +0200
+++ b/src/HOL/Algebra/Sylow.thy Wed Jun 06 14:25:53 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