# Theory Word_Upto

```section‹Word Upto›
theory Word_Upto
imports Main
Word_Lib.Word_Lemmas
begin

text‹Enumerate a range of machine words.›

text‹enumerate from the back (inefficient)›
function word_upto :: "'a word ⇒ 'a word ⇒ ('a::len) word list" where
"word_upto a b = (if a = b then [a] else word_upto a (b - 1) @ [b])"
by pat_completeness auto

(*by the way: does not terminate practically if b < a; will terminate after it
reaches the word wrap-around!*)

termination word_upto
apply(relation "measure (unat ∘ uncurry (-) ∘ prod.swap)")
apply(rule wf_measure; fail)
apply(simp)
apply(subgoal_tac "unat (b - a - 1) < unat (b - a)")
apply(rule measure_unat)
apply auto
done

declare word_upto.simps[simp del]

text‹enumerate from the front (more inefficient)›
function word_upto' :: "'a word ⇒ 'a word ⇒ ('a::len) word list" where
"word_upto' a b = (if a = b then [a] else a # word_upto' (a + 1) b)"
by pat_completeness auto

termination word_upto'
apply(relation "measure (λ (a, b). unat (b - a))")
apply(rule wf_measure; fail)
apply(simp)
apply(subgoal_tac "unat (b - a - 1) < unat (b - a)")
apply(rule measure_unat)
apply auto
done

declare word_upto'.simps[simp del]

lemma word_upto_cons_front[code]:
"word_upto a b = word_upto' a b"
proof(induction a b rule:word_upto'.induct)
case (1 a b)
have hlp1: "a ≠ b ⟹ a # word_upto (a + 1) b = word_upto a b"
apply(induction a b rule:word_upto.induct)
apply simp
apply(subst(1) word_upto.simps)
apply(simp)
apply safe
apply(subst(1) word_upto.simps)
apply (simp)
apply(subst(1) word_upto.simps)
apply (simp; fail)
apply(case_tac "a ≠ b - 1")
apply(simp)
apply (metis Cons_eq_appendI word_upto.simps)
apply(simp)
done

from 1[symmetric] show ?case
apply(cases "a = b")
subgoal
apply(subst word_upto.simps)
apply(subst word_upto'.simps)
by(simp)
apply(subst word_upto'.simps)
qed

(* Most of the lemmas I show about word_upto hold without a ≤ b,
but I don't need that right now and it's giving me a headache *)

lemma word_upto_set_eq: "a ≤ b ⟹ x ∈ set (word_upto a b) ⟷ a ≤ x ∧ x ≤ b"
proof
show "a ≤ b ⟹ x ∈ set (word_upto a b) ⟹ a ≤ x ∧ x ≤ b"
apply(induction a b rule: word_upto.induct)
apply(case_tac "a = b")
apply(subst(asm) word_upto.simps)
apply(simp; fail)
apply(subst(asm) word_upto.simps)
apply(simp)
apply(erule disjE)
apply(simp; fail)
proof(goal_cases)
case (1 a b)
from 1(2-3) have "b ≠ 0" by force
from 1(2,3) have "a ≤ b - 1"
from 1(1)[OF this 1(4)] show ?case by (metis dual_order.trans 1(2,3) less_imp_le measure_unat word_le_0_iff word_le_nat_alt)
qed
next
show "a ≤ x ∧ x ≤ b ⟹ x ∈ set (word_upto a b)"
apply(induction a b rule: word_upto.induct)
apply(case_tac "a = b")
apply(subst word_upto.simps)
apply(simp; force)
apply(subst word_upto.simps)
apply(simp)
apply(case_tac "x = b")
apply(simp;fail)
proof(goal_cases)
case (1 a b)
from 1(2-4) have "b ≠ 0" by force
from 1(2,4) have "x ≤ b - 1"
using le_step_down_word by auto
from 1(1) this show ?case by simp
qed
qed

lemma word_upto_distinct_hlp: "a ≤ b ⟹ a ≠ b ⟹ b ∉ set (word_upto a (b - 1))"
apply(rule ccontr, unfold not_not)
apply(subgoal_tac "a ≤ b - 1")
apply(drule iffD1[OF word_upto_set_eq[of a "b -1" b]])
apply(subgoal_tac "b ≠ 0")
apply(meson leD measure_unat word_le_nat_alt)
apply(blast intro: iffD1[OF word_le_0_iff])
using le_step_down_word apply blast
done

lemma distinct_word_upto: "a ≤ b ⟹ distinct (word_upto a b)"
apply(induction a b rule: word_upto.induct)
apply(case_tac "a = b")
apply(subst word_upto.simps)
apply(simp; force)
apply(subst word_upto.simps)
apply(case_tac "a ≤ b - 1")
apply(simp)
apply(rule word_upto_distinct_hlp; simp)
apply(simp)
apply(rule ccontr)
apply (simp add: not_le antisym word_minus_one_le_leq)
done

lemma word_upto_eq_upto: "s ≤ e ⟹ e ≤ unat (max_word :: 'l word) ⟹
word_upto ((of_nat :: nat ⇒ ('l :: len) word) s) (of_nat e) = map of_nat (upt s (Suc e))"
proof(induction e)
let ?mwon = "of_nat :: nat ⇒ 'l word"
let ?mmw = "max_word :: 'l word"
case (Suc e)
show ?case
proof(cases "?mwon s = ?mwon (Suc e)")
case True
have "s = Suc e" using le_unat_uoi Suc.prems True by metis
with True show ?thesis by(subst word_upto.simps) (simp)
next
case False
hence le: "s ≤ e" using le_SucE Suc.prems by blast
have lm: "e ≤ unat ?mmw" using Suc.prems by simp
have sucm: "(of_nat :: nat ⇒ ('l :: len) word) (Suc e) - 1 = of_nat e" using Suc.prems(2) by simp
note mIH = Suc.IH[OF le lm]
show ?thesis by(subst word_upto.simps) (simp add: False[simplified] Suc.prems mIH sucm)
qed

lemma word_upto_alt: "(a :: ('l :: len) word) ≤ b ⟹
word_upto a b = map of_nat (upt (unat a) (Suc (unat b)))"
proof -
let ?mmw = "- 1 :: 'l word"
assume le: "a ≤ b"
hence nle: "unat a ≤ unat b" by(unat_arith)
have lem: "unat b ≤ unat ?mmw" by (simp add: word_unat_less_le)
then show "word_upto a b = map of_nat [unat a..<Suc (unat b)]"
using word_upto_eq_upto [OF nle lem] by simp
qed

lemma word_upto_upt:
"word_upto a b = (if a ≤ b then map of_nat (upt (unat a) (Suc (unat b))) else word_upto a b)"
using word_upto_alt by metis

lemma sorted_word_upto:
fixes a b :: "('l :: len) word"
assumes "a ≤ b"
shows "sorted (word_upto a b)"
proof -
define m and n where ‹m = unat a› and ‹n = Suc (unat b)›
moreover have ‹sorted_wrt (λx y. (word_of_nat x :: 'l word) ≤ word_of_nat y) [m..<n]›
proof (rule sorted_wrt_mono_rel [of _ ‹(≤)›])
show ‹sorted [m..<n]›
by simp
fix r s
assume ‹r ∈ set [m..<n]› ‹s ∈ set [m..<n]› ‹r ≤ s›
then have ‹m ≤ r› ‹s < n›
by simp_all
then have ‹take_bit LENGTH('l) s = s›
by (auto simp add: m_def n_def less_Suc_eq_le unsigned_of_nat dest: le_unat_uoi)
with ‹r ≤ s› show ‹(word_of_nat r :: 'l word) ≤ word_of_nat s›
using take_bit_nat_less_eq_self apply (rule order_trans)
apply assumption
done
qed
then have ‹sorted (map word_of_nat [m..<n] :: 'l word list)›