1(* Title: HOL/Word/Word.thy 2 Author: Jeremy Dawson and Gerwin Klein, NICTA 3*) 4 5section \<open>A type of finite bit strings\<close> 6 7theory Word 8imports 9 "HOL-Library.Type_Length" 10 "HOL-Library.Boolean_Algebra" 11 Bits_Int 12 Bits_Z2 13 Bit_Comprehension 14 Misc_Typedef 15 Misc_Arithmetic 16begin 17 18text \<open>See \<^file>\<open>Word_Examples.thy\<close> for examples.\<close> 19 20subsection \<open>Type definition\<close> 21 22typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ LENGTH('a::len0)}" 23 morphisms uint Abs_word by auto 24 25lemma uint_nonnegative: "0 \<le> uint w" 26 using word.uint [of w] by simp 27 28lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" 29 for w :: "'a::len0 word" 30 using word.uint [of w] by simp 31 32lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" 33 for w :: "'a::len0 word" 34 using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial) 35 36lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b" 37 by (simp add: uint_inject) 38 39lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b" 40 by (simp add: word_uint_eq_iff) 41 42definition word_of_int :: "int \<Rightarrow> 'a::len0 word" 43 \<comment> \<open>representation of words using unsigned or signed bins, 44 only difference in these is the type class\<close> 45 where "word_of_int k = Abs_word (k mod 2 ^ LENGTH('a))" 46 47lemma uint_word_of_int: "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ LENGTH('a)" 48 by (auto simp add: word_of_int_def intro: Abs_word_inverse) 49 50lemma word_of_int_uint: "word_of_int (uint w) = w" 51 by (simp add: word_of_int_def uint_idem uint_inverse) 52 53lemma split_word_all: "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))" 54proof 55 fix x :: "'a word" 56 assume "\<And>x. PROP P (word_of_int x)" 57 then have "PROP P (word_of_int (uint x))" . 58 then show "PROP P x" by (simp add: word_of_int_uint) 59qed 60 61 62subsection \<open>Type conversions and casting\<close> 63 64definition sint :: "'a::len word \<Rightarrow> int" 65 \<comment> \<open>treats the most-significant-bit as a sign bit\<close> 66 where sint_uint: "sint w = sbintrunc (LENGTH('a) - 1) (uint w)" 67 68definition unat :: "'a::len0 word \<Rightarrow> nat" 69 where "unat w = nat (uint w)" 70 71definition uints :: "nat \<Rightarrow> int set" 72 \<comment> \<open>the sets of integers representing the words\<close> 73 where "uints n = range (bintrunc n)" 74 75definition sints :: "nat \<Rightarrow> int set" 76 where "sints n = range (sbintrunc (n - 1))" 77 78lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}" 79 by (simp add: uints_def range_bintrunc) 80 81lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}" 82 by (simp add: sints_def range_sbintrunc) 83 84definition unats :: "nat \<Rightarrow> nat set" 85 where "unats n = {i. i < 2 ^ n}" 86 87definition norm_sint :: "nat \<Rightarrow> int \<Rightarrow> int" 88 where "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)" 89 90definition scast :: "'a::len word \<Rightarrow> 'b::len word" 91 \<comment> \<open>cast a word to a different length\<close> 92 where "scast w = word_of_int (sint w)" 93 94definition ucast :: "'a::len0 word \<Rightarrow> 'b::len0 word" 95 where "ucast w = word_of_int (uint w)" 96 97instantiation word :: (len0) size 98begin 99 100definition word_size: "size (w :: 'a word) = LENGTH('a)" 101 102instance .. 103 104end 105 106lemma word_size_gt_0 [iff]: "0 < size w" 107 for w :: "'a::len word" 108 by (simp add: word_size) 109 110lemmas lens_gt_0 = word_size_gt_0 len_gt_0 111 112lemma lens_not_0 [iff]: 113 fixes w :: "'a::len word" 114 shows "size w \<noteq> 0" 115 and "LENGTH('a) \<noteq> 0" 116 by auto 117 118definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat" 119 \<comment> \<open>whether a cast (or other) function is to a longer or shorter length\<close> 120 where [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)" 121 122definition target_size :: "('a \<Rightarrow> 'b::len0 word) \<Rightarrow> nat" 123 where [code del]: "target_size c = size (c undefined)" 124 125definition is_up :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool" 126 where "is_up c \<longleftrightarrow> source_size c \<le> target_size c" 127 128definition is_down :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool" 129 where "is_down c \<longleftrightarrow> target_size c \<le> source_size c" 130 131definition of_bl :: "bool list \<Rightarrow> 'a::len0 word" 132 where "of_bl bl = word_of_int (bl_to_bin bl)" 133 134definition to_bl :: "'a::len0 word \<Rightarrow> bool list" 135 where "to_bl w = bin_to_bl (LENGTH('a)) (uint w)" 136 137definition word_reverse :: "'a::len0 word \<Rightarrow> 'a word" 138 where "word_reverse w = of_bl (rev (to_bl w))" 139 140definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len0 word \<Rightarrow> 'b" 141 where "word_int_case f w = f (uint w)" 142 143translations 144 "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x" 145 "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x" 146 147 148subsection \<open>Correspondence relation for theorem transfer\<close> 149 150definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool" 151 where "cr_word = (\<lambda>x y. word_of_int x = y)" 152 153lemma Quotient_word: 154 "Quotient (\<lambda>x y. bintrunc (LENGTH('a)) x = bintrunc (LENGTH('a)) y) 155 word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)" 156 unfolding Quotient_alt_def cr_word_def 157 by (simp add: no_bintr_alt1 word_of_int_uint) (simp add: word_of_int_def Abs_word_inject) 158 159lemma reflp_word: 160 "reflp (\<lambda>x y. bintrunc (LENGTH('a::len0)) x = bintrunc (LENGTH('a)) y)" 161 by (simp add: reflp_def) 162 163setup_lifting Quotient_word reflp_word 164 165text \<open>TODO: The next lemma could be generated automatically.\<close> 166 167lemma uint_transfer [transfer_rule]: 168 "(rel_fun pcr_word (=)) (bintrunc (LENGTH('a))) (uint :: 'a::len0 word \<Rightarrow> int)" 169 unfolding rel_fun_def word.pcr_cr_eq cr_word_def 170 by (simp add: no_bintr_alt1 uint_word_of_int) 171 172 173subsection \<open>Basic code generation setup\<close> 174 175definition Word :: "int \<Rightarrow> 'a::len0 word" 176 where [code_post]: "Word = word_of_int" 177 178lemma [code abstype]: "Word (uint w) = w" 179 by (simp add: Word_def word_of_int_uint) 180 181declare uint_word_of_int [code abstract] 182 183instantiation word :: (len0) equal 184begin 185 186definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" 187 where "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)" 188 189instance 190 by standard (simp add: equal equal_word_def word_uint_eq_iff) 191 192end 193 194notation fcomp (infixl "\<circ>>" 60) 195notation scomp (infixl "\<circ>\<rightarrow>" 60) 196 197instantiation word :: ("{len0, typerep}") random 198begin 199 200definition 201 "random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair ( 202 let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word 203 in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))" 204 205instance .. 206 207end 208 209no_notation fcomp (infixl "\<circ>>" 60) 210no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 211 212 213subsection \<open>Type-definition locale instantiations\<close> 214 215lemmas uint_0 = uint_nonnegative (* FIXME duplicate *) 216lemmas uint_lt = uint_bounded (* FIXME duplicate *) 217lemmas uint_mod_same = uint_idem (* FIXME duplicate *) 218 219lemma td_ext_uint: 220 "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len0))) 221 (\<lambda>w::int. w mod 2 ^ LENGTH('a))" 222 apply (unfold td_ext_def') 223 apply (simp add: uints_num word_of_int_def bintrunc_mod2p) 224 apply (simp add: uint_mod_same uint_0 uint_lt 225 word.uint_inverse word.Abs_word_inverse int_mod_lem) 226 done 227 228interpretation word_uint: 229 td_ext 230 "uint::'a::len0 word \<Rightarrow> int" 231 word_of_int 232 "uints (LENGTH('a::len0))" 233 "\<lambda>w. w mod 2 ^ LENGTH('a::len0)" 234 by (fact td_ext_uint) 235 236lemmas td_uint = word_uint.td_thm 237lemmas int_word_uint = word_uint.eq_norm 238 239lemma td_ext_ubin: 240 "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len0))) 241 (bintrunc (LENGTH('a)))" 242 by (unfold no_bintr_alt1) (fact td_ext_uint) 243 244interpretation word_ubin: 245 td_ext 246 "uint::'a::len0 word \<Rightarrow> int" 247 word_of_int 248 "uints (LENGTH('a::len0))" 249 "bintrunc (LENGTH('a::len0))" 250 by (fact td_ext_ubin) 251 252 253subsection \<open>Arithmetic operations\<close> 254 255lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1" 256 by (auto simp add: bintrunc_mod2p intro: mod_add_cong) 257 258lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1" 259 by (auto simp add: bintrunc_mod2p intro: mod_diff_cong) 260 261instantiation word :: (len0) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}" 262begin 263 264lift_definition zero_word :: "'a word" is "0" . 265 266lift_definition one_word :: "'a word" is "1" . 267 268lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(+)" 269 by (auto simp add: bintrunc_mod2p intro: mod_add_cong) 270 271lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(-)" 272 by (auto simp add: bintrunc_mod2p intro: mod_diff_cong) 273 274lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus 275 by (auto simp add: bintrunc_mod2p intro: mod_minus_cong) 276 277lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(*)" 278 by (auto simp add: bintrunc_mod2p intro: mod_mult_cong) 279 280definition word_div_def: "a div b = word_of_int (uint a div uint b)" 281 282definition word_mod_def: "a mod b = word_of_int (uint a mod uint b)" 283 284instance 285 by standard (transfer, simp add: algebra_simps)+ 286 287end 288 289quickcheck_generator word 290 constructors: 291 "zero_class.zero :: ('a::len) word", 292 "numeral :: num \<Rightarrow> ('a::len) word", 293 "uminus :: ('a::len) word \<Rightarrow> ('a::len) word" 294 295text \<open>Legacy theorems:\<close> 296 297lemma word_arith_wis [code]: 298 shows word_add_def: "a + b = word_of_int (uint a + uint b)" 299 and word_sub_wi: "a - b = word_of_int (uint a - uint b)" 300 and word_mult_def: "a * b = word_of_int (uint a * uint b)" 301 and word_minus_def: "- a = word_of_int (- uint a)" 302 and word_succ_alt: "word_succ a = word_of_int (uint a + 1)" 303 and word_pred_alt: "word_pred a = word_of_int (uint a - 1)" 304 and word_0_wi: "0 = word_of_int 0" 305 and word_1_wi: "1 = word_of_int 1" 306 unfolding plus_word_def minus_word_def times_word_def uminus_word_def 307 unfolding word_succ_def word_pred_def zero_word_def one_word_def 308 by simp_all 309 310lemma wi_homs: 311 shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" 312 and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)" 313 and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" 314 and wi_hom_neg: "- word_of_int a = word_of_int (- a)" 315 and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" 316 and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)" 317 by (transfer, simp)+ 318 319lemmas wi_hom_syms = wi_homs [symmetric] 320 321lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi 322 323lemmas word_of_int_hom_syms = word_of_int_homs [symmetric] 324 325instance word :: (len) comm_ring_1 326proof 327 have *: "0 < LENGTH('a)" by (rule len_gt_0) 328 show "(0::'a word) \<noteq> 1" 329 by transfer (use * in \<open>auto simp add: gr0_conv_Suc\<close>) 330qed 331 332lemma word_of_nat: "of_nat n = word_of_int (int n)" 333 by (induct n) (auto simp add : word_of_int_hom_syms) 334 335lemma word_of_int: "of_int = word_of_int" 336 apply (rule ext) 337 apply (case_tac x rule: int_diff_cases) 338 apply (simp add: word_of_nat wi_hom_sub) 339 done 340 341definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50) 342 where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)" 343 344 345subsection \<open>Ordering\<close> 346 347instantiation word :: (len0) linorder 348begin 349 350definition word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b" 351 352definition word_less_def: "a < b \<longleftrightarrow> uint a < uint b" 353 354instance 355 by standard (auto simp: word_less_def word_le_def) 356 357end 358 359definition word_sle :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" ("(_/ <=s _)" [50, 51] 50) 360 where "a <=s b \<longleftrightarrow> sint a \<le> sint b" 361 362definition word_sless :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" ("(_/ <s _)" [50, 51] 50) 363 where "x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y" 364 365 366subsection \<open>Bit-wise operations\<close> 367 368definition shiftl1 :: "'a::len0 word \<Rightarrow> 'a word" 369 where "shiftl1 w = word_of_int (uint w BIT False)" 370 371definition shiftr1 :: "'a::len0 word \<Rightarrow> 'a word" 372 \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close> 373 where "shiftr1 w = word_of_int (bin_rest (uint w))" 374 375instantiation word :: (len0) bit_operations 376begin 377 378lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is bitNOT 379 by (metis bin_trunc_not) 380 381lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitAND 382 by (metis bin_trunc_and) 383 384lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitOR 385 by (metis bin_trunc_or) 386 387lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitXOR 388 by (metis bin_trunc_xor) 389 390definition word_test_bit_def: "test_bit a = bin_nth (uint a)" 391 392definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))" 393 394definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)" 395 396definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1" 397 398definition shiftl_def: "w << n = (shiftl1 ^^ n) w" 399 400definition shiftr_def: "w >> n = (shiftr1 ^^ n) w" 401 402instance .. 403 404end 405 406lemma word_msb_def: 407 "msb a \<longleftrightarrow> bin_sign (sint a) = - 1" 408 by (simp add: msb_word_def sint_uint) 409 410lemma [code]: 411 shows word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))" 412 and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" 413 and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" 414 and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" 415 by (simp_all add: bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def) 416 417definition setBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word" 418 where "setBit w n = set_bit w n True" 419 420definition clearBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word" 421 where "clearBit w n = set_bit w n False" 422 423 424subsection \<open>Shift operations\<close> 425 426definition sshiftr1 :: "'a::len word \<Rightarrow> 'a word" 427 where "sshiftr1 w = word_of_int (bin_rest (sint w))" 428 429definition bshiftr1 :: "bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word" 430 where "bshiftr1 b w = of_bl (b # butlast (to_bl w))" 431 432definition sshiftr :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" (infixl ">>>" 55) 433 where "w >>> n = (sshiftr1 ^^ n) w" 434 435definition mask :: "nat \<Rightarrow> 'a::len word" 436 where "mask n = (1 << n) - 1" 437 438definition revcast :: "'a::len0 word \<Rightarrow> 'b::len0 word" 439 where "revcast w = of_bl (takefill False (LENGTH('b)) (to_bl w))" 440 441definition slice1 :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word" 442 where "slice1 n w = of_bl (takefill False n (to_bl w))" 443 444definition slice :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word" 445 where "slice n w = slice1 (size w - n) w" 446 447 448subsection \<open>Rotation\<close> 449 450definition rotater1 :: "'a list \<Rightarrow> 'a list" 451 where "rotater1 ys = 452 (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)" 453 454definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" 455 where "rotater n = rotater1 ^^ n" 456 457definition word_rotr :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word" 458 where "word_rotr n w = of_bl (rotater n (to_bl w))" 459 460definition word_rotl :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word" 461 where "word_rotl n w = of_bl (rotate n (to_bl w))" 462 463definition word_roti :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word" 464 where "word_roti i w = 465 (if i \<ge> 0 then word_rotr (nat i) w else word_rotl (nat (- i)) w)" 466 467 468subsection \<open>Split and cat operations\<close> 469 470definition word_cat :: "'a::len0 word \<Rightarrow> 'b::len0 word \<Rightarrow> 'c::len0 word" 471 where "word_cat a b = word_of_int (bin_cat (uint a) (LENGTH('b)) (uint b))" 472 473definition word_split :: "'a::len0 word \<Rightarrow> 'b::len0 word \<times> 'c::len0 word" 474 where "word_split a = 475 (case bin_split (LENGTH('c)) (uint a) of 476 (u, v) \<Rightarrow> (word_of_int u, word_of_int v))" 477 478definition word_rcat :: "'a::len0 word list \<Rightarrow> 'b::len0 word" 479 where "word_rcat ws = word_of_int (bin_rcat (LENGTH('a)) (map uint ws))" 480 481definition word_rsplit :: "'a::len0 word \<Rightarrow> 'b::len word list" 482 where "word_rsplit w = map word_of_int (bin_rsplit (LENGTH('b)) (LENGTH('a), uint w))" 483 484definition max_word :: "'a::len word" 485 \<comment> \<open>Largest representable machine integer.\<close> 486 where "max_word = word_of_int (2 ^ LENGTH('a) - 1)" 487 488 489subsection \<open>Theorems about typedefs\<close> 490 491lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = sbintrunc (LENGTH('a::len) - 1) bin" 492 by (auto simp: sint_uint word_ubin.eq_norm sbintrunc_bintrunc_lt) 493 494lemma uint_sint: "uint w = bintrunc (LENGTH('a)) (sint w)" 495 for w :: "'a::len word" 496 by (auto simp: sint_uint bintrunc_sbintrunc_le) 497 498lemma bintr_uint: "LENGTH('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w" 499 for w :: "'a::len0 word" 500 apply (subst word_ubin.norm_Rep [symmetric]) 501 apply (simp only: bintrunc_bintrunc_min word_size) 502 apply (simp add: min.absorb2) 503 done 504 505lemma wi_bintr: 506 "LENGTH('a::len0) \<le> n \<Longrightarrow> 507 word_of_int (bintrunc n w) = (word_of_int w :: 'a word)" 508 by (auto simp: word_ubin.norm_eq_iff [symmetric] min.absorb1) 509 510lemma td_ext_sbin: 511 "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) 512 (sbintrunc (LENGTH('a) - 1))" 513 apply (unfold td_ext_def' sint_uint) 514 apply (simp add : word_ubin.eq_norm) 515 apply (cases "LENGTH('a)") 516 apply (auto simp add : sints_def) 517 apply (rule sym [THEN trans]) 518 apply (rule word_ubin.Abs_norm) 519 apply (simp only: bintrunc_sbintrunc) 520 apply (drule sym) 521 apply simp 522 done 523 524lemma td_ext_sint: 525 "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) 526 (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 527 2 ^ (LENGTH('a) - 1))" 528 using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2) 529 530text \<open> 531 We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version 532 and interpretations do not produce thm duplicates. I.e. 533 we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>, 534 because the latter is the same thm as the former. 535\<close> 536interpretation word_sint: 537 td_ext 538 "sint ::'a::len word \<Rightarrow> int" 539 word_of_int 540 "sints (LENGTH('a::len))" 541 "\<lambda>w. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) - 542 2 ^ (LENGTH('a::len) - 1)" 543 by (rule td_ext_sint) 544 545interpretation word_sbin: 546 td_ext 547 "sint ::'a::len word \<Rightarrow> int" 548 word_of_int 549 "sints (LENGTH('a::len))" 550 "sbintrunc (LENGTH('a::len) - 1)" 551 by (rule td_ext_sbin) 552 553lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm] 554 555lemmas td_sint = word_sint.td 556 557lemma to_bl_def': "(to_bl :: 'a::len0 word \<Rightarrow> bool list) = bin_to_bl (LENGTH('a)) \<circ> uint" 558 by (auto simp: to_bl_def) 559 560lemmas word_reverse_no_def [simp] = 561 word_reverse_def [of "numeral w"] for w 562 563lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)" 564 by (fact uints_def [unfolded no_bintr_alt1]) 565 566lemma word_numeral_alt: "numeral b = word_of_int (numeral b)" 567 by (induct b, simp_all only: numeral.simps word_of_int_homs) 568 569declare word_numeral_alt [symmetric, code_abbrev] 570 571lemma word_neg_numeral_alt: "- numeral b = word_of_int (- numeral b)" 572 by (simp only: word_numeral_alt wi_hom_neg) 573 574declare word_neg_numeral_alt [symmetric, code_abbrev] 575 576lemma word_numeral_transfer [transfer_rule]: 577 "(rel_fun (=) pcr_word) numeral numeral" 578 "(rel_fun (=) pcr_word) (- numeral) (- numeral)" 579 apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def) 580 using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by auto 581 582lemma uint_bintrunc [simp]: 583 "uint (numeral bin :: 'a word) = 584 bintrunc (LENGTH('a::len0)) (numeral bin)" 585 unfolding word_numeral_alt by (rule word_ubin.eq_norm) 586 587lemma uint_bintrunc_neg [simp]: 588 "uint (- numeral bin :: 'a word) = bintrunc (LENGTH('a::len0)) (- numeral bin)" 589 by (simp only: word_neg_numeral_alt word_ubin.eq_norm) 590 591lemma sint_sbintrunc [simp]: 592 "sint (numeral bin :: 'a word) = sbintrunc (LENGTH('a::len) - 1) (numeral bin)" 593 by (simp only: word_numeral_alt word_sbin.eq_norm) 594 595lemma sint_sbintrunc_neg [simp]: 596 "sint (- numeral bin :: 'a word) = sbintrunc (LENGTH('a::len) - 1) (- numeral bin)" 597 by (simp only: word_neg_numeral_alt word_sbin.eq_norm) 598 599lemma unat_bintrunc [simp]: 600 "unat (numeral bin :: 'a::len0 word) = nat (bintrunc (LENGTH('a)) (numeral bin))" 601 by (simp only: unat_def uint_bintrunc) 602 603lemma unat_bintrunc_neg [simp]: 604 "unat (- numeral bin :: 'a::len0 word) = nat (bintrunc (LENGTH('a)) (- numeral bin))" 605 by (simp only: unat_def uint_bintrunc_neg) 606 607lemma size_0_eq: "size w = 0 \<Longrightarrow> v = w" 608 for v w :: "'a::len0 word" 609 apply (unfold word_size) 610 apply (rule word_uint.Rep_eqD) 611 apply (rule box_equals) 612 defer 613 apply (rule word_ubin.norm_Rep)+ 614 apply simp 615 done 616 617lemma uint_ge_0 [iff]: "0 \<le> uint x" 618 for x :: "'a::len0 word" 619 using word_uint.Rep [of x] by (simp add: uints_num) 620 621lemma uint_lt2p [iff]: "uint x < 2 ^ LENGTH('a)" 622 for x :: "'a::len0 word" 623 using word_uint.Rep [of x] by (simp add: uints_num) 624 625lemma sint_ge: "- (2 ^ (LENGTH('a) - 1)) \<le> sint x" 626 for x :: "'a::len word" 627 using word_sint.Rep [of x] by (simp add: sints_num) 628 629lemma sint_lt: "sint x < 2 ^ (LENGTH('a) - 1)" 630 for x :: "'a::len word" 631 using word_sint.Rep [of x] by (simp add: sints_num) 632 633lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0" 634 by (simp add: sign_Pls_ge_0) 635 636lemma uint_m2p_neg: "uint x - 2 ^ LENGTH('a) < 0" 637 for x :: "'a::len0 word" 638 by (simp only: diff_less_0_iff_less uint_lt2p) 639 640lemma uint_m2p_not_non_neg: "\<not> 0 \<le> uint x - 2 ^ LENGTH('a)" 641 for x :: "'a::len0 word" 642 by (simp only: not_le uint_m2p_neg) 643 644lemma lt2p_lem: "LENGTH('a) \<le> n \<Longrightarrow> uint w < 2 ^ n" 645 for w :: "'a::len0 word" 646 by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p) 647 648lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0" 649 by (fact uint_ge_0 [THEN leD, THEN antisym_conv1]) 650 651lemma uint_nat: "uint w = int (unat w)" 652 by (auto simp: unat_def) 653 654lemma uint_numeral: "uint (numeral b :: 'a::len0 word) = numeral b mod 2 ^ LENGTH('a)" 655 by (simp only: word_numeral_alt int_word_uint) 656 657lemma uint_neg_numeral: "uint (- numeral b :: 'a::len0 word) = - numeral b mod 2 ^ LENGTH('a)" 658 by (simp only: word_neg_numeral_alt int_word_uint) 659 660lemma unat_numeral: "unat (numeral b :: 'a::len0 word) = numeral b mod 2 ^ LENGTH('a)" 661 apply (unfold unat_def) 662 apply (clarsimp simp only: uint_numeral) 663 apply (rule nat_mod_distrib [THEN trans]) 664 apply (rule zero_le_numeral) 665 apply (simp_all add: nat_power_eq) 666 done 667 668lemma sint_numeral: 669 "sint (numeral b :: 'a::len word) = 670 (numeral b + 671 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 672 2 ^ (LENGTH('a) - 1)" 673 unfolding word_numeral_alt by (rule int_word_sint) 674 675lemma word_of_int_0 [simp, code_post]: "word_of_int 0 = 0" 676 unfolding word_0_wi .. 677 678lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1" 679 unfolding word_1_wi .. 680 681lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1" 682 by (simp add: wi_hom_syms) 683 684lemma word_of_int_numeral [simp] : "(word_of_int (numeral bin) :: 'a::len0 word) = numeral bin" 685 by (simp only: word_numeral_alt) 686 687lemma word_of_int_neg_numeral [simp]: 688 "(word_of_int (- numeral bin) :: 'a::len0 word) = - numeral bin" 689 by (simp only: word_numeral_alt wi_hom_syms) 690 691lemma word_int_case_wi: 692 "word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ LENGTH('b::len0))" 693 by (simp add: word_int_case_def word_uint.eq_norm) 694 695lemma word_int_split: 696 "P (word_int_case f x) = 697 (\<forall>i. x = (word_of_int i :: 'b::len0 word) \<and> 0 \<le> i \<and> i < 2 ^ LENGTH('b) \<longrightarrow> P (f i))" 698 by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial) 699 700lemma word_int_split_asm: 701 "P (word_int_case f x) = 702 (\<nexists>n. x = (word_of_int n :: 'b::len0 word) \<and> 0 \<le> n \<and> n < 2 ^ LENGTH('b::len0) \<and> \<not> P (f n))" 703 by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial) 704 705lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq] 706lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq] 707 708lemma uint_range_size: "0 \<le> uint w \<and> uint w < 2 ^ size w" 709 unfolding word_size by (rule uint_range') 710 711lemma sint_range_size: "- (2 ^ (size w - Suc 0)) \<le> sint w \<and> sint w < 2 ^ (size w - Suc 0)" 712 unfolding word_size by (rule sint_range') 713 714lemma sint_above_size: "2 ^ (size w - 1) \<le> x \<Longrightarrow> sint w < x" 715 for w :: "'a::len word" 716 unfolding word_size by (rule less_le_trans [OF sint_lt]) 717 718lemma sint_below_size: "x \<le> - (2 ^ (size w - 1)) \<Longrightarrow> x \<le> sint w" 719 for w :: "'a::len word" 720 unfolding word_size by (rule order_trans [OF _ sint_ge]) 721 722 723subsection \<open>Testing bits\<close> 724 725lemma test_bit_eq_iff: "test_bit u = test_bit v \<longleftrightarrow> u = v" 726 for u v :: "'a::len0 word" 727 unfolding word_test_bit_def by (simp add: bin_nth_eq_iff) 728 729lemma test_bit_size [rule_format] : "w !! n \<longrightarrow> n < size w" 730 for w :: "'a::len0 word" 731 apply (unfold word_test_bit_def) 732 apply (subst word_ubin.norm_Rep [symmetric]) 733 apply (simp only: nth_bintr word_size) 734 apply fast 735 done 736 737lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). x !! n = y !! n)" 738 for x y :: "'a::len0 word" 739 unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric] 740 by (metis test_bit_size [unfolded word_size]) 741 742lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> u !! n = v !! n) \<Longrightarrow> u = v" 743 for u :: "'a::len0 word" 744 by (simp add: word_size word_eq_iff) 745 746lemma word_eqD: "u = v \<Longrightarrow> u !! x = v !! x" 747 for u v :: "'a::len0 word" 748 by simp 749 750lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bin_nth (uint w) n" 751 by (simp add: word_test_bit_def word_size nth_bintr [symmetric]) 752 753lemmas test_bit_bin = test_bit_bin' [unfolded word_size] 754 755lemma bin_nth_uint_imp: "bin_nth (uint w) n \<Longrightarrow> n < LENGTH('a)" 756 for w :: "'a::len0 word" 757 apply (rule nth_bintr [THEN iffD1, THEN conjunct1]) 758 apply (subst word_ubin.norm_Rep) 759 apply assumption 760 done 761 762lemma bin_nth_sint: 763 "LENGTH('a) \<le> n \<Longrightarrow> 764 bin_nth (sint w) n = bin_nth (sint w) (LENGTH('a) - 1)" 765 for w :: "'a::len word" 766 apply (subst word_sbin.norm_Rep [symmetric]) 767 apply (auto simp add: nth_sbintr) 768 done 769 770\<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close> 771lemma td_bl: 772 "type_definition 773 (to_bl :: 'a::len0 word \<Rightarrow> bool list) 774 of_bl 775 {bl. length bl = LENGTH('a)}" 776 apply (unfold type_definition_def of_bl_def to_bl_def) 777 apply (simp add: word_ubin.eq_norm) 778 apply safe 779 apply (drule sym) 780 apply simp 781 done 782 783interpretation word_bl: 784 type_definition 785 "to_bl :: 'a::len0 word \<Rightarrow> bool list" 786 of_bl 787 "{bl. length bl = LENGTH('a::len0)}" 788 by (fact td_bl) 789 790lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff] 791 792lemma word_size_bl: "size w = size (to_bl w)" 793 by (auto simp: word_size) 794 795lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)" 796 by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq]) 797 798lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)" 799 by (simp add: word_reverse_def word_bl.Abs_inverse) 800 801lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w" 802 by (simp add: word_reverse_def word_bl.Abs_inverse) 803 804lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w" 805 by (metis word_rev_rev) 806 807lemma word_rev_gal': "u = word_reverse w \<Longrightarrow> w = word_reverse u" 808 by simp 809 810lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)" 811 for x :: "'a::len word" 812 unfolding word_bl_Rep' by (rule len_gt_0) 813 814lemma bl_not_Nil [iff]: "to_bl x \<noteq> []" 815 for x :: "'a::len word" 816 by (fact length_bl_gt_0 [unfolded length_greater_0_conv]) 817 818lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0" 819 for x :: "'a::len word" 820 by (fact length_bl_gt_0 [THEN gr_implies_not0]) 821 822lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)" 823 apply (unfold to_bl_def sint_uint) 824 apply (rule trans [OF _ bl_sbin_sign]) 825 apply simp 826 done 827 828lemma of_bl_drop': 829 "lend = length bl - LENGTH('a::len0) \<Longrightarrow> 830 of_bl (drop lend bl) = (of_bl bl :: 'a word)" 831 by (auto simp: of_bl_def trunc_bl2bin [symmetric]) 832 833lemma test_bit_of_bl: 834 "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)" 835 by (auto simp add: of_bl_def word_test_bit_def word_size 836 word_ubin.eq_norm nth_bintr bin_nth_of_bl) 837 838lemma no_of_bl: "(numeral bin ::'a::len0 word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))" 839 by (simp add: of_bl_def) 840 841lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)" 842 by (auto simp: word_size to_bl_def) 843 844lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w" 845 by (simp add: uint_bl word_size) 846 847lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (LENGTH('a)) bin" 848 by (auto simp: uint_bl word_ubin.eq_norm word_size) 849 850lemma to_bl_numeral [simp]: 851 "to_bl (numeral bin::'a::len0 word) = 852 bin_to_bl (LENGTH('a)) (numeral bin)" 853 unfolding word_numeral_alt by (rule to_bl_of_bin) 854 855lemma to_bl_neg_numeral [simp]: 856 "to_bl (- numeral bin::'a::len0 word) = 857 bin_to_bl (LENGTH('a)) (- numeral bin)" 858 unfolding word_neg_numeral_alt by (rule to_bl_of_bin) 859 860lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w" 861 by (simp add: uint_bl word_size) 862 863lemma uint_bl_bin: "bl_to_bin (bin_to_bl (LENGTH('a)) (uint x)) = uint x" 864 for x :: "'a::len0 word" 865 by (rule trans [OF bin_bl_bin word_ubin.norm_Rep]) 866 867\<comment> \<open>naturals\<close> 868lemma uints_unats: "uints n = int ` unats n" 869 apply (unfold unats_def uints_num) 870 apply safe 871 apply (rule_tac image_eqI) 872 apply (erule_tac nat_0_le [symmetric]) 873 by auto 874 875lemma unats_uints: "unats n = nat ` uints n" 876 by (auto simp: uints_unats image_iff) 877 878lemmas bintr_num = 879 word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b 880lemmas sbintr_num = 881 word_sbin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b 882 883lemma num_of_bintr': 884 "bintrunc (LENGTH('a::len0)) (numeral a) = (numeral b) \<Longrightarrow> 885 numeral a = (numeral b :: 'a word)" 886 unfolding bintr_num by (erule subst, simp) 887 888lemma num_of_sbintr': 889 "sbintrunc (LENGTH('a::len) - 1) (numeral a) = (numeral b) \<Longrightarrow> 890 numeral a = (numeral b :: 'a word)" 891 unfolding sbintr_num by (erule subst, simp) 892 893lemma num_abs_bintr: 894 "(numeral x :: 'a word) = 895 word_of_int (bintrunc (LENGTH('a::len0)) (numeral x))" 896 by (simp only: word_ubin.Abs_norm word_numeral_alt) 897 898lemma num_abs_sbintr: 899 "(numeral x :: 'a word) = 900 word_of_int (sbintrunc (LENGTH('a::len) - 1) (numeral x))" 901 by (simp only: word_sbin.Abs_norm word_numeral_alt) 902 903text \<open> 904 \<open>cast\<close> -- note, no arg for new length, as it's determined by type of result, 905 thus in \<open>cast w = w\<close>, the type means cast to length of \<open>w\<close>! 906\<close> 907 908lemma ucast_id: "ucast w = w" 909 by (auto simp: ucast_def) 910 911lemma scast_id: "scast w = w" 912 by (auto simp: scast_def) 913 914lemma ucast_bl: "ucast w = of_bl (to_bl w)" 915 by (auto simp: ucast_def of_bl_def uint_bl word_size) 916 917lemma nth_ucast: "(ucast w::'a::len0 word) !! n = (w !! n \<and> n < LENGTH('a))" 918 by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size) 919 (fast elim!: bin_nth_uint_imp) 920 921\<comment> \<open>literal u(s)cast\<close> 922lemma ucast_bintr [simp]: 923 "ucast (numeral w :: 'a::len0 word) = 924 word_of_int (bintrunc (LENGTH('a)) (numeral w))" 925 by (simp add: ucast_def) 926 927(* TODO: neg_numeral *) 928 929lemma scast_sbintr [simp]: 930 "scast (numeral w ::'a::len word) = 931 word_of_int (sbintrunc (LENGTH('a) - Suc 0) (numeral w))" 932 by (simp add: scast_def) 933 934lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = LENGTH('a)" 935 unfolding source_size_def word_size Let_def .. 936 937lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = LENGTH('b)" 938 unfolding target_size_def word_size Let_def .. 939 940lemma is_down: "is_down c \<longleftrightarrow> LENGTH('b) \<le> LENGTH('a)" 941 for c :: "'a::len0 word \<Rightarrow> 'b::len0 word" 942 by (simp only: is_down_def source_size target_size) 943 944lemma is_up: "is_up c \<longleftrightarrow> LENGTH('a) \<le> LENGTH('b)" 945 for c :: "'a::len0 word \<Rightarrow> 'b::len0 word" 946 by (simp only: is_up_def source_size target_size) 947 948lemmas is_up_down = trans [OF is_up is_down [symmetric]] 949 950lemma down_cast_same [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc = scast" 951 apply (unfold is_down) 952 apply safe 953 apply (rule ext) 954 apply (unfold ucast_def scast_def uint_sint) 955 apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 956 apply simp 957 done 958 959lemma word_rev_tf: 960 "to_bl (of_bl bl::'a::len0 word) = 961 rev (takefill False (LENGTH('a)) (rev bl))" 962 by (auto simp: of_bl_def uint_bl bl_bin_bl_rtf word_ubin.eq_norm word_size) 963 964lemma word_rep_drop: 965 "to_bl (of_bl bl::'a::len0 word) = 966 replicate (LENGTH('a) - length bl) False @ 967 drop (length bl - LENGTH('a)) bl" 968 by (simp add: word_rev_tf takefill_alt rev_take) 969 970lemma to_bl_ucast: 971 "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) = 972 replicate (LENGTH('a) - LENGTH('b)) False @ 973 drop (LENGTH('b) - LENGTH('a)) (to_bl w)" 974 apply (unfold ucast_bl) 975 apply (rule trans) 976 apply (rule word_rep_drop) 977 apply simp 978 done 979 980lemma ucast_up_app [OF refl]: 981 "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow> 982 to_bl (uc w) = replicate n False @ (to_bl w)" 983 by (auto simp add : source_size target_size to_bl_ucast) 984 985lemma ucast_down_drop [OF refl]: 986 "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 987 to_bl (uc w) = drop n (to_bl w)" 988 by (auto simp add : source_size target_size to_bl_ucast) 989 990lemma scast_down_drop [OF refl]: 991 "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow> 992 to_bl (sc w) = drop n (to_bl w)" 993 apply (subgoal_tac "sc = ucast") 994 apply safe 995 apply simp 996 apply (erule ucast_down_drop) 997 apply (rule down_cast_same [symmetric]) 998 apply (simp add : source_size target_size is_down) 999 done 1000 1001lemma sint_up_scast [OF refl]: "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w" 1002 apply (unfold is_up) 1003 apply safe 1004 apply (simp add: scast_def word_sbin.eq_norm) 1005 apply (rule box_equals) 1006 prefer 3 1007 apply (rule word_sbin.norm_Rep) 1008 apply (rule sbintrunc_sbintrunc_l) 1009 defer 1010 apply (subst word_sbin.norm_Rep) 1011 apply (rule refl) 1012 apply simp 1013 done 1014 1015lemma uint_up_ucast [OF refl]: "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w" 1016 apply (unfold is_up) 1017 apply safe 1018 apply (rule bin_eqI) 1019 apply (fold word_test_bit_def) 1020 apply (auto simp add: nth_ucast) 1021 apply (auto simp add: test_bit_bin) 1022 done 1023 1024lemma ucast_up_ucast [OF refl]: "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w" 1025 apply (simp (no_asm) add: ucast_def) 1026 apply (clarsimp simp add: uint_up_ucast) 1027 done 1028 1029lemma scast_up_scast [OF refl]: "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w" 1030 apply (simp (no_asm) add: scast_def) 1031 apply (clarsimp simp add: sint_up_scast) 1032 done 1033 1034lemma ucast_of_bl_up [OF refl]: "w = of_bl bl \<Longrightarrow> size bl \<le> size w \<Longrightarrow> ucast w = of_bl bl" 1035 by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI) 1036 1037lemmas ucast_up_ucast_id = trans [OF ucast_up_ucast ucast_id] 1038lemmas scast_up_scast_id = trans [OF scast_up_scast scast_id] 1039 1040lemmas isduu = is_up_down [where c = "ucast", THEN iffD2] 1041lemmas isdus = is_up_down [where c = "scast", THEN iffD2] 1042lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id] 1043lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id] 1044 1045lemma up_ucast_surj: 1046 "is_up (ucast :: 'b::len0 word \<Rightarrow> 'a::len0 word) \<Longrightarrow> 1047 surj (ucast :: 'a word \<Rightarrow> 'b word)" 1048 by (rule surjI) (erule ucast_up_ucast_id) 1049 1050lemma up_scast_surj: 1051 "is_up (scast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow> 1052 surj (scast :: 'a word \<Rightarrow> 'b word)" 1053 by (rule surjI) (erule scast_up_scast_id) 1054 1055lemma down_scast_inj: 1056 "is_down (scast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow> 1057 inj_on (ucast :: 'a word \<Rightarrow> 'b word) A" 1058 by (rule inj_on_inverseI, erule scast_down_scast_id) 1059 1060lemma down_ucast_inj: 1061 "is_down (ucast :: 'b::len0 word \<Rightarrow> 'a::len0 word) \<Longrightarrow> 1062 inj_on (ucast :: 'a word \<Rightarrow> 'b word) A" 1063 by (rule inj_on_inverseI) (erule ucast_down_ucast_id) 1064 1065lemma of_bl_append_same: "of_bl (X @ to_bl w) = w" 1066 by (rule word_bl.Rep_eqD) (simp add: word_rep_drop) 1067 1068lemma ucast_down_wi [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (word_of_int x) = word_of_int x" 1069 apply (unfold is_down) 1070 apply (clarsimp simp add: ucast_def word_ubin.eq_norm) 1071 apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 1072 apply (erule bintrunc_bintrunc_ge) 1073 done 1074 1075lemma ucast_down_no [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (numeral bin) = numeral bin" 1076 unfolding word_numeral_alt by clarify (rule ucast_down_wi) 1077 1078lemma ucast_down_bl [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl" 1079 unfolding of_bl_def by clarify (erule ucast_down_wi) 1080 1081lemmas slice_def' = slice_def [unfolded word_size] 1082lemmas test_bit_def' = word_test_bit_def [THEN fun_cong] 1083 1084lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def 1085 1086 1087subsection \<open>Word Arithmetic\<close> 1088 1089lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b" 1090 by (fact word_less_def) 1091 1092lemma signed_linorder: "class.linorder word_sle word_sless" 1093 by standard (auto simp: word_sle_def word_sless_def) 1094 1095interpretation signed: linorder "word_sle" "word_sless" 1096 by (rule signed_linorder) 1097 1098lemma udvdI: "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b" 1099 by (auto simp: udvd_def) 1100 1101lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b 1102lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b 1103lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b 1104lemmas word_le_no [simp] = word_le_def [of "numeral a" "numeral b"] for a b 1105lemmas word_sless_no [simp] = word_sless_def [of "numeral a" "numeral b"] for a b 1106lemmas word_sle_no [simp] = word_sle_def [of "numeral a" "numeral b"] for a b 1107 1108lemma word_m1_wi: "- 1 = word_of_int (- 1)" 1109 by (simp add: word_neg_numeral_alt [of Num.One]) 1110 1111lemma word_0_bl [simp]: "of_bl [] = 0" 1112 by (simp add: of_bl_def) 1113 1114lemma word_1_bl: "of_bl [True] = 1" 1115 by (simp add: of_bl_def bl_to_bin_def) 1116 1117lemma uint_eq_0 [simp]: "uint 0 = 0" 1118 unfolding word_0_wi word_ubin.eq_norm by simp 1119 1120lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0" 1121 by (simp add: of_bl_def bl_to_bin_rep_False) 1122 1123lemma to_bl_0 [simp]: "to_bl (0::'a::len0 word) = replicate (LENGTH('a)) False" 1124 by (simp add: uint_bl word_size bin_to_bl_zero) 1125 1126lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0" 1127 by (simp add: word_uint_eq_iff) 1128 1129lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0" 1130 by (auto simp: unat_def nat_eq_iff uint_0_iff) 1131 1132lemma unat_0 [simp]: "unat 0 = 0" 1133 by (auto simp: unat_def) 1134 1135lemma size_0_same': "size w = 0 \<Longrightarrow> w = v" 1136 for v w :: "'a::len0 word" 1137 apply (unfold word_size) 1138 apply (rule box_equals) 1139 defer 1140 apply (rule word_uint.Rep_inverse)+ 1141 apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 1142 apply simp 1143 done 1144 1145lemmas size_0_same = size_0_same' [unfolded word_size] 1146 1147lemmas unat_eq_0 = unat_0_iff 1148lemmas unat_eq_zero = unat_0_iff 1149 1150lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0" 1151 by (auto simp: unat_0_iff [symmetric]) 1152 1153lemma ucast_0 [simp]: "ucast 0 = 0" 1154 by (simp add: ucast_def) 1155 1156lemma sint_0 [simp]: "sint 0 = 0" 1157 by (simp add: sint_uint) 1158 1159lemma scast_0 [simp]: "scast 0 = 0" 1160 by (simp add: scast_def) 1161 1162lemma sint_n1 [simp] : "sint (- 1) = - 1" 1163 by (simp only: word_m1_wi word_sbin.eq_norm) simp 1164 1165lemma scast_n1 [simp]: "scast (- 1) = - 1" 1166 by (simp add: scast_def) 1167 1168lemma uint_1 [simp]: "uint (1::'a::len word) = 1" 1169 by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4)) 1170 1171lemma unat_1 [simp]: "unat (1::'a::len word) = 1" 1172 by (simp add: unat_def) 1173 1174lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" 1175 by (simp add: ucast_def) 1176 1177\<comment> \<open>now, to get the weaker results analogous to \<open>word_div\<close>/\<open>mod_def\<close>\<close> 1178 1179 1180subsection \<open>Transferring goals from words to ints\<close> 1181 1182lemma word_ths: 1183 shows word_succ_p1: "word_succ a = a + 1" 1184 and word_pred_m1: "word_pred a = a - 1" 1185 and word_pred_succ: "word_pred (word_succ a) = a" 1186 and word_succ_pred: "word_succ (word_pred a) = a" 1187 and word_mult_succ: "word_succ a * b = b + a * b" 1188 by (transfer, simp add: algebra_simps)+ 1189 1190lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y" 1191 by simp 1192 1193lemma uint_word_ariths: 1194 fixes a b :: "'a::len0 word" 1195 shows "uint (a + b) = (uint a + uint b) mod 2 ^ LENGTH('a::len0)" 1196 and "uint (a - b) = (uint a - uint b) mod 2 ^ LENGTH('a)" 1197 and "uint (a * b) = uint a * uint b mod 2 ^ LENGTH('a)" 1198 and "uint (- a) = - uint a mod 2 ^ LENGTH('a)" 1199 and "uint (word_succ a) = (uint a + 1) mod 2 ^ LENGTH('a)" 1200 and "uint (word_pred a) = (uint a - 1) mod 2 ^ LENGTH('a)" 1201 and "uint (0 :: 'a word) = 0 mod 2 ^ LENGTH('a)" 1202 and "uint (1 :: 'a word) = 1 mod 2 ^ LENGTH('a)" 1203 by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]]) 1204 1205lemma uint_word_arith_bintrs: 1206 fixes a b :: "'a::len0 word" 1207 shows "uint (a + b) = bintrunc (LENGTH('a)) (uint a + uint b)" 1208 and "uint (a - b) = bintrunc (LENGTH('a)) (uint a - uint b)" 1209 and "uint (a * b) = bintrunc (LENGTH('a)) (uint a * uint b)" 1210 and "uint (- a) = bintrunc (LENGTH('a)) (- uint a)" 1211 and "uint (word_succ a) = bintrunc (LENGTH('a)) (uint a + 1)" 1212 and "uint (word_pred a) = bintrunc (LENGTH('a)) (uint a - 1)" 1213 and "uint (0 :: 'a word) = bintrunc (LENGTH('a)) 0" 1214 and "uint (1 :: 'a word) = bintrunc (LENGTH('a)) 1" 1215 by (simp_all add: uint_word_ariths bintrunc_mod2p) 1216 1217lemma sint_word_ariths: 1218 fixes a b :: "'a::len word" 1219 shows "sint (a + b) = sbintrunc (LENGTH('a) - 1) (sint a + sint b)" 1220 and "sint (a - b) = sbintrunc (LENGTH('a) - 1) (sint a - sint b)" 1221 and "sint (a * b) = sbintrunc (LENGTH('a) - 1) (sint a * sint b)" 1222 and "sint (- a) = sbintrunc (LENGTH('a) - 1) (- sint a)" 1223 and "sint (word_succ a) = sbintrunc (LENGTH('a) - 1) (sint a + 1)" 1224 and "sint (word_pred a) = sbintrunc (LENGTH('a) - 1) (sint a - 1)" 1225 and "sint (0 :: 'a word) = sbintrunc (LENGTH('a) - 1) 0" 1226 and "sint (1 :: 'a word) = sbintrunc (LENGTH('a) - 1) 1" 1227 apply (simp_all only: word_sbin.inverse_norm [symmetric]) 1228 apply (simp_all add: wi_hom_syms) 1229 apply transfer apply simp 1230 apply transfer apply simp 1231 done 1232 1233lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]] 1234lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]] 1235 1236lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)" 1237 unfolding word_pred_m1 by simp 1238 1239lemma succ_pred_no [simp]: 1240 "word_succ (numeral w) = numeral w + 1" 1241 "word_pred (numeral w) = numeral w - 1" 1242 "word_succ (- numeral w) = - numeral w + 1" 1243 "word_pred (- numeral w) = - numeral w - 1" 1244 by (simp_all add: word_succ_p1 word_pred_m1) 1245 1246lemma word_sp_01 [simp]: 1247 "word_succ (- 1) = 0 \<and> word_succ 0 = 1 \<and> word_pred 0 = - 1 \<and> word_pred 1 = 0" 1248 by (simp_all add: word_succ_p1 word_pred_m1) 1249 1250\<comment> \<open>alternative approach to lifting arithmetic equalities\<close> 1251lemma word_of_int_Ex: "\<exists>y. x = word_of_int y" 1252 by (rule_tac x="uint x" in exI) simp 1253 1254 1255subsection \<open>Order on fixed-length words\<close> 1256 1257lemma word_zero_le [simp]: "0 \<le> y" 1258 for y :: "'a::len0 word" 1259 unfolding word_le_def by auto 1260 1261lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *) 1262 by (simp only: word_le_def word_pred_0_n1 word_uint.eq_norm m1mod2k) auto 1263 1264lemma word_n1_ge [simp]: "y \<le> -1" 1265 for y :: "'a::len0 word" 1266 by (simp only: word_le_def word_m1_wi word_uint.eq_norm m1mod2k) auto 1267 1268lemmas word_not_simps [simp] = 1269 word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] 1270 1271lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y" 1272 for y :: "'a::len0 word" 1273 by (simp add: less_le) 1274 1275lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y 1276 1277lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b" 1278 by (auto simp add: word_sle_def word_sless_def less_le) 1279 1280lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b" 1281 unfolding unat_def word_le_def 1282 by (rule nat_le_eq_zle [symmetric]) simp 1283 1284lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b" 1285 unfolding unat_def word_less_alt 1286 by (rule nat_less_eq_zless [symmetric]) simp 1287 1288lemmas unat_mono = word_less_nat_alt [THEN iffD1] 1289 1290instance word :: (len) wellorder 1291proof 1292 fix P :: "'a word \<Rightarrow> bool" and a 1293 assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)" 1294 have "wf (measure unat)" .. 1295 moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat" 1296 by (auto simp add: word_less_nat_alt) 1297 ultimately have "wf {(a, b :: ('a::len) word). a < b}" 1298 by (rule wf_subset) 1299 then show "P a" using * 1300 by induction blast 1301qed 1302 1303lemma wi_less: 1304 "(word_of_int n < (word_of_int m :: 'a::len0 word)) = 1305 (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))" 1306 unfolding word_less_alt by (simp add: word_uint.eq_norm) 1307 1308lemma wi_le: 1309 "(word_of_int n \<le> (word_of_int m :: 'a::len0 word)) = 1310 (n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))" 1311 unfolding word_le_def by (simp add: word_uint.eq_norm) 1312 1313lemma udvd_nat_alt: "a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. unat b = n * unat a)" 1314 apply (unfold udvd_def) 1315 apply safe 1316 apply (simp add: unat_def nat_mult_distrib) 1317 apply (simp add: uint_nat) 1318 apply (rule exI) 1319 apply safe 1320 prefer 2 1321 apply (erule notE) 1322 apply (rule refl) 1323 apply force 1324 done 1325 1326lemma udvd_iff_dvd: "x udvd y \<longleftrightarrow> unat x dvd unat y" 1327 unfolding dvd_def udvd_nat_alt by force 1328 1329lemma unat_minus_one: 1330 assumes "w \<noteq> 0" 1331 shows "unat (w - 1) = unat w - 1" 1332proof - 1333 have "0 \<le> uint w" by (fact uint_nonnegative) 1334 moreover from assms have "0 \<noteq> uint w" 1335 by (simp add: uint_0_iff) 1336 ultimately have "1 \<le> uint w" 1337 by arith 1338 from uint_lt2p [of w] have "uint w - 1 < 2 ^ LENGTH('a)" 1339 by arith 1340 with \<open>1 \<le> uint w\<close> have "(uint w - 1) mod 2 ^ LENGTH('a) = uint w - 1" 1341 by (auto intro: mod_pos_pos_trivial) 1342 with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ LENGTH('a)) = nat (uint w) - 1" 1343 by auto 1344 then show ?thesis 1345 by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq) 1346qed 1347 1348lemma measure_unat: "p \<noteq> 0 \<Longrightarrow> unat (p - 1) < unat p" 1349 by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric]) 1350 1351lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0] 1352lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0] 1353 1354lemma uint_sub_lt2p [simp]: "uint x - uint y < 2 ^ LENGTH('a)" 1355 for x :: "'a::len0 word" and y :: "'b::len0 word" 1356 using uint_ge_0 [of y] uint_lt2p [of x] by arith 1357 1358 1359subsection \<open>Conditions for the addition (etc) of two words to overflow\<close> 1360 1361lemma uint_add_lem: 1362 "(uint x + uint y < 2 ^ LENGTH('a)) = 1363 (uint (x + y) = uint x + uint y)" 1364 for x y :: "'a::len0 word" 1365 by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) 1366 1367lemma uint_mult_lem: 1368 "(uint x * uint y < 2 ^ LENGTH('a)) = 1369 (uint (x * y) = uint x * uint y)" 1370 for x y :: "'a::len0 word" 1371 by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) 1372 1373lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y" 1374 by (auto simp: uint_word_ariths intro!: trans [OF _ int_mod_lem]) 1375 1376lemma uint_add_le: "uint (x + y) \<le> uint x + uint y" 1377 unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend) 1378 1379lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y" 1380 unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p) 1381 1382lemma mod_add_if_z: 1383 "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow> 1384 (x + y) mod z = (if x + y < z then x + y else x + y - z)" 1385 for x y z :: int 1386 by (auto intro: int_mod_eq) 1387 1388lemma uint_plus_if': 1389 "uint (a + b) = 1390 (if uint a + uint b < 2 ^ LENGTH('a) then uint a + uint b 1391 else uint a + uint b - 2 ^ LENGTH('a))" 1392 for a b :: "'a::len0 word" 1393 using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths) 1394 1395lemma mod_sub_if_z: 1396 "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow> 1397 (x - y) mod z = (if y \<le> x then x - y else x - y + z)" 1398 for x y z :: int 1399 by (auto intro: int_mod_eq) 1400 1401lemma uint_sub_if': 1402 "uint (a - b) = 1403 (if uint b \<le> uint a then uint a - uint b 1404 else uint a - uint b + 2 ^ LENGTH('a))" 1405 for a b :: "'a::len0 word" 1406 using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths) 1407 1408 1409subsection \<open>Definition of \<open>uint_arith\<close>\<close> 1410 1411lemma word_of_int_inverse: 1412 "word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> uint a = r" 1413 for a :: "'a::len0 word" 1414 apply (erule word_uint.Abs_inverse' [rotated]) 1415 apply (simp add: uints_num) 1416 done 1417 1418lemma uint_split: 1419 "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<longrightarrow> P i)" 1420 for x :: "'a::len0 word" 1421 apply (fold word_int_case_def) 1422 apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial 1423 split: word_int_split) 1424 done 1425 1426lemma uint_split_asm: 1427 "P (uint x) = (\<nexists>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<and> \<not> P i)" 1428 for x :: "'a::len0 word" 1429 by (auto dest!: word_of_int_inverse 1430 simp: int_word_uint mod_pos_pos_trivial 1431 split: uint_split) 1432 1433lemmas uint_splits = uint_split uint_split_asm 1434 1435lemmas uint_arith_simps = 1436 word_le_def word_less_alt 1437 word_uint.Rep_inject [symmetric] 1438 uint_sub_if' uint_plus_if' 1439 1440\<comment> \<open>use this to stop, eg. \<open>2 ^ LENGTH(32)\<close> being simplified\<close> 1441lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d" 1442 by auto 1443 1444\<comment> \<open>\<open>uint_arith_tac\<close>: reduce to arithmetic on int, try to solve by arith\<close> 1445ML \<open> 1446fun uint_arith_simpset ctxt = 1447 ctxt addsimps @{thms uint_arith_simps} 1448 delsimps @{thms word_uint.Rep_inject} 1449 |> fold Splitter.add_split @{thms if_split_asm} 1450 |> fold Simplifier.add_cong @{thms power_False_cong} 1451 1452fun uint_arith_tacs ctxt = 1453 let 1454 fun arith_tac' n t = 1455 Arith_Data.arith_tac ctxt n t 1456 handle Cooper.COOPER _ => Seq.empty; 1457 in 1458 [ clarify_tac ctxt 1, 1459 full_simp_tac (uint_arith_simpset ctxt) 1, 1460 ALLGOALS (full_simp_tac 1461 (put_simpset HOL_ss ctxt 1462 |> fold Splitter.add_split @{thms uint_splits} 1463 |> fold Simplifier.add_cong @{thms power_False_cong})), 1464 rewrite_goals_tac ctxt @{thms word_size}, 1465 ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN 1466 REPEAT (eresolve_tac ctxt [conjE] n) THEN 1467 REPEAT (dresolve_tac ctxt @{thms word_of_int_inverse} n 1468 THEN assume_tac ctxt n 1469 THEN assume_tac ctxt n)), 1470 TRYALL arith_tac' ] 1471 end 1472 1473fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt)) 1474\<close> 1475 1476method_setup uint_arith = 1477 \<open>Scan.succeed (SIMPLE_METHOD' o uint_arith_tac)\<close> 1478 "solving word arithmetic via integers and arith" 1479 1480 1481subsection \<open>More on overflows and monotonicity\<close> 1482 1483lemma no_plus_overflow_uint_size: "x \<le> x + y \<longleftrightarrow> uint x + uint y < 2 ^ size x" 1484 for x y :: "'a::len0 word" 1485 unfolding word_size by uint_arith 1486 1487lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size] 1488 1489lemma no_ulen_sub: "x \<ge> x - y \<longleftrightarrow> uint y \<le> uint x" 1490 for x y :: "'a::len0 word" 1491 by uint_arith 1492 1493lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ LENGTH('a)" 1494 for x y :: "'a::len0 word" 1495 by (simp add: ac_simps no_olen_add) 1496 1497lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]] 1498 1499lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem] 1500lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1] 1501lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem] 1502lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def] 1503lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def] 1504lemmas word_sub_le = word_sub_le_iff [THEN iffD2] 1505 1506lemma word_less_sub1: "x \<noteq> 0 \<Longrightarrow> 1 < x \<longleftrightarrow> 0 < x - 1" 1507 for x :: "'a::len word" 1508 by uint_arith 1509 1510lemma word_le_sub1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> x \<longleftrightarrow> 0 \<le> x - 1" 1511 for x :: "'a::len word" 1512 by uint_arith 1513 1514lemma sub_wrap_lt: "x < x - z \<longleftrightarrow> x < z" 1515 for x z :: "'a::len0 word" 1516 by uint_arith 1517 1518lemma sub_wrap: "x \<le> x - z \<longleftrightarrow> z = 0 \<or> x < z" 1519 for x z :: "'a::len0 word" 1520 by uint_arith 1521 1522lemma plus_minus_not_NULL_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> x + c \<noteq> 0" 1523 for x ab c :: "'a::len0 word" 1524 by uint_arith 1525 1526lemma plus_minus_no_overflow_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> x \<le> x + c" 1527 for x ab c :: "'a::len0 word" 1528 by uint_arith 1529 1530lemma le_minus': "a + c \<le> b \<Longrightarrow> a \<le> a + c \<Longrightarrow> c \<le> b - a" 1531 for a b c :: "'a::len0 word" 1532 by uint_arith 1533 1534lemma le_plus': "a \<le> b \<Longrightarrow> c \<le> b - a \<Longrightarrow> a + c \<le> b" 1535 for a b c :: "'a::len0 word" 1536 by uint_arith 1537 1538lemmas le_plus = le_plus' [rotated] 1539 1540lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *) 1541 1542lemma word_plus_mono_right: "y \<le> z \<Longrightarrow> x \<le> x + z \<Longrightarrow> x + y \<le> x + z" 1543 for x y z :: "'a::len0 word" 1544 by uint_arith 1545 1546lemma word_less_minus_cancel: "y - x < z - x \<Longrightarrow> x \<le> z \<Longrightarrow> y < z" 1547 for x y z :: "'a::len0 word" 1548 by uint_arith 1549 1550lemma word_less_minus_mono_left: "y < z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x < z - x" 1551 for x y z :: "'a::len0 word" 1552 by uint_arith 1553 1554lemma word_less_minus_mono: "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c \<Longrightarrow> a - b < c - d" 1555 for a b c d :: "'a::len word" 1556 by uint_arith 1557 1558lemma word_le_minus_cancel: "y - x \<le> z - x \<Longrightarrow> x \<le> z \<Longrightarrow> y \<le> z" 1559 for x y z :: "'a::len0 word" 1560 by uint_arith 1561 1562lemma word_le_minus_mono_left: "y \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x \<le> z - x" 1563 for x y z :: "'a::len0 word" 1564 by uint_arith 1565 1566lemma word_le_minus_mono: 1567 "a \<le> c \<Longrightarrow> d \<le> b \<Longrightarrow> a - b \<le> a \<Longrightarrow> c - d \<le> c \<Longrightarrow> a - b \<le> c - d" 1568 for a b c d :: "'a::len word" 1569 by uint_arith 1570 1571lemma plus_le_left_cancel_wrap: "x + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> x + y' < x + y \<longleftrightarrow> y' < y" 1572 for x y y' :: "'a::len0 word" 1573 by uint_arith 1574 1575lemma plus_le_left_cancel_nowrap: "x \<le> x + y' \<Longrightarrow> x \<le> x + y \<Longrightarrow> x + y' < x + y \<longleftrightarrow> y' < y" 1576 for x y y' :: "'a::len0 word" 1577 by uint_arith 1578 1579lemma word_plus_mono_right2: "a \<le> a + b \<Longrightarrow> c \<le> b \<Longrightarrow> a \<le> a + c" 1580 for a b c :: "'a::len0 word" 1581 by uint_arith 1582 1583lemma word_less_add_right: "x < y - z \<Longrightarrow> z \<le> y \<Longrightarrow> x + z < y" 1584 for x y z :: "'a::len0 word" 1585 by uint_arith 1586 1587lemma word_less_sub_right: "x < y + z \<Longrightarrow> y \<le> x \<Longrightarrow> x - y < z" 1588 for x y z :: "'a::len0 word" 1589 by uint_arith 1590 1591lemma word_le_plus_either: "x \<le> y \<or> x \<le> z \<Longrightarrow> y \<le> y + z \<Longrightarrow> x \<le> y + z" 1592 for x y z :: "'a::len0 word" 1593 by uint_arith 1594 1595lemma word_less_nowrapI: "x < z - k \<Longrightarrow> k \<le> z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k" 1596 for x z k :: "'a::len0 word" 1597 by uint_arith 1598 1599lemma inc_le: "i < m \<Longrightarrow> i + 1 \<le> m" 1600 for i m :: "'a::len word" 1601 by uint_arith 1602 1603lemma inc_i: "1 \<le> i \<Longrightarrow> i < m \<Longrightarrow> 1 \<le> i + 1 \<and> i + 1 \<le> m" 1604 for i m :: "'a::len word" 1605 by uint_arith 1606 1607lemma udvd_incr_lem: 1608 "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow> 1609 uq = ua + n' * uint K \<Longrightarrow> up + uint K \<le> uq" 1610 apply clarsimp 1611 apply (drule less_le_mult) 1612 apply safe 1613 done 1614 1615lemma udvd_incr': 1616 "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 1617 uint q = ua + n' * uint K \<Longrightarrow> p + K \<le> q" 1618 apply (unfold word_less_alt word_le_def) 1619 apply (drule (2) udvd_incr_lem) 1620 apply (erule uint_add_le [THEN order_trans]) 1621 done 1622 1623lemma udvd_decr': 1624 "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 1625 uint q = ua + n' * uint K \<Longrightarrow> p \<le> q - K" 1626 apply (unfold word_less_alt word_le_def) 1627 apply (drule (2) udvd_incr_lem) 1628 apply (drule le_diff_eq [THEN iffD2]) 1629 apply (erule order_trans) 1630 apply (rule uint_sub_ge) 1631 done 1632 1633lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left] 1634lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left] 1635lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left] 1636 1637lemma udvd_minus_le': "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy \<le> k - z" 1638 apply (unfold udvd_def) 1639 apply clarify 1640 apply (erule (2) udvd_decr0) 1641 done 1642 1643lemma udvd_incr2_K: 1644 "p < a + s \<Longrightarrow> a \<le> a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a \<le> p \<Longrightarrow> 1645 0 < K \<Longrightarrow> p \<le> p + K \<and> p + K \<le> a + s" 1646 supply [[simproc del: linordered_ring_less_cancel_factor]] 1647 apply (unfold udvd_def) 1648 apply clarify 1649 apply (simp add: uint_arith_simps split: if_split_asm) 1650 prefer 2 1651 apply (insert uint_range' [of s])[1] 1652 apply arith 1653 apply (drule add.commute [THEN xtr1]) 1654 apply (simp add: diff_less_eq [symmetric]) 1655 apply (drule less_le_mult) 1656 apply arith 1657 apply simp 1658 done 1659 1660\<comment> \<open>links with \<open>rbl\<close> operations\<close> 1661lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))" 1662 apply (unfold word_succ_def) 1663 apply clarify 1664 apply (simp add: to_bl_of_bin) 1665 apply (simp add: to_bl_def rbl_succ) 1666 done 1667 1668lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))" 1669 apply (unfold word_pred_def) 1670 apply clarify 1671 apply (simp add: to_bl_of_bin) 1672 apply (simp add: to_bl_def rbl_pred) 1673 done 1674 1675lemma word_add_rbl: 1676 "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 1677 to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))" 1678 apply (unfold word_add_def) 1679 apply clarify 1680 apply (simp add: to_bl_of_bin) 1681 apply (simp add: to_bl_def rbl_add) 1682 done 1683 1684lemma word_mult_rbl: 1685 "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 1686 to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))" 1687 apply (unfold word_mult_def) 1688 apply clarify 1689 apply (simp add: to_bl_of_bin) 1690 apply (simp add: to_bl_def rbl_mult) 1691 done 1692 1693lemma rtb_rbl_ariths: 1694 "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys" 1695 "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys" 1696 "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs" 1697 "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs" 1698 by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl) 1699 1700 1701subsection \<open>Arithmetic type class instantiations\<close> 1702 1703lemmas word_le_0_iff [simp] = 1704 word_zero_le [THEN leD, THEN antisym_conv1] 1705 1706lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)" 1707 by (simp add: word_of_int) 1708 1709text \<open> 1710 note that \<open>iszero_def\<close> is only for class \<open>comm_semiring_1_cancel\<close>, 1711 which requires word length \<open>\<ge> 1\<close>, ie \<open>'a::len word\<close> 1712\<close> 1713lemma iszero_word_no [simp]: 1714 "iszero (numeral bin :: 'a::len word) = 1715 iszero (bintrunc (LENGTH('a)) (numeral bin))" 1716 using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0] 1717 by (simp add: iszero_def [symmetric]) 1718 1719text \<open>Use \<open>iszero\<close> to simplify equalities between word numerals.\<close> 1720 1721lemmas word_eq_numeral_iff_iszero [simp] = 1722 eq_numeral_iff_iszero [where 'a="'a::len word"] 1723 1724 1725subsection \<open>Word and nat\<close> 1726 1727lemma td_ext_unat [OF refl]: 1728 "n = LENGTH('a::len) \<Longrightarrow> 1729 td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)" 1730 apply (unfold td_ext_def' unat_def word_of_nat unats_uints) 1731 apply (auto intro!: imageI simp add : word_of_int_hom_syms) 1732 apply (erule word_uint.Abs_inverse [THEN arg_cong]) 1733 apply (simp add: int_word_uint nat_mod_distrib nat_power_eq) 1734 done 1735 1736lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm] 1737 1738interpretation word_unat: 1739 td_ext 1740 "unat::'a::len word \<Rightarrow> nat" 1741 of_nat 1742 "unats (LENGTH('a::len))" 1743 "\<lambda>i. i mod 2 ^ LENGTH('a::len)" 1744 by (rule td_ext_unat) 1745 1746lemmas td_unat = word_unat.td_thm 1747 1748lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq] 1749 1750lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))" 1751 for z :: "'a::len word" 1752 apply (unfold unats_def) 1753 apply clarsimp 1754 apply (rule xtrans, rule unat_lt2p, assumption) 1755 done 1756 1757lemma word_nchotomy: "\<forall>w :: 'a::len word. \<exists>n. w = of_nat n \<and> n < 2 ^ LENGTH('a)" 1758 apply (rule allI) 1759 apply (rule word_unat.Abs_cases) 1760 apply (unfold unats_def) 1761 apply auto 1762 done 1763 1764lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ LENGTH('a))" 1765 for w :: "'a::len word" 1766 using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric] 1767 by (auto simp add: word_unat.inverse_norm) 1768 1769lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)" 1770 unfolding word_size by (rule of_nat_eq) 1771 1772lemma of_nat_0: "of_nat m = (0::'a::len word) \<longleftrightarrow> (\<exists>q. m = q * 2 ^ LENGTH('a))" 1773 by (simp add: of_nat_eq) 1774 1775lemma of_nat_2p [simp]: "of_nat (2 ^ LENGTH('a)) = (0::'a::len word)" 1776 by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]]) 1777 1778lemma of_nat_gt_0: "of_nat k \<noteq> 0 \<Longrightarrow> 0 < k" 1779 by (cases k) auto 1780 1781lemma of_nat_neq_0: "0 < k \<Longrightarrow> k < 2 ^ LENGTH('a::len) \<Longrightarrow> of_nat k \<noteq> (0 :: 'a word)" 1782 by (auto simp add : of_nat_0) 1783 1784lemma Abs_fnat_hom_add: "of_nat a + of_nat b = of_nat (a + b)" 1785 by simp 1786 1787lemma Abs_fnat_hom_mult: "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)" 1788 by (simp add: word_of_nat wi_hom_mult) 1789 1790lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)" 1791 by (simp add: word_of_nat wi_hom_succ ac_simps) 1792 1793lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0" 1794 by simp 1795 1796lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)" 1797 by simp 1798 1799lemmas Abs_fnat_homs = 1800 Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc 1801 Abs_fnat_hom_0 Abs_fnat_hom_1 1802 1803lemma word_arith_nat_add: "a + b = of_nat (unat a + unat b)" 1804 by simp 1805 1806lemma word_arith_nat_mult: "a * b = of_nat (unat a * unat b)" 1807 by simp 1808 1809lemma word_arith_nat_Suc: "word_succ a = of_nat (Suc (unat a))" 1810 by (subst Abs_fnat_hom_Suc [symmetric]) simp 1811 1812lemma word_arith_nat_div: "a div b = of_nat (unat a div unat b)" 1813 by (simp add: word_div_def word_of_nat zdiv_int uint_nat) 1814 1815lemma word_arith_nat_mod: "a mod b = of_nat (unat a mod unat b)" 1816 by (simp add: word_mod_def word_of_nat zmod_int uint_nat) 1817 1818lemmas word_arith_nat_defs = 1819 word_arith_nat_add word_arith_nat_mult 1820 word_arith_nat_Suc Abs_fnat_hom_0 1821 Abs_fnat_hom_1 word_arith_nat_div 1822 word_arith_nat_mod 1823 1824lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y" 1825 by simp 1826 1827lemmas unat_word_ariths = word_arith_nat_defs 1828 [THEN trans [OF unat_cong unat_of_nat]] 1829 1830lemmas word_sub_less_iff = word_sub_le_iff 1831 [unfolded linorder_not_less [symmetric] Not_eq_iff] 1832 1833lemma unat_add_lem: 1834 "unat x + unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x + y) = unat x + unat y" 1835 for x y :: "'a::len word" 1836 by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem]) 1837 1838lemma unat_mult_lem: 1839 "unat x * unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x * y) = unat x * unat y" 1840 for x y :: "'a::len word" 1841 by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem]) 1842 1843lemmas unat_plus_if' = 1844 trans [OF unat_word_ariths(1) mod_nat_add, simplified] 1845 1846lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b" 1847 for a b x :: "'a::len0 word" 1848 apply (erule order_trans) 1849 apply (erule olen_add_eqv [THEN iffD1]) 1850 done 1851 1852lemmas un_ui_le = 1853 trans [OF word_le_nat_alt [symmetric] word_le_def] 1854 1855lemma unat_sub_if_size: 1856 "unat (x - y) = 1857 (if unat y \<le> unat x 1858 then unat x - unat y 1859 else unat x + 2 ^ size x - unat y)" 1860 apply (unfold word_size) 1861 apply (simp add: un_ui_le) 1862 apply (auto simp add: unat_def uint_sub_if') 1863 apply (rule nat_diff_distrib) 1864 prefer 3 1865 apply (simp add: algebra_simps) 1866 apply (rule nat_diff_distrib [THEN trans]) 1867 prefer 3 1868 apply (subst nat_add_distrib) 1869 prefer 3 1870 apply (simp add: nat_power_eq) 1871 apply auto 1872 apply uint_arith 1873 done 1874 1875lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size] 1876 1877lemma unat_div: "unat (x div y) = unat x div unat y" 1878 for x y :: " 'a::len word" 1879 apply (simp add : unat_word_ariths) 1880 apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq']) 1881 apply (rule div_le_dividend) 1882 done 1883 1884lemma unat_mod: "unat (x mod y) = unat x mod unat y" 1885 for x y :: "'a::len word" 1886 apply (clarsimp simp add : unat_word_ariths) 1887 apply (cases "unat y") 1888 prefer 2 1889 apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq']) 1890 apply (rule mod_le_divisor) 1891 apply auto 1892 done 1893 1894lemma uint_div: "uint (x div y) = uint x div uint y" 1895 for x y :: "'a::len word" 1896 by (simp add: uint_nat unat_div zdiv_int) 1897 1898lemma uint_mod: "uint (x mod y) = uint x mod uint y" 1899 for x y :: "'a::len word" 1900 by (simp add: uint_nat unat_mod zmod_int) 1901 1902text \<open>Definition of \<open>unat_arith\<close> tactic\<close> 1903 1904lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^LENGTH('a) \<longrightarrow> P n)" 1905 for x :: "'a::len word" 1906 by (auto simp: unat_of_nat) 1907 1908lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^LENGTH('a) \<and> \<not> P n)" 1909 for x :: "'a::len word" 1910 by (auto simp: unat_of_nat) 1911 1912lemmas of_nat_inverse = 1913 word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified] 1914 1915lemmas unat_splits = unat_split unat_split_asm 1916 1917lemmas unat_arith_simps = 1918 word_le_nat_alt word_less_nat_alt 1919 word_unat.Rep_inject [symmetric] 1920 unat_sub_if' unat_plus_if' unat_div unat_mod 1921 1922\<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close> 1923ML \<open> 1924fun unat_arith_simpset ctxt = 1925 ctxt addsimps @{thms unat_arith_simps} 1926 delsimps @{thms word_unat.Rep_inject} 1927 |> fold Splitter.add_split @{thms if_split_asm} 1928 |> fold Simplifier.add_cong @{thms power_False_cong} 1929 1930fun unat_arith_tacs ctxt = 1931 let 1932 fun arith_tac' n t = 1933 Arith_Data.arith_tac ctxt n t 1934 handle Cooper.COOPER _ => Seq.empty; 1935 in 1936 [ clarify_tac ctxt 1, 1937 full_simp_tac (unat_arith_simpset ctxt) 1, 1938 ALLGOALS (full_simp_tac 1939 (put_simpset HOL_ss ctxt 1940 |> fold Splitter.add_split @{thms unat_splits} 1941 |> fold Simplifier.add_cong @{thms power_False_cong})), 1942 rewrite_goals_tac ctxt @{thms word_size}, 1943 ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN 1944 REPEAT (eresolve_tac ctxt [conjE] n) THEN 1945 REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)), 1946 TRYALL arith_tac' ] 1947 end 1948 1949fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt)) 1950\<close> 1951 1952method_setup unat_arith = 1953 \<open>Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\<close> 1954 "solving word arithmetic via natural numbers and arith" 1955 1956lemma no_plus_overflow_unat_size: "x \<le> x + y \<longleftrightarrow> unat x + unat y < 2 ^ size x" 1957 for x y :: "'a::len word" 1958 unfolding word_size by unat_arith 1959 1960lemmas no_olen_add_nat = 1961 no_plus_overflow_unat_size [unfolded word_size] 1962 1963lemmas unat_plus_simple = 1964 trans [OF no_olen_add_nat unat_add_lem] 1965 1966lemma word_div_mult: "0 < y \<Longrightarrow> unat x * unat y < 2 ^ LENGTH('a) \<Longrightarrow> x * y div y = x" 1967 for x y :: "'a::len word" 1968 apply unat_arith 1969 apply clarsimp 1970 apply (subst unat_mult_lem [THEN iffD1]) 1971 apply auto 1972 done 1973 1974lemma div_lt': "i \<le> k div x \<Longrightarrow> unat i * unat x < 2 ^ LENGTH('a)" 1975 for i k x :: "'a::len word" 1976 apply unat_arith 1977 apply clarsimp 1978 apply (drule mult_le_mono1) 1979 apply (erule order_le_less_trans) 1980 apply (rule xtr7 [OF unat_lt2p div_mult_le]) 1981 done 1982 1983lemmas div_lt'' = order_less_imp_le [THEN div_lt'] 1984 1985lemma div_lt_mult: "i < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k" 1986 for i k x :: "'a::len word" 1987 apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]]) 1988 apply (simp add: unat_arith_simps) 1989 apply (drule (1) mult_less_mono1) 1990 apply (erule order_less_le_trans) 1991 apply (rule div_mult_le) 1992 done 1993 1994lemma div_le_mult: "i \<le> k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x \<le> k" 1995 for i k x :: "'a::len word" 1996 apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]]) 1997 apply (simp add: unat_arith_simps) 1998 apply (drule mult_le_mono1) 1999 apply (erule order_trans) 2000 apply (rule div_mult_le) 2001 done 2002 2003lemma div_lt_uint': "i \<le> k div x \<Longrightarrow> uint i * uint x < 2 ^ LENGTH('a)" 2004 for i k x :: "'a::len word" 2005 apply (unfold uint_nat) 2006 apply (drule div_lt') 2007 apply (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power) 2008 done 2009 2010lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint'] 2011 2012lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ LENGTH('a)" 2013 for x y z :: "'a::len0 word" 2014 apply (rule exI) 2015 apply (rule conjI) 2016 apply (rule zadd_diff_inverse) 2017 apply uint_arith 2018 done 2019 2020lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab] 2021 2022lemmas plus_minus_no_overflow = 2023 order_less_imp_le [THEN plus_minus_no_overflow_ab] 2024 2025lemmas mcs = word_less_minus_cancel word_less_minus_mono_left 2026 word_le_minus_cancel word_le_minus_mono_left 2027 2028lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x 2029lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x 2030lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x 2031 2032lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse] 2033 2034lemmas thd = times_div_less_eq_dividend 2035 2036lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle 2037 2038lemma word_mod_div_equality: "(n div b) * b + (n mod b) = n" 2039 for n b :: "'a::len word" 2040 apply (unfold word_less_nat_alt word_arith_nat_defs) 2041 apply (cut_tac y="unat b" in gt_or_eq_0) 2042 apply (erule disjE) 2043 apply (simp only: div_mult_mod_eq uno_simps Word.word_unat.Rep_inverse) 2044 apply simp 2045 done 2046 2047lemma word_div_mult_le: "a div b * b \<le> a" 2048 for a b :: "'a::len word" 2049 apply (unfold word_le_nat_alt word_arith_nat_defs) 2050 apply (cut_tac y="unat b" in gt_or_eq_0) 2051 apply (erule disjE) 2052 apply (simp only: div_mult_le uno_simps Word.word_unat.Rep_inverse) 2053 apply simp 2054 done 2055 2056lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < n" 2057 for m n :: "'a::len word" 2058 apply (simp only: word_less_nat_alt word_arith_nat_defs) 2059 apply (auto simp: uno_simps) 2060 done 2061 2062lemma word_of_int_power_hom: "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)" 2063 by (induct n) (simp_all add: wi_hom_mult [symmetric]) 2064 2065lemma word_arith_power_alt: "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)" 2066 by (simp add : word_of_int_power_hom [symmetric]) 2067 2068lemma of_bl_length_less: 2069 "length x = k \<Longrightarrow> k < LENGTH('a) \<Longrightarrow> (of_bl x :: 'a::len word) < 2 ^ k" 2070 apply (unfold of_bl_def word_less_alt word_numeral_alt) 2071 apply safe 2072 apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 2073 del: word_of_int_numeral) 2074 apply (simp add: mod_pos_pos_trivial) 2075 apply (subst mod_pos_pos_trivial) 2076 apply (rule bl_to_bin_ge0) 2077 apply (rule order_less_trans) 2078 apply (rule bl_to_bin_lt2p) 2079 apply simp 2080 apply (rule bl_to_bin_lt2p) 2081 done 2082 2083lemma unatSuc: "1 + n \<noteq> 0 \<Longrightarrow> unat (1 + n) = Suc (unat n)" 2084 for n :: "'a::len word" 2085 by unat_arith 2086 2087 2088subsection \<open>Cardinality, finiteness of set of words\<close> 2089 2090instance word :: (len0) finite 2091 by standard (simp add: type_definition.univ [OF type_definition_word]) 2092 2093lemma card_word: "CARD('a word) = 2 ^ LENGTH('a::len0)" 2094 by (simp add: type_definition.card [OF type_definition_word] nat_power_eq) 2095 2096lemma card_word_size: "CARD('a word) = 2 ^ size x" 2097 for x :: "'a::len0 word" 2098 unfolding word_size by (rule card_word) 2099 2100 2101subsection \<open>Bitwise Operations on Words\<close> 2102 2103lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)" 2104 by simp 2105 2106lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or 2107 2108\<comment> \<open>following definitions require both arithmetic and bit-wise word operations\<close> 2109 2110\<comment> \<open>to get \<open>word_no_log_defs\<close> from \<open>word_log_defs\<close>, using \<open>bin_log_bintrs\<close>\<close> 2111lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1], 2112 folded word_ubin.eq_norm, THEN eq_reflection] 2113 2114\<comment> \<open>the binary operations only\<close> (* BH: why is this needed? *) 2115lemmas word_log_binary_defs = 2116 word_and_def word_or_def word_xor_def 2117 2118lemma word_wi_log_defs: 2119 "NOT (word_of_int a) = word_of_int (NOT a)" 2120 "word_of_int a AND word_of_int b = word_of_int (a AND b)" 2121 "word_of_int a OR word_of_int b = word_of_int (a OR b)" 2122 "word_of_int a XOR word_of_int b = word_of_int (a XOR b)" 2123 by (transfer, rule refl)+ 2124 2125lemma word_no_log_defs [simp]: 2126 "NOT (numeral a) = word_of_int (NOT (numeral a))" 2127 "NOT (- numeral a) = word_of_int (NOT (- numeral a))" 2128 "numeral a AND numeral b = word_of_int (numeral a AND numeral b)" 2129 "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)" 2130 "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)" 2131 "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)" 2132 "numeral a OR numeral b = word_of_int (numeral a OR numeral b)" 2133 "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)" 2134 "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)" 2135 "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)" 2136 "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)" 2137 "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)" 2138 "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)" 2139 "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)" 2140 by (transfer, rule refl)+ 2141 2142text \<open>Special cases for when one of the arguments equals 1.\<close> 2143 2144lemma word_bitwise_1_simps [simp]: 2145 "NOT (1::'a::len0 word) = -2" 2146 "1 AND numeral b = word_of_int (1 AND numeral b)" 2147 "1 AND - numeral b = word_of_int (1 AND - numeral b)" 2148 "numeral a AND 1 = word_of_int (numeral a AND 1)" 2149 "- numeral a AND 1 = word_of_int (- numeral a AND 1)" 2150 "1 OR numeral b = word_of_int (1 OR numeral b)" 2151 "1 OR - numeral b = word_of_int (1 OR - numeral b)" 2152 "numeral a OR 1 = word_of_int (numeral a OR 1)" 2153 "- numeral a OR 1 = word_of_int (- numeral a OR 1)" 2154 "1 XOR numeral b = word_of_int (1 XOR numeral b)" 2155 "1 XOR - numeral b = word_of_int (1 XOR - numeral b)" 2156 "numeral a XOR 1 = word_of_int (numeral a XOR 1)" 2157 "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)" 2158 by (transfer, simp)+ 2159 2160text \<open>Special cases for when one of the arguments equals -1.\<close> 2161 2162lemma word_bitwise_m1_simps [simp]: 2163 "NOT (-1::'a::len0 word) = 0" 2164 "(-1::'a::len0 word) AND x = x" 2165 "x AND (-1::'a::len0 word) = x" 2166 "(-1::'a::len0 word) OR x = -1" 2167 "x OR (-1::'a::len0 word) = -1" 2168 " (-1::'a::len0 word) XOR x = NOT x" 2169 "x XOR (-1::'a::len0 word) = NOT x" 2170 by (transfer, simp)+ 2171 2172lemma uint_or: "uint (x OR y) = uint x OR uint y" 2173 by (transfer, simp add: bin_trunc_ao) 2174 2175lemma uint_and: "uint (x AND y) = uint x AND uint y" 2176 by (transfer, simp add: bin_trunc_ao) 2177 2178lemma test_bit_wi [simp]: 2179 "(word_of_int x :: 'a::len0 word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bin_nth x n" 2180 by (simp add: word_test_bit_def word_ubin.eq_norm nth_bintr) 2181 2182lemma word_test_bit_transfer [transfer_rule]: 2183 "(rel_fun pcr_word (rel_fun (=) (=))) 2184 (\<lambda>x n. n < LENGTH('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)" 2185 unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp 2186 2187lemma word_ops_nth_size: 2188 "n < size x \<Longrightarrow> 2189 (x OR y) !! n = (x !! n | y !! n) \<and> 2190 (x AND y) !! n = (x !! n \<and> y !! n) \<and> 2191 (x XOR y) !! n = (x !! n \<noteq> y !! n) \<and> 2192 (NOT x) !! n = (\<not> x !! n)" 2193 for x :: "'a::len0 word" 2194 unfolding word_size by transfer (simp add: bin_nth_ops) 2195 2196lemma word_ao_nth: 2197 "(x OR y) !! n = (x !! n | y !! n) \<and> 2198 (x AND y) !! n = (x !! n \<and> y !! n)" 2199 for x :: "'a::len0 word" 2200 by transfer (auto simp add: bin_nth_ops) 2201 2202lemma test_bit_numeral [simp]: 2203 "(numeral w :: 'a::len0 word) !! n \<longleftrightarrow> 2204 n < LENGTH('a) \<and> bin_nth (numeral w) n" 2205 by transfer (rule refl) 2206 2207lemma test_bit_neg_numeral [simp]: 2208 "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow> 2209 n < LENGTH('a) \<and> bin_nth (- numeral w) n" 2210 by transfer (rule refl) 2211 2212lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \<longleftrightarrow> n = 0" 2213 by transfer auto 2214 2215lemma nth_0 [simp]: "\<not> (0 :: 'a::len0 word) !! n" 2216 by transfer simp 2217 2218lemma nth_minus1 [simp]: "(-1 :: 'a::len0 word) !! n \<longleftrightarrow> n < LENGTH('a)" 2219 by transfer simp 2220 2221\<comment> \<open>get from commutativity, associativity etc of \<open>int_and\<close> etc to same for \<open>word_and etc\<close>\<close> 2222lemmas bwsimps = 2223 wi_hom_add 2224 word_wi_log_defs 2225 2226lemma word_bw_assocs: 2227 "(x AND y) AND z = x AND y AND z" 2228 "(x OR y) OR z = x OR y OR z" 2229 "(x XOR y) XOR z = x XOR y XOR z" 2230 for x :: "'a::len0 word" 2231 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2232 2233lemma word_bw_comms: 2234 "x AND y = y AND x" 2235 "x OR y = y OR x" 2236 "x XOR y = y XOR x" 2237 for x :: "'a::len0 word" 2238 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2239 2240lemma word_bw_lcs: 2241 "y AND x AND z = x AND y AND z" 2242 "y OR x OR z = x OR y OR z" 2243 "y XOR x XOR z = x XOR y XOR z" 2244 for x :: "'a::len0 word" 2245 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2246 2247lemma word_log_esimps [simp]: 2248 "x AND 0 = 0" 2249 "x AND -1 = x" 2250 "x OR 0 = x" 2251 "x OR -1 = -1" 2252 "x XOR 0 = x" 2253 "x XOR -1 = NOT x" 2254 "0 AND x = 0" 2255 "-1 AND x = x" 2256 "0 OR x = x" 2257 "-1 OR x = -1" 2258 "0 XOR x = x" 2259 "-1 XOR x = NOT x" 2260 for x :: "'a::len0 word" 2261 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2262 2263lemma word_not_dist: 2264 "NOT (x OR y) = NOT x AND NOT y" 2265 "NOT (x AND y) = NOT x OR NOT y" 2266 for x :: "'a::len0 word" 2267 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2268 2269lemma word_bw_same: 2270 "x AND x = x" 2271 "x OR x = x" 2272 "x XOR x = 0" 2273 for x :: "'a::len0 word" 2274 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2275 2276lemma word_ao_absorbs [simp]: 2277 "x AND (y OR x) = x" 2278 "x OR y AND x = x" 2279 "x AND (x OR y) = x" 2280 "y AND x OR x = x" 2281 "(y OR x) AND x = x" 2282 "x OR x AND y = x" 2283 "(x OR y) AND x = x" 2284 "x AND y OR x = x" 2285 for x :: "'a::len0 word" 2286 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2287 2288lemma word_not_not [simp]: "NOT (NOT x) = x" 2289 for x :: "'a::len0 word" 2290 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2291 2292lemma word_ao_dist: "(x OR y) AND z = x AND z OR y AND z" 2293 for x :: "'a::len0 word" 2294 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2295 2296lemma word_oa_dist: "x AND y OR z = (x OR z) AND (y OR z)" 2297 for x :: "'a::len0 word" 2298 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) 2299 2300lemma word_add_not [simp]: "x + NOT x = -1" 2301 for x :: "'a::len0 word" 2302 by transfer (simp add: bin_add_not) 2303 2304lemma word_plus_and_or [simp]: "(x AND y) + (x OR y) = x + y" 2305 for x :: "'a::len0 word" 2306 by transfer (simp add: plus_and_or) 2307 2308lemma leoa: "w = x OR y \<Longrightarrow> y = w AND y" 2309 for x :: "'a::len0 word" 2310 by auto 2311 2312lemma leao: "w' = x' AND y' \<Longrightarrow> x' = x' OR w'" 2313 for x' :: "'a::len0 word" 2314 by auto 2315 2316lemma word_ao_equiv: "w = w OR w' \<longleftrightarrow> w' = w AND w'" 2317 for w w' :: "'a::len0 word" 2318 by (auto intro: leoa leao) 2319 2320lemma le_word_or2: "x \<le> x OR y" 2321 for x y :: "'a::len0 word" 2322 by (auto simp: word_le_def uint_or intro: le_int_or) 2323 2324lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2] 2325lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2] 2326lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2] 2327 2328lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" 2329 unfolding to_bl_def word_log_defs bl_not_bin 2330 by (simp add: word_ubin.eq_norm) 2331 2332lemma bl_word_xor: "to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)" 2333 unfolding to_bl_def word_log_defs bl_xor_bin 2334 by (simp add: word_ubin.eq_norm) 2335 2336lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)" 2337 unfolding to_bl_def word_log_defs bl_or_bin 2338 by (simp add: word_ubin.eq_norm) 2339 2340lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)" 2341 unfolding to_bl_def word_log_defs bl_and_bin 2342 by (simp add: word_ubin.eq_norm) 2343 2344lemma word_lsb_alt: "lsb w = test_bit w 0" 2345 for w :: "'a::len0 word" 2346 by (auto simp: word_test_bit_def word_lsb_def) 2347 2348lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len0 word)" 2349 unfolding word_lsb_def uint_eq_0 uint_1 by simp 2350 2351lemma word_lsb_last: "lsb w = last (to_bl w)" 2352 for w :: "'a::len word" 2353 apply (unfold word_lsb_def uint_bl bin_to_bl_def) 2354 apply (rule_tac bin="uint w" in bin_exhaust) 2355 apply (cases "size w") 2356 apply auto 2357 apply (auto simp add: bin_to_bl_aux_alt) 2358 done 2359 2360lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1" 2361 by (auto simp: word_lsb_def bin_last_def) 2362 2363lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0" 2364 by (simp only: word_msb_def sign_Min_lt_0) 2365 2366lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)" 2367 by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem) 2368 2369lemma word_msb_numeral [simp]: 2370 "msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)" 2371 unfolding word_numeral_alt by (rule msb_word_of_int) 2372 2373lemma word_msb_neg_numeral [simp]: 2374 "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)" 2375 unfolding word_neg_numeral_alt by (rule msb_word_of_int) 2376 2377lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)" 2378 by (simp add: word_msb_def) 2379 2380lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1" 2381 unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat] 2382 by (simp add: Suc_le_eq) 2383 2384lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)" 2385 for w :: "'a::len word" 2386 by (simp add: word_msb_def sint_uint bin_sign_lem) 2387 2388lemma word_msb_alt: "msb w = hd (to_bl w)" 2389 for w :: "'a::len word" 2390 apply (unfold word_msb_nth uint_bl) 2391 apply (subst hd_conv_nth) 2392 apply (rule length_greater_0_conv [THEN iffD1]) 2393 apply simp 2394 apply (simp add : nth_bin_to_bl word_size) 2395 done 2396 2397lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w" 2398 for w :: "'a::len0 word" 2399 by (auto simp: word_test_bit_def word_set_bit_def) 2400 2401lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w" 2402 apply (unfold word_size) 2403 apply (safe elim!: bin_nth_uint_imp) 2404 apply (frule bin_nth_uint_imp) 2405 apply (fast dest!: bin_nth_bl)+ 2406 done 2407 2408lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size] 2409 2410lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w" 2411 unfolding to_bl_def word_test_bit_def word_size by (rule bin_nth_uint) 2412 2413lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)" 2414 apply (unfold test_bit_bl) 2415 apply clarsimp 2416 apply (rule trans) 2417 apply (rule nth_rev_alt) 2418 apply (auto simp add: word_size) 2419 done 2420 2421lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x" 2422 for w :: "'a::len0 word" 2423 by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr) 2424 2425lemma test_bit_set_gen: 2426 "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)" 2427 for w :: "'a::len0 word" 2428 apply (unfold word_size word_test_bit_def word_set_bit_def) 2429 apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen) 2430 apply (auto elim!: test_bit_size [unfolded word_size] 2431 simp add: word_test_bit_def [symmetric]) 2432 done 2433 2434lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs" 2435 by (auto simp: of_bl_def bl_to_bin_rep_F) 2436 2437lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)" 2438 for w :: "'a::len word" 2439 by (simp add: word_msb_nth word_test_bit_def) 2440 2441lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]] 2442lemmas msb1 = msb0 [where i = 0] 2443lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]] 2444 2445lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]] 2446lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt] 2447 2448lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y" 2449 for w :: "'a::len0 word" 2450 by (rule word_eqI) (simp add : test_bit_set_gen word_size) 2451 2452lemma word_set_set_diff: 2453 fixes w :: "'a::len0 word" 2454 assumes "m \<noteq> n" 2455 shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 2456 by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms) 2457 2458lemma nth_sint: 2459 fixes w :: "'a::len word" 2460 defines "l \<equiv> LENGTH('a)" 2461 shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))" 2462 unfolding sint_uint l_def 2463 by (auto simp: nth_sbintr word_test_bit_def [symmetric]) 2464 2465lemma word_lsb_numeral [simp]: 2466 "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)" 2467 unfolding word_lsb_alt test_bit_numeral by simp 2468 2469lemma word_lsb_neg_numeral [simp]: 2470 "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)" 2471 by (simp add: word_lsb_alt) 2472 2473lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)" 2474 unfolding word_set_bit_def 2475 by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr) 2476 2477lemma word_set_numeral [simp]: 2478 "set_bit (numeral bin::'a::len0 word) n b = 2479 word_of_int (bin_sc n b (numeral bin))" 2480 unfolding word_numeral_alt by (rule set_bit_word_of_int) 2481 2482lemma word_set_neg_numeral [simp]: 2483 "set_bit (- numeral bin::'a::len0 word) n b = 2484 word_of_int (bin_sc n b (- numeral bin))" 2485 unfolding word_neg_numeral_alt by (rule set_bit_word_of_int) 2486 2487lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)" 2488 unfolding word_0_wi by (rule set_bit_word_of_int) 2489 2490lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)" 2491 unfolding word_1_wi by (rule set_bit_word_of_int) 2492 2493lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))" 2494 by (simp add: setBit_def) 2495 2496lemma clearBit_no [simp]: 2497 "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))" 2498 by (simp add: clearBit_def) 2499 2500lemma to_bl_n1: "to_bl (-1::'a::len0 word) = replicate (LENGTH('a)) True" 2501 apply (rule word_bl.Abs_inverse') 2502 apply simp 2503 apply (rule word_eqI) 2504 apply (clarsimp simp add: word_size) 2505 apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size) 2506 done 2507 2508lemma word_msb_n1 [simp]: "msb (-1::'a::len word)" 2509 unfolding word_msb_alt to_bl_n1 by simp 2510 2511lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w" 2512 for w :: "'a::len0 word" 2513 apply (rule iffI) 2514 apply (rule disjCI) 2515 apply (drule word_eqD) 2516 apply (erule sym [THEN trans]) 2517 apply (simp add: test_bit_set) 2518 apply (erule disjE) 2519 apply clarsimp 2520 apply (rule word_eqI) 2521 apply (clarsimp simp add : test_bit_set_gen) 2522 apply (drule test_bit_size) 2523 apply force 2524 done 2525 2526lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)" 2527 by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin) 2528 2529lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a::len)" 2530 by (simp add: test_bit_2p [symmetric] word_of_int [symmetric]) 2531 2532lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n" 2533 apply (unfold word_arith_power_alt) 2534 apply (case_tac "LENGTH('a)") 2535 apply clarsimp 2536 apply (case_tac "nat") 2537 apply clarsimp 2538 apply (case_tac "n") 2539 apply clarsimp 2540 apply clarsimp 2541 apply (drule word_gt_0 [THEN iffD1]) 2542 apply (safe intro!: word_eqI) 2543 apply (auto simp add: nth_2p_bin) 2544 apply (erule notE) 2545 apply (simp (no_asm_use) add: uint_word_of_int word_size) 2546 apply (subst mod_pos_pos_trivial) 2547 apply simp 2548 apply (rule power_strict_increasing) 2549 apply simp_all 2550 done 2551 2552lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n" 2553 by (induct n) (simp_all add: wi_hom_syms) 2554 2555lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x" 2556 for x :: "'a::len word" 2557 apply (rule xtr3) 2558 apply (rule_tac [2] y = "x" in le_word_or2) 2559 apply (rule word_eqI) 2560 apply (auto simp add: word_ao_nth nth_w2p word_size) 2561 done 2562 2563lemma word_clr_le: "w \<ge> set_bit w n False" 2564 for w :: "'a::len0 word" 2565 apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm) 2566 apply (rule order_trans) 2567 apply (rule bintr_bin_clr_le) 2568 apply simp 2569 done 2570 2571lemma word_set_ge: "w \<le> set_bit w n True" 2572 for w :: "'a::len word" 2573 apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm) 2574 apply (rule order_trans [OF _ bintr_bin_set_ge]) 2575 apply simp 2576 done 2577 2578lemma set_bit_beyond: 2579 "size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len0 word" 2580 by (auto intro: word_eqI simp add: test_bit_set_gen word_size) 2581 2582lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))" 2583 by (simp add: zip_rev bl_word_or rev_map) 2584 2585lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))" 2586 by (simp add: zip_rev bl_word_and rev_map) 2587 2588lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))" 2589 by (simp add: zip_rev bl_word_xor rev_map) 2590 2591lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))" 2592 by (simp add: bl_word_not rev_map) 2593 2594 2595subsection \<open>Bit comprehension\<close> 2596 2597instantiation word :: (len0) bit_comprehension 2598begin 2599 2600definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth LENGTH('a) f)" 2601 2602instance .. 2603 2604end 2605 2606lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *) 2607 2608lemma td_ext_nth [OF refl refl refl, unfolded word_size]: 2609 "n = size w \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> 2610 td_ext test_bit ofn {f. \<forall>i. f i \<longrightarrow> i < n} (\<lambda>h i. h i \<and> i < n)" 2611 for w :: "'a::len0 word" 2612 apply (unfold word_size td_ext_def') 2613 apply safe 2614 apply (rule_tac [3] ext) 2615 apply (rule_tac [4] ext) 2616 apply (unfold word_size of_nth_def test_bit_bl) 2617 apply safe 2618 defer 2619 apply (clarsimp simp: word_bl.Abs_inverse)+ 2620 apply (rule word_bl.Rep_inverse') 2621 apply (rule sym [THEN trans]) 2622 apply (rule bl_of_nth_nth) 2623 apply simp 2624 apply (rule bl_of_nth_inj) 2625 apply (clarsimp simp add : test_bit_bl word_size) 2626 done 2627 2628interpretation test_bit: 2629 td_ext 2630 "(!!) :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> bool" 2631 set_bits 2632 "{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len0)}" 2633 "(\<lambda>h i. h i \<and> i < LENGTH('a::len0))" 2634 by (rule td_ext_nth) 2635 2636lemmas td_nth = test_bit.td_thm 2637 2638lemma set_bits_K_False [simp]: 2639 "set_bits (\<lambda>_. False) = (0 :: 'a :: len0 word)" 2640 by (rule word_eqI) (simp add: test_bit.eq_norm) 2641 2642 2643subsection \<open>Shifting, Rotating, and Splitting Words\<close> 2644 2645lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)" 2646 unfolding shiftl1_def 2647 apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm) 2648 apply (subst refl [THEN bintrunc_BIT_I, symmetric]) 2649 apply (subst bintrunc_bintrunc_min) 2650 apply simp 2651 done 2652 2653lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)" 2654 unfolding word_numeral_alt shiftl1_wi by simp 2655 2656lemma shiftl1_neg_numeral [simp]: "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)" 2657 unfolding word_neg_numeral_alt shiftl1_wi by simp 2658 2659lemma shiftl1_0 [simp] : "shiftl1 0 = 0" 2660 by (simp add: shiftl1_def) 2661 2662lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT False)" 2663 by (simp only: shiftl1_def) (* FIXME: duplicate *) 2664 2665lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT False)" 2666 by (simp add: shiftl1_def Bit_B0 wi_hom_syms) 2667 2668lemma shiftr1_0 [simp]: "shiftr1 0 = 0" 2669 by (simp add: shiftr1_def) 2670 2671lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0" 2672 by (simp add: sshiftr1_def) 2673 2674lemma sshiftr1_n1 [simp]: "sshiftr1 (- 1) = - 1" 2675 by (simp add: sshiftr1_def) 2676 2677lemma shiftl_0 [simp]: "(0::'a::len0 word) << n = 0" 2678 by (induct n) (auto simp: shiftl_def) 2679 2680lemma shiftr_0 [simp]: "(0::'a::len0 word) >> n = 0" 2681 by (induct n) (auto simp: shiftr_def) 2682 2683lemma sshiftr_0 [simp]: "0 >>> n = 0" 2684 by (induct n) (auto simp: sshiftr_def) 2685 2686lemma sshiftr_n1 [simp]: "-1 >>> n = -1" 2687 by (induct n) (auto simp: sshiftr_def) 2688 2689lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)" 2690 apply (unfold shiftl1_def word_test_bit_def) 2691 apply (simp add: nth_bintr word_ubin.eq_norm word_size) 2692 apply (cases n) 2693 apply auto 2694 done 2695 2696lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)" 2697 for w :: "'a::len0 word" 2698 apply (unfold shiftl_def) 2699 apply (induct m arbitrary: n) 2700 apply (force elim!: test_bit_size) 2701 apply (clarsimp simp add : nth_shiftl1 word_size) 2702 apply arith 2703 done 2704 2705lemmas nth_shiftl = nth_shiftl' [unfolded word_size] 2706 2707lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n" 2708 apply (unfold shiftr1_def word_test_bit_def) 2709 apply (simp add: nth_bintr word_ubin.eq_norm) 2710 apply safe 2711 apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp]) 2712 apply simp 2713 done 2714 2715lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)" 2716 for w :: "'a::len0 word" 2717 apply (unfold shiftr_def) 2718 apply (induct "m" arbitrary: n) 2719 apply (auto simp add: nth_shiftr1) 2720 done 2721 2722text \<open> 2723 see paper page 10, (1), (2), \<open>shiftr1_def\<close> is of the form of (1), 2724 where \<open>f\<close> (ie \<open>bin_rest\<close>) takes normal arguments to normal results, 2725 thus we get (2) from (1) 2726\<close> 2727 2728lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" 2729 apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i) 2730 apply (subst bintr_uint [symmetric, OF order_refl]) 2731 apply (simp only : bintrunc_bintrunc_l) 2732 apply simp 2733 done 2734 2735lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)" 2736 apply (unfold sshiftr1_def word_test_bit_def) 2737 apply (simp add: nth_bintr word_ubin.eq_norm bin_nth.Suc [symmetric] word_size 2738 del: bin_nth.simps) 2739 apply (simp add: nth_bintr uint_sint del : bin_nth.simps) 2740 apply (auto simp add: bin_nth_sint) 2741 done 2742 2743lemma nth_sshiftr [rule_format] : 2744 "\<forall>n. sshiftr w m !! n = 2745 (n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))" 2746 apply (unfold sshiftr_def) 2747 apply (induct_tac m) 2748 apply (simp add: test_bit_bl) 2749 apply (clarsimp simp add: nth_sshiftr1 word_size) 2750 apply safe 2751 apply arith 2752 apply arith 2753 apply (erule thin_rl) 2754 apply (case_tac n) 2755 apply safe 2756 apply simp 2757 apply simp 2758 apply (erule thin_rl) 2759 apply (case_tac n) 2760 apply safe 2761 apply simp 2762 apply simp 2763 apply arith+ 2764 done 2765 2766lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2" 2767 apply (unfold shiftr1_def bin_rest_def) 2768 apply (rule word_uint.Abs_inverse) 2769 apply (simp add: uints_num pos_imp_zdiv_nonneg_iff) 2770 apply (rule xtr7) 2771 prefer 2 2772 apply (rule zdiv_le_dividend) 2773 apply auto 2774 done 2775 2776lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2" 2777 apply (unfold sshiftr1_def bin_rest_def [symmetric]) 2778 apply (simp add: word_sbin.eq_norm) 2779 apply (rule trans) 2780 defer 2781 apply (subst word_sbin.norm_Rep [symmetric]) 2782 apply (rule refl) 2783 apply (subst word_sbin.norm_Rep [symmetric]) 2784 apply (unfold One_nat_def) 2785 apply (rule sbintrunc_rest) 2786 done 2787 2788lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n" 2789 apply (unfold shiftr_def) 2790 apply (induct n) 2791 apply simp 2792 apply (simp add: shiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric]) 2793 done 2794 2795lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n" 2796 apply (unfold sshiftr_def) 2797 apply (induct n) 2798 apply simp 2799 apply (simp add: sshiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric]) 2800 done 2801 2802 2803subsubsection \<open>shift functions in terms of lists of bools\<close> 2804 2805lemmas bshiftr1_numeral [simp] = 2806 bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w 2807 2808lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)" 2809 unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp 2810 2811lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])" 2812 by (simp add: of_bl_def bl_to_bin_append) 2813 2814lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])" 2815 for w :: "'a::len0 word" 2816proof - 2817 have "shiftl1 w = shiftl1 (of_bl (to_bl w))" 2818 by simp 2819 also have "\<dots> = of_bl (to_bl w @ [False])" 2820 by (rule shiftl1_of_bl) 2821 finally show ?thesis . 2822qed 2823 2824lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]" 2825 for w :: "'a::len word" 2826 by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI) 2827 2828\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close> 2829lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])" 2830 by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append) 2831 2832lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))" 2833 apply (unfold shiftr1_def uint_bl of_bl_def) 2834 apply (simp add: butlast_rest_bin word_size) 2835 apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def]) 2836 done 2837 2838lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)" 2839 for w :: "'a::len word" 2840 by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI]) 2841 2842\<comment> \<open>Generalized version of \<open>bl_shiftr1\<close>. Maybe this one should replace it?\<close> 2843lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)" 2844 apply (rule word_bl.Abs_inverse') 2845 apply (simp del: butlast.simps) 2846 apply (simp add: shiftr1_bl of_bl_def) 2847 done 2848 2849lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))" 2850 apply (unfold word_reverse_def) 2851 apply (rule word_bl.Rep_inverse' [symmetric]) 2852 apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse) 2853 done 2854 2855lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)" 2856 by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev) 2857 2858lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)" 2859 by (simp add: shiftl_rev) 2860 2861lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)" 2862 by (simp add: rev_shiftl) 2863 2864lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)" 2865 by (simp add: shiftr_rev) 2866 2867lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)" 2868 for w :: "'a::len word" 2869 apply (unfold sshiftr1_def uint_bl word_size) 2870 apply (simp add: butlast_rest_bin word_ubin.eq_norm) 2871 apply (simp add: sint_uint) 2872 apply (rule nth_equalityI) 2873 apply clarsimp 2874 apply clarsimp 2875 apply (case_tac i) 2876 apply (simp_all add: hd_conv_nth length_0_conv [symmetric] 2877 nth_bin_to_bl bin_nth.Suc [symmetric] nth_sbintr 2878 del: bin_nth.Suc) 2879 apply force 2880 apply (rule impI) 2881 apply (rule_tac f = "bin_nth (uint w)" in arg_cong) 2882 apply simp 2883 done 2884 2885lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)" 2886 for w :: "'a::len word" 2887 apply (unfold shiftr_def) 2888 apply (induct n) 2889 prefer 2 2890 apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric]) 2891 apply (rule butlast_take [THEN trans]) 2892 apply (auto simp: word_size) 2893 done 2894 2895lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)" 2896 for w :: "'a::len word" 2897 apply (unfold sshiftr_def) 2898 apply (induct n) 2899 prefer 2 2900 apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric]) 2901 apply (rule butlast_take [THEN trans]) 2902 apply (auto simp: word_size) 2903 done 2904 2905lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False" 2906 apply (unfold shiftr_def) 2907 apply (induct n) 2908 prefer 2 2909 apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size) 2910 apply (rule take_butlast [THEN trans]) 2911 apply (auto simp: word_size) 2912 done 2913 2914lemma take_sshiftr' [rule_format] : 2915 "n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and> 2916 take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" 2917 for w :: "'a::len word" 2918 apply (unfold sshiftr_def) 2919 apply (induct n) 2920 prefer 2 2921 apply (simp add: bl_sshiftr1) 2922 apply (rule impI) 2923 apply (rule take_butlast [THEN trans]) 2924 apply (auto simp: word_size) 2925 done 2926 2927lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1] 2928lemmas take_sshiftr = take_sshiftr' [THEN conjunct2] 2929 2930lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d" 2931 by (auto intro: append_take_drop_id [symmetric]) 2932 2933lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr] 2934lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr] 2935 2936lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)" 2937 by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same) 2938 2939lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)" 2940 for w :: "'a::len0 word" 2941proof - 2942 have "w << n = of_bl (to_bl w) << n" 2943 by simp 2944 also have "\<dots> = of_bl (to_bl w @ replicate n False)" 2945 by (rule shiftl_of_bl) 2946 finally show ?thesis . 2947qed 2948 2949lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w 2950 2951lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False" 2952 by (simp add: shiftl_bl word_rep_drop word_size) 2953 2954lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0" 2955 for x :: "'a::len0 word" 2956 apply (unfold word_size) 2957 apply (rule word_eqI) 2958 apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append) 2959 done 2960 2961\<comment> \<open>note -- the following results use \<open>'a::len word < number_ring\<close>\<close> 2962 2963lemma shiftl1_2t: "shiftl1 w = 2 * w" 2964 for w :: "'a::len word" 2965 by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric]) 2966 2967lemma shiftl1_p: "shiftl1 w = w + w" 2968 for w :: "'a::len word" 2969 by (simp add: shiftl1_2t) 2970 2971lemma shiftl_t2n: "shiftl w n = 2 ^ n * w" 2972 for w :: "'a::len word" 2973 by (induct n) (auto simp: shiftl_def shiftl1_2t) 2974 2975lemma shiftr1_bintr [simp]: 2976 "(shiftr1 (numeral w) :: 'a::len0 word) = 2977 word_of_int (bin_rest (bintrunc (LENGTH('a)) (numeral w)))" 2978 unfolding shiftr1_def word_numeral_alt by (simp add: word_ubin.eq_norm) 2979 2980lemma sshiftr1_sbintr [simp]: 2981 "(sshiftr1 (numeral w) :: 'a::len word) = 2982 word_of_int (bin_rest (sbintrunc (LENGTH('a) - 1) (numeral w)))" 2983 unfolding sshiftr1_def word_numeral_alt by (simp add: word_sbin.eq_norm) 2984 2985lemma shiftr_no [simp]: 2986 (* FIXME: neg_numeral *) 2987 "(numeral w::'a::len0 word) >> n = word_of_int 2988 ((bin_rest ^^ n) (bintrunc (LENGTH('a)) (numeral w)))" 2989 by (rule word_eqI) (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size) 2990 2991lemma sshiftr_no [simp]: 2992 (* FIXME: neg_numeral *) 2993 "(numeral w::'a::len word) >>> n = word_of_int 2994 ((bin_rest ^^ n) (sbintrunc (LENGTH('a) - 1) (numeral w)))" 2995 apply (rule word_eqI) 2996 apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size) 2997 apply (subgoal_tac "na + n = LENGTH('a) - Suc 0", simp, simp)+ 2998 done 2999 3000lemma shiftr1_bl_of: 3001 "length bl \<le> LENGTH('a) \<Longrightarrow> 3002 shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)" 3003 by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin word_ubin.eq_norm trunc_bl2bin) 3004 3005lemma shiftr_bl_of: 3006 "length bl \<le> LENGTH('a) \<Longrightarrow> 3007 (of_bl bl::'a::len0 word) >> n = of_bl (take (length bl - n) bl)" 3008 apply (unfold shiftr_def) 3009 apply (induct n) 3010 apply clarsimp 3011 apply clarsimp 3012 apply (subst shiftr1_bl_of) 3013 apply simp 3014 apply (simp add: butlast_take) 3015 done 3016 3017lemma shiftr_bl: "x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))" 3018 for x :: "'a::len0 word" 3019 using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp 3020 3021lemma msb_shift: "msb w \<longleftrightarrow> w >> (LENGTH('a) - 1) \<noteq> 0" 3022 for w :: "'a::len word" 3023 apply (unfold shiftr_bl word_msb_alt) 3024 apply (simp add: word_size Suc_le_eq take_Suc) 3025 apply (cases "hd (to_bl w)") 3026 apply (auto simp: word_1_bl of_bl_rep_False [where n=1 and bs="[]", simplified]) 3027 done 3028 3029lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys" 3030 apply (induct ys arbitrary: n) 3031 apply simp_all 3032 apply (case_tac n) 3033 apply simp_all 3034 done 3035 3036lemma align_lem_or [rule_format] : 3037 "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow> 3038 drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow> 3039 map2 (|) x y = take m x @ drop m y" 3040 apply (induct y) 3041 apply force 3042 apply clarsimp 3043 apply (case_tac x) 3044 apply force 3045 apply (case_tac m) 3046 apply auto 3047 apply (drule_tac t="length xs" for xs in sym) 3048 apply (auto simp: zip_replicate o_def) 3049 done 3050 3051lemma align_lem_and [rule_format] : 3052 "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow> 3053 drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow> 3054 map2 (\<and>) x y = replicate (n + m) False" 3055 apply (induct y) 3056 apply force 3057 apply clarsimp 3058 apply (case_tac x) 3059 apply force 3060 apply (case_tac m) 3061 apply auto 3062 apply (drule_tac t="length xs" for xs in sym) 3063 apply (auto simp: zip_replicate o_def map_replicate_const) 3064 done 3065 3066lemma aligned_bl_add_size [OF refl]: 3067 "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow> 3068 take m (to_bl y) = replicate m False \<Longrightarrow> 3069 to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)" 3070 apply (subgoal_tac "x AND y = 0") 3071 prefer 2 3072 apply (rule word_bl.Rep_eqD) 3073 apply (simp add: bl_word_and) 3074 apply (rule align_lem_and [THEN trans]) 3075 apply (simp_all add: word_size)[5] 3076 apply simp 3077 apply (subst word_plus_and_or [symmetric]) 3078 apply (simp add : bl_word_or) 3079 apply (rule align_lem_or) 3080 apply (simp_all add: word_size) 3081 done 3082 3083 3084subsubsection \<open>Mask\<close> 3085 3086lemma nth_mask [OF refl, simp]: "m = mask n \<Longrightarrow> test_bit m i \<longleftrightarrow> i < n \<and> i < size m" 3087 apply (unfold mask_def test_bit_bl) 3088 apply (simp only: word_1_bl [symmetric] shiftl_of_bl) 3089 apply (clarsimp simp add: word_size) 3090 apply (simp only: of_bl_def mask_lem word_of_int_hom_syms add_diff_cancel2) 3091 apply (fold of_bl_def) 3092 apply (simp add: word_1_bl) 3093 apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size]) 3094 apply auto 3095 done 3096 3097lemma mask_bl: "mask n = of_bl (replicate n True)" 3098 by (auto simp add : test_bit_of_bl word_size intro: word_eqI) 3099 3100lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))" 3101 by (auto simp add: nth_bintr word_size intro: word_eqI) 3102 3103lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))" 3104 apply (rule word_eqI) 3105 apply (simp add: nth_bintr word_size word_ops_nth_size) 3106 apply (auto simp add: test_bit_bin) 3107 done 3108 3109lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)" 3110 by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff) 3111 3112lemma and_mask_wi': 3113 "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)" 3114 by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff) 3115 3116lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))" 3117 unfolding word_numeral_alt by (rule and_mask_wi) 3118 3119lemma bl_and_mask': 3120 "to_bl (w AND mask n :: 'a::len word) = 3121 replicate (LENGTH('a) - n) False @ 3122 drop (LENGTH('a) - n) (to_bl w)" 3123 apply (rule nth_equalityI) 3124 apply simp 3125 apply (clarsimp simp add: to_bl_nth word_size) 3126 apply (simp add: word_size word_ops_nth_size) 3127 apply (auto simp add: word_size test_bit_bl nth_append nth_rev) 3128 done 3129 3130lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)" 3131 by (simp only: and_mask_bintr bintrunc_mod2p) 3132 3133lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n" 3134 apply (simp add: and_mask_bintr word_ubin.eq_norm) 3135 apply (simp add: bintrunc_mod2p) 3136 apply (rule xtr8) 3137 prefer 2 3138 apply (rule pos_mod_bound) 3139 apply auto 3140 done 3141 3142lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n" 3143 for b n :: int 3144 by (simp add: int_mod_lem eq_sym_conv) 3145 3146lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n" 3147 apply (simp add: and_mask_bintr) 3148 apply (simp add: word_ubin.inverse_norm) 3149 apply (simp add: eq_mod_iff bintrunc_mod2p min_def) 3150 apply (fast intro!: lt2p_lem) 3151 done 3152 3153lemma and_mask_dvd: "2 ^ n dvd uint w \<longleftrightarrow> w AND mask n = 0" 3154 apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p) 3155 apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs del: word_of_int_0) 3156 apply (subst word_uint.norm_Rep [symmetric]) 3157 apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def) 3158 apply auto 3159 done 3160 3161lemma and_mask_dvd_nat: "2 ^ n dvd unat w \<longleftrightarrow> w AND mask n = 0" 3162 apply (unfold unat_def) 3163 apply (rule trans [OF _ and_mask_dvd]) 3164 apply (unfold dvd_def) 3165 apply auto 3166 apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric]) 3167 apply simp 3168 apply (simp add: nat_mult_distrib nat_power_eq) 3169 done 3170 3171lemma word_2p_lem: "n < size w \<Longrightarrow> w < 2 ^ n = (uint w < 2 ^ n)" 3172 for w :: "'a::len word" 3173 apply (unfold word_size word_less_alt word_numeral_alt) 3174 apply (auto simp add: word_of_int_power_hom word_uint.eq_norm mod_pos_pos_trivial 3175 simp del: word_of_int_numeral) 3176 done 3177 3178lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x" 3179 for x :: "'a::len word" 3180 apply (unfold word_less_alt word_numeral_alt) 3181 apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom word_uint.eq_norm 3182 simp del: word_of_int_numeral) 3183 apply (drule xtr8 [rotated]) 3184 apply (rule int_mod_le) 3185 apply (auto simp add : mod_pos_pos_trivial) 3186 done 3187 3188lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]] 3189 3190lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size] 3191 3192lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n" 3193 unfolding word_size by (erule and_mask_less') 3194 3195lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n" 3196 for c x :: "'a::len word" 3197 by (auto simp: word_mod_def uint_2p and_mask_mod_2p) 3198 3199lemma mask_eqs: 3200 "(a AND mask n) + b AND mask n = a + b AND mask n" 3201 "a + (b AND mask n) AND mask n = a + b AND mask n" 3202 "(a AND mask n) - b AND mask n = a - b AND mask n" 3203 "a - (b AND mask n) AND mask n = a - b AND mask n" 3204 "a * (b AND mask n) AND mask n = a * b AND mask n" 3205 "(b AND mask n) * a AND mask n = b * a AND mask n" 3206 "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n" 3207 "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n" 3208 "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n" 3209 "- (a AND mask n) AND mask n = - a AND mask n" 3210 "word_succ (a AND mask n) AND mask n = word_succ a AND mask n" 3211 "word_pred (a AND mask n) AND mask n = word_pred a AND mask n" 3212 using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b] 3213 by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps) 3214 3215lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n" 3216 using word_of_int_Ex [where x=x] 3217 by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps) 3218 3219lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)" 3220 by (simp add: mask_def word_size shiftl_zero_size) 3221 3222 3223subsubsection \<open>Revcast\<close> 3224 3225lemmas revcast_def' = revcast_def [simplified] 3226lemmas revcast_def'' = revcast_def' [simplified word_size] 3227lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w 3228 3229lemma to_bl_revcast: 3230 "to_bl (revcast w :: 'a::len0 word) = takefill False (LENGTH('a)) (to_bl w)" 3231 apply (unfold revcast_def' word_size) 3232 apply (rule word_bl.Abs_inverse) 3233 apply simp 3234 done 3235 3236lemma revcast_rev_ucast [OF refl refl refl]: 3237 "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow> 3238 rc = word_reverse uc" 3239 apply (unfold ucast_def revcast_def' Let_def word_reverse_def) 3240 apply (auto simp: to_bl_of_bin takefill_bintrunc) 3241 apply (simp add: word_bl.Abs_inverse word_size) 3242 done 3243 3244lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))" 3245 using revcast_rev_ucast [of "word_reverse w"] by simp 3246 3247lemma ucast_revcast: "ucast w = word_reverse (revcast (word_reverse w))" 3248 by (fact revcast_rev_ucast [THEN word_rev_gal']) 3249 3250lemma ucast_rev_revcast: "ucast (word_reverse w) = word_reverse (revcast w)" 3251 by (fact revcast_ucast [THEN word_rev_gal']) 3252 3253 3254text "linking revcast and cast via shift" 3255 3256lemmas wsst_TYs = source_size target_size word_size 3257 3258lemma revcast_down_uu [OF refl]: 3259 "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)" 3260 for w :: "'a::len word" 3261 apply (simp add: revcast_def') 3262 apply (rule word_bl.Rep_inverse') 3263 apply (rule trans, rule ucast_down_drop) 3264 prefer 2 3265 apply (rule trans, rule drop_shiftr) 3266 apply (auto simp: takefill_alt wsst_TYs) 3267 done 3268 3269lemma revcast_down_us [OF refl]: 3270 "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)" 3271 for w :: "'a::len word" 3272 apply (simp add: revcast_def') 3273 apply (rule word_bl.Rep_inverse') 3274 apply (rule trans, rule ucast_down_drop) 3275 prefer 2 3276 apply (rule trans, rule drop_sshiftr) 3277 apply (auto simp: takefill_alt wsst_TYs) 3278 done 3279 3280lemma revcast_down_su [OF refl]: 3281 "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)" 3282 for w :: "'a::len word" 3283 apply (simp add: revcast_def') 3284 apply (rule word_bl.Rep_inverse') 3285 apply (rule trans, rule scast_down_drop) 3286 prefer 2 3287 apply (rule trans, rule drop_shiftr) 3288 apply (auto simp: takefill_alt wsst_TYs) 3289 done 3290 3291lemma revcast_down_ss [OF refl]: 3292 "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)" 3293 for w :: "'a::len word" 3294 apply (simp add: revcast_def') 3295 apply (rule word_bl.Rep_inverse') 3296 apply (rule trans, rule scast_down_drop) 3297 prefer 2 3298 apply (rule trans, rule drop_sshiftr) 3299 apply (auto simp: takefill_alt wsst_TYs) 3300 done 3301 3302(* FIXME: should this also be [OF refl] ? *) 3303lemma cast_down_rev: 3304 "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (w << n)" 3305 for w :: "'a::len word" 3306 apply (unfold shiftl_rev) 3307 apply clarify 3308 apply (simp add: revcast_rev_ucast) 3309 apply (rule word_rev_gal') 3310 apply (rule trans [OF _ revcast_rev_ucast]) 3311 apply (rule revcast_down_uu [symmetric]) 3312 apply (auto simp add: wsst_TYs) 3313 done 3314 3315lemma revcast_up [OF refl]: 3316 "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow> 3317 rc w = (ucast w :: 'a::len word) << n" 3318 apply (simp add: revcast_def') 3319 apply (rule word_bl.Rep_inverse') 3320 apply (simp add: takefill_alt) 3321 apply (rule bl_shiftl [THEN trans]) 3322 apply (subst ucast_up_app) 3323 apply (auto simp add: wsst_TYs) 3324 done 3325 3326lemmas rc1 = revcast_up [THEN 3327 revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]] 3328lemmas rc2 = revcast_down_uu [THEN 3329 revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]] 3330 3331lemmas ucast_up = 3332 rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]] 3333lemmas ucast_down = 3334 rc2 [simplified rev_shiftr revcast_ucast [symmetric]] 3335 3336 3337subsubsection \<open>Slices\<close> 3338 3339lemma slice1_no_bin [simp]: 3340 "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len0)) (numeral w)))" 3341 by (simp add: slice1_def) (* TODO: neg_numeral *) 3342 3343lemma slice_no_bin [simp]: 3344 "slice n (numeral w :: 'b word) = of_bl (takefill False (LENGTH('b::len0) - n) 3345 (bin_to_bl (LENGTH('b::len0)) (numeral w)))" 3346 by (simp add: slice_def word_size) (* TODO: neg_numeral *) 3347 3348lemma slice1_0 [simp] : "slice1 n 0 = 0" 3349 unfolding slice1_def by simp 3350 3351lemma slice_0 [simp] : "slice n 0 = 0" 3352 unfolding slice_def by auto 3353 3354lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))" 3355 unfolding slice_def' slice1_def 3356 by (simp add : takefill_alt word_size) 3357 3358lemmas slice_take = slice_take' [unfolded word_size] 3359 3360\<comment> \<open>shiftr to a word of the same size is just slice, 3361 slice is just shiftr then ucast\<close> 3362lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]] 3363 3364lemma slice_shiftr: "slice n w = ucast (w >> n)" 3365 apply (unfold slice_take shiftr_bl) 3366 apply (rule ucast_of_bl_up [symmetric]) 3367 apply (simp add: word_size) 3368 done 3369 3370lemma nth_slice: "(slice n w :: 'a::len0 word) !! m = (w !! (m + n) \<and> m < LENGTH('a))" 3371 by (simp add: slice_shiftr nth_ucast nth_shiftr) 3372 3373lemma slice1_down_alt': 3374 "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow> 3375 to_bl sl = takefill False fs (drop k (to_bl w))" 3376 by (auto simp: slice1_def word_size of_bl_def uint_bl 3377 word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill) 3378 3379lemma slice1_up_alt': 3380 "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow> 3381 to_bl sl = takefill False fs (replicate k False @ (to_bl w))" 3382 apply (unfold slice1_def word_size of_bl_def uint_bl) 3383 apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric]) 3384 apply (rule_tac f = "\<lambda>k. takefill False (LENGTH('a)) 3385 (replicate k False @ bin_to_bl (LENGTH('b)) (uint w))" in arg_cong) 3386 apply arith 3387 done 3388 3389lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size] 3390lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size] 3391lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1] 3392lemmas slice1_up_alts = 3393 le_add_diff_inverse [symmetric, THEN su1] 3394 le_add_diff_inverse2 [symmetric, THEN su1] 3395 3396lemma ucast_slice1: "ucast w = slice1 (size w) w" 3397 by (simp add: slice1_def ucast_bl takefill_same' word_size) 3398 3399lemma ucast_slice: "ucast w = slice 0 w" 3400 by (simp add: slice_def ucast_slice1) 3401 3402lemma slice_id: "slice 0 t = t" 3403 by (simp only: ucast_slice [symmetric] ucast_id) 3404 3405lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc" 3406 by (simp add: slice1_def revcast_def' word_size) 3407 3408lemma slice1_tf_tf': 3409 "to_bl (slice1 n w :: 'a::len0 word) = 3410 rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))" 3411 unfolding slice1_def by (rule word_rev_tf) 3412 3413lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric] 3414 3415lemma rev_slice1: 3416 "n + k = LENGTH('a) + LENGTH('b) \<Longrightarrow> 3417 slice1 n (word_reverse w :: 'b::len0 word) = 3418 word_reverse (slice1 k w :: 'a::len0 word)" 3419 apply (unfold word_reverse_def slice1_tf_tf) 3420 apply (rule word_bl.Rep_inverse') 3421 apply (rule rev_swap [THEN iffD1]) 3422 apply (rule trans [symmetric]) 3423 apply (rule tf_rev) 3424 apply (simp add: word_bl.Abs_inverse) 3425 apply (simp add: word_bl.Abs_inverse) 3426 done 3427 3428lemma rev_slice: 3429 "n + k + LENGTH('a::len0) = LENGTH('b::len0) \<Longrightarrow> 3430 slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)" 3431 apply (unfold slice_def word_size) 3432 apply (rule rev_slice1) 3433 apply arith 3434 done 3435 3436lemmas sym_notr = 3437 not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]] 3438 3439\<comment> \<open>problem posed by TPHOLs referee: 3440 criterion for overflow of addition of signed integers\<close> 3441 3442lemma sofl_test: 3443 "(sint x + sint y = sint (x + y)) = 3444 ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)" 3445 for x y :: "'a::len word" 3446 apply (unfold word_size) 3447 apply (cases "LENGTH('a)", simp) 3448 apply (subst msb_shift [THEN sym_notr]) 3449 apply (simp add: word_ops_msb) 3450 apply (simp add: word_msb_sint) 3451 apply safe 3452 apply simp_all 3453 apply (unfold sint_word_ariths) 3454 apply (unfold word_sbin.set_iff_norm [symmetric] sints_num) 3455 apply safe 3456 apply (insert sint_range' [where x=x]) 3457 apply (insert sint_range' [where x=y]) 3458 defer 3459 apply (simp (no_asm), arith) 3460 apply (simp (no_asm), arith) 3461 defer 3462 defer 3463 apply (simp (no_asm), arith) 3464 apply (simp (no_asm), arith) 3465 apply (rule notI [THEN notnotD], 3466 drule leI not_le_imp_less, 3467 drule sbintrunc_inc sbintrunc_dec, 3468 simp)+ 3469 done 3470 3471lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0" 3472 for x :: "'a :: len0 word" 3473 by (rule word_eqI) (auto simp add: nth_shiftr dest: test_bit_size) 3474 3475 3476subsection \<open>Split and cat\<close> 3477 3478lemmas word_split_bin' = word_split_def 3479lemmas word_cat_bin' = word_cat_def 3480 3481lemma word_rsplit_no: 3482 "(word_rsplit (numeral bin :: 'b::len0 word) :: 'a word list) = 3483 map word_of_int (bin_rsplit (LENGTH('a::len)) 3484 (LENGTH('b), bintrunc (LENGTH('b)) (numeral bin)))" 3485 by (simp add: word_rsplit_def word_ubin.eq_norm) 3486 3487lemmas word_rsplit_no_cl [simp] = word_rsplit_no 3488 [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]] 3489 3490lemma test_bit_cat: 3491 "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and> 3492 (if n < size b then b !! n else a !! (n - size b)))" 3493 apply (auto simp: word_cat_bin' test_bit_bin word_ubin.eq_norm nth_bintr bin_nth_cat word_size) 3494 apply (erule bin_nth_uint_imp) 3495 done 3496 3497lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)" 3498 by (simp add: of_bl_def to_bl_def word_cat_bin' bl_to_bin_app_cat) 3499 3500lemma of_bl_append: 3501 "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys" 3502 apply (simp add: of_bl_def bl_to_bin_app_cat bin_cat_num) 3503 apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms) 3504 done 3505 3506lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs" 3507 by (rule word_eqI) (auto simp: test_bit_of_bl nth_append) 3508 3509lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs" 3510 by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl) 3511 3512lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs" 3513 by (cases x) simp_all 3514 3515lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow> 3516 a = bintrunc (LENGTH('a) - n) a \<and> b = bintrunc (LENGTH('a)) b" 3517 for w :: "'a::len0 word" 3518 apply (frule word_ubin.norm_Rep [THEN ssubst]) 3519 apply (drule bin_split_trunc1) 3520 apply (drule sym [THEN trans]) 3521 apply assumption 3522 apply safe 3523 done 3524 3525lemma word_split_bl': 3526 "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow> 3527 (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))" 3528 apply (unfold word_split_bin') 3529 apply safe 3530 defer 3531 apply (clarsimp split: prod.splits) 3532 apply hypsubst_thin 3533 apply (drule word_ubin.norm_Rep [THEN ssubst]) 3534 apply (drule split_bintrunc) 3535 apply (simp add: of_bl_def bl2bin_drop word_size 3536 word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep) 3537 apply (clarsimp split: prod.splits) 3538 apply (frule split_uint_lem [THEN conjunct1]) 3539 apply (unfold word_size) 3540 apply (cases "LENGTH('a) \<ge> LENGTH('b)") 3541 defer 3542 apply simp 3543 apply (simp add : of_bl_def to_bl_def) 3544 apply (subst bin_split_take1 [symmetric]) 3545 prefer 2 3546 apply assumption 3547 apply simp 3548 apply (erule thin_rl) 3549 apply (erule arg_cong [THEN trans]) 3550 apply (simp add : word_ubin.norm_eq_iff [symmetric]) 3551 done 3552 3553lemma word_split_bl: "std = size c - size b \<Longrightarrow> 3554 (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow> 3555 word_split c = (a, b)" 3556 apply (rule iffI) 3557 defer 3558 apply (erule (1) word_split_bl') 3559 apply (case_tac "word_split c") 3560 apply (auto simp add: word_size) 3561 apply (frule word_split_bl' [rotated]) 3562 apply (auto simp add: word_size) 3563 done 3564 3565lemma word_split_bl_eq: 3566 "(word_split c :: ('c::len0 word \<times> 'd::len0 word)) = 3567 (of_bl (take (LENGTH('a::len) - LENGTH('d::len0)) (to_bl c)), 3568 of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))" 3569 for c :: "'a::len word" 3570 apply (rule word_split_bl [THEN iffD1]) 3571 apply (unfold word_size) 3572 apply (rule refl conjI)+ 3573 done 3574 3575\<comment> \<open>keep quantifiers for use in simplification\<close> 3576lemma test_bit_split': 3577 "word_split c = (a, b) \<longrightarrow> 3578 (\<forall>n m. 3579 b !! n = (n < size b \<and> c !! n) \<and> 3580 a !! m = (m < size a \<and> c !! (m + size b)))" 3581 apply (unfold word_split_bin' test_bit_bin) 3582 apply (clarify) 3583 apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits) 3584 apply (drule bin_nth_split) 3585 apply safe 3586 apply (simp_all add: add.commute) 3587 apply (erule bin_nth_uint_imp)+ 3588 done 3589 3590lemma test_bit_split: 3591 "word_split c = (a, b) \<Longrightarrow> 3592 (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> 3593 (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))" 3594 by (simp add: test_bit_split') 3595 3596lemma test_bit_split_eq: 3597 "word_split c = (a, b) \<longleftrightarrow> 3598 ((\<forall>n::nat. b !! n = (n < size b \<and> c !! n)) \<and> 3599 (\<forall>m::nat. a !! m = (m < size a \<and> c !! (m + size b))))" 3600 apply (rule_tac iffI) 3601 apply (rule_tac conjI) 3602 apply (erule test_bit_split [THEN conjunct1]) 3603 apply (erule test_bit_split [THEN conjunct2]) 3604 apply (case_tac "word_split c") 3605 apply (frule test_bit_split) 3606 apply (erule trans) 3607 apply (fastforce intro!: word_eqI simp add: word_size) 3608 done 3609 3610\<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>, 3611 result to the length given by the result type\<close> 3612 3613lemma word_cat_id: "word_cat a b = b" 3614 by (simp add: word_cat_bin' word_ubin.inverse_norm) 3615 3616\<comment> \<open>limited hom result\<close> 3617lemma word_cat_hom: 3618 "LENGTH('a::len0) \<le> LENGTH('b::len0) + LENGTH('c::len0) \<Longrightarrow> 3619 (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 3620 word_of_int (bin_cat w (size b) (uint b))" 3621 by (auto simp: word_cat_def word_size word_ubin.norm_eq_iff [symmetric] 3622 word_ubin.eq_norm bintr_cat min.absorb1) 3623 3624lemma word_cat_split_alt: "size w \<le> size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w" 3625 apply (rule word_eqI) 3626 apply (drule test_bit_split) 3627 apply (clarsimp simp add : test_bit_cat word_size) 3628 apply safe 3629 apply arith 3630 done 3631 3632lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]] 3633 3634 3635subsubsection \<open>Split and slice\<close> 3636 3637lemma split_slices: "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w \<and> v = slice 0 w" 3638 apply (drule test_bit_split) 3639 apply (rule conjI) 3640 apply (rule word_eqI, clarsimp simp: nth_slice word_size)+ 3641 done 3642 3643lemma slice_cat1 [OF refl]: 3644 "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a" 3645 apply safe 3646 apply (rule word_eqI) 3647 apply (simp add: nth_slice test_bit_cat word_size) 3648 done 3649 3650lemmas slice_cat2 = trans [OF slice_id word_cat_id] 3651 3652lemma cat_slices: 3653 "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow> 3654 size a + size b >= size c \<Longrightarrow> word_cat a b = c" 3655 apply safe 3656 apply (rule word_eqI) 3657 apply (simp add: nth_slice test_bit_cat word_size) 3658 apply safe 3659 apply arith 3660 done 3661 3662lemma word_split_cat_alt: 3663 "w = word_cat u v \<Longrightarrow> size u + size v \<le> size w \<Longrightarrow> word_split w = (u, v)" 3664 apply (case_tac "word_split w") 3665 apply (rule trans, assumption) 3666 apply (drule test_bit_split) 3667 apply safe 3668 apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+ 3669 done 3670 3671lemmas word_cat_bl_no_bin [simp] = 3672 word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral] 3673 for a b (* FIXME: negative numerals, 0 and 1 *) 3674 3675lemmas word_split_bl_no_bin [simp] = 3676 word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c 3677 3678text \<open> 3679 This odd result arises from the fact that the statement of the 3680 result implies that the decoded words are of the same type, 3681 and therefore of the same length, as the original word.\<close> 3682 3683lemma word_rsplit_same: "word_rsplit w = [w]" 3684 by (simp add: word_rsplit_def bin_rsplit_all) 3685 3686lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0" 3687 by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def 3688 split: prod.split) 3689 3690lemma test_bit_rsplit: 3691 "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow> 3692 k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)" 3693 for sw :: "'a::len word list" 3694 apply (unfold word_rsplit_def word_test_bit_def) 3695 apply (rule trans) 3696 apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong) 3697 apply (rule nth_map [symmetric]) 3698 apply simp 3699 apply (rule bin_nth_rsplit) 3700 apply simp_all 3701 apply (simp add : word_size rev_map) 3702 apply (rule trans) 3703 defer 3704 apply (rule map_ident [THEN fun_cong]) 3705 apply (rule refl [THEN map_cong]) 3706 apply (simp add : word_ubin.eq_norm) 3707 apply (erule bin_rsplit_size_sign [OF len_gt_0 refl]) 3708 done 3709 3710lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))" 3711 by (auto simp: word_rcat_def to_bl_def' of_bl_def bin_rcat_bl) 3712 3713lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)" 3714 by (induct wl) (auto simp: word_size) 3715 3716lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size] 3717 3718lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt] 3719 3720lemma nth_rcat_lem: 3721 "n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow> 3722 rev (concat (map to_bl wl)) ! n = 3723 rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))" 3724 apply (induct wl) 3725 apply clarsimp 3726 apply (clarsimp simp add : nth_append size_rcat_lem) 3727 apply (simp (no_asm_use) only: mult_Suc [symmetric] 3728 td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric]) 3729 apply clarsimp 3730 done 3731 3732lemma test_bit_rcat: 3733 "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n = 3734 (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))" 3735 for wl :: "'a::len word list" 3736 apply (unfold word_rcat_bl word_size) 3737 apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len) 3738 apply safe 3739 apply (auto simp: test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem]) 3740 done 3741 3742lemma foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0" 3743 for x :: "'a::comm_monoid_add" 3744 by (induct xs arbitrary: x) (auto simp: add.assoc) 3745 3746lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong] 3747 3748lemmas test_bit_rsplit_alt = 3749 trans [OF nth_rev_alt [THEN test_bit_cong] 3750 test_bit_rsplit [OF refl asm_rl diff_Suc_less]] 3751 3752\<comment> \<open>lazy way of expressing that u and v, and su and sv, have same types\<close> 3753lemma word_rsplit_len_indep [OF refl refl refl refl]: 3754 "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow> 3755 word_rsplit v = sv \<Longrightarrow> length su = length sv" 3756 by (auto simp: word_rsplit_def bin_rsplit_len_indep) 3757 3758lemma length_word_rsplit_size: 3759 "n = LENGTH('a::len) \<Longrightarrow> 3760 length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n" 3761 by (auto simp: word_rsplit_def word_size bin_rsplit_len_le) 3762 3763lemmas length_word_rsplit_lt_size = 3764 length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]] 3765 3766lemma length_word_rsplit_exp_size: 3767 "n = LENGTH('a::len) \<Longrightarrow> 3768 length (word_rsplit w :: 'a word list) = (size w + n - 1) div n" 3769 by (auto simp: word_rsplit_def word_size bin_rsplit_len) 3770 3771lemma length_word_rsplit_even_size: 3772 "n = LENGTH('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow> 3773 length (word_rsplit w :: 'a word list) = m" 3774 by (auto simp: length_word_rsplit_exp_size given_quot_alt) 3775 3776lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size] 3777 3778\<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close> 3779lemmas tdle = times_div_less_eq_dividend 3780lemmas dtle = xtr4 [OF tdle mult.commute] 3781 3782lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w" 3783 apply (rule word_eqI) 3784 apply (clarsimp simp: test_bit_rcat word_size) 3785 apply (subst refl [THEN test_bit_rsplit]) 3786 apply (simp_all add: word_size 3787 refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]]) 3788 apply safe 3789 apply (erule xtr7, rule dtle)+ 3790 done 3791 3792lemma size_word_rsplit_rcat_size: 3793 "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * LENGTH('a) 3794 \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws" 3795 for ws :: "'a::len word list" and frcw :: "'b::len0 word" 3796 apply (clarsimp simp: word_size length_word_rsplit_exp_size') 3797 apply (fast intro: given_quot_alt) 3798 done 3799 3800lemma msrevs: 3801 "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k" 3802 "(k * n + m) mod n = m mod n" 3803 for n :: nat 3804 by (auto simp: add.commute) 3805 3806lemma word_rsplit_rcat_size [OF refl]: 3807 "word_rcat ws = frcw \<Longrightarrow> 3808 size frcw = length ws * LENGTH('a) \<Longrightarrow> word_rsplit frcw = ws" 3809 for ws :: "'a::len word list" 3810 apply (frule size_word_rsplit_rcat_size, assumption) 3811 apply (clarsimp simp add : word_size) 3812 apply (rule nth_equalityI, assumption) 3813 apply clarsimp 3814 apply (rule word_eqI [rule_format]) 3815 apply (rule trans) 3816 apply (rule test_bit_rsplit_alt) 3817 apply (clarsimp simp: word_size)+ 3818 apply (rule trans) 3819 apply (rule test_bit_rcat [OF refl refl]) 3820 apply (simp add: word_size) 3821 apply (subst nth_rev) 3822 apply arith 3823 apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less]) 3824 apply safe 3825 apply (simp add: diff_mult_distrib) 3826 apply (rule mpl_lem) 3827 apply (cases "size ws") 3828 apply simp_all 3829 done 3830 3831 3832subsection \<open>Rotation\<close> 3833 3834lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified] 3835 3836lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def 3837 3838lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs" 3839 apply (rule box_equals) 3840 defer 3841 apply (rule rotate_conv_mod [symmetric])+ 3842 apply simp 3843 done 3844 3845lemmas rotate_eqs = 3846 trans [OF rotate0 [THEN fun_cong] id_apply] 3847 rotate_rotate [symmetric] 3848 rotate_id 3849 rotate_conv_mod 3850 rotate_eq_mod 3851 3852 3853subsubsection \<open>Rotation of list to right\<close> 3854 3855lemma rotate1_rl': "rotater1 (l @ [a]) = a # l" 3856 by (cases l) (auto simp: rotater1_def) 3857 3858lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l" 3859 apply (unfold rotater1_def) 3860 apply (cases "l") 3861 apply (case_tac [2] "list") 3862 apply auto 3863 done 3864 3865lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l" 3866 by (cases l) (auto simp: rotater1_def) 3867 3868lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)" 3869 by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl') 3870 3871lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)" 3872 by (induct n) (auto simp: rotater_def intro: rotater1_rev') 3873 3874lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))" 3875 using rotater_rev' [where xs = "rev ys"] by simp 3876 3877lemma rotater_drop_take: 3878 "rotater n xs = 3879 drop (length xs - n mod length xs) xs @ 3880 take (length xs - n mod length xs) xs" 3881 by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop) 3882 3883lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)" 3884 unfolding rotater_def by auto 3885 3886lemma rotate_inv_plus [rule_format] : 3887 "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and> 3888 rotate k (rotater n xs) = rotate m xs \<and> 3889 rotater n (rotate k xs) = rotate m xs \<and> 3890 rotate n (rotater k xs) = rotater m xs" 3891 by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans]) 3892 3893lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus] 3894 3895lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified] 3896 3897lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1] 3898lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1] 3899 3900lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs" 3901 by auto 3902 3903lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys" 3904 by auto 3905 3906lemma length_rotater [simp]: "length (rotater n xs) = length xs" 3907 by (simp add : rotater_rev) 3908 3909lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z" 3910 by simp 3911 3912lemmas rrs0 = rotate_eqs [THEN restrict_to_left, 3913 simplified rotate_gal [symmetric] rotate_gal' [symmetric]] 3914lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]] 3915lemmas rotater_eqs = rrs1 [simplified length_rotater] 3916lemmas rotater_0 = rotater_eqs (1) 3917lemmas rotater_add = rotater_eqs (2) 3918 3919 3920subsubsection \<open>map, map2, commuting with rotate(r)\<close> 3921 3922lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)" 3923 by (induct xs) auto 3924 3925lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" 3926 by (cases xs) (auto simp: rotater1_def last_map butlast_map) 3927 3928lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)" 3929 by (induct n) (auto simp: rotater_def rotater1_map) 3930 3931lemma but_last_zip [rule_format] : 3932 "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> 3933 last (zip xs ys) = (last xs, last ys) \<and> 3934 butlast (zip xs ys) = zip (butlast xs) (butlast ys)" 3935 apply (induct xs) 3936 apply auto 3937 apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+ 3938 done 3939 3940lemma but_last_map2 [rule_format] : 3941 "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> 3942 last (map2 f xs ys) = f (last xs) (last ys) \<and> 3943 butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)" 3944 apply (induct xs) 3945 apply auto 3946 apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+ 3947 done 3948 3949lemma rotater1_zip: 3950 "length xs = length ys \<Longrightarrow> 3951 rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 3952 apply (unfold rotater1_def) 3953 apply (cases xs) 3954 apply auto 3955 apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+ 3956 done 3957 3958lemma rotater1_map2: 3959 "length xs = length ys \<Longrightarrow> 3960 rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" 3961 by (simp add: rotater1_map rotater1_zip) 3962 3963lemmas lrth = 3964 box_equals [OF asm_rl length_rotater [symmetric] 3965 length_rotater [symmetric], 3966 THEN rotater1_map2] 3967 3968lemma rotater_map2: 3969 "length xs = length ys \<Longrightarrow> 3970 rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" 3971 by (induct n) (auto intro!: lrth) 3972 3973lemma rotate1_map2: 3974 "length xs = length ys \<Longrightarrow> 3975 rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 3976 by (cases xs; cases ys) auto 3977 3978lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] 3979 length_rotate [symmetric], THEN rotate1_map2] 3980 3981lemma rotate_map2: 3982 "length xs = length ys \<Longrightarrow> 3983 rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" 3984 by (induct n) (auto intro!: lth) 3985 3986 3987\<comment> \<open>corresponding equalities for word rotation\<close> 3988 3989lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)" 3990 by (simp add: word_bl.Abs_inverse' word_rotl_def) 3991 3992lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]] 3993 3994lemmas word_rotl_eqs = 3995 blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]] 3996 3997lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)" 3998 by (simp add: word_bl.Abs_inverse' word_rotr_def) 3999 4000lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]] 4001 4002lemmas word_rotr_eqs = 4003 brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]] 4004 4005declare word_rotr_eqs (1) [simp] 4006declare word_rotl_eqs (1) [simp] 4007 4008lemma word_rot_rl [simp]: "word_rotl k (word_rotr k v) = v" 4009 and word_rot_lr [simp]: "word_rotr k (word_rotl k v) = v" 4010 by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric]) 4011 4012lemma word_rot_gal: "word_rotr n v = w \<longleftrightarrow> word_rotl n w = v" 4013 and word_rot_gal': "w = word_rotr n v \<longleftrightarrow> v = word_rotl n w" 4014 by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] dest: sym) 4015 4016lemma word_rotr_rev: "word_rotr n w = word_reverse (word_rotl n (word_reverse w))" 4017 by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev to_bl_rotr to_bl_rotl rotater_rev) 4018 4019lemma word_roti_0 [simp]: "word_roti 0 w = w" 4020 by (auto simp: word_rot_defs) 4021 4022lemmas abl_cong = arg_cong [where f = "of_bl"] 4023 4024lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)" 4025proof - 4026 have rotater_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs" 4027 by auto 4028 4029 have rotate_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs" 4030 by auto 4031 4032 note rpts [symmetric] = 4033 rotate_inv_plus [THEN conjunct1] 4034 rotate_inv_plus [THEN conjunct2, THEN conjunct1] 4035 rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1] 4036 rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2] 4037 4038 note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem] 4039 note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem] 4040 4041 show ?thesis 4042 apply (unfold word_rot_defs) 4043 apply (simp only: split: if_split) 4044 apply (safe intro!: abl_cong) 4045 apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse'] 4046 to_bl_rotl 4047 to_bl_rotr [THEN word_bl.Rep_inverse'] 4048 to_bl_rotr) 4049 apply (rule rrp rrrp rpts, 4050 simp add: nat_add_distrib [symmetric] 4051 nat_diff_distrib [symmetric])+ 4052 done 4053qed 4054 4055lemma word_roti_conv_mod': 4056 "word_roti n w = word_roti (n mod int (size w)) w" 4057proof (cases "size w = 0") 4058 case True 4059 then show ?thesis 4060 by simp 4061next 4062 case False 4063 then have [simp]: "l mod int (size w) \<ge> 0" for l 4064 by simp 4065 then have *: "word_roti (n mod int (size w)) w = word_rotr (nat (n mod int (size w))) w" 4066 by (simp add: word_roti_def) 4067 show ?thesis 4068 proof (cases "n \<ge> 0") 4069 case True 4070 then show ?thesis 4071 apply (auto simp add: not_le *) 4072 apply (auto simp add: word_rot_defs) 4073 apply (safe intro!: abl_cong) 4074 apply (rule rotater_eqs) 4075 apply (simp add: word_size nat_mod_distrib) 4076 done 4077 next 4078 case False 4079 moreover define k where "k = - n" 4080 ultimately have n: "n = - k" 4081 by simp_all 4082 from False show ?thesis 4083 apply (auto simp add: not_le *) 4084 apply (auto simp add: word_rot_defs) 4085 apply (simp add: n) 4086 apply (safe intro!: abl_cong) 4087 apply (simp add: rotater_add [symmetric] rotate_gal [symmetric]) 4088 apply (rule rotater_eqs) 4089 apply (simp add: word_size [symmetric, of w]) 4090 apply (rule of_nat_eq_0_iff [THEN iffD1]) 4091 apply (auto simp add: nat_add_distrib [symmetric] mod_eq_0_iff_dvd) 4092 using dvd_nat_abs_iff [of "size w" "- k mod int (size w) + k"] 4093 apply (simp add: algebra_simps) 4094 apply (simp add: word_size) 4095 apply (metis (no_types, hide_lams) add.right_inverse dvd_0_right dvd_mod_imp_dvd dvd_refl minus_dvd_iff minus_equation_iff mod_0 mod_add_eq mod_minus_eq) 4096 done 4097 qed 4098qed 4099 4100lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size] 4101 4102 4103subsubsection \<open>"Word rotation commutes with bit-wise operations\<close> 4104 4105\<comment> \<open>using locale to not pollute lemma namespace\<close> 4106locale word_rotate 4107begin 4108 4109lemmas word_rot_defs' = to_bl_rotl to_bl_rotr 4110 4111lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor 4112 4113lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]] 4114 4115lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2 4116 4117lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v 4118 4119lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map 4120 4121lemma word_rot_logs: 4122 "word_rotl n (NOT v) = NOT (word_rotl n v)" 4123 "word_rotr n (NOT v) = NOT (word_rotr n v)" 4124 "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y" 4125 "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y" 4126 "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y" 4127 "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y" 4128 "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y" 4129 "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y" 4130 by (rule word_bl.Rep_eqD, 4131 rule word_rot_defs' [THEN trans], 4132 simp only: blwl_syms [symmetric], 4133 rule th1s [THEN trans], 4134 rule refl)+ 4135end 4136 4137lemmas word_rot_logs = word_rotate.word_rot_logs 4138 4139lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take, 4140 simplified word_bl_Rep'] 4141 4142lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take, 4143 simplified word_bl_Rep'] 4144 4145lemma bl_word_roti_dt': 4146 "n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow> 4147 to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)" 4148 apply (unfold word_roti_def) 4149 apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size) 4150 apply safe 4151 apply (simp add: zmod_zminus1_eq_if) 4152 apply safe 4153 apply (simp add: nat_mult_distrib) 4154 apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj 4155 [THEN conjunct2, THEN order_less_imp_le]] 4156 nat_mod_distrib) 4157 apply (simp add: nat_mod_distrib) 4158 done 4159 4160lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size] 4161 4162lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]] 4163lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]] 4164lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]] 4165 4166lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \<and> word_rotl i 0 = 0" 4167 by (simp add: word_rotr_dt word_rotl_dt replicate_add [symmetric]) 4168 4169lemma word_roti_0' [simp] : "word_roti n 0 = 0" 4170 by (auto simp: word_roti_def) 4171 4172lemmas word_rotr_dt_no_bin' [simp] = 4173 word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w 4174 (* FIXME: negative numerals, 0 and 1 *) 4175 4176lemmas word_rotl_dt_no_bin' [simp] = 4177 word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w 4178 (* FIXME: negative numerals, 0 and 1 *) 4179 4180declare word_roti_def [simp] 4181 4182 4183subsection \<open>Maximum machine word\<close> 4184 4185lemma word_int_cases: 4186 fixes x :: "'a::len0 word" 4187 obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^LENGTH('a)" 4188 by (cases x rule: word_uint.Abs_cases) (simp add: uints_num) 4189 4190lemma word_nat_cases [cases type: word]: 4191 fixes x :: "'a::len word" 4192 obtains n where "x = of_nat n" and "n < 2^LENGTH('a)" 4193 by (cases x rule: word_unat.Abs_cases) (simp add: unats_def) 4194 4195lemma max_word_eq: "(max_word::'a::len word) = 2^LENGTH('a) - 1" 4196 by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p) 4197 4198lemma max_word_max [simp,intro!]: "n \<le> max_word" 4199 by (cases n rule: word_int_cases) 4200 (simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1) 4201 4202lemma word_of_int_2p_len: "word_of_int (2 ^ LENGTH('a)) = (0::'a::len0 word)" 4203 by (subst word_uint.Abs_norm [symmetric]) simp 4204 4205lemma word_pow_0: "(2::'a::len word) ^ LENGTH('a) = 0" 4206proof - 4207 have "word_of_int (2 ^ LENGTH('a)) = (0::'a word)" 4208 by (rule word_of_int_2p_len) 4209 then show ?thesis by (simp add: word_of_int_2p) 4210qed 4211 4212lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word" 4213 apply (simp add: max_word_eq) 4214 apply uint_arith 4215 apply (auto simp: word_pow_0) 4216 done 4217 4218lemma max_word_minus: "max_word = (-1::'a::len word)" 4219proof - 4220 have "-1 + 1 = (0::'a word)" 4221 by simp 4222 then show ?thesis 4223 by (rule max_word_wrap [symmetric]) 4224qed 4225 4226lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (LENGTH('a)) True" 4227 by (subst max_word_minus to_bl_n1)+ simp 4228 4229lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < LENGTH('a)" 4230 by (auto simp: test_bit_bl word_size) 4231 4232lemma word_and_max [simp]: "x AND max_word = x" 4233 by (rule word_eqI) (simp add: word_ops_nth_size word_size) 4234 4235lemma word_or_max [simp]: "x OR max_word = max_word" 4236 by (rule word_eqI) (simp add: word_ops_nth_size word_size) 4237 4238lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z" 4239 for x y z :: "'a::len0 word" 4240 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) 4241 4242lemma word_oa_dist2: "x OR y AND z = (x OR y) AND (x OR z)" 4243 for x y z :: "'a::len0 word" 4244 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) 4245 4246lemma word_and_not [simp]: "x AND NOT x = 0" 4247 for x :: "'a::len0 word" 4248 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) 4249 4250lemma word_or_not [simp]: "x OR NOT x = max_word" 4251 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) 4252 4253global_interpretation word_bool_alg: boolean_algebra 4254 where conj = "(AND)" and disj = "(OR)" and compl = bitNOT 4255 and zero = 0 and one = max_word 4256 rewrites "word_bool_alg.xor = (XOR)" 4257proof - 4258 interpret boolean_algebra 4259 where conj = "(AND)" and disj = "(OR)" and compl = bitNOT 4260 and zero = 0 and one = max_word 4261 apply standard 4262 apply (simp_all add: word_bw_assocs word_bw_comms word_bw_lcs) 4263 apply (fact word_ao_dist2) 4264 apply (fact word_oa_dist2) 4265 done 4266 show "boolean_algebra (AND) (OR) bitNOT 0 max_word" .. 4267 show "xor = (XOR)" 4268 by (auto simp add: fun_eq_iff word_eq_iff xor_def word_ops_nth_size word_size) 4269qed 4270 4271lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y" 4272 for x y :: "'a::len0 word" 4273 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) 4274 4275lemma shiftr_x_0 [iff]: "x >> 0 = x" 4276 for x :: "'a::len0 word" 4277 by (simp add: shiftr_bl) 4278 4279lemma shiftl_x_0 [simp]: "x << 0 = x" 4280 for x :: "'a::len word" 4281 by (simp add: shiftl_t2n) 4282 4283lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n" 4284 by (simp add: shiftl_t2n) 4285 4286lemma uint_lt_0 [simp]: "uint x < 0 = False" 4287 by (simp add: linorder_not_less) 4288 4289lemma shiftr1_1 [simp]: "shiftr1 (1::'a::len word) = 0" 4290 unfolding shiftr1_def by simp 4291 4292lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)" 4293 by (induct n) (auto simp: shiftr_def) 4294 4295lemma word_less_1 [simp]: "x < 1 \<longleftrightarrow> x = 0" 4296 for x :: "'a::len word" 4297 by (simp add: word_less_nat_alt unat_0_iff) 4298 4299lemma to_bl_mask: 4300 "to_bl (mask n :: 'a::len word) = 4301 replicate (LENGTH('a) - n) False @ 4302 replicate (min (LENGTH('a)) n) True" 4303 by (simp add: mask_bl word_rep_drop min_def) 4304 4305lemma map_replicate_True: 4306 "n = length xs \<Longrightarrow> 4307 map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs" 4308 by (induct xs arbitrary: n) auto 4309 4310lemma map_replicate_False: 4311 "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y) 4312 (zip xs (replicate n False)) = replicate n False" 4313 by (induct xs arbitrary: n) auto 4314 4315lemma bl_and_mask: 4316 fixes w :: "'a::len word" 4317 and n :: nat 4318 defines "n' \<equiv> LENGTH('a) - n" 4319 shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)" 4320proof - 4321 note [simp] = map_replicate_True map_replicate_False 4322 have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))" 4323 by (simp add: bl_word_and) 4324 also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" 4325 by simp 4326 also have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) = 4327 replicate n' False @ drop n' (to_bl w)" 4328 unfolding to_bl_mask n'_def by (subst zip_append) auto 4329 finally show ?thesis . 4330qed 4331 4332lemma drop_rev_takefill: 4333 "length xs \<le> n \<Longrightarrow> 4334 drop (n - length xs) (rev (takefill False n (rev xs))) = xs" 4335 by (simp add: takefill_alt rev_take) 4336 4337lemma map_nth_0 [simp]: "map ((!!) (0::'a::len0 word)) xs = replicate (length xs) False" 4338 by (induct xs) auto 4339 4340lemma uint_plus_if_size: 4341 "uint (x + y) = 4342 (if uint x + uint y < 2^size x 4343 then uint x + uint y 4344 else uint x + uint y - 2^size x)" 4345 by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size) 4346 4347lemma unat_plus_if_size: 4348 "unat (x + y) = 4349 (if unat x + unat y < 2^size x 4350 then unat x + unat y 4351 else unat x + unat y - 2^size x)" 4352 for x y :: "'a::len word" 4353 apply (subst word_arith_nat_defs) 4354 apply (subst unat_of_nat) 4355 apply (simp add: mod_nat_add word_size) 4356 done 4357 4358lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w" 4359 for w :: "'a::len word" 4360 by (simp add: word_gt_0) 4361 4362lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c" 4363 for c :: "'a::len word" 4364 by (fact unat_div) 4365 4366lemma uint_sub_if_size: 4367 "uint (x - y) = 4368 (if uint y \<le> uint x 4369 then uint x - uint y 4370 else uint x - uint y + 2^size x)" 4371 by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size) 4372 4373lemma unat_sub: "b \<le> a \<Longrightarrow> unat (a - b) = unat a - unat b" 4374 by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib) 4375 4376lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w 4377lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w 4378 4379lemma word_of_int_minus: "word_of_int (2^LENGTH('a) - i) = (word_of_int (-i)::'a::len word)" 4380proof - 4381 have *: "2^LENGTH('a) - i = -i + 2^LENGTH('a)" 4382 by simp 4383 show ?thesis 4384 apply (subst *) 4385 apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2) 4386 apply simp 4387 done 4388qed 4389 4390lemmas word_of_int_inj = 4391 word_uint.Abs_inject [unfolded uints_num, simplified] 4392 4393lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y" 4394 for x y :: "'z::len word" 4395 by (auto simp add: order_class.le_less) 4396 4397lemma mod_plus_cong: 4398 fixes b b' :: int 4399 assumes 1: "b = b'" 4400 and 2: "x mod b' = x' mod b'" 4401 and 3: "y mod b' = y' mod b'" 4402 and 4: "x' + y' = z'" 4403 shows "(x + y) mod b = z' mod b'" 4404proof - 4405 from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'" 4406 by (simp add: mod_add_eq) 4407 also have "\<dots> = (x' + y') mod b'" 4408 by (simp add: mod_add_eq) 4409 finally show ?thesis 4410 by (simp add: 4) 4411qed 4412 4413lemma mod_minus_cong: 4414 fixes b b' :: int 4415 assumes "b = b'" 4416 and "x mod b' = x' mod b'" 4417 and "y mod b' = y' mod b'" 4418 and "x' - y' = z'" 4419 shows "(x - y) mod b = z' mod b'" 4420 using assms [symmetric] by (auto intro: mod_diff_cong) 4421 4422lemma word_induct_less: "P 0 \<Longrightarrow> (\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m" 4423 for P :: "'a::len word \<Rightarrow> bool" 4424 apply (cases m) 4425 apply atomize 4426 apply (erule rev_mp)+ 4427 apply (rule_tac x=m in spec) 4428 apply (induct_tac n) 4429 apply simp 4430 apply clarsimp 4431 apply (erule impE) 4432 apply clarsimp 4433 apply (erule_tac x=n in allE) 4434 apply (erule impE) 4435 apply (simp add: unat_arith_simps) 4436 apply (clarsimp simp: unat_of_nat) 4437 apply simp 4438 apply (erule_tac x="of_nat na" in allE) 4439 apply (erule impE) 4440 apply (simp add: unat_arith_simps) 4441 apply (clarsimp simp: unat_of_nat) 4442 apply simp 4443 done 4444 4445lemma word_induct: "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m" 4446 for P :: "'a::len word \<Rightarrow> bool" 4447 by (erule word_induct_less) simp 4448 4449lemma word_induct2 [induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n" 4450 for P :: "'b::len word \<Rightarrow> bool" 4451 apply (rule word_induct) 4452 apply simp 4453 apply (case_tac "1 + n = 0") 4454 apply auto 4455 done 4456 4457 4458subsection \<open>Recursion combinator for words\<close> 4459 4460definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" 4461 where "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)" 4462 4463lemma word_rec_0: "word_rec z s 0 = z" 4464 by (simp add: word_rec_def) 4465 4466lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)" 4467 for n :: "'a::len word" 4468 apply (simp add: word_rec_def unat_word_ariths) 4469 apply (subst nat_mod_eq') 4470 apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add) 4471 apply simp 4472 done 4473 4474lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))" 4475 apply (rule subst[where t="n" and s="1 + (n - 1)"]) 4476 apply simp 4477 apply (subst word_rec_Suc) 4478 apply simp 4479 apply simp 4480 done 4481 4482lemma word_rec_in: "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n" 4483 by (induct n) (simp_all add: word_rec_0 word_rec_Suc) 4484 4485lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> (+) 1) n" 4486 by (induct n) (simp_all add: word_rec_0 word_rec_Suc) 4487 4488lemma word_rec_twice: 4489 "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> (+) (n - m)) m" 4490 apply (erule rev_mp) 4491 apply (rule_tac x=z in spec) 4492 apply (rule_tac x=f in spec) 4493 apply (induct n) 4494 apply (simp add: word_rec_0) 4495 apply clarsimp 4496 apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst) 4497 apply simp 4498 apply (case_tac "1 + (n - m) = 0") 4499 apply (simp add: word_rec_0) 4500 apply (rule_tac f = "word_rec a b" for a b in arg_cong) 4501 apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst) 4502 apply simp 4503 apply (simp (no_asm_use)) 4504 apply (simp add: word_rec_Suc word_rec_in2) 4505 apply (erule impE) 4506 apply uint_arith 4507 apply (drule_tac x="x \<circ> (+) 1" in spec) 4508 apply (drule_tac x="x 0 xa" in spec) 4509 apply simp 4510 apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)" in subst) 4511 apply (clarsimp simp add: fun_eq_iff) 4512 apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst) 4513 apply simp 4514 apply (rule refl) 4515 apply (rule refl) 4516 done 4517 4518lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z" 4519 by (induct n) (auto simp add: word_rec_0 word_rec_Suc) 4520 4521lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z" 4522 apply (erule rev_mp) 4523 apply (induct n) 4524 apply (auto simp add: word_rec_0 word_rec_Suc) 4525 apply (drule spec, erule mp) 4526 apply uint_arith 4527 apply (drule_tac x=n in spec, erule impE) 4528 apply uint_arith 4529 apply simp 4530 done 4531 4532lemma word_rec_max: 4533 "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n" 4534 apply (subst word_rec_twice[where n="-1" and m="-1 - n"]) 4535 apply simp 4536 apply simp 4537 apply (rule word_rec_id_eq) 4538 apply clarsimp 4539 apply (drule spec, rule mp, erule mp) 4540 apply (rule word_plus_mono_right2[OF _ order_less_imp_le]) 4541 prefer 2 4542 apply assumption 4543 apply simp 4544 apply (erule contrapos_pn) 4545 apply simp 4546 apply (drule arg_cong[where f="\<lambda>x. x - n"]) 4547 apply simp 4548 done 4549 4550 4551subsection \<open>More\<close> 4552 4553lemma test_bit_1' [simp]: 4554 "(1 :: 'a :: len0 word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0" 4555 by (cases n) (simp_all only: one_word_def test_bit_wi bin_nth.simps, simp_all) 4556 4557lemma mask_0 [simp]: 4558 "mask 0 = 0" 4559 by (simp add: Word.mask_def) 4560 4561lemma shiftl0 [simp]: 4562 "x << 0 = (x :: 'a :: len0 word)" 4563 by (metis shiftl_rev shiftr_x_0 word_rev_gal) 4564 4565lemma mask_1: "mask 1 = 1" 4566 by (simp add: mask_def) 4567 4568lemma mask_Suc_0: "mask (Suc 0) = 1" 4569 by (simp add: mask_def) 4570 4571lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + 1" 4572 by (simp add: mask_def neg_numeral_class.sub_def numeral_eq_Suc numeral_pow) 4573 4574lemma bin_last_bintrunc: "bin_last (bintrunc l n) = (l > 0 \<and> bin_last n)" 4575 by (cases l) simp_all 4576 4577lemma word_and_1: 4578 "n AND 1 = (if n !! 0 then 1 else 0)" for n :: "_ word" 4579 by transfer (rule bin_rl_eqI, simp_all add: bin_rest_trunc bin_last_bintrunc) 4580 4581lemma bintrunc_shiftl: 4582 "bintrunc n (m << i) = bintrunc (n - i) m << i" 4583proof (induction i arbitrary: n) 4584 case 0 4585 show ?case 4586 by simp 4587next 4588 case (Suc i) 4589 then show ?case by (cases n) simp_all 4590qed 4591 4592lemma shiftl_transfer [transfer_rule]: 4593 includes lifting_syntax 4594 shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)" 4595 by (auto intro!: rel_funI word_eqI simp add: word.pcr_cr_eq cr_word_def word_size nth_shiftl) 4596 4597lemma uint_shiftl: 4598 "uint (n << i) = bintrunc (size n) (uint n << i)" 4599 unfolding word_size by transfer (simp add: bintrunc_shiftl) 4600 4601 4602subsection \<open>Misc\<close> 4603 4604declare bin_to_bl_def [simp] 4605 4606ML_file \<open>Tools/word_lib.ML\<close> 4607ML_file \<open>Tools/smt_word.ML\<close> 4608 4609hide_const (open) Word 4610 4611end 4612