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