# HG changeset patch # User haftmann # Date 1555444209 0 # Node ID c247bf924d25b476abee045f7ebec1fd6755acbf # Parent 3173d787827455bc6c1eed8b541743e7baec5e82 integrated Bit_Comparison into Word corpus diff -r 3173d7878274 -r c247bf924d25 src/HOL/ROOT --- a/src/HOL/ROOT Tue Apr 16 19:50:07 2019 +0000 +++ b/src/HOL/ROOT Tue Apr 16 19:50:09 2019 +0000 @@ -830,7 +830,6 @@ theories Word WordBitwise - Bit_Comparison WordExamples document_files "root.bib" "root.tex" diff -r 3173d7878274 -r c247bf924d25 src/HOL/SPARK/SPARK_Setup.thy --- a/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 16 19:50:07 2019 +0000 +++ b/src/HOL/SPARK/SPARK_Setup.thy Tue Apr 16 19:50:09 2019 +0000 @@ -6,7 +6,8 @@ *) theory SPARK_Setup -imports "HOL-Word.Word" "HOL-Word.Bit_Comparison" + imports + "HOL-Word.Word" keywords "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and "spark_open" :: thy_load ("siv", "fdl", "rls") and diff -r 3173d7878274 -r c247bf924d25 src/HOL/Word/Bit_Comparison.thy --- a/src/HOL/Word/Bit_Comparison.thy Tue Apr 16 19:50:07 2019 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,202 +0,0 @@ -(* Title: HOL/Word/Bit_Comparison.thy - Author: Stefan Berghofer - Copyright: secunet Security Networks AG - -Comparison on bit operations on integers. -*) - -theory Bit_Comparison - imports Bits_Int -begin - -lemma AND_lower [simp]: - fixes x y :: int - assumes "0 \ x" - shows "0 \ 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 \ bin" - by (cases bit) (simp_all add: Bit_def) - then have "0 \ bin AND bin'" by (rule 3) - with 1 show ?thesis - by simp (simp add: Bit_def) - qed -qed - -lemma OR_lower [simp]: - fixes x 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 (cases bit) (simp_all add: Bit_def) - moreover from 1 3 have "0 \ bin'" - by (cases bit') (simp_all add: Bit_def) - ultimately have "0 \ bin OR bin'" by (rule 3) - with 1 show ?thesis - by simp (simp add: Bit_def) - qed -qed simp_all - -lemma XOR_lower [simp]: - fixes x 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 (cases bit) (simp_all add: Bit_def) - moreover from 1 3 have "0 \ bin'" - by (cases bit') (simp_all add: Bit_def) - ultimately have "0 \ 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]: - fixes x 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 (cases bit) (simp_all add: Bit_def) - then have "bin AND bin' \ 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] -lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] - -lemma AND_upper2 [simp]: - fixes x y :: int - assumes "0 \ y" - shows "x AND y \ 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 \ bin" - by (cases bit) (simp_all add: Bit_def) - then have "bin' AND bin \ 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] -lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] - -lemma OR_upper: - fixes x 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" and "\ bit" - by (auto simp add: Bit_def split: if_splits) arith - then show ?thesis using 0 1 \y < 2 ^ n\ - by simp - next - case (Suc m) - from 3 have "0 \ 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: - fixes x 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 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 "\ bit" - by (auto simp add: Bit_def split: if_splits) arith - then show ?thesis using 0 1 \y < 2 ^ n\ - by simp - next - case (Suc m) - from 3 have "0 \ 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 - -end diff -r 3173d7878274 -r c247bf924d25 src/HOL/Word/Bits_Int.thy --- 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 \Comparison\ + +lemma AND_lower [simp]: \<^marker>\contributor \Stefan Berghofer\\ + fixes x y :: int + assumes "0 \ x" + shows "0 \ 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 \ bin" + by (cases bit) (simp_all add: Bit_def) + then have "0 \ bin AND bin'" by (rule 3) + with 1 show ?thesis + by simp (simp add: Bit_def) + qed +qed + +lemma OR_lower [simp]: \<^marker>\contributor \Stefan Berghofer\\ + fixes x 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 (cases bit) (simp_all add: Bit_def) + moreover from 1 3 have "0 \ bin'" + by (cases bit') (simp_all add: Bit_def) + ultimately have "0 \ 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>\contributor \Stefan Berghofer\\ + fixes x 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 (cases bit) (simp_all add: Bit_def) + moreover from 1 3 have "0 \ bin'" + by (cases bit') (simp_all add: Bit_def) + ultimately have "0 \ 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>\contributor \Stefan Berghofer\\ + fixes x 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 (cases bit) (simp_all add: Bit_def) + then have "bin AND bin' \ 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>\contributor \Stefan Berghofer\\ +lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] \<^marker>\contributor \Stefan Berghofer\\ + +lemma AND_upper2 [simp]: \<^marker>\contributor \Stefan Berghofer\\ + fixes x y :: int + assumes "0 \ y" + shows "x AND y \ 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 \ bin" + by (cases bit) (simp_all add: Bit_def) + then have "bin' AND bin \ 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>\contributor \Stefan Berghofer\\ +lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] \<^marker>\contributor \Stefan Berghofer\\ + +lemma OR_upper: \<^marker>\contributor \Stefan Berghofer\\ + fixes x 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" and "\ bit" + by (auto simp add: Bit_def split: if_splits) arith + then show ?thesis using 0 1 \y < 2 ^ n\ + by simp + next + case (Suc m) + from 3 have "0 \ 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>\contributor \Stefan Berghofer\\ + fixes x 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 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 "\ bit" + by (auto simp add: Bit_def split: if_splits) arith + then show ?thesis using 0 1 \y < 2 ^ n\ + by simp + next + case (Suc m) + from 3 have "0 \ 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 \Truncating results of bit-wise operations\ lemma bin_trunc_ao: