equal
deleted
inserted
replaced
15 |
15 |
16 typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set" |
16 typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set" |
17 morphisms coeff Abs_poly |
17 morphisms coeff Abs_poly |
18 unfolding Poly_def by auto |
18 unfolding Poly_def by auto |
19 |
19 |
|
20 (* FIXME should be named poly_eq_iff *) |
20 lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)" |
21 lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)" |
21 by (simp add: coeff_inject [symmetric] fun_eq_iff) |
22 by (simp add: coeff_inject [symmetric] fun_eq_iff) |
22 |
23 |
|
24 (* FIXME should be named poly_eqI *) |
23 lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q" |
25 lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q" |
24 by (simp add: expand_poly_eq) |
26 by (simp add: expand_poly_eq) |
25 |
27 |
26 |
28 |
27 subsection {* Degree of a polynomial *} |
29 subsection {* Degree of a polynomial *} |