author haftmann Sat Dec 17 15:22:13 2016 +0100 (2016-12-17) changeset 64591 240a39af9ec4 parent 64590 6621d91d3c8a child 64592 7759f1766189
restructured matter on polynomials and normalized fractions
 src/HOL/Fields.thy file | annotate | diff | revisions src/HOL/Fun_Def.thy file | annotate | diff | revisions src/HOL/GCD.thy file | annotate | diff | revisions src/HOL/Hilbert_Choice.thy file | annotate | diff | revisions src/HOL/Library/Field_as_Ring.thy file | annotate | diff | revisions src/HOL/Library/Multiset.thy file | annotate | diff | revisions src/HOL/Library/Normalized_Fraction.thy file | annotate | diff | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | revisions src/HOL/Library/Polynomial_Factorial.thy file | annotate | diff | revisions src/HOL/ROOT file | annotate | diff | revisions src/HOL/Rings.thy file | annotate | diff | revisions
```     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.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.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.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.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.130
8.131  lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
8.132 @@ -1137,6 +1243,11 @@
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.149 +
8.150 +definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
8.151 +  "lead_coeff p= coeff p (degree p)"
8.152 +
8.155 +    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
8.157 +
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.168 +   fixes p q::"'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
8.171 +
8.173 +  assumes "degree p < degree q"
8.177 +
8.180 +by (metis coeff_minus degree_minus lead_coeff_def)
8.181 +
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.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.193 +
8.196 +
8.198 +  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
8.200 +
8.202 +  "lead_coeff (numeral n) = numeral n"
8.204 +  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
8.205 +
8.207 +  "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
8.209 +
8.212 +
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.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.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.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.494 -
8.495 -definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
8.496 -  "lead_coeff p= coeff p (degree p)"
8.497 -
8.500 -    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
8.502 -
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.513 -   fixes p q::"'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
8.516 -
8.518 -  assumes "degree p < degree q"
8.522 -
8.525 -by (metis coeff_minus degree_minus lead_coeff_def)
8.526 -
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.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.538 -
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.548 -
8.550 -  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
8.552 -
8.554 -  "lead_coeff (numeral n) = numeral n"
8.556 -  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
8.557 -
8.559 -  "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
8.561 -
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.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.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.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
```