Theory WB_More_Word

theory WB_More_Word
  imports "Word_Lib.Many_More" Isabelle_LLVM.Bits_Natural
begin

lemma nat_uint_XOR: ‹nat (uint (a XOR b)) = nat (uint a) XOR nat (uint b)›
  if len: ‹LENGTH('a) > 0›
  for a b :: ‹'a ::len Word.word›
proof -
  have 1: ‹uint ((word_of_int:: int ⇒ 'a Word.word)(uint a)) = uint a›
    by (subst (2) word_of_int_uint[of a, symmetric]) (rule refl)
  have H: ‹nat (bintrunc n (a XOR b)) = nat (bintrunc n a XOR bintrunc n b)›
    if ‹n> 0› for n and a :: int and b :: int
    using that
  proof (induction n arbitrary: a b)
    case 0
    then show ?case by auto
  next
    case (Suc n) note IH = this(1) and Suc = this(2)
    then show ?case
      by (cases n) simp_all
  qed
  have ‹nat (bintrunc LENGTH('a) (a XOR b)) = nat (bintrunc LENGTH('a) a XOR bintrunc LENGTH('a) b)› for a b
    using len H[of ‹LENGTH('a)› a b] by auto
  then have ‹nat (uint (a XOR b)) = nat (uint a XOR uint b)›
    by transfer
  then show ?thesis
    unfolding xor_nat_def by auto
qed

lemma bitXOR_1_if_mod_2_int: ‹L OR 1 = (if L mod 2 = 0 then L + 1 else L)› for L :: int
  apply (rule bin_rl_eqI)
  unfolding bin_rest_OR bin_last_OR
  by (auto simp: )

lemma bitOR_1_if_mod_2_nat:
  ‹L OR 1 = (if L mod 2 = 0 then L + 1 else L)›
  ‹L OR (Suc 0) = (if L mod 2 = 0 then L + 1 else L)› for L :: nat
proof -
  have H: ‹L OR 1 =  L + (if bin_last (int L) then 0 else 1)›
    unfolding or_nat_def
    apply (auto simp: or_nat_def bin_last_def xor_one_eq
      bitXOR_1_if_mod_2_int)
      apply presburger
    done
  show ‹L OR 1 = (if L mod 2 = 0 then L + 1 else L)›
    unfolding H
    apply (auto simp: or_nat_def bin_last_def)
    apply presburger+
    done
  then show ‹L OR (Suc 0) = (if L mod 2 = 0 then L + 1 else L)›
    by simp
qed

lemma bin_pos_same_XOR3:
  ‹a XOR a XOR c = c›
  ‹a XOR c XOR a = c› for a c :: int
  by (metis bin_ops_same(3) int_xor_assoc int_xor_zero)+

lemma bin_pos_same_XOR3_nat:
  ‹a XOR a XOR c = c›
  ‹a XOR c XOR a = c› for a c :: nat
 unfolding xor_nat_def by (auto simp: bin_pos_same_XOR3)

end