Theory WB_More_Word

theory WB_More_Word
  imports "HOL-Word.More_Word" "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 ::len0 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
    proof (cases n)
      case (Suc m)
      moreover have
        ‹nat (bintrunc m (bin_rest (bin_rest a) XOR bin_rest (bin_rest b)) BIT
            ((bin_last (bin_rest a) ∨ bin_last (bin_rest b)) ∧
             (bin_last (bin_rest a) ⟶ ¬ bin_last (bin_rest b))) BIT
            ((bin_last a ∨ bin_last b) ∧ (bin_last a ⟶ ¬ bin_last b))) =
         nat ((bintrunc m (bin_rest (bin_rest a)) XOR bintrunc m (bin_rest (bin_rest b))) BIT
              ((bin_last (bin_rest a) ∨ bin_last (bin_rest b)) ∧
               (bin_last (bin_rest a) ⟶ ¬ bin_last (bin_rest b))) BIT
              ((bin_last a ∨ bin_last b) ∧ (bin_last a ⟶ ¬ bin_last b)))›
        (is ‹nat (?n1 BIT ?b) = nat (?n2 BIT ?b)›)
      proof - (* Sledgehammer proof changed to use the more readable ?n1 and ?n2 *)
        have a1:  "nat ?n1 = nat ?n2"
          using IH Suc by auto
        have f2: "0 ≤ ?n2"
          by (simp add: bintr_ge0)
        have "0 ≤ ?n1"
          using bintr_ge0 by auto
        then have "?n2 = ?n1"
          using f2 a1 by presburger
        then show ?thesis by simp
      qed
      ultimately show ?thesis by simp
    qed simp
  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 bitXOR_nat_def by auto
qed
lemma bitXOR_1_if_mod_2_int: ‹bitOR L 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
   apply (auto simp: bin_rest_def bin_last_def)
  done


lemma bitOR_1_if_mod_2_nat:
  ‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)›
  ‹bitOR L (Suc 0) = (if L mod 2 = 0 then L + 1 else L)› for L :: nat
proof -
  have H: ‹bitOR L 1 =  L + (if bin_last (int L) then 0 else 1)›
    unfolding bitOR_nat_def
    apply (auto simp: bitOR_nat_def bin_last_def
        bitXOR_1_if_mod_2_int)
    done
  show ‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)›
    unfolding H
    apply (auto simp: bitOR_nat_def bin_last_def)
    apply presburger+
    done
  then show ‹bitOR L (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 bitXOR_nat_def by (auto simp: bin_pos_same_XOR3)

end