src/HOL/Library/Polynomial_GCD_euclidean.thy
author paulson <lp15@cam.ac.uk>
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