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