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]: