src/HOL/SMT_Examples/SMT_Word_Examples.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 41601 fda8511006f9
child 47152 446cfc760ccf
permissions -rw-r--r--
Quotient_Info stores only relation maps
boehmes@36899
     1
(*  Title:      HOL/SMT_Examples/SMT_Word_Examples.thy
boehmes@36899
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36899
     3
*)
boehmes@36899
     4
boehmes@36899
     5
header {* Word examples for for SMT binding *}
boehmes@36899
     6
boehmes@36899
     7
theory SMT_Word_Examples
boehmes@36899
     8
imports Word
boehmes@36899
     9
begin
boehmes@36899
    10
boehmes@41601
    11
declare [[smt_oracle=true]]
boehmes@40513
    12
declare [[smt_certificates="SMT_Word_Examples.certs"]]
boehmes@36899
    13
declare [[smt_fixed=true]]
boehmes@36899
    14
boehmes@36899
    15
boehmes@36899
    16
boehmes@36899
    17
text {*
boehmes@36899
    18
Currently, there is no proof reconstruction for words.
boehmes@36899
    19
All lemmas are proved using the oracle mechanism.
boehmes@36899
    20
*}
boehmes@36899
    21
boehmes@36899
    22
boehmes@36899
    23
boehmes@36899
    24
section {* Bitvector numbers *}
boehmes@36899
    25
boehmes@36899
    26
lemma "(27 :: 4 word) = -5" by smt
boehmes@36899
    27
boehmes@36899
    28
lemma "(27 :: 4 word) = 11" by smt
boehmes@36899
    29
boehmes@36899
    30
lemma "23 < (27::8 word)" by smt
boehmes@36899
    31
boehmes@36899
    32
lemma "27 + 11 = (6::5 word)" by smt
boehmes@36899
    33
boehmes@36899
    34
lemma "7 * 3 = (21::8 word)" by smt
boehmes@36899
    35
boehmes@36899
    36
lemma "11 - 27 = (-16::8 word)" by smt
boehmes@36899
    37
boehmes@36899
    38
lemma "- -11 = (11::5 word)" by smt
boehmes@36899
    39
boehmes@36899
    40
lemma "-40 + 1 = (-39::7 word)" by smt
boehmes@36899
    41
boehmes@36899
    42
lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt
boehmes@36899
    43
boehmes@36899
    44
lemma "x = (5 :: 4 word) \<Longrightarrow> 4 * x = 4" by smt
boehmes@36899
    45
boehmes@36899
    46
boehmes@36899
    47
boehmes@36899
    48
section {* Bit-level logic *}
boehmes@36899
    49
boehmes@36899
    50
lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt
boehmes@36899
    51
boehmes@36899
    52
lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt
boehmes@36899
    53
boehmes@36899
    54
lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt
boehmes@36899
    55
boehmes@36899
    56
lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by smt
boehmes@36899
    57
boehmes@36899
    58
lemma "word_cat (27::4 word) (27::8 word) = (2843::12 word)" by smt
boehmes@36899
    59
boehmes@36899
    60
lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
boehmes@36899
    61
  by smt
boehmes@36899
    62
boehmes@36899
    63
lemma "slice 1 (0b10110 :: 4 word) = (0b11 :: 2 word)" by smt
boehmes@36899
    64
boehmes@36899
    65
lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt
boehmes@36899
    66
boehmes@36899
    67
lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt
boehmes@36899
    68
boehmes@41282
    69
lemma "0b10011 << 2 = (0b1001100::8 word)" by smt
boehmes@36899
    70
boehmes@41282
    71
lemma "0b11001 >> 2 = (0b110::8 word)" by smt
boehmes@36899
    72
boehmes@41282
    73
lemma "0b10011 >>> 2 = (0b100::8 word)" by smt
boehmes@36899
    74
boehmes@36899
    75
lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt
boehmes@36899
    76
boehmes@36899
    77
lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt
boehmes@36899
    78
boehmes@36899
    79
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt
boehmes@36899
    80
boehmes@36899
    81
lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt
boehmes@36899
    82
boehmes@36899
    83
boehmes@36899
    84
boehmes@36899
    85
section {* Combined integer-bitvector properties *}
boehmes@36899
    86
boehmes@36899
    87
lemma
boehmes@36899
    88
  assumes "bv2int 0 = 0"
boehmes@36899
    89
      and "bv2int 1 = 1"
boehmes@36899
    90
      and "bv2int 2 = 2"
boehmes@36899
    91
      and "bv2int 3 = 3"
boehmes@36899
    92
      and "\<forall>x::2 word. bv2int x > 0"
boehmes@36899
    93
  shows "\<forall>i::int. i < 0 \<longrightarrow> (\<forall>x::2 word. bv2int x > i)"
boehmes@36899
    94
  using assms
boehmes@36899
    95
  using [[z3_options="AUTO_CONFIG=false"]]
boehmes@36899
    96
  by smt
boehmes@36899
    97
boehmes@36899
    98
lemma "P (0 \<le> (a :: 4 word)) = P True" by smt
boehmes@36899
    99
boehmes@36899
   100
end