# HG changeset patch # User huffman # Date 1234979278 28800 # Node ID d76b830366bcb6b3d7cc0f5a1a980ba43a4546cd # Parent 3241eb2737b985b0ab381dd0abd6a7254c314be9 move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial diff -r 3241eb2737b9 -r d76b830366bc src/HOL/Library/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Feb 18 09:08:04 2009 -0800 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Feb 18 09:47:58 2009 -0800 @@ -946,90 +946,6 @@ ultimately show ?case by blast qed simp -subsection {* Order of polynomial roots *} - -definition - order :: "'a::{idom,recpower} \ 'a poly \ nat" -where - [code del]: - "order a p = (LEAST n. \ [:-a, 1:] ^ Suc n dvd p)" - -lemma degree_power_le: "degree (p ^ n) \ degree p * n" -by (induct n, simp, auto intro: order_trans degree_mult_le) - -lemma coeff_linear_power: - fixes a :: "'a::{comm_semiring_1,recpower}" - shows "coeff ([:a, 1:] ^ n) n = 1" -apply (induct n, simp_all) -apply (subst coeff_eq_0) -apply (auto intro: le_less_trans degree_power_le) -done - -lemma degree_linear_power: - fixes a :: "'a::{comm_semiring_1,recpower}" - shows "degree ([:a, 1:] ^ n) = n" -apply (rule order_antisym) -apply (rule ord_le_eq_trans [OF degree_power_le], simp) -apply (rule le_degree, simp add: coeff_linear_power) -done - -lemma order_1: "[:-a, 1:] ^ order a p dvd p" -apply (cases "p = 0", simp) -apply (cases "order a p", simp) -apply (subgoal_tac "nat < (LEAST n. \ [:-a, 1:] ^ Suc n dvd p)") -apply (drule not_less_Least, simp) -apply (fold order_def, simp) -done - -lemma order_2: "p \ 0 \ \ [:-a, 1:] ^ Suc (order a p) dvd p" -unfolding order_def -apply (rule LeastI_ex) -apply (rule_tac x="degree p" in exI) -apply (rule notI) -apply (drule (1) dvd_imp_degree_le) -apply (simp only: degree_linear_power) -done - -lemma order: - "p \ 0 \ [:-a, 1:] ^ order a p dvd p \ \ [:-a, 1:] ^ Suc (order a p) dvd p" -by (rule conjI [OF order_1 order_2]) - -lemma order_degree: - assumes p: "p \ 0" - shows "order a p \ degree p" -proof - - have "order a p = degree ([:-a, 1:] ^ order a p)" - by (simp only: degree_linear_power) - also have "\ \ degree p" - using order_1 p by (rule dvd_imp_degree_le) - finally show ?thesis . -qed - -lemma order_root: "poly p a = 0 \ p = 0 \ order a p \ 0" -apply (cases "p = 0", simp_all) -apply (rule iffI) -apply (rule ccontr, simp) -apply (frule order_2 [where a=a], simp) -apply (simp add: poly_eq_0_iff_dvd) -apply (simp add: poly_eq_0_iff_dvd) -apply (simp only: order_def) -apply (drule not_less_Least, simp) -done - -lemma poly_zero: - fixes p :: "'a::{idom,ring_char_0} poly" - shows "poly p = poly 0 \ p = 0" -apply (cases "p = 0", simp_all) -apply (drule poly_roots_finite) -apply (auto simp add: infinite_UNIV_char_0) -done - -lemma poly_eq_iff: - fixes p q :: "'a::{idom,ring_char_0} poly" - shows "poly p = poly q \ p = q" - using poly_zero [of "p - q"] - by (simp add: expand_fun_eq) - subsection{* Nullstellenstatz, degrees and divisibility of polynomials *} diff -r 3241eb2737b9 -r d76b830366bc src/HOL/Polynomial.thy --- a/src/HOL/Polynomial.thy Wed Feb 18 09:08:04 2009 -0800 +++ b/src/HOL/Polynomial.thy Wed Feb 18 09:47:58 2009 -0800 @@ -1209,6 +1209,91 @@ qed +subsection {* Order of polynomial roots *} + +definition + order :: "'a::{idom,recpower} \ 'a poly \ nat" +where + [code del]: + "order a p = (LEAST n. \ [:-a, 1:] ^ Suc n dvd p)" + +lemma degree_power_le: "degree (p ^ n) \ degree p * n" +by (induct n, simp, auto intro: order_trans degree_mult_le) + +lemma coeff_linear_power: + fixes a :: "'a::{comm_semiring_1,recpower}" + shows "coeff ([:a, 1:] ^ n) n = 1" +apply (induct n, simp_all) +apply (subst coeff_eq_0) +apply (auto intro: le_less_trans degree_power_le) +done + +lemma degree_linear_power: + fixes a :: "'a::{comm_semiring_1,recpower}" + shows "degree ([:a, 1:] ^ n) = n" +apply (rule order_antisym) +apply (rule ord_le_eq_trans [OF degree_power_le], simp) +apply (rule le_degree, simp add: coeff_linear_power) +done + +lemma order_1: "[:-a, 1:] ^ order a p dvd p" +apply (cases "p = 0", simp) +apply (cases "order a p", simp) +apply (subgoal_tac "nat < (LEAST n. \ [:-a, 1:] ^ Suc n dvd p)") +apply (drule not_less_Least, simp) +apply (fold order_def, simp) +done + +lemma order_2: "p \ 0 \ \ [:-a, 1:] ^ Suc (order a p) dvd p" +unfolding order_def +apply (rule LeastI_ex) +apply (rule_tac x="degree p" in exI) +apply (rule notI) +apply (drule (1) dvd_imp_degree_le) +apply (simp only: degree_linear_power) +done + +lemma order: + "p \ 0 \ [:-a, 1:] ^ order a p dvd p \ \ [:-a, 1:] ^ Suc (order a p) dvd p" +by (rule conjI [OF order_1 order_2]) + +lemma order_degree: + assumes p: "p \ 0" + shows "order a p \ degree p" +proof - + have "order a p = degree ([:-a, 1:] ^ order a p)" + by (simp only: degree_linear_power) + also have "\ \ degree p" + using order_1 p by (rule dvd_imp_degree_le) + finally show ?thesis . +qed + +lemma order_root: "poly p a = 0 \ p = 0 \ order a p \ 0" +apply (cases "p = 0", simp_all) +apply (rule iffI) +apply (rule ccontr, simp) +apply (frule order_2 [where a=a], simp) +apply (simp add: poly_eq_0_iff_dvd) +apply (simp add: poly_eq_0_iff_dvd) +apply (simp only: order_def) +apply (drule not_less_Least, simp) +done + +lemma poly_zero: + fixes p :: "'a::{idom,ring_char_0} poly" + shows "poly p = poly 0 \ p = 0" +apply (cases "p = 0", simp_all) +apply (drule poly_roots_finite) +apply (auto simp add: infinite_UNIV_char_0) +done + +lemma poly_eq_iff: + fixes p q :: "'a::{idom,ring_char_0} poly" + shows "poly p = poly q \ p = q" + using poly_zero [of "p - q"] + by (simp add: expand_fun_eq) + + subsection {* Configuration of the code generator *} code_datatype "0::'a::zero poly" pCons