1(* SPDX-License-Identifier: BSD-3-Clause *)
2
3section\<open>Increment and Decrement Machine Words Without Wrap-Around\<close>
4
5theory Word_Next
6imports
7  Aligned
8begin
9
10text\<open>Previous and next words addresses, without wrap around.\<close>
11
12definition word_next :: "'a::len word \<Rightarrow> 'a::len word" where
13  "word_next a \<equiv> if a = max_word then max_word else a + 1"
14
15definition word_prev :: "'a::len word \<Rightarrow> 'a::len word" where
16  "word_prev a \<equiv> if a = 0 then 0 else a - 1"
17
18text\<open>Examples:\<close>
19
20lemma "word_next (2:: 8 word) = 3" by eval
21lemma "word_next (255:: 8 word) = 255" by eval
22lemma "word_prev (2:: 8 word) = 1" by eval
23lemma "word_prev (0:: 8 word) = 0" by eval
24
25
26lemma plus_one_helper[elim!]:
27  "x < n + (1 :: 'a :: len word) \<Longrightarrow> x \<le> n"
28  apply (simp add: word_less_nat_alt word_le_nat_alt field_simps)
29  apply (case_tac "1 + n = 0")
30   apply simp
31  apply (subst(asm) unatSuc, assumption)
32  apply arith
33  done
34
35lemma plus_one_helper2:
36  "\<lbrakk> x \<le> n; n + 1 \<noteq> 0 \<rbrakk> \<Longrightarrow> x < n + (1 :: 'a :: len word)"
37  by (simp add: word_less_nat_alt word_le_nat_alt field_simps
38                unatSuc)
39
40lemma less_x_plus_1:
41  fixes x :: "'a :: len word" shows
42  "x \<noteq> max_word \<Longrightarrow> (y < (x + 1)) = (y < x \<or> y = x)"
43  apply (rule iffI)
44   apply (rule disjCI)
45   apply (drule plus_one_helper)
46   apply simp
47  apply (subgoal_tac "x < x + 1")
48   apply (erule disjE, simp_all)
49  apply (rule plus_one_helper2 [OF order_refl])
50  apply (rule notI, drule max_word_wrap)
51  apply simp
52  done
53
54
55lemma word_Suc_leq: fixes k::"'a::len word" shows "k \<noteq> max_word \<Longrightarrow> x < k + 1 \<longleftrightarrow> x \<le> k"
56  using less_x_plus_1 word_le_less_eq by auto
57
58lemma word_Suc_le: fixes k::"'a::len word" shows "x \<noteq> max_word \<Longrightarrow> x + 1 \<le> k \<longleftrightarrow> x < k"
59  by (meson not_less word_Suc_leq)
60
61lemma word_lessThan_Suc_atMost: fixes k::"'a::len word" shows "k \<noteq> max_word \<Longrightarrow> {..< k + 1} = {..k}"
62  by(simp add: lessThan_def atMost_def word_Suc_leq)
63
64lemma word_atLeastLessThan_Suc_atLeastAtMost:
65  fixes l::"'a::len word" shows "u \<noteq> max_word \<Longrightarrow> {l..< u + 1} = {l..u}"
66  by (simp add: atLeastAtMost_def atLeastLessThan_def word_lessThan_Suc_atMost)
67
68lemma word_atLeastAtMost_Suc_greaterThanAtMost: fixes l::"'a::len word"
69  shows "m \<noteq> max_word \<Longrightarrow> {m<..u} = {m + 1..u}"
70  by(simp add: greaterThanAtMost_def greaterThan_def atLeastAtMost_def atLeast_def word_Suc_le)
71
72lemma word_atLeastLessThan_Suc_atLeastAtMost_union:
73  fixes l::"'a::len word"
74  assumes "m \<noteq> max_word" and "l \<le> m" and "m \<le> u"
75  shows "{l..m} \<union> {m+1..u} = {l..u}"
76  proof -
77  from ivl_disj_un_two(8)[OF assms(2) assms(3)] have "{l..u} = {l..m} \<union> {m<..u}" by blast
78  with assms show ?thesis by(simp add: word_atLeastAtMost_Suc_greaterThanAtMost)
79  qed
80
81lemma word_adjacent_union:
82  "word_next e = s' \<Longrightarrow> s \<le> e \<Longrightarrow> s' \<le> e' \<Longrightarrow> {s..e} \<union> {s'..e'} = {s .. e'}"
83  by (metis Un_absorb2 atLeastatMost_subset_iff ivl_disj_un_two(7) max_word_max
84            word_atLeastLessThan_Suc_atLeastAtMost word_le_less_eq word_next_def linorder_not_le)
85
86end
87