Theory Word_Lib.Sgn_Abs

(*
 * Copyright 2023, Proofcraft Pty Ltd
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Sgn_Abs
  imports Most_significant_bit
begin

lemma not_0_sless_minus_1 [simp]:
  ‹¬ 0 <s - 1›
  by transfer simp

lemma not_0_sless_eq_minus_1 [simp]:
  ‹¬ 0 ≤s - 1›
  by transfer simp

section ‹@{const sgn} and @{const abs} for @{typ "'a word"}›

subsection ‹Instances›

text ‹@{const sgn} on words returns -1, 0, or 1.›

instantiation word :: (len) sgn
begin

lift_definition sgn_word :: ‹'a word ⇒ 'a word›
  is ‹λk. sgn (signed_take_bit (LENGTH('a) - Suc 0) k)›
  by (simp flip: signed_take_bit_decr_length_iff)

instance ..

end

lemma sgn_word_if:
  ‹sgn w = (if w = 0 then 0 else if 0 <s w then 1 else - 1)›
  by transfer (simp only: flip: signed_take_bit_decr_length_iff, auto simp add: sgn_if)

text ‹Simplificattion setup for sgn on numerals›

lemma word_sgn_0[simp]:
  "sgn 0 = (0::'a::len word)"
  by transfer simp

lemma word_sgn_1[simp]:
  "sgn 1 = (1::'a::len word)"
  by (transfer; cases ‹LENGTH('a) - Suc 0›) simp_all

lemma word_sgn_max_word[simp]:
  "sgn (- 1) = (-1::'a::len word)"
  by transfer simp

lemma word_sgn_numeral [simp]:
  ‹sgn (numeral n) = (if numeral n = (0 :: 'a::len word) then 0
    else if (0 :: 'a::len word) <s numeral n then 1 else (- 1 :: 'a::len word))›
  by (fact sgn_word_if)

text ‹@{const abs} on words is the usual definition.›

instantiation word :: (len) abs
begin

lift_definition abs_word :: ‹'a word ⇒ 'a word›
  is ‹λk. ¦signed_take_bit (LENGTH('a) - Suc 0) k¦›
  by (simp flip: signed_take_bit_decr_length_iff)

instance ..

end

lemma abs_word_if:
  ‹abs w = (if w ≤s 0 then - w else w)›
  by transfer (simp only: flip: signed_take_bit_decr_length_iff,
    auto simp add: abs_of_pos signed_take_bit_minus)


text ‹Simplification setup for abs on numerals›

lemma word_abs_0[simp]:
  "¦0¦ = (0::'a::len word)"
  by transfer simp

lemma word_abs_1[simp]:
  "¦1¦ = (1::'a::len word)"
  by (transfer; cases ‹LENGTH('a) - Suc 0›) simp_all

lemma word_abs_max_word[simp]:
  "¦- 1¦ = (1::'a::len word)"
  by transfer simp

lemma word_abs_msb:
  "¦w¦ = (if msb w then - w else w)" for w :: "'a::len word"
  by transfer
    (simp add: abs_of_neg msb_int_def signed_take_bit_eq_take_bit_minus take_bit_minus flip: take_bit_diff [of _ ‹2 ^ LENGTH('a)›])

lemmas word_abs_numeral[simp] = word_abs_msb[where w="numeral w" for w]


subsection ‹Properties›

(* Many of these are from linordered_idom, but need <s instead of < and occasionally
   an additional assumption on minimum word length, because in "1 word" we have -1 = 1. *)

lemma word_sgn_0_0:
  "sgn a = 0 ⟷ a = 0" for a::"'a::len word"
  by (simp add: sgn_word_if)

lemma word_sgn_1_pos:
  "1 < LENGTH('a) ⟹ sgn a = 1 ⟷ 0 <s a" for a::"'a::len word"
  by (simp add: sgn_word_if)

lemma word_sgn_1_neg:
  "sgn a = - 1 ⟷ a <s 0"
  by (cases a rule: word_length_one) (auto simp add: sgn_word_if)

lemma word_sgn_pos[simp]:
  "0 <s a ⟹ sgn a = 1"
  by transfer simp

lemma word_sgn_neg[simp]:
  "a <s 0 ⟹ sgn a = - 1"
  by (simp only: word_sgn_1_neg)

lemma word_abs_sgn:
  "¦k¦ = k * sgn k" for k :: "'a::len word"
  by (auto simp add: sgn_word_if abs_word_if)

lemma word_sgn_greater[simp]:
  "0 <s sgn a ⟷ 0 <s a" for a::"'a::len word"
  by (cases a rule: word_length_one) (simp_all add: sgn_word_if)

lemma word_sgn_less[simp]:
  "sgn a <s 0 ⟷ a <s 0" for a::"'a::len word"
  by (cases a rule: word_length_one) (auto simp add: sgn_word_if)

lemma word_abs_sgn_eq_1[simp]:
  "a ≠ 0 ⟹ ¦sgn a¦ = 1" for a::"'a::len word"
  by (simp add: sgn_word_if)

lemma word_abs_sgn_eq:
  "¦sgn a¦ = (if a = 0 then 0 else 1)" for a::"'a::len word"
  by simp

lemma word_sgn_mult_self_eq[simp]:
  "sgn a * sgn a = of_bool (a ≠ 0)" for a::"'a::len word"
  by (cases "0 <s a") simp_all

end