add lemmas degree_{add,diff}_less
authorhuffman
Mon Jan 12 08:15:07 2009 -0800 (2009-01-12)
changeset 29453de4f26f59135
parent 29452 b81ae415873d
child 29454 b0f586f38dd7
add lemmas degree_{add,diff}_less
src/HOL/Polynomial.thy
     1.1 --- a/src/HOL/Polynomial.thy	Sun Jan 11 21:50:05 2009 +0100
     1.2 +++ b/src/HOL/Polynomial.thy	Mon Jan 12 08:15:07 2009 -0800
     1.3 @@ -319,6 +319,10 @@
     1.4  lemma degree_add_le: "degree (p + q) \<le> max (degree p) (degree q)"
     1.5    by (rule degree_le, auto simp add: coeff_eq_0)
     1.6  
     1.7 +lemma degree_add_less:
     1.8 +  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n"
     1.9 +  by (auto intro: le_less_trans degree_add_le)
    1.10 +
    1.11  lemma degree_add_eq_right:
    1.12    "degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
    1.13    apply (cases "q = 0", simp)
    1.14 @@ -341,6 +345,10 @@
    1.15    using degree_add_le [where p=p and q="-q"]
    1.16    by (simp add: diff_minus)
    1.17  
    1.18 +lemma degree_diff_less:
    1.19 +  "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
    1.20 +  by (auto intro: le_less_trans degree_diff_le)
    1.21 +
    1.22  lemma add_monom: "monom a n + monom b n = monom (a + b) n"
    1.23    by (rule poly_ext) simp
    1.24  
    1.25 @@ -762,7 +770,7 @@
    1.26    from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
    1.27      by (simp add: ring_simps)
    1.28    from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
    1.29 -    by (auto intro: le_less_trans [OF degree_diff_le])
    1.30 +    by (auto intro: degree_diff_less)
    1.31  
    1.32    show "q1 = q2 \<and> r1 = r2"
    1.33    proof (rule ccontr)