# HG changeset patch
# User haftmann
# Date 1384366335 -3600
# Node ID 783861a66a60194aca6d2c1c888dd8745f47aeba
# Parent  edb87aac9cca741fb9b16d43e757b36db2966470
separated comparision on bit operations into separate theory

diff -r edb87aac9cca -r 783861a66a60 src/HOL/SPARK/SPARK.thy
--- a/src/HOL/SPARK/SPARK.thy	Wed Nov 13 15:36:32 2013 +0100
+++ b/src/HOL/SPARK/SPARK.thy	Wed Nov 13 19:12:15 2013 +0100
@@ -16,151 +16,6 @@
   bit__or (integer, integer) : integer = "op OR"
   bit__xor (integer, integer) : integer = "op XOR"
 
-lemma AND_lower [simp]:
-  fixes x :: int and y :: int
-  assumes "0 \<le> x"
-  shows "0 \<le> x AND 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 (simp add: Bit_def bitval_def split add: bit.split_asm)
-    then have "0 \<le> bin AND bin'" by (rule 3)
-    with 1 show ?thesis
-      by simp (simp add: Bit_def bitval_def split add: bit.split)
-  qed
-next
-  case 2
-  then show ?case by (simp only: Min_def)
-qed simp
-
-lemma OR_lower [simp]:
-  fixes x :: int and 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 (simp add: Bit_def bitval_def split add: bit.split_asm)
-    moreover from 1 3 have "0 \<le> bin'"
-      by (simp add: Bit_def bitval_def split add: bit.split_asm)
-    ultimately have "0 \<le> bin OR bin'" by (rule 3)
-    with 1 show ?thesis
-      by simp (simp add: Bit_def bitval_def split add: bit.split)
-  qed
-qed simp_all
-
-lemma XOR_lower [simp]:
-  fixes x :: int and 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 (simp add: Bit_def bitval_def split add: bit.split_asm)
-    moreover from 1 3 have "0 \<le> bin'"
-      by (simp add: Bit_def bitval_def split add: bit.split_asm)
-    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
-    with 1 show ?thesis
-      by simp (simp add: Bit_def bitval_def split add: bit.split)
-  qed
-next
-  case 2
-  then show ?case by (simp only: Min_def)
-qed simp
-
-lemma AND_upper1 [simp]:
-  fixes x :: int and 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 (simp add: Bit_def bitval_def split add: bit.split_asm)
-    then have "bin AND bin' \<le> bin" by (rule 3)
-    with 1 show ?thesis
-      by simp (simp add: Bit_def bitval_def split add: bit.split)
-  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 :: int and y :: int
-  assumes "0 \<le> y"
-  shows "x AND y \<le> y"
-  using assms
-proof (induct y arbitrary: x rule: bin_induct)
-  case (3 bin bit)
-  show ?case
-  proof (cases x rule: bin_exhaust)
-    case (1 bin' bit')
-    from 3 have "0 \<le> bin"
-      by (simp add: Bit_def bitval_def split add: bit.split_asm)
-    then have "bin' AND bin \<le> bin" by (rule 3)
-    with 1 show ?thesis
-      by simp (simp add: Bit_def bitval_def split add: bit.split)
-  qed
-next
-  case 2
-  then show ?case by (simp only: Min_def)
-qed simp
-
-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 :: int and 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" "bit = 0"
-        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
-      then show ?thesis using 0 1 `y < 2 ^ n`
-        by simp
-    next
-      case (Suc m)
-      from 3 have "0 \<le> bin"
-        by (simp add: Bit_def bitval_def split add: bit.split_asm)
-      moreover from 3 Suc have "bin < 2 ^ m"
-        by (simp add: Bit_def bitval_def split add: bit.split_asm)
-      moreover from 1 3 Suc have "bin' < 2 ^ m"
-        by (simp add: Bit_def bitval_def split add: bit.split_asm)
-      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
-      with 1 Suc show ?thesis
-        by simp (simp add: Bit_def bitval_def split add: bit.split)
-    qed
-  qed
-qed simp_all
-
 lemmas [simp] =
   OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
   OR_upper [of _ 8, simplified]
@@ -171,42 +26,6 @@
   OR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
   OR_upper [of _ 64, simplified]
 
-lemma XOR_upper:
-  fixes x :: int and 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 (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" "bit = 0"
-        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
-      then show ?thesis using 0 1 `y < 2 ^ n`
-        by simp
-    next
-      case (Suc m)
-      from 3 have "0 \<le> bin"
-        by (simp add: Bit_def bitval_def split add: bit.split_asm)
-      moreover from 3 Suc have "bin < 2 ^ m"
-        by (simp add: Bit_def bitval_def split add: bit.split_asm)
-      moreover from 1 3 Suc have "bin' < 2 ^ m"
-        by (simp add: Bit_def bitval_def split add: bit.split_asm)
-      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
-      with 1 Suc show ?thesis
-        by simp (simp add: Bit_def bitval_def split add: bit.split)
-    qed
-  qed
-next
-  case 2
-  then show ?case by (simp only: Min_def)
-qed simp
-
 lemmas [simp] =
   XOR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
   XOR_upper [of _ 8, simplified]
@@ -234,47 +53,6 @@
   bit_not_spark_eq [where 'a=32, simplified]
   bit_not_spark_eq [where 'a=64, simplified]
 
-lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
-  unfolding Bit_B1
-  by (induct n) simp_all
-
-lemma mod_BIT:
-  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
-proof -
-  have "bin mod 2 ^ n < 2 ^ n" by simp
-  then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
-  then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
-    by (rule mult_left_mono) simp
-  then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
-  then show ?thesis
-    by (auto simp add: Bit_def bitval_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
-      mod_pos_pos_trivial split add: bit.split)
-qed
-
-lemma AND_mod:
-  fixes x :: int
-  shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
-proof (induct x arbitrary: n rule: bin_induct)
-  case 1
-  then show ?case
-    by simp
-next
-  case 2
-  then show ?case
-    by (simp, simp add: m1mod2k)
-next
-  case (3 bin bit)
-  show ?case
-  proof (cases n)
-    case 0
-    then show ?thesis by (simp add: int_and_extra_simps)
-  next
-    case (Suc m)
-    with 3 show ?thesis
-      by (simp only: power_BIT mod_BIT int_and_Bits) simp
-  qed
-qed
-
 
 text {* Minimum and maximum *}
 
@@ -283,3 +61,4 @@
   integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"
 
 end
+
diff -r edb87aac9cca -r 783861a66a60 src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Wed Nov 13 15:36:32 2013 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Wed Nov 13 19:12:15 2013 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory SPARK_Setup
-imports Word
+imports "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
 keywords
   "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
   "spark_open_siv" :: thy_load ("siv", "fdl", "rls") and
diff -r edb87aac9cca -r 783861a66a60 src/HOL/Word/Bit_Comparison.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bit_Comparison.thy	Wed Nov 13 19:12:15 2013 +0100
@@ -0,0 +1,193 @@
+(*  Title:      HOL/SPARK/SPARK.thy
+    Author:     Stefan Berghofer
+    Copyright:  secunet Security Networks AG
+
+Comparison on bit operations on integers.
+*)
+
+theory Bit_Comparison
+imports Type_Length Bit_Operations Bit_Int
+begin
+
+lemma AND_lower [simp]:
+  fixes x :: int and y :: int
+  assumes "0 \<le> x"
+  shows "0 \<le> x AND 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 (simp add: Bit_def bitval_def split add: bit.split_asm)
+    then have "0 \<le> bin AND bin'" by (rule 3)
+    with 1 show ?thesis
+      by simp (simp add: Bit_def bitval_def split add: bit.split)
+  qed
+next
+  case 2
+  then show ?case by (simp only: Min_def)
+qed simp
+
+lemma OR_lower [simp]:
+  fixes x :: int and 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 (simp add: Bit_def bitval_def split add: bit.split_asm)
+    moreover from 1 3 have "0 \<le> bin'"
+      by (simp add: Bit_def bitval_def split add: bit.split_asm)
+    ultimately have "0 \<le> bin OR bin'" by (rule 3)
+    with 1 show ?thesis
+      by simp (simp add: Bit_def bitval_def split add: bit.split)
+  qed
+qed simp_all
+
+lemma XOR_lower [simp]:
+  fixes x :: int and 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 (simp add: Bit_def bitval_def split add: bit.split_asm)
+    moreover from 1 3 have "0 \<le> bin'"
+      by (simp add: Bit_def bitval_def split add: bit.split_asm)
+    ultimately have "0 \<le> bin XOR bin'" by (rule 3)
+    with 1 show ?thesis
+      by simp (simp add: Bit_def bitval_def split add: bit.split)
+  qed
+next
+  case 2
+  then show ?case by (simp only: Min_def)
+qed simp
+
+lemma AND_upper1 [simp]:
+  fixes x :: int and 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 (simp add: Bit_def bitval_def split add: bit.split_asm)
+    then have "bin AND bin' \<le> bin" by (rule 3)
+    with 1 show ?thesis
+      by simp (simp add: Bit_def bitval_def split add: bit.split)
+  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 :: int and y :: int
+  assumes "0 \<le> y"
+  shows "x AND y \<le> y"
+  using assms
+proof (induct y arbitrary: x rule: bin_induct)
+  case (3 bin bit)
+  show ?case
+  proof (cases x rule: bin_exhaust)
+    case (1 bin' bit')
+    from 3 have "0 \<le> bin"
+      by (simp add: Bit_def bitval_def split add: bit.split_asm)
+    then have "bin' AND bin \<le> bin" by (rule 3)
+    with 1 show ?thesis
+      by simp (simp add: Bit_def bitval_def split add: bit.split)
+  qed
+next
+  case 2
+  then show ?case by (simp only: Min_def)
+qed simp
+
+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 :: int and 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" "bit = 0"
+        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
+      then show ?thesis using 0 1 `y < 2 ^ n`
+        by simp
+    next
+      case (Suc m)
+      from 3 have "0 \<le> bin"
+        by (simp add: Bit_def bitval_def split add: bit.split_asm)
+      moreover from 3 Suc have "bin < 2 ^ m"
+        by (simp add: Bit_def bitval_def split add: bit.split_asm)
+      moreover from 1 3 Suc have "bin' < 2 ^ m"
+        by (simp add: Bit_def bitval_def split add: bit.split_asm)
+      ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
+      with 1 Suc show ?thesis
+        by simp (simp add: Bit_def bitval_def split add: bit.split)
+    qed
+  qed
+qed simp_all
+
+lemma XOR_upper:
+  fixes x :: int and 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 (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" "bit = 0"
+        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
+      then show ?thesis using 0 1 `y < 2 ^ n`
+        by simp
+    next
+      case (Suc m)
+      from 3 have "0 \<le> bin"
+        by (simp add: Bit_def bitval_def split add: bit.split_asm)
+      moreover from 3 Suc have "bin < 2 ^ m"
+        by (simp add: Bit_def bitval_def split add: bit.split_asm)
+      moreover from 1 3 Suc have "bin' < 2 ^ m"
+        by (simp add: Bit_def bitval_def split add: bit.split_asm)
+      ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
+      with 1 Suc show ?thesis
+        by simp (simp add: Bit_def bitval_def split add: bit.split)
+    qed
+  qed
+next
+  case 2
+  then show ?case by (simp only: Min_def)
+qed simp
+
+end
diff -r edb87aac9cca -r 783861a66a60 src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Wed Nov 13 15:36:32 2013 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Wed Nov 13 19:12:15 2013 +0100
@@ -632,5 +632,46 @@
   "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
   by auto
 
+lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
+  unfolding Bit_B1
+  by (induct n) simp_all
+
+lemma mod_BIT:
+  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
+proof -
+  have "bin mod 2 ^ n < 2 ^ n" by simp
+  then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
+  then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
+    by (rule mult_left_mono) simp
+  then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
+  then show ?thesis
+    by (auto simp add: Bit_def bitval_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
+      mod_pos_pos_trivial split add: bit.split)
+qed
+
+lemma AND_mod:
+  fixes x :: int
+  shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
+proof (induct x arbitrary: n rule: bin_induct)
+  case 1
+  then show ?case
+    by simp
+next
+  case 2
+  then show ?case
+    by (simp, simp add: m1mod2k)
+next
+  case (3 bin bit)
+  show ?case
+  proof (cases n)
+    case 0
+    then show ?thesis by (simp add: int_and_extra_simps)
+  next
+    case (Suc m)
+    with 3 show ?thesis
+      by (simp only: power_BIT mod_BIT int_and_Bits) simp
+  qed
+qed
+
 end