--- a/src/HOL/Hyperreal/Poly.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/Poly.thy Fri Nov 17 02:20:03 2006 +0100
@@ -82,25 +82,30 @@
text{*Other definitions*}
definition
- poly_minus :: "real list => real list" ("-- _" [80] 80)
+ poly_minus :: "real list => real list" ("-- _" [80] 80) where
"-- p = (- 1) %* p"
- pderiv :: "real list => real list"
+definition
+ pderiv :: "real list => real list" where
"pderiv p = (if p = [] then [] else pderiv_aux 1 (tl p))"
- divides :: "[real list,real list] => bool" (infixl "divides" 70)
+definition
+ divides :: "[real list,real list] => bool" (infixl "divides" 70) where
"p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
- order :: "real => real list => nat"
+definition
+ order :: "real => real list => nat" where
--{*order of a polynomial*}
"order a p = (SOME n. ([-a, 1] %^ n) divides p &
~ (([-a, 1] %^ (Suc n)) divides p))"
- degree :: "real list => nat"
+definition
+ degree :: "real list => nat" where
--{*degree of a polynomial*}
"degree p = length (pnormalize p)"
- rsquarefree :: "real list => bool"
+definition
+ rsquarefree :: "real list => bool" where
--{*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)))"
@@ -108,7 +113,7 @@
lemma padd_Nil2: "p +++ [] = p"
-by (induct "p", auto)
+by (induct p) auto
declare padd_Nil2 [simp]
lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"