# HG changeset patch
# User chaieb
# Date 1181053936 -7200
# Node ID d797768d56553c2ccadcae961d3ff57cbb0f9c46
# Parent  631bd424fd72648901e92e7f859dda1ff9d37535
Polynomials now only depend on Deriv; Definition of degree changed

diff -r 631bd424fd72 -r d797768d5655 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Tue Jun 05 16:31:10 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Tue Jun 05 16:32:16 2007 +0200
@@ -9,7 +9,7 @@
 header{*Univariate Real Polynomials*}
 
 theory Poly
-imports Transcendental
+imports Deriv
 begin
 
 text{*Application of polynomial as a real function.*}
@@ -48,7 +48,6 @@
    mulexp_zero:  "mulexp 0 p q = q"
    mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
 
-
 text{*Exponential*}
 consts pexp :: "[real list, nat] => real list"  (infixl "%^" 80)
 primrec
@@ -78,7 +77,8 @@
                                      then (if (h = 0) then [] else [h])
                                      else (h#(pnormalize p)))"
 
-
+definition "pnormal p = ((pnormalize p = p) \<and> p \<noteq> [])"
+definition "nonconstant p = (pnormal p \<and> (\<forall>x. p \<noteq> [x]))"
 text{*Other definitions*}
 
 definition
@@ -102,7 +102,7 @@
 definition
   degree :: "real list => nat" where
      --{*degree of a polynomial*}
-  "degree p = length (pnormalize p)"
+  "degree p = length (pnormalize p) - 1"
 
 definition
   rsquarefree :: "real list => bool" where
@@ -296,7 +296,6 @@
 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 =
@@ -1003,16 +1002,38 @@
 
 text{*The degree of a polynomial.*}
 
-lemma lemma_degree_zero [rule_format]:
-     "list_all (%c. c = 0) p -->  pnormalize p = []"
+lemma lemma_degree_zero:
+     "list_all (%c. c = 0) p \<longleftrightarrow>  pnormalize p = []"
 by (induct "p", auto)
 
-lemma degree_zero: "poly p = poly [] ==> degree p = 0"
+lemma degree_zero: "(poly p = poly []) \<Longrightarrow> (degree p = 0)"
 apply (simp add: degree_def)
 apply (case_tac "pnormalize p = []")
-apply (auto dest: lemma_degree_zero simp add: poly_zero)
+apply (auto simp add: poly_zero lemma_degree_zero )
 done
 
+lemma pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp
+lemma pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp
+lemma pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)" 
+  unfolding pnormal_def by simp
+lemma pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p"
+  unfolding pnormal_def 
+  apply (cases "pnormalize p = []", auto)
+  by (cases "c = 0", auto)
+lemma pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0"
+  apply (induct p, auto simp add: pnormal_def)
+  apply (case_tac "pnormalize p = []", auto)
+  by (case_tac "a=0", auto)
+lemma  pnormal_length: "pnormal p \<Longrightarrow> 0 < length p"
+  unfolding pnormal_def length_greater_0_conv by blast
+lemma pnormal_last_length: "\<lbrakk>0 < length p ; last p \<noteq> 0\<rbrakk> \<Longrightarrow> pnormal p"
+  apply (induct p, auto)
+  apply (case_tac "p = []", auto)
+  apply (simp add: pnormal_def)
+  by (rule pnormal_cons, auto)
+lemma pnormal_id: "pnormal p \<longleftrightarrow> (0 < length p \<and> last p \<noteq> 0)"
+  using pnormal_last_length pnormal_length pnormal_last_nonzero by blast
+
 text{*Tidier versions of finiteness of roots.*}
 
 lemma poly_roots_finite_set: "poly p \<noteq> poly [] ==> finite {x. poly p x = 0}"
@@ -1032,4 +1053,5 @@
 apply (auto intro!: mult_mono simp add: abs_mult)
 done
 
+lemma poly_Sing: "poly [c] x = c" by simp
 end