src/HOL/Library/Polynomial_GCD_euclidean.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 62352 35a9e1cbb5b3 permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
```     1 (*  Title:      HOL/Library/Polynomial_GCD_euclidean.thy
```
```     2     Author:     Brian Huffman
```
```     3     Author:     Clemens Ballarin
```
```     4     Author:     Amine Chaieb
```
```     5     Author:     Florian Haftmann
```
```     6 *)
```
```     7
```
```     8 section \<open>GCD and LCM on polynomials over a field\<close>
```
```     9
```
```    10 theory Polynomial_GCD_euclidean
```
```    11 imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
```
```    12 begin
```
```    13
```
```    14 subsection \<open>GCD of polynomials\<close>
```
```    15
```
```    16 instantiation poly :: (field) gcd
```
```    17 begin
```
```    18
```
```    19 function gcd_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
```
```    20 where
```
```    21   "gcd (x::'a poly) 0 = smult (inverse (coeff x (degree x))) x"
```
```    22 | "y \<noteq> 0 \<Longrightarrow> gcd (x::'a poly) y = gcd y (x mod y)"
```
```    23 by auto
```
```    24
```
```    25 termination "gcd :: _ poly \<Rightarrow> _"
```
```    26 by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
```
```    27    (auto dest: degree_mod_less)
```
```    28
```
```    29 declare gcd_poly.simps [simp del]
```
```    30
```
```    31 definition lcm_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
```
```    32 where
```
```    33   "lcm_poly a b = a * b div smult (coeff a (degree a) * coeff b (degree b)) (gcd a b)"
```
```    34
```
```    35 instance ..
```
```    36
```
```    37 end
```
```    38
```
```    39 lemma
```
```    40   fixes x y :: "_ poly"
```
```    41   shows poly_gcd_dvd1 [iff]: "gcd x y dvd x"
```
```    42     and poly_gcd_dvd2 [iff]: "gcd x y dvd y"
```
```    43   apply (induct x y rule: gcd_poly.induct)
```
```    44   apply (simp_all add: gcd_poly.simps)
```
```    45   apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
```
```    46   apply (blast dest: dvd_mod_imp_dvd)
```
```    47   done
```
```    48
```
```    49 lemma poly_gcd_greatest:
```
```    50   fixes k x y :: "_ poly"
```
```    51   shows "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd gcd x y"
```
```    52   by (induct x y rule: gcd_poly.induct)
```
```    53      (simp_all add: gcd_poly.simps dvd_mod dvd_smult)
```
```    54
```
```    55 lemma dvd_poly_gcd_iff [iff]:
```
```    56   fixes k x y :: "_ poly"
```
```    57   shows "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
```
```    58   by (auto intro!: poly_gcd_greatest intro: dvd_trans [of _ "gcd x y"])
```
```    59
```
```    60 lemma poly_gcd_monic:
```
```    61   fixes x y :: "_ poly"
```
```    62   shows "coeff (gcd x y) (degree (gcd x y)) =
```
```    63     (if x = 0 \<and> y = 0 then 0 else 1)"
```
```    64   by (induct x y rule: gcd_poly.induct)
```
```    65      (simp_all add: gcd_poly.simps nonzero_imp_inverse_nonzero)
```
```    66
```
```    67 lemma poly_gcd_zero_iff [simp]:
```
```    68   fixes x y :: "_ poly"
```
```    69   shows "gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
```
```    70   by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
```
```    71
```
```    72 lemma poly_gcd_0_0 [simp]:
```
```    73   "gcd (0::_ poly) 0 = 0"
```
```    74   by simp
```
```    75
```
```    76 lemma poly_dvd_antisym:
```
```    77   fixes p q :: "'a::idom poly"
```
```    78   assumes coeff: "coeff p (degree p) = coeff q (degree q)"
```
```    79   assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
```
```    80 proof (cases "p = 0")
```
```    81   case True with coeff show "p = q" by simp
```
```    82 next
```
```    83   case False with coeff have "q \<noteq> 0" by auto
```
```    84   have degree: "degree p = degree q"
```
```    85     using \<open>p dvd q\<close> \<open>q dvd p\<close> \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close>
```
```    86     by (intro order_antisym dvd_imp_degree_le)
```
```    87
```
```    88   from \<open>p dvd q\<close> obtain a where a: "q = p * a" ..
```
```    89   with \<open>q \<noteq> 0\<close> have "a \<noteq> 0" by auto
```
```    90   with degree a \<open>p \<noteq> 0\<close> have "degree a = 0"
```
```    91     by (simp add: degree_mult_eq)
```
```    92   with coeff a show "p = q"
```
```    93     by (cases a, auto split: if_splits)
```
```    94 qed
```
```    95
```
```    96 lemma poly_gcd_unique:
```
```    97   fixes d x y :: "_ poly"
```
```    98   assumes dvd1: "d dvd x" and dvd2: "d dvd y"
```
```    99     and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
```
```   100     and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
```
```   101   shows "gcd x y = d"
```
```   102 proof -
```
```   103   have "coeff (gcd x y) (degree (gcd x y)) = coeff d (degree d)"
```
```   104     by (simp_all add: poly_gcd_monic monic)
```
```   105   moreover have "gcd x y dvd d"
```
```   106     using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
```
```   107   moreover have "d dvd gcd x y"
```
```   108     using dvd1 dvd2 by (rule poly_gcd_greatest)
```
```   109   ultimately show ?thesis
```
```   110     by (rule poly_dvd_antisym)
```
```   111 qed
```
```   112
```
```   113 instance poly :: (field) semiring_gcd
```
```   114 proof
```
```   115   fix p q :: "'a::field poly"
```
```   116   show "normalize (gcd p q) = gcd p q"
```
```   117     by (induct p q rule: gcd_poly.induct)
```
```   118       (simp_all add: gcd_poly.simps normalize_poly_def)
```
```   119   show "lcm p q = normalize (p * q) div gcd p q"
```
```   120     by (simp add: coeff_degree_mult div_smult_left div_smult_right lcm_poly_def normalize_poly_def)
```
```   121       (metis (no_types, lifting) div_smult_right inverse_mult_distrib inverse_zero mult.commute pdivmod_rel pdivmod_rel_def smult_eq_0_iff)
```
```   122 qed simp_all
```
```   123
```
```   124 lemma poly_gcd_1_left [simp]: "gcd 1 y = (1 :: _ poly)"
```
```   125 by (rule poly_gcd_unique) simp_all
```
```   126
```
```   127 lemma poly_gcd_1_right [simp]: "gcd x 1 = (1 :: _ poly)"
```
```   128 by (rule poly_gcd_unique) simp_all
```
```   129
```
```   130 lemma poly_gcd_minus_left [simp]: "gcd (- x) y = gcd x (y :: _ poly)"
```
```   131 by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
```
```   132
```
```   133 lemma poly_gcd_minus_right [simp]: "gcd x (- y) = gcd x (y :: _ poly)"
```
```   134 by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
```
```   135
```
```   136 lemma poly_gcd_code [code]:
```
```   137   "gcd x y = (if y = 0 then normalize x else gcd y (x mod (y :: _ poly)))"
```
```   138   by (simp add: gcd_poly.simps)
```
```   139
```
```   140 end
```