171 class recpower_semiring = semiring + recpower |
171 class recpower_semiring = semiring + recpower |
172 class recpower_semiring_1 = semiring_1 + recpower |
172 class recpower_semiring_1 = semiring_1 + recpower |
173 class recpower_semiring_0 = semiring_0 + recpower |
173 class recpower_semiring_0 = semiring_0 + recpower |
174 class recpower_ring = ring + recpower |
174 class recpower_ring = ring + recpower |
175 class recpower_ring_1 = ring_1 + recpower |
175 class recpower_ring_1 = ring_1 + recpower |
176 subclass (in recpower_ring_1) recpower_ring by unfold_locales |
176 subclass (in recpower_ring_1) recpower_ring .. |
177 class recpower_comm_semiring_1 = recpower + comm_semiring_1 |
177 class recpower_comm_semiring_1 = recpower + comm_semiring_1 |
178 class recpower_comm_ring_1 = recpower + comm_ring_1 |
178 class recpower_comm_ring_1 = recpower + comm_ring_1 |
179 subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by unfold_locales |
179 subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 .. |
180 class recpower_idom = recpower + idom |
180 class recpower_idom = recpower + idom |
181 subclass (in recpower_idom) recpower_comm_ring_1 by unfold_locales |
181 subclass (in recpower_idom) recpower_comm_ring_1 .. |
182 class idom_char_0 = idom + ring_char_0 |
182 class idom_char_0 = idom + ring_char_0 |
183 class recpower_idom_char_0 = recpower + idom_char_0 |
183 class recpower_idom_char_0 = recpower + idom_char_0 |
184 subclass (in recpower_idom_char_0) recpower_idom by unfold_locales |
184 subclass (in recpower_idom_char_0) recpower_idom .. |
185 |
185 |
186 lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n" |
186 lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n" |
187 apply (induct "n") |
187 apply (induct "n") |
188 apply (auto simp add: poly_cmult poly_mult power_Suc) |
188 apply (auto simp add: poly_cmult poly_mult power_Suc) |
189 done |
189 done |
427 by (auto simp add: ring_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric]) |
427 by (auto simp add: ring_simps poly_add poly_minus_def fun_eq poly_cmult minus_mult_left[symmetric]) |
428 |
428 |
429 lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))" |
429 lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))" |
430 by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric]) |
430 by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric]) |
431 |
431 |
432 subclass (in idom_char_0) comm_ring_1 by unfold_locales |
432 subclass (in idom_char_0) comm_ring_1 .. |
433 lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)" |
433 lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)" |
434 proof- |
434 proof- |
435 have "poly (p *** q) = poly (p *** r) \<longleftrightarrow> poly (p *** q +++ -- (p *** r)) = poly []" by (simp only: poly_add_minus_zero_iff) |
435 have "poly (p *** q) = poly (p *** r) \<longleftrightarrow> poly (p *** q +++ -- (p *** r)) = poly []" by (simp only: poly_add_minus_zero_iff) |
436 also have "\<dots> \<longleftrightarrow> poly p = poly [] | poly q = poly r" |
436 also have "\<dots> \<longleftrightarrow> poly p = poly [] | poly q = poly r" |
437 by (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff) |
437 by (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff) |