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