Theory Word_Lib.Legacy_Aliases

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section ‹Legacy aliases›

theory Legacy_Aliases
  imports "HOL-Library.Word"
begin

context abstract_boolean_algebra
begin

lemma conj_assoc: "(x  y)  z = x  (y  z)"
  by (fact conj.assoc)

lemma conj_commute: "x  y = y  x"
  by (fact conj.commute)

lemmas conj_left_commute = conj.left_commute
lemmas conj_ac = conj.assoc conj.commute conj.left_commute

lemma conj_one_left: "1  x = x"
  by (fact conj.left_neutral)

lemma conj_left_absorb: "x  (x  y) = x  y"
  by (fact conj.left_idem)

lemma conj_absorb: "x  x = x"
  by (fact conj.idem)

lemma disj_assoc: "(x  y)  z = x  (y  z)"
  by (fact disj.assoc)

lemma disj_commute: "x  y = y  x"
  by (fact disj.commute)

lemmas disj_left_commute = disj.left_commute

lemmas disj_ac = disj.assoc disj.commute disj.left_commute

lemma disj_zero_left: "0  x = x"
  by (fact disj.left_neutral)

lemma disj_left_absorb: "x  (x  y) = x  y"
  by (fact disj.left_idem)

lemma disj_absorb: "x  x = x"
  by (fact disj.idem)

end

context abstract_boolean_algebra_sym_diff
begin

lemmas xor_assoc = xor.assoc
lemmas xor_commute = xor.commute
lemmas xor_left_commute = xor.left_commute

lemmas xor_ac = xor.assoc xor.commute xor.left_commute

lemma xor_zero_right: "x  0 = x"
  by (fact xor.comm_neutral)

lemma xor_zero_left: "0  x = x"
  by (fact xor.left_neutral)

end

abbreviation (input) test_bit :: 'a::semiring_bits  nat  bool
  where test_bit  bit

abbreviation (input) bin_nth :: int  nat  bool
  where bin_nth  bit

abbreviation (input) bin_last :: int  bool
  where bin_last  odd

abbreviation (input) bin_rest :: int  int
  where bin_rest w  w div 2

abbreviation (input) bintrunc :: nat  int  int
  where bintrunc  take_bit

abbreviation (input) sbintrunc :: nat  int  int
  where sbintrunc  signed_take_bit

abbreviation (input) bin_cat :: int  nat  int  int
  where bin_cat k n l  concat_bit n l k

abbreviation (input) norm_sint :: nat  int  int
  where norm_sint n  signed_take_bit (n - 1)

abbreviation (input) max_word :: 'a::len word
  where max_word  - 1

abbreviation (input) complement :: 'a::len word  'a word
  where complement  not

lemma complement_mask:
  "complement (2 ^ n - 1) = not (mask n)"
  unfolding mask_eq_decr_exp by simp

context
  includes bit_operations_syntax
begin

abbreviation (input) bshiftr1 :: bool  'a::len word  'a word
  where bshiftr1 b w  w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b)

end

lemma bit_bshiftr1_iff:
  bit (bshiftr1 b w) n  b  n = LENGTH('a) - 1  bit w (Suc n)
    for w :: 'a::len word
  by (auto simp add: bit_simps simp flip: bit_Suc)

abbreviation (input) setBit :: 'a::len word  nat  'a word
  where setBit w n  set_bit n w

abbreviation (input) clearBit :: 'a::len word  nat  'a word
  where clearBit w n  unset_bit n w

lemma bit_setBit_iff:
  bit (setBit w m) n  (m = n  n < LENGTH('a)  bit w n)
  for w :: 'a::len word
  by (auto simp add: bit_simps)

lemma bit_clearBit_iff:
  bit (clearBit w m) n  m  n  bit w n
  for w :: 'a::len word
  by (auto simp add: bit_simps)

lemmas less_def = less_eq [symmetric]
lemmas le_def = not_less [symmetric, where ?'a = nat]

end