restructured matter on polynomials and normalized fractions
authorhaftmann
Sat Dec 17 15:22:13 2016 +0100 (2016-12-17)
changeset 64591240a39af9ec4
parent 64590 6621d91d3c8a
child 64592 7759f1766189
restructured matter on polynomials and normalized fractions
src/HOL/Fields.thy
src/HOL/Fun_Def.thy
src/HOL/GCD.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Field_as_Ring.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Normalized_Fraction.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/ROOT
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Fields.thy	Sat Dec 17 15:22:13 2016 +0100
     1.2 +++ b/src/HOL/Fields.thy	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -506,6 +506,21 @@
     1.4    "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
     1.5    by (simp add: add_divide_distrib add.commute)
     1.6  
     1.7 +lemma dvd_field_iff:
     1.8 +  "a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)"
     1.9 +proof (cases "a = 0")
    1.10 +  case True
    1.11 +  then show ?thesis
    1.12 +    by simp
    1.13 +next
    1.14 +  case False
    1.15 +  then have "b = a * (b / a)"
    1.16 +    by (simp add: field_simps)
    1.17 +  then have "a dvd b" ..
    1.18 +  with False show ?thesis
    1.19 +    by simp
    1.20 +qed
    1.21 +
    1.22  end
    1.23  
    1.24  class field_char_0 = field + ring_char_0
     2.1 --- a/src/HOL/Fun_Def.thy	Sat Dec 17 15:22:13 2016 +0100
     2.2 +++ b/src/HOL/Fun_Def.thy	Sat Dec 17 15:22:13 2016 +0100
     2.3 @@ -278,6 +278,16 @@
     2.4    done
     2.5  
     2.6  
     2.7 +subsection \<open>Yet another induction principle on the natural numbers\<close>
     2.8 +
     2.9 +lemma nat_descend_induct [case_names base descend]:
    2.10 +  fixes P :: "nat \<Rightarrow> bool"
    2.11 +  assumes H1: "\<And>k. k > n \<Longrightarrow> P k"
    2.12 +  assumes H2: "\<And>k. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
    2.13 +  shows "P m"
    2.14 +  using assms by induction_schema (force intro!: wf_measure [of "\<lambda>k. Suc n - k"])+
    2.15 +
    2.16 +
    2.17  subsection \<open>Tool setup\<close>
    2.18  
    2.19  ML_file "Tools/Function/termination.ML"
     3.1 --- a/src/HOL/GCD.thy	Sat Dec 17 15:22:13 2016 +0100
     3.2 +++ b/src/HOL/GCD.thy	Sat Dec 17 15:22:13 2016 +0100
     3.3 @@ -639,7 +639,6 @@
     3.4      using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
     3.5  qed
     3.6  
     3.7 -
     3.8  lemma divides_mult:
     3.9    assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
    3.10    shows "a * b dvd c"
    3.11 @@ -695,6 +694,10 @@
    3.12    using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
    3.13    by blast
    3.14  
    3.15 +lemma coprime_mul_eq':
    3.16 +  "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
    3.17 +  using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
    3.18 +
    3.19  lemma gcd_coprime:
    3.20    assumes c: "gcd a b \<noteq> 0"
    3.21      and a: "a = a' * gcd a b"
    3.22 @@ -958,6 +961,24 @@
    3.23    ultimately show ?thesis by (rule that)
    3.24  qed
    3.25  
    3.26 +lemma coprime_crossproduct':
    3.27 +  fixes a b c d
    3.28 +  assumes "b \<noteq> 0"
    3.29 +  assumes unit_factors: "unit_factor b = unit_factor d"
    3.30 +  assumes coprime: "coprime a b" "coprime c d"
    3.31 +  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
    3.32 +proof safe
    3.33 +  assume eq: "a * d = b * c"
    3.34 +  hence "normalize a * normalize d = normalize c * normalize b"
    3.35 +    by (simp only: normalize_mult [symmetric] mult_ac)
    3.36 +  with coprime have "normalize b = normalize d"
    3.37 +    by (subst (asm) coprime_crossproduct) simp_all
    3.38 +  from this and unit_factors show "b = d"
    3.39 +    by (rule normalize_unit_factor_eqI)
    3.40 +  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
    3.41 +  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
    3.42 +qed (simp_all add: mult_ac)
    3.43 +
    3.44  end
    3.45  
    3.46  class ring_gcd = comm_ring_1 + semiring_gcd
     4.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Dec 17 15:22:13 2016 +0100
     4.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Dec 17 15:22:13 2016 +0100
     4.3 @@ -657,6 +657,12 @@
     4.4    for x :: nat
     4.5    unfolding Greatest_def by (rule GreatestM_nat_le) auto
     4.6  
     4.7 +lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
     4.8 +  apply (erule exE)
     4.9 +  apply (rule GreatestI)
    4.10 +   apply assumption+
    4.11 +  done
    4.12 +
    4.13  
    4.14  subsection \<open>An aside: bounded accessible part\<close>
    4.15  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Field_as_Ring.thy	Sat Dec 17 15:22:13 2016 +0100
     5.3 @@ -0,0 +1,108 @@
     5.4 +(*  Title:      HOL/Library/Field_as_Ring.thy
     5.5 +    Author:     Manuel Eberl
     5.6 +*)
     5.7 +
     5.8 +theory Field_as_Ring
     5.9 +imports 
    5.10 +  Complex_Main
    5.11 +  "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
    5.12 +begin
    5.13 +
    5.14 +context field
    5.15 +begin
    5.16 +
    5.17 +subclass idom_divide ..
    5.18 +
    5.19 +definition normalize_field :: "'a \<Rightarrow> 'a" 
    5.20 +  where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
    5.21 +definition unit_factor_field :: "'a \<Rightarrow> 'a" 
    5.22 +  where [simp]: "unit_factor_field x = x"
    5.23 +definition euclidean_size_field :: "'a \<Rightarrow> nat" 
    5.24 +  where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
    5.25 +definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    5.26 +  where [simp]: "mod_field x y = (if y = 0 then x else 0)"
    5.27 +
    5.28 +end
    5.29 +
    5.30 +instantiation real :: euclidean_ring
    5.31 +begin
    5.32 +
    5.33 +definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    5.34 +definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
    5.35 +definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
    5.36 +definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
    5.37 +
    5.38 +instance by standard (simp_all add: dvd_field_iff divide_simps)
    5.39 +end
    5.40 +
    5.41 +instantiation real :: euclidean_ring_gcd
    5.42 +begin
    5.43 +
    5.44 +definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    5.45 +  "gcd_real = gcd_eucl"
    5.46 +definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    5.47 +  "lcm_real = lcm_eucl"
    5.48 +definition Gcd_real :: "real set \<Rightarrow> real" where
    5.49 + "Gcd_real = Gcd_eucl"
    5.50 +definition Lcm_real :: "real set \<Rightarrow> real" where
    5.51 + "Lcm_real = Lcm_eucl"
    5.52 +
    5.53 +instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
    5.54 +
    5.55 +end
    5.56 +
    5.57 +instantiation rat :: euclidean_ring
    5.58 +begin
    5.59 +
    5.60 +definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    5.61 +definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
    5.62 +definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
    5.63 +definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
    5.64 +
    5.65 +instance by standard (simp_all add: dvd_field_iff divide_simps)
    5.66 +end
    5.67 +
    5.68 +instantiation rat :: euclidean_ring_gcd
    5.69 +begin
    5.70 +
    5.71 +definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
    5.72 +  "gcd_rat = gcd_eucl"
    5.73 +definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
    5.74 +  "lcm_rat = lcm_eucl"
    5.75 +definition Gcd_rat :: "rat set \<Rightarrow> rat" where
    5.76 + "Gcd_rat = Gcd_eucl"
    5.77 +definition Lcm_rat :: "rat set \<Rightarrow> rat" where
    5.78 + "Lcm_rat = Lcm_eucl"
    5.79 +
    5.80 +instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
    5.81 +
    5.82 +end
    5.83 +
    5.84 +instantiation complex :: euclidean_ring
    5.85 +begin
    5.86 +
    5.87 +definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
    5.88 +definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
    5.89 +definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
    5.90 +definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
    5.91 +
    5.92 +instance by standard (simp_all add: dvd_field_iff divide_simps)
    5.93 +end
    5.94 +
    5.95 +instantiation complex :: euclidean_ring_gcd
    5.96 +begin
    5.97 +
    5.98 +definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
    5.99 +  "gcd_complex = gcd_eucl"
   5.100 +definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   5.101 +  "lcm_complex = lcm_eucl"
   5.102 +definition Gcd_complex :: "complex set \<Rightarrow> complex" where
   5.103 + "Gcd_complex = Gcd_eucl"
   5.104 +definition Lcm_complex :: "complex set \<Rightarrow> complex" where
   5.105 + "Lcm_complex = Lcm_eucl"
   5.106 +
   5.107 +instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
   5.108 +
   5.109 +end
   5.110 +
   5.111 +end
     6.1 --- a/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:13 2016 +0100
     6.2 +++ b/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:13 2016 +0100
     6.3 @@ -1738,6 +1738,10 @@
     6.4    "(\<forall>x y. (x, y) \<in># M \<longrightarrow> f x y = g x y) \<Longrightarrow> {#f x y. (x, y) \<in># M#} = {#g x y. (x, y) \<in># M#}"
     6.5    by (metis image_mset_cong split_cong)
     6.6  
     6.7 +lemma image_mset_const_eq:
     6.8 +  "{#c. a \<in># M#} = replicate_mset (size M) c"
     6.9 +  by (induct M) simp_all
    6.10 +
    6.11  
    6.12  subsection \<open>Further conversions\<close>
    6.13  
    6.14 @@ -2310,6 +2314,9 @@
    6.15  translations
    6.16    "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
    6.17  
    6.18 +lemma prod_mset_constant [simp]: "(\<Prod>_\<in>#A. c) = c ^ size A"
    6.19 +  by (simp add: image_mset_const_eq)
    6.20 +
    6.21  lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
    6.22    assumes "A \<subseteq># B"
    6.23    shows   "prod_mset A dvd prod_mset B"
     7.1 --- a/src/HOL/Library/Normalized_Fraction.thy	Sat Dec 17 15:22:13 2016 +0100
     7.2 +++ b/src/HOL/Library/Normalized_Fraction.thy	Sat Dec 17 15:22:13 2016 +0100
     7.3 @@ -1,3 +1,7 @@
     7.4 +(*  Title:      HOL/Library/Normalized_Fraction.thy
     7.5 +    Author:     Manuel Eberl
     7.6 +*)
     7.7 +
     7.8  theory Normalized_Fraction
     7.9  imports 
    7.10    Main 
    7.11 @@ -5,75 +9,6 @@
    7.12    "~~/src/HOL/Library/Fraction_Field"
    7.13  begin
    7.14  
    7.15 -lemma dvd_neg_div': "y dvd (x :: 'a :: idom_divide) \<Longrightarrow> -x div y = - (x div y)"
    7.16 -apply (case_tac "y = 0") apply simp
    7.17 -apply (auto simp add: dvd_def)
    7.18 -apply (subgoal_tac "-(y * k) = y * - k")
    7.19 -apply (simp only:)
    7.20 -apply (erule nonzero_mult_div_cancel_left)
    7.21 -apply simp
    7.22 -done
    7.23 -
    7.24 -(* TODO Move *)
    7.25 -lemma (in semiring_gcd) coprime_mul_eq': "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
    7.26 -  using coprime_mul_eq[of d a b] by (simp add: gcd.commute)
    7.27 -
    7.28 -lemma dvd_div_eq_0_iff:
    7.29 -  assumes "b dvd (a :: 'a :: semidom_divide)"
    7.30 -  shows   "a div b = 0 \<longleftrightarrow> a = 0"
    7.31 -  using assms by (elim dvdE, cases "b = 0") simp_all  
    7.32 -
    7.33 -lemma dvd_div_eq_0_iff':
    7.34 -  assumes "b dvd (a :: 'a :: semiring_div)"
    7.35 -  shows   "a div b = 0 \<longleftrightarrow> a = 0"
    7.36 -  using assms by (elim dvdE, cases "b = 0") simp_all
    7.37 -
    7.38 -lemma unit_div_eq_0_iff:
    7.39 -  assumes "is_unit (b :: 'a :: {algebraic_semidom,semidom_divide})"
    7.40 -  shows   "a div b = 0 \<longleftrightarrow> a = 0"
    7.41 -  by (rule dvd_div_eq_0_iff) (insert assms, auto)  
    7.42 -
    7.43 -lemma unit_div_eq_0_iff':
    7.44 -  assumes "is_unit (b :: 'a :: semiring_div)"
    7.45 -  shows   "a div b = 0 \<longleftrightarrow> a = 0"
    7.46 -  by (rule dvd_div_eq_0_iff) (insert assms, auto)
    7.47 -
    7.48 -lemma dvd_div_eq_cancel:
    7.49 -  "a div c = b div c \<Longrightarrow> (c :: 'a :: semiring_div) dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
    7.50 -  by (elim dvdE, cases "c = 0") simp_all
    7.51 -
    7.52 -lemma dvd_div_eq_iff:
    7.53 -  "(c :: 'a :: semiring_div) dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
    7.54 -  by (elim dvdE, cases "c = 0") simp_all
    7.55 -
    7.56 -lemma normalize_imp_eq:
    7.57 -  "normalize a = normalize b \<Longrightarrow> unit_factor a = unit_factor b \<Longrightarrow> a = b"
    7.58 -  by (cases "a = 0 \<or> b = 0")
    7.59 -     (auto simp add: div_unit_factor [symmetric] unit_div_cancel simp del: div_unit_factor)
    7.60 -    
    7.61 -lemma coprime_crossproduct':
    7.62 -  fixes a b c d :: "'a :: semiring_gcd"
    7.63 -  assumes nz: "b \<noteq> 0"
    7.64 -  assumes unit_factors: "unit_factor b = unit_factor d"
    7.65 -  assumes coprime: "coprime a b" "coprime c d"
    7.66 -  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
    7.67 -proof safe
    7.68 -  assume eq: "a * d = b * c"
    7.69 -  hence "normalize a * normalize d = normalize c * normalize b"
    7.70 -    by (simp only: normalize_mult [symmetric] mult_ac)
    7.71 -  with coprime have "normalize b = normalize d"
    7.72 -    by (subst (asm) coprime_crossproduct) simp_all
    7.73 -  from this and unit_factors show "b = d" by (rule normalize_imp_eq)
    7.74 -  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
    7.75 -  with nz \<open>b = d\<close> show "a = c" by simp
    7.76 -qed (simp_all add: mult_ac)
    7.77 -  
    7.78 -     
    7.79 -lemma div_mult_unit2: "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
    7.80 -  by (subst dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
    7.81 -(* END TODO *)
    7.82 -
    7.83 -
    7.84  definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where
    7.85    "quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)"
    7.86  
     8.1 --- a/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:13 2016 +0100
     8.2 +++ b/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:13 2016 +0100
     8.3 @@ -877,7 +877,7 @@
     8.4    by (induct n, simp add: monom_0, simp add: monom_Suc)
     8.5  
     8.6  lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)"
     8.7 -  by (auto simp add: poly_eq_iff coeff_Poly_eq nth_default_def)
     8.8 +  by (auto simp add: poly_eq_iff nth_default_def)
     8.9  
    8.10  lemma degree_smult_eq [simp]:
    8.11    fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
    8.12 @@ -1064,6 +1064,111 @@
    8.13      by (rule le_trans[OF degree_mult_le], insert insert, auto)
    8.14  qed simp
    8.15  
    8.16 +
    8.17 +subsection \<open>Mapping polynomials\<close>
    8.18 +
    8.19 +definition map_poly 
    8.20 +     :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
    8.21 +  "map_poly f p = Poly (map f (coeffs p))"
    8.22 +
    8.23 +lemma map_poly_0 [simp]: "map_poly f 0 = 0"
    8.24 +  by (simp add: map_poly_def)
    8.25 +
    8.26 +lemma map_poly_1: "map_poly f 1 = [:f 1:]"
    8.27 +  by (simp add: map_poly_def)
    8.28 +
    8.29 +lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
    8.30 +  by (simp add: map_poly_def one_poly_def)
    8.31 +
    8.32 +lemma coeff_map_poly:
    8.33 +  assumes "f 0 = 0"
    8.34 +  shows   "coeff (map_poly f p) n = f (coeff p n)"
    8.35 +  by (auto simp: map_poly_def nth_default_def coeffs_def assms
    8.36 +        not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
    8.37 +
    8.38 +lemma coeffs_map_poly [code abstract]: 
    8.39 +    "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
    8.40 +  by (simp add: map_poly_def)
    8.41 +
    8.42 +lemma set_coeffs_map_poly:
    8.43 +  "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
    8.44 +  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
    8.45 +
    8.46 +lemma coeffs_map_poly': 
    8.47 +  assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
    8.48 +  shows   "coeffs (map_poly f p) = map f (coeffs p)"
    8.49 +  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 
    8.50 +                           intro!: strip_while_not_last split: if_splits)
    8.51 +
    8.52 +lemma degree_map_poly:
    8.53 +  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
    8.54 +  shows   "degree (map_poly f p) = degree p"
    8.55 +  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
    8.56 +
    8.57 +lemma map_poly_eq_0_iff:
    8.58 +  assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
    8.59 +  shows   "map_poly f p = 0 \<longleftrightarrow> p = 0"
    8.60 +proof -
    8.61 +  {
    8.62 +    fix n :: nat
    8.63 +    have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
    8.64 +    also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
    8.65 +    proof (cases "n < length (coeffs p)")
    8.66 +      case True
    8.67 +      hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
    8.68 +      with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
    8.69 +    qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
    8.70 +    finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
    8.71 +  }
    8.72 +  thus ?thesis by (auto simp: poly_eq_iff)
    8.73 +qed
    8.74 +
    8.75 +lemma map_poly_smult:
    8.76 +  assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
    8.77 +  shows   "map_poly f (smult c p) = smult (f c) (map_poly f p)"
    8.78 +  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
    8.79 +
    8.80 +lemma map_poly_pCons:
    8.81 +  assumes "f 0 = 0"
    8.82 +  shows   "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
    8.83 +  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
    8.84 +
    8.85 +lemma map_poly_map_poly:
    8.86 +  assumes "f 0 = 0" "g 0 = 0"
    8.87 +  shows   "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
    8.88 +  by (intro poly_eqI) (simp add: coeff_map_poly assms)
    8.89 +
    8.90 +lemma map_poly_id [simp]: "map_poly id p = p"
    8.91 +  by (simp add: map_poly_def)
    8.92 +
    8.93 +lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
    8.94 +  by (simp add: map_poly_def)
    8.95 +
    8.96 +lemma map_poly_cong: 
    8.97 +  assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
    8.98 +  shows   "map_poly f p = map_poly g p"
    8.99 +proof -
   8.100 +  from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
   8.101 +  thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
   8.102 +qed
   8.103 +
   8.104 +lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
   8.105 +  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   8.106 +
   8.107 +lemma map_poly_idI:
   8.108 +  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
   8.109 +  shows   "map_poly f p = p"
   8.110 +  using map_poly_cong[OF assms, of _ id] by simp
   8.111 +
   8.112 +lemma map_poly_idI':
   8.113 +  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
   8.114 +  shows   "p = map_poly f p"
   8.115 +  using map_poly_cong[OF assms, of _ id] by simp
   8.116 +
   8.117 +lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
   8.118 +  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   8.119 +
   8.120 +
   8.121  subsection \<open>Conversions from natural numbers\<close>
   8.122  
   8.123  lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
   8.124 @@ -1086,6 +1191,7 @@
   8.125  lemma numeral_poly: "numeral n = [:numeral n:]"
   8.126    by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
   8.127  
   8.128 +
   8.129  subsection \<open>Lemmas about divisibility\<close>
   8.130  
   8.131  lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
   8.132 @@ -1137,6 +1243,11 @@
   8.133  apply (simp add: coeff_mult_degree_sum)
   8.134  done
   8.135  
   8.136 +lemma degree_mult_eq_0:
   8.137 +  fixes p q:: "'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
   8.138 +  shows "degree (p * q) = 0 \<longleftrightarrow> p = 0 \<or> q = 0 \<or> (p \<noteq> 0 \<and> q \<noteq> 0 \<and> degree p = 0 \<and> degree q = 0)"
   8.139 +  by (auto simp add: degree_mult_eq)
   8.140 +
   8.141  lemma degree_mult_right_le:
   8.142    fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   8.143    assumes "q \<noteq> 0"
   8.144 @@ -1290,6 +1401,75 @@
   8.145  text \<open>TODO: Simplification rules for comparisons\<close>
   8.146  
   8.147  
   8.148 +subsection \<open>Leading coefficient\<close>
   8.149 +
   8.150 +definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
   8.151 +  "lead_coeff p= coeff p (degree p)"
   8.152 +
   8.153 +lemma lead_coeff_pCons[simp]:
   8.154 +    "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
   8.155 +    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
   8.156 +unfolding lead_coeff_def by auto
   8.157 +
   8.158 +lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
   8.159 +  unfolding lead_coeff_def by auto
   8.160 +
   8.161 +lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
   8.162 +  by (induction xs) (simp_all add: coeff_mult)
   8.163 +
   8.164 +lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
   8.165 +  by (induction n) (simp_all add: coeff_mult)
   8.166 +
   8.167 +lemma lead_coeff_mult:
   8.168 +   fixes p q::"'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
   8.169 +   shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
   8.170 +by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)
   8.171 +
   8.172 +lemma lead_coeff_add_le:
   8.173 +  assumes "degree p < degree q"
   8.174 +  shows "lead_coeff (p+q) = lead_coeff q" 
   8.175 +using assms unfolding lead_coeff_def
   8.176 +by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
   8.177 +
   8.178 +lemma lead_coeff_minus:
   8.179 +  "lead_coeff (-p) = - lead_coeff p"
   8.180 +by (metis coeff_minus degree_minus lead_coeff_def)
   8.181 +
   8.182 +lemma lead_coeff_smult:
   8.183 +  "lead_coeff (smult c p :: 'a :: {comm_semiring_0,semiring_no_zero_divisors} poly) = c * lead_coeff p"
   8.184 +proof -
   8.185 +  have "smult c p = [:c:] * p" by simp
   8.186 +  also have "lead_coeff \<dots> = c * lead_coeff p"
   8.187 +    by (subst lead_coeff_mult) simp_all
   8.188 +  finally show ?thesis .
   8.189 +qed
   8.190 +
   8.191 +lemma lead_coeff_eq_zero_iff [simp]: "lead_coeff p = 0 \<longleftrightarrow> p = 0"
   8.192 +  by (simp add: lead_coeff_def)
   8.193 +
   8.194 +lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
   8.195 +  by (simp add: lead_coeff_def)
   8.196 +
   8.197 +lemma lead_coeff_of_nat [simp]:
   8.198 +  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
   8.199 +  by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
   8.200 +
   8.201 +lemma lead_coeff_numeral [simp]: 
   8.202 +  "lead_coeff (numeral n) = numeral n"
   8.203 +  unfolding lead_coeff_def
   8.204 +  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
   8.205 +
   8.206 +lemma lead_coeff_power: 
   8.207 +  "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
   8.208 +  by (induction n) (simp_all add: lead_coeff_mult)
   8.209 +
   8.210 +lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
   8.211 +  by (simp add: lead_coeff_def)
   8.212 +
   8.213 +lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
   8.214 +  by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
   8.215 +
   8.216 +
   8.217  subsection \<open>Synthetic division and polynomial roots\<close>
   8.218  
   8.219  text \<open>
   8.220 @@ -1555,7 +1735,7 @@
   8.221  
   8.222  
   8.223  
   8.224 -subsection\<open>Pseudo-Division and Division of Polynomials\<close>
   8.225 +subsection \<open>Pseudo-Division and Division of Polynomials\<close>
   8.226  
   8.227  text\<open>This part is by René Thiemann and Akihisa Yamada.\<close>
   8.228  
   8.229 @@ -1838,15 +2018,172 @@
   8.230  lemma divide_poly_0: "f div 0 = (0 :: 'a poly)"
   8.231    by (simp add: divide_poly_def Let_def divide_poly_main_0)
   8.232  
   8.233 -instance by (standard, auto simp: divide_poly divide_poly_0)
   8.234 +instance
   8.235 +  by standard (auto simp: divide_poly divide_poly_0)
   8.236 +
   8.237  end
   8.238  
   8.239 -
   8.240  instance poly :: (idom_divide) algebraic_semidom ..
   8.241  
   8.242 -
   8.243 -
   8.244 -subsubsection\<open>Division in Field Polynomials\<close>
   8.245 +lemma div_const_poly_conv_map_poly: 
   8.246 +  assumes "[:c:] dvd p"
   8.247 +  shows   "p div [:c:] = map_poly (\<lambda>x. x div c) p"
   8.248 +proof (cases "c = 0")
   8.249 +  case False
   8.250 +  from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
   8.251 +  moreover {
   8.252 +    have "smult c q = [:c:] * q" by simp
   8.253 +    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
   8.254 +    finally have "smult c q div [:c:] = q" .
   8.255 +  }
   8.256 +  ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
   8.257 +qed (auto intro!: poly_eqI simp: coeff_map_poly)
   8.258 +
   8.259 +lemma is_unit_monom_0:
   8.260 +  fixes a :: "'a::field"
   8.261 +  assumes "a \<noteq> 0"
   8.262 +  shows "is_unit (monom a 0)"
   8.263 +proof
   8.264 +  from assms show "1 = monom a 0 * monom (inverse a) 0"
   8.265 +    by (simp add: mult_monom)
   8.266 +qed
   8.267 +
   8.268 +lemma is_unit_triv:
   8.269 +  fixes a :: "'a::field"
   8.270 +  assumes "a \<noteq> 0"
   8.271 +  shows "is_unit [:a:]"
   8.272 +  using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
   8.273 +
   8.274 +lemma is_unit_iff_degree:
   8.275 +  assumes "p \<noteq> (0 :: _ :: field poly)"
   8.276 +  shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
   8.277 +proof
   8.278 +  assume ?Q
   8.279 +  then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
   8.280 +  with assms show ?P by (simp add: is_unit_triv)
   8.281 +next
   8.282 +  assume ?P
   8.283 +  then obtain q where "q \<noteq> 0" "p * q = 1" ..
   8.284 +  then have "degree (p * q) = degree 1"
   8.285 +    by simp
   8.286 +  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
   8.287 +    by (simp add: degree_mult_eq)
   8.288 +  then show ?Q by simp
   8.289 +qed
   8.290 +
   8.291 +lemma is_unit_pCons_iff:
   8.292 +  "is_unit (pCons (a::_::field) p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
   8.293 +  by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
   8.294 +
   8.295 +lemma is_unit_monom_trival:
   8.296 +  fixes p :: "'a::field poly"
   8.297 +  assumes "is_unit p"
   8.298 +  shows "monom (coeff p (degree p)) 0 = p"
   8.299 +  using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
   8.300 +
   8.301 +lemma is_unit_const_poly_iff: 
   8.302 +  "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
   8.303 +  by (auto simp: one_poly_def)
   8.304 +
   8.305 +lemma is_unit_polyE:
   8.306 +  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   8.307 +  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
   8.308 +proof -
   8.309 +  from assms obtain q where "1 = p * q"
   8.310 +    by (rule dvdE)
   8.311 +  then have "p \<noteq> 0" and "q \<noteq> 0"
   8.312 +    by auto
   8.313 +  from \<open>1 = p * q\<close> have "degree 1 = degree (p * q)"
   8.314 +    by simp
   8.315 +  also from \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> have "\<dots> = degree p + degree q"
   8.316 +    by (simp add: degree_mult_eq)
   8.317 +  finally have "degree p = 0" by simp
   8.318 +  with degree_eq_zeroE obtain c where c: "p = [:c:]" .
   8.319 +  moreover with \<open>p dvd 1\<close> have "c dvd 1"
   8.320 +    by (simp add: is_unit_const_poly_iff)
   8.321 +  ultimately show thesis
   8.322 +    by (rule that)
   8.323 +qed
   8.324 +
   8.325 +lemma is_unit_polyE':
   8.326 +  assumes "is_unit (p::_::field poly)"
   8.327 +  obtains a where "p = monom a 0" and "a \<noteq> 0"
   8.328 +proof -
   8.329 +  obtain a q where "p = pCons a q" by (cases p)
   8.330 +  with assms have "p = [:a:]" and "a \<noteq> 0"
   8.331 +    by (simp_all add: is_unit_pCons_iff)
   8.332 +  with that show thesis by (simp add: monom_0)
   8.333 +qed
   8.334 +
   8.335 +lemma is_unit_poly_iff:
   8.336 +  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   8.337 +  shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
   8.338 +  by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
   8.339 +
   8.340 +instantiation poly :: ("{normalization_semidom, idom_divide}") normalization_semidom
   8.341 +begin
   8.342 +
   8.343 +definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
   8.344 +  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
   8.345 +
   8.346 +definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
   8.347 +  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
   8.348 +
   8.349 +instance proof
   8.350 +  fix p :: "'a poly"
   8.351 +  show "unit_factor p * normalize p = p"
   8.352 +    by (cases "p = 0")
   8.353 +       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
   8.354 +          smult_conv_map_poly map_poly_map_poly o_def)
   8.355 +next
   8.356 +  fix p :: "'a poly"
   8.357 +  assume "is_unit p"
   8.358 +  then obtain c where p: "p = [:c:]" "is_unit c"
   8.359 +    by (auto simp: is_unit_poly_iff)
   8.360 +  thus "normalize p = 1"
   8.361 +    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
   8.362 +next
   8.363 +  fix p :: "'a poly" assume "p \<noteq> 0"
   8.364 +  thus "is_unit (unit_factor p)"
   8.365 +    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
   8.366 +qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
   8.367 +
   8.368 +end
   8.369 +
   8.370 +lemma normalize_poly_eq_div:
   8.371 +  "normalize p = p div [:unit_factor (lead_coeff p):]"
   8.372 +proof (cases "p = 0")
   8.373 +  case False
   8.374 +  thus ?thesis
   8.375 +    by (subst div_const_poly_conv_map_poly)
   8.376 +       (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
   8.377 +qed (auto simp: normalize_poly_def)
   8.378 +
   8.379 +lemma unit_factor_pCons:
   8.380 +  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
   8.381 +  by (simp add: unit_factor_poly_def)
   8.382 +
   8.383 +lemma normalize_monom [simp]:
   8.384 +  "normalize (monom a n) = monom (normalize a) n"
   8.385 +  by (simp add: map_poly_monom normalize_poly_def)
   8.386 +
   8.387 +lemma unit_factor_monom [simp]:
   8.388 +  "unit_factor (monom a n) = monom (unit_factor a) 0"
   8.389 +  by (simp add: unit_factor_poly_def )
   8.390 +
   8.391 +lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
   8.392 +  by (simp add: normalize_poly_def map_poly_pCons)
   8.393 +
   8.394 +lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
   8.395 +proof -
   8.396 +  have "smult c p = [:c:] * p" by simp
   8.397 +  also have "normalize \<dots> = smult (normalize c) (normalize p)"
   8.398 +    by (subst normalize_mult) (simp add: normalize_const_poly)
   8.399 +  finally show ?thesis .
   8.400 +qed
   8.401 +
   8.402 +
   8.403 +subsubsection \<open>Division in Field Polynomials\<close>
   8.404  
   8.405  text\<open>
   8.406   This part connects the above result to the division of field polynomials.
   8.407 @@ -1978,58 +2315,6 @@
   8.408  
   8.409  end
   8.410  
   8.411 -lemma is_unit_monom_0:
   8.412 -  fixes a :: "'a::field"
   8.413 -  assumes "a \<noteq> 0"
   8.414 -  shows "is_unit (monom a 0)"
   8.415 -proof
   8.416 -  from assms show "1 = monom a 0 * monom (inverse a) 0"
   8.417 -    by (simp add: mult_monom)
   8.418 -qed
   8.419 -
   8.420 -lemma is_unit_triv:
   8.421 -  fixes a :: "'a::field"
   8.422 -  assumes "a \<noteq> 0"
   8.423 -  shows "is_unit [:a:]"
   8.424 -  using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
   8.425 -
   8.426 -lemma is_unit_iff_degree:
   8.427 -  assumes "p \<noteq> (0 :: _ :: field poly)"
   8.428 -  shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
   8.429 -proof
   8.430 -  assume ?Q
   8.431 -  then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
   8.432 -  with assms show ?P by (simp add: is_unit_triv)
   8.433 -next
   8.434 -  assume ?P
   8.435 -  then obtain q where "q \<noteq> 0" "p * q = 1" ..
   8.436 -  then have "degree (p * q) = degree 1"
   8.437 -    by simp
   8.438 -  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
   8.439 -    by (simp add: degree_mult_eq)
   8.440 -  then show ?Q by simp
   8.441 -qed
   8.442 -
   8.443 -lemma is_unit_pCons_iff:
   8.444 -  "is_unit (pCons (a::_::field) p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
   8.445 -  by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
   8.446 -
   8.447 -lemma is_unit_monom_trival:
   8.448 -  fixes p :: "'a::field poly"
   8.449 -  assumes "is_unit p"
   8.450 -  shows "monom (coeff p (degree p)) 0 = p"
   8.451 -  using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
   8.452 -
   8.453 -lemma is_unit_polyE:
   8.454 -  assumes "is_unit (p::_::field poly)"
   8.455 -  obtains a where "p = monom a 0" and "a \<noteq> 0"
   8.456 -proof -
   8.457 -  obtain a q where "p = pCons a q" by (cases p)
   8.458 -  with assms have "p = [:a:]" and "a \<noteq> 0"
   8.459 -    by (simp_all add: is_unit_pCons_iff)
   8.460 -  with that show thesis by (simp add: monom_0)
   8.461 -qed
   8.462 -
   8.463  lemma degree_mod_less:
   8.464    "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
   8.465    using pdivmod_rel [of x y]
   8.466 @@ -2860,18 +3145,11 @@
   8.467    by (cases "finite A", induction rule: finite_induct)
   8.468       (simp_all add: pcompose_1 pcompose_mult)
   8.469  
   8.470 -
   8.471 -(* The remainder of this section and the next were contributed by Wenda Li *)
   8.472 -
   8.473 -lemma degree_mult_eq_0:
   8.474 -  fixes p q:: "'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
   8.475 -  shows "degree (p*q) = 0 \<longleftrightarrow> p=0 \<or> q=0 \<or> (p\<noteq>0 \<and> q\<noteq>0 \<and> degree p =0 \<and> degree q =0)"
   8.476 -by (auto simp add:degree_mult_eq)
   8.477 -
   8.478 -lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp) 
   8.479 +lemma pcompose_const [simp]: "pcompose [:a:] q = [:a:]"
   8.480 +  by (subst pcompose_pCons) simp
   8.481  
   8.482  lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]"
   8.483 -  by (induct p) (auto simp add:pcompose_pCons)
   8.484 +  by (induct p) (auto simp add: pcompose_pCons)
   8.485  
   8.486  lemma degree_pcompose:
   8.487    fixes p q:: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   8.488 @@ -2932,53 +3210,6 @@
   8.489    thus ?thesis using \<open>p=[:a:]\<close> by simp
   8.490  qed
   8.491  
   8.492 -
   8.493 -subsection \<open>Leading coefficient\<close>
   8.494 -
   8.495 -definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
   8.496 -  "lead_coeff p= coeff p (degree p)"
   8.497 -
   8.498 -lemma lead_coeff_pCons[simp]:
   8.499 -    "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
   8.500 -    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
   8.501 -unfolding lead_coeff_def by auto
   8.502 -
   8.503 -lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
   8.504 -  unfolding lead_coeff_def by auto
   8.505 -
   8.506 -lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
   8.507 -  by (induction xs) (simp_all add: coeff_mult)
   8.508 -
   8.509 -lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
   8.510 -  by (induction n) (simp_all add: coeff_mult)
   8.511 -
   8.512 -lemma lead_coeff_mult:
   8.513 -   fixes p q::"'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
   8.514 -   shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
   8.515 -by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)
   8.516 -
   8.517 -lemma lead_coeff_add_le:
   8.518 -  assumes "degree p < degree q"
   8.519 -  shows "lead_coeff (p+q) = lead_coeff q" 
   8.520 -using assms unfolding lead_coeff_def
   8.521 -by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
   8.522 -
   8.523 -lemma lead_coeff_minus:
   8.524 -  "lead_coeff (-p) = - lead_coeff p"
   8.525 -by (metis coeff_minus degree_minus lead_coeff_def)
   8.526 -
   8.527 -lemma lead_coeff_smult:
   8.528 -  "lead_coeff (smult c p :: 'a :: {comm_semiring_0,semiring_no_zero_divisors} poly) = c * lead_coeff p"
   8.529 -proof -
   8.530 -  have "smult c p = [:c:] * p" by simp
   8.531 -  also have "lead_coeff \<dots> = c * lead_coeff p"
   8.532 -    by (subst lead_coeff_mult) simp_all
   8.533 -  finally show ?thesis .
   8.534 -qed
   8.535 -
   8.536 -lemma lead_coeff_eq_zero_iff [simp]: "lead_coeff p = 0 \<longleftrightarrow> p = 0"
   8.537 -  by (simp add: lead_coeff_def)
   8.538 -
   8.539  lemma lead_coeff_comp:
   8.540    fixes p q:: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
   8.541    assumes "degree q > 0" 
   8.542 @@ -3009,25 +3240,6 @@
   8.543    ultimately show ?case by blast
   8.544  qed
   8.545  
   8.546 -lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
   8.547 -  by (simp add: lead_coeff_def)
   8.548 -
   8.549 -lemma lead_coeff_of_nat [simp]:
   8.550 -  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
   8.551 -  by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
   8.552 -
   8.553 -lemma lead_coeff_numeral [simp]: 
   8.554 -  "lead_coeff (numeral n) = numeral n"
   8.555 -  unfolding lead_coeff_def
   8.556 -  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
   8.557 -
   8.558 -lemma lead_coeff_power: 
   8.559 -  "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
   8.560 -  by (induction n) (simp_all add: lead_coeff_mult)
   8.561 -
   8.562 -lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
   8.563 -  by (simp add: lead_coeff_def)
   8.564 -
   8.565  
   8.566  subsection \<open>Shifting polynomials\<close>
   8.567  
     9.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Sat Dec 17 15:22:13 2016 +0100
     9.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Sat Dec 17 15:22:13 2016 +0100
     9.3 @@ -9,144 +9,84 @@
     9.4  theory Polynomial_Factorial
     9.5  imports 
     9.6    Complex_Main
     9.7 -  "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
     9.8    "~~/src/HOL/Library/Polynomial"
     9.9    "~~/src/HOL/Library/Normalized_Fraction"
    9.10 -begin
    9.11 -
    9.12 -subsection \<open>Prelude\<close>
    9.13 -
    9.14 -lemma prod_mset_mult: 
    9.15 -  "prod_mset (image_mset (\<lambda>x. f x * g x) A) = prod_mset (image_mset f A) * prod_mset (image_mset g A)"
    9.16 -  by (induction A) (simp_all add: mult_ac)
    9.17 -  
    9.18 -lemma prod_mset_const: "prod_mset (image_mset (\<lambda>_. c) A) = c ^ size A"
    9.19 -  by (induction A) (simp_all add: mult_ac)
    9.20 -  
    9.21 -lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
    9.22 -proof safe
    9.23 -  assume "x \<noteq> 0"
    9.24 -  hence "y = x * (y / x)" by (simp add: field_simps)
    9.25 -  thus "x dvd y" by (rule dvdI)
    9.26 -qed auto
    9.27 -
    9.28 -lemma nat_descend_induct [case_names base descend]:
    9.29 -  assumes "\<And>k::nat. k > n \<Longrightarrow> P k"
    9.30 -  assumes "\<And>k::nat. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
    9.31 -  shows   "P m"
    9.32 -  using assms by induction_schema (force intro!: wf_measure[of "\<lambda>k. Suc n - k"])+
    9.33 -
    9.34 -lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
    9.35 -  by (metis GreatestI)
    9.36 -
    9.37 -
    9.38 -context field
    9.39 -begin
    9.40 -
    9.41 -subclass idom_divide ..
    9.42 -
    9.43 -end
    9.44 -
    9.45 -context field
    9.46 -begin
    9.47 -
    9.48 -definition normalize_field :: "'a \<Rightarrow> 'a" 
    9.49 -  where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
    9.50 -definition unit_factor_field :: "'a \<Rightarrow> 'a" 
    9.51 -  where [simp]: "unit_factor_field x = x"
    9.52 -definition euclidean_size_field :: "'a \<Rightarrow> nat" 
    9.53 -  where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
    9.54 -definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    9.55 -  where [simp]: "mod_field x y = (if y = 0 then x else 0)"
    9.56 -
    9.57 -end
    9.58 -
    9.59 -instantiation real :: euclidean_ring
    9.60 -begin
    9.61 -
    9.62 -definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    9.63 -definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
    9.64 -definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
    9.65 -definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
    9.66 -
    9.67 -instance by standard (simp_all add: dvd_field_iff divide_simps)
    9.68 -end
    9.69 -
    9.70 -instantiation real :: euclidean_ring_gcd
    9.71 +  "~~/src/HOL/Library/Field_as_Ring"
    9.72  begin
    9.73  
    9.74 -definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    9.75 -  "gcd_real = gcd_eucl"
    9.76 -definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    9.77 -  "lcm_real = lcm_eucl"
    9.78 -definition Gcd_real :: "real set \<Rightarrow> real" where
    9.79 - "Gcd_real = Gcd_eucl"
    9.80 -definition Lcm_real :: "real set \<Rightarrow> real" where
    9.81 - "Lcm_real = Lcm_eucl"
    9.82 +subsection \<open>Various facts about polynomials\<close>
    9.83  
    9.84 -instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
    9.85 -
    9.86 -end
    9.87 +lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
    9.88 +  by (induction A) (simp_all add: one_poly_def mult_ac)
    9.89  
    9.90 -instantiation rat :: euclidean_ring
    9.91 -begin
    9.92 -
    9.93 -definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    9.94 -definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
    9.95 -definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
    9.96 -definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
    9.97 -
    9.98 -instance by standard (simp_all add: dvd_field_iff divide_simps)
    9.99 -end
   9.100 -
   9.101 -instantiation rat :: euclidean_ring_gcd
   9.102 -begin
   9.103 +lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   9.104 +proof -
   9.105 +  have "smult c p = [:c:] * p" by simp
   9.106 +  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   9.107 +  proof safe
   9.108 +    assume A: "[:c:] * p dvd 1"
   9.109 +    thus "p dvd 1" by (rule dvd_mult_right)
   9.110 +    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
   9.111 +    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
   9.112 +    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
   9.113 +    also note B [symmetric]
   9.114 +    finally show "c dvd 1" by simp
   9.115 +  next
   9.116 +    assume "c dvd 1" "p dvd 1"
   9.117 +    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
   9.118 +    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
   9.119 +    hence "[:c:] dvd 1" by (rule dvdI)
   9.120 +    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
   9.121 +  qed
   9.122 +  finally show ?thesis .
   9.123 +qed
   9.124  
   9.125 -definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
   9.126 -  "gcd_rat = gcd_eucl"
   9.127 -definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
   9.128 -  "lcm_rat = lcm_eucl"
   9.129 -definition Gcd_rat :: "rat set \<Rightarrow> rat" where
   9.130 - "Gcd_rat = Gcd_eucl"
   9.131 -definition Lcm_rat :: "rat set \<Rightarrow> rat" where
   9.132 - "Lcm_rat = Lcm_eucl"
   9.133 -
   9.134 -instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
   9.135 -
   9.136 -end
   9.137 -
   9.138 -instantiation complex :: euclidean_ring
   9.139 -begin
   9.140 +lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
   9.141 +  using degree_mod_less[of b a] by auto
   9.142 +  
   9.143 +lemma smult_eq_iff:
   9.144 +  assumes "(b :: 'a :: field) \<noteq> 0"
   9.145 +  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
   9.146 +proof
   9.147 +  assume "smult a p = smult b q"
   9.148 +  also from assms have "smult (inverse b) \<dots> = q" by simp
   9.149 +  finally show "smult (a / b) p = q" by (simp add: field_simps)
   9.150 +qed (insert assms, auto)
   9.151  
   9.152 -definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
   9.153 -definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
   9.154 -definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
   9.155 -definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
   9.156 -
   9.157 -instance by standard (simp_all add: dvd_field_iff divide_simps)
   9.158 -end
   9.159 -
   9.160 -instantiation complex :: euclidean_ring_gcd
   9.161 -begin
   9.162 -
   9.163 -definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   9.164 -  "gcd_complex = gcd_eucl"
   9.165 -definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
   9.166 -  "lcm_complex = lcm_eucl"
   9.167 -definition Gcd_complex :: "complex set \<Rightarrow> complex" where
   9.168 - "Gcd_complex = Gcd_eucl"
   9.169 -definition Lcm_complex :: "complex set \<Rightarrow> complex" where
   9.170 - "Lcm_complex = Lcm_eucl"
   9.171 -
   9.172 -instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
   9.173 -
   9.174 -end
   9.175 -
   9.176 +lemma irreducible_const_poly_iff:
   9.177 +  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
   9.178 +  shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
   9.179 +proof
   9.180 +  assume A: "irreducible c"
   9.181 +  show "irreducible [:c:]"
   9.182 +  proof (rule irreducibleI)
   9.183 +    fix a b assume ab: "[:c:] = a * b"
   9.184 +    hence "degree [:c:] = degree (a * b)" by (simp only: )
   9.185 +    also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
   9.186 +    hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
   9.187 +    finally have "degree a = 0" "degree b = 0" by auto
   9.188 +    then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
   9.189 +    from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
   9.190 +    hence "c = a' * b'" by (simp add: ab' mult_ac)
   9.191 +    from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
   9.192 +    with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
   9.193 +  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
   9.194 +next
   9.195 +  assume A: "irreducible [:c:]"
   9.196 +  show "irreducible c"
   9.197 +  proof (rule irreducibleI)
   9.198 +    fix a b assume ab: "c = a * b"
   9.199 +    hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
   9.200 +    from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
   9.201 +    thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
   9.202 +  qed (insert A, auto simp: irreducible_def one_poly_def)
   9.203 +qed
   9.204  
   9.205  
   9.206  subsection \<open>Lifting elements into the field of fractions\<close>
   9.207  
   9.208  definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
   9.209 +  -- \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
   9.210  
   9.211  lemma to_fract_0 [simp]: "to_fract 0 = 0"
   9.212    by (simp add: to_fract_def eq_fract Zero_fract_def)
   9.213 @@ -219,285 +159,6 @@
   9.214  lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
   9.215    by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
   9.216  
   9.217 -  
   9.218 -subsection \<open>Mapping polynomials\<close>
   9.219 -
   9.220 -definition map_poly 
   9.221 -     :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
   9.222 -  "map_poly f p = Poly (map f (coeffs p))"
   9.223 -
   9.224 -lemma map_poly_0 [simp]: "map_poly f 0 = 0"
   9.225 -  by (simp add: map_poly_def)
   9.226 -
   9.227 -lemma map_poly_1: "map_poly f 1 = [:f 1:]"
   9.228 -  by (simp add: map_poly_def)
   9.229 -
   9.230 -lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
   9.231 -  by (simp add: map_poly_def one_poly_def)
   9.232 -
   9.233 -lemma coeff_map_poly:
   9.234 -  assumes "f 0 = 0"
   9.235 -  shows   "coeff (map_poly f p) n = f (coeff p n)"
   9.236 -  by (auto simp: map_poly_def nth_default_def coeffs_def assms
   9.237 -        not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
   9.238 -
   9.239 -lemma coeffs_map_poly [code abstract]: 
   9.240 -    "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
   9.241 -  by (simp add: map_poly_def)
   9.242 -
   9.243 -lemma set_coeffs_map_poly:
   9.244 -  "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
   9.245 -  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
   9.246 -
   9.247 -lemma coeffs_map_poly': 
   9.248 -  assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
   9.249 -  shows   "coeffs (map_poly f p) = map f (coeffs p)"
   9.250 -  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 
   9.251 -                           intro!: strip_while_not_last split: if_splits)
   9.252 -
   9.253 -lemma degree_map_poly:
   9.254 -  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
   9.255 -  shows   "degree (map_poly f p) = degree p"
   9.256 -  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
   9.257 -
   9.258 -lemma map_poly_eq_0_iff:
   9.259 -  assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
   9.260 -  shows   "map_poly f p = 0 \<longleftrightarrow> p = 0"
   9.261 -proof -
   9.262 -  {
   9.263 -    fix n :: nat
   9.264 -    have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
   9.265 -    also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
   9.266 -    proof (cases "n < length (coeffs p)")
   9.267 -      case True
   9.268 -      hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
   9.269 -      with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
   9.270 -    qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
   9.271 -    finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
   9.272 -  }
   9.273 -  thus ?thesis by (auto simp: poly_eq_iff)
   9.274 -qed
   9.275 -
   9.276 -lemma map_poly_smult:
   9.277 -  assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
   9.278 -  shows   "map_poly f (smult c p) = smult (f c) (map_poly f p)"
   9.279 -  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
   9.280 -
   9.281 -lemma map_poly_pCons:
   9.282 -  assumes "f 0 = 0"
   9.283 -  shows   "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
   9.284 -  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
   9.285 -
   9.286 -lemma map_poly_map_poly:
   9.287 -  assumes "f 0 = 0" "g 0 = 0"
   9.288 -  shows   "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
   9.289 -  by (intro poly_eqI) (simp add: coeff_map_poly assms)
   9.290 -
   9.291 -lemma map_poly_id [simp]: "map_poly id p = p"
   9.292 -  by (simp add: map_poly_def)
   9.293 -
   9.294 -lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
   9.295 -  by (simp add: map_poly_def)
   9.296 -
   9.297 -lemma map_poly_cong: 
   9.298 -  assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
   9.299 -  shows   "map_poly f p = map_poly g p"
   9.300 -proof -
   9.301 -  from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
   9.302 -  thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
   9.303 -qed
   9.304 -
   9.305 -lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
   9.306 -  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   9.307 -
   9.308 -lemma map_poly_idI:
   9.309 -  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
   9.310 -  shows   "map_poly f p = p"
   9.311 -  using map_poly_cong[OF assms, of _ id] by simp
   9.312 -
   9.313 -lemma map_poly_idI':
   9.314 -  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
   9.315 -  shows   "p = map_poly f p"
   9.316 -  using map_poly_cong[OF assms, of _ id] by simp
   9.317 -
   9.318 -lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
   9.319 -  by (intro poly_eqI) (simp_all add: coeff_map_poly)
   9.320 -
   9.321 -lemma div_const_poly_conv_map_poly: 
   9.322 -  assumes "[:c:] dvd p"
   9.323 -  shows   "p div [:c:] = map_poly (\<lambda>x. x div c) p"
   9.324 -proof (cases "c = 0")
   9.325 -  case False
   9.326 -  from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
   9.327 -  moreover {
   9.328 -    have "smult c q = [:c:] * q" by simp
   9.329 -    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
   9.330 -    finally have "smult c q div [:c:] = q" .
   9.331 -  }
   9.332 -  ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
   9.333 -qed (auto intro!: poly_eqI simp: coeff_map_poly)
   9.334 -
   9.335 -
   9.336 -
   9.337 -subsection \<open>Various facts about polynomials\<close>
   9.338 -
   9.339 -lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
   9.340 -  by (induction A) (simp_all add: one_poly_def mult_ac)
   9.341 -
   9.342 -lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
   9.343 -  using degree_mod_less[of b a] by auto
   9.344 -  
   9.345 -lemma is_unit_const_poly_iff: 
   9.346 -    "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
   9.347 -  by (auto simp: one_poly_def)
   9.348 -
   9.349 -lemma is_unit_poly_iff:
   9.350 -  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   9.351 -  shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
   9.352 -proof safe
   9.353 -  assume "p dvd 1"
   9.354 -  then obtain q where pq: "1 = p * q" by (erule dvdE)
   9.355 -  hence "degree 1 = degree (p * q)" by simp
   9.356 -  also from pq have "\<dots> = degree p + degree q" by (intro degree_mult_eq) auto
   9.357 -  finally have "degree p = 0" by simp
   9.358 -  from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" .
   9.359 -  with \<open>p dvd 1\<close> show "\<exists>c. p = [:c:] \<and> c dvd 1"
   9.360 -    by (auto simp: is_unit_const_poly_iff)
   9.361 -qed (auto simp: is_unit_const_poly_iff)
   9.362 -
   9.363 -lemma is_unit_polyE:
   9.364 -  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
   9.365 -  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
   9.366 -  using assms by (subst (asm) is_unit_poly_iff) blast
   9.367 -
   9.368 -lemma smult_eq_iff:
   9.369 -  assumes "(b :: 'a :: field) \<noteq> 0"
   9.370 -  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
   9.371 -proof
   9.372 -  assume "smult a p = smult b q"
   9.373 -  also from assms have "smult (inverse b) \<dots> = q" by simp
   9.374 -  finally show "smult (a / b) p = q" by (simp add: field_simps)
   9.375 -qed (insert assms, auto)
   9.376 -
   9.377 -lemma irreducible_const_poly_iff:
   9.378 -  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
   9.379 -  shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
   9.380 -proof
   9.381 -  assume A: "irreducible c"
   9.382 -  show "irreducible [:c:]"
   9.383 -  proof (rule irreducibleI)
   9.384 -    fix a b assume ab: "[:c:] = a * b"
   9.385 -    hence "degree [:c:] = degree (a * b)" by (simp only: )
   9.386 -    also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
   9.387 -    hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
   9.388 -    finally have "degree a = 0" "degree b = 0" by auto
   9.389 -    then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
   9.390 -    from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
   9.391 -    hence "c = a' * b'" by (simp add: ab' mult_ac)
   9.392 -    from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
   9.393 -    with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
   9.394 -  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
   9.395 -next
   9.396 -  assume A: "irreducible [:c:]"
   9.397 -  show "irreducible c"
   9.398 -  proof (rule irreducibleI)
   9.399 -    fix a b assume ab: "c = a * b"
   9.400 -    hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
   9.401 -    from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
   9.402 -    thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
   9.403 -  qed (insert A, auto simp: irreducible_def one_poly_def)
   9.404 -qed
   9.405 -
   9.406 -lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
   9.407 -  by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
   9.408 -
   9.409 -  
   9.410 -subsection \<open>Normalisation of polynomials\<close>
   9.411 -
   9.412 -instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom
   9.413 -begin
   9.414 -
   9.415 -definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
   9.416 -  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
   9.417 -
   9.418 -definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
   9.419 -  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
   9.420 -
   9.421 -lemma normalize_poly_altdef:
   9.422 -  "normalize p = p div [:unit_factor (lead_coeff p):]"
   9.423 -proof (cases "p = 0")
   9.424 -  case False
   9.425 -  thus ?thesis
   9.426 -    by (subst div_const_poly_conv_map_poly)
   9.427 -       (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
   9.428 -qed (auto simp: normalize_poly_def)
   9.429 -
   9.430 -instance
   9.431 -proof
   9.432 -  fix p :: "'a poly"
   9.433 -  show "unit_factor p * normalize p = p"
   9.434 -    by (cases "p = 0")
   9.435 -       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
   9.436 -          smult_conv_map_poly map_poly_map_poly o_def)
   9.437 -next
   9.438 -  fix p :: "'a poly"
   9.439 -  assume "is_unit p"
   9.440 -  then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff)
   9.441 -  thus "normalize p = 1"
   9.442 -    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
   9.443 -next
   9.444 -  fix p :: "'a poly" assume "p \<noteq> 0"
   9.445 -  thus "is_unit (unit_factor p)"
   9.446 -    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
   9.447 -qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
   9.448 -
   9.449 -end
   9.450 -
   9.451 -lemma unit_factor_pCons:
   9.452 -  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
   9.453 -  by (simp add: unit_factor_poly_def)
   9.454 -
   9.455 -lemma normalize_monom [simp]:
   9.456 -  "normalize (monom a n) = monom (normalize a) n"
   9.457 -  by (simp add: map_poly_monom normalize_poly_def)
   9.458 -
   9.459 -lemma unit_factor_monom [simp]:
   9.460 -  "unit_factor (monom a n) = monom (unit_factor a) 0"
   9.461 -  by (simp add: unit_factor_poly_def )
   9.462 -
   9.463 -lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
   9.464 -  by (simp add: normalize_poly_def map_poly_pCons)
   9.465 -
   9.466 -lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
   9.467 -proof -
   9.468 -  have "smult c p = [:c:] * p" by simp
   9.469 -  also have "normalize \<dots> = smult (normalize c) (normalize p)"
   9.470 -    by (subst normalize_mult) (simp add: normalize_const_poly)
   9.471 -  finally show ?thesis .
   9.472 -qed
   9.473 -
   9.474 -lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   9.475 -proof -
   9.476 -  have "smult c p = [:c:] * p" by simp
   9.477 -  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
   9.478 -  proof safe
   9.479 -    assume A: "[:c:] * p dvd 1"
   9.480 -    thus "p dvd 1" by (rule dvd_mult_right)
   9.481 -    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
   9.482 -    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
   9.483 -    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
   9.484 -    also note B [symmetric]
   9.485 -    finally show "c dvd 1" by simp
   9.486 -  next
   9.487 -    assume "c dvd 1" "p dvd 1"
   9.488 -    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
   9.489 -    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
   9.490 -    hence "[:c:] dvd 1" by (rule dvdI)
   9.491 -    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
   9.492 -  qed
   9.493 -  finally show ?thesis .
   9.494 -qed
   9.495 -
   9.496  
   9.497  subsection \<open>Content and primitive part of a polynomial\<close>
   9.498  
   9.499 @@ -1243,7 +904,7 @@
   9.500  
   9.501  end
   9.502  
   9.503 -  
   9.504 + 
   9.505  subsection \<open>Prime factorisation of polynomials\<close>   
   9.506  
   9.507  context
   9.508 @@ -1264,7 +925,8 @@
   9.509      by (simp add: e_def content_prod_mset multiset.map_comp o_def)
   9.510    also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
   9.511      by (intro image_mset_cong content_primitive_part_fract) auto
   9.512 -  finally have content_e: "content e = 1" by (simp add: prod_mset_const)    
   9.513 +  finally have content_e: "content e = 1"
   9.514 +    by simp    
   9.515    
   9.516    have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
   9.517            normalize_field_poly (fract_poly p)" by simp
   9.518 @@ -1277,7 +939,7 @@
   9.519                 image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
   9.520      by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
   9.521    also have "prod_mset \<dots> = smult c (fract_poly e)"
   9.522 -    by (subst prod_mset_mult) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
   9.523 +    by (subst prod_mset.distrib) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
   9.524    also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
   9.525      by (simp add: c'_def)
   9.526    finally have eq: "fract_poly p = smult c' (fract_poly e)" .
   9.527 @@ -1466,20 +1128,22 @@
   9.528                smult (gcd (content p) (content q)) 
   9.529                  (gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
   9.530  
   9.531 +lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
   9.532 +  by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
   9.533 +
   9.534  lemma lcm_poly_code [code]: 
   9.535    fixes p q :: "'a :: factorial_ring_gcd poly"
   9.536    shows "lcm p q = normalize (p * q) div gcd p q"
   9.537 -  by (rule lcm_gcd)
   9.538 -
   9.539 -lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
   9.540 -  by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
   9.541 +  by (fact lcm_gcd)
   9.542  
   9.543  declare Gcd_set
   9.544    [where ?'a = "'a :: factorial_ring_gcd poly", code]
   9.545  
   9.546  declare Lcm_set
   9.547    [where ?'a = "'a :: factorial_ring_gcd poly", code]
   9.548 +
   9.549 +text \<open>Example:
   9.550 +  @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
   9.551 +\<close>
   9.552    
   9.553 -value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
   9.554 -
   9.555  end
    10.1 --- a/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
    10.2 +++ b/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
    10.3 @@ -31,10 +31,11 @@
    10.4    *}
    10.5    theories
    10.6      Library
    10.7 -    Polynomial_Factorial
    10.8      (*conflicting type class instantiations and dependent applications*)
    10.9 +    Field_as_Ring
   10.10      Finite_Lattice
   10.11      List_lexord
   10.12 +    Polynomial_Factorial
   10.13      Prefix_Order
   10.14      Product_Lexorder
   10.15      Product_Order
    11.1 --- a/src/HOL/Rings.thy	Sat Dec 17 15:22:13 2016 +0100
    11.2 +++ b/src/HOL/Rings.thy	Sat Dec 17 15:22:13 2016 +0100
    11.3 @@ -713,9 +713,41 @@
    11.4  lemma div_by_1 [simp]: "a div 1 = a"
    11.5    using nonzero_mult_div_cancel_left [of 1 a] by simp
    11.6  
    11.7 +lemma dvd_div_eq_0_iff:
    11.8 +  assumes "b dvd a"
    11.9 +  shows "a div b = 0 \<longleftrightarrow> a = 0"
   11.10 +  using assms by (elim dvdE, cases "b = 0") simp_all  
   11.11 +
   11.12 +lemma dvd_div_eq_cancel:
   11.13 +  "a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
   11.14 +  by (elim dvdE, cases "c = 0") simp_all
   11.15 +
   11.16 +lemma dvd_div_eq_iff:
   11.17 +  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
   11.18 +  by (elim dvdE, cases "c = 0") simp_all
   11.19 +
   11.20  end
   11.21  
   11.22  class idom_divide = idom + semidom_divide
   11.23 +begin
   11.24 +
   11.25 +lemma dvd_neg_div':
   11.26 +  assumes "b dvd a"
   11.27 +  shows "- a div b = - (a div b)"
   11.28 +proof (cases "b = 0")
   11.29 +  case True
   11.30 +  then show ?thesis by simp
   11.31 +next
   11.32 +  case False
   11.33 +  from assms obtain c where "a = b * c" ..
   11.34 +  moreover from False have "b * - c div b = - (b * c div b)"
   11.35 +    using nonzero_mult_div_cancel_left [of b "- c"]
   11.36 +    by simp
   11.37 +  ultimately show ?thesis
   11.38 +    by simp
   11.39 +qed
   11.40 +
   11.41 +end
   11.42  
   11.43  class algebraic_semidom = semidom_divide
   11.44  begin
   11.45 @@ -1060,6 +1092,15 @@
   11.46    shows "a div (b * a) = 1 div b"
   11.47    using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
   11.48  
   11.49 +lemma unit_div_eq_0_iff:
   11.50 +  assumes "is_unit b"
   11.51 +  shows "a div b = 0 \<longleftrightarrow> a = 0"
   11.52 +  by (rule dvd_div_eq_0_iff) (insert assms, auto)  
   11.53 +
   11.54 +lemma div_mult_unit2:
   11.55 +  "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
   11.56 +  by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
   11.57 +
   11.58  end
   11.59  
   11.60  class normalization_semidom = algebraic_semidom +
   11.61 @@ -1373,6 +1414,17 @@
   11.62      by simp
   11.63  qed
   11.64  
   11.65 +lemma normalize_unit_factor_eqI:
   11.66 +  assumes "normalize a = normalize b"
   11.67 +    and "unit_factor a = unit_factor b"
   11.68 +  shows "a = b"
   11.69 +proof -
   11.70 +  from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
   11.71 +    by simp
   11.72 +  then show ?thesis
   11.73 +    by simp
   11.74 +qed
   11.75 +
   11.76  end
   11.77  
   11.78