src/HOL/Library/Polynomial.thy
 changeset 31663 5eb82f064630 parent 31021 53642251a04f child 31998 2c7a24f74db9
1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jun 15 21:29:04 2009 -0700
1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Jun 16 00:01:32 2009 -0700
1.3 @@ -632,6 +632,25 @@
1.4    shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
1.5    by (safe elim!: dvd_smult dvd_smult_cancel)
1.7 +lemma smult_dvd_cancel:
1.8 +  "smult a p dvd q \<Longrightarrow> p dvd q"
1.9 +proof -
1.10 +  assume "smult a p dvd q"
1.11 +  then obtain k where "q = smult a p * k" ..
1.12 +  then have "q = p * smult a k" by simp
1.13 +  then show "p dvd q" ..
1.14 +qed
1.15 +
1.16 +lemma smult_dvd:
1.17 +  fixes a :: "'a::field"
1.18 +  shows "p dvd q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> smult a p dvd q"
1.19 +  by (rule smult_dvd_cancel [where a="inverse a"]) simp
1.20 +
1.21 +lemma smult_dvd_iff:
1.22 +  fixes a :: "'a::field"
1.23 +  shows "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
1.24 +  by (auto elim: smult_dvd smult_dvd_cancel)
1.25 +
1.26  lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
1.27  by (induct n, simp, auto intro: order_trans degree_mult_le)
1.29 @@ -1102,6 +1121,109 @@
1.30  done
1.33 +subsection {* GCD of polynomials *}
1.34 +
1.35 +function
1.36 +  poly_gcd :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
1.37 +  "poly_gcd x 0 = smult (inverse (coeff x (degree x))) x"
1.38 +| "y \<noteq> 0 \<Longrightarrow> poly_gcd x y = poly_gcd y (x mod y)"
1.39 +by auto
1.40 +
1.41 +termination poly_gcd
1.42 +by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
1.43 +   (auto dest: degree_mod_less)
1.44 +
1.45 +declare poly_gcd.simps [simp del, code del]
1.46 +
1.47 +lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x"
1.48 +  and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
1.49 +  apply (induct x y rule: poly_gcd.induct)
1.50 +  apply (simp_all add: poly_gcd.simps)
1.51 +  apply (fastsimp simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
1.52 +  apply (blast dest: dvd_mod_imp_dvd)
1.53 +  done
1.54 +
1.55 +lemma poly_gcd_greatest: "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd poly_gcd x y"
1.56 +  by (induct x y rule: poly_gcd.induct)
1.57 +     (simp_all add: poly_gcd.simps dvd_mod dvd_smult)
1.58 +
1.59 +lemma dvd_poly_gcd_iff [iff]:
1.60 +  "k dvd poly_gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
1.61 +  by (blast intro!: poly_gcd_greatest intro: dvd_trans)
1.62 +
1.63 +lemma poly_gcd_monic:
1.64 +  "coeff (poly_gcd x y) (degree (poly_gcd x y)) =
1.65 +    (if x = 0 \<and> y = 0 then 0 else 1)"
1.66 +  by (induct x y rule: poly_gcd.induct)
1.67 +     (simp_all add: poly_gcd.simps nonzero_imp_inverse_nonzero)
1.68 +
1.69 +lemma poly_gcd_zero_iff [simp]:
1.70 +  "poly_gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
1.71 +  by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
1.72 +
1.73 +lemma poly_gcd_0_0 [simp]: "poly_gcd 0 0 = 0"
1.74 +  by simp
1.75 +
1.76 +lemma poly_dvd_antisym:
1.77 +  fixes p q :: "'a::idom poly"
1.78 +  assumes coeff: "coeff p (degree p) = coeff q (degree q)"
1.79 +  assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
1.80 +proof (cases "p = 0")
1.81 +  case True with coeff show "p = q" by simp
1.82 +next
1.83 +  case False with coeff have "q \<noteq> 0" by auto
1.84 +  have degree: "degree p = degree q"
1.85 +    using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0`
1.86 +    by (intro order_antisym dvd_imp_degree_le)
1.87 +
1.88 +  from `p dvd q` obtain a where a: "q = p * a" ..
1.89 +  with `q \<noteq> 0` have "a \<noteq> 0" by auto
1.90 +  with degree a `p \<noteq> 0` have "degree a = 0"
1.91 +    by (simp add: degree_mult_eq)
1.92 +  with coeff a show "p = q"
1.93 +    by (cases a, auto split: if_splits)
1.94 +qed
1.95 +
1.96 +lemma poly_gcd_unique:
1.97 +  assumes dvd1: "d dvd x" and dvd2: "d dvd y"
1.98 +    and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
1.99 +    and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
1.100 +  shows "poly_gcd x y = d"
1.101 +proof -
1.102 +  have "coeff (poly_gcd x y) (degree (poly_gcd x y)) = coeff d (degree d)"
1.103 +    by (simp_all add: poly_gcd_monic monic)
1.104 +  moreover have "poly_gcd x y dvd d"
1.105 +    using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
1.106 +  moreover have "d dvd poly_gcd x y"
1.107 +    using dvd1 dvd2 by (rule poly_gcd_greatest)
1.108 +  ultimately show ?thesis
1.109 +    by (rule poly_dvd_antisym)
1.110 +qed
1.112 +lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x"
1.113 +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.115 +lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
1.116 +by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
1.118 +lemmas poly_gcd_left_commute =
1.119 +  mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
1.121 +lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
1.123 +lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1"
1.124 +by (rule poly_gcd_unique) simp_all
1.126 +lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1"
1.127 +by (rule poly_gcd_unique) simp_all
1.129 +lemma poly_gcd_minus_left [simp]: "poly_gcd (- x) y = poly_gcd x y"
1.130 +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.132 +lemma poly_gcd_minus_right [simp]: "poly_gcd x (- y) = poly_gcd x y"
1.133 +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
1.136  subsection {* Evaluation of polynomials *}
1.138  definition
1.139 @@ -1472,4 +1594,10 @@
1.140  apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
1.141  done
1.143 +lemma poly_gcd_code [code]:
1.144 +  "poly_gcd x y =
1.145 +    (if y = 0 then smult (inverse (coeff x (degree x))) x
1.146 +              else poly_gcd y (x mod y))"
1.147 +  by (simp add: poly_gcd.simps)
1.149  end