proof of concept for algebraically founded word types
authorhaftmann
Mon Oct 03 14:37:06 2016 +0200 (2016-10-03)
changeset 64015c9f3a94cb825
parent 64014 ca1239a3277b
child 64016 5c2c559f01eb
proof of concept for algebraically founded word types
src/HOL/ROOT
src/HOL/ex/Word_Type.thy
     1.1 --- a/src/HOL/ROOT	Mon Oct 03 14:34:32 2016 +0200
     1.2 +++ b/src/HOL/ROOT	Mon Oct 03 14:37:06 2016 +0200
     1.3 @@ -627,6 +627,7 @@
     1.4      Code_Timing
     1.5      Perm_Fragments
     1.6      Argo_Examples
     1.7 +    Word_Type
     1.8    theories [skip_proofs = false]
     1.9      Meson_Test
    1.10    document_files "root.bib" "root.tex"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Word_Type.thy	Mon Oct 03 14:37:06 2016 +0200
     2.3 @@ -0,0 +1,354 @@
     2.4 +(*  Author:  Florian Haftmann, TUM
     2.5 +*)
     2.6 +
     2.7 +section \<open>Proof of concept for algebraically founded bit word types\<close>
     2.8 +
     2.9 +theory Word_Type
    2.10 +  imports
    2.11 +    Main
    2.12 +    "~~/src/HOL/Library/Type_Length"
    2.13 +begin
    2.14 +
    2.15 +subsection \<open>Compact syntax for types with a length\<close>
    2.16 +
    2.17 +syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))")
    2.18 +
    2.19 +translations "LENGTH('a)" \<rightharpoonup>
    2.20 +  "CONST len_of (CONST Pure.type :: 'a itself)"
    2.21 +
    2.22 +print_translation \<open>
    2.23 +  let
    2.24 +    fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] =
    2.25 +      Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T
    2.26 +  in [(@{const_syntax len_of}, len_of_itself_tr')] end
    2.27 +\<close>
    2.28 +
    2.29 +
    2.30 +subsection \<open>Truncating bit representations of numeric types\<close>
    2.31 +
    2.32 +class semiring_bits = semiring_div_parity +
    2.33 +  assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)"
    2.34 +
    2.35 +context semiring_bits
    2.36 +begin
    2.37 +
    2.38 +definition bits :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    2.39 +  where bits_eq_mod: "bits n a = a mod of_nat (2 ^ n)"
    2.40 +
    2.41 +lemma bits_bits [simp]:
    2.42 +  "bits n (bits n a) = bits n a"
    2.43 +  by (simp add: bits_eq_mod)
    2.44 +  
    2.45 +lemma bits_0 [simp]:
    2.46 +  "bits 0 a = 0"
    2.47 +  by (simp add: bits_eq_mod)
    2.48 +
    2.49 +lemma bits_Suc [simp]:
    2.50 +  "bits (Suc n) a = bits n (a div 2) * 2 + a mod 2"
    2.51 +proof -
    2.52 +  define b and c
    2.53 +    where "b = a div 2" and "c = a mod 2"
    2.54 +  then have a: "a = b * 2 + c" 
    2.55 +    and "c = 0 \<or> c = 1"
    2.56 +    by (simp_all add: mod_div_equality parity)
    2.57 +  from \<open>c = 0 \<or> c = 1\<close>
    2.58 +  have "bits (Suc n) (b * 2 + c) = bits n b * 2 + c"
    2.59 +  proof
    2.60 +    assume "c = 0"
    2.61 +    moreover have "(2 * b) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n)"
    2.62 +      by (simp add: mod_mult_mult1)
    2.63 +    ultimately show ?thesis
    2.64 +      by (simp add: bits_eq_mod ac_simps)
    2.65 +  next
    2.66 +    assume "c = 1"
    2.67 +    with semiring_bits [of b "2 ^ n"] show ?thesis
    2.68 +      by (simp add: bits_eq_mod ac_simps)
    2.69 +  qed
    2.70 +  with a show ?thesis
    2.71 +    by (simp add: b_def c_def)
    2.72 +qed
    2.73 +
    2.74 +lemma bits_of_0 [simp]:
    2.75 +  "bits n 0 = 0"
    2.76 +  by (simp add: bits_eq_mod)
    2.77 +
    2.78 +lemma bits_plus:
    2.79 +  "bits n (bits n a + bits n b) = bits n (a + b)"
    2.80 +  by (simp add: bits_eq_mod mod_add_eq [symmetric])
    2.81 +
    2.82 +lemma bits_of_1_eq_0_iff [simp]:
    2.83 +  "bits n 1 = 0 \<longleftrightarrow> n = 0"
    2.84 +  by (induct n) simp_all
    2.85 +
    2.86 +end
    2.87 +
    2.88 +instance nat :: semiring_bits
    2.89 +  by standard (simp add: mod_Suc Suc_double_not_eq_double)
    2.90 +
    2.91 +instance int :: semiring_bits
    2.92 +  by standard (simp add: pos_zmod_mult_2)
    2.93 +
    2.94 +lemma bits_uminus:
    2.95 +  fixes k :: int
    2.96 +  shows "bits n (- (bits n k)) = bits n (- k)"
    2.97 +  by (simp add: bits_eq_mod mod_minus_eq [symmetric])
    2.98 +
    2.99 +lemma bits_minus:
   2.100 +  fixes k l :: int
   2.101 +  shows "bits n (bits n k - bits n l) = bits n (k - l)"
   2.102 +  by (simp add: bits_eq_mod mod_diff_eq [symmetric])
   2.103 +
   2.104 +lemma bits_nonnegative [simp]:
   2.105 +  fixes k :: int
   2.106 +  shows "bits n k \<ge> 0"
   2.107 +  by (simp add: bits_eq_mod)
   2.108 +
   2.109 +definition signed_bits :: "nat \<Rightarrow> int \<Rightarrow> int"
   2.110 +  where signed_bits_eq_bits:
   2.111 +    "signed_bits n k = bits (Suc n) (k + 2 ^ n) - 2 ^ n"
   2.112 +
   2.113 +lemma signed_bits_eq_bits':
   2.114 +  assumes "n > 0"
   2.115 +  shows "signed_bits (n - Suc 0) k = bits n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)"
   2.116 +  using assms by (simp add: signed_bits_eq_bits)
   2.117 +  
   2.118 +lemma signed_bits_0 [simp]:
   2.119 +  "signed_bits 0 k = - (k mod 2)"
   2.120 +proof (cases "even k")
   2.121 +  case True
   2.122 +  then have "odd (k + 1)"
   2.123 +    by simp
   2.124 +  then have "(k + 1) mod 2 = 1"
   2.125 +    by (simp add: even_iff_mod_2_eq_zero)
   2.126 +  with True show ?thesis
   2.127 +    by (simp add: signed_bits_eq_bits)
   2.128 +next
   2.129 +  case False
   2.130 +  then show ?thesis
   2.131 +    by (simp add: signed_bits_eq_bits odd_iff_mod_2_eq_one)
   2.132 +qed
   2.133 +
   2.134 +lemma signed_bits_Suc [simp]:
   2.135 +  "signed_bits (Suc n) k = signed_bits n (k div 2) * 2 + k mod 2"
   2.136 +  using zero_not_eq_two by (simp add: signed_bits_eq_bits algebra_simps)
   2.137 +
   2.138 +lemma signed_bits_of_0 [simp]:
   2.139 +  "signed_bits n 0 = 0"
   2.140 +  by (simp add: signed_bits_eq_bits bits_eq_mod)
   2.141 +
   2.142 +lemma signed_bits_of_minus_1 [simp]:
   2.143 +  "signed_bits n (- 1) = - 1"
   2.144 +  by (induct n) simp_all
   2.145 +
   2.146 +lemma signed_bits_eq_iff_bits_eq:
   2.147 +  assumes "n > 0"
   2.148 +  shows "signed_bits (n - Suc 0) k = signed_bits (n - Suc 0) l \<longleftrightarrow> bits n k = bits n l" (is "?P \<longleftrightarrow> ?Q")
   2.149 +proof -
   2.150 +  from assms obtain m where m: "n = Suc m"
   2.151 +    by (cases n) auto
   2.152 +  show ?thesis
   2.153 +  proof 
   2.154 +    assume ?Q
   2.155 +    have "bits (Suc m) (k + 2 ^ m) =
   2.156 +      bits (Suc m) (bits (Suc m) k + bits (Suc m) (2 ^ m))"
   2.157 +      by (simp only: bits_plus)
   2.158 +    also have "\<dots> =
   2.159 +      bits (Suc m) (bits (Suc m) l + bits (Suc m) (2 ^ m))"
   2.160 +      by (simp only: \<open>?Q\<close> m [symmetric])
   2.161 +    also have "\<dots> = bits (Suc m) (l + 2 ^ m)"
   2.162 +      by (simp only: bits_plus)
   2.163 +    finally show ?P
   2.164 +      by (simp only: signed_bits_eq_bits m) simp
   2.165 +  next
   2.166 +    assume ?P
   2.167 +    with assms have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
   2.168 +      by (simp add: signed_bits_eq_bits' bits_eq_mod)
   2.169 +    then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i
   2.170 +      by (metis mod_add_eq)
   2.171 +    then have "k mod 2 ^ n = l mod 2 ^ n"
   2.172 +      by (metis add_diff_cancel_right' uminus_add_conv_diff)
   2.173 +    then show ?Q
   2.174 +      by (simp add: bits_eq_mod)
   2.175 +  qed
   2.176 +qed 
   2.177 +
   2.178 +
   2.179 +subsection \<open>Bit strings as quotient type\<close>
   2.180 +
   2.181 +subsubsection \<open>Basic properties\<close>
   2.182 +
   2.183 +quotient_type (overloaded) 'a word = int / "\<lambda>k l. bits LENGTH('a) k = bits LENGTH('a::len0) l"
   2.184 +  by (auto intro!: equivpI reflpI sympI transpI)
   2.185 +
   2.186 +instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}"
   2.187 +begin
   2.188 +
   2.189 +lift_definition zero_word :: "'a word"
   2.190 +  is 0
   2.191 +  .
   2.192 +
   2.193 +lift_definition one_word :: "'a word"
   2.194 +  is 1
   2.195 +  .
   2.196 +
   2.197 +lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   2.198 +  is plus
   2.199 +  by (subst bits_plus [symmetric]) (simp add: bits_plus)
   2.200 +
   2.201 +lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
   2.202 +  is uminus
   2.203 +  by (subst bits_uminus [symmetric]) (simp add: bits_uminus)
   2.204 +
   2.205 +lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   2.206 +  is minus
   2.207 +  by (subst bits_minus [symmetric]) (simp add: bits_minus)
   2.208 +
   2.209 +lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   2.210 +  is times
   2.211 +  by (auto simp add: bits_eq_mod intro: mod_mult_cong)
   2.212 +
   2.213 +instance
   2.214 +  by standard (transfer; simp add: algebra_simps)+
   2.215 +
   2.216 +end
   2.217 +
   2.218 +instance word :: (len) comm_ring_1
   2.219 +  by standard (transfer; simp)+
   2.220 +
   2.221 +
   2.222 +subsubsection \<open>Conversions\<close>
   2.223 +
   2.224 +lemma [transfer_rule]:
   2.225 +  "rel_fun HOL.eq pcr_word int of_nat"
   2.226 +proof -
   2.227 +  note transfer_rule_of_nat [transfer_rule]
   2.228 +  show ?thesis by transfer_prover
   2.229 +qed
   2.230 +  
   2.231 +lemma [transfer_rule]:
   2.232 +  "rel_fun HOL.eq pcr_word (\<lambda>k. k) of_int"
   2.233 +proof -
   2.234 +  note transfer_rule_of_int [transfer_rule]
   2.235 +  have "rel_fun HOL.eq pcr_word (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> 'a word)"
   2.236 +    by transfer_prover
   2.237 +  then show ?thesis by (simp add: id_def)
   2.238 +qed
   2.239 +
   2.240 +context semiring_1
   2.241 +begin
   2.242 +
   2.243 +lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a"
   2.244 +  is "of_nat \<circ> nat \<circ> bits LENGTH('b)"
   2.245 +  by simp
   2.246 +
   2.247 +lemma unsigned_0 [simp]:
   2.248 +  "unsigned 0 = 0"
   2.249 +  by transfer simp
   2.250 +
   2.251 +end
   2.252 +
   2.253 +context semiring_char_0
   2.254 +begin
   2.255 +
   2.256 +lemma word_eq_iff_unsigned:
   2.257 +  "a = b \<longleftrightarrow> unsigned a = unsigned b"
   2.258 +  by safe (transfer; simp add: eq_nat_nat_iff)
   2.259 +
   2.260 +end
   2.261 +
   2.262 +context ring_1
   2.263 +begin
   2.264 +
   2.265 +lift_definition signed :: "'b::len word \<Rightarrow> 'a"
   2.266 +  is "of_int \<circ> signed_bits (LENGTH('b) - 1)"
   2.267 +  by (simp add: signed_bits_eq_iff_bits_eq [symmetric])
   2.268 +
   2.269 +lemma signed_0 [simp]:
   2.270 +  "signed 0 = 0"
   2.271 +  by transfer simp
   2.272 +
   2.273 +end
   2.274 +
   2.275 +lemma unsigned_of_nat [simp]:
   2.276 +  "unsigned (of_nat n :: 'a word) = bits LENGTH('a::len) n"
   2.277 +  by transfer (simp add: nat_eq_iff bits_eq_mod zmod_int)
   2.278 +
   2.279 +lemma of_nat_unsigned [simp]:
   2.280 +  "of_nat (unsigned a) = a"
   2.281 +  by transfer simp
   2.282 +
   2.283 +lemma of_int_unsigned [simp]:
   2.284 +  "of_int (unsigned a) = a"
   2.285 +  by transfer simp
   2.286 +
   2.287 +context ring_char_0
   2.288 +begin
   2.289 +
   2.290 +lemma word_eq_iff_signed:
   2.291 +  "a = b \<longleftrightarrow> signed a = signed b"
   2.292 +  by safe (transfer; auto simp add: signed_bits_eq_iff_bits_eq)
   2.293 +
   2.294 +end
   2.295 +
   2.296 +lemma signed_of_int [simp]:
   2.297 +  "signed (of_int k :: 'a word) = signed_bits (LENGTH('a::len) - 1) k"
   2.298 +  by transfer simp
   2.299 +
   2.300 +lemma of_int_signed [simp]:
   2.301 +  "of_int (signed a) = a"
   2.302 +  by transfer (simp add: signed_bits_eq_bits bits_eq_mod zdiff_zmod_left)
   2.303 +
   2.304 +
   2.305 +subsubsection \<open>Properties\<close>
   2.306 +
   2.307 +
   2.308 +subsubsection \<open>Division\<close>
   2.309 +
   2.310 +instantiation word :: (len0) modulo
   2.311 +begin
   2.312 +
   2.313 +lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   2.314 +  is "\<lambda>a b. bits LENGTH('a) a div bits LENGTH('a) b"
   2.315 +  by simp
   2.316 +
   2.317 +lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   2.318 +  is "\<lambda>a b. bits LENGTH('a) a mod bits LENGTH('a) b"
   2.319 +  by simp
   2.320 +
   2.321 +instance ..
   2.322 +
   2.323 +end
   2.324 +
   2.325 +
   2.326 +subsubsection \<open>Orderings\<close>
   2.327 +
   2.328 +instantiation word :: (len0) linorder
   2.329 +begin
   2.330 +
   2.331 +lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   2.332 +  is "\<lambda>a b. bits LENGTH('a) a \<le> bits LENGTH('a) b"
   2.333 +  by simp
   2.334 +
   2.335 +lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   2.336 +  is "\<lambda>a b. bits LENGTH('a) a < bits LENGTH('a) b"
   2.337 +  by simp
   2.338 +
   2.339 +instance
   2.340 +  by standard (transfer; auto)+
   2.341 +
   2.342 +end
   2.343 +
   2.344 +context linordered_semidom
   2.345 +begin
   2.346 +
   2.347 +lemma word_less_eq_iff_unsigned:
   2.348 +  "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b"
   2.349 +  by (transfer fixing: less_eq) (simp add: nat_le_eq_zle)
   2.350 +
   2.351 +lemma word_less_iff_unsigned:
   2.352 +  "a < b \<longleftrightarrow> unsigned a < unsigned b"
   2.353 +  by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF bits_nonnegative])
   2.354 +
   2.355 +end
   2.356 +
   2.357 +end