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.42  apply (simp add: coeff_mult_degree_sum)
    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 -