prefer convention to place operation name before type name
authorhaftmann
Wed Mar 21 19:39:23 2018 +0100 (14 months ago)
changeset 6790702a14c1cb917
parent 67906 9cc32b18c785
child 67908 537f891d8f14
prefer convention to place operation name before type name
src/HOL/Parity.thy
src/HOL/Set_Interval.thy
src/HOL/ex/Word_Type.thy
     1.1 --- a/src/HOL/Parity.thy	Tue Mar 20 09:27:40 2018 +0000
     1.2 +++ b/src/HOL/Parity.thy	Wed Mar 21 19:39:23 2018 +0100
     1.3 @@ -681,29 +681,29 @@
     1.4  text \<open>The primary purpose of the following operations is
     1.5    to avoid ad-hoc simplification of concrete expressions @{term "2 ^ n"}\<close>
     1.6  
     1.7 -definition bit_push :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
     1.8 -  where bit_push_eq_mult: "bit_push n a = a * 2 ^ n"
     1.9 +definition push_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.10 +  where push_bit_eq_mult: "push_bit n a = a * 2 ^ n"
    1.11   
    1.12 -definition bit_take :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.13 -  where bit_take_eq_mod: "bit_take n a = a mod of_nat (2 ^ n)"
    1.14 +definition take_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.15 +  where take_bit_eq_mod: "take_bit n a = a mod of_nat (2 ^ n)"
    1.16  
    1.17 -definition bit_drop :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.18 -  where bit_drop_eq_div: "bit_drop n a = a div of_nat (2 ^ n)"
    1.19 +definition drop_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.20 +  where drop_bit_eq_div: "drop_bit n a = a div of_nat (2 ^ n)"
    1.21  
    1.22  lemma bit_ident:
    1.23 -  "bit_push n (bit_drop n a) + bit_take n a = a"
    1.24 -  using div_mult_mod_eq by (simp add: bit_push_eq_mult bit_take_eq_mod bit_drop_eq_div)
    1.25 +  "push_bit n (drop_bit n a) + take_bit n a = a"
    1.26 +  using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
    1.27  
    1.28 -lemma bit_take_bit_take [simp]:
    1.29 -  "bit_take n (bit_take n a) = bit_take n a"
    1.30 -  by (simp add: bit_take_eq_mod)
    1.31 +lemma take_bit_take_bit [simp]:
    1.32 +  "take_bit n (take_bit n a) = take_bit n a"
    1.33 +  by (simp add: take_bit_eq_mod)
    1.34    
    1.35 -lemma bit_take_0 [simp]:
    1.36 -  "bit_take 0 a = 0"
    1.37 -  by (simp add: bit_take_eq_mod)
    1.38 +lemma take_bit_0 [simp]:
    1.39 +  "take_bit 0 a = 0"
    1.40 +  by (simp add: take_bit_eq_mod)
    1.41  
    1.42 -lemma bit_take_Suc [simp]:
    1.43 -  "bit_take (Suc n) a = bit_take n (a div 2) * 2 + of_bool (odd a)"
    1.44 +lemma take_bit_Suc [simp]:
    1.45 +  "take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)"
    1.46  proof -
    1.47    have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)"
    1.48      if "odd a"
    1.49 @@ -712,99 +712,99 @@
    1.50    also have "\<dots> = a mod (2 * 2 ^ n)"
    1.51      by (simp only: div_mult_mod_eq)
    1.52    finally show ?thesis
    1.53 -    by (simp add: bit_take_eq_mod algebra_simps mult_mod_right)
    1.54 +    by (simp add: take_bit_eq_mod algebra_simps mult_mod_right)
    1.55  qed
    1.56  
    1.57 -lemma bit_take_of_0 [simp]:
    1.58 -  "bit_take n 0 = 0"
    1.59 -  by (simp add: bit_take_eq_mod)
    1.60 +lemma take_bit_of_0 [simp]:
    1.61 +  "take_bit n 0 = 0"
    1.62 +  by (simp add: take_bit_eq_mod)
    1.63  
    1.64 -lemma bit_take_plus:
    1.65 -  "bit_take n (bit_take n a + bit_take n b) = bit_take n (a + b)"
    1.66 -  by (simp add: bit_take_eq_mod mod_simps)
    1.67 +lemma take_bit_plus:
    1.68 +  "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
    1.69 +  by (simp add: take_bit_eq_mod mod_simps)
    1.70  
    1.71 -lemma bit_take_of_1_eq_0_iff [simp]:
    1.72 -  "bit_take n 1 = 0 \<longleftrightarrow> n = 0"
    1.73 -  by (simp add: bit_take_eq_mod)
    1.74 +lemma take_bit_of_1_eq_0_iff [simp]:
    1.75 +  "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
    1.76 +  by (simp add: take_bit_eq_mod)
    1.77  
    1.78 -lemma bit_push_eq_0_iff [simp]:
    1.79 -  "bit_push n a = 0 \<longleftrightarrow> a = 0"
    1.80 -  by (simp add: bit_push_eq_mult)
    1.81 +lemma push_bit_eq_0_iff [simp]:
    1.82 +  "push_bit n a = 0 \<longleftrightarrow> a = 0"
    1.83 +  by (simp add: push_bit_eq_mult)
    1.84  
    1.85 -lemma bit_drop_0 [simp]:
    1.86 -  "bit_drop 0 = id"
    1.87 -  by (simp add: fun_eq_iff bit_drop_eq_div)
    1.88 +lemma drop_bit_0 [simp]:
    1.89 +  "drop_bit 0 = id"
    1.90 +  by (simp add: fun_eq_iff drop_bit_eq_div)
    1.91  
    1.92 -lemma bit_drop_of_0 [simp]:
    1.93 -  "bit_drop n 0 = 0"
    1.94 -  by (simp add: bit_drop_eq_div)
    1.95 +lemma drop_bit_of_0 [simp]:
    1.96 +  "drop_bit n 0 = 0"
    1.97 +  by (simp add: drop_bit_eq_div)
    1.98  
    1.99 -lemma bit_drop_Suc [simp]:
   1.100 -  "bit_drop (Suc n) a = bit_drop n (a div 2)"
   1.101 +lemma drop_bit_Suc [simp]:
   1.102 +  "drop_bit (Suc n) a = drop_bit n (a div 2)"
   1.103  proof (cases "even a")
   1.104    case True
   1.105    then obtain b where "a = 2 * b" ..
   1.106 -  moreover have "bit_drop (Suc n) (2 * b) = bit_drop n b"
   1.107 -    by (simp add: bit_drop_eq_div)
   1.108 +  moreover have "drop_bit (Suc n) (2 * b) = drop_bit n b"
   1.109 +    by (simp add: drop_bit_eq_div)
   1.110    ultimately show ?thesis
   1.111      by simp
   1.112  next
   1.113    case False
   1.114    then obtain b where "a = 2 * b + 1" ..
   1.115 -  moreover have "bit_drop (Suc n) (2 * b + 1) = bit_drop n b"
   1.116 +  moreover have "drop_bit (Suc n) (2 * b + 1) = drop_bit n b"
   1.117      using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"]
   1.118 -    by (auto simp add: bit_drop_eq_div ac_simps)
   1.119 +    by (auto simp add: drop_bit_eq_div ac_simps)
   1.120    ultimately show ?thesis
   1.121      by simp
   1.122  qed
   1.123  
   1.124 -lemma bit_drop_half:
   1.125 -  "bit_drop n (a div 2) = bit_drop n a div 2"
   1.126 +lemma drop_bit_half:
   1.127 +  "drop_bit n (a div 2) = drop_bit n a div 2"
   1.128    by (induction n arbitrary: a) simp_all
   1.129  
   1.130 -lemma bit_drop_of_bool [simp]:
   1.131 -  "bit_drop n (of_bool d) = of_bool (n = 0 \<and> d)"
   1.132 +lemma drop_bit_of_bool [simp]:
   1.133 +  "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)"
   1.134    by (cases n) simp_all
   1.135  
   1.136 -lemma even_bit_take_eq [simp]:
   1.137 -  "even (bit_take n a) \<longleftrightarrow> n = 0 \<or> even a"
   1.138 -  by (cases n) (simp_all add: bit_take_eq_mod dvd_mod_iff)
   1.139 +lemma even_take_bit_eq [simp]:
   1.140 +  "even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a"
   1.141 +  by (cases n) (simp_all add: take_bit_eq_mod dvd_mod_iff)
   1.142  
   1.143 -lemma bit_push_0_id [simp]:
   1.144 -  "bit_push 0 = id"
   1.145 -  by (simp add: fun_eq_iff bit_push_eq_mult)
   1.146 +lemma push_bit_0_id [simp]:
   1.147 +  "push_bit 0 = id"
   1.148 +  by (simp add: fun_eq_iff push_bit_eq_mult)
   1.149  
   1.150 -lemma bit_push_of_0 [simp]:
   1.151 -  "bit_push n 0 = 0"
   1.152 -  by (simp add: bit_push_eq_mult)
   1.153 +lemma push_bit_of_0 [simp]:
   1.154 +  "push_bit n 0 = 0"
   1.155 +  by (simp add: push_bit_eq_mult)
   1.156  
   1.157 -lemma bit_push_of_1:
   1.158 -  "bit_push n 1 = 2 ^ n"
   1.159 -  by (simp add: bit_push_eq_mult)
   1.160 +lemma push_bit_of_1:
   1.161 +  "push_bit n 1 = 2 ^ n"
   1.162 +  by (simp add: push_bit_eq_mult)
   1.163  
   1.164 -lemma bit_push_Suc [simp]:
   1.165 -  "bit_push (Suc n) a = bit_push n (a * 2)"
   1.166 -  by (simp add: bit_push_eq_mult ac_simps)
   1.167 +lemma push_bit_Suc [simp]:
   1.168 +  "push_bit (Suc n) a = push_bit n (a * 2)"
   1.169 +  by (simp add: push_bit_eq_mult ac_simps)
   1.170  
   1.171 -lemma bit_push_double:
   1.172 -  "bit_push n (a * 2) = bit_push n a * 2"
   1.173 -  by (simp add: bit_push_eq_mult ac_simps)
   1.174 +lemma push_bit_double:
   1.175 +  "push_bit n (a * 2) = push_bit n a * 2"
   1.176 +  by (simp add: push_bit_eq_mult ac_simps)
   1.177  
   1.178 -lemma bit_drop_bit_take [simp]:
   1.179 -  "bit_drop n (bit_take n a) = 0"
   1.180 -  by (simp add: bit_drop_eq_div bit_take_eq_mod)
   1.181 +lemma drop_bit_take_bit [simp]:
   1.182 +  "drop_bit n (take_bit n a) = 0"
   1.183 +  by (simp add: drop_bit_eq_div take_bit_eq_mod)
   1.184  
   1.185 -lemma bit_take_bit_drop_commute:
   1.186 -  "bit_drop m (bit_take n a) = bit_take (n - m) (bit_drop m a)"
   1.187 +lemma take_bit_drop_bit_commute:
   1.188 +  "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
   1.189    for m n :: nat
   1.190  proof (cases "n \<ge> m")
   1.191    case True
   1.192    moreover define q where "q = n - m"
   1.193    ultimately have "n - m = q" and "n = m + q"
   1.194      by simp_all
   1.195 -  moreover have "bit_drop m (bit_take (m + q) a) = bit_take q (bit_drop m a)"
   1.196 +  moreover have "drop_bit m (take_bit (m + q) a) = take_bit q (drop_bit m a)"
   1.197      using mod_mult2_eq' [of a "2 ^ m" "2 ^ q"]
   1.198 -    by (simp add: bit_drop_eq_div bit_take_eq_mod power_add)
   1.199 +    by (simp add: drop_bit_eq_div take_bit_eq_mod power_add)
   1.200    ultimately show ?thesis
   1.201      by simp
   1.202  next
   1.203 @@ -812,9 +812,9 @@
   1.204    moreover define q where "q = m - n"
   1.205    ultimately have "m - n = q" and "m = n + q"
   1.206      by simp_all
   1.207 -  moreover have "bit_drop (n + q) (bit_take n a) = 0"
   1.208 +  moreover have "drop_bit (n + q) (take_bit n a) = 0"
   1.209      using div_mult2_eq' [of "a mod 2 ^ n" "2 ^ n" "2 ^ q"]
   1.210 -    by (simp add: bit_drop_eq_div bit_take_eq_mod power_add div_mult2_eq)
   1.211 +    by (simp add: drop_bit_eq_div take_bit_eq_mod power_add div_mult2_eq)
   1.212    ultimately show ?thesis
   1.213      by simp
   1.214  qed
     2.1 --- a/src/HOL/Set_Interval.thy	Tue Mar 20 09:27:40 2018 +0000
     2.2 +++ b/src/HOL/Set_Interval.thy	Wed Mar 21 19:39:23 2018 +0100
     2.3 @@ -1929,8 +1929,8 @@
     2.4  lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x  \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
     2.5    by (subst sum_subtractf_nat) auto
     2.6  
     2.7 -lemma bit_take_sum_nat:
     2.8 -  "bit_take n m = (\<Sum>k = 0..<n. bit_push k (of_bool (odd (bit_drop k m))))"
     2.9 +lemma take_bit_sum_nat:
    2.10 +  "take_bit n m = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k m))))"
    2.11    for n m :: nat
    2.12  proof (induction n arbitrary: m)
    2.13    case 0
    2.14 @@ -1938,12 +1938,12 @@
    2.15      by simp
    2.16  next
    2.17    case (Suc n)
    2.18 -  have "(\<Sum>k = 0..<Suc n. bit_push k (of_bool (odd (bit_drop k m)))) = 
    2.19 -    of_bool (odd m) + (\<Sum>k = Suc 0..<Suc n. bit_push k (of_bool (odd (bit_drop k m))))"
    2.20 +  have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (odd (drop_bit k m)))) = 
    2.21 +    of_bool (odd m) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (odd (drop_bit k m))))"
    2.22      by (simp add: sum_head_upt_Suc ac_simps)
    2.23 -  also have "(\<Sum>k = Suc 0..<Suc n. bit_push k (of_bool (odd (bit_drop k m))))
    2.24 -    = (\<Sum>k = 0..<n. bit_push k (of_bool (odd (bit_drop k (m div 2))))) * (2::nat)"
    2.25 -    by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right bit_push_double)
    2.26 +  also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (odd (drop_bit k m))))
    2.27 +    = (\<Sum>k = 0..<n. push_bit k (of_bool (odd (drop_bit k (m div 2))))) * (2::nat)"
    2.28 +    by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double)
    2.29    finally show ?case
    2.30      using Suc [of "m div 2"] by simp
    2.31  qed    
     3.1 --- a/src/HOL/ex/Word_Type.thy	Tue Mar 20 09:27:40 2018 +0000
     3.2 +++ b/src/HOL/ex/Word_Type.thy	Wed Mar 21 19:39:23 2018 +0100
     3.3 @@ -9,32 +9,32 @@
     3.4      "HOL-Library.Type_Length"
     3.5  begin
     3.6  
     3.7 -lemma bit_take_uminus:
     3.8 +lemma take_bit_uminus:
     3.9    fixes k :: int
    3.10 -  shows "bit_take n (- (bit_take n k)) = bit_take n (- k)"
    3.11 -  by (simp add: bit_take_eq_mod mod_minus_eq)
    3.12 +  shows "take_bit n (- (take_bit n k)) = take_bit n (- k)"
    3.13 +  by (simp add: take_bit_eq_mod mod_minus_eq)
    3.14  
    3.15 -lemma bit_take_minus:
    3.16 +lemma take_bit_minus:
    3.17    fixes k l :: int
    3.18 -  shows "bit_take n (bit_take n k - bit_take n l) = bit_take n (k - l)"
    3.19 -  by (simp add: bit_take_eq_mod mod_diff_eq)
    3.20 +  shows "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)"
    3.21 +  by (simp add: take_bit_eq_mod mod_diff_eq)
    3.22  
    3.23 -lemma bit_take_nonnegative [simp]:
    3.24 +lemma take_bit_nonnegative [simp]:
    3.25    fixes k :: int
    3.26 -  shows "bit_take n k \<ge> 0"
    3.27 -  by (simp add: bit_take_eq_mod)
    3.28 +  shows "take_bit n k \<ge> 0"
    3.29 +  by (simp add: take_bit_eq_mod)
    3.30  
    3.31 -definition signed_bit_take :: "nat \<Rightarrow> int \<Rightarrow> int"
    3.32 -  where signed_bit_take_eq_bit_take:
    3.33 -    "signed_bit_take n k = bit_take (Suc n) (k + 2 ^ n) - 2 ^ n"
    3.34 +definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
    3.35 +  where signed_take_bit_eq_take_bit:
    3.36 +    "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n"
    3.37  
    3.38 -lemma signed_bit_take_eq_bit_take':
    3.39 +lemma signed_take_bit_eq_take_bit':
    3.40    assumes "n > 0"
    3.41 -  shows "signed_bit_take (n - Suc 0) k = bit_take n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)"
    3.42 -  using assms by (simp add: signed_bit_take_eq_bit_take)
    3.43 +  shows "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)"
    3.44 +  using assms by (simp add: signed_take_bit_eq_take_bit)
    3.45    
    3.46 -lemma signed_bit_take_0 [simp]:
    3.47 -  "signed_bit_take 0 k = - (k mod 2)"
    3.48 +lemma signed_take_bit_0 [simp]:
    3.49 +  "signed_take_bit 0 k = - (k mod 2)"
    3.50  proof (cases "even k")
    3.51    case True
    3.52    then have "odd (k + 1)"
    3.53 @@ -42,54 +42,54 @@
    3.54    then have "(k + 1) mod 2 = 1"
    3.55      by (simp add: even_iff_mod_2_eq_zero)
    3.56    with True show ?thesis
    3.57 -    by (simp add: signed_bit_take_eq_bit_take)
    3.58 +    by (simp add: signed_take_bit_eq_take_bit)
    3.59  next
    3.60    case False
    3.61    then show ?thesis
    3.62 -    by (simp add: signed_bit_take_eq_bit_take odd_iff_mod_2_eq_one)
    3.63 +    by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one)
    3.64  qed
    3.65  
    3.66 -lemma signed_bit_take_Suc [simp]:
    3.67 -  "signed_bit_take (Suc n) k = signed_bit_take n (k div 2) * 2 + k mod 2"
    3.68 -  by (simp add: odd_iff_mod_2_eq_one signed_bit_take_eq_bit_take algebra_simps)
    3.69 +lemma signed_take_bit_Suc [simp]:
    3.70 +  "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2"
    3.71 +  by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps)
    3.72  
    3.73 -lemma signed_bit_take_of_0 [simp]:
    3.74 -  "signed_bit_take n 0 = 0"
    3.75 -  by (simp add: signed_bit_take_eq_bit_take bit_take_eq_mod)
    3.76 +lemma signed_take_bit_of_0 [simp]:
    3.77 +  "signed_take_bit n 0 = 0"
    3.78 +  by (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod)
    3.79  
    3.80 -lemma signed_bit_take_of_minus_1 [simp]:
    3.81 -  "signed_bit_take n (- 1) = - 1"
    3.82 +lemma signed_take_bit_of_minus_1 [simp]:
    3.83 +  "signed_take_bit n (- 1) = - 1"
    3.84    by (induct n) simp_all
    3.85  
    3.86 -lemma signed_bit_take_eq_iff_bit_take_eq:
    3.87 +lemma signed_take_bit_eq_iff_take_bit_eq:
    3.88    assumes "n > 0"
    3.89 -  shows "signed_bit_take (n - Suc 0) k = signed_bit_take (n - Suc 0) l \<longleftrightarrow> bit_take n k = bit_take n l" (is "?P \<longleftrightarrow> ?Q")
    3.90 +  shows "signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \<longleftrightarrow> take_bit n k = take_bit n l" (is "?P \<longleftrightarrow> ?Q")
    3.91  proof -
    3.92    from assms obtain m where m: "n = Suc m"
    3.93      by (cases n) auto
    3.94    show ?thesis
    3.95    proof 
    3.96      assume ?Q
    3.97 -    have "bit_take (Suc m) (k + 2 ^ m) =
    3.98 -      bit_take (Suc m) (bit_take (Suc m) k + bit_take (Suc m) (2 ^ m))"
    3.99 -      by (simp only: bit_take_plus)
   3.100 +    have "take_bit (Suc m) (k + 2 ^ m) =
   3.101 +      take_bit (Suc m) (take_bit (Suc m) k + take_bit (Suc m) (2 ^ m))"
   3.102 +      by (simp only: take_bit_plus)
   3.103      also have "\<dots> =
   3.104 -      bit_take (Suc m) (bit_take (Suc m) l + bit_take (Suc m) (2 ^ m))"
   3.105 +      take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))"
   3.106        by (simp only: \<open>?Q\<close> m [symmetric])
   3.107 -    also have "\<dots> = bit_take (Suc m) (l + 2 ^ m)"
   3.108 -      by (simp only: bit_take_plus)
   3.109 +    also have "\<dots> = take_bit (Suc m) (l + 2 ^ m)"
   3.110 +      by (simp only: take_bit_plus)
   3.111      finally show ?P
   3.112 -      by (simp only: signed_bit_take_eq_bit_take m) simp
   3.113 +      by (simp only: signed_take_bit_eq_take_bit m) simp
   3.114    next
   3.115      assume ?P
   3.116      with assms have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
   3.117 -      by (simp add: signed_bit_take_eq_bit_take' bit_take_eq_mod)
   3.118 +      by (simp add: signed_take_bit_eq_take_bit' take_bit_eq_mod)
   3.119      then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i
   3.120        by (metis mod_add_eq)
   3.121      then have "k mod 2 ^ n = l mod 2 ^ n"
   3.122        by (metis add_diff_cancel_right' uminus_add_conv_diff)
   3.123      then show ?Q
   3.124 -      by (simp add: bit_take_eq_mod)
   3.125 +      by (simp add: take_bit_eq_mod)
   3.126    qed
   3.127  qed 
   3.128  
   3.129 @@ -98,7 +98,7 @@
   3.130  
   3.131  subsubsection \<open>Basic properties\<close>
   3.132  
   3.133 -quotient_type (overloaded) 'a word = int / "\<lambda>k l. bit_take LENGTH('a) k = bit_take LENGTH('a::len0) l"
   3.134 +quotient_type (overloaded) 'a word = int / "\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l"
   3.135    by (auto intro!: equivpI reflpI sympI transpI)
   3.136  
   3.137  instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}"
   3.138 @@ -114,19 +114,19 @@
   3.139  
   3.140  lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   3.141    is plus
   3.142 -  by (subst bit_take_plus [symmetric]) (simp add: bit_take_plus)
   3.143 +  by (subst take_bit_plus [symmetric]) (simp add: take_bit_plus)
   3.144  
   3.145  lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
   3.146    is uminus
   3.147 -  by (subst bit_take_uminus [symmetric]) (simp add: bit_take_uminus)
   3.148 +  by (subst take_bit_uminus [symmetric]) (simp add: take_bit_uminus)
   3.149  
   3.150  lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   3.151    is minus
   3.152 -  by (subst bit_take_minus [symmetric]) (simp add: bit_take_minus)
   3.153 +  by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus)
   3.154  
   3.155  lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   3.156    is times
   3.157 -  by (auto simp add: bit_take_eq_mod intro: mod_mult_cong)
   3.158 +  by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
   3.159  
   3.160  instance
   3.161    by standard (transfer; simp add: algebra_simps)+
   3.162 @@ -159,7 +159,7 @@
   3.163  begin
   3.164  
   3.165  lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a"
   3.166 -  is "of_nat \<circ> nat \<circ> bit_take LENGTH('b)"
   3.167 +  is "of_nat \<circ> nat \<circ> take_bit LENGTH('b)"
   3.168    by simp
   3.169  
   3.170  lemma unsigned_0 [simp]:
   3.171 @@ -181,8 +181,8 @@
   3.172  begin
   3.173  
   3.174  lift_definition signed :: "'b::len word \<Rightarrow> 'a"
   3.175 -  is "of_int \<circ> signed_bit_take (LENGTH('b) - 1)"
   3.176 -  by (simp add: signed_bit_take_eq_iff_bit_take_eq [symmetric])
   3.177 +  is "of_int \<circ> signed_take_bit (LENGTH('b) - 1)"
   3.178 +  by (simp add: signed_take_bit_eq_iff_take_bit_eq [symmetric])
   3.179  
   3.180  lemma signed_0 [simp]:
   3.181    "signed 0 = 0"
   3.182 @@ -191,8 +191,8 @@
   3.183  end
   3.184  
   3.185  lemma unsigned_of_nat [simp]:
   3.186 -  "unsigned (of_nat n :: 'a word) = bit_take LENGTH('a::len) n"
   3.187 -  by transfer (simp add: nat_eq_iff bit_take_eq_mod zmod_int)
   3.188 +  "unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n"
   3.189 +  by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int)
   3.190  
   3.191  lemma of_nat_unsigned [simp]:
   3.192    "of_nat (unsigned a) = a"
   3.193 @@ -207,17 +207,17 @@
   3.194  
   3.195  lemma word_eq_iff_signed:
   3.196    "a = b \<longleftrightarrow> signed a = signed b"
   3.197 -  by safe (transfer; auto simp add: signed_bit_take_eq_iff_bit_take_eq)
   3.198 +  by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq)
   3.199  
   3.200  end
   3.201  
   3.202  lemma signed_of_int [simp]:
   3.203 -  "signed (of_int k :: 'a word) = signed_bit_take (LENGTH('a::len) - 1) k"
   3.204 +  "signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) k"
   3.205    by transfer simp
   3.206  
   3.207  lemma of_int_signed [simp]:
   3.208    "of_int (signed a) = a"
   3.209 -  by transfer (simp add: signed_bit_take_eq_bit_take bit_take_eq_mod mod_simps)
   3.210 +  by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps)
   3.211  
   3.212  
   3.213  subsubsection \<open>Properties\<close>
   3.214 @@ -229,11 +229,11 @@
   3.215  begin
   3.216  
   3.217  lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   3.218 -  is "\<lambda>a b. bit_take LENGTH('a) a div bit_take LENGTH('a) b"
   3.219 +  is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b"
   3.220    by simp
   3.221  
   3.222  lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   3.223 -  is "\<lambda>a b. bit_take LENGTH('a) a mod bit_take LENGTH('a) b"
   3.224 +  is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b"
   3.225    by simp
   3.226  
   3.227  instance ..
   3.228 @@ -247,11 +247,11 @@
   3.229  begin
   3.230  
   3.231  lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   3.232 -  is "\<lambda>a b. bit_take LENGTH('a) a \<le> bit_take LENGTH('a) b"
   3.233 +  is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b"
   3.234    by simp
   3.235  
   3.236  lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   3.237 -  is "\<lambda>a b. bit_take LENGTH('a) a < bit_take LENGTH('a) b"
   3.238 +  is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b"
   3.239    by simp
   3.240  
   3.241  instance
   3.242 @@ -268,7 +268,7 @@
   3.243  
   3.244  lemma word_less_iff_unsigned:
   3.245    "a < b \<longleftrightarrow> unsigned a < unsigned b"
   3.246 -  by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF bit_take_nonnegative])
   3.247 +  by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative])
   3.248  
   3.249  end
   3.250