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.14  text{*addition*}
    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")
    1.76 -apply (simp add: poly_exp)
    1.77 -using zero_neq_one apply blast
    1.78 +apply (induct n)
    1.79  apply (auto simp add: poly_exp poly_mult)
    1.80  done
    1.81