--- a/src/HOL/Fields.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Fields.thy Sat Dec 17 15:22:13 2016 +0100
@@ -506,6 +506,21 @@
"y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
by (simp add: add_divide_distrib add.commute)
+lemma dvd_field_iff:
+ "a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)"
+proof (cases "a = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ then have "b = a * (b / a)"
+ by (simp add: field_simps)
+ then have "a dvd b" ..
+ with False show ?thesis
+ by simp
+qed
+
end
class field_char_0 = field + ring_char_0
--- a/src/HOL/Fun_Def.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Fun_Def.thy Sat Dec 17 15:22:13 2016 +0100
@@ -278,6 +278,16 @@
done
+subsection \<open>Yet another induction principle on the natural numbers\<close>
+
+lemma nat_descend_induct [case_names base descend]:
+ fixes P :: "nat \<Rightarrow> bool"
+ assumes H1: "\<And>k. k > n \<Longrightarrow> P k"
+ assumes H2: "\<And>k. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
+ shows "P m"
+ using assms by induction_schema (force intro!: wf_measure [of "\<lambda>k. Suc n - k"])+
+
+
subsection \<open>Tool setup\<close>
ML_file "Tools/Function/termination.ML"
--- a/src/HOL/GCD.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/GCD.thy Sat Dec 17 15:22:13 2016 +0100
@@ -639,7 +639,6 @@
using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
qed
-
lemma divides_mult:
assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
shows "a * b dvd c"
@@ -695,6 +694,10 @@
using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
by blast
+lemma coprime_mul_eq':
+ "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
+ using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
+
lemma gcd_coprime:
assumes c: "gcd a b \<noteq> 0"
and a: "a = a' * gcd a b"
@@ -958,6 +961,24 @@
ultimately show ?thesis by (rule that)
qed
+lemma coprime_crossproduct':
+ fixes a b c d
+ assumes "b \<noteq> 0"
+ assumes unit_factors: "unit_factor b = unit_factor d"
+ assumes coprime: "coprime a b" "coprime c d"
+ shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
+proof safe
+ assume eq: "a * d = b * c"
+ hence "normalize a * normalize d = normalize c * normalize b"
+ by (simp only: normalize_mult [symmetric] mult_ac)
+ with coprime have "normalize b = normalize d"
+ by (subst (asm) coprime_crossproduct) simp_all
+ from this and unit_factors show "b = d"
+ by (rule normalize_unit_factor_eqI)
+ from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
+ with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
+qed (simp_all add: mult_ac)
+
end
class ring_gcd = comm_ring_1 + semiring_gcd
--- a/src/HOL/Hilbert_Choice.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Hilbert_Choice.thy Sat Dec 17 15:22:13 2016 +0100
@@ -657,6 +657,12 @@
for x :: nat
unfolding Greatest_def by (rule GreatestM_nat_le) auto
+lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
+ apply (erule exE)
+ apply (rule GreatestI)
+ apply assumption+
+ done
+
subsection \<open>An aside: bounded accessible part\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Field_as_Ring.thy Sat Dec 17 15:22:13 2016 +0100
@@ -0,0 +1,108 @@
+(* Title: HOL/Library/Field_as_Ring.thy
+ Author: Manuel Eberl
+*)
+
+theory Field_as_Ring
+imports
+ Complex_Main
+ "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
+begin
+
+context field
+begin
+
+subclass idom_divide ..
+
+definition normalize_field :: "'a \<Rightarrow> 'a"
+ where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
+definition unit_factor_field :: "'a \<Rightarrow> 'a"
+ where [simp]: "unit_factor_field x = x"
+definition euclidean_size_field :: "'a \<Rightarrow> nat"
+ where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
+definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ where [simp]: "mod_field x y = (if y = 0 then x else 0)"
+
+end
+
+instantiation real :: euclidean_ring
+begin
+
+definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
+definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
+definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
+definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
+
+instance by standard (simp_all add: dvd_field_iff divide_simps)
+end
+
+instantiation real :: euclidean_ring_gcd
+begin
+
+definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
+ "gcd_real = gcd_eucl"
+definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
+ "lcm_real = lcm_eucl"
+definition Gcd_real :: "real set \<Rightarrow> real" where
+ "Gcd_real = Gcd_eucl"
+definition Lcm_real :: "real set \<Rightarrow> real" where
+ "Lcm_real = Lcm_eucl"
+
+instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
+
+end
+
+instantiation rat :: euclidean_ring
+begin
+
+definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
+definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
+definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
+definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
+
+instance by standard (simp_all add: dvd_field_iff divide_simps)
+end
+
+instantiation rat :: euclidean_ring_gcd
+begin
+
+definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
+ "gcd_rat = gcd_eucl"
+definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
+ "lcm_rat = lcm_eucl"
+definition Gcd_rat :: "rat set \<Rightarrow> rat" where
+ "Gcd_rat = Gcd_eucl"
+definition Lcm_rat :: "rat set \<Rightarrow> rat" where
+ "Lcm_rat = Lcm_eucl"
+
+instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
+
+end
+
+instantiation complex :: euclidean_ring
+begin
+
+definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
+definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
+definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
+definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
+
+instance by standard (simp_all add: dvd_field_iff divide_simps)
+end
+
+instantiation complex :: euclidean_ring_gcd
+begin
+
+definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
+ "gcd_complex = gcd_eucl"
+definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
+ "lcm_complex = lcm_eucl"
+definition Gcd_complex :: "complex set \<Rightarrow> complex" where
+ "Gcd_complex = Gcd_eucl"
+definition Lcm_complex :: "complex set \<Rightarrow> complex" where
+ "Lcm_complex = Lcm_eucl"
+
+instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
+
+end
+
+end
--- a/src/HOL/Library/Multiset.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Dec 17 15:22:13 2016 +0100
@@ -1738,6 +1738,10 @@
"(\<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#}"
by (metis image_mset_cong split_cong)
+lemma image_mset_const_eq:
+ "{#c. a \<in># M#} = replicate_mset (size M) c"
+ by (induct M) simp_all
+
subsection \<open>Further conversions\<close>
@@ -2310,6 +2314,9 @@
translations
"\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
+lemma prod_mset_constant [simp]: "(\<Prod>_\<in>#A. c) = c ^ size A"
+ by (simp add: image_mset_const_eq)
+
lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
assumes "A \<subseteq># B"
shows "prod_mset A dvd prod_mset B"
--- a/src/HOL/Library/Normalized_Fraction.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Normalized_Fraction.thy Sat Dec 17 15:22:13 2016 +0100
@@ -1,3 +1,7 @@
+(* Title: HOL/Library/Normalized_Fraction.thy
+ Author: Manuel Eberl
+*)
+
theory Normalized_Fraction
imports
Main
@@ -5,75 +9,6 @@
"~~/src/HOL/Library/Fraction_Field"
begin
-lemma dvd_neg_div': "y dvd (x :: 'a :: idom_divide) \<Longrightarrow> -x div y = - (x div y)"
-apply (case_tac "y = 0") apply simp
-apply (auto simp add: dvd_def)
-apply (subgoal_tac "-(y * k) = y * - k")
-apply (simp only:)
-apply (erule nonzero_mult_div_cancel_left)
-apply simp
-done
-
-(* TODO Move *)
-lemma (in semiring_gcd) coprime_mul_eq': "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
- using coprime_mul_eq[of d a b] by (simp add: gcd.commute)
-
-lemma dvd_div_eq_0_iff:
- assumes "b dvd (a :: 'a :: semidom_divide)"
- shows "a div b = 0 \<longleftrightarrow> a = 0"
- using assms by (elim dvdE, cases "b = 0") simp_all
-
-lemma dvd_div_eq_0_iff':
- assumes "b dvd (a :: 'a :: semiring_div)"
- shows "a div b = 0 \<longleftrightarrow> a = 0"
- using assms by (elim dvdE, cases "b = 0") simp_all
-
-lemma unit_div_eq_0_iff:
- assumes "is_unit (b :: 'a :: {algebraic_semidom,semidom_divide})"
- shows "a div b = 0 \<longleftrightarrow> a = 0"
- by (rule dvd_div_eq_0_iff) (insert assms, auto)
-
-lemma unit_div_eq_0_iff':
- assumes "is_unit (b :: 'a :: semiring_div)"
- shows "a div b = 0 \<longleftrightarrow> a = 0"
- by (rule dvd_div_eq_0_iff) (insert assms, auto)
-
-lemma dvd_div_eq_cancel:
- "a div c = b div c \<Longrightarrow> (c :: 'a :: semiring_div) dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
- by (elim dvdE, cases "c = 0") simp_all
-
-lemma dvd_div_eq_iff:
- "(c :: 'a :: semiring_div) dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
- by (elim dvdE, cases "c = 0") simp_all
-
-lemma normalize_imp_eq:
- "normalize a = normalize b \<Longrightarrow> unit_factor a = unit_factor b \<Longrightarrow> a = b"
- by (cases "a = 0 \<or> b = 0")
- (auto simp add: div_unit_factor [symmetric] unit_div_cancel simp del: div_unit_factor)
-
-lemma coprime_crossproduct':
- fixes a b c d :: "'a :: semiring_gcd"
- assumes nz: "b \<noteq> 0"
- assumes unit_factors: "unit_factor b = unit_factor d"
- assumes coprime: "coprime a b" "coprime c d"
- shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
-proof safe
- assume eq: "a * d = b * c"
- hence "normalize a * normalize d = normalize c * normalize b"
- by (simp only: normalize_mult [symmetric] mult_ac)
- with coprime have "normalize b = normalize d"
- by (subst (asm) coprime_crossproduct) simp_all
- from this and unit_factors show "b = d" by (rule normalize_imp_eq)
- from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
- with nz \<open>b = d\<close> show "a = c" by simp
-qed (simp_all add: mult_ac)
-
-
-lemma div_mult_unit2: "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
- by (subst dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
-(* END TODO *)
-
-
definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where
"quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)"
--- a/src/HOL/Library/Polynomial.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy Sat Dec 17 15:22:13 2016 +0100
@@ -877,7 +877,7 @@
by (induct n, simp add: monom_0, simp add: monom_Suc)
lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)"
- by (auto simp add: poly_eq_iff coeff_Poly_eq nth_default_def)
+ by (auto simp add: poly_eq_iff nth_default_def)
lemma degree_smult_eq [simp]:
fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
@@ -1064,6 +1064,111 @@
by (rule le_trans[OF degree_mult_le], insert insert, auto)
qed simp
+
+subsection \<open>Mapping polynomials\<close>
+
+definition map_poly
+ :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
+ "map_poly f p = Poly (map f (coeffs p))"
+
+lemma map_poly_0 [simp]: "map_poly f 0 = 0"
+ by (simp add: map_poly_def)
+
+lemma map_poly_1: "map_poly f 1 = [:f 1:]"
+ by (simp add: map_poly_def)
+
+lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
+ by (simp add: map_poly_def one_poly_def)
+
+lemma coeff_map_poly:
+ assumes "f 0 = 0"
+ shows "coeff (map_poly f p) n = f (coeff p n)"
+ by (auto simp: map_poly_def nth_default_def coeffs_def assms
+ not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
+
+lemma coeffs_map_poly [code abstract]:
+ "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
+ by (simp add: map_poly_def)
+
+lemma set_coeffs_map_poly:
+ "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
+ by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
+
+lemma coeffs_map_poly':
+ assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
+ shows "coeffs (map_poly f p) = map f (coeffs p)"
+ by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms
+ intro!: strip_while_not_last split: if_splits)
+
+lemma degree_map_poly:
+ assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
+ shows "degree (map_poly f p) = degree p"
+ by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
+
+lemma map_poly_eq_0_iff:
+ assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
+ shows "map_poly f p = 0 \<longleftrightarrow> p = 0"
+proof -
+ {
+ fix n :: nat
+ have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
+ also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
+ proof (cases "n < length (coeffs p)")
+ case True
+ hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
+ with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
+ qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
+ finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
+ }
+ thus ?thesis by (auto simp: poly_eq_iff)
+qed
+
+lemma map_poly_smult:
+ assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
+ shows "map_poly f (smult c p) = smult (f c) (map_poly f p)"
+ by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
+
+lemma map_poly_pCons:
+ assumes "f 0 = 0"
+ shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
+ by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
+
+lemma map_poly_map_poly:
+ assumes "f 0 = 0" "g 0 = 0"
+ shows "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
+ by (intro poly_eqI) (simp add: coeff_map_poly assms)
+
+lemma map_poly_id [simp]: "map_poly id p = p"
+ by (simp add: map_poly_def)
+
+lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
+ by (simp add: map_poly_def)
+
+lemma map_poly_cong:
+ assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
+ shows "map_poly f p = map_poly g p"
+proof -
+ from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
+ thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
+qed
+
+lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
+ by (intro poly_eqI) (simp_all add: coeff_map_poly)
+
+lemma map_poly_idI:
+ assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
+ shows "map_poly f p = p"
+ using map_poly_cong[OF assms, of _ id] by simp
+
+lemma map_poly_idI':
+ assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
+ shows "p = map_poly f p"
+ using map_poly_cong[OF assms, of _ id] by simp
+
+lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
+ by (intro poly_eqI) (simp_all add: coeff_map_poly)
+
+
subsection \<open>Conversions from natural numbers\<close>
lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
@@ -1086,6 +1191,7 @@
lemma numeral_poly: "numeral n = [:numeral n:]"
by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+
subsection \<open>Lemmas about divisibility\<close>
lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
@@ -1137,6 +1243,11 @@
apply (simp add: coeff_mult_degree_sum)
done
+lemma degree_mult_eq_0:
+ fixes p q:: "'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
+ 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)"
+ by (auto simp add: degree_mult_eq)
+
lemma degree_mult_right_le:
fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
assumes "q \<noteq> 0"
@@ -1290,6 +1401,75 @@
text \<open>TODO: Simplification rules for comparisons\<close>
+subsection \<open>Leading coefficient\<close>
+
+definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
+ "lead_coeff p= coeff p (degree p)"
+
+lemma lead_coeff_pCons[simp]:
+ "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
+ "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
+unfolding lead_coeff_def by auto
+
+lemma lead_coeff_0[simp]:"lead_coeff 0 =0"
+ unfolding lead_coeff_def by auto
+
+lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
+ by (induction xs) (simp_all add: coeff_mult)
+
+lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
+ by (induction n) (simp_all add: coeff_mult)
+
+lemma lead_coeff_mult:
+ fixes p q::"'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
+ shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
+by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)
+
+lemma lead_coeff_add_le:
+ assumes "degree p < degree q"
+ shows "lead_coeff (p+q) = lead_coeff q"
+using assms unfolding lead_coeff_def
+by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
+
+lemma lead_coeff_minus:
+ "lead_coeff (-p) = - lead_coeff p"
+by (metis coeff_minus degree_minus lead_coeff_def)
+
+lemma lead_coeff_smult:
+ "lead_coeff (smult c p :: 'a :: {comm_semiring_0,semiring_no_zero_divisors} poly) = c * lead_coeff p"
+proof -
+ have "smult c p = [:c:] * p" by simp
+ also have "lead_coeff \<dots> = c * lead_coeff p"
+ by (subst lead_coeff_mult) simp_all
+ finally show ?thesis .
+qed
+
+lemma lead_coeff_eq_zero_iff [simp]: "lead_coeff p = 0 \<longleftrightarrow> p = 0"
+ by (simp add: lead_coeff_def)
+
+lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
+ by (simp add: lead_coeff_def)
+
+lemma lead_coeff_of_nat [simp]:
+ "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
+ by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
+
+lemma lead_coeff_numeral [simp]:
+ "lead_coeff (numeral n) = numeral n"
+ unfolding lead_coeff_def
+ by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+
+lemma lead_coeff_power:
+ "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
+ by (induction n) (simp_all add: lead_coeff_mult)
+
+lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
+ by (simp add: lead_coeff_def)
+
+lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
+ by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
+
+
subsection \<open>Synthetic division and polynomial roots\<close>
text \<open>
@@ -1555,7 +1735,7 @@
-subsection\<open>Pseudo-Division and Division of Polynomials\<close>
+subsection \<open>Pseudo-Division and Division of Polynomials\<close>
text\<open>This part is by René Thiemann and Akihisa Yamada.\<close>
@@ -1838,15 +2018,172 @@
lemma divide_poly_0: "f div 0 = (0 :: 'a poly)"
by (simp add: divide_poly_def Let_def divide_poly_main_0)
-instance by (standard, auto simp: divide_poly divide_poly_0)
+instance
+ by standard (auto simp: divide_poly divide_poly_0)
+
end
-
instance poly :: (idom_divide) algebraic_semidom ..
-
-
-subsubsection\<open>Division in Field Polynomials\<close>
+lemma div_const_poly_conv_map_poly:
+ assumes "[:c:] dvd p"
+ shows "p div [:c:] = map_poly (\<lambda>x. x div c) p"
+proof (cases "c = 0")
+ case False
+ from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
+ moreover {
+ have "smult c q = [:c:] * q" by simp
+ also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
+ finally have "smult c q div [:c:] = q" .
+ }
+ ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
+qed (auto intro!: poly_eqI simp: coeff_map_poly)
+
+lemma is_unit_monom_0:
+ fixes a :: "'a::field"
+ assumes "a \<noteq> 0"
+ shows "is_unit (monom a 0)"
+proof
+ from assms show "1 = monom a 0 * monom (inverse a) 0"
+ by (simp add: mult_monom)
+qed
+
+lemma is_unit_triv:
+ fixes a :: "'a::field"
+ assumes "a \<noteq> 0"
+ shows "is_unit [:a:]"
+ using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
+
+lemma is_unit_iff_degree:
+ assumes "p \<noteq> (0 :: _ :: field poly)"
+ shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?Q
+ then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
+ with assms show ?P by (simp add: is_unit_triv)
+next
+ assume ?P
+ then obtain q where "q \<noteq> 0" "p * q = 1" ..
+ then have "degree (p * q) = degree 1"
+ by simp
+ with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
+ by (simp add: degree_mult_eq)
+ then show ?Q by simp
+qed
+
+lemma is_unit_pCons_iff:
+ "is_unit (pCons (a::_::field) p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
+ by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
+
+lemma is_unit_monom_trival:
+ fixes p :: "'a::field poly"
+ assumes "is_unit p"
+ shows "monom (coeff p (degree p)) 0 = p"
+ using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
+
+lemma is_unit_const_poly_iff:
+ "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
+ by (auto simp: one_poly_def)
+
+lemma is_unit_polyE:
+ fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
+ assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
+proof -
+ from assms obtain q where "1 = p * q"
+ by (rule dvdE)
+ then have "p \<noteq> 0" and "q \<noteq> 0"
+ by auto
+ from \<open>1 = p * q\<close> have "degree 1 = degree (p * q)"
+ by simp
+ also from \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> have "\<dots> = degree p + degree q"
+ by (simp add: degree_mult_eq)
+ finally have "degree p = 0" by simp
+ with degree_eq_zeroE obtain c where c: "p = [:c:]" .
+ moreover with \<open>p dvd 1\<close> have "c dvd 1"
+ by (simp add: is_unit_const_poly_iff)
+ ultimately show thesis
+ by (rule that)
+qed
+
+lemma is_unit_polyE':
+ assumes "is_unit (p::_::field poly)"
+ obtains a where "p = monom a 0" and "a \<noteq> 0"
+proof -
+ obtain a q where "p = pCons a q" by (cases p)
+ with assms have "p = [:a:]" and "a \<noteq> 0"
+ by (simp_all add: is_unit_pCons_iff)
+ with that show thesis by (simp add: monom_0)
+qed
+
+lemma is_unit_poly_iff:
+ fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
+ shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
+ by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
+
+instantiation poly :: ("{normalization_semidom, idom_divide}") normalization_semidom
+begin
+
+definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
+ where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
+
+definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
+ where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+
+instance proof
+ fix p :: "'a poly"
+ show "unit_factor p * normalize p = p"
+ by (cases "p = 0")
+ (simp_all add: unit_factor_poly_def normalize_poly_def monom_0
+ smult_conv_map_poly map_poly_map_poly o_def)
+next
+ fix p :: "'a poly"
+ assume "is_unit p"
+ then obtain c where p: "p = [:c:]" "is_unit c"
+ by (auto simp: is_unit_poly_iff)
+ thus "normalize p = 1"
+ by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
+next
+ fix p :: "'a poly" assume "p \<noteq> 0"
+ thus "is_unit (unit_factor p)"
+ by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
+qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
+
+end
+
+lemma normalize_poly_eq_div:
+ "normalize p = p div [:unit_factor (lead_coeff p):]"
+proof (cases "p = 0")
+ case False
+ thus ?thesis
+ by (subst div_const_poly_conv_map_poly)
+ (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
+qed (auto simp: normalize_poly_def)
+
+lemma unit_factor_pCons:
+ "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
+ by (simp add: unit_factor_poly_def)
+
+lemma normalize_monom [simp]:
+ "normalize (monom a n) = monom (normalize a) n"
+ by (simp add: map_poly_monom normalize_poly_def)
+
+lemma unit_factor_monom [simp]:
+ "unit_factor (monom a n) = monom (unit_factor a) 0"
+ by (simp add: unit_factor_poly_def )
+
+lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
+ by (simp add: normalize_poly_def map_poly_pCons)
+
+lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
+proof -
+ have "smult c p = [:c:] * p" by simp
+ also have "normalize \<dots> = smult (normalize c) (normalize p)"
+ by (subst normalize_mult) (simp add: normalize_const_poly)
+ finally show ?thesis .
+qed
+
+
+subsubsection \<open>Division in Field Polynomials\<close>
text\<open>
This part connects the above result to the division of field polynomials.
@@ -1978,58 +2315,6 @@
end
-lemma is_unit_monom_0:
- fixes a :: "'a::field"
- assumes "a \<noteq> 0"
- shows "is_unit (monom a 0)"
-proof
- from assms show "1 = monom a 0 * monom (inverse a) 0"
- by (simp add: mult_monom)
-qed
-
-lemma is_unit_triv:
- fixes a :: "'a::field"
- assumes "a \<noteq> 0"
- shows "is_unit [:a:]"
- using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
-
-lemma is_unit_iff_degree:
- assumes "p \<noteq> (0 :: _ :: field poly)"
- shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
-proof
- assume ?Q
- then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
- with assms show ?P by (simp add: is_unit_triv)
-next
- assume ?P
- then obtain q where "q \<noteq> 0" "p * q = 1" ..
- then have "degree (p * q) = degree 1"
- by simp
- with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
- by (simp add: degree_mult_eq)
- then show ?Q by simp
-qed
-
-lemma is_unit_pCons_iff:
- "is_unit (pCons (a::_::field) p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
- by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
-
-lemma is_unit_monom_trival:
- fixes p :: "'a::field poly"
- assumes "is_unit p"
- shows "monom (coeff p (degree p)) 0 = p"
- using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
-
-lemma is_unit_polyE:
- assumes "is_unit (p::_::field poly)"
- obtains a where "p = monom a 0" and "a \<noteq> 0"
-proof -
- obtain a q where "p = pCons a q" by (cases p)
- with assms have "p = [:a:]" and "a \<noteq> 0"
- by (simp_all add: is_unit_pCons_iff)
- with that show thesis by (simp add: monom_0)
-qed
-
lemma degree_mod_less:
"y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
using pdivmod_rel [of x y]
@@ -2860,18 +3145,11 @@
by (cases "finite A", induction rule: finite_induct)
(simp_all add: pcompose_1 pcompose_mult)
-
-(* The remainder of this section and the next were contributed by Wenda Li *)
-
-lemma degree_mult_eq_0:
- fixes p q:: "'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
- 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)"
-by (auto simp add:degree_mult_eq)
-
-lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp)
+lemma pcompose_const [simp]: "pcompose [:a:] q = [:a:]"
+ by (subst pcompose_pCons) simp
lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]"
- by (induct p) (auto simp add:pcompose_pCons)
+ by (induct p) (auto simp add: pcompose_pCons)
lemma degree_pcompose:
fixes p q:: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
@@ -2932,53 +3210,6 @@
thus ?thesis using \<open>p=[:a:]\<close> by simp
qed
-
-subsection \<open>Leading coefficient\<close>
-
-definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
- "lead_coeff p= coeff p (degree p)"
-
-lemma lead_coeff_pCons[simp]:
- "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
- "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
-unfolding lead_coeff_def by auto
-
-lemma lead_coeff_0[simp]:"lead_coeff 0 =0"
- unfolding lead_coeff_def by auto
-
-lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
- by (induction xs) (simp_all add: coeff_mult)
-
-lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
- by (induction n) (simp_all add: coeff_mult)
-
-lemma lead_coeff_mult:
- fixes p q::"'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
- shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
-by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)
-
-lemma lead_coeff_add_le:
- assumes "degree p < degree q"
- shows "lead_coeff (p+q) = lead_coeff q"
-using assms unfolding lead_coeff_def
-by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
-
-lemma lead_coeff_minus:
- "lead_coeff (-p) = - lead_coeff p"
-by (metis coeff_minus degree_minus lead_coeff_def)
-
-lemma lead_coeff_smult:
- "lead_coeff (smult c p :: 'a :: {comm_semiring_0,semiring_no_zero_divisors} poly) = c * lead_coeff p"
-proof -
- have "smult c p = [:c:] * p" by simp
- also have "lead_coeff \<dots> = c * lead_coeff p"
- by (subst lead_coeff_mult) simp_all
- finally show ?thesis .
-qed
-
-lemma lead_coeff_eq_zero_iff [simp]: "lead_coeff p = 0 \<longleftrightarrow> p = 0"
- by (simp add: lead_coeff_def)
-
lemma lead_coeff_comp:
fixes p q:: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
assumes "degree q > 0"
@@ -3009,25 +3240,6 @@
ultimately show ?case by blast
qed
-lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
- by (simp add: lead_coeff_def)
-
-lemma lead_coeff_of_nat [simp]:
- "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
- by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
-
-lemma lead_coeff_numeral [simp]:
- "lead_coeff (numeral n) = numeral n"
- unfolding lead_coeff_def
- by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
-
-lemma lead_coeff_power:
- "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
- by (induction n) (simp_all add: lead_coeff_mult)
-
-lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
- by (simp add: lead_coeff_def)
-
subsection \<open>Shifting polynomials\<close>
--- a/src/HOL/Library/Polynomial_Factorial.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Polynomial_Factorial.thy Sat Dec 17 15:22:13 2016 +0100
@@ -9,144 +9,84 @@
theory Polynomial_Factorial
imports
Complex_Main
- "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
"~~/src/HOL/Library/Polynomial"
"~~/src/HOL/Library/Normalized_Fraction"
-begin
-
-subsection \<open>Prelude\<close>
-
-lemma prod_mset_mult:
- "prod_mset (image_mset (\<lambda>x. f x * g x) A) = prod_mset (image_mset f A) * prod_mset (image_mset g A)"
- by (induction A) (simp_all add: mult_ac)
-
-lemma prod_mset_const: "prod_mset (image_mset (\<lambda>_. c) A) = c ^ size A"
- by (induction A) (simp_all add: mult_ac)
-
-lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
-proof safe
- assume "x \<noteq> 0"
- hence "y = x * (y / x)" by (simp add: field_simps)
- thus "x dvd y" by (rule dvdI)
-qed auto
-
-lemma nat_descend_induct [case_names base descend]:
- assumes "\<And>k::nat. k > n \<Longrightarrow> P k"
- assumes "\<And>k::nat. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
- shows "P m"
- using assms by induction_schema (force intro!: wf_measure[of "\<lambda>k. Suc n - k"])+
-
-lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
- by (metis GreatestI)
-
-
-context field
-begin
-
-subclass idom_divide ..
-
-end
-
-context field
-begin
-
-definition normalize_field :: "'a \<Rightarrow> 'a"
- where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
-definition unit_factor_field :: "'a \<Rightarrow> 'a"
- where [simp]: "unit_factor_field x = x"
-definition euclidean_size_field :: "'a \<Rightarrow> nat"
- where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
-definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
- where [simp]: "mod_field x y = (if y = 0 then x else 0)"
-
-end
-
-instantiation real :: euclidean_ring
-begin
-
-definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
-definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
-definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
-definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
-
-instance by standard (simp_all add: dvd_field_iff divide_simps)
-end
-
-instantiation real :: euclidean_ring_gcd
+ "~~/src/HOL/Library/Field_as_Ring"
begin
-definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
- "gcd_real = gcd_eucl"
-definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
- "lcm_real = lcm_eucl"
-definition Gcd_real :: "real set \<Rightarrow> real" where
- "Gcd_real = Gcd_eucl"
-definition Lcm_real :: "real set \<Rightarrow> real" where
- "Lcm_real = Lcm_eucl"
+subsection \<open>Various facts about polynomials\<close>
-instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
-
-end
+lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
+ by (induction A) (simp_all add: one_poly_def mult_ac)
-instantiation rat :: euclidean_ring
-begin
-
-definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
-definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
-definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
-definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
-
-instance by standard (simp_all add: dvd_field_iff divide_simps)
-end
-
-instantiation rat :: euclidean_ring_gcd
-begin
+lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
+proof -
+ have "smult c p = [:c:] * p" by simp
+ also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
+ proof safe
+ assume A: "[:c:] * p dvd 1"
+ thus "p dvd 1" by (rule dvd_mult_right)
+ from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
+ have "c dvd c * (coeff p 0 * coeff q 0)" by simp
+ also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
+ also note B [symmetric]
+ finally show "c dvd 1" by simp
+ next
+ assume "c dvd 1" "p dvd 1"
+ from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
+ hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
+ hence "[:c:] dvd 1" by (rule dvdI)
+ from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
+ qed
+ finally show ?thesis .
+qed
-definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
- "gcd_rat = gcd_eucl"
-definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
- "lcm_rat = lcm_eucl"
-definition Gcd_rat :: "rat set \<Rightarrow> rat" where
- "Gcd_rat = Gcd_eucl"
-definition Lcm_rat :: "rat set \<Rightarrow> rat" where
- "Lcm_rat = Lcm_eucl"
-
-instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
-
-end
-
-instantiation complex :: euclidean_ring
-begin
+lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
+ using degree_mod_less[of b a] by auto
+
+lemma smult_eq_iff:
+ assumes "(b :: 'a :: field) \<noteq> 0"
+ shows "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
+proof
+ assume "smult a p = smult b q"
+ also from assms have "smult (inverse b) \<dots> = q" by simp
+ finally show "smult (a / b) p = q" by (simp add: field_simps)
+qed (insert assms, auto)
-definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
-definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
-definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
-definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
-
-instance by standard (simp_all add: dvd_field_iff divide_simps)
-end
-
-instantiation complex :: euclidean_ring_gcd
-begin
-
-definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
- "gcd_complex = gcd_eucl"
-definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
- "lcm_complex = lcm_eucl"
-definition Gcd_complex :: "complex set \<Rightarrow> complex" where
- "Gcd_complex = Gcd_eucl"
-definition Lcm_complex :: "complex set \<Rightarrow> complex" where
- "Lcm_complex = Lcm_eucl"
-
-instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
-
-end
-
+lemma irreducible_const_poly_iff:
+ fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
+ shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
+proof
+ assume A: "irreducible c"
+ show "irreducible [:c:]"
+ proof (rule irreducibleI)
+ fix a b assume ab: "[:c:] = a * b"
+ hence "degree [:c:] = degree (a * b)" by (simp only: )
+ also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
+ hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
+ finally have "degree a = 0" "degree b = 0" by auto
+ then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
+ from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
+ hence "c = a' * b'" by (simp add: ab' mult_ac)
+ from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
+ with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
+ qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
+next
+ assume A: "irreducible [:c:]"
+ show "irreducible c"
+ proof (rule irreducibleI)
+ fix a b assume ab: "c = a * b"
+ hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
+ from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
+ thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
+ qed (insert A, auto simp: irreducible_def one_poly_def)
+qed
subsection \<open>Lifting elements into the field of fractions\<close>
definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
+ -- \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
lemma to_fract_0 [simp]: "to_fract 0 = 0"
by (simp add: to_fract_def eq_fract Zero_fract_def)
@@ -219,285 +159,6 @@
lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
-
-subsection \<open>Mapping polynomials\<close>
-
-definition map_poly
- :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
- "map_poly f p = Poly (map f (coeffs p))"
-
-lemma map_poly_0 [simp]: "map_poly f 0 = 0"
- by (simp add: map_poly_def)
-
-lemma map_poly_1: "map_poly f 1 = [:f 1:]"
- by (simp add: map_poly_def)
-
-lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
- by (simp add: map_poly_def one_poly_def)
-
-lemma coeff_map_poly:
- assumes "f 0 = 0"
- shows "coeff (map_poly f p) n = f (coeff p n)"
- by (auto simp: map_poly_def nth_default_def coeffs_def assms
- not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
-
-lemma coeffs_map_poly [code abstract]:
- "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
- by (simp add: map_poly_def)
-
-lemma set_coeffs_map_poly:
- "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
- by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
-
-lemma coeffs_map_poly':
- assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
- shows "coeffs (map_poly f p) = map f (coeffs p)"
- by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms
- intro!: strip_while_not_last split: if_splits)
-
-lemma degree_map_poly:
- assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
- shows "degree (map_poly f p) = degree p"
- by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
-
-lemma map_poly_eq_0_iff:
- assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
- shows "map_poly f p = 0 \<longleftrightarrow> p = 0"
-proof -
- {
- fix n :: nat
- have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
- also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
- proof (cases "n < length (coeffs p)")
- case True
- hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
- with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
- qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
- finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
- }
- thus ?thesis by (auto simp: poly_eq_iff)
-qed
-
-lemma map_poly_smult:
- assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
- shows "map_poly f (smult c p) = smult (f c) (map_poly f p)"
- by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
-
-lemma map_poly_pCons:
- assumes "f 0 = 0"
- shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
- by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
-
-lemma map_poly_map_poly:
- assumes "f 0 = 0" "g 0 = 0"
- shows "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
- by (intro poly_eqI) (simp add: coeff_map_poly assms)
-
-lemma map_poly_id [simp]: "map_poly id p = p"
- by (simp add: map_poly_def)
-
-lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
- by (simp add: map_poly_def)
-
-lemma map_poly_cong:
- assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
- shows "map_poly f p = map_poly g p"
-proof -
- from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
- thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
-qed
-
-lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
- by (intro poly_eqI) (simp_all add: coeff_map_poly)
-
-lemma map_poly_idI:
- assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
- shows "map_poly f p = p"
- using map_poly_cong[OF assms, of _ id] by simp
-
-lemma map_poly_idI':
- assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
- shows "p = map_poly f p"
- using map_poly_cong[OF assms, of _ id] by simp
-
-lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
- by (intro poly_eqI) (simp_all add: coeff_map_poly)
-
-lemma div_const_poly_conv_map_poly:
- assumes "[:c:] dvd p"
- shows "p div [:c:] = map_poly (\<lambda>x. x div c) p"
-proof (cases "c = 0")
- case False
- from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
- moreover {
- have "smult c q = [:c:] * q" by simp
- also have "\<dots> div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (insert False, auto)
- finally have "smult c q div [:c:] = q" .
- }
- ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
-qed (auto intro!: poly_eqI simp: coeff_map_poly)
-
-
-
-subsection \<open>Various facts about polynomials\<close>
-
-lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
- by (induction A) (simp_all add: one_poly_def mult_ac)
-
-lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
- using degree_mod_less[of b a] by auto
-
-lemma is_unit_const_poly_iff:
- "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
- by (auto simp: one_poly_def)
-
-lemma is_unit_poly_iff:
- fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
- shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
-proof safe
- assume "p dvd 1"
- then obtain q where pq: "1 = p * q" by (erule dvdE)
- hence "degree 1 = degree (p * q)" by simp
- also from pq have "\<dots> = degree p + degree q" by (intro degree_mult_eq) auto
- finally have "degree p = 0" by simp
- from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" .
- with \<open>p dvd 1\<close> show "\<exists>c. p = [:c:] \<and> c dvd 1"
- by (auto simp: is_unit_const_poly_iff)
-qed (auto simp: is_unit_const_poly_iff)
-
-lemma is_unit_polyE:
- fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
- assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
- using assms by (subst (asm) is_unit_poly_iff) blast
-
-lemma smult_eq_iff:
- assumes "(b :: 'a :: field) \<noteq> 0"
- shows "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
-proof
- assume "smult a p = smult b q"
- also from assms have "smult (inverse b) \<dots> = q" by simp
- finally show "smult (a / b) p = q" by (simp add: field_simps)
-qed (insert assms, auto)
-
-lemma irreducible_const_poly_iff:
- fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
- shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
-proof
- assume A: "irreducible c"
- show "irreducible [:c:]"
- proof (rule irreducibleI)
- fix a b assume ab: "[:c:] = a * b"
- hence "degree [:c:] = degree (a * b)" by (simp only: )
- also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
- hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
- finally have "degree a = 0" "degree b = 0" by auto
- then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
- from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
- hence "c = a' * b'" by (simp add: ab' mult_ac)
- from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
- with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
- qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
-next
- assume A: "irreducible [:c:]"
- show "irreducible c"
- proof (rule irreducibleI)
- fix a b assume ab: "c = a * b"
- hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
- from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
- thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
- qed (insert A, auto simp: irreducible_def one_poly_def)
-qed
-
-lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
- by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
-
-
-subsection \<open>Normalisation of polynomials\<close>
-
-instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom
-begin
-
-definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
- where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
-
-definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
- where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
-
-lemma normalize_poly_altdef:
- "normalize p = p div [:unit_factor (lead_coeff p):]"
-proof (cases "p = 0")
- case False
- thus ?thesis
- by (subst div_const_poly_conv_map_poly)
- (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
-qed (auto simp: normalize_poly_def)
-
-instance
-proof
- fix p :: "'a poly"
- show "unit_factor p * normalize p = p"
- by (cases "p = 0")
- (simp_all add: unit_factor_poly_def normalize_poly_def monom_0
- smult_conv_map_poly map_poly_map_poly o_def)
-next
- fix p :: "'a poly"
- assume "is_unit p"
- then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff)
- thus "normalize p = 1"
- by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
-next
- fix p :: "'a poly" assume "p \<noteq> 0"
- thus "is_unit (unit_factor p)"
- by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
-qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
-
-end
-
-lemma unit_factor_pCons:
- "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
- by (simp add: unit_factor_poly_def)
-
-lemma normalize_monom [simp]:
- "normalize (monom a n) = monom (normalize a) n"
- by (simp add: map_poly_monom normalize_poly_def)
-
-lemma unit_factor_monom [simp]:
- "unit_factor (monom a n) = monom (unit_factor a) 0"
- by (simp add: unit_factor_poly_def )
-
-lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
- by (simp add: normalize_poly_def map_poly_pCons)
-
-lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
-proof -
- have "smult c p = [:c:] * p" by simp
- also have "normalize \<dots> = smult (normalize c) (normalize p)"
- by (subst normalize_mult) (simp add: normalize_const_poly)
- finally show ?thesis .
-qed
-
-lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
-proof -
- have "smult c p = [:c:] * p" by simp
- also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
- proof safe
- assume A: "[:c:] * p dvd 1"
- thus "p dvd 1" by (rule dvd_mult_right)
- from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
- have "c dvd c * (coeff p 0 * coeff q 0)" by simp
- also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
- also note B [symmetric]
- finally show "c dvd 1" by simp
- next
- assume "c dvd 1" "p dvd 1"
- from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
- hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
- hence "[:c:] dvd 1" by (rule dvdI)
- from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
- qed
- finally show ?thesis .
-qed
-
subsection \<open>Content and primitive part of a polynomial\<close>
@@ -1243,7 +904,7 @@
end
-
+
subsection \<open>Prime factorisation of polynomials\<close>
context
@@ -1264,7 +925,8 @@
by (simp add: e_def content_prod_mset multiset.map_comp o_def)
also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
by (intro image_mset_cong content_primitive_part_fract) auto
- finally have content_e: "content e = 1" by (simp add: prod_mset_const)
+ finally have content_e: "content e = 1"
+ by simp
have "fract_poly p = unit_factor_field_poly (fract_poly p) *
normalize_field_poly (fract_poly p)" by simp
@@ -1277,7 +939,7 @@
image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
also have "prod_mset \<dots> = smult c (fract_poly e)"
- by (subst prod_mset_mult) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
+ by (subst prod_mset.distrib) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
by (simp add: c'_def)
finally have eq: "fract_poly p = smult c' (fract_poly e)" .
@@ -1466,20 +1128,22 @@
smult (gcd (content p) (content q))
(gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
+lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
+ by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
+
lemma lcm_poly_code [code]:
fixes p q :: "'a :: factorial_ring_gcd poly"
shows "lcm p q = normalize (p * q) div gcd p q"
- by (rule lcm_gcd)
-
-lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
- by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
+ by (fact lcm_gcd)
declare Gcd_set
[where ?'a = "'a :: factorial_ring_gcd poly", code]
declare Lcm_set
[where ?'a = "'a :: factorial_ring_gcd poly", code]
+
+text \<open>Example:
+ @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
+\<close>
-value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
-
end
--- a/src/HOL/ROOT Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/ROOT Sat Dec 17 15:22:13 2016 +0100
@@ -31,10 +31,11 @@
*}
theories
Library
- Polynomial_Factorial
(*conflicting type class instantiations and dependent applications*)
+ Field_as_Ring
Finite_Lattice
List_lexord
+ Polynomial_Factorial
Prefix_Order
Product_Lexorder
Product_Order
--- a/src/HOL/Rings.thy Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Rings.thy Sat Dec 17 15:22:13 2016 +0100
@@ -713,9 +713,41 @@
lemma div_by_1 [simp]: "a div 1 = a"
using nonzero_mult_div_cancel_left [of 1 a] by simp
+lemma dvd_div_eq_0_iff:
+ assumes "b dvd a"
+ shows "a div b = 0 \<longleftrightarrow> a = 0"
+ using assms by (elim dvdE, cases "b = 0") simp_all
+
+lemma dvd_div_eq_cancel:
+ "a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
+ by (elim dvdE, cases "c = 0") simp_all
+
+lemma dvd_div_eq_iff:
+ "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
+ by (elim dvdE, cases "c = 0") simp_all
+
end
class idom_divide = idom + semidom_divide
+begin
+
+lemma dvd_neg_div':
+ assumes "b dvd a"
+ shows "- a div b = - (a div b)"
+proof (cases "b = 0")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ from assms obtain c where "a = b * c" ..
+ moreover from False have "b * - c div b = - (b * c div b)"
+ using nonzero_mult_div_cancel_left [of b "- c"]
+ by simp
+ ultimately show ?thesis
+ by simp
+qed
+
+end
class algebraic_semidom = semidom_divide
begin
@@ -1060,6 +1092,15 @@
shows "a div (b * a) = 1 div b"
using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
+lemma unit_div_eq_0_iff:
+ assumes "is_unit b"
+ shows "a div b = 0 \<longleftrightarrow> a = 0"
+ by (rule dvd_div_eq_0_iff) (insert assms, auto)
+
+lemma div_mult_unit2:
+ "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
+ by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
+
end
class normalization_semidom = algebraic_semidom +
@@ -1373,6 +1414,17 @@
by simp
qed
+lemma normalize_unit_factor_eqI:
+ assumes "normalize a = normalize b"
+ and "unit_factor a = unit_factor b"
+ shows "a = b"
+proof -
+ from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
+ by simp
+ then show ?thesis
+ by simp
+qed
+
end