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