# HG changeset patch # User haftmann # Date 1384366335 -3600 # Node ID 783861a66a60194aca6d2c1c888dd8745f47aeba # Parent edb87aac9cca741fb9b16d43e757b36db2966470 separated comparision on bit operations into separate theory diff -r edb87aac9cca -r 783861a66a60 src/HOL/SPARK/SPARK.thy --- 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 \ x" - shows "0 \ 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 \ bin" - by (simp add: Bit_def bitval_def split add: bit.split_asm) - then have "0 \ 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 \ x" "0 \ y" - shows "0 \ 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 \ bin" - by (simp add: Bit_def bitval_def split add: bit.split_asm) - moreover from 1 3 have "0 \ bin'" - by (simp add: Bit_def bitval_def split add: bit.split_asm) - ultimately have "0 \ 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 \ x" "0 \ y" - shows "0 \ 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 \ bin" - by (simp add: Bit_def bitval_def split add: bit.split_asm) - moreover from 1 3 have "0 \ bin'" - by (simp add: Bit_def bitval_def split add: bit.split_asm) - ultimately have "0 \ 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 \ x" - shows "x AND y \ 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 \ bin" - by (simp add: Bit_def bitval_def split add: bit.split_asm) - then have "bin AND bin' \ 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 \ y" - shows "x AND y \ 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 \ bin" - by (simp add: Bit_def bitval_def split add: bit.split_asm) - then have "bin' AND bin \ 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 \ 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 \ 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 \ 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 \ 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 \ 2 ^ n - 1" by simp - then have "2 * (bin mod 2 ^ n) \ 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 \ int \ int" end + diff -r edb87aac9cca -r 783861a66a60 src/HOL/SPARK/SPARK_Setup.thy --- 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 diff -r edb87aac9cca -r 783861a66a60 src/HOL/Word/Bit_Comparison.thy --- /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 \ x" + shows "0 \ 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 \ bin" + by (simp add: Bit_def bitval_def split add: bit.split_asm) + then have "0 \ 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 \ x" "0 \ y" + shows "0 \ 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 \ bin" + by (simp add: Bit_def bitval_def split add: bit.split_asm) + moreover from 1 3 have "0 \ bin'" + by (simp add: Bit_def bitval_def split add: bit.split_asm) + ultimately have "0 \ 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 \ x" "0 \ y" + shows "0 \ 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 \ bin" + by (simp add: Bit_def bitval_def split add: bit.split_asm) + moreover from 1 3 have "0 \ bin'" + by (simp add: Bit_def bitval_def split add: bit.split_asm) + ultimately have "0 \ 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 \ x" + shows "x AND y \ 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 \ bin" + by (simp add: Bit_def bitval_def split add: bit.split_asm) + then have "bin AND bin' \ 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 \ y" + shows "x AND y \ 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 \ bin" + by (simp add: Bit_def bitval_def split add: bit.split_asm) + then have "bin' AND bin \ 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 \ 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 \ 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 \ 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 \ 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 diff -r edb87aac9cca -r 783861a66a60 src/HOL/Word/Bit_Int.thy --- 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 \ 2 ^ n - 1" by simp + then have "2 * (bin mod 2 ^ n) \ 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