author huffman Wed Feb 18 09:47:58 2009 -0800 (2009-02-18) changeset 29977 d76b830366bc parent 29976 3241eb2737b9 child 29978 33df3c4eb629
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
```     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.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.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
```