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.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)
```