src/HOL/SPARK/SPARK.thy
author haftmann
Wed Nov 13 19:12:15 2013 +0100 (2013-11-13)
changeset 54427 783861a66a60
parent 50788 fec14e8fefb8
child 63167 0909deb8059b
permissions -rw-r--r--
separated comparision on bit operations into separate theory
     1 (*  Title:      HOL/SPARK/SPARK.thy
     2     Author:     Stefan Berghofer
     3     Copyright:  secunet Security Networks AG
     4 
     5 Declaration of proof functions for SPARK/Ada verification environment.
     6 *)
     7 
     8 theory SPARK
     9 imports SPARK_Setup
    10 begin
    11 
    12 text {* Bitwise logical operators *}
    13 
    14 spark_proof_functions
    15   bit__and (integer, integer) : integer = "op AND"
    16   bit__or (integer, integer) : integer = "op OR"
    17   bit__xor (integer, integer) : integer = "op XOR"
    18 
    19 lemmas [simp] =
    20   OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
    21   OR_upper [of _ 8, simplified]
    22   OR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified]
    23   OR_upper [of _ 16, simplified]
    24   OR_upper [of _ 32, simplified zle_diff1_eq [symmetric], simplified]
    25   OR_upper [of _ 32, simplified]
    26   OR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
    27   OR_upper [of _ 64, simplified]
    28 
    29 lemmas [simp] =
    30   XOR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
    31   XOR_upper [of _ 8, simplified]
    32   XOR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified]
    33   XOR_upper [of _ 16, simplified]
    34   XOR_upper [of _ 32, simplified zle_diff1_eq [symmetric], simplified]
    35   XOR_upper [of _ 32, simplified]
    36   XOR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
    37   XOR_upper [of _ 64, simplified]
    38 
    39 lemma bit_not_spark_eq:
    40   "NOT (word_of_int x :: ('a::len0) word) =
    41   word_of_int (2 ^ len_of TYPE('a) - 1 - x)"
    42 proof -
    43   have "word_of_int x + NOT (word_of_int x) =
    44     word_of_int x + (word_of_int (2 ^ len_of TYPE('a) - 1 - x)::'a word)"
    45     by (simp only: bwsimps bin_add_not Min_def)
    46       (simp add: word_of_int_hom_syms word_of_int_2p_len)
    47   then show ?thesis by (rule add_left_imp_eq)
    48 qed
    49 
    50 lemmas [simp] =
    51   bit_not_spark_eq [where 'a=8, simplified]
    52   bit_not_spark_eq [where 'a=16, simplified]
    53   bit_not_spark_eq [where 'a=32, simplified]
    54   bit_not_spark_eq [where 'a=64, simplified]
    55 
    56 
    57 text {* Minimum and maximum *}
    58 
    59 spark_proof_functions
    60   integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int"
    61   integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
    62 
    63 end
    64