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