--- a/src/HOL/SPARK/SPARK.thy Wed Nov 13 15:36:32 2013 +0100
+++ b/src/HOL/SPARK/SPARK.thy Wed Nov 13 19:12:15 2013 +0100
@@ -16,151 +16,6 @@
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
- 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]
@@ -171,42 +26,6 @@
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
- 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]
@@ -234,47 +53,6 @@
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
-next
- case 2
- then show ?case
- by (simp, 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)
- next
- case (Suc m)
- with 3 show ?thesis
- by (simp only: power_BIT mod_BIT int_and_Bits) simp
- qed
-qed
-
text {* Minimum and maximum *}
@@ -283,3 +61,4 @@
integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
end
+
--- a/src/HOL/SPARK/SPARK_Setup.thy Wed Nov 13 15:36:32 2013 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy Wed Nov 13 19:12:15 2013 +0100
@@ -6,7 +6,7 @@
*)
theory SPARK_Setup
-imports Word
+imports "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
keywords
"spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
"spark_open_siv" :: thy_load ("siv", "fdl", "rls") and
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bit_Comparison.thy Wed Nov 13 19:12:15 2013 +0100
@@ -0,0 +1,193 @@
+(* Title: HOL/SPARK/SPARK.thy
+ Author: Stefan Berghofer
+ Copyright: secunet Security Networks AG
+
+Comparison on bit operations on integers.
+*)
+
+theory Bit_Comparison
+imports Type_Length Bit_Operations Bit_Int
+begin
+
+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
+ 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
+
+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
+ 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
+
+end
--- a/src/HOL/Word/Bit_Int.thy Wed Nov 13 15:36:32 2013 +0100
+++ b/src/HOL/Word/Bit_Int.thy Wed Nov 13 19:12:15 2013 +0100
@@ -632,5 +632,46 @@
"(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
by auto
+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
+next
+ case 2
+ then show ?case
+ by (simp, 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)
+ next
+ case (Suc m)
+ with 3 show ?thesis
+ by (simp only: power_BIT mod_BIT int_and_Bits) simp
+ qed
+qed
+
end