--- a/src/HOL/Word/Bits_Int.thy Tue Apr 16 19:50:07 2019 +0000
+++ b/src/HOL/Word/Bits_Int.thy Tue Apr 16 19:50:09 2019 +0000
@@ -401,6 +401,200 @@
qed
+subsubsection \<open>Comparison\<close>
+
+lemma AND_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> x"
+ shows "0 \<le> x AND y"
+ using assms
+proof (induct x arbitrary: y rule: bin_induct)
+ case 1
+ then show ?case by simp
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+next
+ case (3 bin bit)
+ show ?case
+ proof (cases y rule: bin_exhaust)
+ case (1 bin' bit')
+ from 3 have "0 \<le> bin"
+ by (cases bit) (simp_all add: Bit_def)
+ then have "0 \<le> bin AND bin'" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def)
+ qed
+qed
+
+lemma OR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x 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 (cases bit) (simp_all add: Bit_def)
+ moreover from 1 3 have "0 \<le> bin'"
+ by (cases bit') (simp_all add: Bit_def)
+ ultimately have "0 \<le> bin OR bin'" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def)
+ qed
+qed simp_all
+
+lemma XOR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x 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 (cases bit) (simp_all add: Bit_def)
+ moreover from 1 3 have "0 \<le> bin'"
+ by (cases bit') (simp_all add: Bit_def)
+ ultimately have "0 \<le> bin XOR bin'" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def)
+ qed
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+qed simp
+
+lemma AND_upper1 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x 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 (cases bit) (simp_all add: Bit_def)
+ then have "bin AND bin' \<le> bin" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def)
+ qed
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+qed simp
+
+lemmas AND_upper1' [simp] = order_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+
+lemma AND_upper2 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x y :: int
+ assumes "0 \<le> y"
+ shows "x AND y \<le> y"
+ using assms
+proof (induct y arbitrary: x rule: bin_induct)
+ case 1
+ then show ?case by simp
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+next
+ case (3 bin bit)
+ show ?case
+ proof (cases x rule: bin_exhaust)
+ case (1 bin' bit')
+ from 3 have "0 \<le> bin"
+ by (cases bit) (simp_all add: Bit_def)
+ then have "bin' AND bin \<le> bin" by (rule 3)
+ with 1 show ?thesis
+ by simp (simp add: Bit_def)
+ qed
+qed
+
+lemmas AND_upper2' [simp] = order_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+
+lemma OR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x 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" and "\<not> bit"
+ by (auto simp add: Bit_def split: if_splits) arith
+ then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
+ by simp
+ next
+ case (Suc m)
+ from 3 have "0 \<le> bin"
+ by (cases bit) (simp_all add: Bit_def)
+ moreover from 3 Suc have "bin < 2 ^ m"
+ by (cases bit) (simp_all add: Bit_def)
+ moreover from 1 3 Suc have "bin' < 2 ^ m"
+ by (cases bit') (simp_all add: Bit_def)
+ ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
+ with 1 Suc show ?thesis
+ by simp (simp add: Bit_def)
+ qed
+ qed
+qed simp_all
+
+lemma XOR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+ fixes x 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 1
+ then show ?case by simp
+next
+ case 2
+ then show ?case by (simp only: Min_def)
+next
+ 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" and "\<not> bit"
+ by (auto simp add: Bit_def split: if_splits) arith
+ then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
+ by simp
+ next
+ case (Suc m)
+ from 3 have "0 \<le> bin"
+ by (cases bit) (simp_all add: Bit_def)
+ moreover from 3 Suc have "bin < 2 ^ m"
+ by (cases bit) (simp_all add: Bit_def)
+ moreover from 1 3 Suc have "bin' < 2 ^ m"
+ by (cases bit') (simp_all add: Bit_def)
+ ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
+ with 1 Suc show ?thesis
+ by simp (simp add: Bit_def)
+ qed
+ qed
+qed
+
+
+
subsubsection \<open>Truncating results of bit-wise operations\<close>
lemma bin_trunc_ao: