Quelle Bit_Operations.thy Sprache: Isabelle

(*  Author:  Florian Haftmann, TUM
*)

section \<open>Bit operations in suitable algebraic structures\<close>

theory Bit_Operations
  imports Presburger Groups_List
begin

subsection \<open>Abstract bit structures\<close>

class semiring_bits = semiring_parity + semiring_modulo_trivial +
  assumes bit_induct [case_names stable rec]:
    \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
     \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
        \<Longrightarrow> P a\<close>
  assumes bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
    and half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
    and even_double_div_exp_iff: \<open>2 ^ Suc n \<noteq> 0 \<Longrightarrow> even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close>
  fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>
  assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close>
begin

text \<open>
  Having \<^const>\<open>bit\<close> as definitional class operation
  takes into account that specific instances can be implemented
  differently wrt. code generation.
\<close>

lemma half_1 [simp]:
  \<open>1 div 2 = 0\<close>
  using even_half_succ_eq [of 0] by simp

lemma div_exp_eq_funpow_half:
  \<open>a div 2 ^ n = ((\<lambda>a. a div 2) ^^ n) a\<close>
proof -
  have \<open>((\<lambda>a. a div 2) ^^ n) = (\<lambda>a. a div 2 ^ n)\<close>
    by (induction n)
      (simp_all del: funpow.simps power.simps add: power_0 funpow_Suc_right half_div_exp_eq)
  then show ?thesis
    by simp
qed

lemma div_exp_eq:
  \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
  by (simp add: div_exp_eq_funpow_half Groups.add.commute [of m] funpow_add)

lemma bit_0:
  \<open>bit a 0 \<longleftrightarrow> odd a\<close>
  by (simp add: bit_iff_odd)

lemma bit_Suc:
  \<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close>
  using div_exp_eq [of a 1 n] by (simp add: bit_iff_odd)

lemma bit_rec:
  \<open>bit a n \<longleftrightarrow> (if n = 0 then odd a else bit (a div 2) (n - 1))\<close>
  by (cases n) (simp_all add: bit_Suc bit_0)

context
  fixes a
  assumes stable: \<open>a div 2 = a\<close>
begin

lemma bits_stable_imp_add_self:
  \<open>a + a mod 2 = 0\<close>
proof -
  have \<open>a div 2 * 2 + a mod 2 = a\<close>
    by (fact div_mult_mod_eq)
  then have \<open>a * 2 + a mod 2 = a\<close>
    by (simp add: stable)
  then show ?thesis
    by (simp add: mult_2_right ac_simps)
qed

lemma stable_imp_bit_iff_odd:
  \<open>bit a n \<longleftrightarrow> odd a\<close>
  by (induction n) (simp_all add: stable bit_Suc bit_0)

end

lemma bit_iff_odd_imp_stable:
  \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close>
using that proof (induction a rule: bit_induct)
  case (stable a)
  then show ?case
    by simp
next
  case (rec a b)
  from rec.prems [of 1] have [simp]: \<open>b = odd a\<close>
    by (simp add: rec.hyps bit_Suc bit_0)
  from rec.hyps have hyp: \<open>(of_bool (odd a) + 2 * a) div 2 = a\<close>
    by simp
  have \<open>bit a n \<longleftrightarrow> odd a\<close> for n
    using rec.prems [of \<open>Suc n\<close>] by (simp add: hyp bit_Suc)
  then have \<open>a div 2 = a\<close>
    by (rule rec.IH)
  then have \<open>of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)\<close>
    by (simp add: ac_simps)
  also have \<open>\<dots> = a\<close>
    using mult_div_mod_eq [of 2 a]
    by (simp add: of_bool_odd_eq_mod_2)
  finally show ?case
    using \<open>a div 2 = a\<close> by (simp add: hyp)
qed

lemma even_succ_div_exp [simp]:
  \<open>(1 + a) div 2 ^ n = a div 2 ^ n\<close> if \<open>even a\<close> and \<open>n > 0\<close>
proof (cases n)
  case 0
  with that show ?thesis
    by simp
next
  case (Suc n)
  with \<open>even a\<close> have \<open>(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\<close>
  proof (induction n)
    case 0
    then show ?case
      by simp
  next
    case (Suc n)
    then show ?case
      using div_exp_eq [of _ 1 \<open>Suc n\<close>, symmetric]
      by simp
  qed
  with Suc show ?thesis
    by simp
qed

lemma even_succ_mod_exp [simp]:
  \<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close>
  using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] div_mult_mod_eq [of a \<open>2 ^ n\<close>] that
  by simp (metis (full_types) add.left_commute add_left_imp_eq)

lemma half_numeral_Bit1_eq [simp]:
  \<open>numeral (num.Bit1 m) div 2 = numeral (num.Bit0 m) div 2\<close>
  using even_half_succ_eq [of \<open>2 * numeral m\<close>]
  by simp

lemma double_half_numeral_Bit_0_eq [simp]:
  \<open>2 * (numeral (num.Bit0 m) div 2) = numeral (num.Bit0 m)\<close>
  \<open>(numeral (num.Bit0 m) div 2) * 2 = numeral (num.Bit0 m)\<close>
  using mod_mult_div_eq [of \<open>numeral (Num.Bit0 m)\<close> 2]
  by (simp_all add: mod2_eq_if ac_simps)

named_theorems bit_simps \<open>Simplification rules for \<^const>\<open>bit\<close>\<close>

definition possible_bit :: \<open>'a itself \<Rightarrow> nat \<Rightarrow> bool\<close>
  where \<open>possible_bit TYPE('a) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
  \<comment> \<open>This auxiliary avoids non-termination with extensionality.\<close>

lemma possible_bit_0 [simp]:
  \<open>possible_bit TYPE('a) 0\<close>
  by (simp add: possible_bit_def)

lemma fold_possible_bit:
  \<open>2 ^ n = 0 \<longleftrightarrow> \<not> possible_bit TYPE('a) n\<close>
  by (simp add: possible_bit_def)

lemma bit_imp_possible_bit:
  \<open>possible_bit TYPE('a) n\<close> if \<open>bit a n\<close>
  by (rule ccontr) (use that in \<open>auto simp: bit_iff_odd possible_bit_def\<close>)

lemma impossible_bit:
  \<open>\<not> bit a n\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
  using that by (blast dest: bit_imp_possible_bit)

lemma possible_bit_less_imp:
  \<open>possible_bit TYPE('a) j\<close> if \<open>possible_bit TYPE('a) i\<close> \<open>j \<le> i\<close>
  using power_add [of 2 j \<open>i - j\<close>] that mult_not_zero [of \<open>2 ^ j\<close> \<open>2 ^ (i - j)\<close>]
  by (simp add: possible_bit_def)

lemma possible_bit_min [simp]:
  \<open>possible_bit TYPE('a) (min i j) \<longleftrightarrow> possible_bit TYPE('a) i \<or> possible_bit TYPE('a) j\<close>
  by (auto simp: min_def elim: possible_bit_less_imp)

lemma bit_eqI:
  \<open>a = b\<close> if \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
proof -
  have \<open>bit a n \<longleftrightarrow> bit b n\<close> for n
  proof (cases \<open>possible_bit TYPE('a) n\<close>)
    case False
    then show ?thesis
      by (simp add: impossible_bit)
  next
    case True
    then show ?thesis
      by (rule that)
  qed
  then show ?thesis proof (induction a arbitrary: b rule: bit_induct)
    case (stable a)
    from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close>
      by (simp add: bit_0)
    have \<open>b div 2 = b\<close>
    proof (rule bit_iff_odd_imp_stable)
      fix n
      from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close>
        by simp
      also have \<open>bit a n \<longleftrightarrow> odd a\<close>
        using stable by (simp add: stable_imp_bit_iff_odd)
      finally show \<open>bit b n \<longleftrightarrow> odd b\<close>
        by (simp add: **)
    qed
    from ** have \<open>a mod 2 = b mod 2\<close>
      by (simp add: mod2_eq_if)
    then have \<open>a mod 2 + (a + b) = b mod 2 + (a + b)\<close>
      by simp
    then have \<open>a + a mod 2 + b = b + b mod 2 + a\<close>
      by (simp add: ac_simps)
    with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
      by (simp add: bits_stable_imp_add_self)
  next
    case (rec a p)
    from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
      by (simp add: bit_0)
    from rec.hyps have \<open>bit a n \<longleftrightarrow> bit (b div 2) n\<close> for n
      using rec.prems [of \<open>Suc n\<close>] by (simp add: bit_Suc)
    then have \<open>a = b div 2\<close>
      by (rule rec.IH)
    then have \<open>2 * a = 2 * (b div 2)\<close>
      by simp
    then have \<open>b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\<close>
      by simp
    also have \<open>\<dots> = b\<close>
      by (fact mod_mult_div_eq)
    finally show ?case
      by (auto simp: mod2_eq_if)
  qed
qed

lemma bit_eq_rec:
  \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close> (is \<open>?P = ?Q\<close>)
proof
  assume ?P
  then show ?Q
    by simp
next
  assume ?Q
  then have \<open>even a \<longleftrightarrow> even b\<close> and \<open>a div 2 = b div 2\<close>
    by simp_all
  show ?P
  proof (rule bit_eqI)
    fix n
    show \<open>bit a n \<longleftrightarrow> bit b n\<close>
    proof (cases n)
      case 0
      with \<open>even a \<longleftrightarrow> even b\<close> show ?thesis
        by (simp add: bit_0)
    next
      case (Suc n)
      moreover from \<open>a div 2 = b div 2\<close> have \<open>bit (a div 2) n = bit (b div 2) n\<close>
        by simp
      ultimately show ?thesis
        by (simp add: bit_Suc)
    qed
  qed
qed

lemma bit_eq_iff:
  \<open>a = b \<longleftrightarrow> (\<forall>n. possible_bit TYPE('a) n \<longrightarrow> bit a n \<longleftrightarrow> bit b n)\<close>
  by (auto intro: bit_eqI simp add: possible_bit_def)

lemma bit_0_eq [simp]:
  \<open>bit 0 = \<bottom>\<close>
proof -
  have \<open>0 div 2 ^ n = 0\<close> for n
    unfolding div_exp_eq_funpow_half by (induction n) simp_all
  then show ?thesis
    by (simp add: fun_eq_iff bit_iff_odd)
qed

lemma bit_double_Suc_iff:
  \<open>bit (2 * a) (Suc n) \<longleftrightarrow> possible_bit TYPE('a) (Suc n) \<and> bit a n\<close>
  using even_double_div_exp_iff [of n a]
  by (cases \<open>possible_bit TYPE('a) (Suc n)\<close>)
    (auto simp: bit_iff_odd possible_bit_def)

lemma bit_double_iff [bit_simps]:
  \<open>bit (2 * a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<noteq> 0 \<and> bit a (n - 1)\<close>
  by (cases n) (simp_all add: bit_0 bit_double_Suc_iff)

lemma even_bit_succ_iff:
  \<open>bit (1 + a) n \<longleftrightarrow> bit a n \<or> n = 0\<close> if \<open>even a\<close>
  using that by (cases \<open>n = 0\<close>) (simp_all add: bit_iff_odd)

lemma odd_bit_iff_bit_pred:
  \<open>bit a n \<longleftrightarrow> bit (a - 1) n \<or> n = 0\<close> if \<open>odd a\<close>
proof -
  from \<open>odd a\<close> obtain b where \<open>a = 2 * b + 1\<close> ..
  moreover have \<open>bit (2 * b) n \<or> n = 0 \<longleftrightarrow> bit (1 + 2 * b) n\<close>
    using even_bit_succ_iff by simp
  ultimately show ?thesis by (simp add: ac_simps)
qed

lemma bit_exp_iff [bit_simps]:
  \<open>bit (2 ^ m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n = m\<close>
proof (cases \<open>possible_bit TYPE('a) n\<close>)
  case False
  then show ?thesis
    by (simp add: impossible_bit)
next
  case True
  then show ?thesis
  proof (induction n arbitrary: m)
    case 0
    show ?case
      by (simp add: bit_0)
  next
    case (Suc n)
    then have \<open>possible_bit TYPE('a) n\<close>
      by (simp add: possible_bit_less_imp)
    show ?case
    proof (cases m)
      case 0
      then show ?thesis
        by (simp add: bit_Suc)
    next
      case (Suc m)
      with Suc.IH [of m] \<open>possible_bit TYPE('a) n\<close> show ?thesis
        by (simp add: bit_double_Suc_iff)
    qed
  qed
qed

lemma bit_1_iff [bit_simps]:
  \<open>bit 1 n \<longleftrightarrow> n = 0\<close>
  using bit_exp_iff [of 0 n] by auto

lemma bit_2_iff [bit_simps]:
  \<open>bit 2 n \<longleftrightarrow> possible_bit TYPE('a) 1 \<and> n = 1\<close>
  using bit_exp_iff [of 1 n] by auto

lemma bit_of_bool_iff [bit_simps]:
  \<open>bit (of_bool b) n \<longleftrightarrow> n = 0 \<and> b\<close>
  by (simp add: bit_1_iff)

lemma bit_mod_2_iff [simp]:
  \<open>bit (a mod 2) n \<longleftrightarrow> n = 0 \<and> odd a\<close>
  by (simp add: mod_2_eq_odd bit_simps)

lemma stable_index:
  obtains m where \<open>possible_bit TYPE('a) m\<close>
    \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> bit a n \<longleftrightarrow> bit a m\<close>
proof -
  have \<open>\<exists>m. possible_bit TYPE('a) m \<and> (\<forall>n\<ge>m. possible_bit TYPE('a) n \<longrightarrow> bit a n \<longleftrightarrow> bit a m)\<close>
  proof (induction a rule: bit_induct)
    case (stable a)
    show ?case
      by (rule exI [of _ \<open>0::nat\<close>]) (simp add: stable_imp_bit_iff_odd stable)
  next
    case (rec a b)
    then obtain m where \<open>possible_bit TYPE('a) m\<close>
       and hyp: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> bit a n \<longleftrightarrow> bit a m\<close>
      by blast
    show ?case
    proof (cases \<open>possible_bit TYPE('a) (Suc m)\<close>)
      case True
      moreover have \<open>bit (of_bool b + 2 * a) n \<longleftrightarrow> bit (of_bool b + 2 * a) (Suc m)\<close>
        if \<open>possible_bit TYPE('a) n\<close> \<open>Suc m \<le> n\<close> for n
        using hyp [of \<open>n - 1\<close>] possible_bit_less_imp [of n \<open>n - 1\<close>] rec.hyps that
        by (cases n) (simp_all add: bit_Suc)
      ultimately show ?thesis
        by blast
    next
      case False
      have \<open>bit (of_bool b + 2 * a) n \<longleftrightarrow> bit (of_bool b + 2 * a) m\<close>
        if \<open>possible_bit TYPE('a) n\<close> \<open>m \<le> n\<close> for n
      proof (cases \<open>m = n\<close>)
        case True
        then show ?thesis
          by simp
      next
        case False
        with \<open>m \<le> n\<close> have \<open>m < n\<close>
          by simp
        with \<open>\<not> possible_bit TYPE('a) (Suc m)\<close>
        have \<open>\<not> possible_bit TYPE('a) n\<close> using possible_bit_less_imp [of n \<open>Suc m\<close>]
          by auto
        with \<open>possible_bit TYPE('a) n\<close>
        show ?thesis
          by simp
      qed
      with \<open>possible_bit TYPE('a) m\<close> show ?thesis
        by blast
    qed
  qed
  with that show thesis
    by blast
qed

end

lemma nat_bit_induct [case_names zero even odd]:
  \<open>P n\<close> if zero: \<open>P 0\<close>
    and even: \<open>\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)\<close>
    and odd: \<open>\<And>n. P n \<Longrightarrow> P (Suc (2 * n))\<close>
proof (induction n rule: less_induct)
  case (less n)
  show \<open>P n\<close>
  proof (cases \<open>n = 0\<close>)
    case True with zero show ?thesis by simp
  next
    case False
    with less have hyp: \<open>P (n div 2)\<close> by simp
    show ?thesis
    proof (cases \<open>even n\<close>)
      case True
      then have \<open>n \<noteq> 1\<close>
        by auto
      with \<open>n \<noteq> 0\<close> have \<open>n div 2 > 0\<close>
        by simp
      with \<open>even n\<close> hyp even [of \<open>n div 2\<close>] show ?thesis
        by simp
    next
      case False
      with hyp odd [of \<open>n div 2\<close>] show ?thesis
        by simp
    qed
  qed
qed

instantiation nat :: semiring_bits
begin

definition bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> bool\<close>
  where \<open>bit_nat m n \<longleftrightarrow> odd (m div 2 ^ n)\<close>

instance
proof
  show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close>
    and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close>
    for P and n :: nat
  proof (induction n rule: nat_bit_induct)
    case zero
    from stable [of 0] show ?case
      by simp
  next
    case (even n)
    with rec [of n False] show ?case
      by simp
  next
    case (odd n)
    with rec [of n True] show ?case
      by simp
  qed
qed (auto simp: div_mult2_eq bit_nat_def)

end

lemma possible_bit_nat [simp]:
  \<open>possible_bit TYPE(nat) n\<close>
  by (simp add: possible_bit_def)

lemma bit_Suc_0_iff [bit_simps]:
  \<open>bit (Suc 0) n \<longleftrightarrow> n = 0\<close>
  using bit_1_iff [of n, where ?'a = nat] by simp

lemma not_bit_Suc_0_Suc [simp]:
  \<open>\<not> bit (Suc 0) (Suc n)\<close>
  by (simp add: bit_Suc)

lemma not_bit_Suc_0_numeral [simp]:
  \<open>\<not> bit (Suc 0) (numeral n)\<close>
  by (simp add: numeral_eq_Suc)

context semiring_bits
begin

lemma bit_of_nat_iff [bit_simps]:
  \<open>bit (of_nat m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit m n\<close>
proof (cases \<open>possible_bit TYPE('a) n\<close>)
  case False
  then show ?thesis
    by (simp add: impossible_bit)
next
  case True
  then have \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
  proof (induction m arbitrary: n rule: nat_bit_induct)
    case zero
    then show ?case
      by simp
  next
    case (even m)
    then show ?case
      by (cases n)
        (auto simp: bit_double_iff Bit_Operations.bit_double_iff possible_bit_def bit_0 dest: mult_not_zero)
  next
    case (odd m)
    then show ?case
      by (cases n)
        (auto simp: bit_double_iff even_bit_succ_iff possible_bit_def
          Bit_Operations.bit_Suc Bit_Operations.bit_0 dest: mult_not_zero)
  qed
  with True show ?thesis
    by simp
qed

end

lemma int_bit_induct [case_names zero minus even odd]:
  \<open>P k\<close> if zero_int: \<open>P 0\<close>
    and minus_int: \<open>P (- 1)\<close>
    and even_int: \<open>\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)\<close>
    and odd_int: \<open>\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))\<close> for k :: int
proof (cases \<open>k \<ge> 0\<close>)
  case True
  define n where \<open>n = nat k\<close>
  with True have \<open>k = int n\<close>
    by simp
  then show \<open>P k\<close>
  proof (induction n arbitrary: k rule: nat_bit_induct)
    case zero
    then show ?case
      by (simp add: zero_int)
  next
    case (even n)
    have \<open>P (int n * 2)\<close>
      by (rule even_int) (use even in simp_all)
    with even show ?case
      by (simp add: ac_simps)
  next
    case (odd n)
    have \<open>P (1 + (int n * 2))\<close>
      by (rule odd_int) (use odd in simp_all)
    with odd show ?case
      by (simp add: ac_simps)
  qed
next
  case False
  define n where \<open>n = nat (- k - 1)\<close>
  with False have \<open>k = - int n - 1\<close>
    by simp
  then show \<open>P k\<close>
  proof (induction n arbitrary: k rule: nat_bit_induct)
    case zero
    then show ?case
      by (simp add: minus_int)
  next
    case (even n)
    have \<open>P (1 + (- int (Suc n) * 2))\<close>
      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
    also have \<open>\<dots> = - int (2 * n) - 1\<close>
      by (simp add: algebra_simps)
    finally show ?case
      using even.prems by simp
  next
    case (odd n)
    have \<open>P (- int (Suc n) * 2)\<close>
      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
    also have \<open>\<dots> = - int (Suc (2 * n)) - 1\<close>
      by (simp add: algebra_simps)
    finally show ?case
      using odd.prems by simp
  qed
qed

instantiation int :: semiring_bits
begin

definition bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
  where \<open>bit_int k n \<longleftrightarrow> odd (k div 2 ^ n)\<close>

instance
proof
  show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close>
    and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close>
    for P and k :: int
  proof (induction k rule: int_bit_induct)
    case zero
    from stable [of 0] show ?case
      by simp
  next
    case minus
    from stable [of \<open>- 1\<close>] show ?case
      by simp
  next
    case (even k)
    with rec [of k False] show ?case
      by (simp add: ac_simps)
  next
    case (odd k)
    with rec [of k True] show ?case
      by (simp add: ac_simps)
  qed
qed (auto simp: zdiv_zmult2_eq bit_int_def)

end

lemma possible_bit_int [simp]:
  \<open>possible_bit TYPE(int) n\<close>
  by (simp add: possible_bit_def)

lemma bit_nat_iff [bit_simps]:
  \<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
proof (cases \<open>k \<ge> 0\<close>)
  case True
  moreover define m where \<open>m = nat k\<close>
  ultimately have \<open>k = int m\<close>
    by simp
  then show ?thesis
    by (simp add: bit_simps)
next
  case False
  then show ?thesis
    by simp
qed

subsection \<open>Bit operations\<close>

class semiring_bit_operations = semiring_bits +
  fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>AND\<close> 64)
    and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>OR\<close> 59)
    and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>XOR\<close> 59)
    and mask :: \<open>nat \<Rightarrow> 'a\<close>
    and set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
    and unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
    and flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
    and push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
    and drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
    and take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
  assumes and_rec: \<open>a AND b = of_bool (odd a \<and> odd b) + 2 * ((a div 2) AND (b div 2))\<close>
    and or_rec: \<open>a OR b = of_bool (odd a \<or> odd b) + 2 * ((a div 2) OR (b div 2))\<close>
    and xor_rec: \<open>a XOR b = of_bool (odd a \<noteq> odd b) + 2 * ((a div 2) XOR (b div 2))\<close>
    and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
    and set_bit_eq_or: \<open>set_bit n a = a OR push_bit n 1\<close>
    and unset_bit_eq_or_xor: \<open>unset_bit n a = (a OR push_bit n 1) XOR push_bit n 1\<close>
    and flip_bit_eq_xor: \<open>flip_bit n a = a XOR push_bit n 1\<close>
    and push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close>
    and drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
    and take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
begin

text \<open>
  We want the bitwise operations to bind slightly weaker
  than \<open>+\<close> and \<open>-\<close>.

  Logically, \<^const>\<open>push_bit\<close>,
  \<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them
  as separate operations makes proofs easier, otherwise proof automation
  would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic
  algebraic relationships between those operations.

  For the sake of code generation operations
  are specified as definitional class operations,
  taking into account that specific instances of these can be implemented
  differently wrt. code generation.
\<close>

lemma bit_iff_odd_drop_bit:
  \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
  by (simp add: bit_iff_odd drop_bit_eq_div)

lemma even_drop_bit_iff_not_bit:
  \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close>
  by (simp add: bit_iff_odd_drop_bit)

lemma bit_and_iff [bit_simps]:
  \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
proof (induction n arbitrary: a b)
  case 0
  show ?case
    by (simp add: bit_0 and_rec [of a b] even_bit_succ_iff)
next
  case (Suc n)
  from Suc [of \<open>a div 2\<close> \<open>b div 2\<close>]
  show ?case
    by (simp add: and_rec [of a b] bit_Suc)
      (auto simp flip: bit_Suc simp add: bit_double_iff dest: bit_imp_possible_bit)
qed

lemma bit_or_iff [bit_simps]:
  \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
proof (induction n arbitrary: a b)
  case 0
  show ?case
    by (simp add: bit_0 or_rec [of a b] even_bit_succ_iff)
next
  case (Suc n)
  from Suc [of \<open>a div 2\<close> \<open>b div 2\<close>]
  show ?case
    by (simp add: or_rec [of a b] bit_Suc)
      (auto simp flip: bit_Suc simp add: bit_double_iff dest: bit_imp_possible_bit)
qed

lemma bit_xor_iff [bit_simps]:
  \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
proof (induction n arbitrary: a b)
  case 0
  show ?case
    by (simp add: bit_0 xor_rec [of a b] even_bit_succ_iff)
next
  case (Suc n)
  from Suc [of \<open>a div 2\<close> \<open>b div 2\<close>]
  show ?case
    by (simp add: xor_rec [of a b] bit_Suc)
      (auto simp flip: bit_Suc simp add: bit_double_iff dest: bit_imp_possible_bit)
qed

sublocale "and": semilattice \<open>(AND)\<close>
  by standard (auto simp: bit_eq_iff bit_and_iff)

sublocale or: semilattice_neutr \<open>(OR)\<close> 0
  by standard (auto simp: bit_eq_iff bit_or_iff)

sublocale xor: comm_monoid \<open>(XOR)\<close> 0
  by standard (auto simp: bit_eq_iff bit_xor_iff)

lemma even_and_iff:
  \<open>even (a AND b) \<longleftrightarrow> even a \<or> even b\<close>
  using bit_and_iff [of a b 0] by (auto simp: bit_0)

lemma even_or_iff:
  \<open>even (a OR b) \<longleftrightarrow> even a \<and> even b\<close>
  using bit_or_iff [of a b 0] by (auto simp: bit_0)

lemma even_xor_iff:
  \<open>even (a XOR b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close>
  using bit_xor_iff [of a b 0] by (auto simp: bit_0)

lemma zero_and_eq [simp]:
  \<open>0 AND a = 0\<close>
  by (simp add: bit_eq_iff bit_and_iff)

lemma and_zero_eq [simp]:
  \<open>a AND 0 = 0\<close>
  by (simp add: bit_eq_iff bit_and_iff)

lemma one_and_eq:
  \<open>1 AND a = a mod 2\<close>
  by (simp add: bit_eq_iff bit_and_iff) (auto simp: bit_1_iff bit_0)

lemma and_one_eq:
  \<open>a AND 1 = a mod 2\<close>
  using one_and_eq [of a] by (simp add: ac_simps)

lemma one_or_eq:
  \<open>1 OR a = a + of_bool (even a)\<close>
  by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff)
    (auto simp: bit_1_iff bit_0)

lemma or_one_eq:
  \<open>a OR 1 = a + of_bool (even a)\<close>
  using one_or_eq [of a] by (simp add: ac_simps)

lemma one_xor_eq:
  \<open>1 XOR a = a + of_bool (even a) - of_bool (odd a)\<close>
  by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff)
    (auto simp: bit_1_iff odd_bit_iff_bit_pred bit_0 elim: oddE)

lemma xor_one_eq:
  \<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
  using one_xor_eq [of a] by (simp add: ac_simps)

lemma xor_self_eq [simp]:
  \<open>a XOR a = 0\<close>
  by (rule bit_eqI) (simp add: bit_simps)

lemma mask_0 [simp]:
  \<open>mask 0 = 0\<close>
  by (simp add: mask_eq_exp_minus_1)

lemma inc_mask_eq_exp:
  \<open>mask n + 1 = 2 ^ n\<close>
proof (induction n)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  from Suc.IH [symmetric] have \<open>2 ^ Suc n = 2 * mask n + 2\<close>
    by (simp add: algebra_simps)
  also have \<open>\<dots> = 2 * mask n + 1 + 1\<close>
    by (simp add: add.assoc)
  finally have *: \<open>2 ^ Suc n = 2 * mask n + 1 + 1\<close> .
  then show ?case
    by (simp add: mask_eq_exp_minus_1)
qed

lemma mask_eq_iff_eq_exp:
  \<open>mask n = a \<longleftrightarrow> a + 1 = 2 ^ n\<close>
  by (auto simp flip: inc_mask_eq_exp)

lemma eq_mask_iff_eq_exp:
  \<open>a = mask n \<longleftrightarrow> a + 1 = 2 ^ n\<close>
  by (auto simp flip: inc_mask_eq_exp)

lemma mask_Suc_double:
  \<open>mask (Suc n) = 1 OR 2 * mask n\<close>
proof -
  have \<open>mask (Suc n) + 1 = (mask n + 1) + (mask n + 1)\<close>
    by (simp add: inc_mask_eq_exp mult_2)
  also have \<open>\<dots> = (1 OR 2 * mask n) + 1\<close>
    by (simp add: one_or_eq mult_2_right algebra_simps)
  finally show ?thesis
    by simp
qed

lemma bit_mask_iff [bit_simps]:
  \<open>bit (mask m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < m\<close>
proof (cases \<open>possible_bit TYPE('a) n\<close>)
  case False
  then show ?thesis
    by (simp add: impossible_bit)
next
  case True
  then have \<open>bit (mask m) n \<longleftrightarrow> n < m\<close>
  proof (induction m arbitrary: n)
    case 0
    then show ?case
      by (simp add: bit_iff_odd)
  next
    case (Suc m)
    show ?case
    proof (cases n)
      case 0
      then show ?thesis
        by (simp add: bit_0 mask_Suc_double even_or_iff)
    next
      case (Suc n)
      with Suc.prems have \<open>possible_bit TYPE('a) n\<close>
        using possible_bit_less_imp by auto
      with Suc.IH [of n] have \<open>bit (mask m) n \<longleftrightarrow> n < m\<close> .
      with Suc.prems show ?thesis
        by (simp add: Suc mask_Suc_double bit_simps)
    qed
  qed
  with True show ?thesis
    by simp
qed

lemma even_mask_iff:
  \<open>even (mask n) \<longleftrightarrow> n = 0\<close>
  using bit_mask_iff [of n 0] by (auto simp: bit_0)

lemma mask_Suc_0 [simp]:
  \<open>mask (Suc 0) = 1\<close>
  by (simp add: mask_Suc_double)

lemma mask_Suc_exp:
  \<open>mask (Suc n) = 2 ^ n OR mask n\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma mask_numeral:
  \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
  by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps)

lemma push_bit_0_id [simp]:
  \<open>push_bit 0 = id\<close>
  by (simp add: fun_eq_iff push_bit_eq_mult)

lemma push_bit_Suc [simp]:
  \<open>push_bit (Suc n) a = push_bit n (a * 2)\<close>
  by (simp add: push_bit_eq_mult ac_simps)

lemma push_bit_double:
  \<open>push_bit n (a * 2) = push_bit n a * 2\<close>
  by (simp add: push_bit_eq_mult ac_simps)

lemma bit_push_bit_iff [bit_simps]:
  \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> possible_bit TYPE('a) n \<and> bit a (n - m)\<close>
proof (induction n arbitrary: m)
  case 0
  then show ?case
    by (auto simp: bit_0 push_bit_eq_mult)
next
  case (Suc n)
  show ?case
  proof (cases m)
    case 0
    then show ?thesis
      by (auto simp: bit_imp_possible_bit)
  next
    case (Suc m')
    with Suc.prems Suc.IH [of m'] show ?thesis
      apply (simp add: push_bit_double)
      apply (auto simp: possible_bit_less_imp bit_simps mult.commute [of _ 2])
      done
  qed
qed

lemma funpow_double_eq_push_bit:
  \<open>times 2 ^^ n = push_bit n\<close>
  by (induction n) (simp_all add: fun_eq_iff push_bit_double ac_simps)

lemma div_push_bit_of_1_eq_drop_bit:
  \<open>a div push_bit n 1 = drop_bit n a\<close>
  by (simp add: push_bit_eq_mult drop_bit_eq_div)

lemma bits_ident:
  \<open>push_bit n (drop_bit n a) + take_bit n a = a\<close>
  using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)

lemma push_bit_push_bit [simp]:
  \<open>push_bit m (push_bit n a) = push_bit (m + n) a\<close>
  by (simp add: push_bit_eq_mult power_add ac_simps)

lemma push_bit_of_0 [simp]:
  \<open>push_bit n 0 = 0\<close>
  by (simp add: push_bit_eq_mult)

lemma push_bit_of_1 [simp]:
  \<open>push_bit n 1 = 2 ^ n\<close>
  by (simp add: push_bit_eq_mult)

lemma push_bit_add:
  \<open>push_bit n (a + b) = push_bit n a + push_bit n b\<close>
  by (simp add: push_bit_eq_mult algebra_simps)

lemma push_bit_numeral [simp]:
  \<open>push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))\<close>
  by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)

lemma bit_drop_bit_eq [bit_simps]:
  \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
  by rule (simp add: drop_bit_eq_div bit_iff_odd div_exp_eq)

lemma disjunctive_xor_eq_or:
  \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
  using that by (auto simp: bit_eq_iff bit_simps)

lemma disjunctive_add_eq_or:
  \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
proof (rule bit_eqI)
  fix n
  assume \<open>possible_bit TYPE('a) n\<close>
  moreover from that have \<open>\<And>n. \<not> bit (a AND b) n\<close>
    by simp
  then have \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
    by (simp add: bit_simps)
  ultimately show \<open>bit (a + b) n \<longleftrightarrow> bit (a OR b) n\<close>
  proof (induction n arbitrary: a b)
    case 0
    from "0"(2)[of 0] show ?case
      by (auto simp: even_or_iff bit_0)
  next
    case (Suc n)
    from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
      by (auto simp: bit_0)
    have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
      using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
    from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
      using possible_bit_less_imp by force
    with \<open>\<And>n. \<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> Suc.IH [of \<open>a div 2\<close> \<open>b div 2\<close>]
    have IH: \<open>bit (a div 2 + b div 2) n \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
      by (simp add: bit_Suc)
    have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
      using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
    also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
      using even by (auto simp: algebra_simps mod2_eq_if)
    finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
      using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
    also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
      by (rule IH)
    finally show ?case
      by (simp add: bit_simps flip: bit_Suc)
  qed
qed

lemma disjunctive_add_eq_xor:
  \<open>a + b = a XOR b\<close> if \<open>a AND b = 0\<close>
  using that by (simp add: disjunctive_add_eq_or disjunctive_xor_eq_or)

lemma take_bit_0 [simp]:
  "take_bit 0 a = 0"
  by (simp add: take_bit_eq_mod)

lemma bit_take_bit_iff [bit_simps]:
  \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close>
proof -
  have \<open>push_bit m (drop_bit m a) AND take_bit m a = 0\<close> (is \<open>?lhs = _\<close>)
  proof (rule bit_eqI)
    fix n
    show \<open>bit ?lhs n \<longleftrightarrow> bit 0 n\<close>
    proof (cases \<open>m \<le> n\<close>)
      case False
      then show ?thesis
        by (simp add: bit_simps)
    next
      case True
      moreover define q where \<open>q = n - m\<close>
      ultimately have \<open>n = m + q\<close> by simp
      moreover have \<open>\<not> bit (take_bit m a) (m + q)\<close>
        by (simp add: take_bit_eq_mod bit_iff_odd flip: div_exp_eq)
      ultimately show ?thesis
        by (simp add: bit_simps)
    qed
  qed
  then have \<open>push_bit m (drop_bit m a) XOR take_bit m a = push_bit m (drop_bit m a) + take_bit m a\<close>
    by (simp add: disjunctive_add_eq_xor)
  also have \<open>\<dots> = a\<close>
    by (simp add: bits_ident)
  finally have \<open>bit (push_bit m (drop_bit m a) XOR take_bit m a) n \<longleftrightarrow> bit a n\<close>
    by simp
  also have \<open>\<dots> \<longleftrightarrow> (m \<le> n \<or> n < m) \<and> bit a n\<close>
    by auto
  also have \<open>\<dots> \<longleftrightarrow> m \<le> n \<and> bit a n \<or> n < m \<and> bit a n\<close>
    by auto
  also have \<open>m \<le> n \<and> bit a n \<longleftrightarrow> bit (push_bit m (drop_bit m a)) n\<close>
    by (auto simp: bit_simps bit_imp_possible_bit)
  finally show ?thesis
    by (auto simp: bit_simps)
qed

lemma take_bit_Suc:
  \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>)
proof (rule bit_eqI)
  fix m
  assume \<open>possible_bit TYPE('a) m\<close>
  then show \<open>bit ?lhs m \<longleftrightarrow> bit ?rhs m\<close>
    apply (cases a rule: parity_cases; cases m)
       apply (simp_all add: bit_simps even_bit_succ_iff mult.commute [of _ 2] add.commute [of _ 1] flip: bit_Suc)
     apply (simp_all add: bit_0)
    done
qed

lemma take_bit_rec:
  \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + a mod 2)\<close>
  by (cases n) (simp_all add: take_bit_Suc)

lemma take_bit_Suc_0 [simp]:
  \<open>take_bit (Suc 0) a = a mod 2\<close>
  by (simp add: take_bit_eq_mod)

lemma take_bit_of_0 [simp]:
  \<open>take_bit n 0 = 0\<close>
  by (rule bit_eqI) (simp add: bit_simps)

lemma take_bit_of_1 [simp]:
  \<open>take_bit n 1 = of_bool (n > 0)\<close>
  by (cases n) (simp_all add: take_bit_Suc)

lemma drop_bit_of_0 [simp]:
  \<open>drop_bit n 0 = 0\<close>
  by (rule bit_eqI) (simp add: bit_simps)

lemma drop_bit_of_1 [simp]:
  \<open>drop_bit n 1 = of_bool (n = 0)\<close>
  by (rule bit_eqI) (simp add: bit_simps ac_simps)

lemma drop_bit_0 [simp]:
  \<open>drop_bit 0 = id\<close>
  by (simp add: fun_eq_iff drop_bit_eq_div)

lemma drop_bit_Suc:
  \<open>drop_bit (Suc n) a = drop_bit n (a div 2)\<close>
  using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)

lemma drop_bit_rec:
  \<open>drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))\<close>
  by (cases n) (simp_all add: drop_bit_Suc)

lemma drop_bit_half:
  \<open>drop_bit n (a div 2) = drop_bit n a div 2\<close>
  by (induction n arbitrary: a) (simp_all add: drop_bit_Suc)

lemma drop_bit_of_bool [simp]:
  \<open>drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)\<close>
  by (cases n) simp_all

lemma even_take_bit_eq [simp]:
  \<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close>
  by (simp add: take_bit_rec [of n a])

lemma take_bit_take_bit [simp]:
  \<open>take_bit m (take_bit n a) = take_bit (min m n) a\<close>
  by (rule bit_eqI) (simp add: bit_simps)

lemma drop_bit_drop_bit [simp]:
  \<open>drop_bit m (drop_bit n a) = drop_bit (m + n) a\<close>
  by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps)

lemma push_bit_take_bit:
  \<open>push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)\<close>
  by (rule bit_eqI) (auto simp: bit_simps)

lemma take_bit_push_bit:
  \<open>take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)\<close>
  by (rule bit_eqI) (auto simp: bit_simps)

lemma take_bit_drop_bit:
  \<open>take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)\<close>
  by (rule bit_eqI) (auto simp: bit_simps)

lemma drop_bit_take_bit:
  \<open>drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)\<close>
  by (rule bit_eqI) (auto simp: bit_simps)

lemma even_push_bit_iff [simp]:
  \<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
  by (simp add: push_bit_eq_mult) auto

lemma stable_imp_drop_bit_eq:
  \<open>drop_bit n a = a\<close>
  if \<open>a div 2 = a\<close>
  by (induction n) (simp_all add: that drop_bit_Suc)

lemma stable_imp_take_bit_eq:
  \<open>take_bit n a = (if even a then 0 else mask n)\<close>
    if \<open>a div 2 = a\<close>
  by (rule bit_eqI) (use that in \<open>simp add: bit_simps stable_imp_bit_iff_odd\<close>)

lemma exp_dvdE:
  assumes \<open>2 ^ n dvd a\<close>
  obtains b where \<open>a = push_bit n b\<close>
proof -
  from assms obtain b where \<open>a = 2 ^ n * b\<close> ..
  then have \<open>a = push_bit n b\<close>
    by (simp add: push_bit_eq_mult ac_simps)
  with that show thesis .
qed

lemma take_bit_eq_0_iff:
  \<open>take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
proof
  assume ?P
  then show ?Q
    by (simp add: take_bit_eq_mod mod_0_imp_dvd)
next
  assume ?Q
  then obtain b where \<open>a = push_bit n b\<close>
    by (rule exp_dvdE)
  then show ?P
    by (simp add: take_bit_push_bit)
qed

lemma take_bit_tightened:
  \<open>take_bit m a = take_bit m b\<close> if \<open>take_bit n a = take_bit n b\<close> and \<open>m \<le> n\<close>
proof -
  from that have \<open>take_bit m (take_bit n a) = take_bit m (take_bit n b)\<close>
    by simp
  then have \<open>take_bit (min m n) a = take_bit (min m n) b\<close>
    by simp
  with that show ?thesis
    by (simp add: min_def)
qed

lemma take_bit_eq_self_iff_drop_bit_eq_0:
  \<open>take_bit n a = a \<longleftrightarrow> drop_bit n a = 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
proof
  assume ?P
  show ?Q
  proof (rule bit_eqI)
    fix m
    from \<open>?P\<close> have \<open>a = take_bit n a\<close> ..
    also have \<open>\<not> bit (take_bit n a) (n + m)\<close>
      unfolding bit_simps
      by (simp add: bit_simps)
    finally show \<open>bit (drop_bit n a) m \<longleftrightarrow> bit 0 m\<close>
      by (simp add: bit_simps)
  qed
next
  assume ?Q
  show ?P
  proof (rule bit_eqI)
    fix m
    from \<open>?Q\<close> have \<open>\<not> bit (drop_bit n a) (m - n)\<close>
      by simp
    then have \<open> \<not> bit a (n + (m - n))\<close>
      by (simp add: bit_simps)
    then show \<open>bit (take_bit n a) m \<longleftrightarrow> bit a m\<close>
      by (cases \<open>m < n\<close>) (auto simp: bit_simps)
  qed
qed

lemma impossible_bit_imp_take_bit_eq_self:
  \<open>take_bit n a = a\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
proof -
  have \<open>drop_bit n a = 0\<close>
  proof (rule bit_eqI)
    fix m
    show \<open>bit (drop_bit n a) m \<longleftrightarrow> bit 0 m\<close>
      using possible_bit_less_imp [of \<open>n + m\<close> n] that
      by (auto simp add: bit_simps dest: bit_imp_possible_bit)
  qed
  then show ?thesis
    by (simp add: take_bit_eq_self_iff_drop_bit_eq_0)
qed

lemma drop_bit_exp_eq:
  \<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> possible_bit TYPE('a) n) * 2 ^ (n - m)\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma take_bit_and [simp]:
  \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma take_bit_or [simp]:
  \<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma take_bit_xor [simp]:
  \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma push_bit_and [simp]:
  \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma push_bit_or [simp]:
  \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma push_bit_xor [simp]:
  \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma drop_bit_and [simp]:
  \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma drop_bit_or [simp]:
  \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma drop_bit_xor [simp]:
  \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma take_bit_of_mask [simp]:
  \<open>take_bit m (mask n) = mask (min m n)\<close>
  by (rule bit_eqI) (simp add: bit_simps)

lemma take_bit_eq_mask:
  \<open>take_bit n a = a AND mask n\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma or_eq_0_iff:
  \<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
  by (auto simp: bit_eq_iff bit_or_iff)

lemma bit_iff_and_drop_bit_eq_1:
  \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
  by (simp add: bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one)

lemma bit_iff_and_push_bit_not_eq_0:
  \<open>bit a n \<longleftrightarrow> a AND push_bit n 1 \<noteq> 0\<close>
  by (cases \<open>possible_bit TYPE('a) n\<close>) (simp_all add: bit_eq_iff bit_simps impossible_bit)

lemma bit_set_bit_iff [bit_simps]:
  \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> possible_bit TYPE('a) n)\<close>
  by (auto simp: set_bit_eq_or bit_or_iff bit_exp_iff)

lemma even_set_bit_iff:
  \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
  using bit_set_bit_iff [of m a 0] by (auto simp: bit_0)

lemma bit_unset_bit_iff [bit_simps]:
  \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
  by (auto simp: unset_bit_eq_or_xor bit_simps dest: bit_imp_possible_bit)

lemma even_unset_bit_iff:
  \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
  using bit_unset_bit_iff [of m a 0] by (auto simp: bit_0)

lemma bit_flip_bit_iff [bit_simps]:
  \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> possible_bit TYPE('a) n\<close>
  by (auto simp: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit)

lemma even_flip_bit_iff:
  \<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close>
  using bit_flip_bit_iff [of m a 0] by (auto simp: possible_bit_def  bit_0)

lemma and_exp_eq_0_iff_not_bit:
  \<open>a AND 2 ^ n = 0 \<longleftrightarrow> \<not> bit a n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
  using bit_imp_possible_bit[of a n]
  by (auto simp: bit_eq_iff bit_simps)

lemma bit_sum_mult_2_cases:
  assumes a: \<open>\<forall>j. \<not> bit a (Suc j)\<close>
  shows \<open>bit (a + 2 * b) n = (if n = 0 then odd a else bit (2 * b) n)\<close>
proof -
  from a have \<open>n = 0\<close> if \<open>bit a n\<close> for n using that
    by (cases n) simp_all
  then have \<open>a = 0 \<or> a = 1\<close>
    by (auto simp: bit_eq_iff bit_1_iff)
  then show ?thesis
    by (cases n) (auto simp: bit_0 bit_double_iff even_bit_succ_iff)
qed

lemma set_bit_0:
  \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
  by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)

lemma set_bit_Suc:
  \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
  by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
    elim: possible_bit_less_imp)

lemma unset_bit_0:
  \<open>unset_bit 0 a = 2 * (a div 2)\<close>
  by (auto simp: bit_eq_iff bit_simps simp flip: bit_Suc)

lemma unset_bit_Suc:
  \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
  by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)

lemma flip_bit_0:
  \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
  by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)

lemma flip_bit_Suc:
  \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
  by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
    elim: possible_bit_less_imp)

lemma flip_bit_eq_if:
  \<open>flip_bit n a = (if bit a n then unset_bit else set_bit) n a\<close>
  by (rule bit_eqI) (auto simp: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff)

lemma take_bit_set_bit_eq:
  \<open>take_bit n (set_bit m a) = (if n \<le> m then take_bit n a else set_bit m (take_bit n a))\<close>
  by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_set_bit_iff)

lemma take_bit_unset_bit_eq:
  \<open>take_bit n (unset_bit m a) = (if n \<le> m then take_bit n a else unset_bit m (take_bit n a))\<close>
  by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_unset_bit_iff)

lemma take_bit_flip_bit_eq:
  \<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
  by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_flip_bit_iff)

lemma push_bit_Suc_numeral [simp]:
  \<open>push_bit (Suc n) (numeral k) = push_bit n (numeral (Num.Bit0 k))\<close>
  by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)

lemma mask_eq_0_iff [simp]:
  \<open>mask n = 0 \<longleftrightarrow> n = 0\<close>
  by (cases n) (simp_all add: mask_Suc_double or_eq_0_iff)

lemma bit_horner_sum_bit_iff [bit_simps]:
  \<open>bit (horner_sum of_bool 2 bs) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < length bs \<and> bs ! n\<close>
proof (induction bs arbitrary: n)
  case Nil
  then show ?case
    by simp
next
  case (Cons b bs)
  show ?case
  proof (cases n)
    case 0
    then show ?thesis
      by (simp add: bit_0)
  next
    case (Suc m)
    with bit_rec [of _ n] Cons.prems Cons.IH [of m]
    show ?thesis
      by (simp add: bit_simps)
        (auto simp: possible_bit_less_imp bit_simps simp flip: bit_Suc)
  qed
qed

lemma horner_sum_bit_eq_take_bit:
  \<open>horner_sum of_bool 2 (map (bit a) [0..<n]) = take_bit n a\<close>
  by (rule bit_eqI) (auto simp: bit_simps)

lemma take_bit_horner_sum_bit_eq:
  \<open>take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\<close>
  by (auto simp: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff)

lemma take_bit_sum:
  \<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
  by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult)

lemma set_bit_eq:
  \<open>set_bit n a = a + of_bool (\<not> bit a n) * 2 ^ n\<close>
proof -
  have \<open>a AND of_bool (\<not> bit a n) * 2 ^ n = 0\<close>
    by (auto simp: bit_eq_iff bit_simps)
  then show ?thesis
    by (auto simp: bit_eq_iff bit_simps disjunctive_add_eq_or)
qed

end

class ring_bit_operations = semiring_bit_operations + ring_parity +
  fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
  assumes not_eq_complement: \<open>NOT a = - a - 1\<close>
begin

text \<open>
  For the sake of code generation \<^const>\<open>not\<close> is specified as
  definitional class operation.  Note that \<^const>\<open>not\<close> has no
  sensible definition for unlimited but only positive bit strings
  (type \<^typ>\<open>nat\<close>).
\<close>

lemma bits_minus_1_mod_2_eq [simp]:
  \<open>(- 1) mod 2 = 1\<close>
  by (simp add: mod_2_eq_odd)

lemma minus_eq_not_plus_1:
  \<open>- a = NOT a + 1\<close>
  using not_eq_complement [of a] by simp

lemma minus_eq_not_minus_1:
  \<open>- a = NOT (a - 1)\<close>
  using not_eq_complement [of \<open>a - 1\<close>] by simp (simp add: algebra_simps)

lemma not_rec:
  \<open>NOT a = of_bool (even a) + 2 * NOT (a div 2)\<close>
  by (simp add: not_eq_complement algebra_simps mod_2_eq_odd flip: minus_mod_eq_mult_div)

lemma decr_eq_not_minus:
  \<open>a - 1 = NOT (- a)\<close>
  using not_eq_complement [of \<open>- a\<close>] by simp

lemma even_not_iff [simp]:
  \<open>even (NOT a) \<longleftrightarrow> odd a\<close>
  by (simp add: not_eq_complement)

lemma bit_not_iff [bit_simps]:
  \<open>bit (NOT a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit a n\<close>
proof (cases \<open>possible_bit TYPE('a) n\<close>)
  case False
  then show ?thesis
    by (auto dest: bit_imp_possible_bit)
next
  case True
  moreover have \<open>bit (NOT a) n \<longleftrightarrow> \<not> bit a n\<close>
  using \<open>possible_bit TYPE('a) n\<close> proof (induction n arbitrary: a)
    case 0
    then show ?case
      by (simp add: bit_0)
  next
    case (Suc n)
    from Suc.prems Suc.IH [of \<open>a div 2\<close>]
    show ?case
      by (simp add: impossible_bit possible_bit_less_imp not_rec [of a] even_bit_succ_iff bit_double_iff flip: bit_Suc)
  qed
  ultimately show ?thesis
    by simp
qed

lemma bit_not_exp_iff [bit_simps]:
  \<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<noteq> m\<close>
  by (auto simp: bit_not_iff bit_exp_iff)

lemma bit_minus_iff [bit_simps]:
  \<open>bit (- a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit (a - 1) n\<close>
  by (simp add: minus_eq_not_minus_1 bit_not_iff)

lemma bit_minus_1_iff [simp]:
  \<open>bit (- 1) n \<longleftrightarrow> possible_bit TYPE('a) n\<close>
  by (simp add: bit_minus_iff)

lemma bit_minus_exp_iff [bit_simps]:
  \<open>bit (- (2 ^ m)) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<ge> m\<close>
  by (auto simp: bit_simps simp flip: mask_eq_exp_minus_1)

lemma bit_minus_2_iff [simp]:
  \<open>bit (- 2) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n > 0\<close>
  by (simp add: bit_minus_iff bit_1_iff)

lemma bit_decr_iff:
  \<open>bit (a - 1) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit (- a) n\<close>
  by (simp add: decr_eq_not_minus bit_not_iff)

lemma bit_not_iff_eq:
  \<open>bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
  by (simp add: bit_simps possible_bit_def)

lemma not_one_eq [simp]:
  \<open>NOT 1 = - 2\<close>
  by (rule bit_eqI, simp add: bit_simps)

sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
  by standard (rule bit_eqI, simp add: bit_and_iff)

sublocale bit: abstract_boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
  by standard (auto simp: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)

sublocale bit: abstract_boolean_algebra_sym_diff \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close> \<open>(XOR)\<close>
proof
  show \<open>\<And>x y. x XOR y = x AND NOT y OR NOT x AND y\<close>
    by (intro bit_eqI) (auto simp: bit_simps)
qed

lemma and_eq_not_not_or:
  \<open>a AND b = NOT (NOT a OR NOT b)\<close>
  by simp

lemma or_eq_not_not_and:
  \<open>a OR b = NOT (NOT a AND NOT b)\<close>
  by simp

lemma not_add_distrib:
  \<open>NOT (a + b) = NOT a - b\<close>
  by (simp add: not_eq_complement algebra_simps)

lemma not_diff_distrib:
  \<open>NOT (a - b) = NOT a + b\<close>
  using not_add_distrib [of a \<open>- b\<close>] by simp

lemma and_eq_minus_1_iff:
  \<open>a AND b = - 1 \<longleftrightarrow> a = - 1 \<and> b = - 1\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma disjunctive_and_not_eq_xor:
  \<open>a AND NOT b = a XOR b\<close> if \<open>NOT a AND b = 0\<close>
  using that by (auto simp: bit_eq_iff bit_simps)

lemma disjunctive_diff_eq_and_not:
  \<open>a - b = a AND NOT b\<close> if \<open>NOT a AND b = 0\<close>
proof -
  from that have \<open>NOT a + b = NOT a OR b\<close>
    by (rule disjunctive_add_eq_or)
  then have \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
    by simp
  then show ?thesis
    by (simp add: not_add_distrib)
qed

lemma disjunctive_diff_eq_xor:
  \<open>a AND NOT b = a XOR b\<close> if \<open>NOT a AND b = 0\<close>
  using that by (simp add: disjunctive_and_not_eq_xor disjunctive_diff_eq_and_not)

lemma push_bit_minus:
  \<open>push_bit n (- a) = - push_bit n a\<close>
  by (simp add: push_bit_eq_mult)

lemma take_bit_not_take_bit:
  \<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
  by (auto simp: bit_eq_iff bit_take_bit_iff bit_not_iff)

lemma take_bit_not_iff:
  \<open>take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b\<close>
  by (auto simp: bit_eq_iff bit_simps)

lemma take_bit_not_eq_mask_diff:
  \<open>take_bit n (NOT a) = mask n - take_bit n a\<close>
proof -
  have \<open>NOT (mask n) AND take_bit n a = 0\<close>
    by (simp add: bit_eq_iff bit_simps)
  moreover have \<open>take_bit n (NOT a) = mask n AND NOT (take_bit n a)\<close>
    by (auto simp: bit_eq_iff bit_simps)
  ultimately show ?thesis
    by (simp add: disjunctive_diff_eq_and_not)
qed

lemma mask_eq_take_bit_minus_one:
  \<open>mask n = take_bit n (- 1)\<close>
  by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute)

lemma take_bit_minus_one_eq_mask [simp]:
  \<open>take_bit n (- 1) = mask n\<close>
  by (simp add: mask_eq_take_bit_minus_one)

lemma minus_exp_eq_not_mask:
  \<open>- (2 ^ n) = NOT (mask n)\<close>
  by (rule bit_eqI) (simp add: bit_minus_iff bit_not_iff flip: mask_eq_exp_minus_1)

lemma push_bit_minus_one_eq_not_mask [simp]:
  \<open>push_bit n (- 1) = NOT (mask n)\<close>
  by (simp add: push_bit_eq_mult minus_exp_eq_not_mask)

lemma take_bit_not_mask_eq_0:
  \<open>take_bit m (NOT (mask n)) = 0\<close> if \<open>n \<ge> m\<close>
  by (rule bit_eqI) (use that in \<open>simp add: bit_take_bit_iff bit_not_iff bit_mask_iff\<close>)

lemma mask_eq_minus_one_if_not_possible_bit:
  \<open>mask n = - 1\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
  using that mask_eq_take_bit_minus_one [of n] impossible_bit_imp_take_bit_eq_self [of n \<open>- 1\<close>]
  by simp

lemma unset_bit_eq_and_not:
  \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
  by (rule bit_eqI) (auto simp: bit_simps)

lemma push_bit_Suc_minus_numeral [simp]:
  \<open>push_bit (Suc n) (- numeral k) = push_bit n (- numeral (Num.Bit0 k))\<close>
  using local.push_bit_Suc_numeral push_bit_minus by presburger

lemma push_bit_minus_numeral [simp]:
  \<open>push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))\<close>
  by (simp only: numeral_eq_Suc push_bit_Suc_minus_numeral)

lemma take_bit_Suc_minus_1_eq:
  \<open>take_bit (Suc n) (- 1) = 2 ^ Suc n - 1\<close>
  by (simp add: mask_eq_exp_minus_1)

lemma take_bit_numeral_minus_1_eq:
  \<open>take_bit (numeral k) (- 1) = 2 ^ numeral k - 1\<close>
  by (simp add: mask_eq_exp_minus_1)

lemma push_bit_mask_eq:
  \<open>push_bit m (mask n) = mask (n + m) AND NOT (mask m)\<close>
  by (rule bit_eqI) (auto simp: bit_simps not_less possible_bit_less_imp)

lemma slice_eq_mask:
  \<open>push_bit n (take_bit m (drop_bit n a)) = a AND mask (m + n) AND NOT (mask n)\<close>
  by (rule bit_eqI) (auto simp: bit_simps)

lemma push_bit_numeral_minus_1 [simp]:
  \<open>push_bit (numeral n) (- 1) = - (2 ^ numeral n)\<close>
  by (simp add: push_bit_eq_mult)

lemma unset_bit_eq:
  \<open>unset_bit n a = a - of_bool (bit a n) * 2 ^ n\<close>
proof -
  have \<open>NOT a AND of_bool (bit a n) * 2 ^ n = 0\<close>
    by (auto simp: bit_eq_iff bit_simps)
  moreover have \<open>unset_bit n a = a AND NOT (of_bool (bit a n) * 2 ^ n)\<close>
    by (auto simp: bit_eq_iff bit_simps)
  ultimately show ?thesis
    by (simp add: disjunctive_diff_eq_and_not)
qed

end

subsection \<open>Common algebraic structure\<close>

class linordered_euclidean_semiring_bit_operations =
  linordered_euclidean_semiring + semiring_bit_operations
begin

lemma possible_bit [simp]:
  \<open>possible_bit TYPE('a) n\<close>
  by (simp add: possible_bit_def)

lemma take_bit_of_exp [simp]:
  \<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close>
  by (simp add: take_bit_eq_mod exp_mod_exp)

lemma take_bit_of_2 [simp]:
  \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
  using take_bit_of_exp [of n 1] by simp

lemma push_bit_eq_0_iff [simp]:
  \<open>push_bit n a = 0 \<longleftrightarrow> a = 0\<close>
  by (simp add: push_bit_eq_mult)

lemma take_bit_add:
  \<open>take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)\<close>
  by (simp add: take_bit_eq_mod mod_simps)

lemma take_bit_of_1_eq_0_iff [simp]:
  \<open>take_bit n 1 = 0 \<longleftrightarrow> n = 0\<close>
  by (simp add: take_bit_eq_mod)

lemma drop_bit_Suc_bit0 [simp]:
  \<open>drop_bit (Suc n) (numeral (Num.Bit0 k)) = drop_bit n (numeral k)\<close>
  by (simp add: drop_bit_Suc numeral_Bit0_div_2)

lemma drop_bit_Suc_bit1 [simp]:
  \<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
  by (simp add: drop_bit_Suc numeral_Bit0_div_2)

lemma drop_bit_numeral_bit0 [simp]:
  \<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
  by (simp add: drop_bit_rec numeral_Bit0_div_2)

lemma drop_bit_numeral_bit1 [simp]:
  \<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
  by (simp add: drop_bit_rec numeral_Bit0_div_2)

lemma take_bit_Suc_1 [simp]:
  \<open>take_bit (Suc n) 1 = 1\<close>
  by (simp add: take_bit_Suc)

lemma take_bit_Suc_bit0:
  \<open>take_bit (Suc n) (numeral (Num.Bit0 k)) = take_bit n (numeral k) * 2\<close>
  by (simp add: take_bit_Suc numeral_Bit0_div_2)

lemma take_bit_Suc_bit1:
  \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
  by (simp add: take_bit_Suc numeral_Bit0_div_2 mod_2_eq_odd)

lemma take_bit_numeral_1 [simp]:
  \<open>take_bit (numeral l) 1 = 1\<close>
  by (simp add: take_bit_rec [of \<open>numeral l\<close> 1])

lemma take_bit_numeral_bit0:
  \<open>take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2\<close>
  by (simp add: take_bit_rec numeral_Bit0_div_2)

lemma take_bit_numeral_bit1:
  \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
  by (simp add: take_bit_rec numeral_Bit0_div_2 mod_2_eq_odd)

lemma bit_of_nat_iff_bit [bit_simps]:
  \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
proof -
  have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
    by simp
  also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close>
    by (simp add: of_nat_div)
  finally show ?thesis
    by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
qed

lemma drop_bit_mask_eq:
  \<open>drop_bit m (mask n) = mask (n - m)\<close>
  by (rule bit_eqI) (auto simp: bit_simps possible_bit_def)

lemma bit_push_bit_iff':
  \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> bit a (n - m)\<close>
  by (simp add: bit_simps)

lemma mask_half:
  \<open>mask n div 2 = mask (n - 1)\<close>
  by (cases n) (simp_all add: mask_Suc_double one_or_eq)

lemma take_bit_Suc_from_most:
  \<open>take_bit (Suc n) a = 2 ^ n * of_bool (bit a n) + take_bit n a\<close>
  using mod_mult2_eq' [of a \2 ^ n\ 2]
  by (simp only: take_bit_eq_mod power_Suc2)
    (simp_all add: bit_iff_odd odd_iff_mod_2_eq_one)

lemma take_bit_nonnegative [simp]:
  \<open>0 \<le> take_bit n a\<close>
  using horner_sum_nonnegative by (simp flip: horner_sum_bit_eq_take_bit)

lemma not_take_bit_negative [simp]:
  \<open>\<not> take_bit n a < 0\<close>
  by (simp add: not_less)

lemma bit_imp_take_bit_positive:
  \<open>0 < take_bit m a\<close> if \<open>n < m\<close> and \<open>bit a n\<close>
proof (rule ccontr)
  assume \<open>\<not> 0 < take_bit m a\<close>
  then have \<open>take_bit m a = 0\<close>
    by (auto simp: not_less intro: order_antisym)
  then have \<open>bit (take_bit m a) n = bit 0 n\<close>
    by simp
  with that show False
    by (simp add: bit_take_bit_iff)
qed

lemma take_bit_mult:
  \<open>take_bit n (take_bit n a * take_bit n b) = take_bit n (a * b)\<close>
  by (simp add: take_bit_eq_mod mod_mult_eq)

lemma drop_bit_push_bit:
  \<open>drop_bit m (push_bit n a) = drop_bit (m - n) (push_bit (n - m) a)\<close>
  by (cases \<open>m \<le> n\<close>)
    (auto simp: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc
    mult.commute [of a] drop_bit_eq_div push_bit_eq_mult not_le power_add Orderings.not_le dest!: le_Suc_ex less_imp_Suc_add)

end

subsection \<open>Instance \<^typ>\<open>int\<close>\<close>

locale fold2_bit_int =
  fixes f :: \<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>
begin

context
begin

function F :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
  where \<open>F k l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
    then - of_bool (f (odd k) (odd l))
    else of_bool (f (odd k) (odd l)) + 2 * (F (k div 2) (l div 2)))\<close>
  by auto

private termination proof (relation \<open>measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))\<close>)
  have less_eq: \<open>\<bar>k div 2\<bar> \<le> \<bar>k\<bar>\<close> for k :: int
    by (cases k) (simp_all add: divide_int_def nat_add_distrib)
  then have less: \<open>\<bar>k div 2\<bar> < \<bar>k\<bar>\<close> if \<open>k \<notin> {0, - 1}\<close> for k :: int
    using that by (auto simp: less_le [of k])
  show \<open>wf (measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>)))\<close>
    by simp
  show \<open>((k div 2, l div 2), k, l) \<in> measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))\<close>
    if \<open>\<not> (k \<in> {0, - 1} \<and> l \<in> {0, - 1})\<close> for k l
  proof -
    from that have *: \<open>k \<notin> {0, - 1} \<or> l \<notin> {0, - 1}\<close>
      by simp
    then have \<open>0 < \<bar>k\<bar> + \<bar>l\<bar>\<close>
      by auto
    moreover from * have \<open>\<bar>k div 2\<bar> + \<bar>l div 2\<bar> < \<bar>k\<bar> + \<bar>l\<bar>\<close>
    proof
      assume \<open>k \<notin> {0, - 1}\<close>
      then have \<open>\<bar>k div 2\<bar> < \<bar>k\<bar>\<close>
        by (rule less)
      with less_eq [of l] show ?thesis
        by auto
    next
      assume \<open>l \<notin> {0, - 1}\<close>
      then have \<open>\<bar>l div 2\<bar> < \<bar>l\<bar>\<close>
        by (rule less)
      with less_eq [of k] show ?thesis
        by auto
    qed
    ultimately show ?thesis
      by (simp only: in_measure split_def fst_conv snd_conv nat_mono_iff)
  qed
qed

declare F.simps [simp del]

lemma rec:
  \<open>F k l = of_bool (f (odd k) (odd l)) + 2 * (F (k div 2) (l div 2))\<close>
    for k l :: int
proof (cases \<open>k \<in> {0, - 1} \<and> l \<in> {0, - 1}\<close>)
  case True
  then show ?thesis
    by (auto simp: F.simps [of 0] F.simps [of \<open>- 1\<close>])
next
  case False
  then show ?thesis
    by (auto simp: ac_simps F.simps [of k l])
qed

lemma bit_iff:
  \<open>bit (F k l) n \<longleftrightarrow> f (bit k n) (bit l n)\<close> for k l :: int
proof (induction n arbitrary: k l)
  case 0
  then show ?case
    by (simp add: rec [of k l] bit_0)
next
  case (Suc n)
  then show ?case
    by (simp add: rec [of k l] bit_Suc)
qed

end

end

instantiation int :: ring_bit_operations
begin

definition not_int :: \<open>int \<Rightarrow> int\<close>
  where \<open>not_int k = - k - 1\<close>

global_interpretation and_int: fold2_bit_int \<open>(\<and>)\<close>
  defines and_int = and_int.F .

global_interpretation or_int: fold2_bit_int \<open>(\<or>)\<close>
  defines or_int = or_int.F .

global_interpretation xor_int: fold2_bit_int \<open>(\<noteq>)\<close>
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.