src/HOL/Word/Word.thy
changeset 66808 1907167b6038
parent 66453 cc19f7ca2ed6
child 66912 a99a7cbf0fb5
     1.1 --- a/src/HOL/Word/Word.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -2024,7 +2024,7 @@
     1.4  
     1.5  lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
     1.6  
     1.7 -lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
     1.8 +lemmas thd = times_div_less_eq_dividend
     1.9  
    1.10  lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
    1.11  
    1.12 @@ -3724,7 +3724,7 @@
    1.13  lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
    1.14  
    1.15  (* alternative proof of word_rcat_rsplit *)
    1.16 -lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
    1.17 +lemmas tdle = times_div_less_eq_dividend
    1.18  lemmas dtle = xtr4 [OF tdle mult.commute]
    1.19  
    1.20  lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
    1.21 @@ -3734,7 +3734,7 @@
    1.22      apply (simp_all add: word_size
    1.23        refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
    1.24     apply safe
    1.25 -   apply (erule xtr7, rule len_gt_0 [THEN dtle])+
    1.26 +   apply (erule xtr7, rule dtle)+
    1.27    done
    1.28  
    1.29  lemma size_word_rsplit_rcat_size: