--- 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
+