src/HOL/SPARK/SPARK.thy
author huffman
Sun Mar 25 20:15:39 2012 +0200 (2012-03-25)
changeset 47108 2a1953f0d20d
parent 41561 d1318f3c86ba
child 50788 fec14e8fefb8
permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
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
berghofe@41561
    12
text {* Bitwise logical operators *}
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
lemma AND_lower [simp]:
berghofe@41561
    20
  fixes x :: int and y :: int
berghofe@41561
    21
  assumes "0 \<le> x"
berghofe@41561
    22
  shows "0 \<le> x AND y"
berghofe@41561
    23
  using assms
berghofe@41561
    24
proof (induct x arbitrary: y rule: bin_induct)
berghofe@41561
    25
  case (3 bin bit)
berghofe@41561
    26
  show ?case
berghofe@41561
    27
  proof (cases y rule: bin_exhaust)
berghofe@41561
    28
    case (1 bin' bit')
berghofe@41561
    29
    from 3 have "0 \<le> bin"
berghofe@41561
    30
      by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
    31
    then have "0 \<le> bin AND bin'" by (rule 3)
berghofe@41561
    32
    with 1 show ?thesis
berghofe@41561
    33
      by simp (simp add: Bit_def bitval_def split add: bit.split)
berghofe@41561
    34
  qed
berghofe@41561
    35
next
berghofe@41561
    36
  case 2
berghofe@41561
    37
  then show ?case by (simp only: Min_def)
berghofe@41561
    38
qed simp
berghofe@41561
    39
berghofe@41561
    40
lemma OR_lower [simp]:
berghofe@41561
    41
  fixes x :: int and y :: int
berghofe@41561
    42
  assumes "0 \<le> x" "0 \<le> y"
berghofe@41561
    43
  shows "0 \<le> x OR y"
berghofe@41561
    44
  using assms
berghofe@41561
    45
proof (induct x arbitrary: y rule: bin_induct)
berghofe@41561
    46
  case (3 bin bit)
berghofe@41561
    47
  show ?case
berghofe@41561
    48
  proof (cases y rule: bin_exhaust)
berghofe@41561
    49
    case (1 bin' bit')
berghofe@41561
    50
    from 3 have "0 \<le> bin"
berghofe@41561
    51
      by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
    52
    moreover from 1 3 have "0 \<le> bin'"
berghofe@41561
    53
      by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
    54
    ultimately have "0 \<le> bin OR bin'" by (rule 3)
berghofe@41561
    55
    with 1 show ?thesis
berghofe@41561
    56
      by simp (simp add: Bit_def bitval_def split add: bit.split)
berghofe@41561
    57
  qed
berghofe@41561
    58
qed simp_all
berghofe@41561
    59
berghofe@41561
    60
lemma XOR_lower [simp]:
berghofe@41561
    61
  fixes x :: int and y :: int
berghofe@41561
    62
  assumes "0 \<le> x" "0 \<le> y"
berghofe@41561
    63
  shows "0 \<le> x XOR y"
berghofe@41561
    64
  using assms
berghofe@41561
    65
proof (induct x arbitrary: y rule: bin_induct)
berghofe@41561
    66
  case (3 bin bit)
berghofe@41561
    67
  show ?case
berghofe@41561
    68
  proof (cases y rule: bin_exhaust)
berghofe@41561
    69
    case (1 bin' bit')
berghofe@41561
    70
    from 3 have "0 \<le> bin"
berghofe@41561
    71
      by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
    72
    moreover from 1 3 have "0 \<le> bin'"
berghofe@41561
    73
      by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
    74
    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
berghofe@41561
    75
    with 1 show ?thesis
berghofe@41561
    76
      by simp (simp add: Bit_def bitval_def split add: bit.split)
berghofe@41561
    77
  qed
berghofe@41561
    78
next
berghofe@41561
    79
  case 2
berghofe@41561
    80
  then show ?case by (simp only: Min_def)
berghofe@41561
    81
qed simp
berghofe@41561
    82
berghofe@41561
    83
lemma AND_upper1 [simp]:
berghofe@41561
    84
  fixes x :: int and y :: int
berghofe@41561
    85
  assumes "0 \<le> x"
berghofe@41561
    86
  shows "x AND y \<le> x"
berghofe@41561
    87
  using assms
berghofe@41561
    88
proof (induct x arbitrary: y rule: bin_induct)
berghofe@41561
    89
  case (3 bin bit)
berghofe@41561
    90
  show ?case
berghofe@41561
    91
  proof (cases y rule: bin_exhaust)
berghofe@41561
    92
    case (1 bin' bit')
berghofe@41561
    93
    from 3 have "0 \<le> bin"
berghofe@41561
    94
      by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
    95
    then have "bin AND bin' \<le> bin" by (rule 3)
berghofe@41561
    96
    with 1 show ?thesis
berghofe@41561
    97
      by simp (simp add: Bit_def bitval_def split add: bit.split)
berghofe@41561
    98
  qed
berghofe@41561
    99
next
berghofe@41561
   100
  case 2
berghofe@41561
   101
  then show ?case by (simp only: Min_def)
berghofe@41561
   102
qed simp
berghofe@41561
   103
berghofe@41561
   104
lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
berghofe@41561
   105
lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
berghofe@41561
   106
berghofe@41561
   107
lemma AND_upper2 [simp]:
berghofe@41561
   108
  fixes x :: int and y :: int
berghofe@41561
   109
  assumes "0 \<le> y"
berghofe@41561
   110
  shows "x AND y \<le> y"
berghofe@41561
   111
  using assms
berghofe@41561
   112
proof (induct y arbitrary: x rule: bin_induct)
berghofe@41561
   113
  case (3 bin bit)
berghofe@41561
   114
  show ?case
berghofe@41561
   115
  proof (cases x rule: bin_exhaust)
berghofe@41561
   116
    case (1 bin' bit')
berghofe@41561
   117
    from 3 have "0 \<le> bin"
berghofe@41561
   118
      by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
   119
    then have "bin' AND bin \<le> bin" by (rule 3)
berghofe@41561
   120
    with 1 show ?thesis
berghofe@41561
   121
      by simp (simp add: Bit_def bitval_def split add: bit.split)
berghofe@41561
   122
  qed
berghofe@41561
   123
next
berghofe@41561
   124
  case 2
berghofe@41561
   125
  then show ?case by (simp only: Min_def)
berghofe@41561
   126
qed simp
berghofe@41561
   127
berghofe@41561
   128
lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
berghofe@41561
   129
lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
berghofe@41561
   130
berghofe@41561
   131
lemma OR_upper:
berghofe@41561
   132
  fixes x :: int and y :: int
berghofe@41561
   133
  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
berghofe@41561
   134
  shows "x OR y < 2 ^ n"
berghofe@41561
   135
  using assms
berghofe@41561
   136
proof (induct x arbitrary: y n rule: bin_induct)
berghofe@41561
   137
  case (3 bin bit)
berghofe@41561
   138
  show ?case
berghofe@41561
   139
  proof (cases y rule: bin_exhaust)
berghofe@41561
   140
    case (1 bin' bit')
berghofe@41561
   141
    show ?thesis
berghofe@41561
   142
    proof (cases n)
berghofe@41561
   143
      case 0
berghofe@41561
   144
      with 3 have "bin BIT bit = 0" by simp
berghofe@41561
   145
      then have "bin = 0" "bit = 0"
berghofe@41561
   146
        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
berghofe@41561
   147
      then show ?thesis using 0 1 `y < 2 ^ n`
huffman@47108
   148
        by simp
berghofe@41561
   149
    next
berghofe@41561
   150
      case (Suc m)
berghofe@41561
   151
      from 3 have "0 \<le> bin"
berghofe@41561
   152
        by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
   153
      moreover from 3 Suc have "bin < 2 ^ m"
berghofe@41561
   154
        by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
   155
      moreover from 1 3 Suc have "bin' < 2 ^ m"
berghofe@41561
   156
        by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
   157
      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
berghofe@41561
   158
      with 1 Suc show ?thesis
berghofe@41561
   159
        by simp (simp add: Bit_def bitval_def split add: bit.split)
berghofe@41561
   160
    qed
berghofe@41561
   161
  qed
berghofe@41561
   162
qed simp_all
berghofe@41561
   163
berghofe@41561
   164
lemmas [simp] =
berghofe@41561
   165
  OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
berghofe@41561
   166
  OR_upper [of _ 8, simplified]
berghofe@41561
   167
  OR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified]
berghofe@41561
   168
  OR_upper [of _ 16, simplified]
berghofe@41561
   169
  OR_upper [of _ 32, simplified zle_diff1_eq [symmetric], simplified]
berghofe@41561
   170
  OR_upper [of _ 32, simplified]
berghofe@41561
   171
  OR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
berghofe@41561
   172
  OR_upper [of _ 64, simplified]
berghofe@41561
   173
berghofe@41561
   174
lemma XOR_upper:
berghofe@41561
   175
  fixes x :: int and y :: int
berghofe@41561
   176
  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
berghofe@41561
   177
  shows "x XOR y < 2 ^ n"
berghofe@41561
   178
  using assms
berghofe@41561
   179
proof (induct x arbitrary: y n rule: bin_induct)
berghofe@41561
   180
  case (3 bin bit)
berghofe@41561
   181
  show ?case
berghofe@41561
   182
  proof (cases y rule: bin_exhaust)
berghofe@41561
   183
    case (1 bin' bit')
berghofe@41561
   184
    show ?thesis
berghofe@41561
   185
    proof (cases n)
berghofe@41561
   186
      case 0
berghofe@41561
   187
      with 3 have "bin BIT bit = 0" by simp
berghofe@41561
   188
      then have "bin = 0" "bit = 0"
berghofe@41561
   189
        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
berghofe@41561
   190
      then show ?thesis using 0 1 `y < 2 ^ n`
huffman@47108
   191
        by simp
berghofe@41561
   192
    next
berghofe@41561
   193
      case (Suc m)
berghofe@41561
   194
      from 3 have "0 \<le> bin"
berghofe@41561
   195
        by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
   196
      moreover from 3 Suc have "bin < 2 ^ m"
berghofe@41561
   197
        by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
   198
      moreover from 1 3 Suc have "bin' < 2 ^ m"
berghofe@41561
   199
        by (simp add: Bit_def bitval_def split add: bit.split_asm)
berghofe@41561
   200
      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
berghofe@41561
   201
      with 1 Suc show ?thesis
berghofe@41561
   202
        by simp (simp add: Bit_def bitval_def split add: bit.split)
berghofe@41561
   203
    qed
berghofe@41561
   204
  qed
berghofe@41561
   205
next
berghofe@41561
   206
  case 2
berghofe@41561
   207
  then show ?case by (simp only: Min_def)
berghofe@41561
   208
qed simp
berghofe@41561
   209
berghofe@41561
   210
lemmas [simp] =
berghofe@41561
   211
  XOR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
berghofe@41561
   212
  XOR_upper [of _ 8, simplified]
berghofe@41561
   213
  XOR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified]
berghofe@41561
   214
  XOR_upper [of _ 16, simplified]
berghofe@41561
   215
  XOR_upper [of _ 32, simplified zle_diff1_eq [symmetric], simplified]
berghofe@41561
   216
  XOR_upper [of _ 32, simplified]
berghofe@41561
   217
  XOR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
berghofe@41561
   218
  XOR_upper [of _ 64, simplified]
berghofe@41561
   219
berghofe@41561
   220
lemma bit_not_spark_eq:
berghofe@41561
   221
  "NOT (word_of_int x :: ('a::len0) word) =
berghofe@41561
   222
  word_of_int (2 ^ len_of TYPE('a) - 1 - x)"
berghofe@41561
   223
proof -
berghofe@41561
   224
  have "word_of_int x + NOT (word_of_int x) =
berghofe@41561
   225
    word_of_int x + (word_of_int (2 ^ len_of TYPE('a) - 1 - x)::'a word)"
berghofe@41561
   226
    by (simp only: bwsimps bin_add_not Min_def)
berghofe@41561
   227
      (simp add: word_of_int_hom_syms word_of_int_2p_len)
berghofe@41561
   228
  then show ?thesis by (rule add_left_imp_eq)
berghofe@41561
   229
qed
berghofe@41561
   230
berghofe@41561
   231
lemmas [simp] =
berghofe@41561
   232
  bit_not_spark_eq [where 'a=8, simplified]
berghofe@41561
   233
  bit_not_spark_eq [where 'a=16, simplified]
berghofe@41561
   234
  bit_not_spark_eq [where 'a=32, simplified]
berghofe@41561
   235
  bit_not_spark_eq [where 'a=64, simplified]
berghofe@41561
   236
berghofe@41561
   237
lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
berghofe@41561
   238
  unfolding Bit_B1
berghofe@41561
   239
  by (induct n) simp_all
berghofe@41561
   240
berghofe@41561
   241
lemma mod_BIT:
berghofe@41561
   242
  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
berghofe@41561
   243
proof -
berghofe@41561
   244
  have "bin mod 2 ^ n < 2 ^ n" by simp
berghofe@41561
   245
  then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
berghofe@41561
   246
  then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
berghofe@41561
   247
    by (rule mult_left_mono) simp
berghofe@41561
   248
  then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
berghofe@41561
   249
  then show ?thesis
berghofe@41561
   250
    by (auto simp add: Bit_def bitval_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
berghofe@41561
   251
      mod_pos_pos_trivial split add: bit.split)
berghofe@41561
   252
qed
berghofe@41561
   253
berghofe@41561
   254
lemma AND_mod:
berghofe@41561
   255
  fixes x :: int
berghofe@41561
   256
  shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
berghofe@41561
   257
proof (induct x arbitrary: n rule: bin_induct)
berghofe@41561
   258
  case 1
berghofe@41561
   259
  then show ?case
huffman@47108
   260
    by simp
berghofe@41561
   261
next
berghofe@41561
   262
  case 2
berghofe@41561
   263
  then show ?case
huffman@47108
   264
    by (simp, simp add: m1mod2k)
berghofe@41561
   265
next
berghofe@41561
   266
  case (3 bin bit)
berghofe@41561
   267
  show ?case
berghofe@41561
   268
  proof (cases n)
berghofe@41561
   269
    case 0
huffman@47108
   270
    then show ?thesis by (simp add: int_and_extra_simps)
berghofe@41561
   271
  next
berghofe@41561
   272
    case (Suc m)
berghofe@41561
   273
    with 3 show ?thesis
berghofe@41561
   274
      by (simp only: power_BIT mod_BIT int_and_Bits) simp
berghofe@41561
   275
  qed
berghofe@41561
   276
qed
berghofe@41561
   277
berghofe@41561
   278
end