--- a/src/HOL/Deriv.thy Wed Feb 18 19:18:34 2009 +0100
+++ b/src/HOL/Deriv.thy Wed Feb 18 17:02:38 2009 -0800
@@ -217,9 +217,7 @@
by (cases "n", simp, simp add: DERIV_power_Suc f)
-(* ------------------------------------------------------------------------ *)
-(* Caratheodory formulation of derivative at a point: standard proof *)
-(* ------------------------------------------------------------------------ *)
+text {* Caratheodory formulation of derivative at a point *}
lemma CARAT_DERIV:
"(DERIV f x :> l) =
@@ -307,6 +305,9 @@
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
+lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
+by auto
+
subsection {* Differentiability predicate *}
@@ -655,6 +656,9 @@
apply (blast intro: IVT2)
done
+
+subsection {* Boundedness of continuous functions *}
+
text{*By bisection, function continuous on closed interval is bounded above*}
lemma isCont_bounded:
@@ -773,6 +777,8 @@
done
+subsection {* Local extrema *}
+
text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
lemma DERIV_left_inc:
@@ -877,6 +883,9 @@
shows "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
by (auto dest!: DERIV_local_max)
+
+subsection {* Rolle's Theorem *}
+
text{*Lemma about introducing open ball in open interval*}
lemma lemma_interval_lt:
"[| a < x; x < b |]
@@ -1163,6 +1172,8 @@
qed
+subsection {* Continuous injective functions *}
+
text{*Dull lemma: an continuous injection on an interval must have a
strict maximum at an end point, not in the middle.*}
@@ -1356,6 +1367,9 @@
using neq by (rule LIM_inverse)
qed
+
+subsection {* Generalized Mean Value Theorem *}
+
theorem GMVT:
fixes a b :: real
assumes alb: "a < b"
@@ -1442,9 +1456,6 @@
with g'cdef f'cdef cint show ?thesis by auto
qed
-lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
-by auto
-
subsection {* Derivatives of univariate polynomials *}
@@ -1559,128 +1570,197 @@
text{*Lemmas for Derivatives*}
-(* FIXME
+lemma order_unique_lemma:
+ fixes p :: "'a::idom poly"
+ assumes "[:-a, 1:] ^ n dvd p \<and> \<not> [:-a, 1:] ^ Suc n dvd p"
+ shows "n = order a p"
+unfolding Polynomial.order_def
+apply (rule Least_equality [symmetric])
+apply (rule assms [THEN conjunct2])
+apply (erule contrapos_np)
+apply (rule power_le_dvd)
+apply (rule assms [THEN conjunct1])
+apply simp
+done
+
+lemma lemma_order_pderiv1:
+ "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
+ smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
+apply (simp only: pderiv_mult pderiv_power_Suc)
+apply (simp del: power_poly_Suc of_nat_Suc add: pderiv_pCons)
+done
+
+lemma dvd_add_cancel1:
+ fixes a b c :: "'a::comm_ring_1"
+ shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
+ by (drule (1) Ring_and_Field.dvd_diff, simp)
+
lemma lemma_order_pderiv [rule_format]:
"\<forall>p q a. 0 < n &
- poly (pderiv p) \<noteq> poly [] &
- poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
+ pderiv p \<noteq> 0 &
+ p = [:- a, 1:] ^ n * q & ~ [:- a, 1:] dvd q
--> n = Suc (order a (pderiv p))"
-apply (induct "n", safe)
-apply (rule order_unique_lemma, rule conjI, assumption)
-apply (subgoal_tac "\<forall>r. r divides (pderiv p) = r divides (pderiv ([-a, 1] %^ Suc n *** q))")
-apply (drule_tac [2] poly_pderiv_welldef)
- prefer 2 apply (simp add: divides_def del: pmult_Cons pexp_Suc)
-apply (simp del: pmult_Cons pexp_Suc)
-apply (rule conjI)
-apply (simp add: divides_def fun_eq del: pmult_Cons pexp_Suc)
-apply (rule_tac x = "[-a, 1] *** (pderiv q) +++ real (Suc n) %* q" in exI)
-apply (simp add: poly_pderiv_mult poly_pderiv_exp_prime poly_add poly_mult poly_cmult right_distrib mult_ac del: pmult_Cons pexp_Suc)
-apply (simp add: poly_mult right_distrib left_distrib mult_ac del: pmult_Cons)
-apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl)
-apply (unfold divides_def)
-apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc)
-apply (rule contrapos_np, assumption)
-apply (rotate_tac 3, erule contrapos_np)
-apply (simp del: pmult_Cons pexp_Suc, safe)
-apply (rule_tac x = "inverse (real (Suc n)) %* (qa +++ -- (pderiv q))" in exI)
-apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ")
-apply (drule poly_mult_left_cancel [THEN iffD1], simp)
-apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left, safe)
-apply (rule_tac c1 = "real (Suc n)" in real_mult_left_cancel [THEN iffD1])
-apply (simp (no_asm))
-apply (subgoal_tac "real (Suc n) * (poly ([- a, 1] %^ n) xa * poly q xa) =
- (poly qa xa + - poly (pderiv q) xa) *
- (poly ([- a, 1] %^ n) xa *
- ((- a + xa) * (inverse (real (Suc n)) * real (Suc n))))")
-apply (simp only: mult_ac)
-apply (rotate_tac 2)
-apply (drule_tac x = xa in spec)
-apply (simp add: left_distrib mult_ac del: pmult_Cons)
+ apply (cases "n", safe, rename_tac n p q a)
+ apply (rule order_unique_lemma)
+ apply (rule conjI)
+ apply (subst lemma_order_pderiv1)
+ apply (rule dvd_add)
+ apply (rule dvd_mult2)
+ apply (rule le_imp_power_dvd, simp)
+ apply (rule dvd_smult)
+ apply (rule dvd_mult)
+ apply (rule dvd_refl)
+ apply (subst lemma_order_pderiv1)
+ apply (erule contrapos_nn) back
+ apply (subgoal_tac "[:- a, 1:] ^ Suc n dvd q * [:- a, 1:] ^ n")
+ apply (simp del: mult_pCons_left)
+ apply (drule dvd_add_cancel1)
+ apply (simp del: mult_pCons_left)
+ apply (drule dvd_smult_cancel, simp del: of_nat_Suc)
+ apply assumption
done
-lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
+lemma order_decomp:
+ "p \<noteq> 0
+ ==> \<exists>q. p = [:-a, 1:] ^ (order a p) * q &
+ ~([:-a, 1:] dvd q)"
+apply (drule order [where a=a])
+apply (erule conjE)
+apply (erule dvdE)
+apply (rule exI)
+apply (rule conjI, assumption)
+apply (erule contrapos_nn)
+apply (erule ssubst) back
+apply (subst power_Suc2)
+apply (erule mult_dvd_mono [OF dvd_refl])
+done
+
+lemma order_pderiv: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
==> (order a p = Suc (order a (pderiv p)))"
-apply (case_tac "poly p = poly []")
-apply (auto dest: pderiv_zero)
+apply (case_tac "p = 0", simp)
apply (drule_tac a = a and p = p in order_decomp)
using neq0_conv
apply (blast intro: lemma_order_pderiv)
done
+lemma order_mult: "p * q \<noteq> 0 \<Longrightarrow> order a (p * q) = order a p + order a q"
+proof -
+ def i \<equiv> "order a p"
+ def j \<equiv> "order a q"
+ def t \<equiv> "[:-a, 1:]"
+ have t_dvd_iff: "\<And>u. t dvd u \<longleftrightarrow> poly u a = 0"
+ unfolding t_def by (simp add: dvd_iff_poly_eq_0)
+ assume "p * q \<noteq> 0"
+ then show "order a (p * q) = i + j"
+ apply clarsimp
+ apply (drule order [where a=a and p=p, folded i_def t_def])
+ apply (drule order [where a=a and p=q, folded j_def t_def])
+ apply clarify
+ apply (rule order_unique_lemma [symmetric], fold t_def)
+ apply (erule dvdE)+
+ apply (simp add: power_add t_dvd_iff)
+ done
+qed
+
text{*Now justify the standard squarefree decomposition, i.e. f / gcd(f,f'). *}
-lemma poly_squarefree_decomp_order: "[| poly (pderiv p) \<noteq> poly [];
- poly p = poly (q *** d);
- poly (pderiv p) = poly (e *** d);
- poly d = poly (r *** p +++ s *** pderiv p)
- |] ==> order a q = (if order a p = 0 then 0 else 1)"
-apply (subgoal_tac "order a p = order a q + order a d")
-apply (rule_tac [2] s = "order a (q *** d)" in trans)
-prefer 2 apply (blast intro: order_poly)
-apply (rule_tac [2] order_mult)
- prefer 2 apply force
-apply (case_tac "order a p = 0", simp)
-apply (subgoal_tac "order a (pderiv p) = order a e + order a d")
-apply (rule_tac [2] s = "order a (e *** d)" in trans)
-prefer 2 apply (blast intro: order_poly)
-apply (rule_tac [2] order_mult)
- prefer 2 apply force
-apply (case_tac "poly p = poly []")
-apply (drule_tac p = p in pderiv_zero, simp)
-apply (drule order_pderiv, assumption)
-apply (subgoal_tac "order a (pderiv p) \<le> order a d")
-apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides d")
- prefer 2 apply (simp add: poly_entire order_divides)
-apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides p & ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p) ")
- prefer 3 apply (simp add: order_divides)
- prefer 2 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
-apply (rule_tac x = "r *** qa +++ s *** qaa" in exI)
-apply (simp add: fun_eq poly_add poly_mult left_distrib right_distrib mult_ac del: pexp_Suc pmult_Cons, auto)
+lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
+apply (cases "p = 0", auto)
+apply (drule order_2 [where a=a and p=p])
+apply (erule contrapos_np)
+apply (erule power_le_dvd)
+apply simp
+apply (erule power_le_dvd [OF order_1])
done
+lemma poly_squarefree_decomp_order:
+ assumes "pderiv p \<noteq> 0"
+ and p: "p = q * d"
+ and p': "pderiv p = e * d"
+ and d: "d = r * p + s * pderiv p"
+ shows "order a q = (if order a p = 0 then 0 else 1)"
+proof (rule classical)
+ assume 1: "order a q \<noteq> (if order a p = 0 then 0 else 1)"
+ from `pderiv p \<noteq> 0` have "p \<noteq> 0" by auto
+ with p have "order a p = order a q + order a d"
+ by (simp add: order_mult)
+ with 1 have "order a p \<noteq> 0" by (auto split: if_splits)
+ have "order a (pderiv p) = order a e + order a d"
+ using `pderiv p \<noteq> 0` `pderiv p = e * d` by (simp add: order_mult)
+ have "order a p = Suc (order a (pderiv p))"
+ using `pderiv p \<noteq> 0` `order a p \<noteq> 0` by (rule order_pderiv)
+ have "d \<noteq> 0" using `p \<noteq> 0` `p = q * d` by simp
+ have "([:-a, 1:] ^ (order a (pderiv p))) dvd d"
+ apply (simp add: d)
+ apply (rule dvd_add)
+ apply (rule dvd_mult)
+ apply (simp add: order_divides `p \<noteq> 0`
+ `order a p = Suc (order a (pderiv p))`)
+ apply (rule dvd_mult)
+ apply (simp add: order_divides)
+ done
+ then have "order a (pderiv p) \<le> order a d"
+ using `d \<noteq> 0` by (simp add: order_divides)
+ show ?thesis
+ using `order a p = order a q + order a d`
+ using `order a (pderiv p) = order a e + order a d`
+ using `order a p = Suc (order a (pderiv p))`
+ using `order a (pderiv p) \<le> order a d`
+ by auto
+qed
-lemma poly_squarefree_decomp_order2: "[| poly (pderiv p) \<noteq> poly [];
- poly p = poly (q *** d);
- poly (pderiv p) = poly (e *** d);
- poly d = poly (r *** p +++ s *** pderiv p)
+lemma poly_squarefree_decomp_order2: "[| pderiv p \<noteq> 0;
+ p = q * d;
+ pderiv p = e * d;
+ d = r * p + s * pderiv p
|] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
apply (blast intro: poly_squarefree_decomp_order)
done
-lemma order_pderiv2: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
+lemma order_pderiv2: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
==> (order a (pderiv p) = n) = (order a p = Suc n)"
apply (auto dest: order_pderiv)
done
+definition
+ rsquarefree :: "'a::idom poly => bool" where
+ "rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
+
+lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h:]"
+apply (simp add: pderiv_eq_0_iff)
+apply (case_tac p, auto split: if_splits)
+done
+
lemma rsquarefree_roots:
"rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))"
apply (simp add: rsquarefree_def)
-apply (case_tac "poly p = poly []", simp, simp)
-apply (case_tac "poly (pderiv p) = poly []")
+apply (case_tac "p = 0", simp, simp)
+apply (case_tac "pderiv p = 0")
apply simp
apply (drule pderiv_iszero, clarify)
-apply (subgoal_tac "\<forall>a. order a p = order a [h]")
-apply (simp add: fun_eq)
+apply simp
apply (rule allI)
-apply (cut_tac p = "[h]" and a = a in order_root)
-apply (simp add: fun_eq)
-apply (blast intro: order_poly)
+apply (cut_tac p = "[:h:]" and a = a in order_root)
+apply simp
apply (auto simp add: order_root order_pderiv2)
apply (erule_tac x="a" in allE, simp)
done
-lemma poly_squarefree_decomp: "[| poly (pderiv p) \<noteq> poly [];
- poly p = poly (q *** d);
- poly (pderiv p) = poly (e *** d);
- poly d = poly (r *** p +++ s *** pderiv p)
- |] ==> rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
-apply (frule poly_squarefree_decomp_order2, assumption+)
-apply (case_tac "poly p = poly []")
-apply (blast dest: pderiv_zero)
-apply (simp (no_asm) add: rsquarefree_def order_root del: pmult_Cons)
-apply (simp add: poly_entire del: pmult_Cons)
-done
-*)
+lemma poly_squarefree_decomp:
+ assumes "pderiv p \<noteq> 0"
+ and "p = q * d"
+ and "pderiv p = e * d"
+ and "d = r * p + s * pderiv p"
+ shows "rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
+proof -
+ from `pderiv p \<noteq> 0` have "p \<noteq> 0" by auto
+ with `p = q * d` have "q \<noteq> 0" by simp
+ have "\<forall>a. order a q = (if order a p = 0 then 0 else 1)"
+ using assms by (rule poly_squarefree_decomp_order2)
+ with `p \<noteq> 0` `q \<noteq> 0` show ?thesis
+ by (simp add: rsquarefree_def order_root)
+qed
+
subsection {* Theorems about Limits *}
--- a/src/HOL/Divides.thy Wed Feb 18 19:18:34 2009 +0100
+++ b/src/HOL/Divides.thy Wed Feb 18 17:02:38 2009 -0800
@@ -889,21 +889,9 @@
apply (simp only: dvd_eq_mod_eq_0)
done
-lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
- apply (unfold dvd_def)
- apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
- apply (simp add: power_add)
- done
-
lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct n) auto
-lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
- apply (induct j)
- apply (simp_all add: le_Suc_eq)
- apply (blast dest!: dvd_mult_right)
- done
-
lemma power_dvd_imp_le: "[|i^m dvd i^n; (1::nat) < i|] ==> m \<le> n"
apply (rule power_le_imp_le_exp, assumption)
apply (erule dvd_imp_le, simp)
--- a/src/HOL/IntDiv.thy Wed Feb 18 19:18:34 2009 +0100
+++ b/src/HOL/IntDiv.thy Wed Feb 18 17:02:38 2009 -0800
@@ -1265,9 +1265,9 @@
thus ?thesis by simp
qed
-lemma zdvd_zmult_cancel_disj[simp]:
+lemma zdvd_zmult_cancel_disj:
"(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
-by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel)
+by (rule dvd_mult_cancel_left) (* already declared [simp] *)
theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Feb 18 19:18:34 2009 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Feb 18 17:02:38 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 19:18:34 2009 +0100
+++ b/src/HOL/Polynomial.thy Wed Feb 18 17:02:38 2009 -0800
@@ -611,6 +611,26 @@
unfolding one_poly_def
by (rule degree_pCons_0)
+text {* Lemmas about divisibility *}
+
+lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
+proof -
+ assume "p dvd q"
+ then obtain k where "q = p * k" ..
+ then have "smult a q = p * smult a k" by simp
+ then show "p dvd smult a q" ..
+qed
+
+lemma dvd_smult_cancel:
+ fixes a :: "'a::field"
+ shows "p dvd smult a q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> p dvd q"
+ by (drule dvd_smult [where a="inverse a"]) simp
+
+lemma dvd_smult_iff:
+ fixes a :: "'a::field"
+ shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
+ by (safe elim!: dvd_smult dvd_smult_cancel)
+
instantiation poly :: (comm_semiring_1) recpower
begin
@@ -623,6 +643,9 @@
end
+lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
+by (induct n, simp, auto intro: order_trans degree_mult_le)
+
instance poly :: (comm_ring) comm_ring ..
instance poly :: (comm_ring_1) comm_ring_1 ..
@@ -1097,6 +1120,11 @@
subsection {* Synthetic division *}
+text {*
+ Synthetic division is simply division by the
+ linear polynomial @{term "x - c"}.
+*}
+
definition
synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
where [code del]:
@@ -1208,6 +1236,114 @@
qed
qed
+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 {* Composition of polynomials *}
+
+definition
+ pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+where
+ "pcompose p q = poly_rec 0 (\<lambda>a _ c. [:a:] + q * c) p"
+
+lemma pcompose_0 [simp]: "pcompose 0 q = 0"
+ unfolding pcompose_def by (simp add: poly_rec_0)
+
+lemma pcompose_pCons:
+ "pcompose (pCons a p) q = [:a:] + q * pcompose p q"
+ unfolding pcompose_def by (simp add: poly_rec_pCons)
+
+lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)"
+ by (induct p) (simp_all add: pcompose_pCons)
+
+lemma degree_pcompose_le:
+ "degree (pcompose p q) \<le> degree p * degree q"
+apply (induct p, simp)
+apply (simp add: pcompose_pCons, clarify)
+apply (rule degree_add_le, simp)
+apply (rule order_trans [OF degree_mult_le], simp)
+done
+
+
+subsection {* Order of polynomial roots *}
+
+definition
+ order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat"
+where
+ [code del]:
+ "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
+
+lemma coeff_linear_power:
+ fixes a :: "'a::comm_semiring_1"
+ 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"
+ 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
+
subsection {* Configuration of the code generator *}
--- a/src/HOL/Power.thy Wed Feb 18 19:18:34 2009 +0100
+++ b/src/HOL/Power.thy Wed Feb 18 17:02:38 2009 -0800
@@ -324,6 +324,24 @@
shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
by (cases n, simp_all, rule power_inject_base)
+text {* The divides relation *}
+
+lemma le_imp_power_dvd:
+ fixes a :: "'a::{comm_semiring_1,recpower}"
+ assumes "m \<le> n" shows "a^m dvd a^n"
+proof
+ have "a^n = a^(m + (n - m))"
+ using `m \<le> n` by simp
+ also have "\<dots> = a^m * a^(n - m)"
+ by (rule power_add)
+ finally show "a^n = a^m * a^(n - m)" .
+qed
+
+lemma power_le_dvd:
+ fixes a b :: "'a::{comm_semiring_1,recpower}"
+ shows "a^n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a^m dvd b"
+ by (rule dvd_trans [OF le_imp_power_dvd])
+
subsection{*Exponentiation for the Natural Numbers*}
--- a/src/HOL/Ring_and_Field.thy Wed Feb 18 19:18:34 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Wed Feb 18 17:02:38 2009 -0800
@@ -384,6 +384,26 @@
then show "a * a = b * b" by auto
qed
+lemma dvd_mult_cancel_right [simp]:
+ "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
+proof -
+ have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
+ unfolding dvd_def by (simp add: mult_ac)
+ also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
+ unfolding dvd_def by simp
+ finally show ?thesis .
+qed
+
+lemma dvd_mult_cancel_left [simp]:
+ "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
+proof -
+ have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
+ unfolding dvd_def by (simp add: mult_ac)
+ also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
+ unfolding dvd_def by simp
+ finally show ?thesis .
+qed
+
end
class division_ring = ring_1 + inverse +
--- a/src/HOL/Tools/int_factor_simprocs.ML Wed Feb 18 19:18:34 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML Wed Feb 18 17:02:38 2009 -0800
@@ -263,8 +263,8 @@
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
- val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.intT
- val simplify_meta_eq = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
+ val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
+ val simplify_meta_eq = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
);
(*Version for all fields, including unordered ones (type complex).*)
@@ -288,8 +288,8 @@
("int_mod_cancel_factor",
["((l::int) * m) mod n", "(l::int) mod (m * n)"],
K IntModCancelFactor.proc),
- ("int_dvd_cancel_factor",
- ["((l::int) * m) dvd n", "(l::int) dvd (m * n)"],
+ ("dvd_cancel_factor",
+ ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
K IntDvdCancelFactor.proc),
("divide_cancel_factor",
["((l::'a::{division_by_zero,field}) * m) / n",
--- a/src/HOL/ex/ThreeDivides.thy Wed Feb 18 19:18:34 2009 +0100
+++ b/src/HOL/ex/ThreeDivides.thy Wed Feb 18 17:02:38 2009 -0800
@@ -187,9 +187,8 @@
"nd = nlen (m div 10) \<Longrightarrow>
m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
by blast
- have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger
- then obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..
- then have cdef: "c = m mod 10" by arith
+ obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10"
+ and cdef: "c = m mod 10" by simp
show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)"
proof -
from `Suc nd = nlen m`