Theory Word_Next

theory Word_Next
imports Aligned
(* SPDX-License-Identifier: BSD-3-Clause *)

section‹Increment and Decrement Machine Words Without Wrap-Around›

theory Word_Next
imports
  Aligned
begin

text‹Previous and next words addresses, without wrap around.›

definition word_next :: "'a::len word ⇒ 'a::len word" where
  "word_next a ≡ if a = max_word then max_word else a + 1"

definition word_prev :: "'a::len word ⇒ 'a::len word" where
  "word_prev a ≡ if a = 0 then 0 else a - 1"

text‹Examples:›

lemma "word_next (2:: 8 word) = 3" by eval
lemma "word_next (255:: 8 word) = 255" by eval
lemma "word_prev (2:: 8 word) = 1" by eval
lemma "word_prev (0:: 8 word) = 0" by eval

lemma plus_one_helper[elim!]:
  "x < n + (1 :: 'a :: len word) ⟹ x ≤ n"
  apply (simp add: word_less_nat_alt word_le_nat_alt field_simps)
  apply (case_tac "1 + n = 0")
   apply simp
  apply (subst(asm) unatSuc, assumption)
  apply arith
  done

lemma plus_one_helper2:
  "⟦ x ≤ n; n + 1 ≠ 0 ⟧ ⟹ x < n + (1 :: 'a :: len word)"
  by (simp add: word_less_nat_alt word_le_nat_alt field_simps
                unatSuc)

lemma less_x_plus_1:
  fixes x :: "'a :: len word" shows
  "x ≠ max_word ⟹ (y < (x + 1)) = (y < x ∨ y = x)"
  apply (rule iffI)
   apply (rule disjCI)
   apply (drule plus_one_helper)
   apply simp
  apply (subgoal_tac "x < x + 1")
   apply (erule disjE, simp_all)
  apply (rule plus_one_helper2 [OF order_refl])
  apply (rule notI, drule max_word_wrap)
  apply simp
  done


lemma word_Suc_leq: fixes k::"'a::len word" shows "k ≠ max_word ⟹ x < k + 1 ⟷ x ≤ k"
  using less_x_plus_1 word_le_less_eq by auto

lemma word_Suc_le: fixes k::"'a::len word" shows "x ≠ max_word ⟹ x + 1 ≤ k ⟷ x < k"
  by (meson not_less word_Suc_leq)

lemma word_lessThan_Suc_atMost:
  ‹{..< k + 1} = {..k}› if ‹k ≠ - 1› for k :: ‹'a::len word›
  using that by (simp add: lessThan_def atMost_def word_Suc_leq)

lemma word_atLeastLessThan_Suc_atLeastAtMost:
  ‹{l ..< u + 1} = {l..u}› if ‹u ≠ - 1› for l :: ‹'a::len word›
  using that by (simp add: atLeastAtMost_def atLeastLessThan_def word_lessThan_Suc_atMost)

lemma word_atLeastAtMost_Suc_greaterThanAtMost:
  ‹{m<..u} = {m + 1..u}› if ‹m ≠ - 1› for m :: ‹'a::len word›
  using that by (simp add: greaterThanAtMost_def greaterThan_def atLeastAtMost_def atLeast_def word_Suc_le)

lemma word_atLeastLessThan_Suc_atLeastAtMost_union:
  fixes l::"'a::len word"
  assumes "m ≠ max_word" and "l ≤ m" and "m ≤ u"
  shows "{l..m} ∪ {m+1..u} = {l..u}"
  proof -
  from ivl_disj_un_two(8)[OF assms(2) assms(3)] have "{l..u} = {l..m} ∪ {m<..u}" by blast
  with assms show ?thesis by(simp add: word_atLeastAtMost_Suc_greaterThanAtMost)
  qed

lemma max_word_less_eq_iff [simp]:
  ‹- 1 ≤ w ⟷ w = - 1› for w :: ‹'a::len word›
  by (auto simp add: le_less)  

lemma word_adjacent_union:
  "word_next e = s' ⟹ s ≤ e ⟹ s' ≤ e' ⟹ {s..e} ∪ {s'..e'} = {s .. e'}"
  apply (simp add: word_next_def ivl_disj_un_two_touch split: if_splits)
  apply (drule sym)
  apply simp
  apply (subst word_atLeastLessThan_Suc_atLeastAtMost_union)
     apply (simp_all add: word_Suc_le)
  done

end