summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sun, 16 Apr 2017 15:30:03 +0200 | |

changeset 65484 | 751f9ed8e940 |

parent 65483 | 1cb9fd58d55e |

child 65485 | 8c7bc3a13513 |

more rules concerning of_nat, of_int, numeral

--- a/src/HOL/Computational_Algebra/Polynomial.thy Thu Apr 13 10:10:12 2017 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Sun Apr 16 15:30:03 2017 +0200 @@ -1213,46 +1213,57 @@ by (intro poly_eqI) (simp_all add: coeff_map_poly) -subsection \<open>Conversions from @{typ nat} and @{typ int} numbers\<close> - -lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]" -proof (induct n) - case 0 - then show ?case by simp -next - case (Suc n) - then have "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" - by simp - also have "(of_nat n :: 'a poly) = [: of_nat n :]" - by (subst Suc) (rule refl) - also have "1 = [:1:]" - by (simp add: one_poly_def) - finally show ?case - by (subst (asm) add_pCons) simp -qed - -lemma degree_of_nat [simp]: "degree (of_nat n) = 0" +subsection \<open>Conversions\<close> + +lemma of_nat_poly: + "of_nat n = [:of_nat n:]" + by (induct n) (simp_all add: one_poly_def) + +lemma of_nat_monom: + "of_nat n = monom (of_nat n) 0" + by (simp add: of_nat_poly monom_0) + +lemma degree_of_nat [simp]: + "degree (of_nat n) = 0" by (simp add: of_nat_poly) lemma lead_coeff_of_nat [simp]: - "lead_coeff (of_nat n) = (of_nat n :: 'a::{comm_semiring_1,semiring_char_0})" + "lead_coeff (of_nat n) = of_nat n" by (simp add: of_nat_poly) -lemma of_int_poly: "of_int k = [:of_int k :: 'a :: comm_ring_1:]" +lemma of_int_poly: + "of_int k = [:of_int k:]" by (simp only: of_int_of_nat of_nat_poly) simp -lemma degree_of_int [simp]: "degree (of_int k) = 0" +lemma of_int_monom: + "of_int k = monom (of_int k) 0" + by (simp add: of_int_poly monom_0) + +lemma degree_of_int [simp]: + "degree (of_int k) = 0" by (simp add: of_int_poly) lemma lead_coeff_of_int [simp]: - "lead_coeff (of_int k) = (of_int k :: 'a::{comm_ring_1,ring_char_0})" + "lead_coeff (of_int k) = of_int k" by (simp add: of_int_poly) lemma numeral_poly: "numeral n = [:numeral n:]" - by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp - -lemma degree_numeral [simp]: "degree (numeral n) = 0" - by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp +proof - + have "numeral n = of_nat (numeral n)" + by simp + also have "\<dots> = [:of_nat (numeral n):]" + by (simp add: of_nat_poly) + finally show ?thesis + by simp +qed + +lemma numeral_monom: + "numeral n = monom (numeral n) 0" + by (simp add: numeral_poly monom_0) + +lemma degree_numeral [simp]: + "degree (numeral n) = 0" + by (simp add: numeral_poly) lemma lead_coeff_numeral [simp]: "lead_coeff (numeral n) = numeral n"