src/HOL/Computational_Algebra/Polynomial_Factorial.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 66840 0d689d71dbdc
child 67051 e7e54a0b9197
permissions -rw-r--r--
proper merge (amending fb46c031c841);
wenzelm@65435
     1
(*  Title:      HOL/Computational_Algebra/Polynomial_Factorial.thy
wenzelm@63764
     2
    Author:     Manuel Eberl
wenzelm@63764
     3
*)
wenzelm@63764
     4
haftmann@66805
     5
section \<open>Polynomials, fractions and rings\<close>
haftmann@66805
     6
eberlm@63498
     7
theory Polynomial_Factorial
eberlm@63498
     8
imports 
eberlm@63498
     9
  Complex_Main
wenzelm@65366
    10
  Polynomial
wenzelm@65366
    11
  Normalized_Fraction
eberlm@63498
    12
begin
eberlm@63498
    13
eberlm@63498
    14
subsection \<open>Lifting elements into the field of fractions\<close>
eberlm@63498
    15
haftmann@66805
    16
definition to_fract :: "'a :: idom \<Rightarrow> 'a fract"
haftmann@66805
    17
  where "to_fract x = Fract x 1"
haftmann@66808
    18
  \<comment> \<open>FIXME: more idiomatic name, abbreviation\<close>
eberlm@63498
    19
eberlm@63498
    20
lemma to_fract_0 [simp]: "to_fract 0 = 0"
eberlm@63498
    21
  by (simp add: to_fract_def eq_fract Zero_fract_def)
eberlm@63498
    22
eberlm@63498
    23
lemma to_fract_1 [simp]: "to_fract 1 = 1"
eberlm@63498
    24
  by (simp add: to_fract_def eq_fract One_fract_def)
eberlm@63498
    25
eberlm@63498
    26
lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y"
eberlm@63498
    27
  by (simp add: to_fract_def)
eberlm@63498
    28
eberlm@63498
    29
lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y"
eberlm@63498
    30
  by (simp add: to_fract_def)
eberlm@63498
    31
  
eberlm@63498
    32
lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x"
eberlm@63498
    33
  by (simp add: to_fract_def)
eberlm@63498
    34
  
eberlm@63498
    35
lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y"
eberlm@63498
    36
  by (simp add: to_fract_def)
eberlm@63498
    37
eberlm@63498
    38
lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \<longleftrightarrow> x = y"
eberlm@63498
    39
  by (simp add: to_fract_def eq_fract)
eberlm@63498
    40
  
eberlm@63498
    41
lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \<longleftrightarrow> x = 0"
eberlm@63498
    42
  by (simp add: to_fract_def Zero_fract_def eq_fract)
eberlm@63498
    43
eberlm@63498
    44
lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0"
eberlm@63498
    45
  by transfer simp
eberlm@63498
    46
eberlm@63498
    47
lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x"
eberlm@63498
    48
  by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp)
eberlm@63498
    49
eberlm@63498
    50
lemma to_fract_quot_of_fract:
eberlm@63498
    51
  assumes "snd (quot_of_fract x) = 1"
eberlm@63498
    52
  shows   "to_fract (fst (quot_of_fract x)) = x"
eberlm@63498
    53
proof -
eberlm@63498
    54
  have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp
eberlm@63498
    55
  also note assms
eberlm@63498
    56
  finally show ?thesis by (simp add: to_fract_def)
eberlm@63498
    57
qed
eberlm@63498
    58
eberlm@63498
    59
lemma snd_quot_of_fract_Fract_whole:
eberlm@63498
    60
  assumes "y dvd x"
eberlm@63498
    61
  shows   "snd (quot_of_fract (Fract x y)) = 1"
eberlm@63498
    62
  using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd)
eberlm@63498
    63
  
eberlm@63498
    64
lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b"
eberlm@63498
    65
  by (simp add: to_fract_def)
eberlm@63498
    66
eberlm@63498
    67
lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)"
eberlm@63498
    68
  unfolding to_fract_def by transfer (simp add: normalize_quot_def)
eberlm@63498
    69
eberlm@63498
    70
lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0"
eberlm@63498
    71
  by transfer simp
eberlm@63498
    72
 
eberlm@63498
    73
lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1"
eberlm@63498
    74
  unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all
eberlm@63498
    75
eberlm@63498
    76
lemma coprime_quot_of_fract:
eberlm@63498
    77
  "coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))"
eberlm@63498
    78
  by transfer (simp add: coprime_normalize_quot)
eberlm@63498
    79
eberlm@63498
    80
lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1"
eberlm@63498
    81
  using quot_of_fract_in_normalized_fracts[of x] 
eberlm@63498
    82
  by (simp add: normalized_fracts_def case_prod_unfold)  
eberlm@63498
    83
eberlm@63498
    84
lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x"
eberlm@63498
    85
  by (subst (2) normalize_mult_unit_factor [symmetric, of x])
eberlm@63498
    86
     (simp del: normalize_mult_unit_factor)
eberlm@63498
    87
  
eberlm@63498
    88
lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
eberlm@63498
    89
  by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
eberlm@63498
    90
eberlm@63498
    91
eberlm@63498
    92
subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
eberlm@63498
    93
eberlm@63498
    94
abbreviation (input) fract_poly 
eberlm@63498
    95
  where "fract_poly \<equiv> map_poly to_fract"
eberlm@63498
    96
eberlm@63498
    97
abbreviation (input) unfract_poly 
eberlm@63498
    98
  where "unfract_poly \<equiv> map_poly (fst \<circ> quot_of_fract)"
eberlm@63498
    99
  
eberlm@63498
   100
lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)"
eberlm@63498
   101
  by (simp add: smult_conv_map_poly map_poly_map_poly o_def)
eberlm@63498
   102
eberlm@63498
   103
lemma fract_poly_0 [simp]: "fract_poly 0 = 0"
eberlm@63498
   104
  by (simp add: poly_eqI coeff_map_poly)
eberlm@63498
   105
eberlm@63498
   106
lemma fract_poly_1 [simp]: "fract_poly 1 = 1"
haftmann@65486
   107
  by (simp add: map_poly_pCons)
eberlm@63498
   108
eberlm@63498
   109
lemma fract_poly_add [simp]:
eberlm@63498
   110
  "fract_poly (p + q) = fract_poly p + fract_poly q"
eberlm@63498
   111
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
eberlm@63498
   112
eberlm@63498
   113
lemma fract_poly_diff [simp]:
eberlm@63498
   114
  "fract_poly (p - q) = fract_poly p - fract_poly q"
eberlm@63498
   115
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
eberlm@63498
   116
nipkow@64267
   117
lemma to_fract_sum [simp]: "to_fract (sum f A) = sum (\<lambda>x. to_fract (f x)) A"
eberlm@63498
   118
  by (cases "finite A", induction A rule: finite_induct) simp_all 
eberlm@63498
   119
eberlm@63498
   120
lemma fract_poly_mult [simp]:
eberlm@63498
   121
  "fract_poly (p * q) = fract_poly p * fract_poly q"
eberlm@63498
   122
  by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult)
eberlm@63498
   123
eberlm@63498
   124
lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \<longleftrightarrow> p = q"
eberlm@63498
   125
  by (auto simp: poly_eq_iff coeff_map_poly)
eberlm@63498
   126
eberlm@63498
   127
lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \<longleftrightarrow> p = 0"
eberlm@63498
   128
  using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff)
eberlm@63498
   129
eberlm@63498
   130
lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
eberlm@63498
   131
  by (auto elim!: dvdE)
eberlm@63498
   132
nipkow@63830
   133
lemma prod_mset_fract_poly: 
haftmann@65390
   134
  "(\<Prod>x\<in>#A. map_poly to_fract (f x)) = fract_poly (prod_mset (image_mset f A))"
haftmann@65390
   135
  by (induct A) (simp_all add: ac_simps)
eberlm@63498
   136
  
eberlm@63498
   137
lemma is_unit_fract_poly_iff:
eberlm@63498
   138
  "p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
eberlm@63498
   139
proof safe
eberlm@63498
   140
  assume A: "p dvd 1"
haftmann@65389
   141
  with fract_poly_dvd [of p 1] show "is_unit (fract_poly p)"
haftmann@65389
   142
    by simp
eberlm@63498
   143
  from A show "content p = 1"
eberlm@63498
   144
    by (auto simp: is_unit_poly_iff normalize_1_iff)
eberlm@63498
   145
next
eberlm@63498
   146
  assume A: "fract_poly p dvd 1" and B: "content p = 1"
eberlm@63498
   147
  from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)
eberlm@63498
   148
  {
eberlm@63498
   149
    fix n :: nat assume "n > 0"
eberlm@63498
   150
    have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly)
eberlm@63498
   151
    also note c
eberlm@63498
   152
    also from \<open>n > 0\<close> have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits)
eberlm@63498
   153
    finally have "coeff p n = 0" by simp
eberlm@63498
   154
  }
eberlm@63498
   155
  hence "degree p \<le> 0" by (intro degree_le) simp_all
eberlm@63498
   156
  with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE)
eberlm@63498
   157
qed
eberlm@63498
   158
  
eberlm@63498
   159
lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1"
eberlm@63498
   160
  using fract_poly_dvd[of p 1] by simp
eberlm@63498
   161
eberlm@63498
   162
lemma fract_poly_smult_eqE:
eberlm@63498
   163
  fixes c :: "'a :: {idom_divide,ring_gcd} fract"
eberlm@63498
   164
  assumes "fract_poly p = smult c (fract_poly q)"
eberlm@63498
   165
  obtains a b 
eberlm@63498
   166
    where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a"
eberlm@63498
   167
proof -
eberlm@63498
   168
  define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)"
eberlm@63498
   169
  have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)"
eberlm@63498
   170
    by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms)
eberlm@63498
   171
  hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
eberlm@63498
   172
  hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
eberlm@63498
   173
  moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
eberlm@63498
   174
    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
eberlm@63498
   175
          normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
eberlm@63498
   176
  ultimately show ?thesis by (intro that[of a b])
eberlm@63498
   177
qed
eberlm@63498
   178
eberlm@63498
   179
eberlm@63498
   180
subsection \<open>Fractional content\<close>
eberlm@63498
   181
eberlm@63498
   182
abbreviation (input) Lcm_coeff_denoms 
eberlm@63498
   183
    :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a"
eberlm@63498
   184
  where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))"
eberlm@63498
   185
  
eberlm@63498
   186
definition fract_content :: 
eberlm@63498
   187
      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where
eberlm@63498
   188
  "fract_content p = 
eberlm@63498
   189
     (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" 
eberlm@63498
   190
eberlm@63498
   191
definition primitive_part_fract :: 
eberlm@63498
   192
      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where
eberlm@63498
   193
  "primitive_part_fract p = 
eberlm@63498
   194
     primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
eberlm@63498
   195
eberlm@63498
   196
lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0"
eberlm@63498
   197
  by (simp add: primitive_part_fract_def)
eberlm@63498
   198
eberlm@63498
   199
lemma fract_content_eq_0_iff [simp]:
eberlm@63498
   200
  "fract_content p = 0 \<longleftrightarrow> p = 0"
eberlm@63498
   201
  unfolding fract_content_def Let_def Zero_fract_def
eberlm@63498
   202
  by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff)
eberlm@63498
   203
eberlm@63498
   204
lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
eberlm@63498
   205
  unfolding primitive_part_fract_def
eberlm@63498
   206
  by (rule content_primitive_part)
eberlm@63498
   207
     (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)  
eberlm@63498
   208
eberlm@63498
   209
lemma content_times_primitive_part_fract:
eberlm@63498
   210
  "smult (fract_content p) (fract_poly (primitive_part_fract p)) = p"
eberlm@63498
   211
proof -
eberlm@63498
   212
  define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)"
eberlm@63498
   213
  have "fract_poly p' = 
eberlm@63498
   214
          map_poly (to_fract \<circ> fst \<circ> quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)"
eberlm@63498
   215
    unfolding primitive_part_fract_def p'_def 
eberlm@63498
   216
    by (subst map_poly_map_poly) (simp_all add: o_assoc)
eberlm@63498
   217
  also have "\<dots> = smult (to_fract (Lcm_coeff_denoms p)) p"
eberlm@63498
   218
  proof (intro map_poly_idI, unfold o_apply)
eberlm@63498
   219
    fix c assume "c \<in> set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))"
eberlm@63498
   220
    then obtain c' where c: "c' \<in> set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'"
eberlm@63498
   221
      by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits)
eberlm@63498
   222
    note c(2)
eberlm@63498
   223
    also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))"
eberlm@63498
   224
      by simp
eberlm@63498
   225
    also have "to_fract (Lcm_coeff_denoms p) * \<dots> = 
eberlm@63498
   226
                 Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))"
eberlm@63498
   227
      unfolding to_fract_def by (subst mult_fract) simp_all
eberlm@63498
   228
    also have "snd (quot_of_fract \<dots>) = 1"
eberlm@63498
   229
      by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto)
eberlm@63498
   230
    finally show "to_fract (fst (quot_of_fract c)) = c"
eberlm@63498
   231
      by (rule to_fract_quot_of_fract)
eberlm@63498
   232
  qed
eberlm@63498
   233
  also have "p' = smult (content p') (primitive_part p')" 
eberlm@63498
   234
    by (rule content_times_primitive_part [symmetric])
eberlm@63498
   235
  also have "primitive_part p' = primitive_part_fract p"
eberlm@63498
   236
    by (simp add: primitive_part_fract_def p'_def)
eberlm@63498
   237
  also have "fract_poly (smult (content p') (primitive_part_fract p)) = 
eberlm@63498
   238
               smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp
eberlm@63498
   239
  finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) =
eberlm@63498
   240
                      smult (to_fract (Lcm_coeff_denoms p)) p" .
eberlm@63498
   241
  thus ?thesis
eberlm@63498
   242
    by (subst (asm) smult_eq_iff)
eberlm@63498
   243
       (auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def)
eberlm@63498
   244
qed
eberlm@63498
   245
eberlm@63498
   246
lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
eberlm@63498
   247
proof -
eberlm@63498
   248
  have "Lcm_coeff_denoms (fract_poly p) = 1"
haftmann@63905
   249
    by (auto simp: set_coeffs_map_poly)
eberlm@63498
   250
  hence "fract_content (fract_poly p) = 
eberlm@63498
   251
           to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
eberlm@63498
   252
    by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
eberlm@63498
   253
  also have "map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p = p"
eberlm@63498
   254
    by (intro map_poly_idI) simp_all
eberlm@63498
   255
  finally show ?thesis .
eberlm@63498
   256
qed
eberlm@63498
   257
eberlm@63498
   258
lemma content_decompose_fract:
eberlm@63498
   259
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
eberlm@63498
   260
  obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
eberlm@63498
   261
proof (cases "p = 0")
eberlm@63498
   262
  case True
eberlm@63498
   263
  hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all
eberlm@63498
   264
  thus ?thesis ..
eberlm@63498
   265
next
eberlm@63498
   266
  case False
eberlm@63498
   267
  thus ?thesis
eberlm@63498
   268
    by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract])
eberlm@63498
   269
qed
eberlm@63498
   270
eberlm@63498
   271
eberlm@63498
   272
subsection \<open>More properties of content and primitive part\<close>
eberlm@63498
   273
eberlm@63498
   274
lemma lift_prime_elem_poly:
eberlm@63633
   275
  assumes "prime_elem (c :: 'a :: semidom)"
eberlm@63633
   276
  shows   "prime_elem [:c:]"
eberlm@63633
   277
proof (rule prime_elemI)
eberlm@63498
   278
  fix a b assume *: "[:c:] dvd a * b"
eberlm@63498
   279
  from * have dvd: "c dvd coeff (a * b) n" for n
eberlm@63498
   280
    by (subst (asm) const_poly_dvd_iff) blast
eberlm@63498
   281
  {
eberlm@63498
   282
    define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
eberlm@63498
   283
    assume "\<not>[:c:] dvd b"
eberlm@63498
   284
    hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
nipkow@65963
   285
    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b"
nipkow@65963
   286
      by (auto intro: le_degree)
nipkow@65965
   287
    have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B])
eberlm@63498
   288
    have "i \<le> m" if "\<not>c dvd coeff b i" for i
nipkow@65965
   289
      unfolding m_def by (rule Greatest_le_nat[OF that B])
eberlm@63498
   290
    hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
eberlm@63498
   291
eberlm@63498
   292
    have "c dvd coeff a i" for i
eberlm@63498
   293
    proof (induction i rule: nat_descend_induct[of "degree a"])
eberlm@63498
   294
      case (base i)
eberlm@63498
   295
      thus ?case by (simp add: coeff_eq_0)
eberlm@63498
   296
    next
eberlm@63498
   297
      case (descend i)
eberlm@63498
   298
      let ?A = "{..i+m} - {i}"
eberlm@63498
   299
      have "c dvd coeff (a * b) (i + m)" by (rule dvd)
eberlm@63498
   300
      also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
eberlm@63498
   301
        by (simp add: coeff_mult)
eberlm@63498
   302
      also have "{..i+m} = insert i ?A" by auto
eberlm@63498
   303
      also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
eberlm@63498
   304
                   coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
eberlm@63498
   305
        (is "_ = _ + ?S")
nipkow@64267
   306
        by (subst sum.insert) simp_all
eberlm@63498
   307
      finally have eq: "c dvd coeff a i * coeff b m + ?S" .
eberlm@63498
   308
      moreover have "c dvd ?S"
nipkow@64267
   309
      proof (rule dvd_sum)
eberlm@63498
   310
        fix k assume k: "k \<in> {..i+m} - {i}"
eberlm@63498
   311
        show "c dvd coeff a k * coeff b (i + m - k)"
eberlm@63498
   312
        proof (cases "k < i")
eberlm@63498
   313
          case False
eberlm@63498
   314
          with k have "c dvd coeff a k" by (intro descend.IH) simp
eberlm@63498
   315
          thus ?thesis by simp
eberlm@63498
   316
        next
eberlm@63498
   317
          case True
eberlm@63498
   318
          hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
eberlm@63498
   319
          thus ?thesis by simp
eberlm@63498
   320
        qed
eberlm@63498
   321
      qed
eberlm@63498
   322
      ultimately have "c dvd coeff a i * coeff b m"
eberlm@63498
   323
        by (simp add: dvd_add_left_iff)
eberlm@63498
   324
      with assms coeff_m show "c dvd coeff a i"
eberlm@63633
   325
        by (simp add: prime_elem_dvd_mult_iff)
eberlm@63498
   326
    qed
eberlm@63498
   327
    hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
eberlm@63498
   328
  }
haftmann@65486
   329
  then show "[:c:] dvd a \<or> [:c:] dvd b" by blast
haftmann@65486
   330
next
haftmann@65486
   331
  from assms show "[:c:] \<noteq> 0" and "\<not> [:c:] dvd 1"
haftmann@65486
   332
    by (simp_all add: prime_elem_def is_unit_const_poly_iff)
haftmann@65486
   333
qed
eberlm@63498
   334
eberlm@63498
   335
lemma prime_elem_const_poly_iff:
eberlm@63498
   336
  fixes c :: "'a :: semidom"
eberlm@63633
   337
  shows   "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
eberlm@63498
   338
proof
eberlm@63633
   339
  assume A: "prime_elem [:c:]"
eberlm@63633
   340
  show "prime_elem c"
eberlm@63633
   341
  proof (rule prime_elemI)
eberlm@63498
   342
    fix a b assume "c dvd a * b"
eberlm@63498
   343
    hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
eberlm@63633
   344
    from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD)
eberlm@63498
   345
    thus "c dvd a \<or> c dvd b" by simp
eberlm@63633
   346
  qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
eberlm@63498
   347
qed (auto intro: lift_prime_elem_poly)
eberlm@63498
   348
eberlm@63498
   349
context
eberlm@63498
   350
begin
eberlm@63498
   351
eberlm@63498
   352
private lemma content_1_mult:
eberlm@63498
   353
  fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly"
eberlm@63498
   354
  assumes "content f = 1" "content g = 1"
eberlm@63498
   355
  shows   "content (f * g) = 1"
eberlm@63498
   356
proof (cases "f * g = 0")
eberlm@63498
   357
  case False
eberlm@63498
   358
  from assms have "f \<noteq> 0" "g \<noteq> 0" by auto
eberlm@63498
   359
eberlm@63498
   360
  hence "f * g \<noteq> 0" by auto
eberlm@63498
   361
  {
eberlm@63498
   362
    assume "\<not>is_unit (content (f * g))"
eberlm@63633
   363
    with False have "\<exists>p. p dvd content (f * g) \<and> prime p"
eberlm@63498
   364
      by (intro prime_divisor_exists) simp_all
eberlm@63633
   365
    then obtain p where "p dvd content (f * g)" "prime p" by blast
eberlm@63498
   366
    from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
eberlm@63498
   367
      by (simp add: const_poly_dvd_iff_dvd_content)
eberlm@63633
   368
    moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
eberlm@63498
   369
    ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
eberlm@63633
   370
      by (simp add: prime_elem_dvd_mult_iff)
eberlm@63498
   371
    with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
eberlm@63633
   372
    with \<open>prime p\<close> have False by simp
eberlm@63498
   373
  }
eberlm@63498
   374
  hence "is_unit (content (f * g))" by blast
eberlm@63498
   375
  hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
eberlm@63498
   376
  thus ?thesis by simp
eberlm@63498
   377
qed (insert assms, auto)
eberlm@63498
   378
eberlm@63498
   379
lemma content_mult:
eberlm@63498
   380
  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
eberlm@63498
   381
  shows "content (p * q) = content p * content q"
eberlm@63498
   382
proof -
eberlm@63498
   383
  from content_decompose[of p] guess p' . note p = this
eberlm@63498
   384
  from content_decompose[of q] guess q' . note q = this
eberlm@63498
   385
  have "content (p * q) = content p * content q * content (p' * q')"
eberlm@63498
   386
    by (subst p, subst q) (simp add: mult_ac normalize_mult)
eberlm@63498
   387
  also from p q have "content (p' * q') = 1" by (intro content_1_mult)
eberlm@63498
   388
  finally show ?thesis by simp
eberlm@63498
   389
qed
eberlm@63498
   390
eberlm@63498
   391
lemma fract_poly_dvdD:
eberlm@63498
   392
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
   393
  assumes "fract_poly p dvd fract_poly q" "content p = 1"
eberlm@63498
   394
  shows   "p dvd q"
eberlm@63498
   395
proof -
eberlm@63498
   396
  from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
eberlm@63498
   397
  from content_decompose_fract[of r] guess c r' . note r' = this
eberlm@63498
   398
  from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp  
eberlm@63498
   399
  from fract_poly_smult_eqE[OF this] guess a b . note ab = this
eberlm@63498
   400
  have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
eberlm@63498
   401
  hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
eberlm@63498
   402
  have "1 = gcd a (normalize b)" by (simp add: ab)
eberlm@63498
   403
  also note eq'
eberlm@63498
   404
  also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4))
eberlm@63498
   405
  finally have [simp]: "a = 1" by simp
eberlm@63498
   406
  from eq ab have "q = p * ([:b:] * r')" by simp
eberlm@63498
   407
  thus ?thesis by (rule dvdI)
eberlm@63498
   408
qed
eberlm@63498
   409
eberlm@63498
   410
end
eberlm@63498
   411
eberlm@63498
   412
eberlm@63498
   413
subsection \<open>Polynomials over a field are a Euclidean ring\<close>
eberlm@63498
   414
haftmann@66805
   415
context
haftmann@66805
   416
begin
eberlm@63498
   417
eberlm@63498
   418
interpretation field_poly: 
haftmann@66817
   419
  normalization_euclidean_semiring where zero = "0 :: 'a :: field poly"
haftmann@66817
   420
    and one = 1 and plus = plus and minus = minus
haftmann@64164
   421
    and times = times
haftmann@66805
   422
    and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p"
haftmann@66805
   423
    and unit_factor = "\<lambda>p. [:lead_coeff p:]"
haftmann@66805
   424
    and euclidean_size = "\<lambda>p. if p = 0 then 0 else 2 ^ degree p"
haftmann@64164
   425
    and divide = divide and modulo = modulo
haftmann@66805
   426
  rewrites "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
haftmann@66805
   427
    and "comm_monoid_mult.prod_mset times 1 = prod_mset"
haftmann@66805
   428
    and "comm_semiring_1.irreducible times 1 0 = irreducible"
haftmann@66805
   429
    and "comm_semiring_1.prime_elem times 1 0 = prime_elem"
haftmann@66805
   430
proof -
haftmann@66805
   431
  show "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
haftmann@66805
   432
    by (simp add: dvd_dict)
haftmann@66805
   433
  show "comm_monoid_mult.prod_mset times 1 = prod_mset"
haftmann@66805
   434
    by (simp add: prod_mset_dict)
haftmann@66805
   435
  show "comm_semiring_1.irreducible times 1 0 = irreducible"
haftmann@66805
   436
    by (simp add: irreducible_dict)
haftmann@66805
   437
  show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
haftmann@66805
   438
    by (simp add: prime_elem_dict)
haftmann@66817
   439
  show "class.normalization_euclidean_semiring divide plus minus (0 :: 'a poly) times 1
haftmann@66817
   440
    modulo (\<lambda>p. if p = 0 then 0 else 2 ^ degree p)
haftmann@66817
   441
    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)"
haftmann@66805
   442
  proof (standard, fold dvd_dict)
haftmann@66805
   443
    fix p :: "'a poly"
haftmann@66805
   444
    show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p"
haftmann@66805
   445
      by (cases "p = 0") simp_all
haftmann@66805
   446
  next
haftmann@66805
   447
    fix p :: "'a poly" assume "is_unit p"
haftmann@66805
   448
    then show "[:lead_coeff p:] = p"
haftmann@66805
   449
      by (elim is_unit_polyE) (auto simp: monom_0 one_poly_def field_simps)
haftmann@66805
   450
  next
haftmann@66805
   451
    fix p :: "'a poly" assume "p \<noteq> 0"
haftmann@66805
   452
    then show "is_unit [:lead_coeff p:]"
haftmann@66805
   453
      by (simp add: is_unit_pCons_iff)
haftmann@66805
   454
  qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
haftmann@66805
   455
qed
eberlm@63498
   456
eberlm@63722
   457
lemma field_poly_irreducible_imp_prime:
haftmann@66805
   458
  "prime_elem p" if "irreducible p" for p :: "'a :: field poly"
haftmann@66805
   459
  using that by (fact field_poly.irreducible_imp_prime_elem)
eberlm@63498
   460
nipkow@63830
   461
lemma field_poly_prod_mset_prime_factorization:
haftmann@66805
   462
  "prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p"
haftmann@66805
   463
  if "p \<noteq> 0" for p :: "'a :: field poly"
haftmann@66805
   464
  using that by (fact field_poly.prod_mset_prime_factorization)
eberlm@63498
   465
eberlm@63722
   466
lemma field_poly_in_prime_factorization_imp_prime:
haftmann@66805
   467
  "prime_elem p" if "p \<in># field_poly.prime_factorization x"
haftmann@66805
   468
  for p :: "'a :: field poly"
haftmann@66805
   469
  by (rule field_poly.prime_imp_prime_elem, rule field_poly.in_prime_factors_imp_prime)
haftmann@66805
   470
    (fact that)
eberlm@63498
   471
eberlm@63498
   472
eberlm@63498
   473
subsection \<open>Primality and irreducibility in polynomial rings\<close>
eberlm@63498
   474
eberlm@63498
   475
lemma nonconst_poly_irreducible_iff:
eberlm@63498
   476
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
   477
  assumes "degree p \<noteq> 0"
eberlm@63498
   478
  shows   "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
eberlm@63498
   479
proof safe
eberlm@63498
   480
  assume p: "irreducible p"
eberlm@63498
   481
eberlm@63498
   482
  from content_decompose[of p] guess p' . note p' = this
eberlm@63498
   483
  hence "p = [:content p:] * p'" by simp
eberlm@63498
   484
  from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
eberlm@63498
   485
  moreover have "\<not>p' dvd 1"
eberlm@63498
   486
  proof
eberlm@63498
   487
    assume "p' dvd 1"
eberlm@63498
   488
    hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff)
eberlm@63498
   489
    with assms show False by contradiction
eberlm@63498
   490
  qed
eberlm@63498
   491
  ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff)
eberlm@63498
   492
  
eberlm@63498
   493
  show "irreducible (map_poly to_fract p)"
eberlm@63498
   494
  proof (rule irreducibleI)
eberlm@63498
   495
    have "fract_poly p = 0 \<longleftrightarrow> p = 0" by (intro map_poly_eq_0_iff) auto
eberlm@63498
   496
    with assms show "map_poly to_fract p \<noteq> 0" by auto
eberlm@63498
   497
  next
eberlm@63498
   498
    show "\<not>is_unit (fract_poly p)"
eberlm@63498
   499
    proof
eberlm@63498
   500
      assume "is_unit (map_poly to_fract p)"
eberlm@63498
   501
      hence "degree (map_poly to_fract p) = 0"
eberlm@63498
   502
        by (auto simp: is_unit_poly_iff)
eberlm@63498
   503
      hence "degree p = 0" by (simp add: degree_map_poly)
eberlm@63498
   504
      with assms show False by contradiction
eberlm@63498
   505
   qed
eberlm@63498
   506
 next
eberlm@63498
   507
   fix q r assume qr: "fract_poly p = q * r"
eberlm@63498
   508
   from content_decompose_fract[of q] guess cg q' . note q = this
eberlm@63498
   509
   from content_decompose_fract[of r] guess cr r' . note r = this
eberlm@63498
   510
   from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
eberlm@63498
   511
   from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
eberlm@63498
   512
     by (simp add: q r)
eberlm@63498
   513
   from fract_poly_smult_eqE[OF this] guess a b . note ab = this
eberlm@63498
   514
   hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
eberlm@63498
   515
   with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
eberlm@63498
   516
   hence "normalize b = gcd a b" by simp
eberlm@63498
   517
   also from ab(3) have "\<dots> = 1" .
eberlm@63498
   518
   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
eberlm@63498
   519
   
eberlm@63498
   520
   note eq
eberlm@63498
   521
   also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
eberlm@63498
   522
   also have "smult \<dots> (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp
eberlm@63498
   523
   finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult)
eberlm@63498
   524
   from p and this have "([:b:] * q') dvd 1 \<or> r' dvd 1" by (rule irreducibleD)
eberlm@63498
   525
   hence "q' dvd 1 \<or> r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left)
eberlm@63498
   526
   hence "fract_poly q' dvd 1 \<or> fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit)
eberlm@63498
   527
   with q r show "is_unit q \<or> is_unit r"
eberlm@63498
   528
     by (auto simp add: is_unit_smult_iff dvd_field_iff nz)
eberlm@63498
   529
 qed
eberlm@63498
   530
eberlm@63498
   531
next
eberlm@63498
   532
eberlm@63498
   533
  assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
eberlm@63498
   534
  show "irreducible p"
eberlm@63498
   535
  proof (rule irreducibleI)
eberlm@63498
   536
    from irred show "p \<noteq> 0" by auto
eberlm@63498
   537
  next
eberlm@63498
   538
    from irred show "\<not>p dvd 1"
eberlm@63498
   539
      by (auto simp: irreducible_def dest: fract_poly_is_unit)
eberlm@63498
   540
  next
eberlm@63498
   541
    fix q r assume qr: "p = q * r"
eberlm@63498
   542
    hence "fract_poly p = fract_poly q * fract_poly r" by simp
eberlm@63498
   543
    from irred and this have "fract_poly q dvd 1 \<or> fract_poly r dvd 1" 
eberlm@63498
   544
      by (rule irreducibleD)
eberlm@63498
   545
    with primitive qr show "q dvd 1 \<or> r dvd 1"
eberlm@63498
   546
      by (auto simp:  content_prod_eq_1_iff is_unit_fract_poly_iff)
eberlm@63498
   547
  qed
eberlm@63498
   548
qed
eberlm@63498
   549
eberlm@63498
   550
private lemma irreducible_imp_prime_poly:
eberlm@63498
   551
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
   552
  assumes "irreducible p"
eberlm@63633
   553
  shows   "prime_elem p"
eberlm@63498
   554
proof (cases "degree p = 0")
eberlm@63498
   555
  case True
eberlm@63498
   556
  with assms show ?thesis
eberlm@63498
   557
    by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
eberlm@63633
   558
             intro!: irreducible_imp_prime_elem elim!: degree_eq_zeroE)
eberlm@63498
   559
next
eberlm@63498
   560
  case False
eberlm@63498
   561
  from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
eberlm@63498
   562
    by (simp_all add: nonconst_poly_irreducible_iff)
eberlm@63633
   563
  from irred have prime: "prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
eberlm@63498
   564
  show ?thesis
eberlm@63633
   565
  proof (rule prime_elemI)
eberlm@63498
   566
    fix q r assume "p dvd q * r"
eberlm@63498
   567
    hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
eberlm@63498
   568
    hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
eberlm@63498
   569
    from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
eberlm@63633
   570
      by (rule prime_elem_dvd_multD)
eberlm@63498
   571
    with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
eberlm@63498
   572
  qed (insert assms, auto simp: irreducible_def)
eberlm@63498
   573
qed
eberlm@63498
   574
eberlm@63498
   575
lemma degree_primitive_part_fract [simp]:
eberlm@63498
   576
  "degree (primitive_part_fract p) = degree p"
eberlm@63498
   577
proof -
eberlm@63498
   578
  have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))"
eberlm@63498
   579
    by (simp add: content_times_primitive_part_fract)
eberlm@63498
   580
  also have "degree \<dots> = degree (primitive_part_fract p)"
eberlm@63498
   581
    by (auto simp: degree_map_poly)
eberlm@63498
   582
  finally show ?thesis ..
eberlm@63498
   583
qed
eberlm@63498
   584
eberlm@63498
   585
lemma irreducible_primitive_part_fract:
eberlm@63498
   586
  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
eberlm@63498
   587
  assumes "irreducible p"
eberlm@63498
   588
  shows   "irreducible (primitive_part_fract p)"
eberlm@63498
   589
proof -
eberlm@63498
   590
  from assms have deg: "degree (primitive_part_fract p) \<noteq> 0"
eberlm@63498
   591
    by (intro notI) 
eberlm@63498
   592
       (auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff)
eberlm@63498
   593
  hence [simp]: "p \<noteq> 0" by auto
eberlm@63498
   594
eberlm@63498
   595
  note \<open>irreducible p\<close>
eberlm@63498
   596
  also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" 
eberlm@63498
   597
    by (simp add: content_times_primitive_part_fract)
eberlm@63498
   598
  also have "irreducible \<dots> \<longleftrightarrow> irreducible (fract_poly (primitive_part_fract p))"
eberlm@63498
   599
    by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff)
eberlm@63498
   600
  finally show ?thesis using deg
eberlm@63498
   601
    by (simp add: nonconst_poly_irreducible_iff)
eberlm@63498
   602
qed
eberlm@63498
   603
eberlm@63633
   604
lemma prime_elem_primitive_part_fract:
eberlm@63498
   605
  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
eberlm@63633
   606
  shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)"
eberlm@63498
   607
  by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
eberlm@63498
   608
eberlm@63498
   609
lemma irreducible_linear_field_poly:
eberlm@63498
   610
  fixes a b :: "'a::field"
eberlm@63498
   611
  assumes "b \<noteq> 0"
eberlm@63498
   612
  shows "irreducible [:a,b:]"
eberlm@63498
   613
proof (rule irreducibleI)
eberlm@63498
   614
  fix p q assume pq: "[:a,b:] = p * q"
wenzelm@63539
   615
  also from pq assms have "degree \<dots> = degree p + degree q" 
eberlm@63498
   616
    by (intro degree_mult_eq) auto
eberlm@63498
   617
  finally have "degree p = 0 \<or> degree q = 0" using assms by auto
eberlm@63498
   618
  with assms pq show "is_unit p \<or> is_unit q"
eberlm@63498
   619
    by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
eberlm@63498
   620
qed (insert assms, auto simp: is_unit_poly_iff)
eberlm@63498
   621
eberlm@63633
   622
lemma prime_elem_linear_field_poly:
eberlm@63633
   623
  "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> prime_elem [:a,b:]"
eberlm@63498
   624
  by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
eberlm@63498
   625
eberlm@63498
   626
lemma irreducible_linear_poly:
eberlm@63498
   627
  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
eberlm@63498
   628
  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]"
eberlm@63498
   629
  by (auto intro!: irreducible_linear_field_poly 
eberlm@63498
   630
           simp:   nonconst_poly_irreducible_iff content_def map_poly_pCons)
eberlm@63498
   631
eberlm@63633
   632
lemma prime_elem_linear_poly:
eberlm@63498
   633
  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
eberlm@63633
   634
  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
eberlm@63498
   635
  by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
eberlm@63498
   636
haftmann@64591
   637
 
eberlm@63498
   638
subsection \<open>Prime factorisation of polynomials\<close>   
eberlm@63498
   639
eberlm@63498
   640
private lemma poly_prime_factorization_exists_content_1:
eberlm@63498
   641
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
   642
  assumes "p \<noteq> 0" "content p = 1"
nipkow@63830
   643
  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
eberlm@63498
   644
proof -
eberlm@63498
   645
  let ?P = "field_poly.prime_factorization (fract_poly p)"
nipkow@63830
   646
  define c where "c = prod_mset (image_mset fract_content ?P)"
eberlm@63498
   647
  define c' where "c' = c * to_fract (lead_coeff p)"
nipkow@63830
   648
  define e where "e = prod_mset (image_mset primitive_part_fract ?P)"
eberlm@63498
   649
  define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
eberlm@63498
   650
  have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 
eberlm@63498
   651
                      content (primitive_part_fract x))"
nipkow@63830
   652
    by (simp add: e_def content_prod_mset multiset.map_comp o_def)
eberlm@63498
   653
  also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
eberlm@63498
   654
    by (intro image_mset_cong content_primitive_part_fract) auto
haftmann@64591
   655
  finally have content_e: "content e = 1"
haftmann@64591
   656
    by simp    
eberlm@63498
   657
  
haftmann@66805
   658
  from \<open>p \<noteq> 0\<close> have "fract_poly p = [:lead_coeff (fract_poly p):] * 
haftmann@66805
   659
    smult (inverse (lead_coeff (fract_poly p))) (fract_poly p)"
haftmann@66805
   660
    by simp 
haftmann@66805
   661
  also have "[:lead_coeff (fract_poly p):] = [:to_fract (lead_coeff p):]" 
haftmann@66805
   662
    by (simp add: monom_0 degree_map_poly coeff_map_poly)
haftmann@66805
   663
  also from assms have "smult (inverse (lead_coeff (fract_poly p))) (fract_poly p) = prod_mset ?P" 
nipkow@63830
   664
    by (subst field_poly_prod_mset_prime_factorization) simp_all
nipkow@63830
   665
  also have "\<dots> = prod_mset (image_mset id ?P)" by simp
eberlm@63498
   666
  also have "image_mset id ?P = 
eberlm@63498
   667
               image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
eberlm@63498
   668
    by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
nipkow@63830
   669
  also have "prod_mset \<dots> = smult c (fract_poly e)"
haftmann@64591
   670
    by (subst prod_mset.distrib) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
eberlm@63498
   671
  also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
eberlm@63498
   672
    by (simp add: c'_def)
eberlm@63498
   673
  finally have eq: "fract_poly p = smult c' (fract_poly e)" .
eberlm@63498
   674
  also obtain b where b: "c' = to_fract b" "is_unit b"
eberlm@63498
   675
  proof -
eberlm@63498
   676
    from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
eberlm@63498
   677
    from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
eberlm@63498
   678
    with assms content_e have "a = normalize b" by (simp add: ab(4))
eberlm@63498
   679
    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
eberlm@63498
   680
    with ab ab' have "c' = to_fract b" by auto
eberlm@63498
   681
    from this and \<open>is_unit b\<close> show ?thesis by (rule that)
eberlm@63498
   682
  qed
eberlm@63498
   683
  hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp
eberlm@63498
   684
  finally have "p = smult b e" by (simp only: fract_poly_eq_iff)
eberlm@63498
   685
  hence "p = [:b:] * e" by simp
eberlm@63498
   686
  with b have "normalize p = normalize e" 
eberlm@63498
   687
    by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
nipkow@63830
   688
  also have "normalize e = prod_mset A"
nipkow@63830
   689
    by (simp add: multiset.map_comp e_def A_def normalize_prod_mset)
nipkow@63830
   690
  finally have "prod_mset A = normalize p" ..
eberlm@63498
   691
  
eberlm@63633
   692
  have "prime_elem p" if "p \<in># A" for p
eberlm@63633
   693
    using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible 
eberlm@63498
   694
                        dest!: field_poly_in_prime_factorization_imp_prime )
nipkow@63830
   695
  from this and \<open>prod_mset A = normalize p\<close> show ?thesis
eberlm@63498
   696
    by (intro exI[of _ A]) blast
eberlm@63498
   697
qed
eberlm@63498
   698
eberlm@63498
   699
lemma poly_prime_factorization_exists:
eberlm@63498
   700
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
   701
  assumes "p \<noteq> 0"
nipkow@63830
   702
  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
eberlm@63498
   703
proof -
eberlm@63498
   704
  define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
nipkow@63830
   705
  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)"
eberlm@63498
   706
    by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
eberlm@63498
   707
  then guess A by (elim exE conjE) note A = this
nipkow@63830
   708
  moreover from assms have "prod_mset B = [:content p:]"
nipkow@63830
   709
    by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization)
eberlm@63633
   710
  moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
haftmann@63905
   711
    by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime)
eberlm@63498
   712
  ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
eberlm@63498
   713
qed
eberlm@63498
   714
eberlm@63498
   715
end
eberlm@63498
   716
eberlm@63498
   717
eberlm@63498
   718
subsection \<open>Typeclass instances\<close>
eberlm@63498
   719
eberlm@63498
   720
instance poly :: (factorial_ring_gcd) factorial_semiring
eberlm@63498
   721
  by standard (rule poly_prime_factorization_exists)  
eberlm@63498
   722
eberlm@63498
   723
instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
eberlm@63498
   724
begin
eberlm@63498
   725
eberlm@63498
   726
definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
eberlm@63498
   727
  [code del]: "gcd_poly = gcd_factorial"
eberlm@63498
   728
eberlm@63498
   729
definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
eberlm@63498
   730
  [code del]: "lcm_poly = lcm_factorial"
eberlm@63498
   731
  
eberlm@63498
   732
definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
eberlm@63498
   733
 [code del]: "Gcd_poly = Gcd_factorial"
eberlm@63498
   734
eberlm@63498
   735
definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
eberlm@63498
   736
 [code del]: "Lcm_poly = Lcm_factorial"
eberlm@63498
   737
 
eberlm@63498
   738
instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
eberlm@63498
   739
eberlm@63498
   740
end
eberlm@63498
   741
haftmann@66817
   742
instantiation poly :: ("{field,factorial_ring_gcd}") "{unique_euclidean_ring, normalization_euclidean_semiring}"
eberlm@63498
   743
begin
eberlm@63498
   744
haftmann@64784
   745
definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
haftmann@64784
   746
  where "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
haftmann@64784
   747
haftmann@66838
   748
definition division_segment_poly :: "'a poly \<Rightarrow> 'a poly"
haftmann@66838
   749
  where [simp]: "division_segment_poly p = 1"
eberlm@63498
   750
haftmann@66806
   751
instance proof
haftmann@66806
   752
  show "(q * p + r) div p = q" if "p \<noteq> 0"
haftmann@66806
   753
    and "euclidean_size r < euclidean_size p" for q p r :: "'a poly"
haftmann@66806
   754
  proof -
haftmann@66806
   755
    from \<open>p \<noteq> 0\<close> eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
haftmann@66806
   756
      by (simp add: eucl_rel_poly_iff distrib_right)
haftmann@66806
   757
    then have "(r + q * p) div p = q + r div p"
haftmann@66806
   758
      by (rule div_poly_eq)
haftmann@66806
   759
    with that show ?thesis
haftmann@66806
   760
      by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps)
haftmann@66806
   761
  qed
haftmann@66840
   762
qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq power_add
haftmann@66840
   763
    intro!: degree_mod_less' split: if_splits)
haftmann@64784
   764
eberlm@63498
   765
end
eberlm@63498
   766
haftmann@66817
   767
instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd
haftmann@66817
   768
  by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard
eberlm@63498
   769
eberlm@63498
   770
  
eberlm@63498
   771
subsection \<open>Polynomial GCD\<close>
eberlm@63498
   772
eberlm@63498
   773
lemma gcd_poly_decompose:
eberlm@63498
   774
  fixes p q :: "'a :: factorial_ring_gcd poly"
eberlm@63498
   775
  shows "gcd p q = 
eberlm@63498
   776
           smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
eberlm@63498
   777
proof (rule sym, rule gcdI)
eberlm@63498
   778
  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
eberlm@63498
   779
          [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all
eberlm@63498
   780
  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p"
eberlm@63498
   781
    by simp
eberlm@63498
   782
next
eberlm@63498
   783
  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
eberlm@63498
   784
          [:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all
eberlm@63498
   785
  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q"
eberlm@63498
   786
    by simp
eberlm@63498
   787
next
eberlm@63498
   788
  fix d assume "d dvd p" "d dvd q"
eberlm@63498
   789
  hence "[:content d:] * primitive_part d dvd 
eberlm@63498
   790
           [:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)"
eberlm@63498
   791
    by (intro mult_dvd_mono) auto
eberlm@63498
   792
  thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
eberlm@63498
   793
    by simp
eberlm@63498
   794
qed (auto simp: normalize_smult)
eberlm@63498
   795
  
eberlm@63498
   796
eberlm@63498
   797
lemma gcd_poly_pseudo_mod:
eberlm@63498
   798
  fixes p q :: "'a :: factorial_ring_gcd poly"
eberlm@63498
   799
  assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1"
eberlm@63498
   800
  shows   "gcd p q = gcd q (primitive_part (pseudo_mod p q))"
eberlm@63498
   801
proof -
eberlm@63498
   802
  define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)"
eberlm@63498
   803
  define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]"
eberlm@63498
   804
  have [simp]: "primitive_part a = unit_factor a"
eberlm@63498
   805
    by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0)
eberlm@63498
   806
  from nz have [simp]: "a \<noteq> 0" by (auto simp: a_def)
eberlm@63498
   807
  
eberlm@63498
   808
  have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def)
eberlm@63498
   809
  have "gcd (q * r + s) q = gcd q s"
eberlm@63498
   810
    using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac)
eberlm@63498
   811
  with pseudo_divmod(1)[OF nz rs]
eberlm@63498
   812
    have "gcd (p * a) q = gcd q s" by (simp add: a_def)
eberlm@63498
   813
  also from prim have "gcd (p * a) q = gcd p q"
eberlm@63498
   814
    by (subst gcd_poly_decompose)
eberlm@63498
   815
       (auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim 
eberlm@63498
   816
             simp del: mult_pCons_right )
eberlm@63498
   817
  also from prim have "gcd q s = gcd q (primitive_part s)"
eberlm@63498
   818
    by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim)
eberlm@63498
   819
  also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def)
eberlm@63498
   820
  finally show ?thesis .
eberlm@63498
   821
qed
eberlm@63498
   822
eberlm@63498
   823
lemma degree_pseudo_mod_less:
eberlm@63498
   824
  assumes "q \<noteq> 0" "pseudo_mod p q \<noteq> 0"
eberlm@63498
   825
  shows   "degree (pseudo_mod p q) < degree q"
eberlm@63498
   826
  using pseudo_mod(2)[of q p] assms by auto
eberlm@63498
   827
eberlm@63498
   828
function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
eberlm@63498
   829
  "gcd_poly_code_aux p q = 
eberlm@63498
   830
     (if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" 
eberlm@63498
   831
by auto
eberlm@63498
   832
termination
eberlm@63498
   833
  by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
haftmann@64164
   834
     (auto simp: degree_pseudo_mod_less)
eberlm@63498
   835
eberlm@63498
   836
declare gcd_poly_code_aux.simps [simp del]
eberlm@63498
   837
eberlm@63498
   838
lemma gcd_poly_code_aux_correct:
eberlm@63498
   839
  assumes "content p = 1" "q = 0 \<or> content q = 1"
eberlm@63498
   840
  shows   "gcd_poly_code_aux p q = gcd p q"
eberlm@63498
   841
  using assms
eberlm@63498
   842
proof (induction p q rule: gcd_poly_code_aux.induct)
eberlm@63498
   843
  case (1 p q)
eberlm@63498
   844
  show ?case
eberlm@63498
   845
  proof (cases "q = 0")
eberlm@63498
   846
    case True
eberlm@63498
   847
    thus ?thesis by (subst gcd_poly_code_aux.simps) auto
eberlm@63498
   848
  next
eberlm@63498
   849
    case False
eberlm@63498
   850
    hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))"
eberlm@63498
   851
      by (subst gcd_poly_code_aux.simps) simp_all
eberlm@63498
   852
    also from "1.prems" False 
eberlm@63498
   853
      have "primitive_part (pseudo_mod p q) = 0 \<or> 
eberlm@63498
   854
              content (primitive_part (pseudo_mod p q)) = 1"
eberlm@63498
   855
      by (cases "pseudo_mod p q = 0") auto
eberlm@63498
   856
    with "1.prems" False 
eberlm@63498
   857
      have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = 
eberlm@63498
   858
              gcd q (primitive_part (pseudo_mod p q))"
eberlm@63498
   859
      by (intro 1) simp_all
eberlm@63498
   860
    also from "1.prems" False 
eberlm@63498
   861
      have "\<dots> = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto
eberlm@63498
   862
    finally show ?thesis .
eberlm@63498
   863
  qed
eberlm@63498
   864
qed
eberlm@63498
   865
eberlm@63498
   866
definition gcd_poly_code 
eberlm@63498
   867
    :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
eberlm@63498
   868
  where "gcd_poly_code p q = 
eberlm@63498
   869
           (if p = 0 then normalize q else if q = 0 then normalize p else
eberlm@63498
   870
              smult (gcd (content p) (content q)) 
eberlm@63498
   871
                (gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
eberlm@63498
   872
haftmann@64591
   873
lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
haftmann@64591
   874
  by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
haftmann@64591
   875
eberlm@63498
   876
lemma lcm_poly_code [code]: 
eberlm@63498
   877
  fixes p q :: "'a :: factorial_ring_gcd poly"
eberlm@63498
   878
  shows "lcm p q = normalize (p * q) div gcd p q"
haftmann@64591
   879
  by (fact lcm_gcd)
eberlm@63498
   880
haftmann@64850
   881
lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
haftmann@64850
   882
lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
haftmann@64860
   883
haftmann@64591
   884
text \<open>Example:
haftmann@64591
   885
  @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
haftmann@64591
   886
\<close>
eberlm@63498
   887
  
wenzelm@63764
   888
end