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:]"
-  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"

-  "lead_coeff (of_nat n) = (of_nat n :: 'a::{comm_semiring_1,semiring_char_0})"
+  "lead_coeff (of_nat n) = of_nat n"

-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"

-  "lead_coeff (of_int k) = (of_int k :: 'a::{comm_ring_1,ring_char_0})"
+  "lead_coeff (of_int k) = of_int k"

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):]"
+  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"