src/HOL/GCD.thy
 changeset 31813 4df828bbc411 parent 31798 fe9a3043d36c child 31814 7c122634da81
```     1.1 --- a/src/HOL/GCD.thy	Thu Jun 25 20:26:17 2009 +0200
1.2 +++ b/src/HOL/GCD.thy	Fri Jun 26 10:46:33 2009 +0200
1.3 @@ -181,8 +181,17 @@
1.4  lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
1.6
1.7 +lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
1.9 +
1.10  lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
1.11 -  by (simp add: gcd_int_def)
1.13 +
1.14 +lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
1.15 +by (metis abs_idempotent int_gcd_abs)
1.16 +
1.17 +lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
1.18 +by (metis abs_idempotent int_gcd_abs)
1.19
1.20  lemma int_gcd_cases:
1.21    fixes x :: int and y
1.22 @@ -252,7 +261,7 @@
1.23  by simp
1.24
1.25  lemma int_gcd_idem: "gcd (x::int) x = abs x"
1.26 -by (subst int_gcd_abs, auto simp add: gcd_int_def)
1.27 +by (auto simp add: gcd_int_def)
1.28
1.29  declare gcd_nat.simps [simp del]
1.30
1.31 @@ -269,18 +278,10 @@
1.32  done
1.33
1.34  lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
1.35 -  apply (subst int_gcd_abs)
1.36 -  apply (rule dvd_trans)
1.37 -  apply (rule nat_gcd_dvd1 [transferred])
1.38 -  apply auto
1.39 -done
1.40 +by (metis gcd_int_def int_dvd_iff nat_gcd_dvd1)
1.41
1.42  lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
1.43 -  apply (subst int_gcd_abs)
1.44 -  apply (rule dvd_trans)
1.45 -  apply (rule nat_gcd_dvd2 [transferred])
1.46 -  apply auto
1.47 -done
1.48 +by (metis gcd_int_def int_dvd_iff nat_gcd_dvd2)
1.49
1.50  lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
1.51  by(metis nat_gcd_dvd1 dvd_trans)
1.52 @@ -310,13 +311,11 @@
1.53  by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
1.54
1.55  lemma int_gcd_greatest:
1.56 -  assumes "(k::int) dvd m" and "k dvd n"
1.57 -  shows "k dvd gcd m n"
1.58 -
1.59 +  "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
1.60    apply (subst int_gcd_abs)
1.61    apply (subst abs_dvd_iff [symmetric])
1.62    apply (rule nat_gcd_greatest [transferred])
1.63 -  using prems apply auto
1.64 +  apply auto
1.65  done
1.66
1.67  lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
1.68 @@ -412,7 +411,7 @@
1.69
1.70  lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
1.71    apply (subst (1 2) int_gcd_abs)
1.72 -  apply (simp add: abs_mult)
1.73 +  apply (subst (1 2) abs_mult)
1.74    apply (rule nat_gcd_mult_distrib [transferred])
1.75    apply auto
1.76  done
1.77 @@ -425,16 +424,14 @@
1.78    done
1.79
1.80  lemma int_coprime_dvd_mult:
1.81 -  assumes "coprime (k::int) n" and "k dvd m * n"
1.82 -  shows "k dvd m"
1.83 -
1.84 -  using prems
1.85 -  apply (subst abs_dvd_iff [symmetric])
1.86 -  apply (subst dvd_abs_iff [symmetric])
1.87 -  apply (subst (asm) int_gcd_abs)
1.88 -  apply (rule nat_coprime_dvd_mult [transferred])
1.89 -  apply auto
1.90 -  apply (subst abs_mult [symmetric], auto)
1.91 +  "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
1.92 +apply (subst abs_dvd_iff [symmetric])
1.93 +apply (subst dvd_abs_iff [symmetric])
1.94 +apply (subst (asm) int_gcd_abs)
1.95 +apply (rule nat_coprime_dvd_mult [transferred])
1.96 +    prefer 4 apply assumption
1.97 +   apply auto
1.98 +apply (subst abs_mult [symmetric], auto)
1.99  done
1.100
1.101  lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
1.102 @@ -455,14 +452,10 @@
1.103  done
1.104
1.105  lemma int_gcd_mult_cancel:
1.106 -  assumes "coprime (k::int) n"
1.107 -  shows "gcd (k * m) n = gcd m n"
1.108 -
1.109 -  using prems
1.110 -  apply (subst (1 2) int_gcd_abs)
1.111 -  apply (subst abs_mult)
1.112 -  apply (rule nat_gcd_mult_cancel [transferred])
1.113 -  apply (auto simp add: int_gcd_abs [symmetric])
1.114 +  "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
1.115 +apply (subst (1 2) int_gcd_abs)
1.116 +apply (subst abs_mult)
1.117 +apply (rule nat_gcd_mult_cancel [transferred], auto)
1.118  done
1.119
1.120  text {* \medskip Addition laws *}
1.121 @@ -573,7 +566,7 @@
1.122
1.123  subsection {* Coprimality *}
1.124
1.125 -lemma nat_div_gcd_coprime [intro]:
1.126 +lemma nat_div_gcd_coprime:
1.127    assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
1.128    shows "coprime (a div gcd a b) (b div gcd a b)"
1.129  proof -
1.130 @@ -597,16 +590,16 @@
1.131    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
1.132  qed
1.133
1.134 -lemma int_div_gcd_coprime [intro]:
1.135 +lemma int_div_gcd_coprime:
1.136    assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
1.137    shows "coprime (a div gcd a b) (b div gcd a b)"
1.138 -
1.139 -  apply (subst (1 2 3) int_gcd_abs)
1.140 -  apply (subst (1 2) abs_div)
1.141 -  apply auto
1.142 -  prefer 3
1.143 -  apply (rule nat_div_gcd_coprime [transferred])
1.144 -  using nz apply (auto simp add: int_gcd_abs [symmetric])
1.145 +apply (subst (1 2 3) int_gcd_abs)
1.146 +apply (subst (1 2) abs_div)
1.147 +  apply simp
1.148 + apply simp
1.149 +apply(subst (1 2) abs_gcd_int)
1.150 +apply (rule nat_div_gcd_coprime [transferred])
1.151 +using nz apply (auto simp add: int_gcd_abs [symmetric])
1.152  done
1.153
1.154  lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
1.155 @@ -771,7 +764,7 @@
1.156    thus ?thesis by simp
1.157    next assume "~(a = 0 & b = 0)"
1.158    hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
1.159 -    by auto
1.160 +    by (auto simp:nat_div_gcd_coprime)
1.161    hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
1.162        ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
1.163      apply (subst (1 2) mult_commute)
```