src/HOL/SPARK/SPARK.thy
author berghofe
Sat Jan 15 12:35:29 2011 +0100 (2011-01-15)
changeset 41561 d1318f3c86ba
child 47108 2a1953f0d20d
permissions -rw-r--r--
Added new SPARK verification environment.
     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 (simp add: Bit0_def int_or_Pls [unfolded Pls_def])
   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 (simp add: Bit0_def int_xor_Pls [unfolded Pls_def])
   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 (simp add: Pls_def)
   261 next
   262   case 2
   263   then show ?case
   264     by (simp, simp only: Min_def, 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 [unfolded Pls_def])
   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