# HG changeset patch
# User paulson
# Date 1078496339 -3600
# Node ID 9e22eeccf1298cf07ffe319a0c0832e0ec083b4a
# Parent  5f14c12074991c61e9eb926ac5dc7e0954093565
Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal

diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/EvenOdd.thy
--- 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";
 *}
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/HSeries.thy
--- 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:
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/HyperPow.thy
--- 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";
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/Integration.ML
--- 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 
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/Lim.ML
--- 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);
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/Poly.ML
--- 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"; 
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/Poly.thy
--- 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
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/SEQ.ML
--- 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
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/Hyperreal/Transcendental.ML
--- 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] 
diff -r 5f14c1207499 -r 9e22eeccf129 src/HOL/IsaMakefile
--- 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 \