src/HOL/Library/Polynomial.thy
changeset 59815 cce82e360c2f
parent 59557 ebd8ecacfba6
child 59983 cd2efd7d06bd
     1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Mar 23 19:05:14 2015 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Mar 23 19:05:14 2015 +0100
     1.3 @@ -559,13 +559,32 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
     1.8 -proof
     1.9 +instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
    1.10 +begin
    1.11 +
    1.12 +lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    1.13 +  is "\<lambda>p q n. coeff p n - coeff q n"
    1.14 +proof (rule almost_everywhere_zeroI) 
    1.15 +  fix q p :: "'a poly" and i
    1.16 +  assume "max (degree q) (degree p) < i"
    1.17 +  then show "coeff p i - coeff q i = 0"
    1.18 +    by (simp add: coeff_eq_0)
    1.19 +qed
    1.20 +
    1.21 +lemma coeff_diff [simp]:
    1.22 +  "coeff (p - q) n = coeff p n - coeff q n"
    1.23 +  by (simp add: minus_poly.rep_eq)
    1.24 +
    1.25 +instance proof
    1.26    fix p q r :: "'a poly"
    1.27 -  assume "p + q = p + r" thus "q = r"
    1.28 +  show "p + q - p = q"
    1.29      by (simp add: poly_eq_iff)
    1.30 +  show "p - q - r = p - (q + r)"
    1.31 +    by (simp add: poly_eq_iff diff_diff_eq)
    1.32  qed
    1.33  
    1.34 +end
    1.35 +
    1.36  instantiation poly :: (ab_group_add) ab_group_add
    1.37  begin
    1.38  
    1.39 @@ -578,22 +597,9 @@
    1.40      by (simp add: coeff_eq_0)
    1.41  qed
    1.42  
    1.43 -lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    1.44 -  is "\<lambda>p q n. coeff p n - coeff q n"
    1.45 -proof (rule almost_everywhere_zeroI) 
    1.46 -  fix q p :: "'a poly" and i
    1.47 -  assume "max (degree q) (degree p) < i"
    1.48 -  then show "coeff p i - coeff q i = 0"
    1.49 -    by (simp add: coeff_eq_0)
    1.50 -qed
    1.51 -
    1.52  lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
    1.53    by (simp add: uminus_poly.rep_eq)
    1.54  
    1.55 -lemma coeff_diff [simp]:
    1.56 -  "coeff (p - q) n = coeff p n - coeff q n"
    1.57 -  by (simp add: minus_poly.rep_eq)
    1.58 -
    1.59  instance proof
    1.60    fix p q :: "'a poly"
    1.61    show "- p + p = 0"
    1.62 @@ -641,20 +647,27 @@
    1.63    using degree_add_eq_right [of q p]
    1.64    by (simp add: add.commute)
    1.65  
    1.66 -lemma degree_minus [simp]: "degree (- p) = degree p"
    1.67 +lemma degree_minus [simp]:
    1.68 +  "degree (- p) = degree p"
    1.69    unfolding degree_def by simp
    1.70  
    1.71 -lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
    1.72 +lemma degree_diff_le_max:
    1.73 +  fixes p q :: "'a :: ab_group_add poly"
    1.74 +  shows "degree (p - q) \<le> max (degree p) (degree q)"
    1.75    using degree_add_le [where p=p and q="-q"]
    1.76    by simp
    1.77  
    1.78  lemma degree_diff_le:
    1.79 -  "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p - q) \<le> n"
    1.80 -  using degree_add_le [of p n "- q"] by simp
    1.81 +  fixes p q :: "'a :: ab_group_add poly"
    1.82 +  assumes "degree p \<le> n" and "degree q \<le> n"
    1.83 +  shows "degree (p - q) \<le> n"
    1.84 +  using assms degree_add_le [of p n "- q"] by simp
    1.85  
    1.86  lemma degree_diff_less:
    1.87 -  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
    1.88 -  using degree_add_less [of p n "- q"] by simp
    1.89 +  fixes p q :: "'a :: ab_group_add poly"
    1.90 +  assumes "degree p < n" and "degree q < n"
    1.91 +  shows "degree (p - q) < n"
    1.92 +  using assms degree_add_less [of p n "- q"] by simp
    1.93  
    1.94  lemma add_monom: "monom a n + monom b n = monom (a + b) n"
    1.95    by (rule poly_eqI) simp