src/HOL/Library/Polynomial.thy
 changeset 60570 7ed2cde6806d parent 60562 24af00b010cf child 60679 ade12ef2773c
```     1.1 --- a/src/HOL/Library/Polynomial.thy	Thu Jun 25 15:01:41 2015 +0200
1.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Jun 25 15:01:42 2015 +0200
1.3 @@ -244,6 +244,17 @@
1.4      using \<open>p = pCons a q\<close> by simp
1.5  qed
1.6
1.7 +lemma degree_eq_zeroE:
1.8 +  fixes p :: "'a::zero poly"
1.9 +  assumes "degree p = 0"
1.10 +  obtains a where "p = pCons a 0"
1.11 +proof -
1.12 +  obtain a q where p: "p = pCons a q" by (cases p)
1.13 +  with assms have "q = 0" by (cases "q = 0") simp_all
1.14 +  with p have "p = pCons a 0" by simp
1.15 +  with that show thesis .
1.16 +qed
1.17 +
1.18
1.19  subsection \<open>List-style syntax for polynomials\<close>
1.20
1.21 @@ -297,7 +308,7 @@
1.22    }
1.23    note * = this
1.24    show ?thesis
1.25 -    by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
1.26 +    by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
1.27  qed
1.28
1.29  lemma not_0_cCons_eq [simp]:
1.30 @@ -876,6 +887,10 @@
1.31    unfolding one_poly_def
1.32    by (simp add: coeff_pCons split: nat.split)
1.33
1.34 +lemma monom_eq_1 [simp]:
1.35 +  "monom 1 0 = 1"
1.36 +  by (simp add: monom_0 one_poly_def)
1.37 +
1.38  lemma degree_1 [simp]: "degree 1 = 0"
1.39    unfolding one_poly_def
1.40    by (rule degree_pCons_0)
1.41 @@ -973,6 +988,18 @@
1.43  done
1.44
1.45 +lemma degree_mult_right_le:
1.46 +  fixes p q :: "'a::idom poly"
1.47 +  assumes "q \<noteq> 0"
1.48 +  shows "degree p \<le> degree (p * q)"
1.49 +  using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
1.50 +
1.51 +lemma coeff_degree_mult:
1.52 +  fixes p q :: "'a::idom poly"
1.53 +  shows "coeff (p * q) (degree (p * q)) =
1.54 +    coeff q (degree q) * coeff p (degree p)"
1.55 +  by (cases "p = 0 \<or> q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum)
1.56 +
1.57  lemma dvd_imp_degree_le:
1.58    fixes p q :: "'a::idom poly"
1.59    shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
1.60 @@ -1436,6 +1463,48 @@
1.61
1.62  end
1.63
1.64 +lemma is_unit_monom_0:
1.65 +  fixes a :: "'a::field"
1.66 +  assumes "a \<noteq> 0"
1.67 +  shows "is_unit (monom a 0)"
1.68 +proof
1.69 +  from assms show "1 = monom a 0 * monom (1 / a) 0"
1.70 +    by (simp add: mult_monom)
1.71 +qed
1.72 +
1.73 +lemma is_unit_triv:
1.74 +  fixes a :: "'a::field"
1.75 +  assumes "a \<noteq> 0"
1.76 +  shows "is_unit [:a:]"
1.77 +  using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
1.78 +
1.79 +lemma is_unit_iff_degree:
1.80 +  assumes "p \<noteq> 0"
1.81 +  shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
1.82 +proof
1.83 +  assume ?Q
1.84 +  then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
1.85 +  with assms show ?P by (simp add: is_unit_triv)
1.86 +next
1.87 +  assume ?P
1.88 +  then obtain q where "q \<noteq> 0" "p * q = 1" ..
1.89 +  then have "degree (p * q) = degree 1"
1.90 +    by simp
1.91 +  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
1.92 +    by (simp add: degree_mult_eq)
1.93 +  then show ?Q by simp
1.94 +qed
1.95 +
1.96 +lemma is_unit_pCons_iff:
1.97 +  "is_unit (pCons a p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0" (is "?P \<longleftrightarrow> ?Q")
1.98 +  by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
1.99 +
1.100 +lemma is_unit_monom_trival:
1.101 +  fixes p :: "'a::field poly"
1.102 +  assumes "is_unit p"
1.103 +  shows "monom (coeff p (degree p)) 0 = p"
1.104 +  using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
1.105 +
1.106  lemma degree_mod_less:
1.107    "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
1.108    using pdivmod_rel [of x y]
1.109 @@ -1833,4 +1902,3 @@
1.110  no_notation cCons (infixr "##" 65)
1.111
1.112  end
1.113 -
```