Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SPARK/SPARK.thy
changeset 41561 d1318f3c86ba
child 47108 2a1953f0d20d 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/SPARK.thy	Sat Jan 15 12:35:29 2011 +0100
@@ -0,0 +1,278 @@
+(*  Title:      HOL/SPARK/SPARK.thy
+    Author:     Stefan Berghofer
+    Copyright:  secunet Security Networks AG
+
+Declaration of proof functions for SPARK/Ada verification environment.
+*)
+
+theory SPARK
+imports SPARK_Setup
+begin
+
+text {* Bitwise logical operators *}
+
+spark_proof_functions
+  bit__and (integer, integer) : integer = "op AND"
+  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 (simp add: Bit0_def int_or_Pls [unfolded Pls_def])
+    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]
+  OR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified]
+  OR_upper [of _ 16, simplified]
+  OR_upper [of _ 32, simplified zle_diff1_eq [symmetric], simplified]
+  OR_upper [of _ 32, simplified]
+  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 (simp add: Bit0_def int_xor_Pls [unfolded Pls_def])
+    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]
+  XOR_upper [of _ 16, simplified zle_diff1_eq [symmetric], simplified]
+  XOR_upper [of _ 16, simplified]
+  XOR_upper [of _ 32, simplified zle_diff1_eq [symmetric], simplified]
+  XOR_upper [of _ 32, simplified]
+  XOR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified]
+  XOR_upper [of _ 64, simplified]
+
+lemma bit_not_spark_eq:
+  "NOT (word_of_int x :: ('a::len0) word) =
+  word_of_int (2 ^ len_of TYPE('a) - 1 - x)"
+proof -
+  have "word_of_int x + NOT (word_of_int x) =
+    word_of_int x + (word_of_int (2 ^ len_of TYPE('a) - 1 - x)::'a word)"
+    by (simp only: bwsimps bin_add_not Min_def)
+      (simp add: word_of_int_hom_syms word_of_int_2p_len)
+  then show ?thesis by (rule add_left_imp_eq)
+qed
+
+lemmas [simp] =
+  bit_not_spark_eq [where 'a=8, simplified]
+  bit_not_spark_eq [where 'a=16, simplified]
+  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 (simp add: Pls_def)
+next
+  case 2
+  then show ?case
+    by (simp, simp only: Min_def, 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 [unfolded Pls_def])
+  next
+    case (Suc m)
+    with 3 show ?thesis
+      by (simp only: power_BIT mod_BIT int_and_Bits) simp
+  qed
+qed
+
+end
isabelle