equal
deleted
inserted
replaced
97 |
97 |
98 definition |
98 definition |
99 pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
99 pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
100 where |
100 where |
101 [code del]: "pCons a p = Abs_poly (nat_case a (coeff p))" |
101 [code del]: "pCons a p = Abs_poly (nat_case a (coeff p))" |
|
102 |
|
103 syntax |
|
104 "_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]") |
|
105 |
|
106 translations |
|
107 "[:x, xs:]" == "CONST pCons x [:xs:]" |
|
108 "[:x:]" == "CONST pCons x 0" |
102 |
109 |
103 lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly" |
110 lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly" |
104 unfolding Poly_def by (auto split: nat.split) |
111 unfolding Poly_def by (auto split: nat.split) |
105 |
112 |
106 lemma coeff_pCons: |
113 lemma coeff_pCons: |