21 |
21 |
22 |
22 |
23 subsection{*Arithmetic Operations on Polynomials*} |
23 subsection{*Arithmetic Operations on Polynomials*} |
24 |
24 |
25 text{*addition*} |
25 text{*addition*} |
26 consts "+++" :: "[real list, real list] => real list" (infixl 65) |
26 consts padd :: "[real list, real list] => real list" (infixl "+++" 65) |
27 primrec |
27 primrec |
28 padd_Nil: "[] +++ l2 = l2" |
28 padd_Nil: "[] +++ l2 = l2" |
29 padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t |
29 padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t |
30 else (h + hd l2)#(t +++ tl l2))" |
30 else (h + hd l2)#(t +++ tl l2))" |
31 |
31 |
32 text{*Multiplication by a constant*} |
32 text{*Multiplication by a constant*} |
33 consts "%*" :: "[real, real list] => real list" (infixl 70) |
33 consts cmult :: "[real, real list] => real list" (infixl "%*" 70) |
34 primrec |
34 primrec |
35 cmult_Nil: "c %* [] = []" |
35 cmult_Nil: "c %* [] = []" |
36 cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)" |
36 cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)" |
37 |
37 |
38 text{*Multiplication by a polynomial*} |
38 text{*Multiplication by a polynomial*} |
39 consts "***" :: "[real list, real list] => real list" (infixl 70) |
39 consts pmult :: "[real list, real list] => real list" (infixl "***" 70) |
40 primrec |
40 primrec |
41 pmult_Nil: "[] *** l2 = []" |
41 pmult_Nil: "[] *** l2 = []" |
42 pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2 |
42 pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2 |
43 else (h %* l2) +++ ((0) # (t *** l2)))" |
43 else (h %* l2) +++ ((0) # (t *** l2)))" |
44 |
44 |
48 mulexp_zero: "mulexp 0 p q = q" |
48 mulexp_zero: "mulexp 0 p q = q" |
49 mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q" |
49 mulexp_Suc: "mulexp (Suc n) p q = p *** mulexp n p q" |
50 |
50 |
51 |
51 |
52 text{*Exponential*} |
52 text{*Exponential*} |
53 consts "%^" :: "[real list, nat] => real list" (infixl 80) |
53 consts pexp :: "[real list, nat] => real list" (infixl "%^" 80) |
54 primrec |
54 primrec |
55 pexp_0: "p %^ 0 = [1]" |
55 pexp_0: "p %^ 0 = [1]" |
56 pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)" |
56 pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)" |
57 |
57 |
58 text{*Quotient related value of dividing a polynomial by x + a*} |
58 text{*Quotient related value of dividing a polynomial by x + a*} |