Theory 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