src/HOL/GCD.thy
 changeset 60688 01488b559910 parent 60687 33dbbcb6a8a3 child 60689 8a2d7c04d8c0
```     1.1 --- a/src/HOL/GCD.thy	Wed Jul 08 14:01:40 2015 +0200
1.2 +++ b/src/HOL/GCD.thy	Wed Jul 08 14:01:41 2015 +0200
1.3 @@ -74,16 +74,6 @@
1.4
1.5  end
1.6
1.7 -context algebraic_semidom
1.8 -begin
1.9 -
1.10 -lemma associated_1 [simp]:
1.11 -  "associated 1 a \<longleftrightarrow> is_unit a"
1.12 -  "associated a 1 \<longleftrightarrow> is_unit a"
1.13 -  by (auto simp add: associated_def)
1.14 -
1.15 -end
1.16 -
1.17  declare One_nat_def [simp del]
1.18
1.19  subsection {* GCD and LCM definitions *}
1.20 @@ -116,29 +106,11 @@
1.21
1.22  lemma gcd_0_left [simp]:
1.23    "gcd 0 a = normalize a"
1.24 -proof (rule associated_eqI)
1.25 -  show "associated (gcd 0 a) (normalize a)"
1.26 -    by (auto intro!: associatedI gcd_greatest)
1.27 -  show "unit_factor (gcd 0 a) = 1" if "gcd 0 a \<noteq> 0"
1.28 -  proof -
1.29 -    from that have "unit_factor (normalize (gcd 0 a)) = 1"
1.30 -      by (rule unit_factor_normalize)
1.31 -    then show ?thesis by simp
1.32 -  qed
1.33 -qed simp
1.34 +  by (rule associated_eqI) simp_all
1.35
1.36  lemma gcd_0_right [simp]:
1.37    "gcd a 0 = normalize a"
1.38 -proof (rule associated_eqI)
1.39 -  show "associated (gcd a 0) (normalize a)"
1.40 -    by (auto intro!: associatedI gcd_greatest)
1.41 -  show "unit_factor (gcd a 0) = 1" if "gcd a 0 \<noteq> 0"
1.42 -  proof -
1.43 -    from that have "unit_factor (normalize (gcd a 0)) = 1"
1.44 -      by (rule unit_factor_normalize)
1.45 -    then show ?thesis by simp
1.46 -  qed
1.47 -qed simp
1.48 +  by (rule associated_eqI) simp_all
1.49
1.50  lemma gcd_eq_0_iff [simp]:
1.51    "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q")
1.52 @@ -169,7 +141,7 @@
1.53  proof
1.54    fix a b c
1.55    show "gcd a b = gcd b a"
1.56 -    by (rule associated_eqI) (auto intro: associatedI gcd_greatest simp add: unit_factor_gcd)
1.57 +    by (rule associated_eqI) simp_all
1.58    from gcd_dvd1 have "gcd (gcd a b) c dvd a"
1.59      by (rule dvd_trans) simp
1.60    moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
1.61 @@ -182,10 +154,8 @@
1.62      by (rule dvd_trans) simp
1.63    ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
1.64      by (auto intro!: gcd_greatest)
1.65 -  from P1 P2 have "associated (gcd (gcd a b) c) (gcd a (gcd b c))"
1.66 -    by (rule associatedI)
1.67 -  then show "gcd (gcd a b) c = gcd a (gcd b c)"
1.68 -    by (rule associated_eqI) (simp_all add: unit_factor_gcd)
1.69 +  from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
1.70 +    by (rule associated_eqI) simp_all
1.71  qed
1.72
1.73  lemma gcd_self [simp]:
1.74 @@ -193,15 +163,13 @@
1.75  proof -
1.76    have "a dvd gcd a a"
1.77      by (rule gcd_greatest) simp_all
1.78 -  then have "associated (gcd a a) (normalize a)"
1.79 -    by (auto intro: associatedI)
1.80    then show ?thesis
1.81 -    by (auto intro: associated_eqI simp add: unit_factor_gcd)
1.82 +    by (auto intro: associated_eqI)
1.83  qed
1.84
1.85  lemma coprime_1_left [simp]:
1.86    "coprime 1 a"
1.87 -  by (rule associated_eqI) (simp_all add: unit_factor_gcd)
1.88 +  by (rule associated_eqI) simp_all
1.89
1.90  lemma coprime_1_right [simp]:
1.91    "coprime a 1"
1.92 @@ -218,7 +186,7 @@
1.93    moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b"
1.94      by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
1.95    ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
1.96 -    by - (rule associated_eqI, auto intro: associated_eqI associatedI simp add: unit_factor_gcd)
1.97 +    by (auto intro: associated_eqI)
1.98    then show ?thesis by (simp add: normalize_mult)
1.99  qed
1.100
1.101 @@ -318,14 +286,15 @@
1.102    fix a b c
1.103    show "lcm a b = lcm b a"
1.104      by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
1.105 -  have "associated (lcm (lcm a b) c) (lcm a (lcm b c))"
1.106 -    by (auto intro!: associatedI lcm_least
1.107 +  have "lcm (lcm a b) c dvd lcm a (lcm b c)"
1.108 +    and "lcm a (lcm b c) dvd lcm (lcm a b) c"
1.109 +    by (auto intro: lcm_least
1.110        dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
1.111        dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
1.112        dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
1.113        dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
1.114    then show "lcm (lcm a b) c = lcm a (lcm b c)"
1.115 -    by (rule associated_eqI) (simp_all add: unit_factor_lcm lcm_eq_0_iff)
1.116 +    by (rule associated_eqI) simp_all
1.117  qed
1.118
1.119  lemma lcm_self [simp]:
1.120 @@ -333,10 +302,8 @@
1.121  proof -
1.122    have "lcm a a dvd a"
1.123      by (rule lcm_least) simp_all
1.124 -  then have "associated (lcm a a) (normalize a)"
1.125 -    by (auto intro: associatedI)
1.126    then show ?thesis
1.127 -    by (rule associated_eqI) (auto simp add: unit_factor_lcm)
1.128 +    by (auto intro: associated_eqI)
1.129  qed
1.130
1.131  lemma gcd_mult_lcm [simp]:
1.132 @@ -471,10 +438,8 @@
1.133        ultimately show ?thesis by (blast intro: dvd_trans)
1.134      qed
1.135    qed
1.136 -  ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))"
1.137 -    by (rule associatedI)
1.138 -  then show ?thesis
1.139 -    by (rule associated_eqI) (auto simp add: unit_factor_gcd unit_factor_Gcd)
1.140 +  ultimately show ?thesis
1.141 +    by (auto intro: associated_eqI)
1.142  qed
1.143
1.144  lemma dvd_Gcd: -- \<open>FIXME remove\<close>
1.145 @@ -507,10 +472,10 @@
1.146      ultimately show "Gcd (normalize ` A) dvd a"
1.147        by simp
1.148    qed
1.149 -  then have "associated (Gcd (normalize ` A)) (Gcd A)"
1.150 -    by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd)
1.151 +  then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
1.152 +    by (auto intro!: Gcd_greatest intro: Gcd_dvd)
1.153    then show ?thesis
1.154 -    by (rule associated_eqI) (simp_all add: unit_factor_Gcd, auto dest!: bspec)
1.155 +    by (auto intro: associated_eqI)
1.156  qed
1.157
1.158  lemma Lcm_least:
1.159 @@ -604,10 +569,8 @@
1.160        ultimately show ?thesis by (blast intro: dvd_trans)
1.161      qed
1.162    qed
1.163 -  ultimately have "associated (lcm a (Lcm A)) (Lcm (insert a A))"
1.164 -    by (rule associatedI)
1.165 -  then show "lcm a (Lcm A) = Lcm (insert a A)"
1.166 -    by (rule associated_eqI) (simp_all add: unit_factor_lcm unit_factor_Lcm lcm_eq_0_iff)
1.167 +  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
1.168 +    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
1.169  qed
1.170
1.171  lemma Lcm_set [code_unfold]:
```