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
```