move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
authorhuffman
Wed Feb 18 09:47:58 2009 -0800 (2009-02-18)
changeset 29977d76b830366bc
parent 29976 3241eb2737b9
child 29978 33df3c4eb629
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Polynomial.thy
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 09:08:04 2009 -0800
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 09:47:58 2009 -0800
     1.3 @@ -946,90 +946,6 @@
     1.4    ultimately show ?case by blast  
     1.5  qed simp
     1.6  
     1.7 -subsection {* Order of polynomial roots *}
     1.8 -
     1.9 -definition
    1.10 -  order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
    1.11 -where
    1.12 -  [code del]:
    1.13 -  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
    1.14 -
    1.15 -lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
    1.16 -by (induct n, simp, auto intro: order_trans degree_mult_le)
    1.17 -
    1.18 -lemma coeff_linear_power:
    1.19 -  fixes a :: "'a::{comm_semiring_1,recpower}"
    1.20 -  shows "coeff ([:a, 1:] ^ n) n = 1"
    1.21 -apply (induct n, simp_all)
    1.22 -apply (subst coeff_eq_0)
    1.23 -apply (auto intro: le_less_trans degree_power_le)
    1.24 -done
    1.25 -
    1.26 -lemma degree_linear_power:
    1.27 -  fixes a :: "'a::{comm_semiring_1,recpower}"
    1.28 -  shows "degree ([:a, 1:] ^ n) = n"
    1.29 -apply (rule order_antisym)
    1.30 -apply (rule ord_le_eq_trans [OF degree_power_le], simp)
    1.31 -apply (rule le_degree, simp add: coeff_linear_power)
    1.32 -done
    1.33 -
    1.34 -lemma order_1: "[:-a, 1:] ^ order a p dvd p"
    1.35 -apply (cases "p = 0", simp)
    1.36 -apply (cases "order a p", simp)
    1.37 -apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
    1.38 -apply (drule not_less_Least, simp)
    1.39 -apply (fold order_def, simp)
    1.40 -done
    1.41 -
    1.42 -lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
    1.43 -unfolding order_def
    1.44 -apply (rule LeastI_ex)
    1.45 -apply (rule_tac x="degree p" in exI)
    1.46 -apply (rule notI)
    1.47 -apply (drule (1) dvd_imp_degree_le)
    1.48 -apply (simp only: degree_linear_power)
    1.49 -done
    1.50 -
    1.51 -lemma order:
    1.52 -  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
    1.53 -by (rule conjI [OF order_1 order_2])
    1.54 -
    1.55 -lemma order_degree:
    1.56 -  assumes p: "p \<noteq> 0"
    1.57 -  shows "order a p \<le> degree p"
    1.58 -proof -
    1.59 -  have "order a p = degree ([:-a, 1:] ^ order a p)"
    1.60 -    by (simp only: degree_linear_power)
    1.61 -  also have "\<dots> \<le> degree p"
    1.62 -    using order_1 p by (rule dvd_imp_degree_le)
    1.63 -  finally show ?thesis .
    1.64 -qed
    1.65 -
    1.66 -lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
    1.67 -apply (cases "p = 0", simp_all)
    1.68 -apply (rule iffI)
    1.69 -apply (rule ccontr, simp)
    1.70 -apply (frule order_2 [where a=a], simp)
    1.71 -apply (simp add: poly_eq_0_iff_dvd)
    1.72 -apply (simp add: poly_eq_0_iff_dvd)
    1.73 -apply (simp only: order_def)
    1.74 -apply (drule not_less_Least, simp)
    1.75 -done
    1.76 -
    1.77 -lemma poly_zero:
    1.78 -  fixes p :: "'a::{idom,ring_char_0} poly"
    1.79 -  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
    1.80 -apply (cases "p = 0", simp_all)
    1.81 -apply (drule poly_roots_finite)
    1.82 -apply (auto simp add: infinite_UNIV_char_0)
    1.83 -done
    1.84 -
    1.85 -lemma poly_eq_iff:
    1.86 -  fixes p q :: "'a::{idom,ring_char_0} poly"
    1.87 -  shows "poly p = poly q \<longleftrightarrow> p = q"
    1.88 -  using poly_zero [of "p - q"]
    1.89 -  by (simp add: expand_fun_eq)
    1.90 -
    1.91  
    1.92  subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}
    1.93  
     2.1 --- a/src/HOL/Polynomial.thy	Wed Feb 18 09:08:04 2009 -0800
     2.2 +++ b/src/HOL/Polynomial.thy	Wed Feb 18 09:47:58 2009 -0800
     2.3 @@ -1209,6 +1209,91 @@
     2.4  qed
     2.5  
     2.6  
     2.7 +subsection {* Order of polynomial roots *}
     2.8 +
     2.9 +definition
    2.10 +  order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
    2.11 +where
    2.12 +  [code del]:
    2.13 +  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
    2.14 +
    2.15 +lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
    2.16 +by (induct n, simp, auto intro: order_trans degree_mult_le)
    2.17 +
    2.18 +lemma coeff_linear_power:
    2.19 +  fixes a :: "'a::{comm_semiring_1,recpower}"
    2.20 +  shows "coeff ([:a, 1:] ^ n) n = 1"
    2.21 +apply (induct n, simp_all)
    2.22 +apply (subst coeff_eq_0)
    2.23 +apply (auto intro: le_less_trans degree_power_le)
    2.24 +done
    2.25 +
    2.26 +lemma degree_linear_power:
    2.27 +  fixes a :: "'a::{comm_semiring_1,recpower}"
    2.28 +  shows "degree ([:a, 1:] ^ n) = n"
    2.29 +apply (rule order_antisym)
    2.30 +apply (rule ord_le_eq_trans [OF degree_power_le], simp)
    2.31 +apply (rule le_degree, simp add: coeff_linear_power)
    2.32 +done
    2.33 +
    2.34 +lemma order_1: "[:-a, 1:] ^ order a p dvd p"
    2.35 +apply (cases "p = 0", simp)
    2.36 +apply (cases "order a p", simp)
    2.37 +apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
    2.38 +apply (drule not_less_Least, simp)
    2.39 +apply (fold order_def, simp)
    2.40 +done
    2.41 +
    2.42 +lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
    2.43 +unfolding order_def
    2.44 +apply (rule LeastI_ex)
    2.45 +apply (rule_tac x="degree p" in exI)
    2.46 +apply (rule notI)
    2.47 +apply (drule (1) dvd_imp_degree_le)
    2.48 +apply (simp only: degree_linear_power)
    2.49 +done
    2.50 +
    2.51 +lemma order:
    2.52 +  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
    2.53 +by (rule conjI [OF order_1 order_2])
    2.54 +
    2.55 +lemma order_degree:
    2.56 +  assumes p: "p \<noteq> 0"
    2.57 +  shows "order a p \<le> degree p"
    2.58 +proof -
    2.59 +  have "order a p = degree ([:-a, 1:] ^ order a p)"
    2.60 +    by (simp only: degree_linear_power)
    2.61 +  also have "\<dots> \<le> degree p"
    2.62 +    using order_1 p by (rule dvd_imp_degree_le)
    2.63 +  finally show ?thesis .
    2.64 +qed
    2.65 +
    2.66 +lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
    2.67 +apply (cases "p = 0", simp_all)
    2.68 +apply (rule iffI)
    2.69 +apply (rule ccontr, simp)
    2.70 +apply (frule order_2 [where a=a], simp)
    2.71 +apply (simp add: poly_eq_0_iff_dvd)
    2.72 +apply (simp add: poly_eq_0_iff_dvd)
    2.73 +apply (simp only: order_def)
    2.74 +apply (drule not_less_Least, simp)
    2.75 +done
    2.76 +
    2.77 +lemma poly_zero:
    2.78 +  fixes p :: "'a::{idom,ring_char_0} poly"
    2.79 +  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
    2.80 +apply (cases "p = 0", simp_all)
    2.81 +apply (drule poly_roots_finite)
    2.82 +apply (auto simp add: infinite_UNIV_char_0)
    2.83 +done
    2.84 +
    2.85 +lemma poly_eq_iff:
    2.86 +  fixes p q :: "'a::{idom,ring_char_0} poly"
    2.87 +  shows "poly p = poly q \<longleftrightarrow> p = q"
    2.88 +  using poly_zero [of "p - q"]
    2.89 +  by (simp add: expand_fun_eq)
    2.90 +
    2.91 +
    2.92  subsection {* Configuration of the code generator *}
    2.93  
    2.94  code_datatype "0::'a::zero poly" pCons