--- a/src/HOL/Hyperreal/EvenOdd.thy Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/EvenOdd.thy Fri Mar 05 15:18:59 2004 +0100
@@ -1,115 +1,72 @@
(* Title : EvenOdd.thy
+ ID: $Id$
Author : Jacques D. Fleuriot
Copyright : 1999 University of Edinburgh
- Description : Even and odd numbers defined
*)
-header{*Compatibility file from Parity*}
+header{*Even and Odd Numbers: Compatibility file for Parity*}
theory EvenOdd = NthRoot:
subsection{*General Lemmas About Division*}
-lemma div_add_self_two_is_m: "(m + m) div 2 = (m::nat)"
-by arith
-declare div_add_self_two_is_m [simp]
-
-lemma div_mult_self_Suc_Suc: "Suc(Suc(m*2)) div 2 = Suc m"
-by arith
-declare div_mult_self_Suc_Suc [simp]
+lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
+apply (induct_tac "m")
+apply (simp_all add: mod_Suc)
+done
-lemma div_mult_self_Suc_Suc2: "Suc(Suc(2*m)) div 2 = Suc m"
-by arith
-declare div_mult_self_Suc_Suc2 [simp]
+declare Suc_times_mod_eq [of "number_of w", standard, simp]
-lemma div_add_self_Suc_Suc: "Suc(Suc(m + m)) div 2 = Suc m"
-by arith
-declare div_add_self_Suc_Suc [simp]
-
-lemma mod_two_Suc_2m: "Suc (2 * m) mod 2 = 1"
-apply (induct_tac "m")
-apply (auto simp add: mod_Suc)
-done
-declare mod_two_Suc_2m [simp]
+lemma [simp]: "n div k \<le> (Suc n) div k"
+by (simp add: div_le_mono)
-lemma Suc_n_le_Suc_Suc_n_div_2: "Suc n div 2 \<le> Suc (Suc n) div 2"
+lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2"
by arith
-declare Suc_n_le_Suc_Suc_n_div_2 [simp]
-lemma Suc_n_div_2_gt_zero: "(0::nat) < n ==> 0 < (n + 1) div 2"
-by arith
-declare Suc_n_div_2_gt_zero [simp]
-
-lemma le_Suc_n_div_2: "n div 2 \<le> (Suc n) div 2"
+lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2"
by arith
-declare le_Suc_n_div_2 [simp]
-
-lemma div_2_gt_zero: "(1::nat) < n ==> 0 < n div 2"
-by arith
-declare div_2_gt_zero [simp]
-lemma mod_mult_self3: "(k*n + m) mod n = m mod (n::nat)"
+lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)"
by (simp add: mult_ac add_ac)
-declare mod_mult_self3 [simp]
-lemma mod_mult_self4: "Suc (k*n + m) mod n = Suc m mod n"
+lemma mod_mult_self4 [simp]: "Suc (k*n + m) mod n = Suc m mod n"
proof -
have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
also have "... = Suc m mod n" by (rule mod_mult_self3)
finally show ?thesis .
qed
-declare mod_mult_self4 [simp]
-
-lemma nat_mod_idem [simp]: "m mod n mod n = (m mod n :: nat)"
-by (case_tac "n=0", auto)
lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
apply (subst mod_Suc [of m])
apply (subst mod_Suc [of "m mod n"], simp)
done
-lemma lemma_4n_add_2_div_2_eq: "((4 * n) + 2) div 2 = (2::nat) * n + 1"
-by arith
-declare lemma_4n_add_2_div_2_eq [simp]
-
-lemma lemma_Suc_Suc_4n_div_2_eq: "(Suc(Suc(4 * n))) div 2 = (2::nat) * n + 1"
-by arith
-declare lemma_Suc_Suc_4n_div_2_eq [simp]
-
-lemma lemma_Suc_Suc_4n_div_2_eq2: "(Suc(Suc(n * 4))) div 2 = (2::nat) * n + 1"
-by arith
-declare lemma_Suc_Suc_4n_div_2_eq2 [simp]
-
subsection{*More Even/Odd Results*}
-lemma even_mult_two_ex: "even(n) = (EX m::nat. n = 2*m)"
+lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)"
by (simp add: even_nat_equiv_def2 numeral_2_eq_2)
-lemma odd_Suc_mult_two_ex: "odd(n) = (EX m. n = Suc (2*m))"
+lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))"
by (simp add: odd_nat_equiv_def2 numeral_2_eq_2)
-lemma even_add: "even(m + n::nat) = (even m = even n)"
+lemma even_add [simp]: "even(m + n::nat) = (even m = even n)"
by auto
-declare even_add [iff]
-lemma odd_add: "odd(m + n::nat) = (odd m ~= odd n)"
+lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)"
by auto
-declare odd_add [iff]
-lemma lemma_even_div2: "even (n::nat) ==> (n + 1) div 2 = n div 2"
+lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2"
apply (simp add: numeral_2_eq_2)
apply (subst div_Suc)
apply (simp add: even_nat_mod_two_eq_zero)
done
-declare lemma_even_div2 [simp]
-lemma lemma_not_even_div2: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
+lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
apply (simp add: numeral_2_eq_2)
apply (subst div_Suc)
apply (simp add: odd_nat_mod_two_eq_one)
done
-declare lemma_not_even_div2 [simp]
lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))"
by (case_tac "n", auto)
@@ -119,9 +76,6 @@
apply (subst mod_Suc, simp)
done
-declare neg_one_odd_power [simp]
-declare neg_one_even_power [simp]
-
lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst])
apply (simp add: even_num_iff)
@@ -132,32 +86,19 @@
ML
{*
-val even_Suc = thm"Parity.even_nat_suc";
+val even_nat_Suc = thm"Parity.even_nat_Suc";
val even_mult_two_ex = thm "even_mult_two_ex";
val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex";
-val div_add_self_two_is_m = thm "div_add_self_two_is_m";
-val div_mult_self_Suc_Suc = thm "div_mult_self_Suc_Suc";
-val div_mult_self_Suc_Suc2 = thm "div_mult_self_Suc_Suc2";
-val div_add_self_Suc_Suc = thm "div_add_self_Suc_Suc";
val even_add = thm "even_add";
val odd_add = thm "odd_add";
-val mod_two_Suc_2m = thm "mod_two_Suc_2m";
-val Suc_n_le_Suc_Suc_n_div_2 = thm "Suc_n_le_Suc_Suc_n_div_2";
val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero";
-val le_Suc_n_div_2 = thm "le_Suc_n_div_2";
val div_2_gt_zero = thm "div_2_gt_zero";
-val lemma_even_div2 = thm "lemma_even_div2";
-val lemma_not_even_div2 = thm "lemma_not_even_div2";
val even_num_iff = thm "even_num_iff";
-val mod_mult_self3 = thm "mod_mult_self3";
-val mod_mult_self4 = thm "mod_mult_self4";
-val nat_mod_idem = thm "nat_mod_idem";
+val nat_mod_div_trivial = thm "nat_mod_div_trivial";
+val nat_mod_mod_trivial = thm "nat_mod_mod_trivial";
val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod";
val even_even_mod_4_iff = thm "even_even_mod_4_iff";
-val lemma_4n_add_2_div_2_eq = thm "lemma_4n_add_2_div_2_eq";
-val lemma_Suc_Suc_4n_div_2_eq = thm "lemma_Suc_Suc_4n_div_2_eq";
-val lemma_Suc_Suc_4n_div_2_eq2 = thm "lemma_Suc_Suc_4n_div_2_eq2";
val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2";
val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2";
*}
--- a/src/HOL/Hyperreal/HSeries.thy Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy Fri Mar 05 15:18:59 2004 +0100
@@ -157,7 +157,7 @@
lemma sumhr_minus_one_realpow_zero [simp]:
"sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
by (simp del: realpow_Suc
- add: sumhr hypnat_add double_lemma hypreal_zero_def
+ add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def
hypnat_zero_def hypnat_omega_def)
lemma sumhr_interval_const:
--- a/src/HOL/Hyperreal/HyperPow.thy Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy Fri Mar 05 15:18:59 2004 +0100
@@ -1,7 +1,6 @@
(* Title : HyperPow.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
- Description : Powers theory for hyperreals
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
*)
@@ -41,9 +40,6 @@
apply (simp (no_asm))
done
-lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)"
-by (simp add: power_abs)
-
lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
by (auto simp add: zero_le_mult_iff)
declare hrealpow_two_le [simp]
@@ -91,17 +87,6 @@
done
declare two_hrealpow_gt [simp]
-lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)"
-by (induct_tac "n", auto)
-
-lemma double_lemma: "n+n = (2*n::nat)"
-by auto
-
-(*ugh: need to get rid fo the n+n*)
-lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)"
-by (auto simp add: double_lemma hrealpow_minus_one)
-declare hrealpow_minus_one2 [simp]
-
lemma hrealpow:
"Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
apply (induct_tac "m")
@@ -291,7 +276,7 @@
apply simp
apply (simp only: hypreal_one_def)
apply (rule eq_Abs_hypnat [of n])
-apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus
+apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus
left_distrib)
done
declare hyperpow_minus_one2 [simp]
@@ -369,7 +354,6 @@
ML
{*
val hrealpow_two = thm "hrealpow_two";
-val hrabs_hrealpow_minus_one = thm "hrabs_hrealpow_minus_one";
val hrealpow_two_le = thm "hrealpow_two_le";
val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order";
val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2";
@@ -379,9 +363,6 @@
val hrabs_hrealpow_two = thm "hrabs_hrealpow_two";
val two_hrealpow_ge_one = thm "two_hrealpow_ge_one";
val two_hrealpow_gt = thm "two_hrealpow_gt";
-val hrealpow_minus_one = thm "hrealpow_minus_one";
-val double_lemma = thm "double_lemma";
-val hrealpow_minus_one2 = thm "hrealpow_minus_one2";
val hrealpow = thm "hrealpow";
val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand";
val hypreal_of_real_power = thm "hypreal_of_real_power";
--- a/src/HOL/Hyperreal/Integration.ML Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/Integration.ML Fri Mar 05 15:18:59 2004 +0100
@@ -634,14 +634,14 @@
by (dtac (partition RS iffD1) 1 THEN Step_tac 1);
by (rtac ccontr 1 THEN dtac leI 1);
by Auto_tac;
-val lemma_additivity1 = result();
+qed "lemma_additivity1";
Goal "[| a <= D n; partition(a,D n) D |] ==> psize D <= n";
by (rtac ccontr 1 THEN dtac not_leE 1);
by (ftac (partition RS iffD1) 1 THEN Step_tac 1);
by (forw_inst_tac [("r","Suc n")] partition_ub 1);
by (auto_tac (claset() addSDs [spec],simpset()));
-val lemma_additivity2 = result();
+qed "lemma_additivity2";
Goal "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)";
by (auto_tac (claset(),simpset() addsimps [partition]));
@@ -734,7 +734,7 @@
by Auto_tac;
by (dres_inst_tac [("n","na")] partition_lt_gen 1);
by Auto_tac;
-val lemma_additivity3 = result();
+qed "lemma_additivity3";
Goalw [psize_def] "psize (%x. k) = 0";
by Auto_tac;
@@ -746,7 +746,7 @@
\ ==> False";
by (forw_inst_tac [("m","n")] partition_lt_cancel 1);
by (auto_tac (claset() addIs [lemma_additivity3],simpset()));
-val lemma_additivity3a = result();
+qed "lemma_additivity3a";
Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D - n";
by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
--- a/src/HOL/Hyperreal/Lim.ML Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Fri Mar 05 15:18:59 2004 +0100
@@ -1,17 +1,17 @@
(* Title : Lim.ML
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
- Description : Theory of limits, continuity and
+ Description : Theory of limits, continuity and
differentiation of real=>real functions
*)
-fun ARITH_PROVE str = prove_goal thy str
+fun ARITH_PROVE str = prove_goal thy str
(fn prems => [cut_facts_tac prems 1,arith_tac 1]);
(*---------------------------------------------------------------
- Theory of limits, continuity and differentiation of
- real=>real functions
+ Theory of limits, continuity and differentiation of
+ real=>real functions
----------------------------------------------------------------*)
Goalw [LIM_def] "(%x. k) -- x --> k";
@@ -22,11 +22,11 @@
(***-----------------------------------------------------------***)
(*** Some Purely Standard Proofs - Can be used for comparison ***)
(***-----------------------------------------------------------***)
-
-(*---------------
- LIM_add
+
+(*---------------
+ LIM_add
---------------*)
-Goalw [LIM_def]
+Goalw [LIM_def]
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)";
by (Clarify_tac 1);
by (REPEAT(dres_inst_tac [("x","r/2")] spec 1));
@@ -37,11 +37,11 @@
by (res_inst_tac [("x","sa")] exI 2);
by (res_inst_tac [("x","sa")] exI 3);
by Safe_tac;
-by (REPEAT(dres_inst_tac [("x","xa")] spec 1)
+by (REPEAT(dres_inst_tac [("x","xa")] spec 1)
THEN step_tac (claset() addSEs [order_less_trans]) 1);
-by (REPEAT(dres_inst_tac [("x","xa")] spec 2)
+by (REPEAT(dres_inst_tac [("x","xa")] spec 2)
THEN step_tac (claset() addSEs [order_less_trans]) 2);
-by (REPEAT(dres_inst_tac [("x","xa")] spec 3)
+by (REPEAT(dres_inst_tac [("x","xa")] spec 3)
THEN step_tac (claset() addSEs [order_less_trans]) 3);
by (ALLGOALS(rtac (abs_sum_triangle_ineq RS order_le_less_trans)));
by (ALLGOALS(rtac (real_sum_of_halves RS subst)));
@@ -50,8 +50,8 @@
Goalw [LIM_def] "f -- a --> L ==> (%x. -f(x)) -- a --> -L";
by (subgoal_tac "ALL x. abs(- f x + L) = abs(f x + - L)" 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [real_abs_def]) 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [real_abs_def]) 1);
qed "LIM_minus";
(*----------------------------------------------
@@ -82,7 +82,7 @@
by (ALLGOALS(dres_inst_tac [("y","s")] real_dense));
by Safe_tac;
by (ALLGOALS(res_inst_tac [("x","r + x")] exI));
-by Auto_tac;
+by Auto_tac;
qed "LIM_not_zero";
(* [| k \\<noteq> 0; (%x. k) -- x --> 0 |] ==> R *)
@@ -115,17 +115,17 @@
by (cut_facts_tac [real_zero_less_one] 1);
by (asm_full_simp_tac (simpset() addsimps [abs_mult]) 1);
by (Clarify_tac 1);
-by (res_inst_tac [("x","s"),("y","sa")]
+by (res_inst_tac [("x","s"),("y","sa")]
linorder_cases 1);
by (res_inst_tac [("x","s")] exI 1);
by (res_inst_tac [("x","sa")] exI 2);
by (res_inst_tac [("x","sa")] exI 3);
by Safe_tac;
-by (REPEAT(dres_inst_tac [("x","xa")] spec 1)
+by (REPEAT(dres_inst_tac [("x","xa")] spec 1)
THEN step_tac (claset() addSEs [order_less_trans]) 1);
-by (REPEAT(dres_inst_tac [("x","xa")] spec 2)
+by (REPEAT(dres_inst_tac [("x","xa")] spec 2)
THEN step_tac (claset() addSEs [order_less_trans]) 2);
-by (REPEAT(dres_inst_tac [("x","xa")] spec 3)
+by (REPEAT(dres_inst_tac [("x","xa")] spec 3)
THEN step_tac (claset() addSEs [order_less_trans]) 3);
by (ALLGOALS(res_inst_tac [("t","r")] (real_mult_1 RS subst)));
by (ALLGOALS(rtac abs_mult_less));
@@ -139,7 +139,7 @@
(*--------------------------------------------------------------
Limits are equal for functions equal except at limit point
--------------------------------------------------------------*)
-Goalw [LIM_def]
+Goalw [LIM_def]
"[| \\<forall>x. x \\<noteq> a --> (f x = g x) |] \
\ ==> (f -- a --> l) = (g -- a --> l)";
by (auto_tac (claset(), simpset() addsimps [real_add_minus_iff]));
@@ -157,14 +157,14 @@
(*--------------------------------------------------------------
Standard and NS definitions of Limit
--------------------------------------------------------------*)
-Goalw [LIM_def,NSLIM_def,approx_def]
+Goalw [LIM_def,NSLIM_def,approx_def]
"f -- x --> L ==> f -- x --NS> L";
by (asm_full_simp_tac
(simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
by Safe_tac;
by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
by (auto_tac (claset(),
- simpset() addsimps [real_add_minus_iff, starfun, hypreal_minus,
+ simpset() addsimps [real_add_minus_iff, starfun, hypreal_minus,
hypreal_of_real_def, hypreal_add]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2 THEN Step_tac 1);
by (dres_inst_tac [("x","u")] spec 1 THEN Clarify_tac 1);
@@ -175,7 +175,7 @@
by (dtac FreeUltrafilterNat_all 1);
by (Ultra_tac 1);
qed "LIM_NSLIM";
-
+
(*---------------------------------------------------------------------
Limit: NS definition ==> standard definition
---------------------------------------------------------------------*)
@@ -184,11 +184,11 @@
\ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \
\ ==> \\<forall>n::nat. \\<exists>xa. xa \\<noteq> x & \
\ abs(xa + -x) < inverse(real(Suc n)) & r \\<le> abs(f xa + -L)";
-by (Clarify_tac 1);
+by (Clarify_tac 1);
by (cut_inst_tac [("n1","n")]
(real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1);
by Auto_tac;
-val lemma_LIM = result();
+qed "lemma_LIM";
Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \
\ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \
@@ -197,20 +197,20 @@
by (dtac lemma_LIM 1);
by (dtac choice 1);
by (Blast_tac 1);
-val lemma_skolemize_LIM2 = result();
+qed "lemma_skolemize_LIM2";
Goal "\\<forall>n. X n \\<noteq> x & \
\ abs (X n + - x) < inverse (real(Suc n)) & \
\ r \\<le> abs (f (X n) + - L) ==> \
\ \\<forall>n. abs (X n + - x) < inverse (real(Suc n))";
by (Auto_tac );
-val lemma_simp = result();
-
+qed "lemma_simp";
+
(*-------------------
NSLIM => LIM
-------------------*)
-Goalw [LIM_def,NSLIM_def,approx_def]
+Goalw [LIM_def,NSLIM_def,approx_def]
"f -- x --NS> L ==> f -- x --> L";
by (asm_full_simp_tac
(simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
@@ -221,14 +221,14 @@
by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1);
by (auto_tac
(claset(),
- simpset() addsimps [starfun, hypreal_minus,
+ simpset() addsimps [starfun, hypreal_minus,
hypreal_of_real_def,hypreal_add]));
by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1);
by (asm_full_simp_tac
- (simpset() addsimps
+ (simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def,
hypreal_minus, hypreal_add]) 1);
-by (Blast_tac 1);
+by (Blast_tac 1);
by (dtac spec 1 THEN dtac mp 1 THEN assume_tac 1);
by (dtac FreeUltrafilterNat_all 1);
by (Ultra_tac 1);
@@ -290,9 +290,9 @@
(*----------------------------------------------
NSLIM_minus
----------------------------------------------*)
-Goalw [NSLIM_def]
+Goalw [NSLIM_def]
"f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L";
-by Auto_tac;
+by Auto_tac;
qed "NSLIM_minus";
Goal "f -- a --> L ==> (%x. -f(x)) -- a --> -L";
@@ -316,13 +316,13 @@
(*-----------------------------
NSLIM_inverse
-----------------------------*)
-Goalw [NSLIM_def]
+Goalw [NSLIM_def]
"[| f -- a --NS> L; L \\<noteq> 0 |] \
\ ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
by (Clarify_tac 1);
by (dtac spec 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_real_approx_inverse]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_approx_inverse]));
qed "NSLIM_inverse";
Goal "[| f -- a --> L; \
@@ -430,24 +430,24 @@
Derivatives and Continuity - NS and Standard properties
-----------------------------------------------------------------------------*)
(*---------------
- Continuity
+ Continuity
---------------*)
-Goalw [isNSCont_def]
+Goalw [isNSCont_def]
"[| isNSCont f a; y \\<approx> hypreal_of_real a |] \
\ ==> ( *f* f) y \\<approx> hypreal_of_real (f a)";
by (Blast_tac 1);
qed "isNSContD";
-Goalw [isNSCont_def,NSLIM_def]
+Goalw [isNSCont_def,NSLIM_def]
"isNSCont f a ==> f -- a --NS> (f a) ";
by (Blast_tac 1);
qed "isNSCont_NSLIM";
-Goalw [isNSCont_def,NSLIM_def]
+Goalw [isNSCont_def,NSLIM_def]
"f -- a --NS> (f a) ==> isNSCont f a";
by Auto_tac;
-by (res_inst_tac [("Q","y = hypreal_of_real a")]
+by (res_inst_tac [("Q","y = hypreal_of_real a")]
(excluded_middle RS disjE) 1);
by Auto_tac;
qed "NSLIM_isNSCont";
@@ -465,12 +465,12 @@
in terms of standard limit
---------------------------------------------*)
Goal "(isNSCont f a) = (f -- a --> (f a))";
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[LIM_NSLIM_iff,isNSCont_NSLIM_iff]) 1);
qed "isNSCont_LIM_iff";
(*-----------------------------------------------
- Moreover, it's trivial now that NS continuity
+ Moreover, it's trivial now that NS continuity
is equivalent to standard continuity
-----------------------------------------------*)
Goalw [isCont_def] "(isNSCont f a) = (isCont f a)";
@@ -478,14 +478,14 @@
qed "isNSCont_isCont_iff";
(*----------------------------------------
- Standard continuity ==> NS continuity
+ Standard continuity ==> NS continuity
----------------------------------------*)
Goal "isCont f a ==> isNSCont f a";
by (etac (isNSCont_isCont_iff RS iffD2) 1);
qed "isCont_isNSCont";
(*----------------------------------------
- NS continuity ==> Standard continuity
+ NS continuity ==> Standard continuity
----------------------------------------*)
Goal "isNSCont f a ==> isCont f a";
by (etac (isNSCont_isCont_iff RS iffD1) 1);
@@ -502,7 +502,7 @@
by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2);
by Safe_tac;
by (Asm_full_simp_tac 1);
-by (rtac ((mem_infmal_iff RS iffD2) RS
+by (rtac ((mem_infmal_iff RS iffD2) RS
(Infinitesimal_add_approx_self RS approx_sym)) 1);
by (rtac (approx_minus_iff2 RS iffD1) 4);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 3);
@@ -526,7 +526,7 @@
qed "isCont_iff";
(*--------------------------------------------------------------------------
- Immediate application of nonstandard criterion for continuity can offer
+ Immediate application of nonstandard criterion for continuity can offer
very simple proofs of some standard property of continuous functions
--------------------------------------------------------------------------*)
(*------------------------
@@ -562,7 +562,7 @@
qed "isCont_o2";
Goalw [isNSCont_def] "isNSCont f a ==> isNSCont (%x. - f x) a";
-by Auto_tac;
+by Auto_tac;
qed "isNSCont_minus";
Goal "isCont f a ==> isCont (%x. - f x) a";
@@ -570,17 +570,17 @@
isNSCont_minus]));
qed "isCont_minus";
-Goalw [isCont_def]
+Goalw [isCont_def]
"[| isCont f x; f x \\<noteq> 0 |] ==> isCont (%x. inverse (f x)) x";
by (blast_tac (claset() addIs [LIM_inverse]) 1);
qed "isCont_inverse";
Goal "[| isNSCont f x; f x \\<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x";
-by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps
+by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps
[isNSCont_isCont_iff]));
qed "isNSCont_inverse";
-Goalw [real_diff_def]
+Goalw [real_diff_def]
"[| isCont f a; isCont g a |] ==> isCont (%x. f(x) - g(x)) a";
by (auto_tac (claset() addIs [isCont_add,isCont_minus],simpset()));
qed "isCont_diff";
@@ -610,9 +610,9 @@
(****************************************************************
(%* Leave as commented until I add topology theory or remove? *%)
(%*------------------------------------------------------------
- Elementary topology proof for a characterisation of
- continuity now: a function f is continuous if and only
- if the inverse image, {x. f(x) \\<in> A}, of any open set A
+ Elementary topology proof for a characterisation of
+ continuity now: a function f is continuous if and only
+ if the inverse image, {x. f(x) \\<in> A}, of any open set A
is always an open set
------------------------------------------------------------*%)
Goal "[| isNSopen A; \\<forall>x. isNSCont f x |] \
@@ -629,8 +629,8 @@
Goalw [isNSCont_def]
"\\<forall>A. isNSopen A --> isNSopen {x. f x \\<in> A} \
\ ==> isNSCont f x";
-by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
- (approx_minus_iff RS iffD2)],simpset() addsimps
+by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
+ (approx_minus_iff RS iffD2)],simpset() addsimps
[Infinitesimal_def,SReal_iff]));
by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
by (etac (isNSopen_open_interval RSN (2,impE)) 1);
@@ -658,7 +658,7 @@
(*-----------------------------------------------------------------
Uniform continuity
------------------------------------------------------------------*)
-Goalw [isNSUCont_def]
+Goalw [isNSUCont_def]
"[| isNSUCont f; x \\<approx> y|] ==> ( *f* f) x \\<approx> ( *f* f) y";
by (Blast_tac 1);
qed "isNSUContD";
@@ -666,13 +666,13 @@
Goalw [isUCont_def,isCont_def,LIM_def]
"isUCont f ==> isCont f x";
by (Clarify_tac 1);
-by (dtac spec 1);
-by (Blast_tac 1);
+by (dtac spec 1);
+by (Blast_tac 1);
qed "isUCont_isCont";
-Goalw [isNSUCont_def,isUCont_def,approx_def]
+Goalw [isNSUCont_def,isUCont_def,approx_def]
"isUCont f ==> isNSUCont f";
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff]) 1);
by Safe_tac;
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -693,11 +693,11 @@
\ ==> \\<forall>n::nat. \\<exists>z y. \
\ abs(z + -y) < inverse(real(Suc n)) & \
\ r \\<le> abs(f z + -f y)";
-by (Clarify_tac 1);
+by (Clarify_tac 1);
by (cut_inst_tac [("n1","n")]
(real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1);
by Auto_tac;
-val lemma_LIMu = result();
+qed "lemma_LIMu";
Goal "\\<forall>s. 0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
\ ==> \\<exists>X Y. \\<forall>n::nat. \
@@ -708,17 +708,17 @@
by Safe_tac;
by (dtac choice 1);
by (Blast_tac 1);
-val lemma_skolemize_LIM2u = result();
+qed "lemma_skolemize_LIM2u";
Goal "\\<forall>n. abs (X n + -Y n) < inverse (real(Suc n)) & \
\ r \\<le> abs (f (X n) + - f(Y n)) ==> \
\ \\<forall>n. abs (X n + - Y n) < inverse (real(Suc n))";
by (Auto_tac );
-val lemma_simpu = result();
+qed "lemma_simpu";
-Goalw [isNSUCont_def,isUCont_def,approx_def]
+Goalw [isNSUCont_def,isUCont_def,approx_def]
"isNSUCont f ==> isUCont f";
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff]) 1);
by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]);
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
@@ -730,7 +730,7 @@
(simpset() addsimps [starfun, hypreal_minus,hypreal_add]) 1);
by Auto_tac;
by (dtac (lemma_simpu RS real_seq_to_hypreal_Infinitesimal2) 1);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[Infinitesimal_FreeUltrafilterNat_iff, hypreal_minus,hypreal_add]) 1);
by (Blast_tac 1);
by (rotate_tac 2 1);
@@ -743,20 +743,20 @@
(*------------------------------------------------------------------
Derivatives
------------------------------------------------------------------*)
-Goalw [deriv_def]
+Goalw [deriv_def]
"(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --> D)";
-by (Blast_tac 1);
+by (Blast_tac 1);
qed "DERIV_iff";
-Goalw [deriv_def]
+Goalw [deriv_def]
"(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)";
by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
qed "DERIV_NS_iff";
-Goalw [deriv_def]
+Goalw [deriv_def]
"DERIV f x :> D \
\ ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D";
-by (Blast_tac 1);
+by (Blast_tac 1);
qed "DERIVD";
Goalw [deriv_def] "DERIV f x :> D ==> \
@@ -765,16 +765,16 @@
qed "NS_DERIVD";
(* Uniqueness *)
-Goalw [deriv_def]
+Goalw [deriv_def]
"[| DERIV f x :> D; DERIV f x :> E |] ==> D = E";
by (blast_tac (claset() addIs [LIM_unique]) 1);
qed "DERIV_unique";
-Goalw [nsderiv_def]
+Goalw [nsderiv_def]
"[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E";
by (cut_facts_tac [Infinitesimal_epsilon, hypreal_epsilon_not_zero] 1);
-by (auto_tac (claset() addSDs [inst "x" "epsilon" bspec]
- addSIs [inj_hypreal_of_real RS injD]
+by (auto_tac (claset() addSDs [inst "x" "epsilon" bspec]
+ addSIs [inj_hypreal_of_real RS injD]
addDs [approx_trans3],
simpset()));
qed "NSDeriv_unique";
@@ -783,22 +783,22 @@
Differentiable
------------------------------------------------------------------------*)
-Goalw [differentiable_def]
+Goalw [differentiable_def]
"f differentiable x ==> \\<exists>D. DERIV f x :> D";
by (assume_tac 1);
qed "differentiableD";
-Goalw [differentiable_def]
+Goalw [differentiable_def]
"DERIV f x :> D ==> f differentiable x";
by (Blast_tac 1);
qed "differentiableI";
-Goalw [NSdifferentiable_def]
+Goalw [NSdifferentiable_def]
"f NSdifferentiable x ==> \\<exists>D. NSDERIV f x :> D";
by (assume_tac 1);
qed "NSdifferentiableD";
-Goalw [NSdifferentiable_def]
+Goalw [NSdifferentiable_def]
"NSDERIV f x :> D ==> f NSdifferentiable x";
by (Blast_tac 1);
qed "NSdifferentiableI";
@@ -807,7 +807,7 @@
Alternative definition for differentiability
-------------------------------------------------------*)
-Goalw [LIM_def]
+Goalw [LIM_def]
"((%h. (f(a + h) + - f(a))/h) -- 0 --> D) = \
\ ((%x. (f(x) + -f(a)) / (x + -a)) -- a --> D)";
by Safe_tac;
@@ -830,11 +830,11 @@
Equivalence of NS and standard defs of differentiation
-------------------------------------------------------*)
(*-------------------------------------------
- First NSDERIV in terms of NSLIM
+ First NSDERIV in terms of NSLIM
-------------------------------------------*)
(*--- first equivalence ---*)
-Goalw [nsderiv_def,NSLIM_def]
+Goalw [nsderiv_def,NSLIM_def]
"(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)";
by Auto_tac;
by (dres_inst_tac [("x","xa")] bspec 1);
@@ -847,7 +847,7 @@
(*--- second equivalence ---*)
Goal "(NSDERIV f x :> D) = \
\ ((%z. (f(z) + -f(x)) / (z + -x)) -- x --NS> D)";
-by (full_simp_tac (simpset() addsimps
+by (full_simp_tac (simpset() addsimps
[NSDERIV_NSLIM_iff, DERIV_LIM_iff, LIM_NSLIM_iff RS sym]) 1);
qed "NSDERIV_NSLIM_iff2";
@@ -875,8 +875,8 @@
by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
by (subgoal_tac "( *f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
by (auto_tac (claset(),
- simpset() addsimps [real_diff_def, hypreal_diff_def,
- (approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
+ simpset() addsimps [real_diff_def, hypreal_diff_def,
+ (approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
Infinitesimal_subset_HFinite RS subsetD]));
qed "NSDERIVD5";
@@ -912,19 +912,19 @@
qed "NSDERIV_DERIV_iff";
(*---------------------------------------------------
- Differentiability implies continuity
+ Differentiability implies continuity
nice and simple "algebraic" proof
--------------------------------------------------*)
Goalw [nsderiv_def]
"NSDERIV f x :> D ==> isNSCont f x";
-by (auto_tac (claset(),simpset() addsimps
+by (auto_tac (claset(),simpset() addsimps
[isNSCont_NSLIM_iff,NSLIM_def]));
by (dtac (approx_minus_iff RS iffD1) 1);
by (dtac (hypreal_not_eq_minus_iff RS iffD1) 1);
by (dres_inst_tac [("x","-hypreal_of_real x + xa")] bspec 1);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[hypreal_add_assoc RS sym]) 2);
-by (auto_tac (claset(),simpset() addsimps
+by (auto_tac (claset(),simpset() addsimps
[mem_infmal_iff RS sym,hypreal_add_commute]));
by (dres_inst_tac [("c","xa + -hypreal_of_real x")] approx_mult1 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite
@@ -938,14 +938,14 @@
(* Now Sandard proof *)
Goal "DERIV f x :> D ==> isCont f x";
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[NSDERIV_DERIV_iff RS sym, isNSCont_isCont_iff RS sym,
NSDERIV_isNSCont]) 1);
qed "DERIV_isCont";
(*----------------------------------------------------------------------------
Differentiation rules for combinations of functions
- follow from clear, straightforard, algebraic
+ follow from clear, straightforard, algebraic
manipulations
----------------------------------------------------------------------------*)
(*-------------------------
@@ -988,23 +988,23 @@
(*-----------------------------------------------------
Product of functions - Proof is trivial but tedious
- and long due to rearrangement of terms
+ and long due to rearrangement of terms
----------------------------------------------------*)
Goal "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))";
by (simp_tac (simpset() addsimps [right_distrib]) 1);
-val lemma_nsderiv1 = result();
+qed "lemma_nsderiv1";
Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\<noteq> 0; \
\ z \\<in> Infinitesimal; yb \\<in> Infinitesimal |] \
\ ==> x + y \\<approx> 0";
-by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1
+by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1
THEN assume_tac 1);
by (thin_tac "(x + y) / z = hypreal_of_real D + yb" 1);
by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2, HFinite_add],
simpset() addsimps [hypreal_mult_assoc, mem_infmal_iff RS sym]));
by (etac (Infinitesimal_subset_HFinite RS subsetD) 1);
-val lemma_nsderiv2 = result();
+qed "lemma_nsderiv2";
Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \
@@ -1013,7 +1013,7 @@
by (REPEAT (Step_tac 1));
by (auto_tac (claset(),
simpset() addsimps [starfun_lambda_cancel, lemma_nsderiv1]));
-by (simp_tac (simpset() addsimps [add_divide_distrib]) 1);
+by (simp_tac (simpset() addsimps [add_divide_distrib]) 1);
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
by (auto_tac (claset(),
simpset() delsimps [times_divide_eq_right]
@@ -1021,7 +1021,7 @@
by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1);
by (dtac (approx_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
by (auto_tac (claset() addSIs [approx_add_mono1],
- simpset() addsimps [left_distrib, right_distrib,
+ simpset() addsimps [left_distrib, right_distrib,
hypreal_mult_commute, hypreal_add_assoc]));
by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")]
(hypreal_add_commute RS subst) 1);
@@ -1043,7 +1043,7 @@
---------------------------*)
Goal "NSDERIV f x :> D \
\ ==> NSDERIV (%x. c * f x) x :> c*D";
-by (asm_full_simp_tac
+by (asm_full_simp_tac
(HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff,
minus_mult_right, right_distrib RS sym]) 1);
by (etac (NSLIM_const RS NSLIM_mult) 1);
@@ -1052,10 +1052,10 @@
(* let's do the standard proof though theorem *)
(* LIM_mult2 follows from a NS proof *)
-Goalw [deriv_def]
+Goalw [deriv_def]
"DERIV f x :> D \
\ ==> DERIV (%x. c * f x) x :> c*D";
-by (asm_full_simp_tac
+by (asm_full_simp_tac
(HOL_ss addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff,
minus_mult_right, right_distrib RS sym]) 1);
by (etac (LIM_const RS LIM_mult2) 1);
@@ -1069,12 +1069,12 @@
by (dtac NSLIM_minus 1);
by (subgoal_tac "ALL a::real. ALL b. - a + b = - (a + - b)" 1);
by (asm_full_simp_tac (HOL_ss addsimps [thm"minus_divide_left" RS sym]) 1);
-by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
qed "NSDERIV_minus";
Goal "DERIV f x :> D \
\ ==> DERIV (%x. -(f x)) x :> -D";
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[NSDERIV_minus,NSDERIV_DERIV_iff RS sym]) 1);
qed "DERIV_minus";
@@ -1106,7 +1106,7 @@
(*---------------------------------------------------------------
(NS) Increment
---------------------------------------------------------------*)
-Goalw [increment_def]
+Goalw [increment_def]
"f NSdifferentiable x ==> \
\ increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \
\ -hypreal_of_real (f x)";
@@ -1125,7 +1125,7 @@
by (forw_inst_tac [("h","h")] incrementI2 1 THEN rewtac nsderiv_def);
by (dtac bspec 1 THEN Auto_tac);
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1);
-by (forw_inst_tac [("b1","hypreal_of_real(D) + y")]
+by (forw_inst_tac [("b1","hypreal_of_real(D) + y")]
((hypreal_mult_right_cancel RS iffD2)) 1);
by (thin_tac "(( *f* f) (hypreal_of_real(x) + h) + \
\ - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2);
@@ -1139,14 +1139,14 @@
Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \
\ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = \
\ hypreal_of_real(D)*h + e*h";
-by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2]
+by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2]
addSIs [increment_thm]) 1);
qed "increment_thm2";
Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \
\ ==> increment f x h \\<approx> 0";
-by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs
- [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps
+by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs
+ [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps
[left_distrib RS sym,mem_infmal_iff RS sym]));
by (etac (Infinitesimal_subset_HFinite RS subsetD) 1);
qed "increment_approx_zero";
@@ -1155,13 +1155,13 @@
Similarly to the above, the chain rule admits an entirely
straightforward derivation. Compare this with Harrison's
HOL proof of the chain rule, which proved to be trickier and
- required an alternative characterisation of differentiability-
+ required an alternative characterisation of differentiability-
the so-called Carathedory derivative. Our main problem is
manipulation of terms.
--------------------------------------------------------------*)
(* lemmas *)
-Goalw [nsderiv_def]
+Goalw [nsderiv_def]
"[| NSDERIV g x :> D; \
\ ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
\ xa \\<in> Infinitesimal;\
@@ -1172,19 +1172,19 @@
qed "NSDERIV_zero";
(* can be proved differently using NSLIM_isCont_iff *)
-Goalw [nsderiv_def]
+Goalw [nsderiv_def]
"[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> 0 |] \
-\ ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0";
-by (asm_full_simp_tac (simpset() addsimps
+\ ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0";
+by (asm_full_simp_tac (simpset() addsimps
[mem_infmal_iff RS sym]) 1);
by (rtac Infinitesimal_ratio 1);
by (rtac approx_hypreal_of_real_HFinite 3);
by Auto_tac;
qed "NSDERIV_approx";
-(*---------------------------------------------------------------
- from one version of differentiability
-
+(*---------------------------------------------------------------
+ from one version of differentiability
+
f(x) - f(a)
--------------- \\<approx> Db
x - a
@@ -1200,8 +1200,8 @@
simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
qed "NSDERIVD1";
-(*--------------------------------------------------------------
- from other version of differentiability
+(*--------------------------------------------------------------
+ from other version of differentiability
f(x + h) - f(x)
----------------- \\<approx> Db
@@ -1211,12 +1211,12 @@
\ ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
\ \\<approx> hypreal_of_real(Db)";
by (auto_tac (claset(),
- simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def,
+ simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def,
mem_infmal_iff, starfun_lambda_cancel]));
qed "NSDERIVD2";
Goal "(z::hypreal) \\<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)";
-by Auto_tac;
+by Auto_tac;
qed "lemma_chain";
(*------------------------------------------------------
@@ -1287,11 +1287,11 @@
Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))";
by (induct_tac "n" 1);
by (dtac (DERIV_Id RS DERIV_mult) 2);
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() addsimps [real_of_nat_Suc, left_distrib]));
by (case_tac "0 < n" 1);
by (dres_inst_tac [("x","x")] realpow_minus_mult 1);
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() addsimps [real_mult_assoc, real_add_commute]));
qed "DERIV_pow";
@@ -1301,7 +1301,7 @@
qed "NSDERIV_pow";
(*---------------------------------------------------------------
- Power of -1
+ Power of -1
---------------------------------------------------------------*)
(*Can't get rid of x \\<noteq> 0 because it isn't continuous at zero*)
@@ -1309,30 +1309,30 @@
"x \\<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))";
by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
by (ftac Infinitesimal_add_not_zero 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2);
by (auto_tac (claset(),
- simpset() addsimps [starfun_inverse_inverse, realpow_two]
+ simpset() addsimps [starfun_inverse_inverse, realpow_two]
delsimps [minus_mult_left RS sym,
minus_mult_right RS sym]));
by (asm_full_simp_tac
(simpset() addsimps [hypreal_inverse_add,
- hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym]
- @ add_ac @ mult_ac
+ hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym]
+ @ add_ac @ mult_ac
delsimps [inverse_mult_distrib,inverse_minus_eq,
minus_mult_left RS sym,
minus_mult_right RS sym] ) 1);
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym,
- right_distrib]
- delsimps [minus_mult_left RS sym,
+ right_distrib]
+ delsimps [minus_mult_left RS sym,
minus_mult_right RS sym]) 1);
-by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")]
+by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")]
approx_trans 1);
by (rtac inverse_add_Infinitesimal_approx2 1);
-by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal],
+by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal],
simpset() addsimps [hypreal_minus_inverse RS sym,
HFinite_minus_iff]));
-by (rtac Infinitesimal_HFinite_mult2 1);
-by Auto_tac;
+by (rtac Infinitesimal_HFinite_mult2 1);
+by Auto_tac;
qed "NSDERIV_inverse";
@@ -1342,7 +1342,7 @@
qed "DERIV_inverse";
(*--------------------------------------------------------------
- Derivative of inverse
+ Derivative of inverse
-------------------------------------------------------------*)
Goal "[| DERIV f x :> d; f(x) \\<noteq> 0 |] \
\ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
@@ -1359,7 +1359,7 @@
qed "NSDERIV_inverse_fun";
(*--------------------------------------------------------------
- Derivative of quotient
+ Derivative of quotient
-------------------------------------------------------------*)
Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> 0 |] \
\ ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ Suc (Suc 0))";
@@ -1368,7 +1368,7 @@
by (REPEAT(assume_tac 1));
by (asm_full_simp_tac
(simpset() addsimps [real_divide_def, right_distrib,
- power_inverse,minus_mult_left] @ mult_ac
+ power_inverse,minus_mult_left] @ mult_ac
delsimps [realpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1);
qed "DERIV_quotient";
@@ -1378,7 +1378,7 @@
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
DERIV_quotient] delsimps [realpow_Suc]) 1);
qed "NSDERIV_quotient";
-
+
(* ------------------------------------------------------------------------ *)
(* Caratheodory formulation of derivative at a point: standard proof *)
(* ------------------------------------------------------------------------ *)
@@ -1386,7 +1386,7 @@
Goal "(DERIV f x :> l) = \
\ (\\<exists>g. (\\<forall>z. f z - f x = g z * (z - x)) & isCont g x & g x = l)";
by Safe_tac;
-by (res_inst_tac
+by (res_inst_tac
[("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (0::real)"]));
@@ -1404,7 +1404,7 @@
(* How about a NS proof? *)
Goal "(\\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \
\ ==> NSDERIV f x :> l";
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() delsimprocs field_cancel_factor
addsimps [NSDERIV_iff2]));
by (auto_tac (claset(),
@@ -1413,7 +1413,7 @@
hypreal_diff_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1);
qed "CARAT_DERIVD";
-
+
(*--------------------------------------------------------------------------*)
@@ -1443,13 +1443,13 @@
\ \\<forall>n. f(n) \\<le> g(n) |] \
\ ==> Bseq g";
by (stac (Bseq_minus_iff RS sym) 1);
-by (res_inst_tac [("g","%x. -(f x)")] f_inc_g_dec_Beq_f 1);
-by Auto_tac;
+by (res_inst_tac [("g","%x. -(f x)")] f_inc_g_dec_Beq_f 1);
+by Auto_tac;
qed "f_inc_g_dec_Beq_g";
Goal "[| \\<forall>n. f n \\<le> f (Suc n); convergent f |] ==> f n \\<le> lim f";
by (rtac (linorder_not_less RS iffD1) 1);
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() addsimps [convergent_LIMSEQ_iff, LIMSEQ_iff, monoseq_Suc]));
by (dtac real_less_sum_gt_zero 1);
by (dres_inst_tac [("x","f n + - lim f")] spec 1);
@@ -1460,21 +1460,21 @@
by (induct_tac "no" 2);
by (auto_tac (claset() addIs [order_trans],
simpset() addsimps [real_diff_def, real_abs_def]));
-by (dres_inst_tac [("x","f(no + n)"),("no1","no")]
+by (dres_inst_tac [("x","f(no + n)"),("no1","no")]
(lemma_f_mono_add RSN (2,order_less_le_trans)) 1);
by (auto_tac (claset(), simpset() addsimps [add_commute]));
qed "f_inc_imp_le_lim";
Goal "convergent g ==> lim (%x. - g x) = - (lim g)";
-by (rtac (LIMSEQ_minus RS limI) 1);
-by (asm_full_simp_tac (simpset() addsimps [convergent_LIMSEQ_iff]) 1);
+by (rtac (LIMSEQ_minus RS limI) 1);
+by (asm_full_simp_tac (simpset() addsimps [convergent_LIMSEQ_iff]) 1);
qed "lim_uminus";
Goal "[| \\<forall>n. g(Suc n) \\<le> g(n); convergent g |] ==> lim g \\<le> g n";
by (subgoal_tac "- (g n) \\<le> - (lim g)" 1);
by (cut_inst_tac [("f", "%x. - (g x)")] f_inc_imp_le_lim 2);
-by (auto_tac (claset(),
- simpset() addsimps [lim_uminus, convergent_minus_iff RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [lim_uminus, convergent_minus_iff RS sym]));
qed "g_dec_imp_lim_le";
Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \
@@ -1485,15 +1485,15 @@
by (subgoal_tac "monoseq f & monoseq g" 1);
by (force_tac (claset(), simpset() addsimps [LIMSEQ_iff,monoseq_Suc]) 2);
by (subgoal_tac "Bseq f & Bseq g" 1);
-by (blast_tac (claset() addIs [f_inc_g_dec_Beq_f, f_inc_g_dec_Beq_g]) 2);
+by (blast_tac (claset() addIs [f_inc_g_dec_Beq_f, f_inc_g_dec_Beq_g]) 2);
by (auto_tac (claset() addSDs [Bseq_monoseq_convergent],
simpset() addsimps [convergent_LIMSEQ_iff]));
by (res_inst_tac [("x","lim f")] exI 1);
by (res_inst_tac [("x","lim g")] exI 1);
by (auto_tac (claset() addIs [LIMSEQ_le], simpset()));
-by (auto_tac (claset(),
- simpset() addsimps [f_inc_imp_le_lim, g_dec_imp_lim_le,
- convergent_LIMSEQ_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [f_inc_imp_le_lim, g_dec_imp_lim_le,
+ convergent_LIMSEQ_iff]));
qed "lemma_nest";
Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \
@@ -1513,44 +1513,44 @@
\ \\<forall>n. fst (Bolzano_bisect P a b n) \\<le> snd (Bolzano_bisect P a b n)";
by (rtac allI 1);
by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [Let_def, split_def]));
+by (auto_tac (claset(), simpset() addsimps [Let_def, split_def]));
qed "Bolzano_bisect_le";
Goal "a \\<le> b ==> \
\ \\<forall>n. fst(Bolzano_bisect P a b n) \\<le> fst (Bolzano_bisect P a b (Suc n))";
by (rtac allI 1);
by (induct_tac "n" 1);
-by (auto_tac (claset(),
- simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
+by (auto_tac (claset(),
+ simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
qed "Bolzano_bisect_fst_le_Suc";
Goal "a \\<le> b ==> \
\ \\<forall>n. snd(Bolzano_bisect P a b (Suc n)) \\<le> snd (Bolzano_bisect P a b n)";
by (rtac allI 1);
by (induct_tac "n" 1);
-by (auto_tac (claset(),
- simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
+by (auto_tac (claset(),
+ simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
qed "Bolzano_bisect_Suc_le_snd";
Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)";
-by Auto_tac;
-by (dres_inst_tac [("f","%u. (1/2)*u")] arg_cong 1);
-by Auto_tac;
+by Auto_tac;
+by (dres_inst_tac [("f","%u. (1/2)*u")] arg_cong 1);
+by Auto_tac;
qed "eq_divide_2_times_iff";
Goal "a \\<le> b ==> \
\ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
\ (b-a) / (2 ^ n)";
by (induct_tac "n" 1);
-by (auto_tac (claset(),
- simpset() addsimps [eq_divide_2_times_iff, add_divide_distrib,
+by (auto_tac (claset(),
+ simpset() addsimps [eq_divide_2_times_iff, add_divide_distrib,
Let_def, split_def]));
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() addsimps (add_ac@[Bolzano_bisect_le, real_diff_def])));
qed "Bolzano_bisect_diff";
val Bolzano_nest_unique =
- [Bolzano_bisect_fst_le_Suc, Bolzano_bisect_Suc_le_snd, Bolzano_bisect_le]
+ [Bolzano_bisect_fst_le_Suc, Bolzano_bisect_Suc_le_snd, Bolzano_bisect_le]
MRS lemma_nest_unique;
(*P_prem is a looping simprule, so it works better if it isn't an assumption*)
@@ -1560,19 +1560,19 @@
\ ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
by (cut_facts_tac rest 1);
by (induct_tac "n" 1);
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() delsimps [surjective_pairing RS sym]
- addsimps [notP_prem, Let_def, split_def]));
+ addsimps [notP_prem, Let_def, split_def]));
by (swap_res_tac [P_prem] 1);
-by (assume_tac 1);
-by (auto_tac (claset(), simpset() addsimps [Bolzano_bisect_le]));
+by (assume_tac 1);
+by (auto_tac (claset(), simpset() addsimps [Bolzano_bisect_le]));
qed "not_P_Bolzano_bisect";
(*Now we re-package P_prem as a formula*)
Goal "[| \\<forall>a b c. P(a,b) & P(b,c) & a \\<le> b & b \\<le> c --> P(a,c); \
\ ~ P(a,b); a \\<le> b |] ==> \
\ \\<forall>n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))";
-by (blast_tac (claset() addSEs [not_P_Bolzano_bisect RSN (2,rev_notE)]) 1);
+by (blast_tac (claset() addSEs [not_P_Bolzano_bisect RSN (2,rev_notE)]) 1);
qed "not_P_Bolzano_bisect'";
@@ -1585,9 +1585,9 @@
by (REPEAT (assume_tac 1));
by (rtac LIMSEQ_minus_cancel 1);
by (asm_simp_tac (simpset() addsimps [Bolzano_bisect_diff,
- LIMSEQ_divide_realpow_zero]) 1);
+ LIMSEQ_divide_realpow_zero]) 1);
by (rtac ccontr 1);
-by (dtac not_P_Bolzano_bisect' 1);
+by (dtac not_P_Bolzano_bisect' 1);
by (REPEAT (assume_tac 1));
by (rename_tac "l" 1);
by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
@@ -1603,12 +1603,12 @@
by Safe_tac;
by (ALLGOALS Asm_simp_tac);
by (res_inst_tac [("y","abs(fst(Bolzano_bisect P a b(no + noa)) - l) + \
-\ abs(snd(Bolzano_bisect P a b(no + noa)) - l)")]
+\ abs(snd(Bolzano_bisect P a b(no + noa)) - l)")]
order_le_less_trans 1);
-by (asm_simp_tac (simpset() addsimps [real_abs_def]) 1);
+by (asm_simp_tac (simpset() addsimps [real_abs_def]) 1);
by (rtac (real_sum_of_halves RS subst) 1);
by (rtac add_strict_mono 1);
-by (ALLGOALS
+by (ALLGOALS
(asm_full_simp_tac (simpset() addsimps [symmetric real_diff_def])));
qed "lemma_BOLZANO";
@@ -1618,7 +1618,7 @@
\ (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)))) \
\ --> (\\<forall>a b. a \\<le> b --> P(a,b))";
by (Clarify_tac 1);
-by (blast_tac (claset() addIs [lemma_BOLZANO]) 1);
+by (blast_tac (claset() addIs [lemma_BOLZANO]) 1);
qed "lemma_BOLZANO2";
@@ -1633,7 +1633,7 @@
by (rtac contrapos_pp 1);
by (assume_tac 1);
by (cut_inst_tac
- [("P","%(u,v). a \\<le> u & u \\<le> v & v \\<le> b --> ~(f(u) \\<le> y & y \\<le> f(v))")]
+ [("P","%(u,v). a \\<le> u & u \\<le> v & v \\<le> b --> ~(f(u) \\<le> y & y \\<le> f(v))")]
lemma_BOLZANO2 1);
by Safe_tac;
by (ALLGOALS(Asm_full_simp_tac));
@@ -1700,7 +1700,7 @@
Addsimps [abs_real_of_nat_cancel];
Goal "~ abs(x) + (1::real) < x";
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
by (auto_tac (claset() addIs [abs_ge_self RS order_trans],simpset()));
qed "abs_add_one_not_less_self";
Addsimps [abs_add_one_not_less_self];
@@ -1709,7 +1709,7 @@
Goal "[| a \\<le> b; \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x |]\
\ ==> \\<exists>M. \\<forall>x. a \\<le> x & x \\<le> b --> f(x) \\<le> M";
by (cut_inst_tac [("P","%(u,v). a \\<le> u & u \\<le> v & v \\<le> b --> \
-\ (\\<exists>M. \\<forall>x. u \\<le> x & x \\<le> v --> f x \\<le> M)")]
+\ (\\<exists>M. \\<forall>x. u \\<le> x & x \\<le> v --> f x \\<le> M)")]
lemma_BOLZANO2 1);
by Safe_tac;
by (ALLGOALS Asm_full_simp_tac);
@@ -1717,21 +1717,21 @@
by (cut_inst_tac [("x","M"),("y","Ma")] linorder_linear 1);
by Safe_tac;
by (res_inst_tac [("x","Ma")] exI 1);
-by (Clarify_tac 1);
+by (Clarify_tac 1);
by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1);
-by (Force_tac 1);
+by (Force_tac 1);
by (res_inst_tac [("x","M")] exI 1);
-by (Clarify_tac 1);
+by (Clarify_tac 1);
by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1);
-by (Force_tac 1);
+by (Force_tac 1);
by (case_tac "a \\<le> x & x \\<le> b" 1);
by (res_inst_tac [("x","1")] exI 2);
-by (Force_tac 2);
+by (Force_tac 2);
by (asm_full_simp_tac (simpset() addsimps [LIM_def,isCont_iff]) 1);
by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac);
by (thin_tac "\\<forall>M. \\<exists>x. a \\<le> x & x \\<le> b & ~ f x \\<le> M" 1);
by (dres_inst_tac [("x","1")] spec 1);
-by Auto_tac;
+by Auto_tac;
by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1);
by (res_inst_tac [("x","abs(f x) + 1")] exI 1 THEN Clarify_tac 1);
by (dres_inst_tac [("x","xa - x")] spec 1);
@@ -1773,7 +1773,7 @@
by (ftac isCont_has_Ub 1 THEN assume_tac 1);
by (Clarify_tac 1);
by (res_inst_tac [("x","M")] exI 1);
-by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
by (rtac ccontr 1);
by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> f x < M" 1 THEN Step_tac 1);
by (rtac ccontr 2 THEN dtac (linorder_not_less RS iffD1) 2);
@@ -1784,20 +1784,20 @@
by (EVERY[rtac isCont_inverse 2, rtac isCont_diff 2, rtac notI 4]);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [diff_eq_eq])));
by (Blast_tac 2);
-by (subgoal_tac
+by (subgoal_tac
"\\<exists>k. \\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x \\<le> k" 1);
by (rtac isCont_bounded 2);
by Safe_tac;
by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> 0 < inverse(M - f(x))" 1);
-by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [less_diff_eq]) 2);
-by (subgoal_tac
+by (subgoal_tac
"\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + 1)" 1);
by Safe_tac;
by (res_inst_tac [("y","k")] order_le_less_trans 2);
by (asm_full_simp_tac (simpset() addsimps [zero_less_one]) 3);
-by (Asm_full_simp_tac 2);
+by (Asm_full_simp_tac 2);
by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> \
\ inverse(k + 1) < inverse((%x. inverse(M - (f x))) x)" 1);
by Safe_tac;
@@ -1809,13 +1809,13 @@
by (dtac (le_diff_eq RS iffD1) 1);
by (REPEAT(dres_inst_tac [("x","a")] spec 1));
by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [inverse_eq_divide, pos_divide_le_eq]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [inverse_eq_divide, pos_divide_le_eq]) 1);
by (cut_inst_tac [("a","k"),("b","M-f a")] zero_less_mult_iff 1);
-by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
(*last one*)
by (REPEAT(dres_inst_tac [("x","x")] spec 1));
-by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
qed "isCont_eq_Ub";
@@ -1863,18 +1863,18 @@
(* If f'(x) > 0 then x is locally strictly increasing at the right *)
(*----------------------------------------------------------------------------*)
-Goalw [deriv_def,LIM_def]
+Goalw [deriv_def,LIM_def]
"[| DERIV f x :> l; 0 < l |] \
\ ==> \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x + h))";
by (dtac spec 1 THEN Auto_tac);
by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
by (subgoal_tac "0 < l*h" 1);
-by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 2);
+by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 2);
by (dres_inst_tac [("x","h")] spec 1);
by (asm_full_simp_tac
- (simpset() addsimps [real_abs_def, inverse_eq_divide,
+ (simpset() addsimps [real_abs_def, inverse_eq_divide,
pos_le_divide_eq, pos_less_divide_eq]
- addsplits [split_if_asm]) 1);
+ addsplits [split_if_asm]) 1);
qed "DERIV_left_inc";
val prems = goalw (the_context()) [deriv_def,LIM_def]
@@ -1885,12 +1885,12 @@
by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
by (dres_inst_tac [("x","-h")] spec 1);
by (asm_full_simp_tac
- (simpset() addsimps [real_abs_def, inverse_eq_divide,
+ (simpset() addsimps [real_abs_def, inverse_eq_divide,
pos_less_divide_eq,
symmetric real_diff_def]
addsplits [split_if_asm]) 1);
by (subgoal_tac "0 < (f (x - h) - f x)/h" 1);
-by (asm_full_simp_tac (simpset() addsimps [pos_less_divide_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [pos_less_divide_eq]) 1);
by (cut_facts_tac prems 1);
by (arith_tac 1);
qed "DERIV_left_dec";
@@ -1899,10 +1899,10 @@
by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac);
by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
by (subgoal_tac "l*h < 0" 1);
-by (asm_full_simp_tac (simpset() addsimps [mult_less_0_iff]) 2);
+by (asm_full_simp_tac (simpset() addsimps [mult_less_0_iff]) 2);
by (dres_inst_tac [("x","-h")] spec 1);
by (asm_full_simp_tac
- (simpset() addsimps [real_abs_def, inverse_eq_divide,
+ (simpset() addsimps [real_abs_def, inverse_eq_divide,
pos_less_divide_eq,
symmetric real_diff_def]
addsplits [split_if_asm]
@@ -1910,7 +1910,7 @@
by (subgoal_tac "0 < (f (x - h) - f x)/h" 1);
by (arith_tac 2);
by (asm_full_simp_tac
- (simpset() addsimps [pos_less_divide_eq]) 1);
+ (simpset() addsimps [pos_less_divide_eq]) 1);
qed "DERIV_left_dec";
*)
@@ -1938,8 +1938,8 @@
Goal "[| DERIV f x :> l; \
\ \\<exists>d::real. 0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \
\ ==> l = 0";
-by (dtac (DERIV_minus RS DERIV_local_max) 1);
-by Auto_tac;
+by (dtac (DERIV_minus RS DERIV_local_max) 1);
+by Auto_tac;
qed "DERIV_local_min";
(*----------------------------------------------------------------------------*)
@@ -2051,7 +2051,7 @@
Goal "f a - (f b - f a)/(b - a) * a = \
\ f b - (f b - f a)/(b - a) * (b::real)";
by (case_tac "a = b" 1);
-by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
by (res_inst_tac [("c1","b - a")] (real_mult_left_cancel RS iffD1) 1);
by (arith_tac 1);
by (auto_tac (claset(), simpset() addsimps [right_diff_distrib]));
@@ -2069,8 +2069,8 @@
by Safe_tac;
by (rtac isCont_diff 1 THEN Blast_tac 1);
by (rtac (isCont_const RS isCont_mult) 1);
-by (rtac isCont_Id 1);
-by (dres_inst_tac [("P", "%x. ?Pre x --> f differentiable x"),
+by (rtac isCont_Id 1);
+by (dres_inst_tac [("P", "%x. ?Pre x --> f differentiable x"),
("x","x")] spec 1);
by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
by Safe_tac;
@@ -2080,15 +2080,15 @@
by (subgoal_tac "(%x. (f b - f a) * x / (b - a)) = \
\ op * ((f b - f a) / (b - a))" 1);
by (rtac ext 2 THEN Simp_tac 2);
-by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
(*final case*)
by (res_inst_tac [("x","((f(b) - f(a)) / (b - a))")] exI 1);
by (res_inst_tac [("x","z")] exI 1);
by Safe_tac;
-by (Asm_full_simp_tac 2);
+by (Asm_full_simp_tac 2);
by (subgoal_tac "DERIV (%x. ((f(b) - f(a)) / (b - a)) * x) z :> \
\ ((f(b) - f(a)) / (b - a))" 1);
-by (rtac DERIV_cmult_Id 2);
+by (rtac DERIV_cmult_Id 2);
by (dtac DERIV_add 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [real_add_assoc, real_diff_def]) 1);
qed "MVT";
@@ -2103,7 +2103,7 @@
\ ==> (f b = f a)";
by (dtac MVT 1 THEN assume_tac 1);
by (blast_tac (claset() addIs [differentiableI]) 1);
-by (auto_tac (claset() addSDs [DERIV_unique],simpset()
+by (auto_tac (claset() addSDs [DERIV_unique],simpset()
addsimps [diff_eq_eq]));
qed "DERIV_isconst_end";
@@ -2136,7 +2136,7 @@
by (res_inst_tac [("x","a"),("y","b")] linorder_cases 1);
by Auto_tac;
by (ALLGOALS(dres_inst_tac [("f","f")] MVT));
-by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps
+by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps
[differentiable_def]));
by (auto_tac (claset() addDs [DERIV_unique],
simpset() addsimps [left_distrib, real_diff_def]));
@@ -2144,17 +2144,17 @@
Goal "[|a \\<noteq> b; \\<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k";
by (res_inst_tac [("c1","b - a")] (real_mult_right_cancel RS iffD1) 1);
-by (auto_tac (claset() addSDs [DERIV_const_ratio_const],
+by (auto_tac (claset() addSDs [DERIV_const_ratio_const],
simpset() addsimps [real_mult_assoc]));
qed "DERIV_const_ratio_const2";
Goal "((a + b) /2 - a) = (b - a)/(2::real)";
-by Auto_tac;
+by Auto_tac;
qed "real_average_minus_first";
Addsimps [real_average_minus_first];
Goal "((b + a)/2 - a) = (b - a)/(2::real)";
-by Auto_tac;
+by Auto_tac;
qed "real_average_minus_second";
Addsimps [real_average_minus_second];
@@ -2167,13 +2167,13 @@
by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2);
by (dtac real_less_half_sum 1);
-by (dtac real_gt_half_sum 2);
+by (dtac real_gt_half_sum 2);
by (ftac (real_not_refl2 RS DERIV_const_ratio_const2) 1 THEN assume_tac 1);
by (dtac ((real_not_refl2 RS not_sym) RS DERIV_const_ratio_const2) 2
THEN assume_tac 2);
-by (ALLGOALS (dres_inst_tac [("f","%u. (b-a)*u")] arg_cong));
-by (auto_tac (claset(), simpset() addsimps [inverse_eq_divide]));
-by (asm_full_simp_tac (simpset() addsimps [real_add_commute, eq_commute]) 1);
+by (ALLGOALS (dres_inst_tac [("f","%u. (b-a)*u")] arg_cong));
+by (auto_tac (claset(), simpset() addsimps [inverse_eq_divide]));
+by (asm_full_simp_tac (simpset() addsimps [real_add_commute, eq_commute]) 1);
qed "DERIV_const_average";
@@ -2190,7 +2190,7 @@
by (forw_inst_tac [("x","x - d")] spec 1);
by (forw_inst_tac [("x","x + d")] spec 1);
by Safe_tac;
-by (cut_inst_tac [("x","f(x - d)"),("y","f(x + d)")]
+by (cut_inst_tac [("x","f(x - d)"),("y","f(x + d)")]
(ARITH_PROVE "x \\<le> y | y \\<le> (x::real)") 4);
by (etac disjE 4);
by (REPEAT(arith_tac 1));
@@ -2224,7 +2224,7 @@
Goal "[|0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
\ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
\ ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(x) \\<le> f(z))";
-by (auto_tac (claset() addSDs [(asm_full_simplify (simpset())
+by (auto_tac (claset() addSDs [(asm_full_simplify (simpset())
(read_instantiate [("f","%x. - f x"),("g","%y. g(-y)"),("x","x"),("d","d")]
lemma_isCont_inj))],simpset() addsimps [isCont_minus]));
qed "lemma_isCont_inj2";
@@ -2244,7 +2244,7 @@
\ abs(y - f(x)) \\<le> e --> \
\ (\\<exists>z. abs(z - x) \\<le> d & (f z = y)))";
by (ftac order_less_imp_le 1);
-by (dtac (lemma_le RS (asm_full_simplify (simpset()) (read_instantiate
+by (dtac (lemma_le RS (asm_full_simplify (simpset()) (read_instantiate
[("f","f"),("a","x - d"),("b","x + d")] isCont_Lb_Ub))) 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
@@ -2255,7 +2255,7 @@
by Safe_tac;
by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> 0 < y - (x::real)") 1);
by (dres_inst_tac [("x","f x")] (ARITH_PROVE "x < y ==> 0 < y - (x::real)") 1);
-by (dres_inst_tac [("d1.0","f x - L"),("d2.0","M - f x")]
+by (dres_inst_tac [("d1.0","f x - L"),("d2.0","M - f x")]
(real_lbound_gt_zero) 1);
by Safe_tac;
by (res_inst_tac [("x","e")] exI 1);
--- a/src/HOL/Hyperreal/Poly.ML Fri Mar 05 11:43:55 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1204 +0,0 @@
-(* Title: Poly.ML
- Author: Jacques D. Fleuriot
- Copyright: 2000 University of Edinburgh
- Description: Properties of real polynomials following
- John Harrison's HOL-Light implementation.
- Some early theorems by Lucas Dixon
-*)
-
-Goal "p +++ [] = p";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed "padd_Nil2";
-Addsimps [padd_Nil2];
-
-Goal "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)";
-by Auto_tac;
-qed "padd_Cons_Cons";
-
-Goal "-- [] = []";
-by (rewtac poly_minus_def);
-by (Auto_tac);
-qed "pminus_Nil";
-Addsimps [pminus_Nil];
-
-Goal "[h1] *** p1 = h1 %* p1";
-by (Simp_tac 1);
-qed "pmult_singleton";
-
-Goal "1 %* t = t";
-by (induct_tac "t" 1);
-by Auto_tac;
-qed "poly_ident_mult";
-Addsimps [poly_ident_mult];
-
-Goal "[a] +++ ((0)#t) = (a#t)";
-by (Simp_tac 1);
-qed "poly_simple_add_Cons";
-Addsimps [poly_simple_add_Cons];
-
-(*-------------------------------------------------------------------------*)
-(* Handy general properties *)
-(*-------------------------------------------------------------------------*)
-
-Goal "b +++ a = a +++ b";
-by (subgoal_tac "ALL a. b +++ a = a +++ b" 1);
-by (induct_tac "b" 2);
-by Auto_tac;
-by (rtac (padd_Cons RS ssubst) 1);
-by (case_tac "aa" 1);
-by Auto_tac;
-qed "padd_commut";
-
-Goal "(a +++ b) +++ c = a +++ (b +++ c)";
-by (subgoal_tac "ALL b c. (a +++ b) +++ c = a +++ (b +++ c)" 1);
-by (Asm_simp_tac 1);
-by (induct_tac "a" 1);
-by (Step_tac 2);
-by (case_tac "b" 2);
-by (Asm_simp_tac 2);
-by (Asm_simp_tac 2);
-by (Asm_simp_tac 1);
-qed "padd_assoc";
-
-Goal "a %* ( p +++ q ) = (a %* p +++ a %* q)";
-by (subgoal_tac "ALL q. a %* ( p +++ q ) = (a %* p +++ a %* q) " 1);
-by (induct_tac "p" 2);
-by (Simp_tac 2);
-by (rtac allI 2 );
-by (case_tac "q" 2);
-by (Asm_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [right_distrib] ) 2);
-by (Asm_simp_tac 1);
-qed "poly_cmult_distr";
-
-Goal "[0, 1] *** t = ((0)#t)";
-by (induct_tac "t" 1);
-by (Simp_tac 1);
-by (simp_tac (simpset() addsimps [poly_ident_mult, padd_commut]) 1);
-by (case_tac "list" 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_ident_mult, padd_commut]) 1);
-qed "pmult_by_x";
-Addsimps [pmult_by_x];
-
-
-(*-------------------------------------------------------------------------*)
-(* properties of evaluation of polynomials. *)
-(*-------------------------------------------------------------------------*)
-
-Goal "poly (p1 +++ p2) x = poly p1 x + poly p2 x";
-by (subgoal_tac "ALL p2. poly (p1 +++ p2) x = poly( p1 ) x + poly( p2 ) x" 1);
-by (induct_tac "p1" 2);
-by Auto_tac;
-by (case_tac "p2" 1);
-by (auto_tac (claset(),simpset() addsimps [right_distrib]));
-qed "poly_add";
-
-Goal "poly (c %* p) x = c * poly p x";
-by (induct_tac "p" 1);
-by (case_tac "x=0" 2);
-by (auto_tac (claset(),simpset() addsimps [right_distrib]
- @ mult_ac));
-qed "poly_cmult";
-
-Goalw [poly_minus_def] "poly (-- p) x = - (poly p x)";
-by (auto_tac (claset(),simpset() addsimps [poly_cmult]));
-qed "poly_minus";
-
-Goal "poly (p1 *** p2) x = poly p1 x * poly p2 x";
-by (subgoal_tac "ALL p2. poly (p1 *** p2) x = poly p1 x * poly p2 x" 1);
-by (Asm_simp_tac 1);
-by (induct_tac "p1" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_cmult]));
-by (case_tac "list" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_cmult,poly_add,
- left_distrib,right_distrib] @ mult_ac));
-qed "poly_mult";
-
-Goal "poly (p %^ n) x = (poly p x) ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_cmult, poly_mult]));
-qed "poly_exp";
-
-(*-------------------------------------------------------------------------*)
-(* More Polynomial Evaluation Lemmas *)
-(*-------------------------------------------------------------------------*)
-
-Goal "poly (a +++ []) x = poly a x";
-by (Simp_tac 1);
-qed "poly_add_rzero";
-Addsimps [poly_add_rzero];
-
-Goal "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x";
-by (simp_tac (simpset() addsimps [poly_mult,real_mult_assoc]) 1);
-qed "poly_mult_assoc";
-
-Goal "poly (p *** []) x = 0";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed "poly_mult_Nil2";
-Addsimps [poly_mult_Nil2];
-
-Goal "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d ) x";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [poly_mult,real_mult_assoc]));
-qed "poly_exp_add";
-
-(*-------------------------------------------------------------------------*)
-(* The derivative *)
-(*-------------------------------------------------------------------------*)
-
-Goalw [pderiv_def] "pderiv [] = []";
-by (Simp_tac 1);
-qed "pderiv_Nil";
-Addsimps [pderiv_Nil];
-
-Goalw [pderiv_def] "pderiv [c] = []";
-by (Simp_tac 1);
-qed "pderiv_singleton";
-Addsimps [pderiv_singleton];
-
-Goalw [pderiv_def] "pderiv (h#t) = pderiv_aux 1 t";
-by (Simp_tac 1);
-qed "pderiv_Cons";
-
-Goal "DERIV f x :> D ==> DERIV (%x. (f x) * c) x :> D * c";
-by (auto_tac (claset() addIs [DERIV_cmult,real_mult_commute RS subst],
- simpset() addsimps [real_mult_commute]));
-qed "DERIV_cmult2";
-
-Goal "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)";
-by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_pow 1);
-by (Simp_tac 1);
-qed "DERIV_pow2";
-Addsimps [DERIV_pow2,DERIV_pow];
-
-Goal "ALL n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :> \
- \ x ^ n * poly (pderiv_aux (Suc n) p) x ";
-by (induct_tac "p" 1);
-by (auto_tac (claset() addSIs [DERIV_add,DERIV_cmult2],simpset() addsimps
- [pderiv_def,right_distrib,real_mult_assoc RS sym] delsimps
- [realpow_Suc]));
-by (rtac (real_mult_commute RS subst) 1);
-by (simp_tac (simpset() delsimps [realpow_Suc]) 1);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_commute,realpow_Suc RS sym]
- delsimps [realpow_Suc]) 1);
-qed "lemma_DERIV_poly1";
-
-Goal "DERIV (%x. (x ^ (Suc n) * poly p x)) x :> \
- \ x ^ n * poly (pderiv_aux (Suc n) p) x ";
-by (simp_tac (simpset() addsimps [lemma_DERIV_poly1] delsimps [realpow_Suc]) 1);
-qed "lemma_DERIV_poly";
-
-Goal "DERIV f x :> D ==> DERIV (%x. a + f x) x :> D";
-by (rtac lemma_DERIV_subst 1 THEN rtac DERIV_add 1);
-by Auto_tac;
-qed "DERIV_add_const";
-
-Goal "DERIV (%x. poly p x) x :> poly (pderiv p) x";
-by (induct_tac "p" 1);
-by (auto_tac (claset(),simpset() addsimps [pderiv_Cons]));
-by (rtac DERIV_add_const 1);
-by (rtac lemma_DERIV_subst 1);
-by (rtac (full_simplify (simpset())
- (read_instantiate [("n","0")] lemma_DERIV_poly)) 1);
-by (simp_tac (simpset() addsimps [CLAIM "1 = 1"]) 1);
-qed "poly_DERIV";
-Addsimps [poly_DERIV];
-
-
-(*-------------------------------------------------------------------------*)
-(* Consequences of the derivative theorem above *)
-(*-------------------------------------------------------------------------*)
-
-Goalw [differentiable_def] "(%x. poly p x) differentiable x";
-by (blast_tac (claset() addIs [poly_DERIV]) 1);
-qed "poly_differentiable";
-Addsimps [poly_differentiable];
-
-Goal "isCont (%x. poly p x) x";
-by (rtac (poly_DERIV RS DERIV_isCont) 1);
-qed "poly_isCont";
-Addsimps [poly_isCont];
-
-Goal "[| a < b; poly p a < 0; 0 < poly p b |] \
-\ ==> EX x. a < x & x < b & (poly p x = 0)";
-by (cut_inst_tac [("f","%x. poly p x"),("a","a"),("b","b"),("y","0")]
- IVT_objl 1);
-by (auto_tac (claset(),simpset() addsimps [order_le_less]));
-qed "poly_IVT_pos";
-
-Goal "[| a < b; 0 < poly p a; poly p b < 0 |] \
-\ ==> EX x. a < x & x < b & (poly p x = 0)";
-by (blast_tac (claset() addIs [full_simplify (simpset()
- addsimps [poly_minus, neg_less_0_iff_less])
- (read_instantiate [("p","-- p")] poly_IVT_pos)]) 1);
-qed "poly_IVT_neg";
-
-Goal "a < b ==> \
-\ EX x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)";
-by (dres_inst_tac [("f","poly p")] MVT 1);
-by Auto_tac;
-by (res_inst_tac [("x","z")] exI 1);
-by (auto_tac (claset() addDs [ARITH_PROVE
- "[| a < z; z < b |] ==> (b - (a::real)) ~= 0"],simpset()
- addsimps [real_mult_left_cancel,poly_DERIV RS DERIV_unique]));
-qed "poly_MVT";
-
-
-(*-------------------------------------------------------------------------*)
-(* Lemmas for Derivatives *)
-(*-------------------------------------------------------------------------*)
-
-Goal "ALL p2 n. poly (pderiv_aux n (p1 +++ p2)) x = \
- \ poly (pderiv_aux n p1 +++ pderiv_aux n p2) x";
-by (induct_tac "p1" 1);
-by (Step_tac 2);
-by (case_tac "p2" 2);
-by (auto_tac (claset(),simpset() addsimps [right_distrib]));
-qed "lemma_poly_pderiv_aux_add";
-
-Goal "poly (pderiv_aux n (p1 +++ p2)) x = \
- \ poly (pderiv_aux n p1 +++ pderiv_aux n p2) x";
-by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_add]) 1);
-qed "poly_pderiv_aux_add";
-
-Goal "ALL n. poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x";
-by (induct_tac "p" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_cmult] @ mult_ac));
-qed "lemma_poly_pderiv_aux_cmult";
-
-Goal "poly (pderiv_aux n (c %* p) ) x = poly (c %* pderiv_aux n p) x";
-by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_cmult]) 1);
-qed "poly_pderiv_aux_cmult";
-
-Goalw [poly_minus_def]
- "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x";
-by (simp_tac (simpset() addsimps [poly_pderiv_aux_cmult]) 1);
-qed "poly_pderiv_aux_minus";
-
-Goal "ALL n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x";
-by (induct_tac "p" 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,
- left_distrib]));
-qed "lemma_poly_pderiv_aux_mult1";
-
-Goal "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x";
-by (simp_tac (simpset() addsimps [lemma_poly_pderiv_aux_mult1]) 1);
-qed "lemma_poly_pderiv_aux_mult";
-
-Goal "ALL q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x";
-by (induct_tac "p" 1);
-by (Step_tac 2);
-by (case_tac "q" 2);
-by (auto_tac (claset(),simpset() addsimps [poly_pderiv_aux_add,poly_add,
- pderiv_def]));
-qed "lemma_poly_pderiv_add";
-
-Goal "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x";
-by (simp_tac (simpset() addsimps [lemma_poly_pderiv_add]) 1);
-qed "poly_pderiv_add";
-
-Goal "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x";
-by (induct_tac "p" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_pderiv_aux_cmult,poly_cmult,
- pderiv_def]));
-qed "poly_pderiv_cmult";
-
-Goalw [poly_minus_def] "poly (pderiv (--p)) x = poly (--(pderiv p)) x";
-by (simp_tac (simpset() addsimps [poly_pderiv_cmult]) 1);
-qed "poly_pderiv_minus";
-
-Goalw [pderiv_def]
- "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x";
-by (induct_tac "t" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_add,
- lemma_poly_pderiv_aux_mult]));
-qed "lemma_poly_mult_pderiv";
-
-Goal "ALL q. poly (pderiv (p *** q)) x = \
-\ poly (p *** (pderiv q) +++ q *** (pderiv p)) x";
-by (induct_tac "p" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
- poly_pderiv_cmult,poly_pderiv_add,poly_mult]));
-by (rtac (lemma_poly_mult_pderiv RS ssubst) 1);
-by (rtac (lemma_poly_mult_pderiv RS ssubst) 1);
-by (rtac (poly_add RS ssubst) 1);
-by (rtac (poly_add RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [poly_mult,right_distrib]
- @ add_ac @ mult_ac) 1);
-qed "poly_pderiv_mult";
-
-Goal "poly (pderiv (p %^ (Suc n))) x = \
- \ poly ((real (Suc n)) %* (p %^ n) *** pderiv p ) x";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_add,poly_pderiv_cmult,
- poly_cmult,poly_pderiv_mult,real_of_nat_zero,poly_mult,
- real_of_nat_Suc,right_distrib,left_distrib]
- @ mult_ac));
-qed "poly_pderiv_exp";
-
-Goal "poly (pderiv ([-a, 1] %^ (Suc n))) x = \
-\ poly (real (Suc n) %* ([-a, 1] %^ n)) x";
-by (simp_tac (simpset() addsimps [poly_pderiv_exp,poly_mult]
- delsimps [pexp_Suc]) 1);
-by (simp_tac (simpset() addsimps [poly_cmult,pderiv_def]) 1);
-qed "poly_pderiv_exp_prime";
-
-(* ----------------------------------------------------------------------- *)
-(* Key property that f(a) = 0 ==> (x - a) divides p(x). *)
-(* ----------------------------------------------------------------------- *)
-
-Goal "ALL h. EX q r. h#t = [r] +++ [-a, 1] *** q";
-by (induct_tac "t" 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","[]")] exI 1);
-by (res_inst_tac [("x","h")] exI 1);
-by (Simp_tac 1);
-by (dres_inst_tac [("x","aa")] spec 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","r#q")] exI 1);
-by (res_inst_tac [("x","a*r + h")] exI 1);
-by (case_tac "q" 1);
-by (Auto_tac);
-qed "lemma_poly_linear_rem";
-
-Goal "EX q r. h#t = [r] +++ [-a, 1] *** q";
-by (cut_inst_tac [("t","t"),("a","a")] lemma_poly_linear_rem 1);
-by Auto_tac;
-qed "poly_linear_rem";
-
-
-Goal "(poly p a = 0) = ((p = []) | (EX q. p = [-a, 1] *** q))";
-by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
- right_distrib]));
-by (case_tac "p" 1);
-by (cut_inst_tac [("h","aa"),("t","list"),("a","a")] poly_linear_rem 2);
-by (Step_tac 2);
-by (case_tac "q" 1);
-by Auto_tac;
-by (dres_inst_tac [("x","[]")] spec 1);
-by (Asm_full_simp_tac 1);
-by (auto_tac (claset(),simpset() addsimps [poly_add,poly_cmult,
- real_add_assoc]));
-by (dres_inst_tac [("x","aa#lista")] spec 1);
-by Auto_tac;
-qed "poly_linear_divides";
-
-Goal "ALL h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed "lemma_poly_length_mult";
-Addsimps [lemma_poly_length_mult];
-
-Goal "ALL h k. length (k %* p +++ (h # p)) = Suc (length p)";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed "lemma_poly_length_mult2";
-Addsimps [lemma_poly_length_mult2];
-
-Goal "length([-a ,1] *** q) = Suc (length q)";
-by Auto_tac;
-qed "poly_length_mult";
-Addsimps [poly_length_mult];
-
-
-(*-------------------------------------------------------------------------*)
-(* Polynomial length *)
-(*-------------------------------------------------------------------------*)
-
-Goal "length (a %* p) = length p";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed "poly_cmult_length";
-Addsimps [poly_cmult_length];
-
-Goal "length (p1 +++ p2) = (if (length( p1 ) < length( p2 )) \
-\ then (length( p2 )) else (length( p1) ))";
-by (subgoal_tac "ALL p2. length (p1 +++ p2) = (if (length( p1 ) < \
-\ length( p2 )) then (length( p2 )) else (length( p1) ))" 1);
-by (induct_tac "p1" 2);
-by (Simp_tac 2);
-by (Simp_tac 2);
-by (Step_tac 2);
-by (Asm_full_simp_tac 2);
-by (arith_tac 2);
-by (Asm_full_simp_tac 2);
-by (arith_tac 2);
-by (induct_tac "p2" 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed "poly_add_length";
-
-Goal "length([a,b] *** p) = Suc (length p)";
-by (asm_full_simp_tac (simpset() addsimps [poly_cmult_length,
- poly_add_length]) 1);
-qed "poly_root_mult_length";
-Addsimps [poly_root_mult_length];
-
-Goal "(poly (p *** q) x ~= poly [] x) = \
-\ (poly p x ~= poly [] x & poly q x ~= poly [] x)";
-by (auto_tac (claset(),simpset() addsimps [poly_mult]));
-qed "poly_mult_not_eq_poly_Nil";
-Addsimps [poly_mult_not_eq_poly_Nil];
-
-Goal "(poly (p *** q) x = 0) = (poly p x = 0 | poly q x = 0)";
-by (auto_tac (claset() addDs [CLAIM "x * y = 0 ==> x = 0 | y = (0::real)"],
- simpset() addsimps [poly_mult]));
-qed "poly_mult_eq_zero_disj";
-
-(*-------------------------------------------------------------------------*)
-(* Normalisation Properties *)
-(*-------------------------------------------------------------------------*)
-
-Goal "(pnormalize p = []) --> (poly p x = 0)";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed "poly_normalized_nil";
-
-(*-------------------------------------------------------------------------*)
-(* A nontrivial polynomial of degree n has no more than n roots *)
-(*-------------------------------------------------------------------------*)
-
-Goal
- "ALL p x. (poly p x ~= poly [] x & length p = n \
-\ --> (EX i. ALL x. (poly p x = (0::real)) --> (EX m. (m <= n & x = i m))))";
-by (induct_tac "n" 1);
-by (Step_tac 1);
-by (rtac ccontr 1);
-by (subgoal_tac "EX a. poly p a = 0" 1 THEN Step_tac 1);
-by (dtac (poly_linear_divides RS iffD1) 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","q")] spec 1);
-by (dres_inst_tac [("x","x")] spec 1);
-by (asm_full_simp_tac (simpset() delsimps [poly_Nil,pmult_Cons]) 1);
-by (etac exE 1);
-by (dres_inst_tac [("x","%m. if m = Suc n then a else i m")] spec 1);
-by (Step_tac 1);
-by (dtac (poly_mult_eq_zero_disj RS iffD1) 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","Suc(length q)")] spec 1);
-by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("x","xa")] spec 1 THEN Step_tac 1);
-by (dres_inst_tac [("x","m")] spec 1);
-by (Asm_full_simp_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "poly_roots_index_lemma";
-bind_thm ("poly_roots_index_lemma2",conjI RS poly_roots_index_lemma);
-
-Goal "poly p x ~= poly [] x ==> \
-\ EX i. ALL x. (poly p x = 0) --> (EX n. n <= length p & x = i n)";
-by (blast_tac (claset() addIs [poly_roots_index_lemma2]) 1);
-qed "poly_roots_index_length";
-
-Goal "poly p x ~= poly [] x ==> \
-\ EX N i. ALL x. (poly p x = 0) --> (EX n. (n::nat) < N & x = i n)";
-by (dtac poly_roots_index_length 1 THEN Step_tac 1);
-by (res_inst_tac [("x","Suc (length p)")] exI 1);
-by (res_inst_tac [("x","i")] exI 1);
-by (auto_tac (claset(),simpset() addsimps
- [ARITH_PROVE "(m < Suc n) = (m <= n)"]));
-qed "poly_roots_finite_lemma";
-
-(* annoying proof *)
-Goal "ALL P. (ALL x. P x --> (EX n. (n::nat) < N & x = (j::nat=>real) n)) \
-\ --> (EX a. ALL x. P x --> x < a)";
-by (induct_tac "N" 1);
-by (Asm_full_simp_tac 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","%z. P z & (z ~= (j::nat=>real) n)")] spec 1);
-by Auto_tac;
-by (dres_inst_tac [("x","x")] spec 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","na")] exI 1);
-by (auto_tac (claset() addDs [ARITH_PROVE "na < Suc n ==> na = n | na < n"],
- simpset()));
-by (res_inst_tac [("x","abs a + abs(j n) + 1")] exI 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","x")] spec 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","j na")] spec 1);
-by (Step_tac 1);
-by (ALLGOALS(arith_tac));
-qed_spec_mp "real_finite_lemma";
-
-Goal "(poly p ~= poly []) = \
-\ (EX N j. ALL x. poly p x = 0 --> (EX n. (n::nat) < N & x = j n))";
-by (Step_tac 1);
-by (etac swap 1 THEN rtac ext 1);
-by (rtac ccontr 1);
-by (clarify_tac (claset() addSDs [poly_roots_finite_lemma]) 1);
-by (clarify_tac (claset() addSDs [real_finite_lemma]) 1);
-by (dres_inst_tac [("x","a")] fun_cong 1);
-by Auto_tac;
-qed "poly_roots_finite";
-
-(*-------------------------------------------------------------------------*)
-(* Entirety and Cancellation for polynomials *)
-(*-------------------------------------------------------------------------*)
-
-Goal "[| poly p ~= poly [] ; poly q ~= poly [] |] \
-\ ==> poly (p *** q) ~= poly []";
-by (auto_tac (claset(),simpset() addsimps [poly_roots_finite]));
-by (res_inst_tac [("x","N + Na")] exI 1);
-by (res_inst_tac [("x","%n. if n < N then j n else ja (n - N)")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [poly_mult_eq_zero_disj]));
-by (flexflex_tac THEN rotate_tac 1 1);
-by (dtac spec 1 THEN Auto_tac);
-qed "poly_entire_lemma";
-
-Goal "(poly (p *** q) = poly []) = ((poly p = poly []) | (poly q = poly []))";
-by (auto_tac (claset() addIs [ext] addDs [fun_cong],simpset()
- addsimps [poly_entire_lemma,poly_mult]));
-by (blast_tac (claset() addIs [ccontr] addDs [poly_entire_lemma,
- poly_mult RS subst]) 1);
-qed "poly_entire";
-
-Goal "(poly (p *** q) ~= poly []) = ((poly p ~= poly []) & (poly q ~= poly []))";
-by (asm_full_simp_tac (simpset() addsimps [poly_entire]) 1);
-qed "poly_entire_neg";
-
-Goal " (f = g) = (ALL x. f x = g x)";
-by (auto_tac (claset() addSIs [ext],simpset()));
-qed "fun_eq";
-
-Goal "(poly (p +++ -- q) = poly []) = (poly p = poly q)";
-by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def,
- fun_eq,poly_cmult,ARITH_PROVE "(p + -q = 0) = (p = (q::real))"]));
-qed "poly_add_minus_zero_iff";
-
-Goal "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))";
-by (auto_tac (claset(),simpset() addsimps [poly_add,poly_minus_def,
- fun_eq,poly_mult,poly_cmult,right_distrib]));
-qed "poly_add_minus_mult_eq";
-
-Goal "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)";
-by (res_inst_tac [("p1","p *** q")] (poly_add_minus_zero_iff RS subst) 1);
-by (auto_tac (claset() addIs [ext], simpset() addsimps [poly_add_minus_mult_eq,
- poly_entire,poly_add_minus_zero_iff]));
-qed "poly_mult_left_cancel";
-
-Goal "(x * y = 0) = (x = (0::real) | y = 0)";
-by (auto_tac (claset() addDs [CLAIM "x * y = 0 ==> x = 0 | y = (0::real)"],
- simpset()));
-qed "real_mult_zero_disj_iff";
-
-Goal "(poly (p %^ n) = poly []) = (poly p = poly [] & n ~= 0)";
-by (simp_tac (simpset() addsimps [fun_eq]) 1);
-by (rtac (CLAIM "((ALL x. P x) & Q) = (ALL x. P x & Q)" RS ssubst) 1);
-by (rtac (CLAIM "f = g ==> (ALL x. f x) = (ALL x. g x)") 1);
-by (rtac ext 1);
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [poly_mult,
- real_mult_zero_disj_iff]));
-qed "poly_exp_eq_zero";
-Addsimps [poly_exp_eq_zero];
-
-Goal "poly [a,1] ~= poly []";
-by (simp_tac (simpset() addsimps [fun_eq]) 1);
-by (res_inst_tac [("x","1 - a")] exI 1);
-by (Simp_tac 1);
-qed "poly_prime_eq_zero";
-Addsimps [poly_prime_eq_zero];
-
-Goal "(poly ([a, 1] %^ n) ~= poly [])";
-by Auto_tac;
-qed "poly_exp_prime_eq_zero";
-Addsimps [poly_exp_prime_eq_zero];
-
-(*-------------------------------------------------------------------------*)
-(* A more constructive notion of polynomials being trivial *)
-(*-------------------------------------------------------------------------*)
-
-Goal "poly (h # t) = poly [] ==> h = 0 & poly t = poly []";
-by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
-by (case_tac "h = 0" 1);
-by (dres_inst_tac [("x","0")] spec 2);
-by (rtac conjI 1);
-by (rtac ((simplify (simpset()) (read_instantiate [("g","poly []")] fun_eq))
- RS iffD1) 2 THEN rtac ccontr 2);
-by (auto_tac (claset(),simpset() addsimps [poly_roots_finite,
- real_mult_zero_disj_iff]));
-by (dtac real_finite_lemma 1 THEN Step_tac 1);
-by (REPEAT(dres_inst_tac [("x","abs a + 1")] spec 1));
-by (arith_tac 1);
-qed "poly_zero_lemma";
-
-Goal "(poly p = poly []) = list_all (%c. c = 0) p";
-by (induct_tac "p" 1);
-by (Asm_full_simp_tac 1);
-by (rtac iffI 1);
-by (dtac poly_zero_lemma 1);
-by Auto_tac;
-qed "poly_zero";
-
-Addsimps [real_mult_zero_disj_iff];
-Goal "ALL n. (list_all (%c. c = 0) (pderiv_aux (Suc n) p) = \
-\ list_all (%c. c = 0) p)";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed_spec_mp "pderiv_aux_iszero";
-Addsimps [pderiv_aux_iszero];
-
-Goal "(number_of n :: nat) ~= 0 \
-\ ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) = \
-\ list_all (%c. c = 0) p)";
-by (res_inst_tac [("n1","number_of n"),("m1","0")] (less_imp_Suc_add RS exE) 1);
-by (Force_tac 1);
-by (res_inst_tac [("n1","0 + x")] (pderiv_aux_iszero RS subst) 1);
-by (asm_simp_tac (simpset() delsimps [pderiv_aux_iszero]) 1);
-qed "pderiv_aux_iszero_num";
-
-Goal "poly (pderiv p) = poly [] --> (EX h. poly p = poly [h])";
-by (asm_full_simp_tac (simpset() addsimps [poly_zero]) 1);
-by (induct_tac "p" 1);
-by (Force_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [pderiv_Cons,
- pderiv_aux_iszero_num] delsimps [poly_Cons]) 1);
-by (auto_tac (claset(),simpset() addsimps [poly_zero RS sym]));
-qed_spec_mp "pderiv_iszero";
-
-Goal "poly p = poly [] --> (poly (pderiv p) = poly [])";
-by (asm_full_simp_tac (simpset() addsimps [poly_zero]) 1);
-by (induct_tac "p" 1);
-by (Force_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [pderiv_Cons,
- pderiv_aux_iszero_num] delsimps [poly_Cons]) 1);
-qed "pderiv_zero_obj";
-
-Goal "poly p = poly [] ==> (poly (pderiv p) = poly [])";
-by (blast_tac (claset() addEs [pderiv_zero_obj RS impE]) 1);
-qed "pderiv_zero";
-Addsimps [pderiv_zero];
-
-Goal "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))";
-by (cut_inst_tac [("p","p +++ --q")] pderiv_zero_obj 1);
-by (auto_tac (claset() addIs [ ARITH_PROVE "x + - y = 0 ==> x = (y::real)"],
- simpset() addsimps [fun_eq,poly_add,poly_minus,poly_pderiv_add,
- poly_pderiv_minus] delsimps [pderiv_zero]));
-qed "poly_pderiv_welldef";
-
-(* ------------------------------------------------------------------------- *)
-(* Basics of divisibility. *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)";
-by (auto_tac (claset(),simpset() addsimps [divides_def,fun_eq,poly_mult,
- poly_add,poly_cmult,left_distrib RS sym]));
-by (dres_inst_tac [("x","-a")] spec 1);
-by (auto_tac (claset(),simpset() addsimps [poly_linear_divides,poly_add,
- poly_cmult,left_distrib RS sym]));
-by (res_inst_tac [("x","qa *** q")] exI 1);
-by (res_inst_tac [("x","p *** qa")] exI 2);
-by (auto_tac (claset(),simpset() addsimps [poly_add,poly_mult,
- poly_cmult] @ mult_ac));
-qed "poly_primes";
-
-Goalw [divides_def] "p divides p";
-by (res_inst_tac [("x","[1]")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq]));
-qed "poly_divides_refl";
-Addsimps [poly_divides_refl];
-
-Goalw [divides_def] "[| p divides q; q divides r |] ==> p divides r";
-by (Step_tac 1);
-by (res_inst_tac [("x","qa *** qaa")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq,
- real_mult_assoc]));
-qed "poly_divides_trans";
-
-Goal "(m::nat) <= n = (EX d. n = m + d)";
-by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq,
- less_iff_Suc_add]));
-qed "le_iff_add";
-
-Goal "m <= n ==> (p %^ m) divides (p %^ n)";
-by (auto_tac (claset(),simpset() addsimps [le_iff_add]));
-by (induct_tac "d" 1);
-by (rtac poly_divides_trans 2);
-by (auto_tac (claset(),simpset() addsimps [divides_def]));
-by (res_inst_tac [("x","p")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq]
- @ mult_ac));
-qed "poly_divides_exp";
-
-Goal "[| (p %^ n) divides q; m <= n |] ==> (p %^ m) divides q";
-by (blast_tac (claset() addIs [poly_divides_exp,poly_divides_trans]) 1);
-qed "poly_exp_divides";
-
-Goalw [divides_def]
- "[| p divides q; p divides r |] ==> p divides (q +++ r)";
-by Auto_tac;
-by (res_inst_tac [("x","qa +++ qaa")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
- right_distrib]));
-qed "poly_divides_add";
-
-Goalw [divides_def]
- "[| p divides q; p divides (q +++ r) |] ==> p divides r";
-by Auto_tac;
-by (res_inst_tac [("x","qaa +++ -- qa")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
- poly_minus,right_distrib,
- ARITH_PROVE "(x = y + -z) = (z + x = (y::real))"]));
-qed "poly_divides_diff";
-
-Goal "[| p divides r; p divides (q +++ r) |] ==> p divides q";
-by (etac poly_divides_diff 1);
-by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult,
- divides_def] @ add_ac));
-qed "poly_divides_diff2";
-
-Goalw [divides_def] "poly p = poly [] ==> q divides p";
-by (auto_tac (claset(),simpset() addsimps [fun_eq,poly_mult]));
-qed "poly_divides_zero";
-
-Goalw [divides_def] "q divides []";
-by (res_inst_tac [("x","[]")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [fun_eq]));
-qed "poly_divides_zero2";
-Addsimps [poly_divides_zero2];
-
-(* ------------------------------------------------------------------------- *)
-(* At last, we can consider the order of a root. *)
-(* ------------------------------------------------------------------------- *)
-
-(* FIXME: Tidy up *)
-Goal "[| length p = d; poly p ~= poly [] |] \
-\ ==> EX n. ([-a, 1] %^ n) divides p & \
-\ ~(([-a, 1] %^ (Suc n)) divides p)";
-by (subgoal_tac "ALL p. length p = d & poly p ~= poly [] \
-\ --> (EX n q. p = mulexp n [-a, 1] q & poly q a ~= 0)" 1);
-by (induct_tac "d" 2);
-by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 2);
-by (Step_tac 2);
-by (case_tac "poly pa a = 0" 2);
-by (dtac (poly_linear_divides RS iffD1) 2);
-by (Step_tac 2);
-by (dres_inst_tac [("x","q")] spec 2);
-by (dtac (poly_entire_neg RS iffD1) 2);
-by (Step_tac 2);
-by (Force_tac 2 THEN Blast_tac 2);
-by (res_inst_tac [("x","Suc na")] exI 2);
-by (res_inst_tac [("x","qa")] exI 2);
-by (asm_full_simp_tac (simpset() delsimps [pmult_Cons]) 2);
-by (res_inst_tac [("x","0")] exI 2);
-by (Force_tac 2);
-by (dres_inst_tac [("x","p")] spec 1 THEN Step_tac 1);
-by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1);
-by (rewtac divides_def);
-by (res_inst_tac [("x","q")] exI 1);
-by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [poly_add,poly_cmult,poly_mult,
- right_distrib] @ mult_ac) 1);
-by (Step_tac 1);
-by (rotate_tac 2 1);
-by (rtac swap 1 THEN assume_tac 2);
-by (induct_tac "n" 1);
-by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
-by (eres_inst_tac [("Pa","poly q a = 0")] swap 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_add,poly_cmult]) 1);
-by (rtac (pexp_Suc RS ssubst) 1);
-by (rtac ccontr 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_mult_left_cancel,
- poly_mult_assoc] delsimps [pmult_Cons,pexp_Suc]) 1);
-qed "poly_order_exists";
-
-Goalw [divides_def] "[1] divides p";
-by Auto_tac;
-qed "poly_one_divides";
-Addsimps [poly_one_divides];
-
-Goal "poly p ~= poly [] \
-\ ==> EX! n. ([-a, 1] %^ n) divides p & \
-\ ~(([-a, 1] %^ (Suc n)) divides p)";
-by (auto_tac (claset() addIs [poly_order_exists],
- simpset() addsimps [less_linear] delsimps [pmult_Cons,pexp_Suc]));
-by (cut_inst_tac [("m","y"),("n","n")] less_linear 1);
-by (dres_inst_tac [("m","n")] poly_exp_divides 1);
-by (auto_tac (claset() addDs [ARITH_PROVE "n < m ==> Suc n <= m" RSN
- (2,poly_exp_divides)],simpset() delsimps [pmult_Cons,pexp_Suc]));
-qed "poly_order";
-
-(* ------------------------------------------------------------------------- *)
-(* Order *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[| n = (@n. P n); EX! n. P n |] ==> P n";
-by (blast_tac (claset() addIs [someI2]) 1);
-qed "some1_equalityD";
-
-Goalw [order_def]
- "(([-a, 1] %^ n) divides p & \
-\ ~(([-a, 1] %^ (Suc n)) divides p)) = \
-\ ((n = order a p) & ~(poly p = poly []))";
-by (rtac iffI 1);
-by (blast_tac (claset() addDs [poly_divides_zero]
- addSIs [some1_equality RS sym, poly_order]) 1);
-by (blast_tac (claset() addSIs [poly_order RSN (2,some1_equalityD)]) 1);
-qed "order";
-
-Goal "[| poly p ~= poly [] |] \
-\ ==> ([-a, 1] %^ (order a p)) divides p & \
-\ ~(([-a, 1] %^ (Suc(order a p))) divides p)";
-by (asm_full_simp_tac (simpset() addsimps [order] delsimps [pexp_Suc]) 1);
-qed "order2";
-
-Goal "[| poly p ~= poly []; ([-a, 1] %^ n) divides p; \
-\ ~(([-a, 1] %^ (Suc n)) divides p) \
-\ |] ==> (n = order a p)";
-by (cut_inst_tac [("p","p"),("a","a"),("n","n")] order 1);
-by Auto_tac;
-qed "order_unique";
-
-Goal "(poly p ~= poly [] & ([-a, 1] %^ n) divides p & \
-\ ~(([-a, 1] %^ (Suc n)) divides p)) \
-\ ==> (n = order a p)";
-by (blast_tac (claset() addIs [order_unique]) 1);
-qed "order_unique_lemma";
-
-Goal "poly p = poly q ==> order a p = order a q";
-by (auto_tac (claset(),simpset() addsimps [fun_eq,divides_def,poly_mult,
- order_def]));
-qed "order_poly";
-
-Goal "p %^ (Suc 0) = p";
-by (induct_tac "p" 1);
-by (auto_tac (claset(),simpset() addsimps [numeral_1_eq_1]));
-qed "pexp_one";
-Addsimps [pexp_one];
-
-Goal "ALL p a. 0 < n & [- a, 1] %^ n divides p & \
-\ ~ [- a, 1] %^ (Suc n) divides p \
-\ --> poly p a = 0";
-by (induct_tac "n" 1);
-by (Blast_tac 1);
-by (auto_tac (claset(),simpset() addsimps [divides_def,poly_mult]
- delsimps [pmult_Cons]));
-qed_spec_mp "lemma_order_root";
-
-Goal "(poly p a = 0) = ((poly p = poly []) | order a p ~= 0)";
-by (case_tac "poly p = poly []" 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [poly_linear_divides]
- delsimps [pmult_Cons]) 1);
-by (Step_tac 1);
-by (ALLGOALS(dres_inst_tac [("a","a")] order2));
-by (rtac ccontr 1);
-by (asm_full_simp_tac (simpset() addsimps [divides_def,poly_mult,fun_eq]
- delsimps [pmult_Cons]) 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addIs [lemma_order_root]) 1);
-qed "order_root";
-
-Goal "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n <= order a p)";
-by (case_tac "poly p = poly []" 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq,poly_mult]) 1);
-by (res_inst_tac [("x","[]")] exI 1);
-by (TRYALL(dres_inst_tac [("a","a")] order2));
-by (auto_tac (claset() addIs [poly_exp_divides],simpset()
- delsimps [pexp_Suc]));
-qed "order_divides";
-
-Goalw [divides_def]
- "poly p ~= poly [] \
-\ ==> EX q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) & \
-\ ~([-a, 1] divides q)";
-by (dres_inst_tac [("a","a")] order2 1);
-by (asm_full_simp_tac (simpset() addsimps [divides_def]
- delsimps [pexp_Suc,pmult_Cons]) 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","q")] exI 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","qa")] spec 1);
-by (auto_tac (claset(),simpset() addsimps [poly_mult,fun_eq,poly_exp]
- @ mult_ac delsimps [pmult_Cons]));
-qed "order_decomp";
-
-(* ------------------------------------------------------------------------- *)
-(* Important composition properties of orders. *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "poly (p *** q) ~= poly [] \
-\ ==> order a (p *** q) = order a p + order a q";
-by (cut_inst_tac [("a","a"),("p","p***q"),("n","order a p + order a q")]
- order 1);
-by (auto_tac (claset(),simpset() addsimps [poly_entire] delsimps [pmult_Cons]));
-by (REPEAT(dres_inst_tac [("a","a")] order2 1));
-by (Step_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq,poly_exp_add,
- poly_mult] delsimps [pmult_Cons]) 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","qa *** qaa")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_mult] @ mult_ac
- delsimps [pmult_Cons]) 1);
-by (REPEAT(dres_inst_tac [("a","a")] order_decomp 1));
-by (Step_tac 1);
-by (subgoal_tac "[-a,1] divides (qa *** qaa)" 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_primes]
- delsimps [pmult_Cons]) 1);
-by (auto_tac (claset(),simpset() addsimps [divides_def]
- delsimps [pmult_Cons]));
-by (res_inst_tac [("x","qb")] exI 1);
-by (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = \
-\ poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))" 1);
-by (dtac (poly_mult_left_cancel RS iffD1) 1);
-by (Force_tac 1);
-by (subgoal_tac "poly ([-a, 1] %^ (order a q) *** \
-\ ([-a, 1] %^ (order a p) *** (qa *** qaa))) = \
-\ poly ([-a, 1] %^ (order a q) *** \
-\ ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb)))" 1);
-by (dtac (poly_mult_left_cancel RS iffD1) 1);
-by (Force_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_exp_add,poly_mult]
- @ mult_ac delsimps [pmult_Cons]) 1);
-qed "order_mult";
-
-(* FIXME: too too long! *)
-Goal "ALL p q a. 0 < n & \
-\ poly (pderiv p) ~= poly [] & \
-\ poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q \
-\ --> n = Suc (order a (pderiv p))";
-by (induct_tac "n" 1);
-by (Step_tac 1);
-by (rtac order_unique_lemma 1 THEN rtac conjI 1);
-by (assume_tac 1);
-by (subgoal_tac "ALL r. r divides (pderiv p) = \
-\ r divides (pderiv ([-a, 1] %^ Suc n *** q))" 1);
-by (dtac poly_pderiv_welldef 2);
-by (asm_full_simp_tac (simpset() addsimps [divides_def] delsimps [pmult_Cons,
- pexp_Suc]) 2);
-by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
-by (rtac conjI 1);
-by (asm_full_simp_tac (simpset() addsimps [divides_def,fun_eq]
- delsimps [pmult_Cons,pexp_Suc]) 1);
-by (res_inst_tac
- [("x","[-a, 1] *** (pderiv q) +++ real (Suc n) %* q")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_pderiv_mult,
- poly_pderiv_exp_prime,poly_add,poly_mult,poly_cmult,
- right_distrib] @ mult_ac
- delsimps [pmult_Cons,pexp_Suc]) 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_mult,right_distrib,
- left_distrib] @ mult_ac delsimps [pmult_Cons]) 1);
-by (thin_tac "ALL r. \
-\ r divides pderiv p = \
-\ r divides pderiv ([- a, 1] %^ Suc n *** q)" 1);
-by (rewtac divides_def);
-by (simp_tac (simpset() addsimps [poly_pderiv_mult,
- poly_pderiv_exp_prime,fun_eq,poly_add,poly_mult]
- delsimps [pmult_Cons,pexp_Suc]) 1);
-by (rtac swap 1 THEN assume_tac 1);
-by (rotate_tac 3 1 THEN etac swap 1);
-by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","inverse(real (Suc n)) %* (qa +++ --(pderiv q))")]
- exI 1);
-by (subgoal_tac "poly ([-a, 1] %^ n *** q) = \
-\ poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* \
-\ (qa +++ -- (pderiv q)))))" 1);
-by (dtac (poly_mult_left_cancel RS iffD1) 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult,
- poly_minus] delsimps [pmult_Cons, mult_cancel_left, field_mult_cancel_left]) 1);
-by (Step_tac 1);
-by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel
- RS iffD1) 1);
-by (Simp_tac 1);
-by (rtac ((CLAIM_SIMP
- "a * (b * (c * (d * e))) = e * (b * (c * (d * (a::real))))"
- mult_ac) RS ssubst) 1);
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x","xa")] spec 1);
-by (asm_full_simp_tac (simpset()
- addsimps [left_distrib] @ mult_ac
- delsimps [pmult_Cons]) 1);
-qed_spec_mp "lemma_order_pderiv";
-
-Goal "[| poly (pderiv p) ~= poly []; order a p ~= 0 |] \
-\ ==> (order a p = Suc (order a (pderiv p)))";
-by (case_tac "poly p = poly []" 1);
-by (auto_tac (claset() addDs [pderiv_zero],simpset()));
-by (dres_inst_tac [("a","a"),("p","p")] order_decomp 1);
-by (blast_tac (claset() addIs [lemma_order_pderiv]) 1);
-qed "order_pderiv";
-
-(* ------------------------------------------------------------------------- *)
-(* Now justify the standard squarefree decomposition, i.e. f / gcd(f,f'). *)
-(* `a la Harrison *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[| poly (pderiv p) ~= 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)";
-by (subgoal_tac "order a p = order a q + order a d" 1);
-by (res_inst_tac [("s","order a (q *** d)")] trans 2);
-by (blast_tac (claset() addIs [order_poly]) 2);
-by (rtac order_mult 2);
-by (rtac notI 2 THEN Asm_full_simp_tac 2);
-by (case_tac "order a p = 0" 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "order a (pderiv p) = order a e + order a d" 1);
-by (res_inst_tac [("s","order a (e *** d)")] trans 2);
-by (blast_tac (claset() addIs [order_poly]) 2);
-by (rtac order_mult 2);
-by (rtac notI 2 THEN Asm_full_simp_tac 2);
-by (case_tac "poly p = poly []" 1);
-by (dres_inst_tac [("p","p")] pderiv_zero 1);
-by (Asm_full_simp_tac 1);
-by (dtac order_pderiv 1 THEN assume_tac 1);
-by (subgoal_tac "order a (pderiv p) <= order a d" 1);
-by (subgoal_tac "([-a, 1] %^ (order a (pderiv p))) divides d" 2);
-by (asm_full_simp_tac (simpset() addsimps [poly_entire,order_divides]) 2);
-by (subgoal_tac "([-a, 1] %^ (order a (pderiv p))) divides p & \
-\ ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p)" 2);
-by (asm_simp_tac (simpset() addsimps [order_divides]) 3);
-by (asm_full_simp_tac (simpset() addsimps [divides_def]
- delsimps [pexp_Suc,pmult_Cons]) 2);
-by (Step_tac 2);
-by (res_inst_tac [("x","r *** qa +++ s *** qaa")] exI 2);
-by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_add,poly_mult,
- left_distrib, right_distrib] @ mult_ac
- delsimps [pexp_Suc,pmult_Cons]) 2);
-by Auto_tac;
-qed "poly_squarefree_decomp_order";
-
-
-Goal "[| poly (pderiv p) ~= poly []; \
-\ poly p = poly (q *** d); \
-\ poly (pderiv p) = poly (e *** d); \
-\ poly d = poly (r *** p +++ s *** pderiv p) \
-\ |] ==> ALL a. order a q = (if order a p = 0 then 0 else 1)";
-by (blast_tac (claset() addIs [poly_squarefree_decomp_order]) 1);
-qed "poly_squarefree_decomp_order2";
-
-Goal "poly p ~= poly [] ==> (poly p a = 0) = (order a p ~= 0)";
-by (rtac (order_root RS ssubst) 1);
-by Auto_tac;
-qed "order_root2";
-
-Goal "[| poly (pderiv p) ~= poly []; order a p ~= 0 |] \
-\ ==> (order a (pderiv p) = n) = (order a p = Suc n)";
-by (auto_tac (claset() addDs [order_pderiv],simpset()));
-qed "order_pderiv2";
-
-Goalw [rsquarefree_def]
- "rsquarefree p = (ALL a. ~(poly p a = 0 & poly (pderiv p) a = 0))";
-by (case_tac "poly p = poly []" 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (case_tac "poly (pderiv p) = poly []" 1);
-by (Asm_full_simp_tac 1);
-by (dtac pderiv_iszero 1 THEN Clarify_tac 1);
-by (subgoal_tac "ALL a. order a p = order a [h]" 1);
-by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
-by (rtac allI 1);
-by (cut_inst_tac [("p","[h]"),("a","a")] order_root 1);
-by (asm_full_simp_tac (simpset() addsimps [fun_eq]) 1);
-by (blast_tac (claset() addIs [order_poly]) 1);
-by (auto_tac (claset(),simpset() addsimps [order_root,order_pderiv2]));
-by (dtac spec 1 THEN Auto_tac);
-qed "rsquarefree_roots";
-
-Goal "[1] *** p = p";
-by Auto_tac;
-qed "pmult_one";
-Addsimps [pmult_one];
-
-Goal "poly [] = poly [0]";
-by (simp_tac (simpset() addsimps [fun_eq]) 1);
-qed "poly_Nil_zero";
-
-Goalw [rsquarefree_def]
- "[| rsquarefree p; poly p a = 0 |] \
-\ ==> EX q. (poly p = poly ([-a, 1] *** q)) & poly q a ~= 0";
-by (Step_tac 1);
-by (forw_inst_tac [("a","a")] order_decomp 1);
-by (dres_inst_tac [("x","a")] spec 1);
-by (dres_inst_tac [("a1","a")] (order_root2 RS sym) 1);
-by (auto_tac (claset(),simpset() delsimps [pmult_Cons]));
-by (res_inst_tac [("x","q")] exI 1 THEN Step_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_mult,fun_eq]) 1);
-by (dres_inst_tac [("p1","q")] (poly_linear_divides RS iffD1) 1);
-by (asm_full_simp_tac (simpset() addsimps [divides_def]
- delsimps [pmult_Cons]) 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","[]")] spec 1);
-by (auto_tac (claset(),simpset() addsimps [fun_eq]));
-qed "rsquarefree_decomp";
-
-Goal "[| poly (pderiv p) ~= poly []; \
-\ poly p = poly (q *** d); \
-\ poly (pderiv p) = poly (e *** d); \
-\ poly d = poly (r *** p +++ s *** pderiv p) \
-\ |] ==> rsquarefree q & (ALL a. (poly q a = 0) = (poly p a = 0))";
-by (ftac poly_squarefree_decomp_order2 1);
-by (TRYALL(assume_tac));
-by (case_tac "poly p = poly []" 1);
-by (blast_tac (claset() addDs [pderiv_zero]) 1);
-by (simp_tac (simpset() addsimps [rsquarefree_def,
- order_root] delsimps [pmult_Cons]) 1);
-by (asm_full_simp_tac (simpset() addsimps [poly_entire]
- delsimps [pmult_Cons]) 1);
-qed "poly_squarefree_decomp";
-
-
-(* ------------------------------------------------------------------------- *)
-(* Normalization of a polynomial. *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "poly (pnormalize p) = poly p";
-by (induct_tac "p" 1);
-by (auto_tac (claset(),simpset() addsimps [fun_eq]));
-qed "poly_normalize";
-Addsimps [poly_normalize];
-
-
-(* ------------------------------------------------------------------------- *)
-(* The degree of a polynomial. *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "list_all (%c. c = 0) p --> pnormalize p = []";
-by (induct_tac "p" 1);
-by Auto_tac;
-qed_spec_mp "lemma_degree_zero";
-
-Goalw [degree_def] "poly p = poly [] ==> degree p = 0";
-by (case_tac "pnormalize p = []" 1);
-by (auto_tac (claset() addDs [lemma_degree_zero],simpset()
- addsimps [poly_zero]));
-qed "degree_zero";
-
-(* ------------------------------------------------------------------------- *)
-(* Tidier versions of finiteness of roots. *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "poly p ~= poly [] ==> finite {x. poly p x = 0}";
-by (auto_tac (claset(),simpset() addsimps [poly_roots_finite]));
-by (res_inst_tac [("B","{x::real. EX n. (n::nat) < N & (x = j n)}")]
- finite_subset 1);
-by (induct_tac "N" 2);
-by Auto_tac;
-by (subgoal_tac "{x::real. EX na. na < Suc n & (x = j na)} = \
-\ {(j n)} Un {x. EX na. na < n & (x = j na)}" 1);
-by (auto_tac (claset(),simpset() addsimps [ARITH_PROVE
- "(na < Suc n) = (na = n | na < n)"]));
-qed "poly_roots_finite_set";
-
-(* ------------------------------------------------------------------------- *)
-(* bound for polynomial. *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "abs(x) <= k --> abs(poly p x) <= poly (map abs p) k";
-by (induct_tac "p" 1);
-by Auto_tac;
-by (res_inst_tac [("j","abs a + abs(x * poly list x)")] real_le_trans 1);
-by (rtac abs_triangle_ineq 1);
-by (auto_tac (claset() addSIs [mult_mono],simpset()
- addsimps [abs_mult]));
-by (arith_tac 1);
-qed_spec_mp "poly_mono";
--- a/src/HOL/Hyperreal/Poly.thy Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/Poly.thy Fri Mar 05 15:18:59 2004 +0100
@@ -1,121 +1,1168 @@
(* Title: Poly.thy
+ ID: $Id$
Author: Jacques D. Fleuriot
Copyright: 2000 University of Edinburgh
- Description: Properties of univariate real polynomials (cf. Harrison)
+
+ Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
*)
-Poly = Transcendental +
+header{*Univariate Real Polynomials*}
-(* ------------------------------------------------------------------------- *)
-(* Application of polynomial as a real function. *)
-(* ------------------------------------------------------------------------- *)
-
-consts poly :: real list => real => real
-primrec
- poly_Nil "poly [] x = 0"
- poly_Cons "poly (h#t) x = h + x * poly t x"
+theory Poly = Transcendental:
-(* ------------------------------------------------------------------------- *)
-(* Arithmetic operations on polynomials. *)
-(* ------------------------------------------------------------------------- *)
+text{*Application of polynomial as a real function.*}
+
+consts poly :: "real list => real => real"
+primrec
+ poly_Nil: "poly [] x = 0"
+ poly_Cons: "poly (h#t) x = h + x * poly t x"
+
-(* addition *)
-consts "+++" :: [real list, real list] => real list (infixl 65)
+subsection{*Arithmetic Operations on Polynomials*}
+
+text{*addition*}
+consts "+++" :: "[real list, real list] => real list" (infixl 65)
primrec
- padd_Nil "[] +++ l2 = l2"
- padd_Cons "(h#t) +++ l2 = (if l2 = [] then h#t
+ padd_Nil: "[] +++ l2 = l2"
+ padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
else (h + hd l2)#(t +++ tl l2))"
-(* Multiplication by a constant *)
-consts "%*" :: [real, real list] => real list (infixl 70)
+text{*Multiplication by a constant*}
+consts "%*" :: "[real, real list] => real list" (infixl 70)
primrec
- cmult_Nil "c %* [] = []"
- cmult_Cons "c %* (h#t) = (c * h)#(c %* t)"
+ cmult_Nil: "c %* [] = []"
+ cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
-(* Multiplication by a polynomial *)
-consts "***" :: [real list, real list] => real list (infixl 70)
+text{*Multiplication by a polynomial*}
+consts "***" :: "[real list, real list] => real list" (infixl 70)
primrec
- pmult_Nil "[] *** l2 = []"
- pmult_Cons "(h#t) *** l2 = (if t = [] then h %* l2
+ pmult_Nil: "[] *** l2 = []"
+ pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
else (h %* l2) +++ ((0) # (t *** l2)))"
-(* Repeated multiplication by a polynomial *)
-consts mulexp :: [nat, real list, real list] => real list
+text{*Repeated multiplication by a polynomial*}
+consts mulexp :: "[nat, real list, real list] => real list"
primrec
- mulexp_zero "mulexp 0 p q = q"
- mulexp_Suc "mulexp (Suc n) p q = p *** mulexp n p q"
-
-
-(* Exponential *)
-consts "%^" :: [real list, nat] => real list (infixl 80)
+ mulexp_zero: "mulexp 0 p q = q"
+ mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q"
+
+
+text{*Exponential*}
+consts "%^" :: "[real list, nat] => real list" (infixl 80)
primrec
- pexp_0 "p %^ 0 = [1]"
- pexp_Suc "p %^ (Suc n) = p *** (p %^ n)"
+ pexp_0: "p %^ 0 = [1]"
+ pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
-(* Quotient related value of dividing a polynomial by x + a *)
+text{*Quotient related value of dividing a polynomial by x + a*}
(* Useful for divisor properties in inductive proofs *)
-consts "pquot" :: [real list, real] => real list
+consts "pquot" :: "[real list, real] => real list"
primrec
- pquot_Nil "pquot [] a= []"
- pquot_Cons "pquot (h#t) a = (if t = [] then [h]
+ pquot_Nil: "pquot [] a= []"
+ pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
-(* ------------------------------------------------------------------------- *)
-(* Differentiation of polynomials (needs an auxiliary function). *)
-(* ------------------------------------------------------------------------- *)
-consts pderiv_aux :: nat => real list => real list
+text{*Differentiation of polynomials (needs an auxiliary function).*}
+consts pderiv_aux :: "nat => real list => real list"
primrec
- pderiv_aux_Nil "pderiv_aux n [] = []"
- pderiv_aux_Cons "pderiv_aux n (h#t) =
+ pderiv_aux_Nil: "pderiv_aux n [] = []"
+ pderiv_aux_Cons: "pderiv_aux n (h#t) =
(real n * h)#(pderiv_aux (Suc n) t)"
-(* ------------------------------------------------------------------------- *)
-(* normalization of polynomials (remove extra 0 coeff) *)
-(* ------------------------------------------------------------------------- *)
-consts pnormalize :: real list => real list
-primrec
- pnormalize_Nil "pnormalize [] = []"
- pnormalize_Cons "pnormalize (h#p) = (if ( (pnormalize p) = [])
- then (if (h = 0) then [] else [h])
+text{*normalization of polynomials (remove extra 0 coeff)*}
+consts pnormalize :: "real list => real list"
+primrec
+ pnormalize_Nil: "pnormalize [] = []"
+ pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
+ then (if (h = 0) then [] else [h])
else (h#(pnormalize p)))"
-(* ------------------------------------------------------------------------- *)
-(* Other definitions *)
-(* ------------------------------------------------------------------------- *)
+text{*Other definitions*}
constdefs
- poly_minus :: real list => real list ("-- _" [80] 80)
+ poly_minus :: "real list => real list" ("-- _" [80] 80)
"-- p == (- 1) %* p"
- pderiv :: real list => real list
+ pderiv :: "real list => real list"
"pderiv p == if p = [] then [] else pderiv_aux 1 (tl p)"
- divides :: [real list,real list] => bool (infixl 70)
- "p1 divides p2 == EX q. poly p2 = poly(p1 *** q)"
+ divides :: "[real list,real list] => bool" (infixl "divides" 70)
+ "p1 divides p2 == \<exists>q. poly p2 = poly(p1 *** q)"
-(* ------------------------------------------------------------------------- *)
-(* Definition of order. *)
-(* ------------------------------------------------------------------------- *)
-
- order :: real => real list => nat
+ order :: "real => real list => nat"
+ --{*order of a polynomial*}
"order a p == (@n. ([-a, 1] %^ n) divides p &
~ (([-a, 1] %^ (Suc n)) divides p))"
-(* ------------------------------------------------------------------------- *)
-(* Definition of degree. *)
-(* ------------------------------------------------------------------------- *)
-
- degree :: real list => nat
+ degree :: "real list => nat"
+ --{*degree of a polynomial*}
"degree p == length (pnormalize p)"
-
-(* ------------------------------------------------------------------------- *)
-(* Define being "squarefree" --- NB with respect to real roots only. *)
-(* ------------------------------------------------------------------------- *)
+
+ rsquarefree :: "real list => bool"
+ --{*squarefree polynomials --- NB with respect to real roots only.*}
+ "rsquarefree p == poly p \<noteq> poly [] &
+ (\<forall>a. (order a p = 0) | (order a p = 1))"
+
+
+
+lemma padd_Nil2: "p +++ [] = p"
+by (induct_tac "p", auto)
+declare padd_Nil2 [simp]
+
+lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"
+by auto
+
+lemma pminus_Nil: "-- [] = []"
+by (simp add: poly_minus_def)
+declare pminus_Nil [simp]
+
+lemma pmult_singleton: "[h1] *** p1 = h1 %* p1"
+by simp
+
+lemma poly_ident_mult: "1 %* t = t"
+by (induct_tac "t", auto)
+declare poly_ident_mult [simp]
+
+lemma poly_simple_add_Cons: "[a] +++ ((0)#t) = (a#t)"
+by simp
+declare poly_simple_add_Cons [simp]
+
+text{*Handy general properties*}
+
+lemma padd_commut: "b +++ a = a +++ b"
+apply (subgoal_tac "\<forall>a. b +++ a = a +++ b")
+apply (induct_tac [2] "b", auto)
+apply (rule padd_Cons [THEN ssubst])
+apply (case_tac "aa", auto)
+done
+
+lemma padd_assoc [rule_format]: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
+apply (induct_tac "a", simp, clarify)
+apply (case_tac b, simp_all)
+done
+
+lemma poly_cmult_distr [rule_format]:
+ "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
+apply (induct_tac "p", simp, clarify)
+apply (case_tac "q")
+apply (simp_all add: right_distrib)
+done
+
+lemma pmult_by_x: "[0, 1] *** t = ((0)#t)"
+apply (induct_tac "t", simp)
+apply (simp add: poly_ident_mult padd_commut)
+apply (case_tac "list")
+apply (simp (no_asm_simp))
+apply (simp add: poly_ident_mult padd_commut)
+done
+declare pmult_by_x [simp]
+
+
+text{*properties of evaluation of polynomials.*}
+
+lemma poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x"
+apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x")
+apply (induct_tac [2] "p1", auto)
+apply (case_tac "p2")
+apply (auto simp add: right_distrib)
+done
+
+lemma poly_cmult: "poly (c %* p) x = c * poly p x"
+apply (induct_tac "p")
+apply (case_tac [2] "x=0")
+apply (auto simp add: right_distrib mult_ac)
+done
+
+lemma poly_minus: "poly (-- p) x = - (poly p x)"
+apply (simp add: poly_minus_def)
+apply (auto simp add: poly_cmult)
+done
+
+lemma poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
+apply (subgoal_tac "\<forall>p2. poly (p1 *** p2) x = poly p1 x * poly p2 x")
+apply (simp (no_asm_simp))
+apply (induct_tac "p1")
+apply (auto simp add: poly_cmult)
+apply (case_tac "list")
+apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac)
+done
+
+lemma poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: poly_cmult poly_mult)
+done
+
+text{*More Polynomial Evaluation Lemmas*}
+
+lemma poly_add_rzero: "poly (a +++ []) x = poly a x"
+by simp
+declare poly_add_rzero [simp]
+
+lemma poly_mult_assoc: "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x"
+by (simp add: poly_mult real_mult_assoc)
+
+lemma poly_mult_Nil2: "poly (p *** []) x = 0"
+by (induct_tac "p", auto)
+declare poly_mult_Nil2 [simp]
+
+lemma poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x"
+apply (induct_tac "n")
+apply (auto simp add: poly_mult real_mult_assoc)
+done
+
+text{*The derivative*}
+
+lemma pderiv_Nil: "pderiv [] = []"
+
+apply (simp add: pderiv_def)
+done
+declare pderiv_Nil [simp]
+
+lemma pderiv_singleton: "pderiv [c] = []"
+by (simp add: pderiv_def)
+declare pderiv_singleton [simp]
+
+lemma pderiv_Cons: "pderiv (h#t) = pderiv_aux 1 t"
+by (simp add: pderiv_def)
+
+lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c) x :> D * c"
+by (simp add: DERIV_cmult mult_commute [of _ c])
+
+lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
+by (rule lemma_DERIV_subst, rule DERIV_pow, simp)
+declare DERIV_pow2 [simp] DERIV_pow [simp]
+
+lemma lemma_DERIV_poly1: "\<forall>n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :>
+ x ^ n * poly (pderiv_aux (Suc n) p) x "
+apply (induct_tac "p")
+apply (auto intro!: DERIV_add DERIV_cmult2
+ simp add: pderiv_def right_distrib real_mult_assoc [symmetric]
+ simp del: realpow_Suc)
+apply (subst mult_commute)
+apply (simp del: realpow_Suc)
+apply (simp add: mult_commute realpow_Suc [symmetric] del: realpow_Suc)
+done
+
+lemma lemma_DERIV_poly: "DERIV (%x. (x ^ (Suc n) * poly p x)) x :>
+ x ^ n * poly (pderiv_aux (Suc n) p) x "
+by (simp add: lemma_DERIV_poly1 del: realpow_Suc)
+
+lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x) x :> D"
+by (rule lemma_DERIV_subst, rule DERIV_add, auto)
+
+lemma poly_DERIV: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
+apply (induct_tac "p")
+apply (auto simp add: pderiv_Cons)
+apply (rule DERIV_add_const)
+apply (rule lemma_DERIV_subst)
+apply (rule lemma_DERIV_poly [where n=0, simplified], simp)
+done
+declare poly_DERIV [simp]
+
+
+text{* Consequences of the derivative theorem above*}
+
+lemma poly_differentiable: "(%x. poly p x) differentiable x"
+
+apply (simp add: differentiable_def)
+apply (blast intro: poly_DERIV)
+done
+declare poly_differentiable [simp]
+
+lemma poly_isCont: "isCont (%x. poly p x) x"
+by (rule poly_DERIV [THEN DERIV_isCont])
+declare poly_isCont [simp]
+
+lemma poly_IVT_pos: "[| a < b; poly p a < 0; 0 < poly p b |]
+ ==> \<exists>x. a < x & x < b & (poly p x = 0)"
+apply (cut_tac f = "%x. poly p x" and a = a and b = b and y = 0 in IVT_objl)
+apply (auto simp add: order_le_less)
+done
+
+lemma poly_IVT_neg: "[| a < b; 0 < poly p a; poly p b < 0 |]
+ ==> \<exists>x. a < x & x < b & (poly p x = 0)"
+apply (insert poly_IVT_pos [where p = "-- p" ])
+apply (simp add: poly_minus neg_less_0_iff_less)
+done
+
+lemma poly_MVT: "a < b ==>
+ \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
+apply (drule_tac f = "poly p" in MVT, auto)
+apply (rule_tac x = z in exI)
+apply (auto simp add: real_mult_left_cancel poly_DERIV [THEN DERIV_unique])
+done
+
+
+text{*Lemmas for Derivatives*}
+
+lemma lemma_poly_pderiv_aux_add: "\<forall>p2 n. poly (pderiv_aux n (p1 +++ p2)) x =
+ poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"
+apply (induct_tac "p1", simp, clarify)
+apply (case_tac "p2")
+apply (auto simp add: right_distrib)
+done
+
+lemma poly_pderiv_aux_add: "poly (pderiv_aux n (p1 +++ p2)) x =
+ poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"
+apply (simp add: lemma_poly_pderiv_aux_add)
+done
+
+lemma lemma_poly_pderiv_aux_cmult: "\<forall>n. poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x"
+apply (induct_tac "p")
+apply (auto simp add: poly_cmult mult_ac)
+done
+
+lemma poly_pderiv_aux_cmult: "poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x"
+by (simp add: lemma_poly_pderiv_aux_cmult)
+
+lemma poly_pderiv_aux_minus:
+ "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x"
+apply (simp add: poly_minus_def poly_pderiv_aux_cmult)
+done
+
+lemma lemma_poly_pderiv_aux_mult1: "\<forall>n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"
+apply (induct_tac "p")
+apply (auto simp add: real_of_nat_Suc left_distrib)
+done
+
+lemma lemma_poly_pderiv_aux_mult: "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"
+by (simp add: lemma_poly_pderiv_aux_mult1)
+
+lemma lemma_poly_pderiv_add: "\<forall>q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"
+apply (induct_tac "p", simp, clarify)
+apply (case_tac "q")
+apply (auto simp add: poly_pderiv_aux_add poly_add pderiv_def)
+done
+
+lemma poly_pderiv_add: "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"
+by (simp add: lemma_poly_pderiv_add)
+
+lemma poly_pderiv_cmult: "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x"
+apply (induct_tac "p")
+apply (auto simp add: poly_pderiv_aux_cmult poly_cmult pderiv_def)
+done
+
+lemma poly_pderiv_minus: "poly (pderiv (--p)) x = poly (--(pderiv p)) x"
+by (simp add: poly_minus_def poly_pderiv_cmult)
+
+lemma lemma_poly_mult_pderiv:
+ "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x"
+apply (simp add: pderiv_def)
+apply (induct_tac "t")
+apply (auto simp add: poly_add lemma_poly_pderiv_aux_mult)
+done
+
+lemma poly_pderiv_mult: "\<forall>q. poly (pderiv (p *** q)) x =
+ poly (p *** (pderiv q) +++ q *** (pderiv p)) x"
+apply (induct_tac "p")
+apply (auto simp add: poly_add poly_cmult poly_pderiv_cmult poly_pderiv_add poly_mult)
+apply (rule lemma_poly_mult_pderiv [THEN ssubst])
+apply (rule lemma_poly_mult_pderiv [THEN ssubst])
+apply (rule poly_add [THEN ssubst])
+apply (rule poly_add [THEN ssubst])
+apply (simp (no_asm_simp) add: poly_mult right_distrib add_ac mult_ac)
+done
+
+lemma poly_pderiv_exp: "poly (pderiv (p %^ (Suc n))) x =
+ poly ((real (Suc n)) %* (p %^ n) *** pderiv p) x"
+apply (induct_tac "n")
+apply (auto simp add: poly_add poly_pderiv_cmult poly_cmult poly_pderiv_mult
+ real_of_nat_zero poly_mult real_of_nat_Suc
+ right_distrib left_distrib mult_ac)
+done
+
+lemma poly_pderiv_exp_prime: "poly (pderiv ([-a, 1] %^ (Suc n))) x =
+ poly (real (Suc n) %* ([-a, 1] %^ n)) x"
+apply (simp add: poly_pderiv_exp poly_mult del: pexp_Suc)
+apply (simp add: poly_cmult pderiv_def)
+done
+
+subsection{*Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides
+ @{term "p(x)"} *}
+
+lemma lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q"
+apply (induct_tac "t", safe)
+apply (rule_tac x = "[]" in exI)
+apply (rule_tac x = h in exI, simp)
+apply (drule_tac x = aa in spec, safe)
+apply (rule_tac x = "r#q" in exI)
+apply (rule_tac x = "a*r + h" in exI)
+apply (case_tac "q", auto)
+done
+
+lemma poly_linear_rem: "\<exists>q r. h#t = [r] +++ [-a, 1] *** q"
+by (cut_tac t = t and a = a in lemma_poly_linear_rem, auto)
+
+
+lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))"
+apply (auto simp add: poly_add poly_cmult right_distrib)
+apply (case_tac "p", simp)
+apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
+apply (case_tac "q", auto)
+apply (drule_tac x = "[]" in spec, simp)
+apply (auto simp add: poly_add poly_cmult real_add_assoc)
+apply (drule_tac x = "aa#lista" in spec, auto)
+done
+
+lemma lemma_poly_length_mult: "\<forall>h k a. length (k %* p +++ (h # (a %* p))) = Suc (length p)"
+by (induct_tac "p", auto)
+declare lemma_poly_length_mult [simp]
+
+lemma lemma_poly_length_mult2: "\<forall>h k. length (k %* p +++ (h # p)) = Suc (length p)"
+by (induct_tac "p", auto)
+declare lemma_poly_length_mult2 [simp]
+
+lemma poly_length_mult: "length([-a,1] *** q) = Suc (length q)"
+by auto
+declare poly_length_mult [simp]
+
+
+subsection{*Polynomial length*}
+
+lemma poly_cmult_length: "length (a %* p) = length p"
+by (induct_tac "p", auto)
+declare poly_cmult_length [simp]
+
+lemma poly_add_length [rule_format]:
+ "\<forall>p2. length (p1 +++ p2) =
+ (if (length p1 < length p2) then length p2 else length p1)"
+apply (induct_tac "p1", simp_all, arith)
+done
+
+lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
+by (simp add: poly_cmult_length poly_add_length)
+declare poly_root_mult_length [simp]
+
+lemma poly_mult_not_eq_poly_Nil: "(poly (p *** q) x \<noteq> poly [] x) =
+ (poly p x \<noteq> poly [] x & poly q x \<noteq> poly [] x)"
+apply (auto simp add: poly_mult)
+done
+declare poly_mult_not_eq_poly_Nil [simp]
+
+lemma poly_mult_eq_zero_disj: "(poly (p *** q) x = 0) = (poly p x = 0 | poly q x = 0)"
+by (auto simp add: poly_mult)
+
+text{*Normalisation Properties*}
+
+lemma poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)"
+by (induct_tac "p", auto)
+
+text{*A nontrivial polynomial of degree n has no more than n roots*}
+
+lemma poly_roots_index_lemma [rule_format]:
+ "\<forall>p x. poly p x \<noteq> poly [] x & length p = n
+ --> (\<exists>i. \<forall>x. (poly p x = (0::real)) --> (\<exists>m. (m \<le> n & x = i m)))"
+apply (induct_tac "n", safe)
+apply (rule ccontr)
+apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
+apply (drule poly_linear_divides [THEN iffD1], safe)
+apply (drule_tac x = q in spec)
+apply (drule_tac x = x in spec)
+apply (simp del: poly_Nil pmult_Cons)
+apply (erule exE)
+apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
+apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
+apply (drule_tac x = "Suc (length q) " in spec)
+apply simp
+apply (drule_tac x = xa in spec, safe)
+apply (drule_tac x = m in spec, simp, blast)
+done
+lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard]
+
+lemma poly_roots_index_length: "poly p x \<noteq> poly [] x ==>
+ \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)"
+by (blast intro: poly_roots_index_lemma2)
+
+lemma poly_roots_finite_lemma: "poly p x \<noteq> poly [] x ==>
+ \<exists>N i. \<forall>x. (poly p x = 0) --> (\<exists>n. (n::nat) < N & x = i n)"
+apply (drule poly_roots_index_length, safe)
+apply (rule_tac x = "Suc (length p) " in exI)
+apply (rule_tac x = i in exI)
+apply (simp add: less_Suc_eq_le)
+done
+
+(* annoying proof *)
+lemma real_finite_lemma [rule_format (no_asm)]:
+ "\<forall>P. (\<forall>x. P x --> (\<exists>n. (n::nat) < N & x = (j::nat=>real) n))
+ --> (\<exists>a. \<forall>x. P x --> x < a)"
+apply (induct_tac "N", simp, safe)
+apply (drule_tac x = "%z. P z & (z \<noteq> (j::nat=>real) n) " in spec)
+apply auto
+apply (drule_tac x = x in spec, safe)
+apply (rule_tac x = na in exI)
+apply (auto simp add: less_Suc_eq)
+apply (rule_tac x = "abs a + abs (j n) + 1" in exI)
+apply safe
+apply (drule_tac x = x in spec, safe)
+apply (drule_tac x = "j na" in spec, arith+)
+done
+
+lemma poly_roots_finite: "(poly p \<noteq> poly []) =
+ (\<exists>N j. \<forall>x. poly p x = 0 --> (\<exists>n. (n::nat) < N & x = j n))"
+apply safe
+apply (erule swap, rule ext)
+apply (rule ccontr)
+apply (clarify dest!: poly_roots_finite_lemma)
+apply (clarify dest!: real_finite_lemma)
+apply (drule_tac x = a in fun_cong, auto)
+done
+
+text{*Entirety and Cancellation for polynomials*}
+
+lemma poly_entire_lemma: "[| poly p \<noteq> poly [] ; poly q \<noteq> poly [] |]
+ ==> poly (p *** q) \<noteq> poly []"
+apply (auto simp add: poly_roots_finite)
+apply (rule_tac x = "N + Na" in exI)
+apply (rule_tac x = "%n. if n < N then j n else ja (n - N) " in exI)
+apply (auto simp add: poly_mult_eq_zero_disj, force)
+done
+
+lemma poly_entire: "(poly (p *** q) = poly []) = ((poly p = poly []) | (poly q = poly []))"
+apply (auto intro: ext dest: fun_cong simp add: poly_entire_lemma poly_mult)
+apply (blast intro: ccontr dest: poly_entire_lemma poly_mult [THEN subst])
+done
+
+lemma poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
+by (simp add: poly_entire)
+
+lemma fun_eq: " (f = g) = (\<forall>x. f x = g x)"
+by (auto intro!: ext)
+
+lemma poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"
+by (auto simp add: poly_add poly_minus_def fun_eq poly_cmult)
+
+lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
+by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib)
+
+lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
+apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst])
+apply (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
+done
+
+lemma real_mult_zero_disj_iff: "(x * y = 0) = (x = (0::real) | y = 0)"
+by simp
+
+lemma poly_exp_eq_zero:
+ "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
+apply (simp only: fun_eq add: all_simps [symmetric])
+apply (rule arg_cong [where f = All])
+apply (rule ext)
+apply (induct_tac "n")
+apply (auto simp add: poly_mult real_mult_zero_disj_iff)
+done
+declare poly_exp_eq_zero [simp]
+
+lemma poly_prime_eq_zero: "poly [a,1] \<noteq> poly []"
+apply (simp add: fun_eq)
+apply (rule_tac x = "1 - a" in exI, simp)
+done
+declare poly_prime_eq_zero [simp]
+
+lemma poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
+by auto
+declare poly_exp_prime_eq_zero [simp]
+
+text{*A more constructive notion of polynomials being trivial*}
+
+lemma poly_zero_lemma: "poly (h # t) = poly [] ==> h = 0 & poly t = poly []"
+apply (simp add: fun_eq)
+apply (case_tac "h = 0")
+apply (drule_tac [2] x = 0 in spec, auto)
+apply (case_tac "poly t = poly []", simp)
+apply (auto simp add: poly_roots_finite real_mult_zero_disj_iff)
+apply (drule real_finite_lemma, safe)
+apply (drule_tac x = "abs a + 1" in spec)+
+apply arith
+done
+
+
+lemma poly_zero: "(poly p = poly []) = list_all (%c. c = 0) p"
+apply (induct_tac "p", simp)
+apply (rule iffI)
+apply (drule poly_zero_lemma, auto)
+done
+
+declare real_mult_zero_disj_iff [simp]
+
+lemma pderiv_aux_iszero [rule_format, simp]:
+ "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
+by (induct_tac "p", auto)
+
+lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
+ ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
+ list_all (%c. c = 0) p)"
+apply (rule_tac n1 = "number_of n" and m1 = 0 in less_imp_Suc_add [THEN exE], force)
+apply (rule_tac n1 = "0 + x" in pderiv_aux_iszero [THEN subst])
+apply (simp (no_asm_simp) del: pderiv_aux_iszero)
+done
+
+lemma pderiv_iszero [rule_format]:
+ "poly (pderiv p) = poly [] --> (\<exists>h. poly p = poly [h])"
+apply (simp add: poly_zero)
+apply (induct_tac "p", force)
+apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
+apply (auto simp add: poly_zero [symmetric])
+done
+
+lemma pderiv_zero_obj: "poly p = poly [] --> (poly (pderiv p) = poly [])"
+apply (simp add: poly_zero)
+apply (induct_tac "p", force)
+apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
+done
+
+lemma pderiv_zero: "poly p = poly [] ==> (poly (pderiv p) = poly [])"
+by (blast elim: pderiv_zero_obj [THEN impE])
+declare pderiv_zero [simp]
+
+lemma poly_pderiv_welldef: "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))"
+apply (cut_tac p = "p +++ --q" in pderiv_zero_obj)
+apply (simp add: fun_eq poly_add poly_minus poly_pderiv_add poly_pderiv_minus del: pderiv_zero)
+done
+
+text{*Basics of divisibility.*}
+
+lemma poly_primes: "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
+apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
+apply (drule_tac x = "-a" in spec)
+apply (auto simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
+apply (rule_tac x = "qa *** q" in exI)
+apply (rule_tac [2] x = "p *** qa" in exI)
+apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
+done
- rsquarefree :: real list => bool
- "rsquarefree p == poly p ~= poly [] &
- (ALL a. (order a p = 0) | (order a p = 1))"
+lemma poly_divides_refl: "p divides p"
+apply (simp add: divides_def)
+apply (rule_tac x = "[1]" in exI)
+apply (auto simp add: poly_mult fun_eq)
+done
+declare poly_divides_refl [simp]
+
+lemma poly_divides_trans: "[| p divides q; q divides r |] ==> p divides r"
+apply (simp add: divides_def, safe)
+apply (rule_tac x = "qa *** qaa" in exI)
+apply (auto simp add: poly_mult fun_eq real_mult_assoc)
+done
+
+lemma le_iff_add: "(m::nat) \<le> n = (\<exists>d. n = m + d)"
+by (auto simp add: le_eq_less_or_eq less_iff_Suc_add)
+
+lemma poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
+apply (auto simp add: le_iff_add)
+apply (induct_tac "d")
+apply (rule_tac [2] poly_divides_trans)
+apply (auto simp add: divides_def)
+apply (rule_tac x = p in exI)
+apply (auto simp add: poly_mult fun_eq mult_ac)
+done
+
+lemma poly_exp_divides: "[| (p %^ n) divides q; m \<le> n |] ==> (p %^ m) divides q"
+by (blast intro: poly_divides_exp poly_divides_trans)
+
+lemma poly_divides_add:
+ "[| p divides q; p divides r |] ==> p divides (q +++ r)"
+apply (simp add: divides_def, auto)
+apply (rule_tac x = "qa +++ qaa" in exI)
+apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
+done
+
+lemma poly_divides_diff:
+ "[| p divides q; p divides (q +++ r) |] ==> p divides r"
+apply (simp add: divides_def, auto)
+apply (rule_tac x = "qaa +++ -- qa" in exI)
+apply (auto simp add: poly_add fun_eq poly_mult poly_minus right_diff_distrib compare_rls add_ac)
+done
+
+lemma poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q"
+apply (erule poly_divides_diff)
+apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
+done
+
+lemma poly_divides_zero: "poly p = poly [] ==> q divides p"
+apply (simp add: divides_def)
+apply (auto simp add: fun_eq poly_mult)
+done
+
+lemma poly_divides_zero2: "q divides []"
+apply (simp add: divides_def)
+apply (rule_tac x = "[]" in exI)
+apply (auto simp add: fun_eq)
+done
+declare poly_divides_zero2 [simp]
+
+text{*At last, we can consider the order of a root.*}
+
+
+lemma poly_order_exists_lemma [rule_format]:
+ "\<forall>p. length p = d --> poly p \<noteq> poly []
+ --> (\<exists>n q. p = mulexp n [-a, 1] q & poly q a \<noteq> 0)"
+apply (induct_tac "d")
+apply (simp add: fun_eq, safe)
+apply (case_tac "poly p a = 0")
+apply (drule_tac poly_linear_divides [THEN iffD1], safe)
+apply (drule_tac x = q in spec)
+apply (drule_tac poly_entire_neg [THEN iffD1], safe, force, blast)
+apply (rule_tac x = "Suc na" in exI)
+apply (rule_tac x = qa in exI)
+apply (simp del: pmult_Cons)
+apply (rule_tac x = 0 in exI, force)
+done
+
+(* FIXME: Tidy up *)
+lemma poly_order_exists:
+ "[| length p = d; poly p \<noteq> poly [] |]
+ ==> \<exists>n. ([-a, 1] %^ n) divides p &
+ ~(([-a, 1] %^ (Suc n)) divides p)"
+apply (drule poly_order_exists_lemma [where a=a], assumption, clarify)
+apply (rule_tac x = n in exI, safe)
+apply (unfold divides_def)
+apply (rule_tac x = q in exI)
+apply (induct_tac "n", simp)
+apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
+apply safe
+apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)")
+apply simp
+apply (induct_tac "n")
+apply (simp del: pmult_Cons pexp_Suc)
+apply (erule_tac Pa = "poly q a = 0" in swap)
+apply (simp add: poly_add poly_cmult)
+apply (rule pexp_Suc [THEN ssubst])
+apply (rule ccontr)
+apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc)
+done
+
+lemma poly_one_divides: "[1] divides p"
+by (simp add: divides_def, auto)
+declare poly_one_divides [simp]
+
+lemma poly_order: "poly p \<noteq> poly []
+ ==> EX! n. ([-a, 1] %^ n) divides p &
+ ~(([-a, 1] %^ (Suc n)) divides p)"
+apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
+apply (cut_tac m = y and n = n in less_linear)
+apply (drule_tac m = n in poly_exp_divides)
+apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides]
+ simp del: pmult_Cons pexp_Suc)
+done
+
+text{*Order*}
+
+lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n"
+by (blast intro: someI2)
+
+lemma order:
+ "(([-a, 1] %^ n) divides p &
+ ~(([-a, 1] %^ (Suc n)) divides p)) =
+ ((n = order a p) & ~(poly p = poly []))"
+apply (unfold order_def)
+apply (rule iffI)
+apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order)
+apply (blast intro!: poly_order [THEN [2] some1_equalityD])
+done
+
+lemma order2: "[| poly p \<noteq> poly [] |]
+ ==> ([-a, 1] %^ (order a p)) divides p &
+ ~(([-a, 1] %^ (Suc(order a p))) divides p)"
+by (simp add: order del: pexp_Suc)
+
+lemma order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
+ ~(([-a, 1] %^ (Suc n)) divides p)
+ |] ==> (n = order a p)"
+by (insert order [of a n p], auto)
+
+lemma order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
+ ~(([-a, 1] %^ (Suc n)) divides p))
+ ==> (n = order a p)"
+by (blast intro: order_unique)
+
+lemma order_poly: "poly p = poly q ==> order a p = order a q"
+by (auto simp add: fun_eq divides_def poly_mult order_def)
+
+lemma pexp_one: "p %^ (Suc 0) = p"
+apply (induct_tac "p")
+apply (auto simp add: numeral_1_eq_1)
+done
+declare pexp_one [simp]
+
+lemma lemma_order_root [rule_format]:
+ "\<forall>p a. 0 < n & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
+ --> poly p a = 0"
+apply (induct_tac "n", blast)
+apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
+done
+
+lemma order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
+apply (case_tac "poly p = poly []", auto)
+apply (simp add: poly_linear_divides del: pmult_Cons, safe)
+apply (drule_tac [!] a = a in order2)
+apply (rule ccontr)
+apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
+apply (blast intro: lemma_order_root)
+done
+
+lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
+apply (case_tac "poly p = poly []", auto)
+apply (simp add: divides_def fun_eq poly_mult)
+apply (rule_tac x = "[]" in exI)
+apply (auto dest!: order2 [where a=a]
+ intro: poly_exp_divides simp del: pexp_Suc)
+done
+
+lemma order_decomp:
+ "poly p \<noteq> poly []
+ ==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
+ ~([-a, 1] divides q)"
+apply (unfold divides_def)
+apply (drule order2 [where a = a])
+apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
+apply (rule_tac x = q in exI, safe)
+apply (drule_tac x = qa in spec)
+apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
+done
+
+text{*Important composition properties of orders.*}
+
+lemma order_mult: "poly (p *** q) \<noteq> poly []
+ ==> order a (p *** q) = order a p + order a q"
+apply (cut_tac a = a and p = "p***q" and n = "order a p + order a q" in order)
+apply (auto simp add: poly_entire simp del: pmult_Cons)
+apply (drule_tac a = a in order2)+
+apply safe
+apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
+apply (rule_tac x = "qa *** qaa" in exI)
+apply (simp add: poly_mult mult_ac del: pmult_Cons)
+apply (drule_tac a = a in order_decomp)+
+apply safe
+apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
+apply (simp add: poly_primes del: pmult_Cons)
+apply (auto simp add: divides_def simp del: pmult_Cons)
+apply (rule_tac x = qb in exI)
+apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))")
+apply (drule poly_mult_left_cancel [THEN iffD1], force)
+apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
+apply (drule poly_mult_left_cancel [THEN iffD1], force)
+apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
+done
+
+(* FIXME: too too long! *)
+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
+ --> n = Suc (order a (pderiv p))"
+apply (induct_tac "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 swap, assumption)
+apply (rotate_tac 3, erule swap)
+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 field_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)
+done
+
+lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; 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 (drule_tac a = a and p = p in order_decomp)
+apply (blast intro: lemma_order_pderiv)
+done
+
+text{*Now justify the standard squarefree decomposition, i.e. f / gcd(f,f'). *)
+(* `a la Harrison*}
+
+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)
+done
+
+
+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)
+ |] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
+apply (blast intro: poly_squarefree_decomp_order)
+done
+
+lemma order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
+by (rule order_root [THEN ssubst], auto)
+
+lemma order_pderiv2: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
+ ==> (order a (pderiv p) = n) = (order a p = Suc n)"
+apply (auto dest: order_pderiv)
+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 simp
+apply (drule pderiv_iszero, clarify)
+apply (subgoal_tac "\<forall>a. order a p = order a [h]")
+apply (simp add: fun_eq)
+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 (auto simp add: order_root order_pderiv2)
+apply (drule spec, auto)
+done
+
+lemma pmult_one: "[1] *** p = p"
+by auto
+declare pmult_one [simp]
+
+lemma poly_Nil_zero: "poly [] = poly [0]"
+by (simp add: fun_eq)
+
+lemma rsquarefree_decomp:
+ "[| rsquarefree p; poly p a = 0 |]
+ ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
+apply (simp add: rsquarefree_def, safe)
+apply (frule_tac a = a in order_decomp)
+apply (drule_tac x = a in spec)
+apply (drule_tac a1 = a in order_root2 [symmetric])
+apply (auto simp del: pmult_Cons)
+apply (rule_tac x = q in exI, safe)
+apply (simp add: poly_mult fun_eq)
+apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1])
+apply (simp add: divides_def del: pmult_Cons, safe)
+apply (drule_tac x = "[]" in spec)
+apply (auto simp add: fun_eq)
+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
+
+
+text{*Normalization of a polynomial.*}
+
+lemma poly_normalize: "poly (pnormalize p) = poly p"
+apply (induct_tac "p")
+apply (auto simp add: fun_eq)
+done
+declare poly_normalize [simp]
+
+
+text{*The degree of a polynomial.*}
+
+lemma lemma_degree_zero [rule_format]:
+ "list_all (%c. c = 0) p --> pnormalize p = []"
+by (induct_tac "p", auto)
+
+lemma degree_zero: "poly p = poly [] ==> degree p = 0"
+apply (simp add: degree_def)
+apply (case_tac "pnormalize p = []")
+apply (auto dest: lemma_degree_zero simp add: poly_zero)
+done
+
+text{*Tidier versions of finiteness of roots.*}
+
+lemma poly_roots_finite_set: "poly p \<noteq> poly [] ==> finite {x. poly p x = 0}"
+apply (auto simp add: poly_roots_finite)
+apply (rule_tac B = "{x::real. \<exists>n. (n::nat) < N & (x = j n) }" in finite_subset)
+apply (induct_tac [2] "N", auto)
+apply (subgoal_tac "{x::real. \<exists>na. na < Suc n & (x = j na) } = { (j n) } Un {x. \<exists>na. na < n & (x = j na) }")
+apply (auto simp add: less_Suc_eq)
+done
+
+text{*bound for polynomial.*}
+
+lemma poly_mono: "abs(x) \<le> k ==> abs(poly p x) \<le> poly (map abs p) k"
+apply (induct_tac "p", auto)
+apply (rule_tac j = "abs a + abs (x * poly list x) " in real_le_trans)
+apply (rule abs_triangle_ineq)
+apply (auto intro!: mult_mono simp add: abs_mult, arith)
+done
+
+ML
+{*
+val padd_Nil2 = thm "padd_Nil2";
+val padd_Cons_Cons = thm "padd_Cons_Cons";
+val pminus_Nil = thm "pminus_Nil";
+val pmult_singleton = thm "pmult_singleton";
+val poly_ident_mult = thm "poly_ident_mult";
+val poly_simple_add_Cons = thm "poly_simple_add_Cons";
+val padd_commut = thm "padd_commut";
+val padd_assoc = thm "padd_assoc";
+val poly_cmult_distr = thm "poly_cmult_distr";
+val pmult_by_x = thm "pmult_by_x";
+val poly_add = thm "poly_add";
+val poly_cmult = thm "poly_cmult";
+val poly_minus = thm "poly_minus";
+val poly_mult = thm "poly_mult";
+val poly_exp = thm "poly_exp";
+val poly_add_rzero = thm "poly_add_rzero";
+val poly_mult_assoc = thm "poly_mult_assoc";
+val poly_mult_Nil2 = thm "poly_mult_Nil2";
+val poly_exp_add = thm "poly_exp_add";
+val pderiv_Nil = thm "pderiv_Nil";
+val pderiv_singleton = thm "pderiv_singleton";
+val pderiv_Cons = thm "pderiv_Cons";
+val DERIV_cmult2 = thm "DERIV_cmult2";
+val DERIV_pow2 = thm "DERIV_pow2";
+val lemma_DERIV_poly1 = thm "lemma_DERIV_poly1";
+val lemma_DERIV_poly = thm "lemma_DERIV_poly";
+val DERIV_add_const = thm "DERIV_add_const";
+val poly_DERIV = thm "poly_DERIV";
+val poly_differentiable = thm "poly_differentiable";
+val poly_isCont = thm "poly_isCont";
+val poly_IVT_pos = thm "poly_IVT_pos";
+val poly_IVT_neg = thm "poly_IVT_neg";
+val poly_MVT = thm "poly_MVT";
+val lemma_poly_pderiv_aux_add = thm "lemma_poly_pderiv_aux_add";
+val poly_pderiv_aux_add = thm "poly_pderiv_aux_add";
+val lemma_poly_pderiv_aux_cmult = thm "lemma_poly_pderiv_aux_cmult";
+val poly_pderiv_aux_cmult = thm "poly_pderiv_aux_cmult";
+val poly_pderiv_aux_minus = thm "poly_pderiv_aux_minus";
+val lemma_poly_pderiv_aux_mult1 = thm "lemma_poly_pderiv_aux_mult1";
+val lemma_poly_pderiv_aux_mult = thm "lemma_poly_pderiv_aux_mult";
+val lemma_poly_pderiv_add = thm "lemma_poly_pderiv_add";
+val poly_pderiv_add = thm "poly_pderiv_add";
+val poly_pderiv_cmult = thm "poly_pderiv_cmult";
+val poly_pderiv_minus = thm "poly_pderiv_minus";
+val lemma_poly_mult_pderiv = thm "lemma_poly_mult_pderiv";
+val poly_pderiv_mult = thm "poly_pderiv_mult";
+val poly_pderiv_exp = thm "poly_pderiv_exp";
+val poly_pderiv_exp_prime = thm "poly_pderiv_exp_prime";
+val lemma_poly_linear_rem = thm "lemma_poly_linear_rem";
+val poly_linear_rem = thm "poly_linear_rem";
+val poly_linear_divides = thm "poly_linear_divides";
+val lemma_poly_length_mult = thm "lemma_poly_length_mult";
+val lemma_poly_length_mult2 = thm "lemma_poly_length_mult2";
+val poly_length_mult = thm "poly_length_mult";
+val poly_cmult_length = thm "poly_cmult_length";
+val poly_add_length = thm "poly_add_length";
+val poly_root_mult_length = thm "poly_root_mult_length";
+val poly_mult_not_eq_poly_Nil = thm "poly_mult_not_eq_poly_Nil";
+val poly_mult_eq_zero_disj = thm "poly_mult_eq_zero_disj";
+val poly_normalized_nil = thm "poly_normalized_nil";
+val poly_roots_index_lemma = thm "poly_roots_index_lemma";
+val poly_roots_index_lemma2 = thms "poly_roots_index_lemma2";
+val poly_roots_index_length = thm "poly_roots_index_length";
+val poly_roots_finite_lemma = thm "poly_roots_finite_lemma";
+val real_finite_lemma = thm "real_finite_lemma";
+val poly_roots_finite = thm "poly_roots_finite";
+val poly_entire_lemma = thm "poly_entire_lemma";
+val poly_entire = thm "poly_entire";
+val poly_entire_neg = thm "poly_entire_neg";
+val fun_eq = thm "fun_eq";
+val poly_add_minus_zero_iff = thm "poly_add_minus_zero_iff";
+val poly_add_minus_mult_eq = thm "poly_add_minus_mult_eq";
+val poly_mult_left_cancel = thm "poly_mult_left_cancel";
+val real_mult_zero_disj_iff = thm "real_mult_zero_disj_iff";
+val poly_exp_eq_zero = thm "poly_exp_eq_zero";
+val poly_prime_eq_zero = thm "poly_prime_eq_zero";
+val poly_exp_prime_eq_zero = thm "poly_exp_prime_eq_zero";
+val poly_zero_lemma = thm "poly_zero_lemma";
+val poly_zero = thm "poly_zero";
+val pderiv_aux_iszero = thm "pderiv_aux_iszero";
+val pderiv_aux_iszero_num = thm "pderiv_aux_iszero_num";
+val pderiv_iszero = thm "pderiv_iszero";
+val pderiv_zero_obj = thm "pderiv_zero_obj";
+val pderiv_zero = thm "pderiv_zero";
+val poly_pderiv_welldef = thm "poly_pderiv_welldef";
+val poly_primes = thm "poly_primes";
+val poly_divides_refl = thm "poly_divides_refl";
+val poly_divides_trans = thm "poly_divides_trans";
+val le_iff_add = thm "le_iff_add";
+val poly_divides_exp = thm "poly_divides_exp";
+val poly_exp_divides = thm "poly_exp_divides";
+val poly_divides_add = thm "poly_divides_add";
+val poly_divides_diff = thm "poly_divides_diff";
+val poly_divides_diff2 = thm "poly_divides_diff2";
+val poly_divides_zero = thm "poly_divides_zero";
+val poly_divides_zero2 = thm "poly_divides_zero2";
+val poly_order_exists_lemma = thm "poly_order_exists_lemma";
+val poly_order_exists = thm "poly_order_exists";
+val poly_one_divides = thm "poly_one_divides";
+val poly_order = thm "poly_order";
+val some1_equalityD = thm "some1_equalityD";
+val order = thm "order";
+val order2 = thm "order2";
+val order_unique = thm "order_unique";
+val order_unique_lemma = thm "order_unique_lemma";
+val order_poly = thm "order_poly";
+val pexp_one = thm "pexp_one";
+val lemma_order_root = thm "lemma_order_root";
+val order_root = thm "order_root";
+val order_divides = thm "order_divides";
+val order_decomp = thm "order_decomp";
+val order_mult = thm "order_mult";
+val lemma_order_pderiv = thm "lemma_order_pderiv";
+val order_pderiv = thm "order_pderiv";
+val poly_squarefree_decomp_order = thm "poly_squarefree_decomp_order";
+val poly_squarefree_decomp_order2 = thm "poly_squarefree_decomp_order2";
+val order_root2 = thm "order_root2";
+val order_pderiv2 = thm "order_pderiv2";
+val rsquarefree_roots = thm "rsquarefree_roots";
+val pmult_one = thm "pmult_one";
+val poly_Nil_zero = thm "poly_Nil_zero";
+val rsquarefree_decomp = thm "rsquarefree_decomp";
+val poly_squarefree_decomp = thm "poly_squarefree_decomp";
+val poly_normalize = thm "poly_normalize";
+val lemma_degree_zero = thm "lemma_degree_zero";
+val degree_zero = thm "degree_zero";
+val poly_roots_finite_set = thm "poly_roots_finite_set";
+val poly_mono = thm "poly_mono";
+*}
end
--- a/src/HOL/Hyperreal/SEQ.ML Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Fri Mar 05 15:18:59 2004 +0100
@@ -76,18 +76,18 @@
by (dres_inst_tac [("x","xa")] spec 1);
by (dres_inst_tac [("x","x")] spec 2);
by (Auto_tac);
-val lemma_NSLIMSEQ1 = result();
+qed "lemma_NSLIMSEQ1";
Goal "{n. f n <= Suc u} = {n. f n <= u} Un {n. f n = Suc u}";
by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
-val lemma_NSLIMSEQ2 = result();
+qed "lemma_NSLIMSEQ2";
Goal "!!(f::nat=>nat). ALL n. n <= f n \
\ ==> {n. f n = Suc u} <= {n. n <= Suc u}";
by (Auto_tac);
by (dres_inst_tac [("x","x")] spec 1);
by (Auto_tac);
-val lemma_NSLIMSEQ3 = result();
+qed "lemma_NSLIMSEQ3";
Goal "!!(f::nat=>nat). ALL n. n <= f n \
\ ==> finite {n. f n <= u}";
@@ -127,7 +127,7 @@
Goal "{n. abs (X (f n) + - L) < r} Int {n. r <= abs (X (f n) + - (L::real))} \
\ = {}";
by Auto_tac;
-val lemmaLIM2 = result();
+qed "lemmaLIM2";
Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \
\ ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
@@ -145,7 +145,7 @@
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [lemmaLIM2,
FreeUltrafilterNat_empty]) 1);
-val lemmaLIM3 = result();
+qed "lemmaLIM3";
Goalw [LIMSEQ_def,NSLIMSEQ_def]
"X ----NS> L ==> X ----> L";
@@ -445,7 +445,7 @@
(* a few lemmas *)
Goal "ALL n. abs(X n) <= K ==> ALL n. abs(X((f::nat=>nat) n)) <= K";
by (Auto_tac);
-val lemma_Bseq = result();
+qed "lemma_Bseq";
Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X";
by (Step_tac 1);
@@ -477,14 +477,14 @@
by (Step_tac 1);
by (cut_inst_tac [("n","N")] real_of_nat_Suc_gt_zero 1);
by (Blast_tac 1);
-val lemmaNSBseq = result();
+qed "lemmaNSBseq";
Goal "ALL K. 0 < K --> (EX n. K < abs (X n)) \
\ ==> EX f. ALL N. real(Suc N) < abs (X (f N))";
by (dtac lemmaNSBseq 1);
by (dtac choice 1);
by (Blast_tac 1);
-val lemmaNSBseq2 = result();
+qed "lemmaNSBseq2";
Goal "ALL N. real(Suc N) < abs (X (f N)) \
\ ==> Abs_hypreal(hyprel``{X o f}) : HInfinite";
@@ -506,7 +506,7 @@
\ {n. f n <= u & real(Suc n) < abs (X (f n))} \
\ Un {n. real(Suc n) < abs (X (Suc u))}";
by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
-val lemma_finite_NSBseq = result();
+qed "lemma_finite_NSBseq";
Goal "finite {n. f n <= (u::nat) & real(Suc n) < abs(X(f n))}";
by (induct_tac "u" 1);
@@ -515,7 +515,7 @@
by (rtac (lemma_finite_NSBseq RS finite_subset) 2);
by (auto_tac (claset() addIs [finite_real_of_nat_less_real],
simpset() addsimps [real_of_nat_Suc, less_diff_eq RS sym]));
-val lemma_finite_NSBseq2 = result();
+qed "lemma_finite_NSBseq2";
Goal "ALL N. real(Suc N) < abs (X (f N)) \
\ ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite";
@@ -619,7 +619,7 @@
by (Step_tac 1);
by (dres_inst_tac [("y","X n")] isLubD2 1);
by (ALLGOALS(blast_tac (claset() addDs [real_le_anti_sym])));
-val lemma_converg1 = result();
+qed "lemma_converg1";
(*-------------------------------------------------------------------
The best of both world: Easier to prove this result as a standard
@@ -651,13 +651,13 @@
by (dres_inst_tac [("y","X m")] isLubD2 1);
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq],
simpset()));
-val lemma_converg2 = result();
+qed "lemma_converg2";
Goal "!!(X ::nat=>real). ALL m. X m <= U ==> \
\ isUb UNIV {x. EX n. X n = x} U";
by (rtac (setleI RS isUbI) 1);
by (Auto_tac);
-val lemma_converg3 = result();
+qed "lemma_converg3";
(* FIXME: U - T < U redundant *)
Goal "!!(X::nat=> real). \
@@ -673,7 +673,7 @@
by (dtac isLub_le_isUb 1 THEN assume_tac 1);
by (auto_tac (claset() addDs [order_less_le_trans],
simpset()));
-val lemma_converg4 = result();
+qed "lemma_converg4";
(*-------------------------------------------------------------------
A standard proof of the theorem for monotone increasing sequence
@@ -777,13 +777,13 @@
simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
by (dres_inst_tac [("x","M")] spec 1);
by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1);
-val lemmaCauchy1 = result();
+qed "lemmaCauchy1";
Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \
\ {n. M <= xa n} Int {n. M <= x n} <= \
\ {n. abs (X (xa n) + - X (x n)) < u}";
by (Blast_tac 1);
-val lemmaCauchy2 = result();
+qed "lemmaCauchy2";
Goalw [Cauchy_def,NSCauchy_def]
"Cauchy X ==> NSCauchy X";
@@ -858,7 +858,7 @@
by (Step_tac 1);
by (dtac spec 1 THEN Auto_tac);
by (arith_tac 1);
-val lemmaCauchy = result();
+qed "lemmaCauchy";
Goal "(n < Suc M) = (n <= M)";
by Auto_tac;
@@ -894,29 +894,29 @@
by (REPEAT(dres_inst_tac [("x","m")] spec 1));
by (auto_tac (claset() addEs [less_asym],
simpset() addsimps [le_def]));
-val lemma_Nat_covered = result();
+qed "lemma_Nat_covered";
Goal "[| ALL n. n <= M --> abs ((X::nat=>real) n) <= a; a < b |] \
\ ==> ALL n. n <= M --> abs(X n) <= b";
by (blast_tac (claset() addIs [order_le_less_trans RS order_less_imp_le]) 1);
-val lemma_trans1 = result();
+qed "lemma_trans1";
Goal "[| ALL n. M <= n --> abs ((X::nat=>real) n) < a; \
\ a < b |] \
\ ==> ALL n. M <= n --> abs(X n)<= b";
by (blast_tac (claset() addIs [order_less_trans RS order_less_imp_le]) 1);
-val lemma_trans2 = result();
+qed "lemma_trans2";
Goal "[| ALL n. n <= M --> abs (X n) <= a; \
\ a = b |] \
\ ==> ALL n. n <= M --> abs(X n) <= b";
by (Auto_tac);
-val lemma_trans3 = result();
+qed "lemma_trans3";
Goal "ALL n. M <= n --> abs ((X::nat=>real) n) < a \
\ ==> ALL n. M <= n --> abs (X n) <= a";
by (blast_tac (claset() addIs [order_less_imp_le]) 1);
-val lemma_trans4 = result();
+qed "lemma_trans4";
(*----------------------------------------------------------
Trickier than expected --- proof is more involved than
--- a/src/HOL/Hyperreal/Transcendental.ML Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Fri Mar 05 15:18:59 2004 +0100
@@ -333,21 +333,21 @@
\ else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0";
by (induct_tac "n" 1);
by (Auto_tac);
-val lemma_STAR_sin = result();
+qed "lemma_STAR_sin";
Addsimps [lemma_STAR_sin];
Goal "0 < n --> \
\ (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0";
by (induct_tac "n" 1);
by (Auto_tac);
-val lemma_STAR_cos = result();
+qed "lemma_STAR_cos";
Addsimps [lemma_STAR_cos];
Goal "0 < n --> \
\ (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0";
by (induct_tac "n" 1);
by (Auto_tac);
-val lemma_STAR_cos1 = result();
+qed "lemma_STAR_cos1";
Addsimps [lemma_STAR_cos1];
Goal "sumr 1 n (%n. if even n \
@@ -357,7 +357,7 @@
by (induct_tac "n" 1);
by (case_tac "n" 2);
by (Auto_tac);
-val lemma_STAR_cos2 = result();
+qed "lemma_STAR_cos2";
Addsimps [lemma_STAR_cos2];
Goalw [exp_def] "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)";
@@ -812,7 +812,7 @@
by (rtac ext 1);
by (stac fact_Suc 1);
by (stac real_of_nat_mult 1);
-by (stac even_Suc 1);
+by (stac even_nat_Suc 1);
by (stac inverse_mult_distrib 1);
by Auto_tac;
qed "sin_fdiffs";
@@ -825,7 +825,7 @@
\ else 0)";
by (stac fact_Suc 1);
by (stac real_of_nat_mult 1);
-by (stac even_Suc 1);
+by (stac even_nat_Suc 1);
by (stac inverse_mult_distrib 1);
by Auto_tac;
qed "sin_fdiffs2";
@@ -838,7 +838,7 @@
by (rtac ext 1);
by (stac fact_Suc 1);
by (stac real_of_nat_mult 1);
-by (stac even_Suc 1);
+by (stac even_nat_Suc 1);
by (stac inverse_mult_distrib 1);
by (res_inst_tac [("a1","real (Suc n)")] (mult_commute RS ssubst) 1);
by (res_inst_tac [("a1","inverse(real (Suc n))")]
@@ -855,7 +855,7 @@
\ else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))";
by (stac fact_Suc 1);
by (stac real_of_nat_mult 1);
-by (stac even_Suc 1);
+by (stac even_nat_Suc 1);
by (stac inverse_mult_distrib 1);
by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1);
by (res_inst_tac [("z1","inverse (real (Suc n))")]
@@ -876,7 +876,7 @@
Goal "exp = (%x. suminf (%n. inverse (real (fact n)) * x ^ n))";
by (auto_tac (claset() addSIs [ext],simpset() addsimps [exp_def]));
-val lemma_exp_ext = result();
+qed "lemma_exp_ext";
Goalw [exp_def] "DERIV exp x :> exp(x)";
by (stac lemma_exp_ext 1);
@@ -893,13 +893,13 @@
\ else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * \
\ x ^ n))";
by (auto_tac (claset() addSIs [ext],simpset() addsimps [sin_def]));
-val lemma_sin_ext = result();
+qed "lemma_sin_ext";
Goal "cos = (%x. suminf(%n. (if even n then \
\ (- 1) ^ (n div 2)/(real (fact n)) \
\ else 0) * x ^ n))";
by (auto_tac (claset() addSIs [ext],simpset() addsimps [cos_def]));
-val lemma_cos_ext = result();
+qed "lemma_cos_ext";
Goalw [cos_def] "DERIV sin x :> cos(x)";
by (stac lemma_sin_ext 1);
@@ -1284,7 +1284,7 @@
Goal "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E";
by (Auto_tac);
-val lemma_DERIV_subst = result();
+qed "lemma_DERIV_subst";
Goal "DERIV (%x. cos(x) ^ 2) x :> -(2 * cos(x) * sin(x))";
by (rtac lemma_DERIV_subst 1);
@@ -1457,7 +1457,7 @@
by (auto_tac (claset(),simpset() addsimps [real_diff_def,
left_distrib,right_distrib] @
mult_ac @ add_ac));
-val lemma_DERIV_sin_cos_add = result();
+qed "lemma_DERIV_sin_cos_add";
Goal "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 + \
\ (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0";
@@ -1485,7 +1485,7 @@
by (auto_tac (claset(),simpset() addsimps [real_diff_def,
left_distrib,right_distrib]
@ mult_ac @ add_ac));
-val lemma_DERIV_sin_cos_minus = result();
+qed "lemma_DERIV_sin_cos_minus";
Goal "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0";
by (cut_inst_tac [("y","0"),("x","x")]
@@ -1550,7 +1550,7 @@
Goal "real (Suc (Suc (Suc (Suc 2)))) = \
\ real (2::nat) * real (Suc 2)";
by (simp_tac (simpset() addsimps [numeral_2_eq_2, real_of_nat_Suc]) 1);
-val lemma_real_of_nat_six_mult = result();
+qed "lemma_real_of_nat_six_mult";
Goal "[|0 < x; x < 2 |] ==> 0 < sin x";
by (cut_inst_tac [("x2","x")] (CLAIM "0 < (2::nat)" RS ((sin_paired
@@ -2056,7 +2056,7 @@
by (auto_tac (claset(),
simpset() delsimps [inverse_mult_distrib]
addsimps [mult_assoc, left_diff_distrib,cos_add]));
-val lemma_tan_add1 = result();
+qed "lemma_tan_add1";
Addsimps [lemma_tan_add1];
Goalw [tan_def]
--- a/src/HOL/IsaMakefile Fri Mar 05 11:43:55 2004 +0100
+++ b/src/HOL/IsaMakefile Fri Mar 05 15:18:59 2004 +0100
@@ -150,8 +150,7 @@
Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy Hyperreal/IntFloor.thy\
Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.thy\
Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
- Hyperreal/NSA.thy Hyperreal/NthRoot.thy\
- Hyperreal/Poly.ML Hyperreal/Poly.thy\
+ Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\
Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.thy\
Hyperreal/Star.thy Hyperreal/Transcendental.ML\
Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \