diff -r 37a7eb7fd5f7 -r b9763c3272cb src/HOL/Library/Univ_Poly.thy --- 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 \ 'a list \ 'a list" (infixl "+++" 65) +primrec (in semiring_0) padd :: "'a list \ 'a list \ '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 \ 'a list \ 'a list" (infixl "%*" 70) where +primrec (in semiring_0) cmult :: "'a \ 'a list \ '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 \ 'a list \ 'a list" (infixl "***" 70) +primrec (in semiring_0) pmult :: "'a list \ 'a list \ '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 \ 'a list \ 'a list \ 'a list" where +primrec (in semiring_0) mulexp :: "nat \ 'a list \ 'a list \ '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 \ nat \ 'a list" (infixl "%^" 80) where +primrec (in semiring_1) pexp :: "'a list \ nat \ '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 \ 'a \ 'a list" where +primrec (in field) "pquot" :: "'a list \ 'a \ '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 \ 'a list" where +primrec (in semiring_0) pnormalize :: "'a list \ '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