--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/SPARK.thy Sat Jan 15 12:35:29 2011 +0100
@@ -0,0 +1,278 @@
+(* Title: HOL/SPARK/SPARK.thy
+ Author: Stefan Berghofer
+ Copyright: secunet Security Networks AG
+
+Declaration of proof functions for SPARK/Ada verification environment.
+*)
+
+theory SPARK
+imports SPARK_Setup
+begin
+
+text {* Bitwise logical operators *}
+
+spark_proof_functions
+ bit__and (integer, integer) : integer = "op AND"
+ bit__or (integer, integer) : integer = "op OR"
+ bit__xor (integer, integer) : integer = "op XOR"
+
+lemma AND_lower [simp]:
+ fixes x :: int and y :: int
+ assumes "0 \<le> x"
+ shows "0 \<le> x AND y"
+ using assms
+proof (induct x arbitrary: y rule: bin_induct)
+ case (3 bin bit)
+ show ?case
+ proof (cases y rule: bin_exhaust)
+ case (1 bin' bit')
+ from 3 have "0 \<le> bin"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ then have "0 \<le> bin AND bin'" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def bitval_def split add: bit.split)
+ qed
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+qed simp
+
+lemma OR_lower [simp]:
+ fixes x :: int and y :: int
+ assumes "0 \<le> x" "0 \<le> y"
+ shows "0 \<le> x OR y"
+ using assms
+proof (induct x arbitrary: y rule: bin_induct)
+ case (3 bin bit)
+ show ?case
+ proof (cases y rule: bin_exhaust)
+ case (1 bin' bit')
+ from 3 have "0 \<le> bin"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ moreover from 1 3 have "0 \<le> bin'"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ ultimately have "0 \<le> bin OR bin'" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def bitval_def split add: bit.split)
+ qed
+qed simp_all
+
+lemma XOR_lower [simp]:
+ fixes x :: int and y :: int
+ assumes "0 \<le> x" "0 \<le> y"
+ shows "0 \<le> x XOR y"
+ using assms
+proof (induct x arbitrary: y rule: bin_induct)
+ case (3 bin bit)
+ show ?case
+ proof (cases y rule: bin_exhaust)
+ case (1 bin' bit')
+ from 3 have "0 \<le> bin"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ moreover from 1 3 have "0 \<le> bin'"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ ultimately have "0 \<le> bin XOR bin'" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def bitval_def split add: bit.split)
+ qed
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+qed simp
+
+lemma AND_upper1 [simp]:
+ fixes x :: int and y :: int
+ assumes "0 \<le> x"
+ shows "x AND y \<le> x"
+ using assms
+proof (induct x arbitrary: y rule: bin_induct)
+ case (3 bin bit)
+ show ?case
+ proof (cases y rule: bin_exhaust)
+ case (1 bin' bit')
+ from 3 have "0 \<le> bin"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ then have "bin AND bin' \<le> bin" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def bitval_def split add: bit.split)
+ qed
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+qed simp
+
+lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
+lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
+
+lemma AND_upper2 [simp]:
+ fixes x :: int and y :: int
+ assumes "0 \<le> y"
+ shows "x AND y \<le> y"
+ using assms
+proof (induct y arbitrary: x rule: bin_induct)
+ case (3 bin bit)
+ show ?case
+ proof (cases x rule: bin_exhaust)
+ case (1 bin' bit')
+ from 3 have "0 \<le> bin"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ then have "bin' AND bin \<le> bin" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def bitval_def split add: bit.split)
+ qed
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+qed simp
+
+lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
+lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
+
+lemma OR_upper:
+ fixes x :: int and y :: int
+ assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
+ shows "x OR y < 2 ^ n"
+ using assms
+proof (induct x arbitrary: y n rule: bin_induct)
+ case (3 bin bit)
+ show ?case
+ proof (cases y rule: bin_exhaust)
+ case (1 bin' bit')
+ show ?thesis
+ proof (cases n)
+ case 0
+ with 3 have "bin BIT bit = 0" by simp
+ then have "bin = 0" "bit = 0"
+ by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
+ then show ?thesis using 0 1 `y < 2 ^ n`
+ by simp (simp add: Bit0_def int_or_Pls [unfolded Pls_def])
+ next
+ case (Suc m)
+ from 3 have "0 \<le> bin"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ moreover from 3 Suc have "bin < 2 ^ m"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ moreover from 1 3 Suc have "bin' < 2 ^ m"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
+ with 1 Suc show ?thesis
+ by simp (simp add: Bit_def bitval_def split add: bit.split)
+ qed
+ qed
+qed simp_all
+
+lemmas [simp] =
+ OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
+ OR_upper [of _ 8, simplified]
+ OR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified]
+ OR_upper [of _ 16, simplified]
+ OR_upper [of _ 32, simplified zle_diff1_eq [symmetric], simplified]
+ OR_upper [of _ 32, simplified]
+ OR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
+ OR_upper [of _ 64, simplified]
+
+lemma XOR_upper:
+ fixes x :: int and y :: int
+ assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
+ shows "x XOR y < 2 ^ n"
+ using assms
+proof (induct x arbitrary: y n rule: bin_induct)
+ case (3 bin bit)
+ show ?case
+ proof (cases y rule: bin_exhaust)
+ case (1 bin' bit')
+ show ?thesis
+ proof (cases n)
+ case 0
+ with 3 have "bin BIT bit = 0" by simp
+ then have "bin = 0" "bit = 0"
+ by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
+ then show ?thesis using 0 1 `y < 2 ^ n`
+ by simp (simp add: Bit0_def int_xor_Pls [unfolded Pls_def])
+ next
+ case (Suc m)
+ from 3 have "0 \<le> bin"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ moreover from 3 Suc have "bin < 2 ^ m"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ moreover from 1 3 Suc have "bin' < 2 ^ m"
+ by (simp add: Bit_def bitval_def split add: bit.split_asm)
+ ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
+ with 1 Suc show ?thesis
+ by simp (simp add: Bit_def bitval_def split add: bit.split)
+ qed
+ qed
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+qed simp
+
+lemmas [simp] =
+ XOR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
+ XOR_upper [of _ 8, simplified]
+ XOR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified]
+ XOR_upper [of _ 16, simplified]
+ XOR_upper [of _ 32, simplified zle_diff1_eq [symmetric], simplified]
+ XOR_upper [of _ 32, simplified]
+ XOR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
+ XOR_upper [of _ 64, simplified]
+
+lemma bit_not_spark_eq:
+ "NOT (word_of_int x :: ('a::len0) word) =
+ word_of_int (2 ^ len_of TYPE('a) - 1 - x)"
+proof -
+ have "word_of_int x + NOT (word_of_int x) =
+ word_of_int x + (word_of_int (2 ^ len_of TYPE('a) - 1 - x)::'a word)"
+ by (simp only: bwsimps bin_add_not Min_def)
+ (simp add: word_of_int_hom_syms word_of_int_2p_len)
+ then show ?thesis by (rule add_left_imp_eq)
+qed
+
+lemmas [simp] =
+ bit_not_spark_eq [where 'a=8, simplified]
+ bit_not_spark_eq [where 'a=16, simplified]
+ bit_not_spark_eq [where 'a=32, simplified]
+ bit_not_spark_eq [where 'a=64, simplified]
+
+lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
+ unfolding Bit_B1
+ by (induct n) simp_all
+
+lemma mod_BIT:
+ "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
+proof -
+ have "bin mod 2 ^ n < 2 ^ n" by simp
+ then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
+ then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
+ by (rule mult_left_mono) simp
+ then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
+ then show ?thesis
+ by (auto simp add: Bit_def bitval_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
+ mod_pos_pos_trivial split add: bit.split)
+qed
+
+lemma AND_mod:
+ fixes x :: int
+ shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
+proof (induct x arbitrary: n rule: bin_induct)
+ case 1
+ then show ?case
+ by simp (simp add: Pls_def)
+next
+ case 2
+ then show ?case
+ by (simp, simp only: Min_def, simp add: m1mod2k)
+next
+ case (3 bin bit)
+ show ?case
+ proof (cases n)
+ case 0
+ then show ?thesis by (simp add: int_and_extra_simps [unfolded Pls_def])
+ next
+ case (Suc m)
+ with 3 show ?thesis
+ by (simp only: power_BIT mod_BIT int_and_Bits) simp
+ qed
+qed
+
+end