src/HOL/ex/Word_Type.thy
author haftmann
Sat Oct 08 14:09:55 2016 +0200 (2016-10-08)
changeset 64114 45e065eea984
parent 64113 86efd3d4dc98
child 64242 93c6f0da5c70
permissions -rw-r--r--
tuned name of bit truncating operations
     1 (*  Author:  Florian Haftmann, TUM
     2 *)
     3 
     4 section \<open>Proof of concept for algebraically founded bit word types\<close>
     5 
     6 theory Word_Type
     7   imports
     8     Main
     9     "~~/src/HOL/Library/Type_Length"
    10 begin
    11 
    12 subsection \<open>Truncating bit representations of numeric types\<close>
    13 
    14 class semiring_bits = semiring_div_parity +
    15   assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
    16 begin
    17 
    18 definition bitrunc :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    19   where bitrunc_eq_mod: "bitrunc n a = a mod of_nat (2 ^ n)"
    20 
    21 lemma bitrunc_bitrunc [simp]:
    22   "bitrunc n (bitrunc n a) = bitrunc n a"
    23   by (simp add: bitrunc_eq_mod)
    24   
    25 lemma bitrunc_0 [simp]:
    26   "bitrunc 0 a = 0"
    27   by (simp add: bitrunc_eq_mod)
    28 
    29 lemma bitrunc_Suc [simp]:
    30   "bitrunc (Suc n) a = bitrunc n (a div 2) * 2 + a mod 2"
    31 proof -
    32   define b and c
    33     where "b = a div 2" and "c = a mod 2"
    34   then have a: "a = b * 2 + c" 
    35     and "c = 0 \<or> c = 1"
    36     by (simp_all add: mod_div_equality parity)
    37   from \<open>c = 0 \<or> c = 1\<close>
    38   have "bitrunc (Suc n) (b * 2 + c) = bitrunc n b * 2 + c"
    39   proof
    40     assume "c = 0"
    41     moreover have "(2 * b) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n)"
    42       by (simp add: mod_mult_mult1)
    43     ultimately show ?thesis
    44       by (simp add: bitrunc_eq_mod ac_simps)
    45   next
    46     assume "c = 1"
    47     with semiring_bits [of b "2 ^ n"] show ?thesis
    48       by (simp add: bitrunc_eq_mod ac_simps)
    49   qed
    50   with a show ?thesis
    51     by (simp add: b_def c_def)
    52 qed
    53 
    54 lemma bitrunc_of_0 [simp]:
    55   "bitrunc n 0 = 0"
    56   by (simp add: bitrunc_eq_mod)
    57 
    58 lemma bitrunc_plus:
    59   "bitrunc n (bitrunc n a + bitrunc n b) = bitrunc n (a + b)"
    60   by (simp add: bitrunc_eq_mod mod_add_eq [symmetric])
    61 
    62 lemma bitrunc_of_1_eq_0_iff [simp]:
    63   "bitrunc n 1 = 0 \<longleftrightarrow> n = 0"
    64   by (induct n) simp_all
    65 
    66 end
    67 
    68 instance nat :: semiring_bits
    69   by standard (simp add: mod_Suc Suc_double_not_eq_double)
    70 
    71 instance int :: semiring_bits
    72   by standard (simp add: pos_zmod_mult_2)
    73 
    74 lemma bitrunc_uminus:
    75   fixes k :: int
    76   shows "bitrunc n (- (bitrunc n k)) = bitrunc n (- k)"
    77   by (simp add: bitrunc_eq_mod mod_minus_eq [symmetric])
    78 
    79 lemma bitrunc_minus:
    80   fixes k l :: int
    81   shows "bitrunc n (bitrunc n k - bitrunc n l) = bitrunc n (k - l)"
    82   by (simp add: bitrunc_eq_mod mod_diff_eq [symmetric])
    83 
    84 lemma bitrunc_nonnegative [simp]:
    85   fixes k :: int
    86   shows "bitrunc n k \<ge> 0"
    87   by (simp add: bitrunc_eq_mod)
    88 
    89 definition signed_bitrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
    90   where signed_bitrunc_eq_bitrunc:
    91     "signed_bitrunc n k = bitrunc (Suc n) (k + 2 ^ n) - 2 ^ n"
    92 
    93 lemma signed_bitrunc_eq_bitrunc':
    94   assumes "n > 0"
    95   shows "signed_bitrunc (n - Suc 0) k = bitrunc n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)"
    96   using assms by (simp add: signed_bitrunc_eq_bitrunc)
    97   
    98 lemma signed_bitrunc_0 [simp]:
    99   "signed_bitrunc 0 k = - (k mod 2)"
   100 proof (cases "even k")
   101   case True
   102   then have "odd (k + 1)"
   103     by simp
   104   then have "(k + 1) mod 2 = 1"
   105     by (simp add: even_iff_mod_2_eq_zero)
   106   with True show ?thesis
   107     by (simp add: signed_bitrunc_eq_bitrunc)
   108 next
   109   case False
   110   then show ?thesis
   111     by (simp add: signed_bitrunc_eq_bitrunc odd_iff_mod_2_eq_one)
   112 qed
   113 
   114 lemma signed_bitrunc_Suc [simp]:
   115   "signed_bitrunc (Suc n) k = signed_bitrunc n (k div 2) * 2 + k mod 2"
   116   using zero_not_eq_two by (simp add: signed_bitrunc_eq_bitrunc algebra_simps)
   117 
   118 lemma signed_bitrunc_of_0 [simp]:
   119   "signed_bitrunc n 0 = 0"
   120   by (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod)
   121 
   122 lemma signed_bitrunc_of_minus_1 [simp]:
   123   "signed_bitrunc n (- 1) = - 1"
   124   by (induct n) simp_all
   125 
   126 lemma signed_bitrunc_eq_iff_bitrunc_eq:
   127   assumes "n > 0"
   128   shows "signed_bitrunc (n - Suc 0) k = signed_bitrunc (n - Suc 0) l \<longleftrightarrow> bitrunc n k = bitrunc n l" (is "?P \<longleftrightarrow> ?Q")
   129 proof -
   130   from assms obtain m where m: "n = Suc m"
   131     by (cases n) auto
   132   show ?thesis
   133   proof 
   134     assume ?Q
   135     have "bitrunc (Suc m) (k + 2 ^ m) =
   136       bitrunc (Suc m) (bitrunc (Suc m) k + bitrunc (Suc m) (2 ^ m))"
   137       by (simp only: bitrunc_plus)
   138     also have "\<dots> =
   139       bitrunc (Suc m) (bitrunc (Suc m) l + bitrunc (Suc m) (2 ^ m))"
   140       by (simp only: \<open>?Q\<close> m [symmetric])
   141     also have "\<dots> = bitrunc (Suc m) (l + 2 ^ m)"
   142       by (simp only: bitrunc_plus)
   143     finally show ?P
   144       by (simp only: signed_bitrunc_eq_bitrunc m) simp
   145   next
   146     assume ?P
   147     with assms have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
   148       by (simp add: signed_bitrunc_eq_bitrunc' bitrunc_eq_mod)
   149     then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i
   150       by (metis mod_add_eq)
   151     then have "k mod 2 ^ n = l mod 2 ^ n"
   152       by (metis add_diff_cancel_right' uminus_add_conv_diff)
   153     then show ?Q
   154       by (simp add: bitrunc_eq_mod)
   155   qed
   156 qed 
   157 
   158 
   159 subsection \<open>Bit strings as quotient type\<close>
   160 
   161 subsubsection \<open>Basic properties\<close>
   162 
   163 quotient_type (overloaded) 'a word = int / "\<lambda>k l. bitrunc LENGTH('a) k = bitrunc LENGTH('a::len0) l"
   164   by (auto intro!: equivpI reflpI sympI transpI)
   165 
   166 instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}"
   167 begin
   168 
   169 lift_definition zero_word :: "'a word"
   170   is 0
   171   .
   172 
   173 lift_definition one_word :: "'a word"
   174   is 1
   175   .
   176 
   177 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   178   is plus
   179   by (subst bitrunc_plus [symmetric]) (simp add: bitrunc_plus)
   180 
   181 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
   182   is uminus
   183   by (subst bitrunc_uminus [symmetric]) (simp add: bitrunc_uminus)
   184 
   185 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   186   is minus
   187   by (subst bitrunc_minus [symmetric]) (simp add: bitrunc_minus)
   188 
   189 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   190   is times
   191   by (auto simp add: bitrunc_eq_mod intro: mod_mult_cong)
   192 
   193 instance
   194   by standard (transfer; simp add: algebra_simps)+
   195 
   196 end
   197 
   198 instance word :: (len) comm_ring_1
   199   by standard (transfer; simp)+
   200 
   201 
   202 subsubsection \<open>Conversions\<close>
   203 
   204 lemma [transfer_rule]:
   205   "rel_fun HOL.eq pcr_word int of_nat"
   206 proof -
   207   note transfer_rule_of_nat [transfer_rule]
   208   show ?thesis by transfer_prover
   209 qed
   210   
   211 lemma [transfer_rule]:
   212   "rel_fun HOL.eq pcr_word (\<lambda>k. k) of_int"
   213 proof -
   214   note transfer_rule_of_int [transfer_rule]
   215   have "rel_fun HOL.eq pcr_word (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> 'a word)"
   216     by transfer_prover
   217   then show ?thesis by (simp add: id_def)
   218 qed
   219 
   220 context semiring_1
   221 begin
   222 
   223 lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a"
   224   is "of_nat \<circ> nat \<circ> bitrunc LENGTH('b)"
   225   by simp
   226 
   227 lemma unsigned_0 [simp]:
   228   "unsigned 0 = 0"
   229   by transfer simp
   230 
   231 end
   232 
   233 context semiring_char_0
   234 begin
   235 
   236 lemma word_eq_iff_unsigned:
   237   "a = b \<longleftrightarrow> unsigned a = unsigned b"
   238   by safe (transfer; simp add: eq_nat_nat_iff)
   239 
   240 end
   241 
   242 context ring_1
   243 begin
   244 
   245 lift_definition signed :: "'b::len word \<Rightarrow> 'a"
   246   is "of_int \<circ> signed_bitrunc (LENGTH('b) - 1)"
   247   by (simp add: signed_bitrunc_eq_iff_bitrunc_eq [symmetric])
   248 
   249 lemma signed_0 [simp]:
   250   "signed 0 = 0"
   251   by transfer simp
   252 
   253 end
   254 
   255 lemma unsigned_of_nat [simp]:
   256   "unsigned (of_nat n :: 'a word) = bitrunc LENGTH('a::len) n"
   257   by transfer (simp add: nat_eq_iff bitrunc_eq_mod zmod_int)
   258 
   259 lemma of_nat_unsigned [simp]:
   260   "of_nat (unsigned a) = a"
   261   by transfer simp
   262 
   263 lemma of_int_unsigned [simp]:
   264   "of_int (unsigned a) = a"
   265   by transfer simp
   266 
   267 context ring_char_0
   268 begin
   269 
   270 lemma word_eq_iff_signed:
   271   "a = b \<longleftrightarrow> signed a = signed b"
   272   by safe (transfer; auto simp add: signed_bitrunc_eq_iff_bitrunc_eq)
   273 
   274 end
   275 
   276 lemma signed_of_int [simp]:
   277   "signed (of_int k :: 'a word) = signed_bitrunc (LENGTH('a::len) - 1) k"
   278   by transfer simp
   279 
   280 lemma of_int_signed [simp]:
   281   "of_int (signed a) = a"
   282   by transfer (simp add: signed_bitrunc_eq_bitrunc bitrunc_eq_mod zdiff_zmod_left)
   283 
   284 
   285 subsubsection \<open>Properties\<close>
   286 
   287 
   288 subsubsection \<open>Division\<close>
   289 
   290 instantiation word :: (len0) modulo
   291 begin
   292 
   293 lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   294   is "\<lambda>a b. bitrunc LENGTH('a) a div bitrunc LENGTH('a) b"
   295   by simp
   296 
   297 lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   298   is "\<lambda>a b. bitrunc LENGTH('a) a mod bitrunc LENGTH('a) b"
   299   by simp
   300 
   301 instance ..
   302 
   303 end
   304 
   305 
   306 subsubsection \<open>Orderings\<close>
   307 
   308 instantiation word :: (len0) linorder
   309 begin
   310 
   311 lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   312   is "\<lambda>a b. bitrunc LENGTH('a) a \<le> bitrunc LENGTH('a) b"
   313   by simp
   314 
   315 lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   316   is "\<lambda>a b. bitrunc LENGTH('a) a < bitrunc LENGTH('a) b"
   317   by simp
   318 
   319 instance
   320   by standard (transfer; auto)+
   321 
   322 end
   323 
   324 context linordered_semidom
   325 begin
   326 
   327 lemma word_less_eq_iff_unsigned:
   328   "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b"
   329   by (transfer fixing: less_eq) (simp add: nat_le_eq_zle)
   330 
   331 lemma word_less_iff_unsigned:
   332   "a < b \<longleftrightarrow> unsigned a < unsigned b"
   333   by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF bitrunc_nonnegative])
   334 
   335 end
   336 
   337 end