--- 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} \<Rightarrow> 'a poly \<Rightarrow> nat"
-where
- [code del]:
- "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
-
-lemma degree_power_le: "degree (p ^ n) \<le> 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. \<not> [:-a, 1:] ^ Suc n dvd p)")
-apply (drule not_less_Least, simp)
-apply (fold order_def, simp)
-done
-
-lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-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 \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
-by (rule conjI [OF order_1 order_2])
-
-lemma order_degree:
- assumes p: "p \<noteq> 0"
- shows "order a p \<le> degree p"
-proof -
- have "order a p = degree ([:-a, 1:] ^ order a p)"
- by (simp only: degree_linear_power)
- also have "\<dots> \<le> degree p"
- using order_1 p by (rule dvd_imp_degree_le)
- finally show ?thesis .
-qed
-
-lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 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 \<longleftrightarrow> 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 \<longleftrightarrow> p = q"
- using poly_zero [of "p - q"]
- by (simp add: expand_fun_eq)
-
subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}
--- 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} \<Rightarrow> 'a poly \<Rightarrow> nat"
+where
+ [code del]:
+ "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
+
+lemma degree_power_le: "degree (p ^ n) \<le> 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. \<not> [:-a, 1:] ^ Suc n dvd p)")
+apply (drule not_less_Least, simp)
+apply (fold order_def, simp)
+done
+
+lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-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 \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
+by (rule conjI [OF order_1 order_2])
+
+lemma order_degree:
+ assumes p: "p \<noteq> 0"
+ shows "order a p \<le> degree p"
+proof -
+ have "order a p = degree ([:-a, 1:] ^ order a p)"
+ by (simp only: degree_linear_power)
+ also have "\<dots> \<le> degree p"
+ using order_1 p by (rule dvd_imp_degree_le)
+ finally show ?thesis .
+qed
+
+lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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