resolution of name clashes in Algebra
authorpaulson <lp15@cam.ac.uk>
Wed Jun 06 14:25:53 2018 +0100 (11 months ago)
changeset 683990b71d08528f0
parent 68382 b10ae73f0bab
child 68400 cada19e0c6c7
resolution of name clashes in Algebra
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/More_Group.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/Sylow.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Tue Jun 05 16:35:52 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Wed Jun 06 14:25:53 2018 +0100
     1.3 @@ -50,14 +50,6 @@
     1.4  
     1.5  subsection \<open>Products of Units in Monoids\<close>
     1.6  
     1.7 -lemma (in monoid) Units_m_closed[simp, intro]:
     1.8 -  assumes h1unit: "h1 \<in> Units G"
     1.9 -    and h2unit: "h2 \<in> Units G"
    1.10 -  shows "h1 \<otimes> h2 \<in> Units G"
    1.11 -  unfolding Units_def
    1.12 -  using assms
    1.13 -  by auto (metis Units_inv_closed Units_l_inv Units_m_closed Units_r_inv)
    1.14 -
    1.15  lemma (in monoid) prod_unit_l:
    1.16    assumes abunit[simp]: "a \<otimes> b \<in> Units G"
    1.17      and aunit[simp]: "a \<in> Units G"
     2.1 --- a/src/HOL/Algebra/Group.thy	Tue Jun 05 16:35:52 2018 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Wed Jun 06 14:25:53 2018 +0100
     2.3 @@ -324,39 +324,19 @@
     2.4  
     2.5  lemma (in group) l_inv [simp]:
     2.6    "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
     2.7 -  using Units_l_inv by simp
     2.8 +  by simp
     2.9  
    2.10  
    2.11  subsection \<open>Cancellation Laws and Basic Properties\<close>
    2.12  
    2.13 -lemma (in group) l_cancel [simp]:
    2.14 -  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    2.15 -   (x \<otimes> y = x \<otimes> z) = (y = z)"
    2.16 -  using Units_l_inv by simp
    2.17 -
    2.18  lemma (in group) r_inv [simp]:
    2.19    "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
    2.20 -proof -
    2.21 -  assume x: "x \<in> carrier G"
    2.22 -  then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
    2.23 -    by (simp add: m_assoc [symmetric])
    2.24 -  with x show ?thesis by (simp del: r_one)
    2.25 -qed
    2.26 +  by simp
    2.27  
    2.28 -lemma (in group) r_cancel [simp]:
    2.29 +lemma (in group) right_cancel [simp]:
    2.30    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    2.31     (y \<otimes> x = z \<otimes> x) = (y = z)"
    2.32 -proof
    2.33 -  assume eq: "y \<otimes> x = z \<otimes> x"
    2.34 -    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
    2.35 -  then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
    2.36 -    by (simp add: m_assoc [symmetric] del: r_inv Units_r_inv)
    2.37 -  with G show "y = z" by simp
    2.38 -next
    2.39 -  assume eq: "y = z"
    2.40 -    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
    2.41 -  then show "y \<otimes> x = z \<otimes> x" by simp
    2.42 -qed
    2.43 +  by (metis inv_closed m_assoc r_inv r_one)
    2.44  
    2.45  lemma (in group) inv_one [simp]:
    2.46    "inv \<one> = \<one>"
    2.47 @@ -389,11 +369,7 @@
    2.48  
    2.49  lemma (in group) inv_equality:
    2.50       "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
    2.51 -apply (simp add: m_inv_def)
    2.52 -apply (rule the_equality)
    2.53 - apply (simp add: inv_comm [of y x])
    2.54 -apply (rule r_cancel [THEN iffD1], auto)
    2.55 -done
    2.56 +  using inv_unique r_inv by blast
    2.57  
    2.58  (* Contributed by Joachim Breitner *)
    2.59  lemma (in group) inv_solve_left:
     3.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Jun 05 16:35:52 2018 +0200
     3.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Jun 06 14:25:53 2018 +0100
     3.3 @@ -4,7 +4,7 @@
     3.4  *)
     3.5  
     3.6  theory IntRing
     3.7 -imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
     3.8 +imports "HOL-Computational_Algebra.Primes" QuotRing Lattice 
     3.9  begin
    3.10  
    3.11  section \<open>The Ring of Integers\<close>
    3.12 @@ -229,7 +229,7 @@
    3.13    by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
    3.14  
    3.15  lemma prime_primeideal:
    3.16 -  assumes prime: "prime p"
    3.17 +  assumes prime: "Factorial_Ring.prime p"
    3.18    shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
    3.19  apply (rule primeidealI)
    3.20     apply (rule int.genideal_ideal, simp)
    3.21 @@ -404,7 +404,7 @@
    3.22    done
    3.23  
    3.24  lemma ZFact_prime_is_domain:
    3.25 -  assumes pprime: "prime p"
    3.26 +  assumes pprime: "Factorial_Ring.prime p"
    3.27    shows "domain (ZFact p)"
    3.28    apply (unfold ZFact_def)
    3.29    apply (rule primeideal.quotient_is_domain)
     4.1 --- a/src/HOL/Algebra/More_Group.thy	Tue Jun 05 16:35:52 2018 +0200
     4.2 +++ b/src/HOL/Algebra/More_Group.thy	Wed Jun 06 14:25:53 2018 +0100
     4.3 @@ -81,31 +81,16 @@
     4.4    done
     4.5  
     4.6  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"
     4.7 -  apply auto
     4.8 -  apply (subst l_cancel [symmetric])
     4.9 -     prefer 4
    4.10 -     apply (erule ssubst)
    4.11 -     apply auto
    4.12 -  done
    4.13 +  by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
    4.14  
    4.15  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"
    4.16 -  apply auto
    4.17 -  apply (subst r_cancel [symmetric])
    4.18 -     prefer 4
    4.19 -     apply (erule ssubst)
    4.20 -     apply auto
    4.21 -  done
    4.22 +  by (metis monoid.l_one monoid_axioms one_closed right_cancel)
    4.23  
    4.24 -(* Is there a better way to do this? *)
    4.25  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"
    4.26 -  apply (subst eq_commute)
    4.27 -  apply simp
    4.28 -  done
    4.29 +  using l_cancel_one by fastforce
    4.30  
    4.31  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"
    4.32 -  apply (subst eq_commute)
    4.33 -  apply simp
    4.34 -  done
    4.35 +  using r_cancel_one by fastforce
    4.36  
    4.37  (* This should be generalized to arbitrary groups, not just commutative
    4.38     ones, using Lagrange's theorem. *)
     5.1 --- a/src/HOL/Algebra/Ring.thy	Tue Jun 05 16:35:52 2018 +0200
     5.2 +++ b/src/HOL/Algebra/Ring.thy	Wed Jun 06 14:25:53 2018 +0100
     5.3 @@ -184,8 +184,6 @@
     5.4    "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<ominus> y \<in> carrier G"
     5.5    by (simp add: a_minus_def)
     5.6  
     5.7 -lemmas a_l_cancel = add.l_cancel
     5.8 -lemmas a_r_cancel = add.r_cancel
     5.9  lemmas l_neg = add.l_inv [simp del]
    5.10  lemmas r_neg = add.r_inv [simp del]
    5.11  lemmas minus_zero = add.inv_one
     6.1 --- a/src/HOL/Algebra/Sylow.thy	Tue Jun 05 16:35:52 2018 +0200
     6.2 +++ b/src/HOL/Algebra/Sylow.thy	Wed Jun 06 14:25:53 2018 +0100
     6.3 @@ -79,7 +79,7 @@
     6.4    show ?thesis
     6.5    proof
     6.6      show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
     6.7 -      by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1)
     6.8 +      by (simp add: H_def inj_on_def m1)
     6.9      show "restrict ((\<otimes>) m1) H \<in> H \<rightarrow> M1"
    6.10      proof (rule restrictI)
    6.11        fix z