integrated Bit_Comparison into Word corpus
authorhaftmann
Tue Apr 16 19:50:09 2019 +0000 (7 days ago)
changeset 70172c247bf924d25
parent 70171 3173d7878274
child 70173 c2786fe88064
integrated Bit_Comparison into Word corpus
src/HOL/ROOT
src/HOL/SPARK/SPARK_Setup.thy
src/HOL/Word/Bit_Comparison.thy
src/HOL/Word/Bits_Int.thy
     1.1 --- a/src/HOL/ROOT	Tue Apr 16 19:50:07 2019 +0000
     1.2 +++ b/src/HOL/ROOT	Tue Apr 16 19:50:09 2019 +0000
     1.3 @@ -830,7 +830,6 @@
     1.4    theories
     1.5      Word
     1.6      WordBitwise
     1.7 -    Bit_Comparison
     1.8      WordExamples
     1.9    document_files "root.bib" "root.tex"
    1.10  
     2.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Tue Apr 16 19:50:07 2019 +0000
     2.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Tue Apr 16 19:50:09 2019 +0000
     2.3 @@ -6,7 +6,8 @@
     2.4  *)
     2.5  
     2.6  theory SPARK_Setup
     2.7 -imports "HOL-Word.Word" "HOL-Word.Bit_Comparison"
     2.8 +  imports
     2.9 +  "HOL-Word.Word"
    2.10  keywords
    2.11    "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
    2.12    "spark_open" :: thy_load ("siv", "fdl", "rls") and
     3.1 --- a/src/HOL/Word/Bit_Comparison.thy	Tue Apr 16 19:50:07 2019 +0000
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,202 +0,0 @@
     3.4 -(*  Title:      HOL/Word/Bit_Comparison.thy
     3.5 -    Author:     Stefan Berghofer
     3.6 -    Copyright:  secunet Security Networks AG
     3.7 -
     3.8 -Comparison on bit operations on integers.
     3.9 -*)
    3.10 -
    3.11 -theory Bit_Comparison
    3.12 -  imports Bits_Int
    3.13 -begin
    3.14 -
    3.15 -lemma AND_lower [simp]:
    3.16 -  fixes x y :: int
    3.17 -  assumes "0 \<le> x"
    3.18 -  shows "0 \<le> x AND y"
    3.19 -  using assms
    3.20 -proof (induct x arbitrary: y rule: bin_induct)
    3.21 -  case 1
    3.22 -  then show ?case by simp
    3.23 -next
    3.24 -  case 2
    3.25 -  then show ?case by (simp only: Min_def)
    3.26 -next
    3.27 -  case (3 bin bit)
    3.28 -  show ?case
    3.29 -  proof (cases y rule: bin_exhaust)
    3.30 -    case (1 bin' bit')
    3.31 -    from 3 have "0 \<le> bin"
    3.32 -      by (cases bit) (simp_all add: Bit_def)
    3.33 -    then have "0 \<le> bin AND bin'" by (rule 3)
    3.34 -    with 1 show ?thesis
    3.35 -      by simp (simp add: Bit_def)
    3.36 -  qed
    3.37 -qed
    3.38 -
    3.39 -lemma OR_lower [simp]:
    3.40 -  fixes x y :: int
    3.41 -  assumes "0 \<le> x" "0 \<le> y"
    3.42 -  shows "0 \<le> x OR y"
    3.43 -  using assms
    3.44 -proof (induct x arbitrary: y rule: bin_induct)
    3.45 -  case (3 bin bit)
    3.46 -  show ?case
    3.47 -  proof (cases y rule: bin_exhaust)
    3.48 -    case (1 bin' bit')
    3.49 -    from 3 have "0 \<le> bin"
    3.50 -      by (cases bit) (simp_all add: Bit_def)
    3.51 -    moreover from 1 3 have "0 \<le> bin'"
    3.52 -      by (cases bit') (simp_all add: Bit_def)
    3.53 -    ultimately have "0 \<le> bin OR bin'" by (rule 3)
    3.54 -    with 1 show ?thesis
    3.55 -      by simp (simp add: Bit_def)
    3.56 -  qed
    3.57 -qed simp_all
    3.58 -
    3.59 -lemma XOR_lower [simp]:
    3.60 -  fixes x y :: int
    3.61 -  assumes "0 \<le> x" "0 \<le> y"
    3.62 -  shows "0 \<le> x XOR y"
    3.63 -  using assms
    3.64 -proof (induct x arbitrary: y rule: bin_induct)
    3.65 -  case (3 bin bit)
    3.66 -  show ?case
    3.67 -  proof (cases y rule: bin_exhaust)
    3.68 -    case (1 bin' bit')
    3.69 -    from 3 have "0 \<le> bin"
    3.70 -      by (cases bit) (simp_all add: Bit_def)
    3.71 -    moreover from 1 3 have "0 \<le> bin'"
    3.72 -      by (cases bit') (simp_all add: Bit_def)
    3.73 -    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
    3.74 -    with 1 show ?thesis
    3.75 -      by simp (simp add: Bit_def)
    3.76 -  qed
    3.77 -next
    3.78 -  case 2
    3.79 -  then show ?case by (simp only: Min_def)
    3.80 -qed simp
    3.81 -
    3.82 -lemma AND_upper1 [simp]:
    3.83 -  fixes x y :: int
    3.84 -  assumes "0 \<le> x"
    3.85 -  shows "x AND y \<le> x"
    3.86 -  using assms
    3.87 -proof (induct x arbitrary: y rule: bin_induct)
    3.88 -  case (3 bin bit)
    3.89 -  show ?case
    3.90 -  proof (cases y rule: bin_exhaust)
    3.91 -    case (1 bin' bit')
    3.92 -    from 3 have "0 \<le> bin"
    3.93 -      by (cases bit) (simp_all add: Bit_def)
    3.94 -    then have "bin AND bin' \<le> bin" by (rule 3)
    3.95 -    with 1 show ?thesis
    3.96 -      by simp (simp add: Bit_def)
    3.97 -  qed
    3.98 -next
    3.99 -  case 2
   3.100 -  then show ?case by (simp only: Min_def)
   3.101 -qed simp
   3.102 -
   3.103 -lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
   3.104 -lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
   3.105 -
   3.106 -lemma AND_upper2 [simp]:
   3.107 -  fixes x y :: int
   3.108 -  assumes "0 \<le> y"
   3.109 -  shows "x AND y \<le> y"
   3.110 -  using assms
   3.111 -proof (induct y arbitrary: x rule: bin_induct)
   3.112 -  case 1
   3.113 -  then show ?case by simp
   3.114 -next
   3.115 -  case 2
   3.116 -  then show ?case by (simp only: Min_def)
   3.117 -next
   3.118 -  case (3 bin bit)
   3.119 -  show ?case
   3.120 -  proof (cases x rule: bin_exhaust)
   3.121 -    case (1 bin' bit')
   3.122 -    from 3 have "0 \<le> bin"
   3.123 -      by (cases bit) (simp_all add: Bit_def)
   3.124 -    then have "bin' AND bin \<le> bin" by (rule 3)
   3.125 -    with 1 show ?thesis
   3.126 -      by simp (simp add: Bit_def)
   3.127 -  qed
   3.128 -qed
   3.129 -
   3.130 -lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
   3.131 -lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
   3.132 -
   3.133 -lemma OR_upper:
   3.134 -  fixes x y :: int
   3.135 -  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   3.136 -  shows "x OR y < 2 ^ n"
   3.137 -  using assms
   3.138 -proof (induct x arbitrary: y n rule: bin_induct)
   3.139 -  case (3 bin bit)
   3.140 -  show ?case
   3.141 -  proof (cases y rule: bin_exhaust)
   3.142 -    case (1 bin' bit')
   3.143 -    show ?thesis
   3.144 -    proof (cases n)
   3.145 -      case 0
   3.146 -      with 3 have "bin BIT bit = 0" by simp
   3.147 -      then have "bin = 0" and "\<not> bit"
   3.148 -        by (auto simp add: Bit_def split: if_splits) arith
   3.149 -      then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
   3.150 -        by simp
   3.151 -    next
   3.152 -      case (Suc m)
   3.153 -      from 3 have "0 \<le> bin"
   3.154 -        by (cases bit) (simp_all add: Bit_def)
   3.155 -      moreover from 3 Suc have "bin < 2 ^ m"
   3.156 -        by (cases bit) (simp_all add: Bit_def)
   3.157 -      moreover from 1 3 Suc have "bin' < 2 ^ m"
   3.158 -        by (cases bit') (simp_all add: Bit_def)
   3.159 -      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
   3.160 -      with 1 Suc show ?thesis
   3.161 -        by simp (simp add: Bit_def)
   3.162 -    qed
   3.163 -  qed
   3.164 -qed simp_all
   3.165 -
   3.166 -lemma XOR_upper:
   3.167 -  fixes x y :: int
   3.168 -  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   3.169 -  shows "x XOR y < 2 ^ n"
   3.170 -  using assms
   3.171 -proof (induct x arbitrary: y n rule: bin_induct)
   3.172 -  case 1
   3.173 -  then show ?case by simp
   3.174 -next
   3.175 -  case 2
   3.176 -  then show ?case by (simp only: Min_def)
   3.177 -next
   3.178 -  case (3 bin bit)
   3.179 -  show ?case
   3.180 -  proof (cases y rule: bin_exhaust)
   3.181 -    case (1 bin' bit')
   3.182 -    show ?thesis
   3.183 -    proof (cases n)
   3.184 -      case 0
   3.185 -      with 3 have "bin BIT bit = 0" by simp
   3.186 -      then have "bin = 0" and "\<not> bit"
   3.187 -        by (auto simp add: Bit_def split: if_splits) arith
   3.188 -      then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
   3.189 -        by simp
   3.190 -    next
   3.191 -      case (Suc m)
   3.192 -      from 3 have "0 \<le> bin"
   3.193 -        by (cases bit) (simp_all add: Bit_def)
   3.194 -      moreover from 3 Suc have "bin < 2 ^ m"
   3.195 -        by (cases bit) (simp_all add: Bit_def)
   3.196 -      moreover from 1 3 Suc have "bin' < 2 ^ m"
   3.197 -        by (cases bit') (simp_all add: Bit_def)
   3.198 -      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
   3.199 -      with 1 Suc show ?thesis
   3.200 -        by simp (simp add: Bit_def)
   3.201 -    qed
   3.202 -  qed
   3.203 -qed
   3.204 -
   3.205 -end
     4.1 --- a/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:07 2019 +0000
     4.2 +++ b/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:09 2019 +0000
     4.3 @@ -401,6 +401,200 @@
     4.4  qed
     4.5  
     4.6  
     4.7 +subsubsection \<open>Comparison\<close>
     4.8 +
     4.9 +lemma AND_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
    4.10 +  fixes x y :: int
    4.11 +  assumes "0 \<le> x"
    4.12 +  shows "0 \<le> x AND y"
    4.13 +  using assms
    4.14 +proof (induct x arbitrary: y rule: bin_induct)
    4.15 +  case 1
    4.16 +  then show ?case by simp
    4.17 +next
    4.18 +  case 2
    4.19 +  then show ?case by (simp only: Min_def)
    4.20 +next
    4.21 +  case (3 bin bit)
    4.22 +  show ?case
    4.23 +  proof (cases y rule: bin_exhaust)
    4.24 +    case (1 bin' bit')
    4.25 +    from 3 have "0 \<le> bin"
    4.26 +      by (cases bit) (simp_all add: Bit_def)
    4.27 +    then have "0 \<le> bin AND bin'" by (rule 3)
    4.28 +    with 1 show ?thesis
    4.29 +      by simp (simp add: Bit_def)
    4.30 +  qed
    4.31 +qed
    4.32 +
    4.33 +lemma OR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
    4.34 +  fixes x y :: int
    4.35 +  assumes "0 \<le> x" "0 \<le> y"
    4.36 +  shows "0 \<le> x OR y"
    4.37 +  using assms
    4.38 +proof (induct x arbitrary: y rule: bin_induct)
    4.39 +  case (3 bin bit)
    4.40 +  show ?case
    4.41 +  proof (cases y rule: bin_exhaust)
    4.42 +    case (1 bin' bit')
    4.43 +    from 3 have "0 \<le> bin"
    4.44 +      by (cases bit) (simp_all add: Bit_def)
    4.45 +    moreover from 1 3 have "0 \<le> bin'"
    4.46 +      by (cases bit') (simp_all add: Bit_def)
    4.47 +    ultimately have "0 \<le> bin OR bin'" by (rule 3)
    4.48 +    with 1 show ?thesis
    4.49 +      by simp (simp add: Bit_def)
    4.50 +  qed
    4.51 +qed simp_all
    4.52 +
    4.53 +lemma XOR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
    4.54 +  fixes x y :: int
    4.55 +  assumes "0 \<le> x" "0 \<le> y"
    4.56 +  shows "0 \<le> x XOR y"
    4.57 +  using assms
    4.58 +proof (induct x arbitrary: y rule: bin_induct)
    4.59 +  case (3 bin bit)
    4.60 +  show ?case
    4.61 +  proof (cases y rule: bin_exhaust)
    4.62 +    case (1 bin' bit')
    4.63 +    from 3 have "0 \<le> bin"
    4.64 +      by (cases bit) (simp_all add: Bit_def)
    4.65 +    moreover from 1 3 have "0 \<le> bin'"
    4.66 +      by (cases bit') (simp_all add: Bit_def)
    4.67 +    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
    4.68 +    with 1 show ?thesis
    4.69 +      by simp (simp add: Bit_def)
    4.70 +  qed
    4.71 +next
    4.72 +  case 2
    4.73 +  then show ?case by (simp only: Min_def)
    4.74 +qed simp
    4.75 +
    4.76 +lemma AND_upper1 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
    4.77 +  fixes x y :: int
    4.78 +  assumes "0 \<le> x"
    4.79 +  shows "x AND y \<le> x"
    4.80 +  using assms
    4.81 +proof (induct x arbitrary: y rule: bin_induct)
    4.82 +  case (3 bin bit)
    4.83 +  show ?case
    4.84 +  proof (cases y rule: bin_exhaust)
    4.85 +    case (1 bin' bit')
    4.86 +    from 3 have "0 \<le> bin"
    4.87 +      by (cases bit) (simp_all add: Bit_def)
    4.88 +    then have "bin AND bin' \<le> bin" by (rule 3)
    4.89 +    with 1 show ?thesis
    4.90 +      by simp (simp add: Bit_def)
    4.91 +  qed
    4.92 +next
    4.93 +  case 2
    4.94 +  then show ?case by (simp only: Min_def)
    4.95 +qed simp
    4.96 +
    4.97 +lemmas AND_upper1' [simp] = order_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
    4.98 +lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
    4.99 +
   4.100 +lemma AND_upper2 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   4.101 +  fixes x y :: int
   4.102 +  assumes "0 \<le> y"
   4.103 +  shows "x AND y \<le> y"
   4.104 +  using assms
   4.105 +proof (induct y arbitrary: x rule: bin_induct)
   4.106 +  case 1
   4.107 +  then show ?case by simp
   4.108 +next
   4.109 +  case 2
   4.110 +  then show ?case by (simp only: Min_def)
   4.111 +next
   4.112 +  case (3 bin bit)
   4.113 +  show ?case
   4.114 +  proof (cases x rule: bin_exhaust)
   4.115 +    case (1 bin' bit')
   4.116 +    from 3 have "0 \<le> bin"
   4.117 +      by (cases bit) (simp_all add: Bit_def)
   4.118 +    then have "bin' AND bin \<le> bin" by (rule 3)
   4.119 +    with 1 show ?thesis
   4.120 +      by simp (simp add: Bit_def)
   4.121 +  qed
   4.122 +qed
   4.123 +
   4.124 +lemmas AND_upper2' [simp] = order_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   4.125 +lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   4.126 +
   4.127 +lemma OR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   4.128 +  fixes x y :: int
   4.129 +  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   4.130 +  shows "x OR y < 2 ^ n"
   4.131 +  using assms
   4.132 +proof (induct x arbitrary: y n rule: bin_induct)
   4.133 +  case (3 bin bit)
   4.134 +  show ?case
   4.135 +  proof (cases y rule: bin_exhaust)
   4.136 +    case (1 bin' bit')
   4.137 +    show ?thesis
   4.138 +    proof (cases n)
   4.139 +      case 0
   4.140 +      with 3 have "bin BIT bit = 0" by simp
   4.141 +      then have "bin = 0" and "\<not> bit"
   4.142 +        by (auto simp add: Bit_def split: if_splits) arith
   4.143 +      then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
   4.144 +        by simp
   4.145 +    next
   4.146 +      case (Suc m)
   4.147 +      from 3 have "0 \<le> bin"
   4.148 +        by (cases bit) (simp_all add: Bit_def)
   4.149 +      moreover from 3 Suc have "bin < 2 ^ m"
   4.150 +        by (cases bit) (simp_all add: Bit_def)
   4.151 +      moreover from 1 3 Suc have "bin' < 2 ^ m"
   4.152 +        by (cases bit') (simp_all add: Bit_def)
   4.153 +      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
   4.154 +      with 1 Suc show ?thesis
   4.155 +        by simp (simp add: Bit_def)
   4.156 +    qed
   4.157 +  qed
   4.158 +qed simp_all
   4.159 +
   4.160 +lemma XOR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   4.161 +  fixes x y :: int
   4.162 +  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   4.163 +  shows "x XOR y < 2 ^ n"
   4.164 +  using assms
   4.165 +proof (induct x arbitrary: y n rule: bin_induct)
   4.166 +  case 1
   4.167 +  then show ?case by simp
   4.168 +next
   4.169 +  case 2
   4.170 +  then show ?case by (simp only: Min_def)
   4.171 +next
   4.172 +  case (3 bin bit)
   4.173 +  show ?case
   4.174 +  proof (cases y rule: bin_exhaust)
   4.175 +    case (1 bin' bit')
   4.176 +    show ?thesis
   4.177 +    proof (cases n)
   4.178 +      case 0
   4.179 +      with 3 have "bin BIT bit = 0" by simp
   4.180 +      then have "bin = 0" and "\<not> bit"
   4.181 +        by (auto simp add: Bit_def split: if_splits) arith
   4.182 +      then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
   4.183 +        by simp
   4.184 +    next
   4.185 +      case (Suc m)
   4.186 +      from 3 have "0 \<le> bin"
   4.187 +        by (cases bit) (simp_all add: Bit_def)
   4.188 +      moreover from 3 Suc have "bin < 2 ^ m"
   4.189 +        by (cases bit) (simp_all add: Bit_def)
   4.190 +      moreover from 1 3 Suc have "bin' < 2 ^ m"
   4.191 +        by (cases bit') (simp_all add: Bit_def)
   4.192 +      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
   4.193 +      with 1 Suc show ?thesis
   4.194 +        by simp (simp add: Bit_def)
   4.195 +    qed
   4.196 +  qed
   4.197 +qed
   4.198 +
   4.199 +
   4.200 +
   4.201  subsubsection \<open>Truncating results of bit-wise operations\<close>
   4.202  
   4.203  lemma bin_trunc_ao: