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