src/HOL/Library/RBT_Impl.thy
changeset 59554 4044f53326c9
parent 58881 b9556a055632
child 59575 55f5e1cbf2a7
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Feb 18 22:46:47 2015 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Feb 18 22:46:47 2015 +0100
     1.3 @@ -1263,8 +1263,7 @@
     1.4        case False
     1.5        hence "length (snd (rbtreeify_f n kvs)) = 
     1.6          length (snd (rbtreeify_f (Suc (2 * (n div 2))) kvs))"
     1.7 -        by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7)
     1.8 -             mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
     1.9 +        by (simp add: mod_eq_0_iff_dvd)
    1.10        also from "1.prems" `\<not> n \<le> 1` obtain k v kvs' 
    1.11          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
    1.12        also have "0 < n div 2" using `\<not> n \<le> 1` by(simp) 
    1.13 @@ -1328,8 +1327,7 @@
    1.14        case False
    1.15        hence "length (snd (rbtreeify_g n kvs)) = 
    1.16          length (snd (rbtreeify_g (Suc (2 * (n div 2))) kvs))"
    1.17 -        by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7) 
    1.18 -            mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
    1.19 +        by (simp add: mod_eq_0_iff_dvd)
    1.20        also from "2.prems" `1 < n` obtain k v kvs'
    1.21          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
    1.22        also have "0 < n div 2" using `1 < n` by(simp)