avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
authorhaftmann
Wed Jul 08 14:01:41 2015 +0200 (2015-07-08)
changeset 6068801488b559910
parent 60687 33dbbcb6a8a3
child 60689 8a2d7c04d8c0
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
NEWS
src/HOL/Equiv_Relations.thy
src/HOL/GCD.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Rat.thy
src/HOL/Rings.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Wed Jul 08 14:01:40 2015 +0200
     1.2 +++ b/NEWS	Wed Jul 08 14:01:41 2015 +0200
     1.3 @@ -186,11 +186,19 @@
     1.4  * Tightened specification of class semiring_no_zero_divisors.  Slight
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -* Class algebraic_semidom introduced common algebraic notions of
     1.8 -integral (semi)domains like units and associated elements.  Although
     1.9 +* Class algebraic_semidom introduces common algebraic notions of
    1.10 +integral (semi)domains, particularly units.  Although
    1.11  logically subsumed by fields, is is not a super class of these
    1.12  in order not to burden fields with notions that are trivial there.
    1.13 -INCOMPATIBILITY.
    1.14 +
    1.15 +* Class normalization_semidom specifies canonical representants
    1.16 +for equivalence classes of associated elements in an integral
    1.17 +(semi)domain.  This formalizes associated elements as well.
    1.18 +
    1.19 +* Abstract specification of gcd/lcm operations in classes semiring_gcd,
    1.20 +semiring_Gcd, semiring_Lcd.  Minor INCOMPATIBILITY: facts gcd_nat.commute
    1.21 +and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc
    1.22 +and gcd_int.assoc by gcd.assoc.
    1.23  
    1.24  * Former constants Fields.divide (_ / _) and Divides.div (_ div _)
    1.25  are logically unified to Rings.divide in syntactic type class
     2.1 --- a/src/HOL/Equiv_Relations.thy	Wed Jul 08 14:01:40 2015 +0200
     2.2 +++ b/src/HOL/Equiv_Relations.thy	Wed Jul 08 14:01:41 2015 +0200
     2.3 @@ -523,20 +523,6 @@
     2.4    "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
     2.5    by (erule equivpE, erule transpE)
     2.6  
     2.7 -
     2.8 -subsection \<open>Prominent examples\<close>
     2.9 -
    2.10 -lemma equivp_associated:
    2.11 -  "equivp associated"
    2.12 -proof (rule equivpI)
    2.13 -  show "reflp associated"
    2.14 -    by (rule reflpI) simp
    2.15 -  show "symp associated"
    2.16 -    by (rule sympI) (simp add: associated_sym)
    2.17 -  show "transp associated"
    2.18 -    by (rule transpI) (fact associated_trans)
    2.19 -qed
    2.20 -
    2.21  hide_const (open) proj
    2.22  
    2.23  end
     3.1 --- a/src/HOL/GCD.thy	Wed Jul 08 14:01:40 2015 +0200
     3.2 +++ b/src/HOL/GCD.thy	Wed Jul 08 14:01:41 2015 +0200
     3.3 @@ -74,16 +74,6 @@
     3.4  
     3.5  end
     3.6  
     3.7 -context algebraic_semidom
     3.8 -begin
     3.9 -
    3.10 -lemma associated_1 [simp]:
    3.11 -  "associated 1 a \<longleftrightarrow> is_unit a"
    3.12 -  "associated a 1 \<longleftrightarrow> is_unit a"
    3.13 -  by (auto simp add: associated_def)
    3.14 -
    3.15 -end
    3.16 -
    3.17  declare One_nat_def [simp del]
    3.18  
    3.19  subsection {* GCD and LCM definitions *}
    3.20 @@ -116,29 +106,11 @@
    3.21  
    3.22  lemma gcd_0_left [simp]:
    3.23    "gcd 0 a = normalize a"
    3.24 -proof (rule associated_eqI)
    3.25 -  show "associated (gcd 0 a) (normalize a)"
    3.26 -    by (auto intro!: associatedI gcd_greatest)
    3.27 -  show "unit_factor (gcd 0 a) = 1" if "gcd 0 a \<noteq> 0"
    3.28 -  proof -
    3.29 -    from that have "unit_factor (normalize (gcd 0 a)) = 1"
    3.30 -      by (rule unit_factor_normalize)
    3.31 -    then show ?thesis by simp
    3.32 -  qed
    3.33 -qed simp
    3.34 +  by (rule associated_eqI) simp_all
    3.35  
    3.36  lemma gcd_0_right [simp]:
    3.37    "gcd a 0 = normalize a"
    3.38 -proof (rule associated_eqI)
    3.39 -  show "associated (gcd a 0) (normalize a)"
    3.40 -    by (auto intro!: associatedI gcd_greatest)
    3.41 -  show "unit_factor (gcd a 0) = 1" if "gcd a 0 \<noteq> 0"
    3.42 -  proof -
    3.43 -    from that have "unit_factor (normalize (gcd a 0)) = 1"
    3.44 -      by (rule unit_factor_normalize)
    3.45 -    then show ?thesis by simp
    3.46 -  qed
    3.47 -qed simp
    3.48 +  by (rule associated_eqI) simp_all
    3.49    
    3.50  lemma gcd_eq_0_iff [simp]:
    3.51    "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q")
    3.52 @@ -169,7 +141,7 @@
    3.53  proof
    3.54    fix a b c
    3.55    show "gcd a b = gcd b a"
    3.56 -    by (rule associated_eqI) (auto intro: associatedI gcd_greatest simp add: unit_factor_gcd)
    3.57 +    by (rule associated_eqI) simp_all
    3.58    from gcd_dvd1 have "gcd (gcd a b) c dvd a"
    3.59      by (rule dvd_trans) simp
    3.60    moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
    3.61 @@ -182,10 +154,8 @@
    3.62      by (rule dvd_trans) simp
    3.63    ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
    3.64      by (auto intro!: gcd_greatest)
    3.65 -  from P1 P2 have "associated (gcd (gcd a b) c) (gcd a (gcd b c))"
    3.66 -    by (rule associatedI)
    3.67 -  then show "gcd (gcd a b) c = gcd a (gcd b c)"
    3.68 -    by (rule associated_eqI) (simp_all add: unit_factor_gcd)
    3.69 +  from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
    3.70 +    by (rule associated_eqI) simp_all
    3.71  qed
    3.72  
    3.73  lemma gcd_self [simp]:
    3.74 @@ -193,15 +163,13 @@
    3.75  proof -
    3.76    have "a dvd gcd a a"
    3.77      by (rule gcd_greatest) simp_all
    3.78 -  then have "associated (gcd a a) (normalize a)"
    3.79 -    by (auto intro: associatedI)
    3.80    then show ?thesis
    3.81 -    by (auto intro: associated_eqI simp add: unit_factor_gcd)
    3.82 +    by (auto intro: associated_eqI)
    3.83  qed
    3.84      
    3.85  lemma coprime_1_left [simp]:
    3.86    "coprime 1 a"
    3.87 -  by (rule associated_eqI) (simp_all add: unit_factor_gcd)
    3.88 +  by (rule associated_eqI) simp_all
    3.89  
    3.90  lemma coprime_1_right [simp]:
    3.91    "coprime a 1"
    3.92 @@ -218,7 +186,7 @@
    3.93    moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b"
    3.94      by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
    3.95    ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
    3.96 -    by - (rule associated_eqI, auto intro: associated_eqI associatedI simp add: unit_factor_gcd)
    3.97 +    by (auto intro: associated_eqI)
    3.98    then show ?thesis by (simp add: normalize_mult)
    3.99  qed
   3.100  
   3.101 @@ -318,14 +286,15 @@
   3.102    fix a b c
   3.103    show "lcm a b = lcm b a"
   3.104      by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
   3.105 -  have "associated (lcm (lcm a b) c) (lcm a (lcm b c))"
   3.106 -    by (auto intro!: associatedI lcm_least
   3.107 +  have "lcm (lcm a b) c dvd lcm a (lcm b c)"
   3.108 +    and "lcm a (lcm b c) dvd lcm (lcm a b) c"
   3.109 +    by (auto intro: lcm_least
   3.110        dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
   3.111        dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
   3.112        dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
   3.113        dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
   3.114    then show "lcm (lcm a b) c = lcm a (lcm b c)"
   3.115 -    by (rule associated_eqI) (simp_all add: unit_factor_lcm lcm_eq_0_iff)
   3.116 +    by (rule associated_eqI) simp_all
   3.117  qed
   3.118  
   3.119  lemma lcm_self [simp]:
   3.120 @@ -333,10 +302,8 @@
   3.121  proof -
   3.122    have "lcm a a dvd a"
   3.123      by (rule lcm_least) simp_all
   3.124 -  then have "associated (lcm a a) (normalize a)"
   3.125 -    by (auto intro: associatedI)
   3.126    then show ?thesis
   3.127 -    by (rule associated_eqI) (auto simp add: unit_factor_lcm)
   3.128 +    by (auto intro: associated_eqI)
   3.129  qed
   3.130  
   3.131  lemma gcd_mult_lcm [simp]:
   3.132 @@ -471,10 +438,8 @@
   3.133        ultimately show ?thesis by (blast intro: dvd_trans)
   3.134      qed
   3.135    qed
   3.136 -  ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))"
   3.137 -    by (rule associatedI)
   3.138 -  then show ?thesis
   3.139 -    by (rule associated_eqI) (auto simp add: unit_factor_gcd unit_factor_Gcd)
   3.140 +  ultimately show ?thesis
   3.141 +    by (auto intro: associated_eqI)
   3.142  qed
   3.143  
   3.144  lemma dvd_Gcd: -- \<open>FIXME remove\<close>
   3.145 @@ -507,10 +472,10 @@
   3.146      ultimately show "Gcd (normalize ` A) dvd a"
   3.147        by simp
   3.148    qed
   3.149 -  then have "associated (Gcd (normalize ` A)) (Gcd A)"
   3.150 -    by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd)
   3.151 +  then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
   3.152 +    by (auto intro!: Gcd_greatest intro: Gcd_dvd)
   3.153    then show ?thesis
   3.154 -    by (rule associated_eqI) (simp_all add: unit_factor_Gcd, auto dest!: bspec)
   3.155 +    by (auto intro: associated_eqI)
   3.156  qed
   3.157  
   3.158  lemma Lcm_least:
   3.159 @@ -604,10 +569,8 @@
   3.160        ultimately show ?thesis by (blast intro: dvd_trans)
   3.161      qed
   3.162    qed
   3.163 -  ultimately have "associated (lcm a (Lcm A)) (Lcm (insert a A))"
   3.164 -    by (rule associatedI)
   3.165 -  then show "lcm a (Lcm A) = Lcm (insert a A)"
   3.166 -    by (rule associated_eqI) (simp_all add: unit_factor_lcm unit_factor_Lcm lcm_eq_0_iff)
   3.167 +  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
   3.168 +    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
   3.169  qed
   3.170    
   3.171  lemma Lcm_set [code_unfold]:
     4.1 --- a/src/HOL/Library/Poly_Deriv.thy	Wed Jul 08 14:01:40 2015 +0200
     4.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Wed Jul 08 14:01:41 2015 +0200
     4.3 @@ -182,11 +182,21 @@
     4.4  qed
     4.5  
     4.6  lemma order_decomp:
     4.7 -     "p \<noteq> 0
     4.8 -      ==> \<exists>q. p = [:-a, 1:] ^ (order a p) * q &
     4.9 -                ~([:-a, 1:] dvd q)"
    4.10 -apply (drule order [where a=a])
    4.11 -by (metis dvdE dvd_mult_cancel_left power_Suc2)
    4.12 +  assumes "p \<noteq> 0"
    4.13 +  shows "\<exists>q. p = [:- a, 1:] ^ order a p * q \<and> \<not> [:- a, 1:] dvd q"
    4.14 +proof -
    4.15 +  from assms have A: "[:- a, 1:] ^ order a p dvd p"
    4.16 +    and B: "\<not> [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order)
    4.17 +  from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" ..
    4.18 +  with B have "\<not> [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q"
    4.19 +    by simp
    4.20 +  then have "\<not> [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q"
    4.21 +    by simp
    4.22 +  then have D: "\<not> [:- a, 1:] dvd q"
    4.23 +    using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q]
    4.24 +    by auto
    4.25 +  from C D show ?thesis by blast
    4.26 +qed
    4.27  
    4.28  lemma order_pderiv: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
    4.29        ==> (order a p = Suc (order a (pderiv p)))"
     5.1 --- a/src/HOL/Number_Theory/Cong.thy	Wed Jul 08 14:01:40 2015 +0200
     5.2 +++ b/src/HOL/Number_Theory/Cong.thy	Wed Jul 08 14:01:41 2015 +0200
     5.3 @@ -267,7 +267,7 @@
     5.4  
     5.5  lemma cong_mult_rcancel_int:
     5.6      "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
     5.7 -  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd_int.commute)
     5.8 +  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd.commute)
     5.9  
    5.10  lemma cong_mult_rcancel_nat:
    5.11      "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
    5.12 @@ -528,15 +528,15 @@
    5.13    done
    5.14  
    5.15  lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
    5.16 -  apply (auto intro: cong_solve_coprime_nat simp: One_nat_def)
    5.17 +  apply (auto intro: cong_solve_coprime_nat)
    5.18    apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
    5.19    apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
    5.20 -      gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute)
    5.21 +      gcd_lcm_complete_lattice_nat.inf_bot_right gcd.commute)
    5.22    done
    5.23  
    5.24  lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
    5.25    apply (auto intro: cong_solve_coprime_int)
    5.26 -  apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd_int.commute gcd_red_int)
    5.27 +  apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd.commute gcd_red_int)
    5.28    done
    5.29  
    5.30  lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m =
    5.31 @@ -571,7 +571,7 @@
    5.32        [x = y] (mod (PROD i:A. m i))"
    5.33    apply (induct set: finite)
    5.34    apply auto
    5.35 -  apply (metis One_nat_def coprime_cong_mult_nat gcd_nat.commute setprod_coprime_nat)
    5.36 +  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
    5.37    done
    5.38  
    5.39  lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
    5.40 @@ -580,7 +580,7 @@
    5.41        [x = y] (mod (PROD i:A. m i))"
    5.42    apply (induct set: finite)
    5.43    apply auto
    5.44 -  apply (metis coprime_cong_mult_int gcd_int.commute setprod_coprime_int)
    5.45 +  apply (metis coprime_cong_mult_int gcd.commute setprod_coprime_int)
    5.46    done
    5.47  
    5.48  lemma binary_chinese_remainder_aux_nat:
    5.49 @@ -827,7 +827,7 @@
    5.50           [x = y] (mod (PROD i:A. m i))"
    5.51    apply (induct set: finite)
    5.52    apply auto
    5.53 -  apply (metis One_nat_def coprime_cong_mult_nat gcd_nat.commute setprod_coprime_nat)
    5.54 +  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
    5.55    done
    5.56  
    5.57  lemma chinese_remainder_unique_nat:
     6.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:40 2015 +0200
     6.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:41 2015 +0200
     6.3 @@ -228,16 +228,15 @@
     6.4    "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
     6.5    by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+
     6.6  
     6.7 -lemma unit_factor_gcd [simp]:
     6.8 -  "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
     6.9 -  by (induct a b rule: gcd_eucl_induct)
    6.10 -    (auto simp add: gcd_0 gcd_non_0)
    6.11 +lemma normalize_gcd [simp]:
    6.12 +  "normalize (gcd a b) = gcd a b"
    6.13 +  by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_0 gcd_non_0)
    6.14  
    6.15  lemma gcdI:
    6.16    assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
    6.17 -    and "unit_factor c = (if c = 0 then 0 else 1)"
    6.18 +    and "normalize c = c"
    6.19    shows "c = gcd a b"
    6.20 -  by (rule associated_eqI) (auto simp: assms associated_def intro: gcd_greatest)
    6.21 +  by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
    6.22  
    6.23  sublocale gcd!: abel_semigroup gcd
    6.24  proof
    6.25 @@ -251,10 +250,10 @@
    6.26      moreover have "gcd (gcd a b) c dvd c" by simp
    6.27      ultimately show "gcd (gcd a b) c dvd gcd b c"
    6.28        by (rule gcd_greatest)
    6.29 -    show "unit_factor (gcd (gcd a b) c) =  (if gcd (gcd a b) c = 0 then 0 else 1)"
    6.30 +    show "normalize (gcd (gcd a b) c) = gcd (gcd a b) c"
    6.31        by auto
    6.32      fix l assume "l dvd a" and "l dvd gcd b c"
    6.33 -    with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
    6.34 +    with dvd_trans [OF _ gcd_dvd1] and dvd_trans [OF _ gcd_dvd2]
    6.35        have "l dvd b" and "l dvd c" by blast+
    6.36      with \<open>l dvd a\<close> show "l dvd gcd (gcd a b) c"
    6.37        by (intro gcd_greatest)
    6.38 @@ -266,9 +265,9 @@
    6.39  qed
    6.40  
    6.41  lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 
    6.42 -    unit_factor d = (if d = 0 then 0 else 1) \<and>
    6.43 +    normalize d = d \<and>
    6.44      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    6.45 -  by (rule, auto intro: gcdI simp: gcd_greatest)
    6.46 +  by rule (auto intro: gcdI simp: gcd_greatest)
    6.47  
    6.48  lemma gcd_dvd_prod: "gcd a b dvd k * b"
    6.49    using mult_dvd_mono [of 1] by auto
    6.50 @@ -378,10 +377,9 @@
    6.51  
    6.52  lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
    6.53    apply (rule gcdI)
    6.54 +  apply simp_all
    6.55    apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
    6.56 -  apply (rule gcd_dvd2)
    6.57    apply (rule gcd_greatest, simp add: unit_simps, assumption)
    6.58 -  apply (subst unit_factor_gcd, simp add: gcd_0)
    6.59    done
    6.60  
    6.61  lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
    6.62 @@ -461,7 +459,7 @@
    6.63    with A show "gcd a b dvd c" by (rule dvd_trans)
    6.64    have "gcd c d dvd d" by simp
    6.65    with A show "gcd a b dvd d" by (rule dvd_trans)
    6.66 -  show "unit_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
    6.67 +  show "normalize (gcd a b) = gcd a b"
    6.68      by simp
    6.69    fix l assume "l dvd c" and "l dvd d"
    6.70    hence "l dvd gcd c d" by (rule gcd_greatest)
    6.71 @@ -484,22 +482,27 @@
    6.72  
    6.73  lemma coprime_crossproduct:
    6.74    assumes [simp]: "gcd a d = 1" "gcd b c = 1"
    6.75 -  shows "associated (a * c) (b * d) \<longleftrightarrow> associated a b \<and> associated c d" (is "?lhs \<longleftrightarrow> ?rhs")
    6.76 +  shows "normalize (a * c) = normalize (b * d) \<longleftrightarrow> normalize a  = normalize b \<and> normalize c = normalize d"
    6.77 +    (is "?lhs \<longleftrightarrow> ?rhs")
    6.78  proof
    6.79 -  assume ?rhs then show ?lhs unfolding associated_def by (fast intro: mult_dvd_mono)
    6.80 +  assume ?rhs
    6.81 +  then have "a dvd b" "b dvd a" "c dvd d" "d dvd c" by (simp_all add: associated_iff_dvd)
    6.82 +  then have "a * c dvd b * d" "b * d dvd a * c" by (fast intro: mult_dvd_mono)+
    6.83 +  then show ?lhs by (simp add: associated_iff_dvd)
    6.84  next
    6.85    assume ?lhs
    6.86 -  from \<open>?lhs\<close> have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left) 
    6.87 +  then have dvd: "a * c dvd b * d" "b * d dvd a * c" by (simp_all add: associated_iff_dvd)
    6.88 +  then have "a dvd b * d" by (metis dvd_mult_left) 
    6.89    hence "a dvd b" by (simp add: coprime_dvd_mult_iff)
    6.90 -  moreover from \<open>?lhs\<close> have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left) 
    6.91 +  moreover from dvd have "b dvd a * c" by (metis dvd_mult_left) 
    6.92    hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
    6.93 -  moreover from \<open>?lhs\<close> have "c dvd d * b" 
    6.94 -    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
    6.95 +  moreover from dvd have "c dvd d * b" 
    6.96 +    by (auto dest: dvd_mult_right simp add: ac_simps)
    6.97    hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
    6.98 -  moreover from \<open>?lhs\<close> have "d dvd c * a"
    6.99 -    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
   6.100 +  moreover from dvd have "d dvd c * a"
   6.101 +    by (auto dest: dvd_mult_right simp add: ac_simps)
   6.102    hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
   6.103 -  ultimately show ?rhs unfolding associated_def by simp
   6.104 +  ultimately show ?rhs by (simp add: associated_iff_dvd)
   6.105  qed
   6.106  
   6.107  lemma gcd_add1 [simp]:
   6.108 @@ -616,19 +619,29 @@
   6.109    apply assumption
   6.110    done
   6.111  
   6.112 +lemma lcm_gcd:
   6.113 +  "lcm a b = normalize (a * b) div gcd a b"
   6.114 +  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
   6.115 +
   6.116 +subclass semiring_gcd
   6.117 +  apply standard
   6.118 +  using gcd_right_idem
   6.119 +  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
   6.120 +  done
   6.121 +
   6.122  lemma gcd_exp:
   6.123 -  "gcd (a^n) (b^n) = (gcd a b) ^ n"
   6.124 +  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
   6.125  proof (cases "a = 0 \<and> b = 0")
   6.126 -  assume "a = 0 \<and> b = 0"
   6.127 -  then show ?thesis by (cases n, simp_all add: gcd_0_left)
   6.128 +  case True
   6.129 +  then show ?thesis by (cases n) simp_all
   6.130  next
   6.131 -  assume A: "\<not>(a = 0 \<and> b = 0)"
   6.132 -  hence "1 = gcd ((a div gcd a b)^n) ((b div gcd a b)^n)"
   6.133 -    using div_gcd_coprime by (subst sym, auto simp: div_gcd_coprime)
   6.134 -  hence "(gcd a b) ^ n = (gcd a b) ^ n * ..." by simp
   6.135 +  case False
   6.136 +  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
   6.137 +    using div_gcd_coprime by (subst sym) (auto simp: div_gcd_coprime)
   6.138 +  then have "gcd a b ^ n = gcd a b ^ n * ..." by simp
   6.139    also note gcd_mult_distrib
   6.140 -  also have "unit_factor ((gcd a b)^n) = 1"
   6.141 -    by (simp add: unit_factor_power A)
   6.142 +  also have "unit_factor (gcd a b ^ n) = 1"
   6.143 +    using False by (auto simp add: unit_factor_power unit_factor_gcd)
   6.144    also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
   6.145      by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
   6.146    also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
   6.147 @@ -749,16 +762,6 @@
   6.148      by (simp add: ac_simps)
   6.149  qed
   6.150  
   6.151 -lemma lcm_gcd:
   6.152 -  "lcm a b = normalize (a * b) div gcd a b"
   6.153 -  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
   6.154 -
   6.155 -subclass semiring_gcd
   6.156 -  apply standard
   6.157 -  using gcd_right_idem
   6.158 -  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
   6.159 -  done
   6.160 -
   6.161  lemma lcm_gcd_prod:
   6.162    "lcm a b * gcd a b = normalize (a * b)"
   6.163    by (simp add: lcm_gcd)
   6.164 @@ -783,9 +786,9 @@
   6.165  
   6.166  lemma lcmI:
   6.167    assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
   6.168 -    and "unit_factor c = (if c = 0 then 0 else 1)"
   6.169 +    and "normalize c = c"
   6.170    shows "c = lcm a b"
   6.171 -  by (rule associated_eqI) (auto simp: assms intro: associatedI lcm_least)
   6.172 +  by (rule associated_eqI) (auto simp: assms intro: lcm_least)
   6.173  
   6.174  sublocale lcm!: abel_semigroup lcm ..
   6.175  
   6.176 @@ -823,9 +826,9 @@
   6.177  
   6.178  lemma lcm_unique:
   6.179    "a dvd d \<and> b dvd d \<and> 
   6.180 -  unit_factor d = (if d = 0 then 0 else 1) \<and>
   6.181 +  normalize d = d \<and>
   6.182    (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   6.183 -  by (rule, auto intro: lcmI simp: lcm_least lcm_zero)
   6.184 +  by rule (auto intro: lcmI simp: lcm_least lcm_zero)
   6.185  
   6.186  lemma dvd_lcm_I1 [simp]:
   6.187    "k dvd m \<Longrightarrow> k dvd lcm m n"
   6.188 @@ -906,7 +909,7 @@
   6.189    apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
   6.190    apply (rule lcm_dvd2)
   6.191    apply (rule lcm_least, simp add: unit_simps, assumption)
   6.192 -  apply (subst unit_factor_lcm, simp add: lcm_zero)
   6.193 +  apply simp
   6.194    done
   6.195  
   6.196  lemma lcm_mult_unit2:
   6.197 @@ -1035,12 +1038,19 @@
   6.198  
   6.199  lemma normalize_Lcm [simp]:
   6.200    "normalize (Lcm A) = Lcm A"
   6.201 -  by (cases "Lcm A = 0") (auto intro: associated_eqI)
   6.202 +proof (cases "Lcm A = 0")
   6.203 +  case True then show ?thesis by simp
   6.204 +next
   6.205 +  case False
   6.206 +  have "unit_factor (Lcm A) * normalize (Lcm A) = Lcm A"
   6.207 +    by (fact unit_factor_mult_normalize)
   6.208 +  with False show ?thesis by simp
   6.209 +qed
   6.210  
   6.211  lemma LcmI:
   6.212    assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
   6.213 -    and "unit_factor b = (if b = 0 then 0 else 1)" shows "b = Lcm A"
   6.214 -  by (rule associated_eqI) (auto simp: assms associated_def intro: Lcm_least)
   6.215 +    and "normalize b = b" shows "b = Lcm A"
   6.216 +  by (rule associated_eqI) (auto simp: assms intro: Lcm_least)
   6.217  
   6.218  lemma Lcm_subset:
   6.219    "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
   6.220 @@ -1204,16 +1214,23 @@
   6.221  
   6.222  lemma normalize_Gcd [simp]:
   6.223    "normalize (Gcd A) = Gcd A"
   6.224 -  by (cases "Gcd A = 0") (auto intro: associated_eqI)
   6.225 +proof (cases "Gcd A = 0")
   6.226 +  case True then show ?thesis by simp
   6.227 +next
   6.228 +  case False
   6.229 +  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A"
   6.230 +    by (fact unit_factor_mult_normalize)
   6.231 +  with False show ?thesis by simp
   6.232 +qed
   6.233  
   6.234  subclass semiring_Gcd
   6.235    by standard (simp_all add: Gcd_greatest)
   6.236  
   6.237  lemma GcdI:
   6.238    assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
   6.239 -    and "unit_factor b = (if b = 0 then 0 else 1)"
   6.240 +    and "normalize b = b"
   6.241    shows "b = Gcd A"
   6.242 -  by (rule associated_eqI) (auto simp: assms associated_def intro: Gcd_greatest)
   6.243 +  by (rule associated_eqI) (auto simp: assms intro: Gcd_greatest)
   6.244  
   6.245  lemma Lcm_Gcd:
   6.246    "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
     7.1 --- a/src/HOL/Number_Theory/Fib.thy	Wed Jul 08 14:01:40 2015 +0200
     7.2 +++ b/src/HOL/Number_Theory/Fib.thy	Wed Jul 08 14:01:41 2015 +0200
     7.3 @@ -67,7 +67,7 @@
     7.4    apply (cases m)
     7.5    apply (auto simp add: fib_add)
     7.6    apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
     7.7 -    gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
     7.8 +    gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute)
     7.9    done
    7.10  
    7.11  lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
     8.1 --- a/src/HOL/Number_Theory/Gauss.thy	Wed Jul 08 14:01:40 2015 +0200
     8.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Wed Jul 08 14:01:41 2015 +0200
     8.3 @@ -112,7 +112,7 @@
     8.4      from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
     8.5      have "[x = y](mod p)"
     8.6        by (metis monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
     8.7 -                cong_mult_self_int gcd_int.commute prime_imp_coprime_int)
     8.8 +                cong_mult_self_int gcd.commute prime_imp_coprime_int)
     8.9      with cong_less_imp_eq_int [of x y p] p_minus_one_l
    8.10          order_le_less_trans [of x "(int p - 1) div 2" p]
    8.11          order_le_less_trans [of y "(int p - 1) div 2" p] 
    8.12 @@ -202,7 +202,7 @@
    8.13  
    8.14  lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
    8.15    using p_prime A_ncong_p [OF assms]
    8.16 -  by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int)
    8.17 +  by (simp add: cong_altdef_int) (metis gcd.commute prime_imp_coprime_int)
    8.18  
    8.19  lemma A_prod_relprime: "gcd (setprod id A) p = 1"
    8.20    by (metis id_def all_A_relprime setprod_coprime_int)
     9.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Wed Jul 08 14:01:40 2015 +0200
     9.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Wed Jul 08 14:01:41 2015 +0200
     9.3 @@ -98,9 +98,9 @@
     9.4    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
     9.5  proof-
     9.6    from pa have ap: "coprime a p"
     9.7 -    by (metis gcd_nat.commute) 
     9.8 +    by (metis gcd.commute) 
     9.9    have px:"coprime x p"
    9.10 -    by (metis gcd_nat.commute p prime x0 xp)
    9.11 +    by (metis gcd.commute p prime x0 xp)
    9.12    obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
    9.13      by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
    9.14    {assume y0: "y = 0"
    9.15 @@ -114,7 +114,7 @@
    9.16  lemma cong_unique_inverse_prime:
    9.17    assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
    9.18    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
    9.19 -by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms) 
    9.20 +by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd.commute assms) 
    9.21  
    9.22  lemma chinese_remainder_coprime_unique:
    9.23    fixes a::nat 
    9.24 @@ -157,7 +157,7 @@
    9.25      by auto
    9.26    also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
    9.27      apply (rule card_mono) using assms
    9.28 -    by auto (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)
    9.29 +    by auto (metis dual_order.antisym gcd_1_int gcd.commute int_one_le_iff_zero_less)
    9.30    also have "... = phi n"
    9.31      by (simp add: phi_def)
    9.32    finally show ?thesis .
    9.33 @@ -242,7 +242,7 @@
    9.34    from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp
    9.35    from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
    9.36    have an: "coprime a n" "coprime (a^(n - 1)) n"
    9.37 -    by (auto simp add: coprime_exp_nat gcd_nat.commute)
    9.38 +    by (auto simp add: coprime_exp_nat gcd.commute)
    9.39    {assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
    9.40      from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
    9.41        m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast
    9.42 @@ -251,7 +251,7 @@
    9.43        let ?y = "a^ ((n - 1) div m * m)"
    9.44        note mdeq = mod_div_equality[of "(n - 1)" m]
    9.45        have yn: "coprime ?y n"
    9.46 -        by (metis an(1) coprime_exp_nat gcd_nat.commute)
    9.47 +        by (metis an(1) coprime_exp_nat gcd.commute)
    9.48        have "?y mod n = (a^m)^((n - 1) div m) mod n"
    9.49          by (simp add: algebra_simps power_mult)
    9.50        also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
    9.51 @@ -310,7 +310,7 @@
    9.52    moreover
    9.53    {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith
    9.54      from assms have na': "coprime a n"
    9.55 -      by (metis gcd_nat.commute)
    9.56 +      by (metis gcd.commute)
    9.57      from phi_lowerbound_1_nat[OF n2] euler_theorem_nat [OF na']
    9.58      have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="phi n"], auto) }
    9.59    ultimately have ex: "\<exists>m>0. ?P m" by blast
    9.60 @@ -367,7 +367,7 @@
    9.61        obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
    9.62        from lh
    9.63        obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"
    9.64 -        by (metis H d0 gcd_nat.commute lucas_coprime_lemma) 
    9.65 +        by (metis H d0 gcd.commute lucas_coprime_lemma) 
    9.66        hence "a ^ d + n * q1 - n * q2 = 1" by simp
    9.67        with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2  d' p
    9.68        have "p dvd 1"
    9.69 @@ -404,7 +404,7 @@
    9.70  
    9.71  lemma order_divides_phi: 
    9.72    fixes n::nat shows "coprime n a \<Longrightarrow> ord n a dvd phi n"
    9.73 -  by (metis ord_divides euler_theorem_nat gcd_nat.commute)
    9.74 +  by (metis ord_divides euler_theorem_nat gcd.commute)
    9.75  
    9.76  lemma order_divides_expdiff:
    9.77    fixes n::nat and a::nat assumes na: "coprime n a"
    9.78 @@ -415,11 +415,11 @@
    9.79      hence "\<exists>c. d = e + c" by presburger
    9.80      then obtain c where c: "d = e + c" by presburger
    9.81      from na have an: "coprime a n"
    9.82 -      by (metis gcd_nat.commute)
    9.83 +      by (metis gcd.commute)
    9.84      have aen: "coprime (a^e) n"
    9.85 -      by (metis coprime_exp_nat gcd_nat.commute na)      
    9.86 +      by (metis coprime_exp_nat gcd.commute na)      
    9.87      have acn: "coprime (a^c) n"
    9.88 -      by (metis coprime_exp_nat gcd_nat.commute na) 
    9.89 +      by (metis coprime_exp_nat gcd.commute na) 
    9.90      have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
    9.91        using c by simp
    9.92      also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
    9.93 @@ -588,7 +588,7 @@
    9.94             gcd_lcm_complete_lattice_nat.top_greatest pn)} 
    9.95    hence cpa: "coprime p a" by auto
    9.96    have arp: "coprime (a^r) p"
    9.97 -    by (metis coprime_exp_nat cpa gcd_nat.commute) 
    9.98 +    by (metis coprime_exp_nat cpa gcd.commute) 
    9.99    from euler_theorem_nat[OF arp, simplified ord_divides] o phip
   9.100    have "q dvd (p - 1)" by simp
   9.101    then obtain d where d:"p - 1 = q * d" 
    10.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Jul 08 14:01:40 2015 +0200
    10.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Jul 08 14:01:41 2015 +0200
    10.3 @@ -44,7 +44,7 @@
    10.4  
    10.5  lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
    10.6    apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
    10.7 -  apply (metis dvd_eq_mod_eq_0 even_Suc even_iff_mod_2_eq_zero mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
    10.8 +  apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
    10.9    done
   10.10  
   10.11  (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
   10.12 @@ -159,11 +159,11 @@
   10.13  
   10.14  
   10.15  lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   10.16 -  by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
   10.17 +  by (metis coprime_exp_nat gcd.commute prime_imp_coprime_nat)
   10.18  
   10.19  lemma prime_imp_power_coprime_int:
   10.20    fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   10.21 -  by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
   10.22 +  by (metis coprime_exp_int gcd.commute prime_imp_coprime_int)
   10.23  
   10.24  lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   10.25    by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
   10.26 @@ -375,7 +375,7 @@
   10.27  lemma bezout_gcd_nat:
   10.28    fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
   10.29    using bezout_nat[of a b]
   10.30 -by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute
   10.31 +by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd.commute
   10.32    gcd_nat.right_neutral mult_0)
   10.33  
   10.34  lemma gcd_bezout_sum_nat:
   10.35 @@ -423,7 +423,7 @@
   10.36    shows "\<exists>x y. a*x = Suc (p*y)"
   10.37  proof-
   10.38    have ap: "coprime a p"
   10.39 -    by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
   10.40 +    by (metis gcd.commute p pa prime_imp_coprime_nat)
   10.41    from coprime_bezout_strong[OF ap] show ?thesis
   10.42      by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
   10.43  qed
    11.1 --- a/src/HOL/Number_Theory/Residues.thy	Wed Jul 08 14:01:40 2015 +0200
    11.2 +++ b/src/HOL/Number_Theory/Residues.thy	Wed Jul 08 14:01:41 2015 +0200
    11.3 @@ -166,15 +166,20 @@
    11.4  lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus>i\<in>A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
    11.5    by (induct set: finite) (auto simp: zero_cong add_cong)
    11.6  
    11.7 -lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R"
    11.8 -  apply (subst res_units_eq)
    11.9 -  apply auto
   11.10 -  apply (insert pos_mod_sign [of m a])
   11.11 -  apply (subgoal_tac "a mod m \<noteq> 0")
   11.12 -  apply arith
   11.13 -  apply auto
   11.14 -  apply (metis gcd_int.commute gcd_red_int)
   11.15 -  done
   11.16 +lemma mod_in_res_units [simp]:
   11.17 +  assumes "1 < m" and "coprime a m"
   11.18 +  shows "a mod m \<in> Units R"
   11.19 +proof (cases "a mod m = 0")
   11.20 +  case True with assms show ?thesis
   11.21 +    by (auto simp add: res_units_eq gcd_red_int [symmetric])
   11.22 +next
   11.23 +  case False
   11.24 +  from assms have "0 < m" by simp
   11.25 +  with pos_mod_sign [of m a] have "0 \<le> a mod m" .
   11.26 +  with False have "0 < a mod m" by simp
   11.27 +  with assms show ?thesis
   11.28 +    by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps)
   11.29 +qed
   11.30  
   11.31  lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
   11.32    unfolding cong_int_def by auto
   11.33 @@ -354,10 +359,7 @@
   11.34    shows "[a^(p - 1) = 1] (mod p)"
   11.35  proof -
   11.36    from assms have "[a ^ phi p = 1] (mod p)"
   11.37 -    apply (intro euler_theorem)
   11.38 -    apply (metis of_nat_0_le_iff)
   11.39 -    apply (metis gcd_int.commute prime_imp_coprime_int)
   11.40 -    done
   11.41 +    by (auto intro!: euler_theorem dest!: prime_imp_coprime_int simp add: ac_simps)
   11.42    also have "phi p = nat p - 1"
   11.43      by (rule phi_prime) (rule assms)
   11.44    finally show ?thesis
    12.1 --- a/src/HOL/Rat.thy	Wed Jul 08 14:01:40 2015 +0200
    12.2 +++ b/src/HOL/Rat.thy	Wed Jul 08 14:01:41 2015 +0200
    12.3 @@ -1001,7 +1001,7 @@
    12.4      in if a = 0 then (0, 1) else (sgn a * b, \<bar>a\<bar>))"
    12.5  proof (cases p)
    12.6    case (Fract a b) then show ?thesis
    12.7 -    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd_int.commute)
    12.8 +    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd.commute)
    12.9  qed
   12.10  
   12.11  lemma rat_divide_code [code abstract]:
    13.1 --- a/src/HOL/Rings.thy	Wed Jul 08 14:01:40 2015 +0200
    13.2 +++ b/src/HOL/Rings.thy	Wed Jul 08 14:01:41 2015 +0200
    13.3 @@ -636,6 +636,13 @@
    13.4  class algebraic_semidom = semidom_divide
    13.5  begin
    13.6  
    13.7 +text \<open>
    13.8 +  Class @{class algebraic_semidom} enriches a integral domain
    13.9 +  by notions from algebra, like units in a ring.
   13.10 +  It is a separate class to avoid spoiling fields with notions
   13.11 +  which are degenerated there.
   13.12 +\<close>
   13.13 +
   13.14  lemma dvd_div_mult_self [simp]:
   13.15    "a dvd b \<Longrightarrow> b div a * a = b"
   13.16    by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
   13.17 @@ -834,84 +841,11 @@
   13.18      by (rule dvd_div_mult2_eq)
   13.19  qed
   13.20  
   13.21 -
   13.22 -text \<open>Associated elements in a ring --- an equivalence relation induced
   13.23 -  by the quasi-order divisibility.\<close>
   13.24 -
   13.25 -definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   13.26 -where
   13.27 -  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
   13.28 -
   13.29 -lemma associatedI:
   13.30 -  "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
   13.31 -  by (simp add: associated_def)
   13.32 -
   13.33 -lemma associatedD1:
   13.34 -  "associated a b \<Longrightarrow> a dvd b"
   13.35 -  by (simp add: associated_def)
   13.36 -
   13.37 -lemma associatedD2:
   13.38 -  "associated a b \<Longrightarrow> b dvd a"
   13.39 -  by (simp add: associated_def)
   13.40 -
   13.41 -lemma associated_refl [simp]:
   13.42 -  "associated a a"
   13.43 -  by (auto intro: associatedI)
   13.44 -
   13.45 -lemma associated_sym:
   13.46 -  "associated b a \<longleftrightarrow> associated a b"
   13.47 -  by (auto intro: associatedI dest: associatedD1 associatedD2)
   13.48 -
   13.49 -lemma associated_trans:
   13.50 -  "associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c"
   13.51 -  by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)
   13.52 -
   13.53 -lemma associated_0 [simp]:
   13.54 -  "associated 0 b \<longleftrightarrow> b = 0"
   13.55 -  "associated a 0 \<longleftrightarrow> a = 0"
   13.56 -  by (auto dest: associatedD1 associatedD2)
   13.57 -
   13.58 -lemma associated_unit:
   13.59 -  "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
   13.60 -  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
   13.61 -
   13.62 -lemma is_unit_associatedI:
   13.63 -  assumes "is_unit c" and "a = c * b"
   13.64 -  shows "associated a b"
   13.65 -proof (rule associatedI)
   13.66 -  from `a = c * b` show "b dvd a" by auto
   13.67 -  from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE)
   13.68 -  moreover from `a = c * b` have "d * a = d * (c * b)" by simp
   13.69 -  ultimately have "b = a * d" by (simp add: ac_simps)
   13.70 -  then show "a dvd b" ..
   13.71 -qed
   13.72 -
   13.73 -lemma associated_is_unitE:
   13.74 -  assumes "associated a b"
   13.75 -  obtains c where "is_unit c" and "a = c * b"
   13.76 -proof (cases "b = 0")
   13.77 -  case True with assms have "is_unit 1" and "a = 1 * b" by simp_all
   13.78 -  with that show thesis .
   13.79 -next
   13.80 -  case False
   13.81 -  from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)
   13.82 -  then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)
   13.83 -  then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)
   13.84 -  with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp
   13.85 -  then have "is_unit c" by auto
   13.86 -  with `a = c * b` that show thesis by blast
   13.87 -qed
   13.88 -
   13.89  lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
   13.90    dvd_div_unit_iff unit_div_mult_swap unit_div_commute
   13.91    unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   13.92    unit_eq_div1 unit_eq_div2
   13.93  
   13.94 -end
   13.95 -
   13.96 -context algebraic_semidom
   13.97 -begin
   13.98 -
   13.99  lemma is_unit_divide_mult_cancel_left:
  13.100    assumes "a \<noteq> 0" and "is_unit b"
  13.101    shows "a div (a * b) = 1 div b"
  13.102 @@ -941,6 +875,16 @@
  13.103    assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
  13.104  begin
  13.105  
  13.106 +text \<open>
  13.107 +  Class @{class normalization_semidom} cultivates the idea that
  13.108 +  each integral domain can be split into equivalence classes
  13.109 +  whose representants are associated, i.e. divide each other.
  13.110 +  @{const normalize} specifies a canonical representant for each equivalence
  13.111 +  class.  The rationale behind this is that it is easier to reason about equality
  13.112 +  than equivalences, hence we prefer to think about equality of normalized
  13.113 +  values rather than associated elements.
  13.114 +\<close>
  13.115 +
  13.116  lemma unit_factor_dvd [simp]:
  13.117    "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
  13.118    by (rule unit_imp_dvd) simp
  13.119 @@ -1140,54 +1084,74 @@
  13.120    then show ?thesis by simp
  13.121  qed
  13.122  
  13.123 -lemma associated_normalize_left [simp]:
  13.124 -  "associated (normalize a) b \<longleftrightarrow> associated a b"
  13.125 -  by (auto simp add: associated_def)
  13.126 +text \<open>
  13.127 +  We avoid an explicit definition of associated elements but prefer
  13.128 +  explicit normalisation instead.  In theory we could define an abbreviation
  13.129 +  like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is
  13.130 +  counterproductive without suggestive infix syntax, which we do not want
  13.131 +  to sacrifice for this purpose here.
  13.132 +\<close>
  13.133  
  13.134 -lemma associated_normalize_right [simp]:
  13.135 -  "associated a (normalize b) \<longleftrightarrow> associated a b"
  13.136 -  by (auto simp add: associated_def)
  13.137 -
  13.138 -lemma associated_iff_normalize:
  13.139 -  "associated a b \<longleftrightarrow> normalize a = normalize b" (is "?P \<longleftrightarrow> ?Q")
  13.140 +lemma associatedI:
  13.141 +  assumes "a dvd b" and "b dvd a"
  13.142 +  shows "normalize a = normalize b"
  13.143  proof (cases "a = 0 \<or> b = 0")
  13.144 -  case True then show ?thesis by auto
  13.145 +  case True with assms show ?thesis by auto
  13.146  next
  13.147    case False
  13.148 -  show ?thesis
  13.149 -  proof
  13.150 -    assume ?P then show ?Q
  13.151 -      by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize)
  13.152 +  from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
  13.153 +  moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
  13.154 +  ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)
  13.155 +  with False have "1 = c * d"
  13.156 +    unfolding mult_cancel_left by simp
  13.157 +  then have "is_unit c" and "is_unit d" by auto
  13.158 +  with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)
  13.159 +qed
  13.160 +
  13.161 +lemma associatedD1:
  13.162 +  "normalize a = normalize b \<Longrightarrow> a dvd b"
  13.163 +  using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
  13.164 +  by simp
  13.165 +
  13.166 +lemma associatedD2:
  13.167 +  "normalize a = normalize b \<Longrightarrow> b dvd a"
  13.168 +  using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
  13.169 +  by simp
  13.170 +
  13.171 +lemma associated_unit:
  13.172 +  "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
  13.173 +  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
  13.174 +
  13.175 +lemma associated_iff_dvd:
  13.176 +  "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")
  13.177 +proof
  13.178 +  assume ?Q then show ?P by (auto intro!: associatedI)
  13.179 +next
  13.180 +  assume ?P
  13.181 +  then have "unit_factor a * normalize a = unit_factor a * normalize b"
  13.182 +    by simp
  13.183 +  then have *: "normalize b * unit_factor a = a"
  13.184 +    by (simp add: ac_simps)
  13.185 +  show ?Q
  13.186 +  proof (cases "a = 0 \<or> b = 0")
  13.187 +    case True with \<open>?P\<close> show ?thesis by auto
  13.188    next
  13.189 -    from False have *: "is_unit (unit_factor a div unit_factor b)"
  13.190 -      by auto
  13.191 -    assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b"
  13.192 -      by simp
  13.193 -    then have "a = unit_factor a * (b div unit_factor b)"
  13.194 -      by simp
  13.195 -    with False have "a = (unit_factor a div unit_factor b) * b"
  13.196 -      by (simp add: unit_div_commute unit_div_mult_swap [symmetric])
  13.197 -    with * show ?P 
  13.198 -      by (rule is_unit_associatedI)
  13.199 +    case False 
  13.200 +    then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
  13.201 +      by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
  13.202 +    with * show ?thesis by simp
  13.203    qed
  13.204  qed
  13.205  
  13.206  lemma associated_eqI:
  13.207 -  assumes "associated a b"
  13.208 -  assumes "a \<noteq> 0 \<Longrightarrow> unit_factor a = 1" and "b \<noteq> 0 \<Longrightarrow> unit_factor b = 1"
  13.209 +  assumes "a dvd b" and "b dvd a"
  13.210 +  assumes "normalize a = a" and "normalize b = b"
  13.211    shows "a = b"
  13.212 -proof (cases "a = 0")
  13.213 -  case True with assms show ?thesis by simp
  13.214 -next
  13.215 -  case False with assms have "b \<noteq> 0" by auto
  13.216 -  with False assms have "unit_factor a = unit_factor b"
  13.217 -    by simp
  13.218 -  moreover from assms have "normalize a = normalize b"
  13.219 -    by (simp add: associated_iff_normalize)
  13.220 -  ultimately have "unit_factor a * normalize a = unit_factor b * normalize b"
  13.221 -    by simp
  13.222 -  then show ?thesis
  13.223 -    by simp
  13.224 +proof -
  13.225 +  from assms have "normalize a = normalize b"
  13.226 +    unfolding associated_iff_dvd by simp
  13.227 +  with \<open>normalize a = a\<close> have "a = normalize b" by simp
  13.228 +  with \<open>normalize b = b\<close> show "a = b" by simp
  13.229  qed
  13.230  
  13.231  end
    14.1 --- a/src/HOL/Transcendental.thy	Wed Jul 08 14:01:40 2015 +0200
    14.2 +++ b/src/HOL/Transcendental.thy	Wed Jul 08 14:01:41 2015 +0200
    14.3 @@ -3602,11 +3602,15 @@
    14.4      done
    14.5  qed
    14.6  
    14.7 -lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
    14.8 +lemma sin_zero_iff_int2:
    14.9 +  "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
   14.10    apply (simp only: sin_zero_iff_int)
   14.11    apply (safe elim!: evenE)
   14.12    apply (simp_all add: field_simps)
   14.13 -  using dvd_triv_left by fastforce
   14.14 +  apply (subst real_numeral(1) [symmetric])
   14.15 +  apply (simp only: real_of_int_mult [symmetric] real_of_int_inject)
   14.16 +  apply auto
   14.17 +  done
   14.18  
   14.19  lemma cos_monotone_0_pi:
   14.20    assumes "0 \<le> y" and "y < x" and "x \<le> pi"