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} \<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 *}