Quelle  Word_Computations.thy

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Tests for simplifying word operations on ground terms›

theory Word_Computations
  imports
    "HOL.Bit_Operations"
    "HOL-Library.Word"
begin

unbundle bit_operations_syntax

named_theorems eval

declare mask_numeral [eval]

type_synonym word16 = ‹16 word›
type_synonym word32 = ‹32 word›

definition computations_arith where
  [eval]: ‹computations_arith = (
  [473514 + - 763, - 5324 - 7892 :: word16],
  [3131 * - 42, - 2342 div 1213, 2152 mod - 235 :: word16],
  [12323 ≤ (- 12132 :: word16), - 123 🚫321312 :: word16), 12323 ≤s (- 12132 :: word16), - 123 🚫(321312 :: word16)]
  )›

definition results_arith where
  [eval]: ‹results_arith = (
  [472751, - 13216 :: word16],
  [- 131502, 52, 2152 :: word16],
  [True, False, False, False]
  )›

lemma ‹computations_arith = results_arith›
  by (simp add: eval)
 
definition computations_bit where
  [eval]: ‹computations_bit = (
  [bit (473514 :: word16) 5, bit (- 805167 :: word16) 7],
  [NOT 473513, NOT (- 805167) :: word16],
  [473514 AND 767063, - 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: word16],
  [473514 OR 767063, - 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: word16],
  [473514 XOR 767063, - 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: word16],
  mask 11 :: word16,
  [set_bit 15 473514, set_bit 11 (- 805167) :: word16],
  [unset_bit 13 473514, unset_bit 12 (- 805167) :: word16],
  [flip_bit 15 473514, flip_bit 12 (- 805167) :: word16],
  [push_bit 12 473514, push_bit 12 (- 805167) :: word16],
  [drop_bit 12 65344, drop_bit 12 (- 17405) :: word16],
  [signed_drop_bit 12 (- 17405) :: word16],
  [take_bit 12 473514, take_bit 12 (- 805167) :: word16],
  [signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: word16]
  )›

definition results_bit where
  [eval]: ‹results_bit = (
  [True, True],
  [- 473514, 805166 :: word16],
  [208898, 242769, 209184, - 839103 :: word16],
  [1031679, - 280873, - 50197, - 280591 :: word16],
  [822781, - 523642, - 259381, 558512 :: word16],
  2047 :: word16,
  [506282, - 803119 :: word16],
  [465322, - 809263 :: word16],
  [506282, - 809263 :: word16],
  [1939513344, - 3297964032 :: word16],
  [15, 11 :: word16],
  [- 5 :: word16],
  [2474, 1745 :: word16],
  [- 1622, - 2351 :: word16]
  )›

lemma ‹computations_bit = results_bit›
  by (simp add: eval)

definition computations_ranges where
  ‹computations_ranges = [
  ∀w :: word16 ∈ {0..31}. (w AND 63) = (w AND 31),
  ∀w :: word32 ∈ {0..31}. (w AND 63) = (w AND 31)
  ]›

definition results_ranges where
  ‹results_ranges = [
  True,
  True
  ]›

lemma ‹computations_ranges = results_ranges›
  by eval

end