# 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 \Products of Units in Monoids\ -lemma (in monoid) Units_m_closed[simp, intro]: - assumes h1unit: "h1 \ Units G" - and h2unit: "h2 \ Units G" - shows "h1 \ h2 \ 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 \ b \ Units G" and aunit[simp]: "a \ 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 \ carrier G ==> inv x \ x = \" - using Units_l_inv by simp + by simp subsection \Cancellation Laws and Basic Properties\ -lemma (in group) l_cancel [simp]: - "[| x \ carrier G; y \ carrier G; z \ carrier G |] ==> - (x \ y = x \ z) = (y = z)" - using Units_l_inv by simp - lemma (in group) r_inv [simp]: "x \ carrier G ==> x \ inv x = \" -proof - - assume x: "x \ carrier G" - then have "inv x \ (x \ inv x) = inv x \ \" - 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 \ carrier G; y \ carrier G; z \ carrier G |] ==> (y \ x = z \ x) = (y = z)" -proof - assume eq: "y \ x = z \ x" - and G: "x \ carrier G" "y \ carrier G" "z \ carrier G" - then have "y \ (x \ inv x) = z \ (x \ 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 \ carrier G" "y \ carrier G" "z \ carrier G" - then show "y \ x = z \ x" by simp -qed + by (metis inv_closed m_assoc r_inv r_one) lemma (in group) inv_one [simp]: "inv \ = \" @@ -389,11 +369,7 @@ lemma (in group) inv_equality: "[|y \ x = \; x \ carrier G; y \ 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 \The Ring of Integers\ @@ -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>\\<^esub> {p}) \" 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 \ carrier G \ a \ carrier G \ x \ a = x \ 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 \ carrier G \ a \ carrier G \ a \ x = x \ 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 \ carrier G \ a \ carrier G \ x = x \ a \ a = one G" - apply (subst eq_commute) - apply simp - done + using l_cancel_one by fastforce lemma (in group) r_cancel_one' [simp]: "x \ carrier G \ a \ carrier G \ x = a \ x \ 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 \ carrier G; y \ carrier G |] ==> x \ y \ 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 (\z\H. m1 \ 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 ((\) m1) H \ H \ M1" proof (rule restrictI) fix z