src/HOL/SPARK/SPARK.thy
 changeset 54427 783861a66a60 parent 50788 fec14e8fefb8 child 63167 0909deb8059b
```     1.1 --- a/src/HOL/SPARK/SPARK.thy	Wed Nov 13 15:36:32 2013 +0100
1.2 +++ b/src/HOL/SPARK/SPARK.thy	Wed Nov 13 19:12:15 2013 +0100
1.3 @@ -16,151 +16,6 @@
1.4    bit__or (integer, integer) : integer = "op OR"
1.5    bit__xor (integer, integer) : integer = "op XOR"
1.6
1.7 -lemma AND_lower [simp]:
1.8 -  fixes x :: int and y :: int
1.9 -  assumes "0 \<le> x"
1.10 -  shows "0 \<le> x AND y"
1.11 -  using assms
1.12 -proof (induct x arbitrary: y rule: bin_induct)
1.13 -  case (3 bin bit)
1.14 -  show ?case
1.15 -  proof (cases y rule: bin_exhaust)
1.16 -    case (1 bin' bit')
1.17 -    from 3 have "0 \<le> bin"
1.19 -    then have "0 \<le> bin AND bin'" by (rule 3)
1.20 -    with 1 show ?thesis
1.22 -  qed
1.23 -next
1.24 -  case 2
1.25 -  then show ?case by (simp only: Min_def)
1.26 -qed simp
1.27 -
1.28 -lemma OR_lower [simp]:
1.29 -  fixes x :: int and y :: int
1.30 -  assumes "0 \<le> x" "0 \<le> y"
1.31 -  shows "0 \<le> x OR y"
1.32 -  using assms
1.33 -proof (induct x arbitrary: y rule: bin_induct)
1.34 -  case (3 bin bit)
1.35 -  show ?case
1.36 -  proof (cases y rule: bin_exhaust)
1.37 -    case (1 bin' bit')
1.38 -    from 3 have "0 \<le> bin"
1.40 -    moreover from 1 3 have "0 \<le> bin'"
1.42 -    ultimately have "0 \<le> bin OR bin'" by (rule 3)
1.43 -    with 1 show ?thesis
1.45 -  qed
1.46 -qed simp_all
1.47 -
1.48 -lemma XOR_lower [simp]:
1.49 -  fixes x :: int and y :: int
1.50 -  assumes "0 \<le> x" "0 \<le> y"
1.51 -  shows "0 \<le> x XOR y"
1.52 -  using assms
1.53 -proof (induct x arbitrary: y rule: bin_induct)
1.54 -  case (3 bin bit)
1.55 -  show ?case
1.56 -  proof (cases y rule: bin_exhaust)
1.57 -    case (1 bin' bit')
1.58 -    from 3 have "0 \<le> bin"
1.60 -    moreover from 1 3 have "0 \<le> bin'"
1.62 -    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
1.63 -    with 1 show ?thesis
1.65 -  qed
1.66 -next
1.67 -  case 2
1.68 -  then show ?case by (simp only: Min_def)
1.69 -qed simp
1.70 -
1.71 -lemma AND_upper1 [simp]:
1.72 -  fixes x :: int and y :: int
1.73 -  assumes "0 \<le> x"
1.74 -  shows "x AND y \<le> x"
1.75 -  using assms
1.76 -proof (induct x arbitrary: y rule: bin_induct)
1.77 -  case (3 bin bit)
1.78 -  show ?case
1.79 -  proof (cases y rule: bin_exhaust)
1.80 -    case (1 bin' bit')
1.81 -    from 3 have "0 \<le> bin"
1.83 -    then have "bin AND bin' \<le> bin" by (rule 3)
1.84 -    with 1 show ?thesis
1.86 -  qed
1.87 -next
1.88 -  case 2
1.89 -  then show ?case by (simp only: Min_def)
1.90 -qed simp
1.91 -
1.92 -lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
1.93 -lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
1.94 -
1.95 -lemma AND_upper2 [simp]:
1.96 -  fixes x :: int and y :: int
1.97 -  assumes "0 \<le> y"
1.98 -  shows "x AND y \<le> y"
1.99 -  using assms
1.100 -proof (induct y arbitrary: x rule: bin_induct)
1.101 -  case (3 bin bit)
1.102 -  show ?case
1.103 -  proof (cases x rule: bin_exhaust)
1.104 -    case (1 bin' bit')
1.105 -    from 3 have "0 \<le> bin"
1.107 -    then have "bin' AND bin \<le> bin" by (rule 3)
1.108 -    with 1 show ?thesis
1.110 -  qed
1.111 -next
1.112 -  case 2
1.113 -  then show ?case by (simp only: Min_def)
1.114 -qed simp
1.115 -
1.116 -lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
1.117 -lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
1.118 -
1.119 -lemma OR_upper:
1.120 -  fixes x :: int and y :: int
1.121 -  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
1.122 -  shows "x OR y < 2 ^ n"
1.123 -  using assms
1.124 -proof (induct x arbitrary: y n rule: bin_induct)
1.125 -  case (3 bin bit)
1.126 -  show ?case
1.127 -  proof (cases y rule: bin_exhaust)
1.128 -    case (1 bin' bit')
1.129 -    show ?thesis
1.130 -    proof (cases n)
1.131 -      case 0
1.132 -      with 3 have "bin BIT bit = 0" by simp
1.133 -      then have "bin = 0" "bit = 0"
1.134 -        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
1.135 -      then show ?thesis using 0 1 `y < 2 ^ n`
1.136 -        by simp
1.137 -    next
1.138 -      case (Suc m)
1.139 -      from 3 have "0 \<le> bin"
1.141 -      moreover from 3 Suc have "bin < 2 ^ m"
1.143 -      moreover from 1 3 Suc have "bin' < 2 ^ m"
1.145 -      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
1.146 -      with 1 Suc show ?thesis
1.148 -    qed
1.149 -  qed
1.150 -qed simp_all
1.151 -
1.152  lemmas [simp] =
1.153    OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
1.154    OR_upper [of _ 8, simplified]
1.155 @@ -171,42 +26,6 @@
1.156    OR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
1.157    OR_upper [of _ 64, simplified]
1.158
1.159 -lemma XOR_upper:
1.160 -  fixes x :: int and y :: int
1.161 -  assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
1.162 -  shows "x XOR y < 2 ^ n"
1.163 -  using assms
1.164 -proof (induct x arbitrary: y n rule: bin_induct)
1.165 -  case (3 bin bit)
1.166 -  show ?case
1.167 -  proof (cases y rule: bin_exhaust)
1.168 -    case (1 bin' bit')
1.169 -    show ?thesis
1.170 -    proof (cases n)
1.171 -      case 0
1.172 -      with 3 have "bin BIT bit = 0" by simp
1.173 -      then have "bin = 0" "bit = 0"
1.174 -        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
1.175 -      then show ?thesis using 0 1 `y < 2 ^ n`
1.176 -        by simp
1.177 -    next
1.178 -      case (Suc m)
1.179 -      from 3 have "0 \<le> bin"
1.181 -      moreover from 3 Suc have "bin < 2 ^ m"
1.183 -      moreover from 1 3 Suc have "bin' < 2 ^ m"
1.185 -      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
1.186 -      with 1 Suc show ?thesis
1.188 -    qed
1.189 -  qed
1.190 -next
1.191 -  case 2
1.192 -  then show ?case by (simp only: Min_def)
1.193 -qed simp
1.194 -
1.195  lemmas [simp] =
1.196    XOR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
1.197    XOR_upper [of _ 8, simplified]
1.198 @@ -234,47 +53,6 @@
1.199    bit_not_spark_eq [where 'a=32, simplified]
1.200    bit_not_spark_eq [where 'a=64, simplified]
1.201
1.202 -lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
1.203 -  unfolding Bit_B1
1.204 -  by (induct n) simp_all
1.205 -
1.206 -lemma mod_BIT:
1.207 -  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
1.208 -proof -
1.209 -  have "bin mod 2 ^ n < 2 ^ n" by simp
1.210 -  then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
1.211 -  then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
1.212 -    by (rule mult_left_mono) simp
1.213 -  then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
1.214 -  then show ?thesis
1.215 -    by (auto simp add: Bit_def bitval_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
1.216 -      mod_pos_pos_trivial split add: bit.split)
1.217 -qed
1.218 -
1.219 -lemma AND_mod:
1.220 -  fixes x :: int
1.221 -  shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
1.222 -proof (induct x arbitrary: n rule: bin_induct)
1.223 -  case 1
1.224 -  then show ?case
1.225 -    by simp
1.226 -next
1.227 -  case 2
1.228 -  then show ?case
1.229 -    by (simp, simp add: m1mod2k)
1.230 -next
1.231 -  case (3 bin bit)
1.232 -  show ?case
1.233 -  proof (cases n)
1.234 -    case 0
1.235 -    then show ?thesis by (simp add: int_and_extra_simps)
1.236 -  next
1.237 -    case (Suc m)
1.238 -    with 3 show ?thesis
1.239 -      by (simp only: power_BIT mod_BIT int_and_Bits) simp
1.240 -  qed
1.241 -qed
1.242 -
1.243
1.244  text {* Minimum and maximum *}
1.245
1.246 @@ -283,3 +61,4 @@
1.247    integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
1.248
1.249  end
1.250 +
```