src/HOL/Library/Univ_Poly.thy
 changeset 26194 b9763c3272cb parent 26124 2514f0ade8bc child 26313 8590bf5ef343
```--- a/src/HOL/Library/Univ_Poly.thy	Mon Mar 03 15:37:14 2008 +0100
+++ b/src/HOL/Library/Univ_Poly.thy	Mon Mar 03 15:37:16 2008 +0100
@@ -11,7 +11,7 @@

text{* Application of polynomial as a function. *}

-fun (in semiring_0) poly :: "'a list => 'a  => 'a" where
+primrec (in semiring_0) poly :: "'a list => 'a  => 'a" where
poly_Nil:  "poly [] x = 0"
| poly_Cons: "poly (h#t) x = h + x * poly t x"

@@ -20,43 +20,43 @@

text{*addition*}

-fun (in semiring_0) padd :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "+++" 65)
+primrec (in semiring_0) padd :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "+++" 65)
where
padd_Nil:  "[] +++ l2 = l2"
| padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
else (h + hd l2)#(t +++ tl l2))"

text{*Multiplication by a constant*}
-fun (in semiring_0) cmult :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "%*" 70) where
+primrec (in semiring_0) cmult :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "%*" 70) where
cmult_Nil:  "c %* [] = []"
|  cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"

text{*Multiplication by a polynomial*}
-fun (in semiring_0) pmult :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "***" 70)
+primrec (in semiring_0) pmult :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "***" 70)
where
pmult_Nil:  "[] *** l2 = []"
|  pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
else (h %* l2) +++ ((0) # (t *** l2)))"

text{*Repeated multiplication by a polynomial*}
-fun (in semiring_0) mulexp :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a  list \<Rightarrow> 'a list" where
+primrec (in semiring_0) mulexp :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a  list \<Rightarrow> 'a list" where
mulexp_zero:  "mulexp 0 p q = q"
|  mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"

text{*Exponential*}
-fun (in semiring_1) pexp :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list"  (infixl "%^" 80) where
+primrec (in semiring_1) pexp :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list"  (infixl "%^" 80) where
pexp_0:   "p %^ 0 = [1]"
|  pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"

text{*Quotient related value of dividing a polynomial by x + a*}
(* Useful for divisor properties in inductive proofs *)
-fun (in field) "pquot" :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
+primrec (in field) "pquot" :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
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))"

text{*normalization of polynomials (remove extra 0 coeff)*}
-fun (in semiring_0) pnormalize :: "'a list \<Rightarrow> 'a list" where
+primrec (in semiring_0) pnormalize :: "'a list \<Rightarrow> 'a list" where
pnormalize_Nil:  "pnormalize [] = []"
| pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
then (if (h = 0) then [] else [h])
@@ -174,7 +174,6 @@
class recpower_ring = ring + recpower
class recpower_ring_1 = ring_1 + recpower
subclass (in recpower_ring_1) recpower_ring by unfold_locales
-subclass (in recpower_ring_1) recpower_ring by unfold_locales
class recpower_comm_semiring_1 = recpower + comm_semiring_1
class recpower_comm_ring_1 = recpower + comm_ring_1
subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by unfold_locales
@@ -439,9 +438,7 @@
apply (simp only: fun_eq add: all_simps [symmetric])
apply (rule arg_cong [where f = All])
apply (rule ext)
-apply (induct_tac "n")
-apply (simp add: poly_exp)
-using zero_neq_one apply blast
+apply (induct n)
apply (auto simp add: poly_exp poly_mult)
done
```