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.18 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.19 -    then have "0 \<le> bin AND bin'" by (rule 3)
    1.20 -    with 1 show ?thesis
    1.21 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    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.39 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.40 -    moreover from 1 3 have "0 \<le> bin'"
    1.41 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.42 -    ultimately have "0 \<le> bin OR bin'" by (rule 3)
    1.43 -    with 1 show ?thesis
    1.44 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    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.59 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.60 -    moreover from 1 3 have "0 \<le> bin'"
    1.61 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.62 -    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
    1.63 -    with 1 show ?thesis
    1.64 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    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.82 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.83 -    then have "bin AND bin' \<le> bin" by (rule 3)
    1.84 -    with 1 show ?thesis
    1.85 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    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.106 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.107 -    then have "bin' AND bin \<le> bin" by (rule 3)
   1.108 -    with 1 show ?thesis
   1.109 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
   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.140 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.141 -      moreover from 3 Suc have "bin < 2 ^ m"
   1.142 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.143 -      moreover from 1 3 Suc have "bin' < 2 ^ m"
   1.144 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.145 -      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
   1.146 -      with 1 Suc show ?thesis
   1.147 -        by simp (simp add: Bit_def bitval_def split add: bit.split)
   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.180 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.181 -      moreover from 3 Suc have "bin < 2 ^ m"
   1.182 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.183 -      moreover from 1 3 Suc have "bin' < 2 ^ m"
   1.184 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.185 -      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
   1.186 -      with 1 Suc show ?thesis
   1.187 -        by simp (simp add: Bit_def bitval_def split add: bit.split)
   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 +