src/HOL/Word/Word_Miscellaneous.thy
changeset 66808 1907167b6038
parent 66801 f3fda9777f9a
child 66886 960509bfd47e
     1.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -304,8 +304,8 @@
     1.4  lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
     1.5  
     1.6  lemmas dme = div_mult_mod_eq
     1.7 -lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
     1.8 -lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
     1.9 +lemmas dtle = div_times_less_eq_dividend
    1.10 +lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend]
    1.11  
    1.12  lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
    1.13    for a b c :: nat
    1.14 @@ -316,15 +316,13 @@
    1.15  
    1.16  lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
    1.17  
    1.18 -lemma div_mult_le: "a div b * b \<le> a"
    1.19 -  for a b :: nat
    1.20 -  by (fact dtle)
    1.21 +lemmas div_mult_le = div_times_less_eq_dividend 
    1.22  
    1.23 -lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
    1.24 +lemmas sdl = div_nat_eqI
    1.25  
    1.26  lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
    1.27    for f l :: nat
    1.28 -  by (rule sdl, assumption) (simp (no_asm))
    1.29 +  by (rule div_nat_eqI) (simp_all)
    1.30  
    1.31  lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
    1.32    for f l :: nat