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.6  
     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.28  
    1.29 @@ -1102,6 +1121,109 @@
    1.30  done
    1.31  
    1.32  
    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.111 +
   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.114 +
   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.117 +
   1.118 +lemmas poly_gcd_left_commute =
   1.119 +  mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
   1.120 +
   1.121 +lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
   1.122 +
   1.123 +lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1"
   1.124 +by (rule poly_gcd_unique) simp_all
   1.125 +
   1.126 +lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1"
   1.127 +by (rule poly_gcd_unique) simp_all
   1.128 +
   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.131 +
   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.134 +
   1.135 +
   1.136  subsection {* Evaluation of polynomials *}
   1.137  
   1.138  definition
   1.139 @@ -1472,4 +1594,10 @@
   1.140  apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
   1.141  done
   1.142  
   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.148 +
   1.149  end