tuned name of bit truncating operations
authorhaftmann
Sat Oct 08 14:09:55 2016 +0200 (2016-10-08)
changeset 6411445e065eea984
parent 64113 86efd3d4dc98
child 64115 68619fa37ca7
tuned name of bit truncating operations
src/HOL/ex/Word_Type.thy
     1.1 --- a/src/HOL/ex/Word_Type.thy	Sat Oct 08 14:09:53 2016 +0200
     1.2 +++ b/src/HOL/ex/Word_Type.thy	Sat Oct 08 14:09:55 2016 +0200
     1.3 @@ -13,23 +13,21 @@
     1.4  
     1.5  class semiring_bits = semiring_div_parity +
     1.6    assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
     1.7 -
     1.8 -context semiring_bits
     1.9  begin
    1.10  
    1.11 -definition bits :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.12 -  where bits_eq_mod: "bits n a = a mod of_nat (2 ^ n)"
    1.13 +definition bitrunc :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    1.14 +  where bitrunc_eq_mod: "bitrunc n a = a mod of_nat (2 ^ n)"
    1.15  
    1.16 -lemma bits_bits [simp]:
    1.17 -  "bits n (bits n a) = bits n a"
    1.18 -  by (simp add: bits_eq_mod)
    1.19 +lemma bitrunc_bitrunc [simp]:
    1.20 +  "bitrunc n (bitrunc n a) = bitrunc n a"
    1.21 +  by (simp add: bitrunc_eq_mod)
    1.22    
    1.23 -lemma bits_0 [simp]:
    1.24 -  "bits 0 a = 0"
    1.25 -  by (simp add: bits_eq_mod)
    1.26 +lemma bitrunc_0 [simp]:
    1.27 +  "bitrunc 0 a = 0"
    1.28 +  by (simp add: bitrunc_eq_mod)
    1.29  
    1.30 -lemma bits_Suc [simp]:
    1.31 -  "bits (Suc n) a = bits n (a div 2) * 2 + a mod 2"
    1.32 +lemma bitrunc_Suc [simp]:
    1.33 +  "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + a mod 2"
    1.34  proof -
    1.35    define b and c
    1.36      where "b = a div 2" and "c = a mod 2"
    1.37 @@ -37,32 +35,32 @@
    1.38      and "c = 0 \<or> c = 1"
    1.39      by (simp_all add: mod_div_equality parity)
    1.40    from \<open>c = 0 \<or> c = 1\<close>
    1.41 -  have "bits (Suc n) (b * 2 + c) = bits n b * 2 + c"
    1.42 +  have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
    1.43    proof
    1.44      assume "c = 0"
    1.45      moreover have "(2 * b) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n)"
    1.46        by (simp add: mod_mult_mult1)
    1.47      ultimately show ?thesis
    1.48 -      by (simp add: bits_eq_mod ac_simps)
    1.49 +      by (simp add: bitrunc_eq_mod ac_simps)
    1.50    next
    1.51      assume "c = 1"
    1.52      with semiring_bits [of b "2 ^ n"] show ?thesis
    1.53 -      by (simp add: bits_eq_mod ac_simps)
    1.54 +      by (simp add: bitrunc_eq_mod ac_simps)
    1.55    qed
    1.56    with a show ?thesis
    1.57      by (simp add: b_def c_def)
    1.58  qed
    1.59  
    1.60 -lemma bits_of_0 [simp]:
    1.61 -  "bits n 0 = 0"
    1.62 -  by (simp add: bits_eq_mod)
    1.63 +lemma bitrunc_of_0 [simp]:
    1.64 +  "bitrunc n 0 = 0"
    1.65 +  by (simp add: bitrunc_eq_mod)
    1.66  
    1.67 -lemma bits_plus:
    1.68 -  "bits n (bits n a + bits n b) = bits n (a + b)"
    1.69 -  by (simp add: bits_eq_mod mod_add_eq [symmetric])
    1.70 +lemma bitrunc_plus:
    1.71 +  "bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
    1.72 +  by (simp add: bitrunc_eq_mod mod_add_eq [symmetric])
    1.73  
    1.74 -lemma bits_of_1_eq_0_iff [simp]:
    1.75 -  "bits n 1 = 0 \<longleftrightarrow> n = 0"
    1.76 +lemma bitrunc_of_1_eq_0_iff [simp]:
    1.77 +  "bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
    1.78    by (induct n) simp_all
    1.79  
    1.80  end
    1.81 @@ -73,32 +71,32 @@
    1.82  instance int :: semiring_bits
    1.83    by standard (simp add: pos_zmod_mult_2)
    1.84  
    1.85 -lemma bits_uminus:
    1.86 +lemma bitrunc_uminus:
    1.87    fixes k :: int
    1.88 -  shows "bits n (- (bits n k)) = bits n (- k)"
    1.89 -  by (simp add: bits_eq_mod mod_minus_eq [symmetric])
    1.90 +  shows "bitrunc n (- (bitrunc n k)) = bitrunc n (- k)"
    1.91 +  by (simp add: bitrunc_eq_mod mod_minus_eq [symmetric])
    1.92  
    1.93 -lemma bits_minus:
    1.94 +lemma bitrunc_minus:
    1.95    fixes k l :: int
    1.96 -  shows "bits n (bits n k - bits n l) = bits n (k - l)"
    1.97 -  by (simp add: bits_eq_mod mod_diff_eq [symmetric])
    1.98 +  shows "bitrunc n (bitrunc n k - bitrunc n l) = bitrunc n (k - l)"
    1.99 +  by (simp add: bitrunc_eq_mod mod_diff_eq [symmetric])
   1.100  
   1.101 -lemma bits_nonnegative [simp]:
   1.102 +lemma bitrunc_nonnegative [simp]:
   1.103    fixes k :: int
   1.104 -  shows "bits n k \<ge> 0"
   1.105 -  by (simp add: bits_eq_mod)
   1.106 +  shows "bitrunc n k \<ge> 0"
   1.107 +  by (simp add: bitrunc_eq_mod)
   1.108  
   1.109 -definition signed_bits :: "nat \<Rightarrow> int \<Rightarrow> int"
   1.110 -  where signed_bits_eq_bits:
   1.111 -    "signed_bits n k = bits (Suc n) (k + 2 ^ n) - 2 ^ n"
   1.112 +definition signed_bitrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
   1.113 +  where signed_bitrunc_eq_bitrunc:
   1.114 +    "signed_bitrunc n k = bitrunc (Suc n) (k + 2 ^ n) - 2 ^ n"
   1.115  
   1.116 -lemma signed_bits_eq_bits':
   1.117 +lemma signed_bitrunc_eq_bitrunc':
   1.118    assumes "n > 0"
   1.119 -  shows "signed_bits (n - Suc 0) k = bits n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)"
   1.120 -  using assms by (simp add: signed_bits_eq_bits)
   1.121 +  shows "signed_bitrunc (n - Suc 0) k = bitrunc n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)"
   1.122 +  using assms by (simp add: signed_bitrunc_eq_bitrunc)
   1.123    
   1.124 -lemma signed_bits_0 [simp]:
   1.125 -  "signed_bits 0 k = - (k mod 2)"
   1.126 +lemma signed_bitrunc_0 [simp]:
   1.127 +  "signed_bitrunc 0 k = - (k mod 2)"
   1.128  proof (cases "even k")
   1.129    case True
   1.130    then have "odd (k + 1)"
   1.131 @@ -106,54 +104,54 @@
   1.132    then have "(k + 1) mod 2 = 1"
   1.133      by (simp add: even_iff_mod_2_eq_zero)
   1.134    with True show ?thesis
   1.135 -    by (simp add: signed_bits_eq_bits)
   1.136 +    by (simp add: signed_bitrunc_eq_bitrunc)
   1.137  next
   1.138    case False
   1.139    then show ?thesis
   1.140 -    by (simp add: signed_bits_eq_bits odd_iff_mod_2_eq_one)
   1.141 +    by (simp add: signed_bitrunc_eq_bitrunc odd_iff_mod_2_eq_one)
   1.142  qed
   1.143  
   1.144 -lemma signed_bits_Suc [simp]:
   1.145 -  "signed_bits (Suc n) k = signed_bits n (k div 2) * 2 + k mod 2"
   1.146 -  using zero_not_eq_two by (simp add: signed_bits_eq_bits algebra_simps)
   1.147 +lemma signed_bitrunc_Suc [simp]:
   1.148 +  "signed_bitrunc (Suc n) k = signed_bitrunc n (k div 2) * 2 + k mod 2"
   1.149 +  using zero_not_eq_two by (simp add: signed_bitrunc_eq_bitrunc algebra_simps)
   1.150  
   1.151 -lemma signed_bits_of_0 [simp]:
   1.152 -  "signed_bits n 0 = 0"
   1.153 -  by (simp add: signed_bits_eq_bits bits_eq_mod)
   1.154 +lemma signed_bitrunc_of_0 [simp]:
   1.155 +  "signed_bitrunc n 0 = 0"
   1.156 +  by (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod)
   1.157  
   1.158 -lemma signed_bits_of_minus_1 [simp]:
   1.159 -  "signed_bits n (- 1) = - 1"
   1.160 +lemma signed_bitrunc_of_minus_1 [simp]:
   1.161 +  "signed_bitrunc n (- 1) = - 1"
   1.162    by (induct n) simp_all
   1.163  
   1.164 -lemma signed_bits_eq_iff_bits_eq:
   1.165 +lemma signed_bitrunc_eq_iff_bitrunc_eq:
   1.166    assumes "n > 0"
   1.167 -  shows "signed_bits (n - Suc 0) k = signed_bits (n - Suc 0) l \<longleftrightarrow> bits n k = bits n l" (is "?P \<longleftrightarrow> ?Q")
   1.168 +  shows "signed_bitrunc (n - Suc 0) k = signed_bitrunc (n - Suc 0) l \<longleftrightarrow> bitrunc n k = bitrunc n l" (is "?P \<longleftrightarrow> ?Q")
   1.169  proof -
   1.170    from assms obtain m where m: "n = Suc m"
   1.171      by (cases n) auto
   1.172    show ?thesis
   1.173    proof 
   1.174      assume ?Q
   1.175 -    have "bits (Suc m) (k + 2 ^ m) =
   1.176 -      bits (Suc m) (bits (Suc m) k + bits (Suc m) (2 ^ m))"
   1.177 -      by (simp only: bits_plus)
   1.178 +    have "bitrunc (Suc m) (k + 2 ^ m) =
   1.179 +      bitrunc (Suc m) (bitrunc (Suc m) k + bitrunc (Suc m) (2 ^ m))"
   1.180 +      by (simp only: bitrunc_plus)
   1.181      also have "\<dots> =
   1.182 -      bits (Suc m) (bits (Suc m) l + bits (Suc m) (2 ^ m))"
   1.183 +      bitrunc (Suc m) (bitrunc (Suc m) l + bitrunc (Suc m) (2 ^ m))"
   1.184        by (simp only: \<open>?Q\<close> m [symmetric])
   1.185 -    also have "\<dots> = bits (Suc m) (l + 2 ^ m)"
   1.186 -      by (simp only: bits_plus)
   1.187 +    also have "\<dots> = bitrunc (Suc m) (l + 2 ^ m)"
   1.188 +      by (simp only: bitrunc_plus)
   1.189      finally show ?P
   1.190 -      by (simp only: signed_bits_eq_bits m) simp
   1.191 +      by (simp only: signed_bitrunc_eq_bitrunc m) simp
   1.192    next
   1.193      assume ?P
   1.194      with assms have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
   1.195 -      by (simp add: signed_bits_eq_bits' bits_eq_mod)
   1.196 +      by (simp add: signed_bitrunc_eq_bitrunc' bitrunc_eq_mod)
   1.197      then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i
   1.198        by (metis mod_add_eq)
   1.199      then have "k mod 2 ^ n = l mod 2 ^ n"
   1.200        by (metis add_diff_cancel_right' uminus_add_conv_diff)
   1.201      then show ?Q
   1.202 -      by (simp add: bits_eq_mod)
   1.203 +      by (simp add: bitrunc_eq_mod)
   1.204    qed
   1.205  qed 
   1.206  
   1.207 @@ -162,7 +160,7 @@
   1.208  
   1.209  subsubsection \<open>Basic properties\<close>
   1.210  
   1.211 -quotient_type (overloaded) 'a word = int / "\<lambda>k l. bits LENGTH('a) k = bits LENGTH('a::len0) l"
   1.212 +quotient_type (overloaded) 'a word = int / "\<lambda>k l. bitrunc LENGTH('a) k = bitrunc LENGTH('a::len0) l"
   1.213    by (auto intro!: equivpI reflpI sympI transpI)
   1.214  
   1.215  instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}"
   1.216 @@ -178,19 +176,19 @@
   1.217  
   1.218  lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   1.219    is plus
   1.220 -  by (subst bits_plus [symmetric]) (simp add: bits_plus)
   1.221 +  by (subst bitrunc_plus [symmetric]) (simp add: bitrunc_plus)
   1.222  
   1.223  lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
   1.224    is uminus
   1.225 -  by (subst bits_uminus [symmetric]) (simp add: bits_uminus)
   1.226 +  by (subst bitrunc_uminus [symmetric]) (simp add: bitrunc_uminus)
   1.227  
   1.228  lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   1.229    is minus
   1.230 -  by (subst bits_minus [symmetric]) (simp add: bits_minus)
   1.231 +  by (subst bitrunc_minus [symmetric]) (simp add: bitrunc_minus)
   1.232  
   1.233  lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   1.234    is times
   1.235 -  by (auto simp add: bits_eq_mod intro: mod_mult_cong)
   1.236 +  by (auto simp add: bitrunc_eq_mod intro: mod_mult_cong)
   1.237  
   1.238  instance
   1.239    by standard (transfer; simp add: algebra_simps)+
   1.240 @@ -223,7 +221,7 @@
   1.241  begin
   1.242  
   1.243  lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a"
   1.244 -  is "of_nat \<circ> nat \<circ> bits LENGTH('b)"
   1.245 +  is "of_nat \<circ> nat \<circ> bitrunc LENGTH('b)"
   1.246    by simp
   1.247  
   1.248  lemma unsigned_0 [simp]:
   1.249 @@ -245,8 +243,8 @@
   1.250  begin
   1.251  
   1.252  lift_definition signed :: "'b::len word \<Rightarrow> 'a"
   1.253 -  is "of_int \<circ> signed_bits (LENGTH('b) - 1)"
   1.254 -  by (simp add: signed_bits_eq_iff_bits_eq [symmetric])
   1.255 +  is "of_int \<circ> signed_bitrunc (LENGTH('b) - 1)"
   1.256 +  by (simp add: signed_bitrunc_eq_iff_bitrunc_eq [symmetric])
   1.257  
   1.258  lemma signed_0 [simp]:
   1.259    "signed 0 = 0"
   1.260 @@ -255,8 +253,8 @@
   1.261  end
   1.262  
   1.263  lemma unsigned_of_nat [simp]:
   1.264 -  "unsigned (of_nat n :: 'a word) = bits LENGTH('a::len) n"
   1.265 -  by transfer (simp add: nat_eq_iff bits_eq_mod zmod_int)
   1.266 +  "unsigned (of_nat n :: 'a word) = bitrunc LENGTH('a::len) n"
   1.267 +  by transfer (simp add: nat_eq_iff bitrunc_eq_mod zmod_int)
   1.268  
   1.269  lemma of_nat_unsigned [simp]:
   1.270    "of_nat (unsigned a) = a"
   1.271 @@ -271,17 +269,17 @@
   1.272  
   1.273  lemma word_eq_iff_signed:
   1.274    "a = b \<longleftrightarrow> signed a = signed b"
   1.275 -  by safe (transfer; auto simp add: signed_bits_eq_iff_bits_eq)
   1.276 +  by safe (transfer; auto simp add: signed_bitrunc_eq_iff_bitrunc_eq)
   1.277  
   1.278  end
   1.279  
   1.280  lemma signed_of_int [simp]:
   1.281 -  "signed (of_int k :: 'a word) = signed_bits (LENGTH('a::len) - 1) k"
   1.282 +  "signed (of_int k :: 'a word) = signed_bitrunc (LENGTH('a::len) - 1) k"
   1.283    by transfer simp
   1.284  
   1.285  lemma of_int_signed [simp]:
   1.286    "of_int (signed a) = a"
   1.287 -  by transfer (simp add: signed_bits_eq_bits bits_eq_mod zdiff_zmod_left)
   1.288 +  by transfer (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod zdiff_zmod_left)
   1.289  
   1.290  
   1.291  subsubsection \<open>Properties\<close>
   1.292 @@ -293,11 +291,11 @@
   1.293  begin
   1.294  
   1.295  lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   1.296 -  is "\<lambda>a b. bits LENGTH('a) a div bits LENGTH('a) b"
   1.297 +  is "\<lambda>a b. bitrunc LENGTH('a) a div bitrunc LENGTH('a) b"
   1.298    by simp
   1.299  
   1.300  lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   1.301 -  is "\<lambda>a b. bits LENGTH('a) a mod bits LENGTH('a) b"
   1.302 +  is "\<lambda>a b. bitrunc LENGTH('a) a mod bitrunc LENGTH('a) b"
   1.303    by simp
   1.304  
   1.305  instance ..
   1.306 @@ -311,11 +309,11 @@
   1.307  begin
   1.308  
   1.309  lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   1.310 -  is "\<lambda>a b. bits LENGTH('a) a \<le> bits LENGTH('a) b"
   1.311 +  is "\<lambda>a b. bitrunc LENGTH('a) a \<le> bitrunc LENGTH('a) b"
   1.312    by simp
   1.313  
   1.314  lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   1.315 -  is "\<lambda>a b. bits LENGTH('a) a < bits LENGTH('a) b"
   1.316 +  is "\<lambda>a b. bitrunc LENGTH('a) a < bitrunc LENGTH('a) b"
   1.317    by simp
   1.318  
   1.319  instance
   1.320 @@ -332,7 +330,7 @@
   1.321  
   1.322  lemma word_less_iff_unsigned:
   1.323    "a < b \<longleftrightarrow> unsigned a < unsigned b"
   1.324 -  by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF bits_nonnegative])
   1.325 +  by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF bitrunc_nonnegative])
   1.326  
   1.327  end
   1.328