src/HOL/Word/Word.thy
changeset 55816 e8dd03241e86
parent 55415 05f5fdb8d093
child 55817 0bc0217387a5
     1.1 --- a/src/HOL/Word/Word.thy	Fri Feb 28 22:56:15 2014 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Sat Mar 01 08:21:46 2014 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  subsection {* Type definition *}
     1.6  
     1.7 -typedef 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
     1.8 +typedef 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
     1.9    morphisms uint Abs_word by auto
    1.10  
    1.11  lemma uint_nonnegative:
    1.12 @@ -35,11 +35,19 @@
    1.13    shows "uint w mod 2 ^ len_of TYPE('a) = uint w"
    1.14    using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
    1.15  
    1.16 +lemma word_uint_eq_iff:
    1.17 +  "a = b \<longleftrightarrow> uint a = uint b"
    1.18 +  by (simp add: uint_inject)
    1.19 +
    1.20 +lemma word_uint_eqI:
    1.21 +  "uint a = uint b \<Longrightarrow> a = b"
    1.22 +  by (simp add: word_uint_eq_iff)
    1.23 +
    1.24  definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
    1.25  where
    1.26 -  -- {* representation of words using unsigned or signed bins, 
    1.27 -        only difference in these is the type class *}
    1.28 -  "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))" 
    1.29 +  -- {* representation of words using unsigned or signed bins,
    1.30 +    only difference in these is the type class *}
    1.31 +  "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))"
    1.32  
    1.33  lemma uint_word_of_int:
    1.34    "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ len_of TYPE('a)"
    1.35 @@ -49,13 +57,183 @@
    1.36    "word_of_int (uint w) = w"
    1.37    by (simp add: word_of_int_def uint_idem uint_inverse)
    1.38  
    1.39 -lemma word_uint_eq_iff:
    1.40 -  "a = b \<longleftrightarrow> uint a = uint b"
    1.41 -  by (simp add: uint_inject)
    1.42 -
    1.43 -lemma word_uint_eqI:
    1.44 -  "uint a = uint b \<Longrightarrow> a = b"
    1.45 -  by (simp add: word_uint_eq_iff)
    1.46 +lemma split_word_all:
    1.47 +  "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
    1.48 +proof
    1.49 +  fix x :: "'a word"
    1.50 +  assume "\<And>x. PROP P (word_of_int x)"
    1.51 +  then have "PROP P (word_of_int (uint x))" .
    1.52 +  find_theorems word_of_int uint
    1.53 +  then show "PROP P x" by (simp add: word_of_int_uint)
    1.54 +qed
    1.55 +
    1.56 +
    1.57 +subsection {* Type conversions and casting *}
    1.58 +
    1.59 +definition sint :: "'a::len word \<Rightarrow> int"
    1.60 +where
    1.61 +  -- {* treats the most-significant-bit as a sign bit *}
    1.62 +  sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
    1.63 +
    1.64 +definition unat :: "'a::len0 word \<Rightarrow> nat"
    1.65 +where
    1.66 +  "unat w = nat (uint w)"
    1.67 +
    1.68 +definition uints :: "nat \<Rightarrow> int set"
    1.69 +where
    1.70 +  -- "the sets of integers representing the words"
    1.71 +  "uints n = range (bintrunc n)"
    1.72 +
    1.73 +definition sints :: "nat \<Rightarrow> int set"
    1.74 +where
    1.75 +  "sints n = range (sbintrunc (n - 1))"
    1.76 +
    1.77 +lemma uints_num:
    1.78 +  "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
    1.79 +  by (simp add: uints_def range_bintrunc)
    1.80 +
    1.81 +lemma sints_num:
    1.82 +  "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
    1.83 +  by (simp add: sints_def range_sbintrunc)
    1.84 +
    1.85 +definition unats :: "nat \<Rightarrow> nat set"
    1.86 +where
    1.87 +  "unats n = {i. i < 2 ^ n}"
    1.88 +
    1.89 +definition norm_sint :: "nat \<Rightarrow> int \<Rightarrow> int"
    1.90 +where
    1.91 +  "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
    1.92 +
    1.93 +definition scast :: "'a::len word \<Rightarrow> 'b::len word"
    1.94 +where
    1.95 +  -- "cast a word to a different length"
    1.96 +  "scast w = word_of_int (sint w)"
    1.97 +
    1.98 +definition ucast :: "'a::len0 word \<Rightarrow> 'b::len0 word"
    1.99 +where
   1.100 +  "ucast w = word_of_int (uint w)"
   1.101 +
   1.102 +instantiation word :: (len0) size
   1.103 +begin
   1.104 +
   1.105 +definition
   1.106 +  word_size: "size (w :: 'a word) = len_of TYPE('a)"
   1.107 +
   1.108 +instance ..
   1.109 +
   1.110 +end
   1.111 +
   1.112 +lemma word_size_gt_0 [iff]:
   1.113 +  "0 < size (w::'a::len word)"
   1.114 +  by (simp add: word_size)
   1.115 +
   1.116 +lemmas lens_gt_0 = word_size_gt_0 len_gt_0
   1.117 +
   1.118 +lemma lens_not_0 [iff]:
   1.119 +  shows "size (w::'a::len word) \<noteq> 0"
   1.120 +  and "len_of TYPE('a::len) \<noteq> 0"
   1.121 +  by auto
   1.122 +
   1.123 +definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"
   1.124 +where
   1.125 +  -- "whether a cast (or other) function is to a longer or shorter length"
   1.126 +  "source_size c = (let arb = undefined ; x = c arb in size arb)"  
   1.127 +
   1.128 +definition target_size :: "('a \<Rightarrow> 'b::len0 word) \<Rightarrow> nat"
   1.129 +where
   1.130 +  "target_size c = size (c undefined)"
   1.131 +
   1.132 +definition is_up :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool"
   1.133 +where
   1.134 +  "is_up c \<longleftrightarrow> source_size c \<le> target_size c"
   1.135 +
   1.136 +definition is_down :: "('a :: len0 word \<Rightarrow> 'b :: len0 word) \<Rightarrow> bool"
   1.137 +where
   1.138 +  "is_down c \<longleftrightarrow> target_size c \<le> source_size c"
   1.139 +
   1.140 +definition of_bl :: "bool list \<Rightarrow> 'a::len0 word"
   1.141 +where
   1.142 +  "of_bl bl = word_of_int (bl_to_bin bl)"
   1.143 +
   1.144 +definition to_bl :: "'a::len0 word \<Rightarrow> bool list"
   1.145 +where
   1.146 +  "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
   1.147 +
   1.148 +definition word_reverse :: "'a::len0 word \<Rightarrow> 'a word"
   1.149 +where
   1.150 +  "word_reverse w = of_bl (rev (to_bl w))"
   1.151 +
   1.152 +definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len0 word \<Rightarrow> 'b" 
   1.153 +where
   1.154 +  "word_int_case f w = f (uint w)"
   1.155 +
   1.156 +translations
   1.157 +  "case x of XCONST of_int y => b" == "CONST word_int_case (%y. b) x"
   1.158 +  "case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
   1.159 +
   1.160 +
   1.161 +subsection {* Type-definition locale instantiations *}
   1.162 +
   1.163 +lemmas uint_0 = uint_nonnegative (* FIXME duplicate *)
   1.164 +lemmas uint_lt = uint_bounded (* FIXME duplicate *)
   1.165 +lemmas uint_mod_same = uint_idem (* FIXME duplicate *)
   1.166 +
   1.167 +lemma td_ext_uint: 
   1.168 +  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0))) 
   1.169 +    (\<lambda>w::int. w mod 2 ^ len_of TYPE('a))"
   1.170 +  apply (unfold td_ext_def')
   1.171 +  apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
   1.172 +  apply (simp add: uint_mod_same uint_0 uint_lt
   1.173 +                   word.uint_inverse word.Abs_word_inverse int_mod_lem)
   1.174 +  done
   1.175 +
   1.176 +interpretation word_uint:
   1.177 +  td_ext "uint::'a::len0 word \<Rightarrow> int" 
   1.178 +         word_of_int 
   1.179 +         "uints (len_of TYPE('a::len0))"
   1.180 +         "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
   1.181 +  by (fact td_ext_uint)
   1.182 +
   1.183 +lemmas td_uint = word_uint.td_thm
   1.184 +lemmas int_word_uint = word_uint.eq_norm
   1.185 +
   1.186 +lemma td_ext_ubin:
   1.187 +  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0)))
   1.188 +    (bintrunc (len_of TYPE('a)))"
   1.189 +  by (unfold no_bintr_alt1) (fact td_ext_uint)
   1.190 +
   1.191 +interpretation word_ubin:
   1.192 +  td_ext "uint::'a::len0 word \<Rightarrow> int" 
   1.193 +         word_of_int 
   1.194 +         "uints (len_of TYPE('a::len0))"
   1.195 +         "bintrunc (len_of TYPE('a::len0))"
   1.196 +  by (fact td_ext_ubin)
   1.197 +
   1.198 +
   1.199 +subsection {* Correspondence relation for theorem transfer *}
   1.200 +
   1.201 +definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
   1.202 +where
   1.203 +  "cr_word = (\<lambda>x y. word_of_int x = y)"
   1.204 +
   1.205 +lemma Quotient_word:
   1.206 +  "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
   1.207 +    word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
   1.208 +  unfolding Quotient_alt_def cr_word_def
   1.209 +  by (simp add: word_ubin.norm_eq_iff)
   1.210 +
   1.211 +lemma reflp_word:
   1.212 +  "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
   1.213 +  by (simp add: reflp_def)
   1.214 +
   1.215 +setup_lifting (no_code) Quotient_word reflp_word
   1.216 +
   1.217 +text {* TODO: The next lemma could be generated automatically. *}
   1.218 +
   1.219 +lemma uint_transfer [transfer_rule]:
   1.220 +  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
   1.221 +    (uint :: 'a::len0 word \<Rightarrow> int)"
   1.222 +  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by (simp add: word_ubin.eq_norm)
   1.223  
   1.224  
   1.225  subsection {* Basic code generation setup *}
   1.226 @@ -66,7 +244,7 @@
   1.227  
   1.228  lemma [code abstype]:
   1.229    "Word (uint w) = w"
   1.230 -  by (simp add: Word_def word_of_int_uint)
   1.231 +  by (simp add: Word_def)
   1.232  
   1.233  declare uint_word_of_int [code abstract]
   1.234  
   1.235 @@ -78,7 +256,7 @@
   1.236    "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
   1.237  
   1.238  instance proof
   1.239 -qed (simp add: equal equal_word_def word_uint_eq_iff)
   1.240 +qed (simp add: equal equal_word_def)
   1.241  
   1.242  end
   1.243  
   1.244 @@ -101,178 +279,7 @@
   1.245  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.246  
   1.247  
   1.248 -subsection {* Type conversions and casting *}
   1.249 -
   1.250 -definition sint :: "'a :: len word => int"
   1.251 -where
   1.252 -  -- {* treats the most-significant-bit as a sign bit *}
   1.253 -  sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
   1.254 -
   1.255 -definition unat :: "'a :: len0 word => nat"
   1.256 -where
   1.257 -  "unat w = nat (uint w)"
   1.258 -
   1.259 -definition uints :: "nat => int set"
   1.260 -where
   1.261 -  -- "the sets of integers representing the words"
   1.262 -  "uints n = range (bintrunc n)"
   1.263 -
   1.264 -definition sints :: "nat => int set"
   1.265 -where
   1.266 -  "sints n = range (sbintrunc (n - 1))"
   1.267 -
   1.268 -definition unats :: "nat => nat set"
   1.269 -where
   1.270 -  "unats n = {i. i < 2 ^ n}"
   1.271 -
   1.272 -definition norm_sint :: "nat => int => int"
   1.273 -where
   1.274 -  "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
   1.275 -
   1.276 -definition scast :: "'a :: len word => 'b :: len word"
   1.277 -where
   1.278 -  -- "cast a word to a different length"
   1.279 -  "scast w = word_of_int (sint w)"
   1.280 -
   1.281 -definition ucast :: "'a :: len0 word => 'b :: len0 word"
   1.282 -where
   1.283 -  "ucast w = word_of_int (uint w)"
   1.284 -
   1.285 -instantiation word :: (len0) size
   1.286 -begin
   1.287 -
   1.288 -definition
   1.289 -  word_size: "size (w :: 'a word) = len_of TYPE('a)"
   1.290 -
   1.291 -instance ..
   1.292 -
   1.293 -end
   1.294 -
   1.295 -definition source_size :: "('a :: len0 word => 'b) => nat"
   1.296 -where
   1.297 -  -- "whether a cast (or other) function is to a longer or shorter length"
   1.298 -  "source_size c = (let arb = undefined ; x = c arb in size arb)"  
   1.299 -
   1.300 -definition target_size :: "('a => 'b :: len0 word) => nat"
   1.301 -where
   1.302 -  "target_size c = size (c undefined)"
   1.303 -
   1.304 -definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
   1.305 -where
   1.306 -  "is_up c \<longleftrightarrow> source_size c <= target_size c"
   1.307 -
   1.308 -definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
   1.309 -where
   1.310 -  "is_down c \<longleftrightarrow> target_size c <= source_size c"
   1.311 -
   1.312 -definition of_bl :: "bool list => 'a :: len0 word"
   1.313 -where
   1.314 -  "of_bl bl = word_of_int (bl_to_bin bl)"
   1.315 -
   1.316 -definition to_bl :: "'a :: len0 word => bool list"
   1.317 -where
   1.318 -  "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
   1.319 -
   1.320 -definition word_reverse :: "'a :: len0 word => 'a word"
   1.321 -where
   1.322 -  "word_reverse w = of_bl (rev (to_bl w))"
   1.323 -
   1.324 -definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" 
   1.325 -where
   1.326 -  "word_int_case f w = f (uint w)"
   1.327 -
   1.328 -translations
   1.329 -  "case x of XCONST of_int y => b" == "CONST word_int_case (%y. b) x"
   1.330 -  "case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
   1.331 -
   1.332 -subsection {* Type-definition locale instantiations *}
   1.333 -
   1.334 -lemma word_size_gt_0 [iff]: "0 < size (w::'a::len word)"
   1.335 -  by (fact xtr1 [OF word_size len_gt_0])
   1.336 -
   1.337 -lemmas lens_gt_0 = word_size_gt_0 len_gt_0
   1.338 -lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0]
   1.339 -
   1.340 -lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
   1.341 -  by (simp add: uints_def range_bintrunc)
   1.342 -
   1.343 -lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
   1.344 -  by (simp add: sints_def range_sbintrunc)
   1.345 -
   1.346 -lemma 
   1.347 -  uint_0:"0 <= uint x" and 
   1.348 -  uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
   1.349 -  by (auto simp: uint [unfolded atLeastLessThan_iff])
   1.350 -
   1.351 -lemma uint_mod_same:
   1.352 -  "uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
   1.353 -  by (simp add: int_mod_eq uint_lt uint_0)
   1.354 -
   1.355 -lemma td_ext_uint: 
   1.356 -  "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0))) 
   1.357 -    (%w::int. w mod 2 ^ len_of TYPE('a))"
   1.358 -  apply (unfold td_ext_def')
   1.359 -  apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
   1.360 -  apply (simp add: uint_mod_same uint_0 uint_lt
   1.361 -                   word.uint_inverse word.Abs_word_inverse int_mod_lem)
   1.362 -  done
   1.363 -
   1.364 -interpretation word_uint:
   1.365 -  td_ext "uint::'a::len0 word \<Rightarrow> int" 
   1.366 -         word_of_int 
   1.367 -         "uints (len_of TYPE('a::len0))"
   1.368 -         "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
   1.369 -  by (rule td_ext_uint)
   1.370 -
   1.371 -lemmas td_uint = word_uint.td_thm
   1.372 -
   1.373 -lemmas int_word_uint = word_uint.eq_norm
   1.374 -
   1.375 -lemmas td_ext_ubin = td_ext_uint 
   1.376 -  [unfolded len_gt_0 no_bintr_alt1 [symmetric]]
   1.377 -
   1.378 -interpretation word_ubin:
   1.379 -  td_ext "uint::'a::len0 word \<Rightarrow> int" 
   1.380 -         word_of_int 
   1.381 -         "uints (len_of TYPE('a::len0))"
   1.382 -         "bintrunc (len_of TYPE('a::len0))"
   1.383 -  by (rule td_ext_ubin)
   1.384 -
   1.385 -lemma split_word_all:
   1.386 -  "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
   1.387 -proof
   1.388 -  fix x :: "'a word"
   1.389 -  assume "\<And>x. PROP P (word_of_int x)"
   1.390 -  hence "PROP P (word_of_int (uint x))" .
   1.391 -  thus "PROP P x" by simp
   1.392 -qed
   1.393 -
   1.394 -subsection {* Correspondence relation for theorem transfer *}
   1.395 -
   1.396 -definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
   1.397 -where
   1.398 -  "cr_word = (\<lambda>x y. word_of_int x = y)"
   1.399 -
   1.400 -lemma Quotient_word:
   1.401 -  "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
   1.402 -    word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
   1.403 -  unfolding Quotient_alt_def cr_word_def
   1.404 -  by (simp add: word_ubin.norm_eq_iff)
   1.405 -
   1.406 -lemma reflp_word:
   1.407 -  "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
   1.408 -  by (simp add: reflp_def)
   1.409 -
   1.410 -setup_lifting(no_code) Quotient_word reflp_word
   1.411 -
   1.412 -text {* TODO: The next lemma could be generated automatically. *}
   1.413 -
   1.414 -lemma uint_transfer [transfer_rule]:
   1.415 -  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
   1.416 -    (uint :: 'a::len0 word \<Rightarrow> int)"
   1.417 -  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by (simp add: word_ubin.eq_norm)
   1.418 -
   1.419 -subsection  "Arithmetic operations"
   1.420 +subsection {* Arithmetic operations *}
   1.421  
   1.422  lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
   1.423    by (metis bintr_ariths(6))
   1.424 @@ -365,7 +372,7 @@
   1.425    "a udvd b = (EX n>=0. uint b = n * uint a)"
   1.426  
   1.427  
   1.428 -subsection "Ordering"
   1.429 +subsection {* Ordering *}
   1.430  
   1.431  instantiation word :: (len0) linorder
   1.432  begin
   1.433 @@ -390,7 +397,7 @@
   1.434    "(x <s y) = (x <=s y & x ~= y)"
   1.435  
   1.436  
   1.437 -subsection "Bit-wise operations"
   1.438 +subsection {* Bit-wise operations *}
   1.439  
   1.440  instantiation word :: (len0) bits
   1.441  begin
   1.442 @@ -467,7 +474,7 @@
   1.443    "clearBit w n = set_bit w n False"
   1.444  
   1.445  
   1.446 -subsection "Shift operations"
   1.447 +subsection {* Shift operations *}
   1.448  
   1.449  definition sshiftr1 :: "'a :: len word => 'a word"
   1.450  where 
   1.451 @@ -498,7 +505,7 @@
   1.452    "slice n w = slice1 (size w - n) w"
   1.453  
   1.454  
   1.455 -subsection "Rotation"
   1.456 +subsection {* Rotation *}
   1.457  
   1.458  definition rotater1 :: "'a list => 'a list"
   1.459  where
   1.460 @@ -523,7 +530,7 @@
   1.461                      else word_rotl (nat (- i)) w)"
   1.462  
   1.463  
   1.464 -subsection "Split and cat operations"
   1.465 +subsection {* Split and cat operations *}
   1.466  
   1.467  definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
   1.468  where
   1.469 @@ -549,8 +556,8 @@
   1.470  where
   1.471    "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
   1.472  
   1.473 -(* FIXME: only provide one theorem name *)
   1.474 -lemmas of_nth_def = word_set_bits_def
   1.475 +lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
   1.476 +
   1.477  
   1.478  subsection {* Theorems about typedefs *}
   1.479  
   1.480 @@ -578,7 +585,7 @@
   1.481    by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min.absorb1)
   1.482  
   1.483  lemma td_ext_sbin: 
   1.484 -  "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len))) 
   1.485 +  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (len_of TYPE('a::len))) 
   1.486      (sbintrunc (len_of TYPE('a) - 1))"
   1.487    apply (unfold td_ext_def' sint_uint)
   1.488    apply (simp add : word_ubin.eq_norm)
   1.489 @@ -591,8 +598,11 @@
   1.490    apply simp
   1.491    done
   1.492  
   1.493 -lemmas td_ext_sint = td_ext_sbin 
   1.494 -  [simplified len_gt_0 no_sbintr_alt2 Suc_pred' [symmetric]]
   1.495 +lemma td_ext_sint:
   1.496 +  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (len_of TYPE('a::len)))
   1.497 +     (\<lambda>w. (w + 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
   1.498 +         2 ^ (len_of TYPE('a) - 1))"
   1.499 +  using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
   1.500  
   1.501  (* We do sint before sbin, before sint is the user version
   1.502     and interpretations do not produce thm duplicates. I.e. 
   1.503 @@ -706,8 +716,8 @@
   1.504    by (simp only: not_le uint_m2p_neg)
   1.505  
   1.506  lemma lt2p_lem:
   1.507 -  "len_of TYPE('a) <= n \<Longrightarrow> uint (w :: 'a :: len0 word) < 2 ^ n"
   1.508 -  by (rule xtr8 [OF _ uint_lt2p]) simp
   1.509 +  "len_of TYPE('a) \<le> n \<Longrightarrow> uint (w :: 'a::len0 word) < 2 ^ n"
   1.510 +  by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)
   1.511  
   1.512  lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
   1.513    by (fact uint_ge_0 [THEN leD, THEN linorder_antisym_conv1])
   1.514 @@ -739,10 +749,12 @@
   1.515      2 ^ (len_of TYPE('a) - 1)"
   1.516    unfolding word_numeral_alt by (rule int_word_sint)
   1.517  
   1.518 -lemma word_of_int_0 [simp, code_post]: "word_of_int 0 = 0"
   1.519 +lemma word_of_int_0 [simp, code_post]:
   1.520 +  "word_of_int 0 = 0"
   1.521    unfolding word_0_wi ..
   1.522  
   1.523 -lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1"
   1.524 +lemma word_of_int_1 [simp, code_post]:
   1.525 +  "word_of_int 1 = 1"
   1.526    unfolding word_1_wi ..
   1.527  
   1.528  lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"
   1.529 @@ -766,14 +778,14 @@
   1.530      (ALL i. x = (word_of_int i :: 'b :: len0 word) & 
   1.531        0 <= i & i < 2 ^ len_of TYPE('b) --> P (f i))"
   1.532    unfolding word_int_case_def
   1.533 -  by (auto simp: word_uint.eq_norm int_mod_eq')
   1.534 +  by (auto simp: word_uint.eq_norm mod_pos_pos_trivial)
   1.535  
   1.536  lemma word_int_split_asm: 
   1.537    "P (word_int_case f x) = 
   1.538      (~ (EX n. x = (word_of_int n :: 'b::len0 word) &
   1.539        0 <= n & n < 2 ^ len_of TYPE('b::len0) & ~ P (f n)))"
   1.540    unfolding word_int_case_def
   1.541 -  by (auto simp: word_uint.eq_norm int_mod_eq')
   1.542 +  by (auto simp: word_uint.eq_norm mod_pos_pos_trivial)
   1.543  
   1.544  lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]
   1.545  lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]
   1.546 @@ -792,6 +804,7 @@
   1.547    "x \<le> - (2 ^ (size (w::'a::len word) - 1)) \<Longrightarrow> x \<le> sint w"
   1.548    unfolding word_size by (rule order_trans [OF _ sint_ge])
   1.549  
   1.550 +
   1.551  subsection {* Testing bits *}
   1.552  
   1.553  lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
   1.554 @@ -855,7 +868,7 @@
   1.555    type_definition "to_bl :: 'a::len0 word => bool list"
   1.556                    of_bl  
   1.557                    "{bl. length bl = len_of TYPE('a::len0)}"
   1.558 -  by (rule td_bl)
   1.559 +  by (fact td_bl)
   1.560  
   1.561  lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
   1.562  
   1.563 @@ -1279,7 +1292,8 @@
   1.564    word_sub_wi
   1.565    word_arith_wis (* FIXME: duplicate *)
   1.566  
   1.567 -subsection  "Transferring goals from words to ints"
   1.568 +
   1.569 +subsection {* Transferring goals from words to ints *}
   1.570  
   1.571  lemma word_ths:  
   1.572    shows
   1.573 @@ -1327,7 +1341,7 @@
   1.574    by (rule_tac x="uint x" in exI) simp
   1.575  
   1.576  
   1.577 -subsection "Order on fixed-length words"
   1.578 +subsection {* Order on fixed-length words *}
   1.579  
   1.580  lemma word_zero_le [simp] :
   1.581    "0 <= (y :: 'a :: len0 word)"
   1.582 @@ -1389,28 +1403,22 @@
   1.583  
   1.584  lemmas unat_mono = word_less_nat_alt [THEN iffD1]
   1.585  
   1.586 -lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1"
   1.587 -  apply (unfold unat_def)
   1.588 -  apply (simp only: int_word_uint word_arith_alts rdmods)
   1.589 -  apply (subgoal_tac "uint x >= 1")
   1.590 -   prefer 2
   1.591 -   apply (drule contrapos_nn)
   1.592 -    apply (erule word_uint.Rep_inverse' [symmetric])
   1.593 -   apply (insert uint_ge_0 [of x])[1]
   1.594 -   apply arith
   1.595 -  apply (rule box_equals)
   1.596 -    apply (rule nat_diff_distrib)
   1.597 -     prefer 2
   1.598 -     apply assumption
   1.599 -    apply simp
   1.600 -   apply (subst mod_pos_pos_trivial)
   1.601 -     apply arith
   1.602 -    apply (insert uint_lt2p [of x])[1]
   1.603 -    apply arith
   1.604 -   apply (rule refl)
   1.605 -  apply simp
   1.606 -  done
   1.607 -    
   1.608 +lemma unat_minus_one:
   1.609 +  assumes "w \<noteq> 0"
   1.610 +  shows "unat (w - 1) = unat w - 1"
   1.611 +proof -
   1.612 +  have "0 \<le> uint w" by (fact uint_nonnegative)
   1.613 +  moreover from assms have "0 \<noteq> uint w" by (simp add: uint_0_iff)
   1.614 +  ultimately have "1 \<le> uint w" by arith
   1.615 +  from uint_lt2p [of w] have "uint w - 1 < 2 ^ len_of TYPE('a)" by arith
   1.616 +  with `1 \<le> uint w` have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
   1.617 +    by (auto intro: mod_pos_pos_trivial)
   1.618 +  with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
   1.619 +    by auto
   1.620 +  then show ?thesis
   1.621 +    by (simp only: unat_def int_word_uint word_arith_alts mod_diff_right_eq [symmetric])
   1.622 +qed
   1.623 +
   1.624  lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
   1.625    by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
   1.626    
   1.627 @@ -1423,7 +1431,7 @@
   1.628    using uint_ge_0 [of y] uint_lt2p [of x] by arith
   1.629  
   1.630  
   1.631 -subsection "Conditions for the addition (etc) of two words to overflow"
   1.632 +subsection {* Conditions for the addition (etc) of two words to overflow *}
   1.633  
   1.634  lemma uint_add_lem: 
   1.635    "(uint x + uint y < 2 ^ len_of TYPE('a)) = 
   1.636 @@ -1440,16 +1448,35 @@
   1.637    by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
   1.638  
   1.639  lemma uint_add_le: "uint (x + y) <= uint x + uint y"
   1.640 -  unfolding uint_word_ariths by (auto simp: mod_add_if_z)
   1.641 +  unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend)
   1.642  
   1.643  lemma uint_sub_ge: "uint (x - y) >= uint x - uint y"
   1.644 -  unfolding uint_word_ariths by (auto simp: mod_sub_if_z)
   1.645 -
   1.646 -lemmas uint_sub_if' = trans [OF uint_word_ariths(1) mod_sub_if_z, simplified]
   1.647 -lemmas uint_plus_if' = trans [OF uint_word_ariths(2) mod_add_if_z, simplified]
   1.648 -
   1.649 -
   1.650 -subsection {* Definition of uint\_arith *}
   1.651 +  unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)
   1.652 +
   1.653 +lemma mod_add_if_z:
   1.654 +  "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 
   1.655 +   (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   1.656 +  by (auto intro: int_mod_eq)
   1.657 +
   1.658 +lemma uint_plus_if':
   1.659 +  "uint ((a::'a word) + b) =
   1.660 +  (if uint a + uint b < 2 ^ len_of TYPE('a::len0) then uint a + uint b
   1.661 +   else uint a + uint b - 2 ^ len_of TYPE('a))"
   1.662 +  using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
   1.663 +
   1.664 +lemma mod_sub_if_z:
   1.665 +  "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 
   1.666 +   (x - y) mod z = (if y <= x then x - y else x - y + z)"
   1.667 +  by (auto intro: int_mod_eq)
   1.668 +
   1.669 +lemma uint_sub_if':
   1.670 +  "uint ((a::'a word) - b) =
   1.671 +  (if uint b \<le> uint a then uint a - uint b
   1.672 +   else uint a - uint b + 2 ^ len_of TYPE('a::len0))"
   1.673 +  using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
   1.674 +
   1.675 +
   1.676 +subsection {* Definition of @{text uint_arith} *}
   1.677  
   1.678  lemma word_of_int_inverse:
   1.679    "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow> 
   1.680 @@ -1463,7 +1490,7 @@
   1.681    shows "P (uint x) = 
   1.682           (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
   1.683    apply (fold word_int_case_def)
   1.684 -  apply (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq'
   1.685 +  apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial
   1.686                split: word_int_split)
   1.687    done
   1.688  
   1.689 @@ -1472,7 +1499,7 @@
   1.690    shows "P (uint x) = 
   1.691           (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
   1.692    by (auto dest!: word_of_int_inverse 
   1.693 -           simp: int_word_uint int_mod_eq'
   1.694 +           simp: int_word_uint mod_pos_pos_trivial
   1.695             split: uint_split)
   1.696  
   1.697  lemmas uint_splits = uint_split uint_split_asm
   1.698 @@ -1523,7 +1550,7 @@
   1.699    "solving word arithmetic via integers and arith"
   1.700  
   1.701  
   1.702 -subsection "More on overflows and monotonicity"
   1.703 +subsection {* More on overflows and monotonicity *}
   1.704  
   1.705  lemma no_plus_overflow_uint_size: 
   1.706    "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
   1.707 @@ -1654,6 +1681,7 @@
   1.708    "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow> 
   1.709      uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
   1.710    apply clarsimp
   1.711 +  
   1.712    apply (drule less_le_mult)
   1.713    apply safe
   1.714    done
   1.715 @@ -1748,7 +1776,7 @@
   1.716                   word_pred_rbl word_mult_rbl word_add_rbl)
   1.717  
   1.718  
   1.719 -subsection "Arithmetic type class instantiations"
   1.720 +subsection {* Arithmetic type class instantiations *}
   1.721  
   1.722  lemmas word_le_0_iff [simp] =
   1.723    word_zero_le [THEN leD, THEN linorder_antisym_conv1]
   1.724 @@ -1771,7 +1799,7 @@
   1.725    eq_numeral_iff_iszero [where 'a="'a::len word"]
   1.726  
   1.727  
   1.728 -subsection "Word and nat"
   1.729 +subsection {* Word and nat *}
   1.730  
   1.731  lemma td_ext_unat [OF refl]:
   1.732    "n = len_of TYPE ('a :: len) \<Longrightarrow> 
   1.733 @@ -1962,7 +1990,7 @@
   1.734    unfolding uint_nat by (simp add : unat_mod zmod_int)
   1.735  
   1.736  
   1.737 -subsection {* Definition of unat\_arith tactic *}
   1.738 +subsection {* Definition of @[text unat_arith} tactic *}
   1.739  
   1.740  lemma unat_split:
   1.741    fixes x::"'a::len word"
   1.742 @@ -2157,7 +2185,7 @@
   1.743    done
   1.744  
   1.745  
   1.746 -subsection "Cardinality, finiteness of set of words"
   1.747 +subsection {* Cardinality, finiteness of set of words *}
   1.748  
   1.749  instance word :: (len0) finite
   1.750    by (default, simp add: type_definition.univ [OF type_definition_word])
   1.751 @@ -2865,7 +2893,8 @@
   1.752                     zdiv_zmult2_eq [symmetric])
   1.753    done
   1.754  
   1.755 -subsubsection "shift functions in terms of lists of bools"
   1.756 +
   1.757 +subsubsection {* shift functions in terms of lists of bools *}
   1.758  
   1.759  lemmas bshiftr1_numeral [simp] = 
   1.760    bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
   1.761 @@ -3152,7 +3181,8 @@
   1.762       apply (simp_all add: word_size)
   1.763    done
   1.764  
   1.765 -subsubsection "Mask"
   1.766 +
   1.767 +subsubsection {* Mask *}
   1.768  
   1.769  lemma nth_mask [OF refl, simp]:
   1.770    "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
   1.771 @@ -3240,7 +3270,7 @@
   1.772    "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
   1.773    apply (unfold word_size word_less_alt word_numeral_alt)
   1.774    apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
   1.775 -                            int_mod_eq'
   1.776 +                            mod_pos_pos_trivial
   1.777                    simp del: word_of_int_numeral)
   1.778    done
   1.779  
   1.780 @@ -3287,7 +3317,7 @@
   1.781    by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
   1.782  
   1.783  
   1.784 -subsubsection "Revcast"
   1.785 +subsubsection {* Revcast *}
   1.786  
   1.787  lemmas revcast_def' = revcast_def [simplified]
   1.788  lemmas revcast_def'' = revcast_def' [simplified word_size]
   1.789 @@ -3402,7 +3432,7 @@
   1.790    rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
   1.791  
   1.792  
   1.793 -subsubsection "Slices"
   1.794 +subsubsection {* Slices *}
   1.795  
   1.796  lemma slice1_no_bin [simp]:
   1.797    "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
   1.798 @@ -3542,7 +3572,7 @@
   1.799    done
   1.800  
   1.801  
   1.802 -subsection "Split and cat"
   1.803 +subsection {* Split and cat *}
   1.804  
   1.805  lemmas word_split_bin' = word_split_def
   1.806  lemmas word_cat_bin' = word_cat_def
   1.807 @@ -3707,7 +3737,7 @@
   1.808  lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
   1.809  
   1.810  
   1.811 -subsubsection "Split and slice"
   1.812 +subsubsection {* Split and slice *}
   1.813  
   1.814  lemma split_slices: 
   1.815    "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
   1.816 @@ -3911,7 +3941,7 @@
   1.817    done
   1.818  
   1.819  
   1.820 -subsection "Rotation"
   1.821 +subsection {* Rotation *}
   1.822  
   1.823  lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
   1.824  
   1.825 @@ -3933,7 +3963,7 @@
   1.826    rotate_eq_mod
   1.827  
   1.828  
   1.829 -subsubsection "Rotation of list to right"
   1.830 +subsubsection {* Rotation of list to right *}
   1.831  
   1.832  lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
   1.833    unfolding rotater1_def by (cases l) auto
   1.834 @@ -4008,7 +4038,7 @@
   1.835  lemmas rotater_add = rotater_eqs (2)
   1.836  
   1.837  
   1.838 -subsubsection "map, map2, commuting with rotate(r)"
   1.839 +subsubsection {* map, map2, commuting with rotate(r) *}
   1.840  
   1.841  lemma butlast_map:
   1.842    "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   1.843 @@ -4184,7 +4214,7 @@
   1.844  lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
   1.845  
   1.846  
   1.847 -subsubsection "Word rotation commutes with bit-wise operations"
   1.848 +subsubsection {* "Word rotation commutes with bit-wise operations *}
   1.849  
   1.850  (* using locale to not pollute lemma namespace *)
   1.851  locale word_rotate 
   1.852 @@ -4279,7 +4309,7 @@
   1.853  
   1.854  lemma max_word_max [simp,intro!]: "n \<le> max_word"
   1.855    by (cases n rule: word_int_cases)
   1.856 -    (simp add: max_word_def word_le_def int_word_uint int_mod_eq' del: minus_mod_self1)
   1.857 +    (simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1)
   1.858    
   1.859  lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
   1.860    by (subst word_uint.Abs_norm [symmetric]) simp
   1.861 @@ -4574,6 +4604,7 @@
   1.862    apply (case_tac "1+n = 0", auto)
   1.863    done
   1.864  
   1.865 +
   1.866  subsection {* Recursion combinator for words *}
   1.867  
   1.868  definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
   1.869 @@ -4693,3 +4724,5 @@
   1.870  
   1.871  end
   1.872  
   1.873 +
   1.874 +