Quelle Word_Computations.thy Sprache: Isabelle

(* Author: Florian Haftmann, TU Muenchen *)

section \<open>Tests for simplifying word operations on ground terms\<close>

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 = \<open>16 word\<close>
type_synonym word32 = \<open>32 word\<close>

definition computations_arith where
  [eval]: \<open>computations_arith = (
    [473514 + - 763, - 5324 - 7892 :: word16],
    [3131 * - 42, - 2342 div 1213, 2152 mod - 235 :: word16],
    [12323 \<le> (- 12132 :: word16), - 123 < (321312 :: word16), 12323 \<le>s (- 12132 :: word16), - 123 <s (321312 :: word16)]
  )\<close>

definition results_arith where
  [eval]: \<open>results_arith = (
    [472751, - 13216 :: word16],
    [- 131502, 52, 2152 :: word16],
    [True, False, False, False]
  )\<close>

lemma \<open>computations_arith = results_arith\<close>
  by (simp add: eval)

definition computations_bit where
  [eval]: \<open>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]
  )\<close>

definition results_bit where
  [eval]: \<open>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]
  )\<close>

lemma \<open>computations_bit = results_bit\<close>
  by (simp add: eval)

definition computations_ranges where
  \<open>computations_ranges = [
    \<forall>w :: word16 \<in> {0..31}. (w AND 63) = (w AND 31),
    \<forall>w :: word32 \<in> {0..31}. (w AND 63) = (w AND 31)
  ]\<close>

definition results_ranges where
  \<open>results_ranges = [
    True,
    True
  ]\<close>

lemma \<open>computations_ranges = results_ranges\<close>
  by eval

end

quality100%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.