src/HOL/Library/Univ_Poly.thy
 changeset 26194 b9763c3272cb parent 26124 2514f0ade8bc child 26313 8590bf5ef343
```     1.1 --- a/src/HOL/Library/Univ_Poly.thy	Mon Mar 03 15:37:14 2008 +0100
1.2 +++ b/src/HOL/Library/Univ_Poly.thy	Mon Mar 03 15:37:16 2008 +0100
1.3 @@ -11,7 +11,7 @@
1.4
1.5  text{* Application of polynomial as a function. *}
1.6
1.7 -fun (in semiring_0) poly :: "'a list => 'a  => 'a" where
1.8 +primrec (in semiring_0) poly :: "'a list => 'a  => 'a" where
1.9    poly_Nil:  "poly [] x = 0"
1.10  | poly_Cons: "poly (h#t) x = h + x * poly t x"
1.11
1.12 @@ -20,43 +20,43 @@
1.13
1.15
1.16 -fun (in semiring_0) padd :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "+++" 65)
1.17 +primrec (in semiring_0) padd :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "+++" 65)
1.18  where
1.19    padd_Nil:  "[] +++ l2 = l2"
1.20  | padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
1.21                              else (h + hd l2)#(t +++ tl l2))"
1.22
1.23  text{*Multiplication by a constant*}
1.24 -fun (in semiring_0) cmult :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "%*" 70) where
1.25 +primrec (in semiring_0) cmult :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "%*" 70) where
1.26     cmult_Nil:  "c %* [] = []"
1.27  |  cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
1.28
1.29  text{*Multiplication by a polynomial*}
1.30 -fun (in semiring_0) pmult :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "***" 70)
1.31 +primrec (in semiring_0) pmult :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixl "***" 70)
1.32  where
1.33     pmult_Nil:  "[] *** l2 = []"
1.34  |  pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
1.35                                else (h %* l2) +++ ((0) # (t *** l2)))"
1.36
1.37  text{*Repeated multiplication by a polynomial*}
1.38 -fun (in semiring_0) mulexp :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a  list \<Rightarrow> 'a list" where
1.39 +primrec (in semiring_0) mulexp :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a  list \<Rightarrow> 'a list" where
1.40     mulexp_zero:  "mulexp 0 p q = q"
1.41  |  mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
1.42
1.43  text{*Exponential*}
1.44 -fun (in semiring_1) pexp :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list"  (infixl "%^" 80) where
1.45 +primrec (in semiring_1) pexp :: "'a list \<Rightarrow> nat \<Rightarrow> 'a list"  (infixl "%^" 80) where
1.46     pexp_0:   "p %^ 0 = [1]"
1.47  |  pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
1.48
1.49  text{*Quotient related value of dividing a polynomial by x + a*}
1.50  (* Useful for divisor properties in inductive proofs *)
1.51 -fun (in field) "pquot" :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
1.52 +primrec (in field) "pquot" :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
1.53     pquot_Nil:  "pquot [] a= []"
1.54  |  pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
1.55                     else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
1.56
1.57  text{*normalization of polynomials (remove extra 0 coeff)*}
1.58 -fun (in semiring_0) pnormalize :: "'a list \<Rightarrow> 'a list" where
1.59 +primrec (in semiring_0) pnormalize :: "'a list \<Rightarrow> 'a list" where
1.60    pnormalize_Nil:  "pnormalize [] = []"
1.61  | pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
1.62                                       then (if (h = 0) then [] else [h])
1.63 @@ -174,7 +174,6 @@
1.64  class recpower_ring = ring + recpower
1.65  class recpower_ring_1 = ring_1 + recpower
1.66  subclass (in recpower_ring_1) recpower_ring by unfold_locales
1.67 -subclass (in recpower_ring_1) recpower_ring by unfold_locales
1.68  class recpower_comm_semiring_1 = recpower + comm_semiring_1
1.69  class recpower_comm_ring_1 = recpower + comm_ring_1
1.70  subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by unfold_locales
1.71 @@ -439,9 +438,7 @@
1.72  apply (simp only: fun_eq add: all_simps [symmetric])
1.73  apply (rule arg_cong [where f = All])
1.74  apply (rule ext)
1.75 -apply (induct_tac "n")