src/HOL/Number_Theory/Polynomial_Factorial.thy
author eberlm <eberlm@in.tum.de>
Thu Jul 14 14:49:09 2016 +0200 (2016-07-14)
changeset 63500 0dac030afd36
parent 63499 9c9a59949887
child 63539 70d4d9e5707b
permissions -rw-r--r--
Added normalized fractions
eberlm@63498
     1
theory Polynomial_Factorial
eberlm@63498
     2
imports 
eberlm@63498
     3
  Complex_Main
eberlm@63498
     4
  Euclidean_Algorithm 
eberlm@63498
     5
  "~~/src/HOL/Library/Polynomial"
eberlm@63500
     6
  "~~/src/HOL/Library/Normalized_Fraction"
eberlm@63498
     7
begin
eberlm@63498
     8
eberlm@63498
     9
subsection \<open>Prelude\<close>
eberlm@63498
    10
eberlm@63498
    11
lemma msetprod_mult: 
eberlm@63498
    12
  "msetprod (image_mset (\<lambda>x. f x * g x) A) = msetprod (image_mset f A) * msetprod (image_mset g A)"
eberlm@63498
    13
  by (induction A) (simp_all add: mult_ac)
eberlm@63498
    14
  
eberlm@63498
    15
lemma msetprod_const: "msetprod (image_mset (\<lambda>_. c) A) = c ^ size A"
eberlm@63498
    16
  by (induction A) (simp_all add: mult_ac)
eberlm@63498
    17
  
eberlm@63498
    18
lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
eberlm@63498
    19
proof safe
eberlm@63498
    20
  assume "x \<noteq> 0"
eberlm@63498
    21
  hence "y = x * (y / x)" by (simp add: field_simps)
eberlm@63498
    22
  thus "x dvd y" by (rule dvdI)
eberlm@63498
    23
qed auto
eberlm@63498
    24
eberlm@63498
    25
lemma nat_descend_induct [case_names base descend]:
eberlm@63498
    26
  assumes "\<And>k::nat. k > n \<Longrightarrow> P k"
eberlm@63498
    27
  assumes "\<And>k::nat. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
eberlm@63498
    28
  shows   "P m"
eberlm@63498
    29
  using assms by induction_schema (force intro!: wf_measure[of "\<lambda>k. Suc n - k"])+
eberlm@63498
    30
eberlm@63498
    31
lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
eberlm@63498
    32
  by (metis GreatestI)
eberlm@63498
    33
eberlm@63498
    34
eberlm@63498
    35
context field
eberlm@63498
    36
begin
eberlm@63498
    37
eberlm@63498
    38
subclass idom_divide ..
eberlm@63498
    39
eberlm@63498
    40
end
eberlm@63498
    41
eberlm@63498
    42
context field
eberlm@63498
    43
begin
eberlm@63498
    44
eberlm@63498
    45
definition normalize_field :: "'a \<Rightarrow> 'a" 
eberlm@63498
    46
  where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
eberlm@63498
    47
definition unit_factor_field :: "'a \<Rightarrow> 'a" 
eberlm@63498
    48
  where [simp]: "unit_factor_field x = x"
eberlm@63498
    49
definition euclidean_size_field :: "'a \<Rightarrow> nat" 
eberlm@63498
    50
  where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
eberlm@63498
    51
definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
eberlm@63498
    52
  where [simp]: "mod_field x y = (if y = 0 then x else 0)"
eberlm@63498
    53
eberlm@63498
    54
end
eberlm@63498
    55
eberlm@63498
    56
instantiation real :: euclidean_ring
eberlm@63498
    57
begin
eberlm@63498
    58
eberlm@63498
    59
definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
eberlm@63498
    60
definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
eberlm@63498
    61
definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
eberlm@63498
    62
definition [simp]: "mod_real = (mod_field :: real \<Rightarrow> _)"
eberlm@63498
    63
eberlm@63498
    64
instance by standard (simp_all add: dvd_field_iff divide_simps)
eberlm@63498
    65
end
eberlm@63498
    66
eberlm@63498
    67
instantiation real :: euclidean_ring_gcd
eberlm@63498
    68
begin
eberlm@63498
    69
eberlm@63498
    70
definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
eberlm@63498
    71
  "gcd_real = gcd_eucl"
eberlm@63498
    72
definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
eberlm@63498
    73
  "lcm_real = lcm_eucl"
eberlm@63498
    74
definition Gcd_real :: "real set \<Rightarrow> real" where
eberlm@63498
    75
 "Gcd_real = Gcd_eucl"
eberlm@63498
    76
definition Lcm_real :: "real set \<Rightarrow> real" where
eberlm@63498
    77
 "Lcm_real = Lcm_eucl"
eberlm@63498
    78
eberlm@63498
    79
instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
eberlm@63498
    80
eberlm@63498
    81
end
eberlm@63498
    82
eberlm@63498
    83
instantiation rat :: euclidean_ring
eberlm@63498
    84
begin
eberlm@63498
    85
eberlm@63498
    86
definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
eberlm@63498
    87
definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
eberlm@63498
    88
definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
eberlm@63498
    89
definition [simp]: "mod_rat = (mod_field :: rat \<Rightarrow> _)"
eberlm@63498
    90
eberlm@63498
    91
instance by standard (simp_all add: dvd_field_iff divide_simps)
eberlm@63498
    92
end
eberlm@63498
    93
eberlm@63498
    94
instantiation rat :: euclidean_ring_gcd
eberlm@63498
    95
begin
eberlm@63498
    96
eberlm@63498
    97
definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
eberlm@63498
    98
  "gcd_rat = gcd_eucl"
eberlm@63498
    99
definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
eberlm@63498
   100
  "lcm_rat = lcm_eucl"
eberlm@63498
   101
definition Gcd_rat :: "rat set \<Rightarrow> rat" where
eberlm@63498
   102
 "Gcd_rat = Gcd_eucl"
eberlm@63498
   103
definition Lcm_rat :: "rat set \<Rightarrow> rat" where
eberlm@63498
   104
 "Lcm_rat = Lcm_eucl"
eberlm@63498
   105
eberlm@63498
   106
instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
eberlm@63498
   107
eberlm@63498
   108
end
eberlm@63498
   109
eberlm@63498
   110
instantiation complex :: euclidean_ring
eberlm@63498
   111
begin
eberlm@63498
   112
eberlm@63498
   113
definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
eberlm@63498
   114
definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
eberlm@63498
   115
definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
eberlm@63498
   116
definition [simp]: "mod_complex = (mod_field :: complex \<Rightarrow> _)"
eberlm@63498
   117
eberlm@63498
   118
instance by standard (simp_all add: dvd_field_iff divide_simps)
eberlm@63498
   119
end
eberlm@63498
   120
eberlm@63498
   121
instantiation complex :: euclidean_ring_gcd
eberlm@63498
   122
begin
eberlm@63498
   123
eberlm@63498
   124
definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
eberlm@63498
   125
  "gcd_complex = gcd_eucl"
eberlm@63498
   126
definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
eberlm@63498
   127
  "lcm_complex = lcm_eucl"
eberlm@63498
   128
definition Gcd_complex :: "complex set \<Rightarrow> complex" where
eberlm@63498
   129
 "Gcd_complex = Gcd_eucl"
eberlm@63498
   130
definition Lcm_complex :: "complex set \<Rightarrow> complex" where
eberlm@63498
   131
 "Lcm_complex = Lcm_eucl"
eberlm@63498
   132
eberlm@63498
   133
instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
eberlm@63498
   134
eberlm@63498
   135
end
eberlm@63498
   136
eberlm@63498
   137
eberlm@63498
   138
eberlm@63498
   139
subsection \<open>Lifting elements into the field of fractions\<close>
eberlm@63498
   140
eberlm@63498
   141
definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
eberlm@63498
   142
eberlm@63498
   143
lemma to_fract_0 [simp]: "to_fract 0 = 0"
eberlm@63498
   144
  by (simp add: to_fract_def eq_fract Zero_fract_def)
eberlm@63498
   145
eberlm@63498
   146
lemma to_fract_1 [simp]: "to_fract 1 = 1"
eberlm@63498
   147
  by (simp add: to_fract_def eq_fract One_fract_def)
eberlm@63498
   148
eberlm@63498
   149
lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y"
eberlm@63498
   150
  by (simp add: to_fract_def)
eberlm@63498
   151
eberlm@63498
   152
lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y"
eberlm@63498
   153
  by (simp add: to_fract_def)
eberlm@63498
   154
  
eberlm@63498
   155
lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x"
eberlm@63498
   156
  by (simp add: to_fract_def)
eberlm@63498
   157
  
eberlm@63498
   158
lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y"
eberlm@63498
   159
  by (simp add: to_fract_def)
eberlm@63498
   160
eberlm@63498
   161
lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \<longleftrightarrow> x = y"
eberlm@63498
   162
  by (simp add: to_fract_def eq_fract)
eberlm@63498
   163
  
eberlm@63498
   164
lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \<longleftrightarrow> x = 0"
eberlm@63498
   165
  by (simp add: to_fract_def Zero_fract_def eq_fract)
eberlm@63498
   166
eberlm@63498
   167
lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0"
eberlm@63498
   168
  by transfer simp
eberlm@63498
   169
eberlm@63498
   170
lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x"
eberlm@63498
   171
  by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp)
eberlm@63498
   172
eberlm@63498
   173
lemma to_fract_quot_of_fract:
eberlm@63498
   174
  assumes "snd (quot_of_fract x) = 1"
eberlm@63498
   175
  shows   "to_fract (fst (quot_of_fract x)) = x"
eberlm@63498
   176
proof -
eberlm@63498
   177
  have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp
eberlm@63498
   178
  also note assms
eberlm@63498
   179
  finally show ?thesis by (simp add: to_fract_def)
eberlm@63498
   180
qed
eberlm@63498
   181
eberlm@63498
   182
lemma snd_quot_of_fract_Fract_whole:
eberlm@63498
   183
  assumes "y dvd x"
eberlm@63498
   184
  shows   "snd (quot_of_fract (Fract x y)) = 1"
eberlm@63498
   185
  using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd)
eberlm@63498
   186
  
eberlm@63498
   187
lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b"
eberlm@63498
   188
  by (simp add: to_fract_def)
eberlm@63498
   189
eberlm@63498
   190
lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)"
eberlm@63498
   191
  unfolding to_fract_def by transfer (simp add: normalize_quot_def)
eberlm@63498
   192
eberlm@63498
   193
lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0"
eberlm@63498
   194
  by transfer simp
eberlm@63498
   195
 
eberlm@63498
   196
lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1"
eberlm@63498
   197
  unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all
eberlm@63498
   198
eberlm@63498
   199
lemma coprime_quot_of_fract:
eberlm@63498
   200
  "coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))"
eberlm@63498
   201
  by transfer (simp add: coprime_normalize_quot)
eberlm@63498
   202
eberlm@63498
   203
lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1"
eberlm@63498
   204
  using quot_of_fract_in_normalized_fracts[of x] 
eberlm@63498
   205
  by (simp add: normalized_fracts_def case_prod_unfold)  
eberlm@63498
   206
eberlm@63498
   207
lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x"
eberlm@63498
   208
  by (subst (2) normalize_mult_unit_factor [symmetric, of x])
eberlm@63498
   209
     (simp del: normalize_mult_unit_factor)
eberlm@63498
   210
  
eberlm@63498
   211
lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
eberlm@63498
   212
  by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
eberlm@63498
   213
eberlm@63498
   214
  
eberlm@63498
   215
subsection \<open>Mapping polynomials\<close>
eberlm@63498
   216
eberlm@63498
   217
definition map_poly 
eberlm@63498
   218
     :: "('a :: comm_semiring_0 \<Rightarrow> 'b :: comm_semiring_0) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
eberlm@63498
   219
  "map_poly f p = Poly (map f (coeffs p))"
eberlm@63498
   220
eberlm@63498
   221
lemma map_poly_0 [simp]: "map_poly f 0 = 0"
eberlm@63498
   222
  by (simp add: map_poly_def)
eberlm@63498
   223
eberlm@63498
   224
lemma map_poly_1: "map_poly f 1 = [:f 1:]"
eberlm@63498
   225
  by (simp add: map_poly_def)
eberlm@63498
   226
eberlm@63498
   227
lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
eberlm@63498
   228
  by (simp add: map_poly_def one_poly_def)
eberlm@63498
   229
eberlm@63498
   230
lemma coeff_map_poly:
eberlm@63498
   231
  assumes "f 0 = 0"
eberlm@63498
   232
  shows   "coeff (map_poly f p) n = f (coeff p n)"
eberlm@63498
   233
  by (auto simp: map_poly_def nth_default_def coeffs_def assms
eberlm@63498
   234
        not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
eberlm@63498
   235
eberlm@63498
   236
lemma coeffs_map_poly [code abstract]: 
eberlm@63498
   237
    "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
eberlm@63498
   238
  by (simp add: map_poly_def)
eberlm@63498
   239
eberlm@63498
   240
lemma set_coeffs_map_poly:
eberlm@63498
   241
  "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
eberlm@63498
   242
  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
eberlm@63498
   243
eberlm@63498
   244
lemma coeffs_map_poly': 
eberlm@63498
   245
  assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
eberlm@63498
   246
  shows   "coeffs (map_poly f p) = map f (coeffs p)"
eberlm@63498
   247
  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 
eberlm@63498
   248
                           intro!: strip_while_not_last split: if_splits)
eberlm@63498
   249
eberlm@63498
   250
lemma degree_map_poly:
eberlm@63498
   251
  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
eberlm@63498
   252
  shows   "degree (map_poly f p) = degree p"
eberlm@63498
   253
  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
eberlm@63498
   254
eberlm@63498
   255
lemma map_poly_eq_0_iff:
eberlm@63498
   256
  assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
eberlm@63498
   257
  shows   "map_poly f p = 0 \<longleftrightarrow> p = 0"
eberlm@63498
   258
proof -
eberlm@63498
   259
  {
eberlm@63498
   260
    fix n :: nat
eberlm@63498
   261
    have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
eberlm@63498
   262
    also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
eberlm@63498
   263
    proof (cases "n < length (coeffs p)")
eberlm@63498
   264
      case True
eberlm@63498
   265
      hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
eberlm@63498
   266
      with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
eberlm@63498
   267
    qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
eberlm@63498
   268
    finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
eberlm@63498
   269
  }
eberlm@63498
   270
  thus ?thesis by (auto simp: poly_eq_iff)
eberlm@63498
   271
qed
eberlm@63498
   272
eberlm@63498
   273
lemma map_poly_smult:
eberlm@63498
   274
  assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
eberlm@63498
   275
  shows   "map_poly f (smult c p) = smult (f c) (map_poly f p)"
eberlm@63498
   276
  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
eberlm@63498
   277
eberlm@63498
   278
lemma map_poly_pCons:
eberlm@63498
   279
  assumes "f 0 = 0"
eberlm@63498
   280
  shows   "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
eberlm@63498
   281
  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
eberlm@63498
   282
eberlm@63498
   283
lemma map_poly_map_poly:
eberlm@63498
   284
  assumes "f 0 = 0" "g 0 = 0"
eberlm@63498
   285
  shows   "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
eberlm@63498
   286
  by (intro poly_eqI) (simp add: coeff_map_poly assms)
eberlm@63498
   287
eberlm@63498
   288
lemma map_poly_id [simp]: "map_poly id p = p"
eberlm@63498
   289
  by (simp add: map_poly_def)
eberlm@63498
   290
eberlm@63498
   291
lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
eberlm@63498
   292
  by (simp add: map_poly_def)
eberlm@63498
   293
eberlm@63498
   294
lemma map_poly_cong: 
eberlm@63498
   295
  assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
eberlm@63498
   296
  shows   "map_poly f p = map_poly g p"
eberlm@63498
   297
proof -
eberlm@63498
   298
  from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
eberlm@63498
   299
  thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
eberlm@63498
   300
qed
eberlm@63498
   301
eberlm@63498
   302
lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
eberlm@63498
   303
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
eberlm@63498
   304
eberlm@63498
   305
lemma map_poly_idI:
eberlm@63498
   306
  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
eberlm@63498
   307
  shows   "map_poly f p = p"
eberlm@63498
   308
  using map_poly_cong[OF assms, of _ id] by simp
eberlm@63498
   309
eberlm@63498
   310
lemma map_poly_idI':
eberlm@63498
   311
  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
eberlm@63498
   312
  shows   "p = map_poly f p"
eberlm@63498
   313
  using map_poly_cong[OF assms, of _ id] by simp
eberlm@63498
   314
eberlm@63498
   315
lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
eberlm@63498
   316
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
eberlm@63498
   317
eberlm@63498
   318
lemma div_const_poly_conv_map_poly: 
eberlm@63498
   319
  assumes "[:c:] dvd p"
eberlm@63498
   320
  shows   "p div [:c:] = map_poly (\<lambda>x. x div c) p"
eberlm@63498
   321
proof (cases "c = 0")
eberlm@63498
   322
  case False
eberlm@63498
   323
  from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
eberlm@63498
   324
  moreover {
eberlm@63498
   325
    have "smult c q = [:c:] * q" by simp
eberlm@63498
   326
    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto)
eberlm@63498
   327
    finally have "smult c q div [:c:] = q" .
eberlm@63498
   328
  }
eberlm@63498
   329
  ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
eberlm@63498
   330
qed (auto intro!: poly_eqI simp: coeff_map_poly)
eberlm@63498
   331
eberlm@63498
   332
eberlm@63498
   333
eberlm@63498
   334
subsection \<open>Various facts about polynomials\<close>
eberlm@63498
   335
eberlm@63498
   336
lemma msetprod_const_poly: "msetprod (image_mset (\<lambda>x. [:f x:]) A) = [:msetprod (image_mset f A):]"
eberlm@63498
   337
  by (induction A) (simp_all add: one_poly_def mult_ac)
eberlm@63498
   338
eberlm@63498
   339
lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
eberlm@63498
   340
  using degree_mod_less[of b a] by auto
eberlm@63498
   341
  
eberlm@63498
   342
lemma is_unit_const_poly_iff: 
eberlm@63498
   343
    "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
eberlm@63498
   344
  by (auto simp: one_poly_def)
eberlm@63498
   345
eberlm@63498
   346
lemma is_unit_poly_iff:
eberlm@63498
   347
  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
eberlm@63498
   348
  shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
eberlm@63498
   349
proof safe
eberlm@63498
   350
  assume "p dvd 1"
eberlm@63498
   351
  then obtain q where pq: "1 = p * q" by (erule dvdE)
eberlm@63498
   352
  hence "degree 1 = degree (p * q)" by simp
eberlm@63498
   353
  also from pq have "\<dots> = degree p + degree q" by (intro degree_mult_eq) auto
eberlm@63498
   354
  finally have "degree p = 0" by simp
eberlm@63498
   355
  from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" .
eberlm@63498
   356
  with \<open>p dvd 1\<close> show "\<exists>c. p = [:c:] \<and> c dvd 1"
eberlm@63498
   357
    by (auto simp: is_unit_const_poly_iff)
eberlm@63498
   358
qed (auto simp: is_unit_const_poly_iff)
eberlm@63498
   359
eberlm@63498
   360
lemma is_unit_polyE:
eberlm@63498
   361
  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
eberlm@63498
   362
  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
eberlm@63498
   363
  using assms by (subst (asm) is_unit_poly_iff) blast
eberlm@63498
   364
eberlm@63498
   365
lemma smult_eq_iff:
eberlm@63498
   366
  assumes "(b :: 'a :: field) \<noteq> 0"
eberlm@63498
   367
  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
eberlm@63498
   368
proof
eberlm@63498
   369
  assume "smult a p = smult b q"
eberlm@63498
   370
  also from assms have "smult (inverse b) \<dots> = q" by simp
eberlm@63498
   371
  finally show "smult (a / b) p = q" by (simp add: field_simps)
eberlm@63498
   372
qed (insert assms, auto)
eberlm@63498
   373
eberlm@63498
   374
lemma irreducible_const_poly_iff:
eberlm@63498
   375
  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
eberlm@63498
   376
  shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
eberlm@63498
   377
proof
eberlm@63498
   378
  assume A: "irreducible c"
eberlm@63498
   379
  show "irreducible [:c:]"
eberlm@63498
   380
  proof (rule irreducibleI)
eberlm@63498
   381
    fix a b assume ab: "[:c:] = a * b"
eberlm@63498
   382
    hence "degree [:c:] = degree (a * b)" by (simp only: )
eberlm@63498
   383
    also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
eberlm@63498
   384
    hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
eberlm@63498
   385
    finally have "degree a = 0" "degree b = 0" by auto
eberlm@63498
   386
    then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
eberlm@63498
   387
    from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
eberlm@63498
   388
    hence "c = a' * b'" by (simp add: ab' mult_ac)
eberlm@63498
   389
    from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
eberlm@63498
   390
    with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
eberlm@63498
   391
  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
eberlm@63498
   392
next
eberlm@63498
   393
  assume A: "irreducible [:c:]"
eberlm@63498
   394
  show "irreducible c"
eberlm@63498
   395
  proof (rule irreducibleI)
eberlm@63498
   396
    fix a b assume ab: "c = a * b"
eberlm@63498
   397
    hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
eberlm@63498
   398
    from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
eberlm@63498
   399
    thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
eberlm@63498
   400
  qed (insert A, auto simp: irreducible_def one_poly_def)
eberlm@63498
   401
qed
eberlm@63498
   402
eberlm@63498
   403
lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
eberlm@63498
   404
  by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
eberlm@63498
   405
eberlm@63498
   406
  
eberlm@63498
   407
subsection \<open>Normalisation of polynomials\<close>
eberlm@63498
   408
eberlm@63498
   409
instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom
eberlm@63498
   410
begin
eberlm@63498
   411
eberlm@63498
   412
definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
eberlm@63498
   413
  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
eberlm@63498
   414
eberlm@63498
   415
definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
eberlm@63498
   416
  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
eberlm@63498
   417
eberlm@63498
   418
lemma normalize_poly_altdef:
eberlm@63498
   419
  "normalize p = p div [:unit_factor (lead_coeff p):]"
eberlm@63498
   420
proof (cases "p = 0")
eberlm@63498
   421
  case False
eberlm@63498
   422
  thus ?thesis
eberlm@63498
   423
    by (subst div_const_poly_conv_map_poly)
eberlm@63498
   424
       (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
eberlm@63498
   425
qed (auto simp: normalize_poly_def)
eberlm@63498
   426
eberlm@63498
   427
instance
eberlm@63498
   428
proof
eberlm@63498
   429
  fix p :: "'a poly"
eberlm@63498
   430
  show "unit_factor p * normalize p = p"
eberlm@63498
   431
    by (cases "p = 0")
eberlm@63498
   432
       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
eberlm@63498
   433
          smult_conv_map_poly map_poly_map_poly o_def)
eberlm@63498
   434
next
eberlm@63498
   435
  fix p :: "'a poly"
eberlm@63498
   436
  assume "is_unit p"
eberlm@63498
   437
  then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff)
eberlm@63498
   438
  thus "normalize p = 1"
eberlm@63498
   439
    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
eberlm@63498
   440
next
eberlm@63498
   441
  fix p :: "'a poly" assume "p \<noteq> 0"
eberlm@63498
   442
  thus "is_unit (unit_factor p)"
eberlm@63498
   443
    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
eberlm@63498
   444
qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
eberlm@63498
   445
eberlm@63498
   446
end
eberlm@63498
   447
eberlm@63498
   448
lemma unit_factor_pCons:
eberlm@63498
   449
  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
eberlm@63498
   450
  by (simp add: unit_factor_poly_def)
eberlm@63498
   451
eberlm@63498
   452
lemma normalize_monom [simp]:
eberlm@63498
   453
  "normalize (monom a n) = monom (normalize a) n"
eberlm@63498
   454
  by (simp add: map_poly_monom normalize_poly_def)
eberlm@63498
   455
eberlm@63498
   456
lemma unit_factor_monom [simp]:
eberlm@63498
   457
  "unit_factor (monom a n) = monom (unit_factor a) 0"
eberlm@63498
   458
  by (simp add: unit_factor_poly_def )
eberlm@63498
   459
eberlm@63498
   460
lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
eberlm@63498
   461
  by (simp add: normalize_poly_def map_poly_pCons)
eberlm@63498
   462
eberlm@63498
   463
lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
eberlm@63498
   464
proof -
eberlm@63498
   465
  have "smult c p = [:c:] * p" by simp
eberlm@63498
   466
  also have "normalize \<dots> = smult (normalize c) (normalize p)"
eberlm@63498
   467
    by (subst normalize_mult) (simp add: normalize_const_poly)
eberlm@63498
   468
  finally show ?thesis .
eberlm@63498
   469
qed
eberlm@63498
   470
eberlm@63498
   471
lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
eberlm@63498
   472
proof -
eberlm@63498
   473
  have "smult c p = [:c:] * p" by simp
eberlm@63498
   474
  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
eberlm@63498
   475
  proof safe
eberlm@63498
   476
    assume A: "[:c:] * p dvd 1"
eberlm@63498
   477
    thus "p dvd 1" by (rule dvd_mult_right)
eberlm@63498
   478
    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
eberlm@63498
   479
    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
eberlm@63498
   480
    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
eberlm@63498
   481
    also note B [symmetric]
eberlm@63498
   482
    finally show "c dvd 1" by simp
eberlm@63498
   483
  next
eberlm@63498
   484
    assume "c dvd 1" "p dvd 1"
eberlm@63498
   485
    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
eberlm@63498
   486
    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
eberlm@63498
   487
    hence "[:c:] dvd 1" by (rule dvdI)
eberlm@63498
   488
    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
eberlm@63498
   489
  qed
eberlm@63498
   490
  finally show ?thesis .
eberlm@63498
   491
qed
eberlm@63498
   492
eberlm@63498
   493
eberlm@63498
   494
subsection \<open>Content and primitive part of a polynomial\<close>
eberlm@63498
   495
eberlm@63498
   496
definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
eberlm@63498
   497
  "content p = Gcd (set (coeffs p))"
eberlm@63498
   498
eberlm@63498
   499
lemma content_0 [simp]: "content 0 = 0"
eberlm@63498
   500
  by (simp add: content_def)
eberlm@63498
   501
eberlm@63498
   502
lemma content_1 [simp]: "content 1 = 1"
eberlm@63498
   503
  by (simp add: content_def)
eberlm@63498
   504
eberlm@63498
   505
lemma content_const [simp]: "content [:c:] = normalize c"
eberlm@63498
   506
  by (simp add: content_def cCons_def)
eberlm@63498
   507
eberlm@63498
   508
lemma const_poly_dvd_iff_dvd_content:
eberlm@63498
   509
  fixes c :: "'a :: semiring_Gcd"
eberlm@63498
   510
  shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
eberlm@63498
   511
proof (cases "p = 0")
eberlm@63498
   512
  case [simp]: False
eberlm@63498
   513
  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
eberlm@63498
   514
  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
eberlm@63498
   515
  proof safe
eberlm@63498
   516
    fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
eberlm@63498
   517
    thus "c dvd coeff p n"
eberlm@63498
   518
      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
eberlm@63498
   519
  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
eberlm@63498
   520
  also have "\<dots> \<longleftrightarrow> c dvd content p"
eberlm@63498
   521
    by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
eberlm@63498
   522
          dvd_mult_unit_iff lead_coeff_nonzero)
eberlm@63498
   523
  finally show ?thesis .
eberlm@63498
   524
qed simp_all
eberlm@63498
   525
eberlm@63498
   526
lemma content_dvd [simp]: "[:content p:] dvd p"
eberlm@63498
   527
  by (subst const_poly_dvd_iff_dvd_content) simp_all
eberlm@63498
   528
  
eberlm@63498
   529
lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
eberlm@63498
   530
  by (cases "n \<le> degree p") 
eberlm@63498
   531
     (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
eberlm@63498
   532
eberlm@63498
   533
lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
eberlm@63498
   534
  by (simp add: content_def Gcd_dvd)
eberlm@63498
   535
eberlm@63498
   536
lemma normalize_content [simp]: "normalize (content p) = content p"
eberlm@63498
   537
  by (simp add: content_def)
eberlm@63498
   538
eberlm@63498
   539
lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
eberlm@63498
   540
proof
eberlm@63498
   541
  assume "is_unit (content p)"
eberlm@63498
   542
  hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
eberlm@63498
   543
  thus "content p = 1" by simp
eberlm@63498
   544
qed auto
eberlm@63498
   545
eberlm@63498
   546
lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
eberlm@63498
   547
  by (simp add: content_def coeffs_smult Gcd_mult)
eberlm@63498
   548
eberlm@63498
   549
lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
eberlm@63498
   550
  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
eberlm@63498
   551
eberlm@63498
   552
definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
eberlm@63498
   553
  "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
eberlm@63498
   554
  
eberlm@63498
   555
lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
eberlm@63498
   556
  by (simp add: primitive_part_def)
eberlm@63498
   557
eberlm@63498
   558
lemma content_times_primitive_part [simp]:
eberlm@63498
   559
  fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
eberlm@63498
   560
  shows "smult (content p) (primitive_part p) = p"
eberlm@63498
   561
proof (cases "p = 0")
eberlm@63498
   562
  case False
eberlm@63498
   563
  thus ?thesis
eberlm@63498
   564
  unfolding primitive_part_def
eberlm@63498
   565
  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 
eberlm@63498
   566
           intro: map_poly_idI)
eberlm@63498
   567
qed simp_all
eberlm@63498
   568
eberlm@63498
   569
lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
eberlm@63498
   570
proof (cases "p = 0")
eberlm@63498
   571
  case False
eberlm@63498
   572
  hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
eberlm@63498
   573
    by (simp add:  primitive_part_def)
eberlm@63498
   574
  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
eberlm@63498
   575
    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
eberlm@63498
   576
  finally show ?thesis using False by simp
eberlm@63498
   577
qed simp
eberlm@63498
   578
eberlm@63498
   579
lemma content_primitive_part [simp]:
eberlm@63498
   580
  assumes "p \<noteq> 0"
eberlm@63498
   581
  shows   "content (primitive_part p) = 1"
eberlm@63498
   582
proof -
eberlm@63498
   583
  have "p = smult (content p) (primitive_part p)" by simp
eberlm@63498
   584
  also have "content \<dots> = content p * content (primitive_part p)" 
eberlm@63498
   585
    by (simp del: content_times_primitive_part)
eberlm@63498
   586
  finally show ?thesis using assms by simp
eberlm@63498
   587
qed
eberlm@63498
   588
eberlm@63498
   589
lemma content_decompose:
eberlm@63498
   590
  fixes p :: "'a :: semiring_Gcd poly"
eberlm@63498
   591
  obtains p' where "p = smult (content p) p'" "content p' = 1"
eberlm@63498
   592
proof (cases "p = 0")
eberlm@63498
   593
  case True
eberlm@63498
   594
  thus ?thesis by (intro that[of 1]) simp_all
eberlm@63498
   595
next
eberlm@63498
   596
  case False
eberlm@63498
   597
  from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
eberlm@63498
   598
  have "content p * 1 = content p * content r" by (subst r) simp
eberlm@63498
   599
  with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
eberlm@63498
   600
  with r show ?thesis by (intro that[of r]) simp_all
eberlm@63498
   601
qed
eberlm@63498
   602
eberlm@63498
   603
lemma smult_content_normalize_primitive_part [simp]:
eberlm@63498
   604
  "smult (content p) (normalize (primitive_part p)) = normalize p"
eberlm@63498
   605
proof -
eberlm@63498
   606
  have "smult (content p) (normalize (primitive_part p)) = 
eberlm@63498
   607
          normalize ([:content p:] * primitive_part p)" 
eberlm@63498
   608
    by (subst normalize_mult) (simp_all add: normalize_const_poly)
eberlm@63498
   609
  also have "[:content p:] * primitive_part p = p" by simp
eberlm@63498
   610
  finally show ?thesis .
eberlm@63498
   611
qed
eberlm@63498
   612
eberlm@63498
   613
lemma content_dvd_contentI [intro]:
eberlm@63498
   614
  "p dvd q \<Longrightarrow> content p dvd content q"
eberlm@63498
   615
  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
eberlm@63498
   616
  
eberlm@63498
   617
lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
eberlm@63498
   618
  by (simp add: primitive_part_def map_poly_pCons)
eberlm@63498
   619
 
eberlm@63498
   620
lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
eberlm@63498
   621
  by (auto simp: primitive_part_def)
eberlm@63498
   622
  
eberlm@63498
   623
lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
eberlm@63498
   624
proof (cases "p = 0")
eberlm@63498
   625
  case False
eberlm@63498
   626
  have "p = smult (content p) (primitive_part p)" by simp
eberlm@63498
   627
  also from False have "degree \<dots> = degree (primitive_part p)"
eberlm@63498
   628
    by (subst degree_smult_eq) simp_all
eberlm@63498
   629
  finally show ?thesis ..
eberlm@63498
   630
qed simp_all
eberlm@63498
   631
eberlm@63498
   632
eberlm@63498
   633
subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
eberlm@63498
   634
eberlm@63498
   635
abbreviation (input) fract_poly 
eberlm@63498
   636
  where "fract_poly \<equiv> map_poly to_fract"
eberlm@63498
   637
eberlm@63498
   638
abbreviation (input) unfract_poly 
eberlm@63498
   639
  where "unfract_poly \<equiv> map_poly (fst \<circ> quot_of_fract)"
eberlm@63498
   640
  
eberlm@63498
   641
lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)"
eberlm@63498
   642
  by (simp add: smult_conv_map_poly map_poly_map_poly o_def)
eberlm@63498
   643
eberlm@63498
   644
lemma fract_poly_0 [simp]: "fract_poly 0 = 0"
eberlm@63498
   645
  by (simp add: poly_eqI coeff_map_poly)
eberlm@63498
   646
eberlm@63498
   647
lemma fract_poly_1 [simp]: "fract_poly 1 = 1"
eberlm@63498
   648
  by (simp add: one_poly_def map_poly_pCons)
eberlm@63498
   649
eberlm@63498
   650
lemma fract_poly_add [simp]:
eberlm@63498
   651
  "fract_poly (p + q) = fract_poly p + fract_poly q"
eberlm@63498
   652
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
eberlm@63498
   653
eberlm@63498
   654
lemma fract_poly_diff [simp]:
eberlm@63498
   655
  "fract_poly (p - q) = fract_poly p - fract_poly q"
eberlm@63498
   656
  by (intro poly_eqI) (simp_all add: coeff_map_poly)
eberlm@63498
   657
eberlm@63498
   658
lemma to_fract_setsum [simp]: "to_fract (setsum f A) = setsum (\<lambda>x. to_fract (f x)) A"
eberlm@63498
   659
  by (cases "finite A", induction A rule: finite_induct) simp_all 
eberlm@63498
   660
eberlm@63498
   661
lemma fract_poly_mult [simp]:
eberlm@63498
   662
  "fract_poly (p * q) = fract_poly p * fract_poly q"
eberlm@63498
   663
  by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult)
eberlm@63498
   664
eberlm@63498
   665
lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \<longleftrightarrow> p = q"
eberlm@63498
   666
  by (auto simp: poly_eq_iff coeff_map_poly)
eberlm@63498
   667
eberlm@63498
   668
lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \<longleftrightarrow> p = 0"
eberlm@63498
   669
  using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff)
eberlm@63498
   670
eberlm@63498
   671
lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
eberlm@63498
   672
  by (auto elim!: dvdE)
eberlm@63498
   673
eberlm@63498
   674
lemma msetprod_fract_poly: 
eberlm@63498
   675
  "msetprod (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (msetprod (image_mset f A))"
eberlm@63498
   676
  by (induction A) (simp_all add: mult_ac)
eberlm@63498
   677
  
eberlm@63498
   678
lemma is_unit_fract_poly_iff:
eberlm@63498
   679
  "p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
eberlm@63498
   680
proof safe
eberlm@63498
   681
  assume A: "p dvd 1"
eberlm@63498
   682
  with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
eberlm@63498
   683
  from A show "content p = 1"
eberlm@63498
   684
    by (auto simp: is_unit_poly_iff normalize_1_iff)
eberlm@63498
   685
next
eberlm@63498
   686
  assume A: "fract_poly p dvd 1" and B: "content p = 1"
eberlm@63498
   687
  from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)
eberlm@63498
   688
  {
eberlm@63498
   689
    fix n :: nat assume "n > 0"
eberlm@63498
   690
    have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly)
eberlm@63498
   691
    also note c
eberlm@63498
   692
    also from \<open>n > 0\<close> have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits)
eberlm@63498
   693
    finally have "coeff p n = 0" by simp
eberlm@63498
   694
  }
eberlm@63498
   695
  hence "degree p \<le> 0" by (intro degree_le) simp_all
eberlm@63498
   696
  with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE)
eberlm@63498
   697
qed
eberlm@63498
   698
  
eberlm@63498
   699
lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1"
eberlm@63498
   700
  using fract_poly_dvd[of p 1] by simp
eberlm@63498
   701
eberlm@63498
   702
lemma fract_poly_smult_eqE:
eberlm@63498
   703
  fixes c :: "'a :: {idom_divide,ring_gcd} fract"
eberlm@63498
   704
  assumes "fract_poly p = smult c (fract_poly q)"
eberlm@63498
   705
  obtains a b 
eberlm@63498
   706
    where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a"
eberlm@63498
   707
proof -
eberlm@63498
   708
  define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)"
eberlm@63498
   709
  have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)"
eberlm@63498
   710
    by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms)
eberlm@63498
   711
  hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
eberlm@63498
   712
  hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
eberlm@63498
   713
  moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
eberlm@63498
   714
    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
eberlm@63498
   715
          normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
eberlm@63498
   716
  ultimately show ?thesis by (intro that[of a b])
eberlm@63498
   717
qed
eberlm@63498
   718
eberlm@63498
   719
eberlm@63498
   720
subsection \<open>Fractional content\<close>
eberlm@63498
   721
eberlm@63498
   722
abbreviation (input) Lcm_coeff_denoms 
eberlm@63498
   723
    :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a"
eberlm@63498
   724
  where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))"
eberlm@63498
   725
  
eberlm@63498
   726
definition fract_content :: 
eberlm@63498
   727
      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where
eberlm@63498
   728
  "fract_content p = 
eberlm@63498
   729
     (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" 
eberlm@63498
   730
eberlm@63498
   731
definition primitive_part_fract :: 
eberlm@63498
   732
      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where
eberlm@63498
   733
  "primitive_part_fract p = 
eberlm@63498
   734
     primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
eberlm@63498
   735
eberlm@63498
   736
lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0"
eberlm@63498
   737
  by (simp add: primitive_part_fract_def)
eberlm@63498
   738
eberlm@63498
   739
lemma fract_content_eq_0_iff [simp]:
eberlm@63498
   740
  "fract_content p = 0 \<longleftrightarrow> p = 0"
eberlm@63498
   741
  unfolding fract_content_def Let_def Zero_fract_def
eberlm@63498
   742
  by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff)
eberlm@63498
   743
eberlm@63498
   744
lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
eberlm@63498
   745
  unfolding primitive_part_fract_def
eberlm@63498
   746
  by (rule content_primitive_part)
eberlm@63498
   747
     (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)  
eberlm@63498
   748
eberlm@63498
   749
lemma content_times_primitive_part_fract:
eberlm@63498
   750
  "smult (fract_content p) (fract_poly (primitive_part_fract p)) = p"
eberlm@63498
   751
proof -
eberlm@63498
   752
  define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)"
eberlm@63498
   753
  have "fract_poly p' = 
eberlm@63498
   754
          map_poly (to_fract \<circ> fst \<circ> quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)"
eberlm@63498
   755
    unfolding primitive_part_fract_def p'_def 
eberlm@63498
   756
    by (subst map_poly_map_poly) (simp_all add: o_assoc)
eberlm@63498
   757
  also have "\<dots> = smult (to_fract (Lcm_coeff_denoms p)) p"
eberlm@63498
   758
  proof (intro map_poly_idI, unfold o_apply)
eberlm@63498
   759
    fix c assume "c \<in> set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))"
eberlm@63498
   760
    then obtain c' where c: "c' \<in> set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'"
eberlm@63498
   761
      by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits)
eberlm@63498
   762
    note c(2)
eberlm@63498
   763
    also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))"
eberlm@63498
   764
      by simp
eberlm@63498
   765
    also have "to_fract (Lcm_coeff_denoms p) * \<dots> = 
eberlm@63498
   766
                 Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))"
eberlm@63498
   767
      unfolding to_fract_def by (subst mult_fract) simp_all
eberlm@63498
   768
    also have "snd (quot_of_fract \<dots>) = 1"
eberlm@63498
   769
      by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto)
eberlm@63498
   770
    finally show "to_fract (fst (quot_of_fract c)) = c"
eberlm@63498
   771
      by (rule to_fract_quot_of_fract)
eberlm@63498
   772
  qed
eberlm@63498
   773
  also have "p' = smult (content p') (primitive_part p')" 
eberlm@63498
   774
    by (rule content_times_primitive_part [symmetric])
eberlm@63498
   775
  also have "primitive_part p' = primitive_part_fract p"
eberlm@63498
   776
    by (simp add: primitive_part_fract_def p'_def)
eberlm@63498
   777
  also have "fract_poly (smult (content p') (primitive_part_fract p)) = 
eberlm@63498
   778
               smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp
eberlm@63498
   779
  finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) =
eberlm@63498
   780
                      smult (to_fract (Lcm_coeff_denoms p)) p" .
eberlm@63498
   781
  thus ?thesis
eberlm@63498
   782
    by (subst (asm) smult_eq_iff)
eberlm@63498
   783
       (auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def)
eberlm@63498
   784
qed
eberlm@63498
   785
eberlm@63498
   786
lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
eberlm@63498
   787
proof -
eberlm@63498
   788
  have "Lcm_coeff_denoms (fract_poly p) = 1"
eberlm@63498
   789
    by (auto simp: Lcm_1_iff set_coeffs_map_poly)
eberlm@63498
   790
  hence "fract_content (fract_poly p) = 
eberlm@63498
   791
           to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
eberlm@63498
   792
    by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
eberlm@63498
   793
  also have "map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p = p"
eberlm@63498
   794
    by (intro map_poly_idI) simp_all
eberlm@63498
   795
  finally show ?thesis .
eberlm@63498
   796
qed
eberlm@63498
   797
eberlm@63498
   798
lemma content_decompose_fract:
eberlm@63498
   799
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
eberlm@63498
   800
  obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
eberlm@63498
   801
proof (cases "p = 0")
eberlm@63498
   802
  case True
eberlm@63498
   803
  hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all
eberlm@63498
   804
  thus ?thesis ..
eberlm@63498
   805
next
eberlm@63498
   806
  case False
eberlm@63498
   807
  thus ?thesis
eberlm@63498
   808
    by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract])
eberlm@63498
   809
qed
eberlm@63498
   810
eberlm@63498
   811
eberlm@63498
   812
subsection \<open>More properties of content and primitive part\<close>
eberlm@63498
   813
eberlm@63498
   814
lemma lift_prime_elem_poly:
eberlm@63498
   815
  assumes "is_prime_elem (c :: 'a :: semidom)"
eberlm@63498
   816
  shows   "is_prime_elem [:c:]"
eberlm@63498
   817
proof (rule is_prime_elemI)
eberlm@63498
   818
  fix a b assume *: "[:c:] dvd a * b"
eberlm@63498
   819
  from * have dvd: "c dvd coeff (a * b) n" for n
eberlm@63498
   820
    by (subst (asm) const_poly_dvd_iff) blast
eberlm@63498
   821
  {
eberlm@63498
   822
    define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
eberlm@63498
   823
    assume "\<not>[:c:] dvd b"
eberlm@63498
   824
    hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
eberlm@63498
   825
    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i < Suc (degree b)"
eberlm@63498
   826
      by (auto intro: le_degree simp: less_Suc_eq_le)
eberlm@63498
   827
    have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B])
eberlm@63498
   828
    have "i \<le> m" if "\<not>c dvd coeff b i" for i
eberlm@63498
   829
      unfolding m_def by (rule Greatest_le[OF that B])
eberlm@63498
   830
    hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
eberlm@63498
   831
eberlm@63498
   832
    have "c dvd coeff a i" for i
eberlm@63498
   833
    proof (induction i rule: nat_descend_induct[of "degree a"])
eberlm@63498
   834
      case (base i)
eberlm@63498
   835
      thus ?case by (simp add: coeff_eq_0)
eberlm@63498
   836
    next
eberlm@63498
   837
      case (descend i)
eberlm@63498
   838
      let ?A = "{..i+m} - {i}"
eberlm@63498
   839
      have "c dvd coeff (a * b) (i + m)" by (rule dvd)
eberlm@63498
   840
      also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
eberlm@63498
   841
        by (simp add: coeff_mult)
eberlm@63498
   842
      also have "{..i+m} = insert i ?A" by auto
eberlm@63498
   843
      also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
eberlm@63498
   844
                   coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
eberlm@63498
   845
        (is "_ = _ + ?S")
eberlm@63498
   846
        by (subst setsum.insert) simp_all
eberlm@63498
   847
      finally have eq: "c dvd coeff a i * coeff b m + ?S" .
eberlm@63498
   848
      moreover have "c dvd ?S"
eberlm@63498
   849
      proof (rule dvd_setsum)
eberlm@63498
   850
        fix k assume k: "k \<in> {..i+m} - {i}"
eberlm@63498
   851
        show "c dvd coeff a k * coeff b (i + m - k)"
eberlm@63498
   852
        proof (cases "k < i")
eberlm@63498
   853
          case False
eberlm@63498
   854
          with k have "c dvd coeff a k" by (intro descend.IH) simp
eberlm@63498
   855
          thus ?thesis by simp
eberlm@63498
   856
        next
eberlm@63498
   857
          case True
eberlm@63498
   858
          hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
eberlm@63498
   859
          thus ?thesis by simp
eberlm@63498
   860
        qed
eberlm@63498
   861
      qed
eberlm@63498
   862
      ultimately have "c dvd coeff a i * coeff b m"
eberlm@63498
   863
        by (simp add: dvd_add_left_iff)
eberlm@63498
   864
      with assms coeff_m show "c dvd coeff a i"
eberlm@63498
   865
        by (simp add: prime_dvd_mult_iff)
eberlm@63498
   866
    qed
eberlm@63498
   867
    hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
eberlm@63498
   868
  }
eberlm@63498
   869
  thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
eberlm@63498
   870
qed (insert assms, simp_all add: is_prime_elem_def one_poly_def)
eberlm@63498
   871
eberlm@63498
   872
lemma prime_elem_const_poly_iff:
eberlm@63498
   873
  fixes c :: "'a :: semidom"
eberlm@63498
   874
  shows   "is_prime_elem [:c:] \<longleftrightarrow> is_prime_elem c"
eberlm@63498
   875
proof
eberlm@63498
   876
  assume A: "is_prime_elem [:c:]"
eberlm@63498
   877
  show "is_prime_elem c"
eberlm@63498
   878
  proof (rule is_prime_elemI)
eberlm@63498
   879
    fix a b assume "c dvd a * b"
eberlm@63498
   880
    hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
eberlm@63498
   881
    from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_divides_productD)
eberlm@63498
   882
    thus "c dvd a \<or> c dvd b" by simp
eberlm@63498
   883
  qed (insert A, auto simp: is_prime_elem_def is_unit_poly_iff)
eberlm@63498
   884
qed (auto intro: lift_prime_elem_poly)
eberlm@63498
   885
eberlm@63498
   886
context
eberlm@63498
   887
begin
eberlm@63498
   888
eberlm@63498
   889
private lemma content_1_mult:
eberlm@63498
   890
  fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly"
eberlm@63498
   891
  assumes "content f = 1" "content g = 1"
eberlm@63498
   892
  shows   "content (f * g) = 1"
eberlm@63498
   893
proof (cases "f * g = 0")
eberlm@63498
   894
  case False
eberlm@63498
   895
  from assms have "f \<noteq> 0" "g \<noteq> 0" by auto
eberlm@63498
   896
eberlm@63498
   897
  hence "f * g \<noteq> 0" by auto
eberlm@63498
   898
  {
eberlm@63498
   899
    assume "\<not>is_unit (content (f * g))"
eberlm@63498
   900
    with False have "\<exists>p. p dvd content (f * g) \<and> is_prime p"
eberlm@63498
   901
      by (intro prime_divisor_exists) simp_all
eberlm@63498
   902
    then obtain p where "p dvd content (f * g)" "is_prime p" by blast
eberlm@63498
   903
    from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
eberlm@63498
   904
      by (simp add: const_poly_dvd_iff_dvd_content)
eberlm@63498
   905
    moreover from \<open>is_prime p\<close> have "is_prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
eberlm@63498
   906
    ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
eberlm@63498
   907
      by (simp add: prime_dvd_mult_iff)
eberlm@63498
   908
    with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
eberlm@63498
   909
    with \<open>is_prime p\<close> have False by simp
eberlm@63498
   910
  }
eberlm@63498
   911
  hence "is_unit (content (f * g))" by blast
eberlm@63498
   912
  hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
eberlm@63498
   913
  thus ?thesis by simp
eberlm@63498
   914
qed (insert assms, auto)
eberlm@63498
   915
eberlm@63498
   916
lemma content_mult:
eberlm@63498
   917
  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
eberlm@63498
   918
  shows "content (p * q) = content p * content q"
eberlm@63498
   919
proof -
eberlm@63498
   920
  from content_decompose[of p] guess p' . note p = this
eberlm@63498
   921
  from content_decompose[of q] guess q' . note q = this
eberlm@63498
   922
  have "content (p * q) = content p * content q * content (p' * q')"
eberlm@63498
   923
    by (subst p, subst q) (simp add: mult_ac normalize_mult)
eberlm@63498
   924
  also from p q have "content (p' * q') = 1" by (intro content_1_mult)
eberlm@63498
   925
  finally show ?thesis by simp
eberlm@63498
   926
qed
eberlm@63498
   927
eberlm@63498
   928
lemma primitive_part_mult:
eberlm@63498
   929
  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
eberlm@63498
   930
  shows "primitive_part (p * q) = primitive_part p * primitive_part q"
eberlm@63498
   931
proof -
eberlm@63498
   932
  have "primitive_part (p * q) = p * q div [:content (p * q):]"
eberlm@63498
   933
    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
eberlm@63498
   934
  also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
eberlm@63498
   935
    by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
eberlm@63498
   936
  also have "\<dots> = primitive_part p * primitive_part q"
eberlm@63498
   937
    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
eberlm@63498
   938
  finally show ?thesis .
eberlm@63498
   939
qed
eberlm@63498
   940
eberlm@63498
   941
lemma primitive_part_smult:
eberlm@63498
   942
  fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
eberlm@63498
   943
  shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
eberlm@63498
   944
proof -
eberlm@63498
   945
  have "smult a p = [:a:] * p" by simp
eberlm@63498
   946
  also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
eberlm@63498
   947
    by (subst primitive_part_mult) simp_all
eberlm@63498
   948
  finally show ?thesis .
eberlm@63498
   949
qed  
eberlm@63498
   950
eberlm@63498
   951
lemma primitive_part_dvd_primitive_partI [intro]:
eberlm@63498
   952
  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
eberlm@63498
   953
  shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
eberlm@63498
   954
  by (auto elim!: dvdE simp: primitive_part_mult)
eberlm@63498
   955
eberlm@63498
   956
lemma content_msetprod: 
eberlm@63498
   957
  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
eberlm@63498
   958
  shows "content (msetprod A) = msetprod (image_mset content A)"
eberlm@63498
   959
  by (induction A) (simp_all add: content_mult mult_ac)
eberlm@63498
   960
eberlm@63498
   961
lemma fract_poly_dvdD:
eberlm@63498
   962
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
   963
  assumes "fract_poly p dvd fract_poly q" "content p = 1"
eberlm@63498
   964
  shows   "p dvd q"
eberlm@63498
   965
proof -
eberlm@63498
   966
  from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
eberlm@63498
   967
  from content_decompose_fract[of r] guess c r' . note r' = this
eberlm@63498
   968
  from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp  
eberlm@63498
   969
  from fract_poly_smult_eqE[OF this] guess a b . note ab = this
eberlm@63498
   970
  have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
eberlm@63498
   971
  hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
eberlm@63498
   972
  have "1 = gcd a (normalize b)" by (simp add: ab)
eberlm@63498
   973
  also note eq'
eberlm@63498
   974
  also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4))
eberlm@63498
   975
  finally have [simp]: "a = 1" by simp
eberlm@63498
   976
  from eq ab have "q = p * ([:b:] * r')" by simp
eberlm@63498
   977
  thus ?thesis by (rule dvdI)
eberlm@63498
   978
qed
eberlm@63498
   979
eberlm@63498
   980
lemma content_prod_eq_1_iff: 
eberlm@63498
   981
  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
eberlm@63498
   982
  shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
eberlm@63498
   983
proof safe
eberlm@63498
   984
  assume A: "content (p * q) = 1"
eberlm@63498
   985
  {
eberlm@63498
   986
    fix p q :: "'a poly" assume "content p * content q = 1"
eberlm@63498
   987
    hence "1 = content p * content q" by simp
eberlm@63498
   988
    hence "content p dvd 1" by (rule dvdI)
eberlm@63498
   989
    hence "content p = 1" by simp
eberlm@63498
   990
  } note B = this
eberlm@63498
   991
  from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 
eberlm@63498
   992
    by (simp_all add: content_mult mult_ac)
eberlm@63498
   993
qed (auto simp: content_mult)
eberlm@63498
   994
eberlm@63498
   995
end
eberlm@63498
   996
eberlm@63498
   997
eberlm@63498
   998
subsection \<open>Polynomials over a field are a Euclidean ring\<close>
eberlm@63498
   999
eberlm@63498
  1000
context
eberlm@63498
  1001
begin
eberlm@63498
  1002
eberlm@63498
  1003
private definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
eberlm@63498
  1004
  "unit_factor_field_poly p = [:lead_coeff p:]"
eberlm@63498
  1005
eberlm@63498
  1006
private definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
eberlm@63498
  1007
  "normalize_field_poly p = smult (inverse (lead_coeff p)) p"
eberlm@63498
  1008
eberlm@63498
  1009
private definition euclidean_size_field_poly :: "'a :: field poly \<Rightarrow> nat" where
eberlm@63498
  1010
  "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
eberlm@63498
  1011
eberlm@63498
  1012
private lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
eberlm@63498
  1013
    by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
eberlm@63498
  1014
eberlm@63498
  1015
interpretation field_poly: 
eberlm@63498
  1016
  euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly" 
eberlm@63498
  1017
    normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus
eberlm@63498
  1018
proof (standard, unfold dvd_field_poly)
eberlm@63498
  1019
  fix p :: "'a poly"
eberlm@63498
  1020
  show "unit_factor_field_poly p * normalize_field_poly p = p"
eberlm@63498
  1021
    by (cases "p = 0") 
eberlm@63498
  1022
       (simp_all add: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_nonzero)
eberlm@63498
  1023
next
eberlm@63498
  1024
  fix p :: "'a poly" assume "is_unit p"
eberlm@63498
  1025
  thus "normalize_field_poly p = 1"
eberlm@63498
  1026
    by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
eberlm@63498
  1027
next
eberlm@63498
  1028
  fix p :: "'a poly" assume "p \<noteq> 0"
eberlm@63498
  1029
  thus "is_unit (unit_factor_field_poly p)"
eberlm@63498
  1030
    by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
eberlm@63498
  1031
qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
eberlm@63498
  1032
       euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le)
eberlm@63498
  1033
eberlm@63498
  1034
private lemma field_poly_irreducible_imp_prime:
eberlm@63498
  1035
  assumes "irreducible (p :: 'a :: field poly)"
eberlm@63498
  1036
  shows   "is_prime_elem p"
eberlm@63498
  1037
proof -
eberlm@63498
  1038
  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
eberlm@63498
  1039
  from field_poly.irreducible_imp_prime[of p] assms
eberlm@63498
  1040
    show ?thesis unfolding irreducible_def is_prime_elem_def dvd_field_poly
eberlm@63498
  1041
      comm_semiring_1.irreducible_def[OF A] comm_semiring_1.is_prime_elem_def[OF A] by blast
eberlm@63498
  1042
qed
eberlm@63498
  1043
eberlm@63498
  1044
private lemma field_poly_msetprod_prime_factorization:
eberlm@63498
  1045
  assumes "(x :: 'a :: field poly) \<noteq> 0"
eberlm@63498
  1046
  shows   "msetprod (field_poly.prime_factorization x) = normalize_field_poly x"
eberlm@63498
  1047
proof -
eberlm@63498
  1048
  have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
eberlm@63498
  1049
  have "comm_monoid_mult.msetprod op * (1 :: 'a poly) = msetprod"
eberlm@63498
  1050
    by (intro ext) (simp add: comm_monoid_mult.msetprod_def[OF A] msetprod_def)
eberlm@63498
  1051
  with field_poly.msetprod_prime_factorization[OF assms] show ?thesis by simp
eberlm@63498
  1052
qed
eberlm@63498
  1053
eberlm@63498
  1054
private lemma field_poly_in_prime_factorization_imp_prime:
eberlm@63498
  1055
  assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
eberlm@63498
  1056
  shows   "is_prime_elem p"
eberlm@63498
  1057
proof -
eberlm@63498
  1058
  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
eberlm@63498
  1059
  have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
eberlm@63498
  1060
             normalize_field_poly unit_factor_field_poly" ..
eberlm@63498
  1061
  from field_poly.in_prime_factorization_imp_prime[of p x] assms
eberlm@63498
  1062
    show ?thesis unfolding is_prime_elem_def dvd_field_poly
eberlm@63498
  1063
      comm_semiring_1.is_prime_elem_def[OF A] normalization_semidom.is_prime_def[OF B] by blast
eberlm@63498
  1064
qed
eberlm@63498
  1065
eberlm@63498
  1066
eberlm@63498
  1067
subsection \<open>Primality and irreducibility in polynomial rings\<close>
eberlm@63498
  1068
eberlm@63498
  1069
lemma nonconst_poly_irreducible_iff:
eberlm@63498
  1070
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
  1071
  assumes "degree p \<noteq> 0"
eberlm@63498
  1072
  shows   "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
eberlm@63498
  1073
proof safe
eberlm@63498
  1074
  assume p: "irreducible p"
eberlm@63498
  1075
eberlm@63498
  1076
  from content_decompose[of p] guess p' . note p' = this
eberlm@63498
  1077
  hence "p = [:content p:] * p'" by simp
eberlm@63498
  1078
  from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
eberlm@63498
  1079
  moreover have "\<not>p' dvd 1"
eberlm@63498
  1080
  proof
eberlm@63498
  1081
    assume "p' dvd 1"
eberlm@63498
  1082
    hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff)
eberlm@63498
  1083
    with assms show False by contradiction
eberlm@63498
  1084
  qed
eberlm@63498
  1085
  ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff)
eberlm@63498
  1086
  
eberlm@63498
  1087
  show "irreducible (map_poly to_fract p)"
eberlm@63498
  1088
  proof (rule irreducibleI)
eberlm@63498
  1089
    have "fract_poly p = 0 \<longleftrightarrow> p = 0" by (intro map_poly_eq_0_iff) auto
eberlm@63498
  1090
    with assms show "map_poly to_fract p \<noteq> 0" by auto
eberlm@63498
  1091
  next
eberlm@63498
  1092
    show "\<not>is_unit (fract_poly p)"
eberlm@63498
  1093
    proof
eberlm@63498
  1094
      assume "is_unit (map_poly to_fract p)"
eberlm@63498
  1095
      hence "degree (map_poly to_fract p) = 0"
eberlm@63498
  1096
        by (auto simp: is_unit_poly_iff)
eberlm@63498
  1097
      hence "degree p = 0" by (simp add: degree_map_poly)
eberlm@63498
  1098
      with assms show False by contradiction
eberlm@63498
  1099
   qed
eberlm@63498
  1100
 next
eberlm@63498
  1101
   fix q r assume qr: "fract_poly p = q * r"
eberlm@63498
  1102
   from content_decompose_fract[of q] guess cg q' . note q = this
eberlm@63498
  1103
   from content_decompose_fract[of r] guess cr r' . note r = this
eberlm@63498
  1104
   from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
eberlm@63498
  1105
   from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
eberlm@63498
  1106
     by (simp add: q r)
eberlm@63498
  1107
   from fract_poly_smult_eqE[OF this] guess a b . note ab = this
eberlm@63498
  1108
   hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
eberlm@63498
  1109
   with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
eberlm@63498
  1110
   hence "normalize b = gcd a b" by simp
eberlm@63498
  1111
   also from ab(3) have "\<dots> = 1" .
eberlm@63498
  1112
   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
eberlm@63498
  1113
   
eberlm@63498
  1114
   note eq
eberlm@63498
  1115
   also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
eberlm@63498
  1116
   also have "smult \<dots> (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp
eberlm@63498
  1117
   finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult)
eberlm@63498
  1118
   from p and this have "([:b:] * q') dvd 1 \<or> r' dvd 1" by (rule irreducibleD)
eberlm@63498
  1119
   hence "q' dvd 1 \<or> r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left)
eberlm@63498
  1120
   hence "fract_poly q' dvd 1 \<or> fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit)
eberlm@63498
  1121
   with q r show "is_unit q \<or> is_unit r"
eberlm@63498
  1122
     by (auto simp add: is_unit_smult_iff dvd_field_iff nz)
eberlm@63498
  1123
 qed
eberlm@63498
  1124
eberlm@63498
  1125
next
eberlm@63498
  1126
eberlm@63498
  1127
  assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
eberlm@63498
  1128
  show "irreducible p"
eberlm@63498
  1129
  proof (rule irreducibleI)
eberlm@63498
  1130
    from irred show "p \<noteq> 0" by auto
eberlm@63498
  1131
  next
eberlm@63498
  1132
    from irred show "\<not>p dvd 1"
eberlm@63498
  1133
      by (auto simp: irreducible_def dest: fract_poly_is_unit)
eberlm@63498
  1134
  next
eberlm@63498
  1135
    fix q r assume qr: "p = q * r"
eberlm@63498
  1136
    hence "fract_poly p = fract_poly q * fract_poly r" by simp
eberlm@63498
  1137
    from irred and this have "fract_poly q dvd 1 \<or> fract_poly r dvd 1" 
eberlm@63498
  1138
      by (rule irreducibleD)
eberlm@63498
  1139
    with primitive qr show "q dvd 1 \<or> r dvd 1"
eberlm@63498
  1140
      by (auto simp:  content_prod_eq_1_iff is_unit_fract_poly_iff)
eberlm@63498
  1141
  qed
eberlm@63498
  1142
qed
eberlm@63498
  1143
eberlm@63498
  1144
private lemma irreducible_imp_prime_poly:
eberlm@63498
  1145
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
  1146
  assumes "irreducible p"
eberlm@63498
  1147
  shows   "is_prime_elem p"
eberlm@63498
  1148
proof (cases "degree p = 0")
eberlm@63498
  1149
  case True
eberlm@63498
  1150
  with assms show ?thesis
eberlm@63498
  1151
    by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
eberlm@63498
  1152
             intro!: irreducible_imp_prime elim!: degree_eq_zeroE)
eberlm@63498
  1153
next
eberlm@63498
  1154
  case False
eberlm@63498
  1155
  from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
eberlm@63498
  1156
    by (simp_all add: nonconst_poly_irreducible_iff)
eberlm@63498
  1157
  from irred have prime: "is_prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
eberlm@63498
  1158
  show ?thesis
eberlm@63498
  1159
  proof (rule is_prime_elemI)
eberlm@63498
  1160
    fix q r assume "p dvd q * r"
eberlm@63498
  1161
    hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
eberlm@63498
  1162
    hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
eberlm@63498
  1163
    from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
eberlm@63498
  1164
      by (rule prime_divides_productD)
eberlm@63498
  1165
    with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
eberlm@63498
  1166
  qed (insert assms, auto simp: irreducible_def)
eberlm@63498
  1167
qed
eberlm@63498
  1168
eberlm@63498
  1169
eberlm@63498
  1170
lemma degree_primitive_part_fract [simp]:
eberlm@63498
  1171
  "degree (primitive_part_fract p) = degree p"
eberlm@63498
  1172
proof -
eberlm@63498
  1173
  have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))"
eberlm@63498
  1174
    by (simp add: content_times_primitive_part_fract)
eberlm@63498
  1175
  also have "degree \<dots> = degree (primitive_part_fract p)"
eberlm@63498
  1176
    by (auto simp: degree_map_poly)
eberlm@63498
  1177
  finally show ?thesis ..
eberlm@63498
  1178
qed
eberlm@63498
  1179
eberlm@63498
  1180
lemma irreducible_primitive_part_fract:
eberlm@63498
  1181
  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
eberlm@63498
  1182
  assumes "irreducible p"
eberlm@63498
  1183
  shows   "irreducible (primitive_part_fract p)"
eberlm@63498
  1184
proof -
eberlm@63498
  1185
  from assms have deg: "degree (primitive_part_fract p) \<noteq> 0"
eberlm@63498
  1186
    by (intro notI) 
eberlm@63498
  1187
       (auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff)
eberlm@63498
  1188
  hence [simp]: "p \<noteq> 0" by auto
eberlm@63498
  1189
eberlm@63498
  1190
  note \<open>irreducible p\<close>
eberlm@63498
  1191
  also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" 
eberlm@63498
  1192
    by (simp add: content_times_primitive_part_fract)
eberlm@63498
  1193
  also have "irreducible \<dots> \<longleftrightarrow> irreducible (fract_poly (primitive_part_fract p))"
eberlm@63498
  1194
    by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff)
eberlm@63498
  1195
  finally show ?thesis using deg
eberlm@63498
  1196
    by (simp add: nonconst_poly_irreducible_iff)
eberlm@63498
  1197
qed
eberlm@63498
  1198
eberlm@63498
  1199
lemma is_prime_elem_primitive_part_fract:
eberlm@63498
  1200
  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
eberlm@63498
  1201
  shows "irreducible p \<Longrightarrow> is_prime_elem (primitive_part_fract p)"
eberlm@63498
  1202
  by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
eberlm@63498
  1203
eberlm@63498
  1204
lemma irreducible_linear_field_poly:
eberlm@63498
  1205
  fixes a b :: "'a::field"
eberlm@63498
  1206
  assumes "b \<noteq> 0"
eberlm@63498
  1207
  shows "irreducible [:a,b:]"
eberlm@63498
  1208
proof (rule irreducibleI)
eberlm@63498
  1209
  fix p q assume pq: "[:a,b:] = p * q"
eberlm@63498
  1210
  also from this assms have "degree \<dots> = degree p + degree q" 
eberlm@63498
  1211
    by (intro degree_mult_eq) auto
eberlm@63498
  1212
  finally have "degree p = 0 \<or> degree q = 0" using assms by auto
eberlm@63498
  1213
  with assms pq show "is_unit p \<or> is_unit q"
eberlm@63498
  1214
    by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
eberlm@63498
  1215
qed (insert assms, auto simp: is_unit_poly_iff)
eberlm@63498
  1216
eberlm@63498
  1217
lemma is_prime_elem_linear_field_poly:
eberlm@63498
  1218
  "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> is_prime_elem [:a,b:]"
eberlm@63498
  1219
  by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
eberlm@63498
  1220
eberlm@63498
  1221
lemma irreducible_linear_poly:
eberlm@63498
  1222
  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
eberlm@63498
  1223
  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]"
eberlm@63498
  1224
  by (auto intro!: irreducible_linear_field_poly 
eberlm@63498
  1225
           simp:   nonconst_poly_irreducible_iff content_def map_poly_pCons)
eberlm@63498
  1226
eberlm@63498
  1227
lemma is_prime_elem_linear_poly:
eberlm@63498
  1228
  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
eberlm@63498
  1229
  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> is_prime_elem [:a,b:]"
eberlm@63498
  1230
  by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
eberlm@63498
  1231
eberlm@63498
  1232
  
eberlm@63498
  1233
subsection \<open>Prime factorisation of polynomials\<close>   
eberlm@63498
  1234
eberlm@63498
  1235
private lemma poly_prime_factorization_exists_content_1:
eberlm@63498
  1236
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
  1237
  assumes "p \<noteq> 0" "content p = 1"
eberlm@63498
  1238
  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
eberlm@63498
  1239
proof -
eberlm@63498
  1240
  let ?P = "field_poly.prime_factorization (fract_poly p)"
eberlm@63498
  1241
  define c where "c = msetprod (image_mset fract_content ?P)"
eberlm@63498
  1242
  define c' where "c' = c * to_fract (lead_coeff p)"
eberlm@63498
  1243
  define e where "e = msetprod (image_mset primitive_part_fract ?P)"
eberlm@63498
  1244
  define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
eberlm@63498
  1245
  have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 
eberlm@63498
  1246
                      content (primitive_part_fract x))"
eberlm@63498
  1247
    by (simp add: e_def content_msetprod multiset.map_comp o_def)
eberlm@63498
  1248
  also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
eberlm@63498
  1249
    by (intro image_mset_cong content_primitive_part_fract) auto
eberlm@63498
  1250
  finally have content_e: "content e = 1" by (simp add: msetprod_const)    
eberlm@63498
  1251
  
eberlm@63498
  1252
  have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
eberlm@63498
  1253
          normalize_field_poly (fract_poly p)" by simp
eberlm@63498
  1254
  also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 
eberlm@63498
  1255
    by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly)
eberlm@63498
  1256
  also from assms have "normalize_field_poly (fract_poly p) = msetprod ?P" 
eberlm@63498
  1257
    by (subst field_poly_msetprod_prime_factorization) simp_all
eberlm@63498
  1258
  also have "\<dots> = msetprod (image_mset id ?P)" by simp
eberlm@63498
  1259
  also have "image_mset id ?P = 
eberlm@63498
  1260
               image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
eberlm@63498
  1261
    by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
eberlm@63498
  1262
  also have "msetprod \<dots> = smult c (fract_poly e)"
eberlm@63498
  1263
    by (subst msetprod_mult) (simp_all add: msetprod_fract_poly msetprod_const_poly c_def e_def)
eberlm@63498
  1264
  also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
eberlm@63498
  1265
    by (simp add: c'_def)
eberlm@63498
  1266
  finally have eq: "fract_poly p = smult c' (fract_poly e)" .
eberlm@63498
  1267
  also obtain b where b: "c' = to_fract b" "is_unit b"
eberlm@63498
  1268
  proof -
eberlm@63498
  1269
    from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
eberlm@63498
  1270
    from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
eberlm@63498
  1271
    with assms content_e have "a = normalize b" by (simp add: ab(4))
eberlm@63498
  1272
    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
eberlm@63498
  1273
    with ab ab' have "c' = to_fract b" by auto
eberlm@63498
  1274
    from this and \<open>is_unit b\<close> show ?thesis by (rule that)
eberlm@63498
  1275
  qed
eberlm@63498
  1276
  hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp
eberlm@63498
  1277
  finally have "p = smult b e" by (simp only: fract_poly_eq_iff)
eberlm@63498
  1278
  hence "p = [:b:] * e" by simp
eberlm@63498
  1279
  with b have "normalize p = normalize e" 
eberlm@63498
  1280
    by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
eberlm@63498
  1281
  also have "normalize e = msetprod A"
eberlm@63498
  1282
    by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
eberlm@63498
  1283
  finally have "msetprod A = normalize p" ..
eberlm@63498
  1284
  
eberlm@63498
  1285
  have "is_prime_elem p" if "p \<in># A" for p
eberlm@63498
  1286
    using that by (auto simp: A_def is_prime_elem_primitive_part_fract prime_imp_irreducible 
eberlm@63498
  1287
                        dest!: field_poly_in_prime_factorization_imp_prime )
eberlm@63498
  1288
  from this and \<open>msetprod A = normalize p\<close> show ?thesis
eberlm@63498
  1289
    by (intro exI[of _ A]) blast
eberlm@63498
  1290
qed
eberlm@63498
  1291
eberlm@63498
  1292
lemma poly_prime_factorization_exists:
eberlm@63498
  1293
  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
eberlm@63498
  1294
  assumes "p \<noteq> 0"
eberlm@63498
  1295
  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
eberlm@63498
  1296
proof -
eberlm@63498
  1297
  define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
eberlm@63498
  1298
  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
eberlm@63498
  1299
    by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
eberlm@63498
  1300
  then guess A by (elim exE conjE) note A = this
eberlm@63498
  1301
  moreover from assms have "msetprod B = [:content p:]"
eberlm@63498
  1302
    by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
eberlm@63498
  1303
  moreover have "\<forall>p. p \<in># B \<longrightarrow> is_prime_elem p"
eberlm@63498
  1304
    by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
eberlm@63498
  1305
  ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
eberlm@63498
  1306
qed
eberlm@63498
  1307
eberlm@63498
  1308
end
eberlm@63498
  1309
eberlm@63498
  1310
eberlm@63498
  1311
subsection \<open>Typeclass instances\<close>
eberlm@63498
  1312
eberlm@63498
  1313
instance poly :: (factorial_ring_gcd) factorial_semiring
eberlm@63498
  1314
  by standard (rule poly_prime_factorization_exists)  
eberlm@63498
  1315
eberlm@63498
  1316
instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
eberlm@63498
  1317
begin
eberlm@63498
  1318
eberlm@63498
  1319
definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
eberlm@63498
  1320
  [code del]: "gcd_poly = gcd_factorial"
eberlm@63498
  1321
eberlm@63498
  1322
definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
eberlm@63498
  1323
  [code del]: "lcm_poly = lcm_factorial"
eberlm@63498
  1324
  
eberlm@63498
  1325
definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
eberlm@63498
  1326
 [code del]: "Gcd_poly = Gcd_factorial"
eberlm@63498
  1327
eberlm@63498
  1328
definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
eberlm@63498
  1329
 [code del]: "Lcm_poly = Lcm_factorial"
eberlm@63498
  1330
 
eberlm@63498
  1331
instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
eberlm@63498
  1332
eberlm@63498
  1333
end
eberlm@63498
  1334
eberlm@63498
  1335
instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring
eberlm@63498
  1336
begin
eberlm@63498
  1337
eberlm@63498
  1338
definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" where
eberlm@63498
  1339
  "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
eberlm@63498
  1340
eberlm@63498
  1341
instance 
eberlm@63498
  1342
  by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le)
eberlm@63498
  1343
end
eberlm@63498
  1344
eberlm@63499
  1345
eberlm@63498
  1346
instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
eberlm@63498
  1347
  by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
eberlm@63498
  1348
eberlm@63498
  1349
  
eberlm@63498
  1350
subsection \<open>Polynomial GCD\<close>
eberlm@63498
  1351
eberlm@63498
  1352
lemma gcd_poly_decompose:
eberlm@63498
  1353
  fixes p q :: "'a :: factorial_ring_gcd poly"
eberlm@63498
  1354
  shows "gcd p q = 
eberlm@63498
  1355
           smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
eberlm@63498
  1356
proof (rule sym, rule gcdI)
eberlm@63498
  1357
  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
eberlm@63498
  1358
          [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all
eberlm@63498
  1359
  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p"
eberlm@63498
  1360
    by simp
eberlm@63498
  1361
next
eberlm@63498
  1362
  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
eberlm@63498
  1363
          [:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all
eberlm@63498
  1364
  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q"
eberlm@63498
  1365
    by simp
eberlm@63498
  1366
next
eberlm@63498
  1367
  fix d assume "d dvd p" "d dvd q"
eberlm@63498
  1368
  hence "[:content d:] * primitive_part d dvd 
eberlm@63498
  1369
           [:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)"
eberlm@63498
  1370
    by (intro mult_dvd_mono) auto
eberlm@63498
  1371
  thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
eberlm@63498
  1372
    by simp
eberlm@63498
  1373
qed (auto simp: normalize_smult)
eberlm@63498
  1374
  
eberlm@63498
  1375
eberlm@63498
  1376
lemma gcd_poly_pseudo_mod:
eberlm@63498
  1377
  fixes p q :: "'a :: factorial_ring_gcd poly"
eberlm@63498
  1378
  assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1"
eberlm@63498
  1379
  shows   "gcd p q = gcd q (primitive_part (pseudo_mod p q))"
eberlm@63498
  1380
proof -
eberlm@63498
  1381
  define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)"
eberlm@63498
  1382
  define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]"
eberlm@63498
  1383
  have [simp]: "primitive_part a = unit_factor a"
eberlm@63498
  1384
    by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0)
eberlm@63498
  1385
  from nz have [simp]: "a \<noteq> 0" by (auto simp: a_def)
eberlm@63498
  1386
  
eberlm@63498
  1387
  have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def)
eberlm@63498
  1388
  have "gcd (q * r + s) q = gcd q s"
eberlm@63498
  1389
    using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac)
eberlm@63498
  1390
  with pseudo_divmod(1)[OF nz rs]
eberlm@63498
  1391
    have "gcd (p * a) q = gcd q s" by (simp add: a_def)
eberlm@63498
  1392
  also from prim have "gcd (p * a) q = gcd p q"
eberlm@63498
  1393
    by (subst gcd_poly_decompose)
eberlm@63498
  1394
       (auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim 
eberlm@63498
  1395
             simp del: mult_pCons_right )
eberlm@63498
  1396
  also from prim have "gcd q s = gcd q (primitive_part s)"
eberlm@63498
  1397
    by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim)
eberlm@63498
  1398
  also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def)
eberlm@63498
  1399
  finally show ?thesis .
eberlm@63498
  1400
qed
eberlm@63498
  1401
eberlm@63498
  1402
lemma degree_pseudo_mod_less:
eberlm@63498
  1403
  assumes "q \<noteq> 0" "pseudo_mod p q \<noteq> 0"
eberlm@63498
  1404
  shows   "degree (pseudo_mod p q) < degree q"
eberlm@63498
  1405
  using pseudo_mod(2)[of q p] assms by auto
eberlm@63498
  1406
eberlm@63498
  1407
function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
eberlm@63498
  1408
  "gcd_poly_code_aux p q = 
eberlm@63498
  1409
     (if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" 
eberlm@63498
  1410
by auto
eberlm@63498
  1411
termination
eberlm@63498
  1412
  by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
eberlm@63498
  1413
     (auto simp: degree_primitive_part degree_pseudo_mod_less)
eberlm@63498
  1414
eberlm@63498
  1415
declare gcd_poly_code_aux.simps [simp del]
eberlm@63498
  1416
eberlm@63498
  1417
lemma gcd_poly_code_aux_correct:
eberlm@63498
  1418
  assumes "content p = 1" "q = 0 \<or> content q = 1"
eberlm@63498
  1419
  shows   "gcd_poly_code_aux p q = gcd p q"
eberlm@63498
  1420
  using assms
eberlm@63498
  1421
proof (induction p q rule: gcd_poly_code_aux.induct)
eberlm@63498
  1422
  case (1 p q)
eberlm@63498
  1423
  show ?case
eberlm@63498
  1424
  proof (cases "q = 0")
eberlm@63498
  1425
    case True
eberlm@63498
  1426
    thus ?thesis by (subst gcd_poly_code_aux.simps) auto
eberlm@63498
  1427
  next
eberlm@63498
  1428
    case False
eberlm@63498
  1429
    hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))"
eberlm@63498
  1430
      by (subst gcd_poly_code_aux.simps) simp_all
eberlm@63498
  1431
    also from "1.prems" False 
eberlm@63498
  1432
      have "primitive_part (pseudo_mod p q) = 0 \<or> 
eberlm@63498
  1433
              content (primitive_part (pseudo_mod p q)) = 1"
eberlm@63498
  1434
      by (cases "pseudo_mod p q = 0") auto
eberlm@63498
  1435
    with "1.prems" False 
eberlm@63498
  1436
      have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = 
eberlm@63498
  1437
              gcd q (primitive_part (pseudo_mod p q))"
eberlm@63498
  1438
      by (intro 1) simp_all
eberlm@63498
  1439
    also from "1.prems" False 
eberlm@63498
  1440
      have "\<dots> = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto
eberlm@63498
  1441
    finally show ?thesis .
eberlm@63498
  1442
  qed
eberlm@63498
  1443
qed
eberlm@63498
  1444
eberlm@63498
  1445
definition gcd_poly_code 
eberlm@63498
  1446
    :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
eberlm@63498
  1447
  where "gcd_poly_code p q = 
eberlm@63498
  1448
           (if p = 0 then normalize q else if q = 0 then normalize p else
eberlm@63498
  1449
              smult (gcd (content p) (content q)) 
eberlm@63498
  1450
                (gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
eberlm@63498
  1451
eberlm@63498
  1452
lemma lcm_poly_code [code]: 
eberlm@63498
  1453
  fixes p q :: "'a :: factorial_ring_gcd poly"
eberlm@63498
  1454
  shows "lcm p q = normalize (p * q) div gcd p q"
eberlm@63498
  1455
  by (rule lcm_gcd)
eberlm@63498
  1456
eberlm@63498
  1457
lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
eberlm@63498
  1458
  by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
eberlm@63498
  1459
eberlm@63498
  1460
declare Gcd_set
eberlm@63498
  1461
  [where ?'a = "'a :: factorial_ring_gcd poly", code]
eberlm@63498
  1462
eberlm@63498
  1463
declare Lcm_set
eberlm@63498
  1464
  [where ?'a = "'a :: factorial_ring_gcd poly", code]
eberlm@63498
  1465
  
eberlm@63498
  1466
value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
eberlm@63498
  1467
eberlm@63498
  1468
end