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.8 -proof
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.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.37  begin
1.38
1.39 @@ -578,22 +597,9 @@
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.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.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
```