src/HOL/SPARK/SPARK.thy

more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
tuned signature;

(*  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
    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
    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
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 *}

spark_proof_functions
  integer__min = "min :: int \<Rightarrow> int \<Rightarrow> int"
  integer__max = "max :: int \<Rightarrow> int \<Rightarrow> int"

end