src/HOL/GCD.thy
changeset 33657 a4179bf442d1
parent 33318 ddd97d9dfbfb
child 33946 fcc20072df9a
     1.1 --- a/src/HOL/GCD.thy	Thu Nov 12 14:32:21 2009 -0800
     1.2 +++ b/src/HOL/GCD.thy	Fri Nov 13 14:14:04 2009 +0100
     1.3 @@ -312,13 +312,13 @@
     1.4    by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
     1.5  
     1.6  lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
     1.7 -  by (rule dvd_anti_sym, auto)
     1.8 +  by (rule dvd_antisym, auto)
     1.9  
    1.10  lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
    1.11    by (auto simp add: gcd_int_def gcd_commute_nat)
    1.12  
    1.13  lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
    1.14 -  apply (rule dvd_anti_sym)
    1.15 +  apply (rule dvd_antisym)
    1.16    apply (blast intro: dvd_trans)+
    1.17  done
    1.18  
    1.19 @@ -339,23 +339,18 @@
    1.20  lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
    1.21      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    1.22    apply auto
    1.23 -  apply (rule dvd_anti_sym)
    1.24 +  apply (rule dvd_antisym)
    1.25    apply (erule (1) gcd_greatest_nat)
    1.26    apply auto
    1.27  done
    1.28  
    1.29  lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
    1.30      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    1.31 -  apply (case_tac "d = 0")
    1.32 -  apply force
    1.33 -  apply (rule iffI)
    1.34 -  apply (rule zdvd_anti_sym)
    1.35 -  apply arith
    1.36 -  apply (subst gcd_pos_int)
    1.37 -  apply clarsimp
    1.38 -  apply (drule_tac x = "d + 1" in spec)
    1.39 -  apply (frule zdvd_imp_le)
    1.40 -  apply (auto intro: gcd_greatest_int)
    1.41 +apply (case_tac "d = 0")
    1.42 + apply simp
    1.43 +apply (rule iffI)
    1.44 + apply (rule zdvd_antisym_nonneg)
    1.45 + apply (auto intro: gcd_greatest_int)
    1.46  done
    1.47  
    1.48  lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
    1.49 @@ -417,7 +412,7 @@
    1.50    by (auto intro: coprime_dvd_mult_int)
    1.51  
    1.52  lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
    1.53 -  apply (rule dvd_anti_sym)
    1.54 +  apply (rule dvd_antisym)
    1.55    apply (rule gcd_greatest_nat)
    1.56    apply (rule_tac n = k in coprime_dvd_mult_nat)
    1.57    apply (simp add: gcd_assoc_nat)
    1.58 @@ -1381,11 +1376,11 @@
    1.59  
    1.60  lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
    1.61      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    1.62 -  by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
    1.63 +  by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
    1.64  
    1.65  lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
    1.66      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    1.67 -  by (auto intro: dvd_anti_sym [transferred] lcm_least_int)
    1.68 +  by (auto intro: dvd_antisym [transferred] lcm_least_int)
    1.69  
    1.70  lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
    1.71    apply (rule sym)