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