src/HOL/Library/RBT_Impl.thy
changeset 64246 15d1ee6e847b
parent 64243 aee949f6642d
child 66808 1907167b6038
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:05 2016 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sun Oct 16 09:31:06 2016 +0200
     1.3 @@ -1240,7 +1240,7 @@
     1.4        case True
     1.5        hence "length (snd (rbtreeify_f n kvs)) = 
     1.6          length (snd (rbtreeify_f (2 * (n div 2)) kvs))"
     1.7 -        by(metis minus_nat.diff_0 mult_div_cancel)
     1.8 +        by(metis minus_nat.diff_0 minus_mod_eq_mult_div [symmetric])
     1.9        also from "1.prems" False obtain k v kvs' 
    1.10          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
    1.11        also have "0 < n div 2" using False by(simp) 
    1.12 @@ -1260,7 +1260,7 @@
    1.13        have "length (snd (rbtreeify_g (n div 2) kvs'')) = 
    1.14          Suc (length kvs'') - n div 2" by(rule IH)
    1.15        finally show ?thesis using len[unfolded kvs''] "1.prems" True
    1.16 -        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
    1.17 +        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] minus_mod_eq_mult_div [symmetric])
    1.18      next
    1.19        case False
    1.20        hence "length (snd (rbtreeify_f n kvs)) = 
    1.21 @@ -1303,7 +1303,7 @@
    1.22        case True
    1.23        hence "length (snd (rbtreeify_g n kvs)) =
    1.24          length (snd (rbtreeify_g (2 * (n div 2)) kvs))"
    1.25 -        by(metis minus_nat.diff_0 mult_div_cancel)
    1.26 +        by(metis minus_nat.diff_0 minus_mod_eq_mult_div [symmetric])
    1.27        also from "2.prems" True obtain k v kvs' 
    1.28          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
    1.29        also have "0 < n div 2" using \<open>1 < n\<close> by(simp) 
    1.30 @@ -1324,7 +1324,7 @@
    1.31        have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
    1.32          by(rule IH)
    1.33        finally show ?thesis using len[unfolded kvs''] "2.prems" True
    1.34 -        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] mult_div_cancel)
    1.35 +        by(simp add: Suc_diff_le[symmetric] mult_2[symmetric] minus_mod_eq_mult_div [symmetric])
    1.36      next
    1.37        case False
    1.38        hence "length (snd (rbtreeify_g n kvs)) = 
    1.39 @@ -1431,7 +1431,7 @@
    1.40          moreover note fodd[unfolded fodd_def]
    1.41          ultimately have "P (Suc (2 * (n div 2))) kvs" by -
    1.42          thus ?thesis using False 
    1.43 -          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
    1.44 +          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend minus_mod_eq_mult_div [symmetric])
    1.45        qed
    1.46      qed
    1.47    next
    1.48 @@ -1478,7 +1478,7 @@
    1.49          moreover note godd[unfolded godd_def]
    1.50          ultimately have "Q (Suc (2 * (n div 2))) kvs" by -
    1.51          thus ?thesis using False 
    1.52 -          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend mult_div_cancel)
    1.53 +          by simp (metis One_nat_def Suc_eq_plus1_left le_add_diff_inverse mod_less_eq_dividend minus_mod_eq_mult_div [symmetric])
    1.54        qed
    1.55      qed
    1.56    qed