src/HOL/SPARK/SPARK.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 47108 2a1953f0d20d child 50788 fec14e8fefb8 permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
1 (*  Title:      HOL/SPARK/SPARK.thy
2     Author:     Stefan Berghofer
3     Copyright:  secunet Security Networks AG
5 Declaration of proof functions for SPARK/Ada verification environment.
6 *)
8 theory SPARK
9 imports SPARK_Setup
10 begin
12 text {* Bitwise logical operators *}
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"
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
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
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
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
104 lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
105 lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
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
128 lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
129 lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
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
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]
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
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]
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
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]
237 lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
238   unfolding Bit_B1
239   by (induct n) simp_all
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
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
278 end