changeset 58259 | 52c35a59bbf5 |
parent 58249 | 180f1b3508ed |
child 58310 | 91ea607a34d8 |
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Tue Sep 09 20:51:36 2014 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Tue Sep 09 20:51:36 2014 +0200 @@ -60,6 +60,9 @@ text {* Defining the basic ring operations on normalized polynomials *} +lemma pol_size_nz[simp]: "size (p :: 'a pol) \<noteq> 0" + by (cases p) simp_all + function add :: "'a::comm_ring pol \<Rightarrow> 'a pol \<Rightarrow> 'a pol" (infixl "\<oplus>" 65) where "Pc a \<oplus> Pc b = Pc (a + b)"