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