Theory Word_Lib.Rsplit
section ‹Splitting words into lists›
theory Rsplit
imports More_Word Bit_Shifts_Infix_Syntax
begin
lemmas th_if_simp1 = if_split [where P = "(=) l", THEN iffD1, THEN conjunct1, THEN mp] for l
lemmas th_if_simp2 = if_split [where P = "(=) l", THEN iffD1, THEN conjunct2, THEN mp] for l
definition bin_split :: ‹nat ⇒ int ⇒ int × int›
where [simp]: ‹bin_split n k = (drop_bit n k, take_bit n k)›
lemma [code]:
"bin_split (Suc n) w = (let (w1, w2) = bin_split n (w div 2) in (w1, of_bool (odd w) + 2 * w2))"
"bin_split 0 w = (w, 0)"
by (simp_all add: drop_bit_Suc take_bit_Suc mod_2_eq_odd)
fun bin_rsplit_aux :: "nat ⇒ nat ⇒ int ⇒ int list ⇒ int list"
where "bin_rsplit_aux n m c bs =
(if m = 0 ∨ n = 0 then bs
else
let (a, b) = bin_split n c
in bin_rsplit_aux n (m - n) a (b # bs))"
definition bin_rsplit :: "nat ⇒ nat × int ⇒ int list"
where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
fun bin_rsplitl_aux :: "nat ⇒ nat ⇒ int ⇒ int list ⇒ int list"
where "bin_rsplitl_aux n m c bs =
(if m = 0 ∨ n = 0 then bs
else
let (a, b) = bin_split (min m n) c
in bin_rsplitl_aux n (m - n) a (b # bs))"
definition bin_rsplitl :: "nat ⇒ nat × int ⇒ int list"
where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
declare bin_rsplit_aux.simps [simp del]
declare bin_rsplitl_aux.simps [simp del]
lemma bin_nth_split:
"bin_split n c = (a, b) ⟹
(∀k. (bit :: int ⇒ nat ⇒ bool) a k = (bit :: int ⇒ nat ⇒ bool) c (n + k)) ∧
(∀k. (bit :: int ⇒ nat ⇒ bool) b k = (k < n ∧ (bit :: int ⇒ nat ⇒ bool) c k))"
apply (drule sym)
apply (simp add: bit_simps)
done
lemma split_bintrunc: "bin_split n c = (a, b) ⟹ b = (take_bit :: nat ⇒ int ⇒ int) n c"
by simp
lemma bin_cat_split: "bin_split n w = (u, v) ⟹ w = (λk n l. concat_bit n l k) u n v"
apply (drule sym)
using bits_ident [of n w]
apply (simp add: concat_bit_eq)
done
lemma bin_split_cat: "bin_split n ((λk n l. concat_bit n l k) v n w) = (v, (take_bit :: nat ⇒ int ⇒ int) n w)"
apply (auto intro!: bit_eqI)
apply (simp_all add: bit_simps)
apply auto
done
lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
by simp
lemma bin_split_minus1 [simp]:
"bin_split n (- 1) = (- 1, (take_bit :: nat ⇒ int ⇒ int) n (- 1))"
by simp
lemma bin_split_trunc:
"bin_split (min m n) c = (a, b) ⟹
bin_split n ((take_bit :: nat ⇒ int ⇒ int) m c) = ((take_bit :: nat ⇒ int ⇒ int) (m - n) a, b)"
apply (drule sym)
apply (simp add: drop_bit_take_bit ac_simps)
apply (cases ‹n ≤ m›)
apply simp_all
done
lemma bin_split_trunc1:
"bin_split n c = (a, b) ⟹
bin_split n ((take_bit :: nat ⇒ int ⇒ int) m c) = ((take_bit :: nat ⇒ int ⇒ int) (m - n) a, (take_bit :: nat ⇒ int ⇒ int) m b)"
apply (drule sym)
apply (simp add: drop_bit_take_bit ac_simps)
done
lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
by (simp add: drop_bit_eq_div take_bit_eq_mod)
lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
lemmas rsplit_aux_simps = bin_rsplit_aux_simps
lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2]
lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
lemmas rbscl = bin_rsplit_aux_simp2s (2)
lemmas rsplit_aux_0_simps [simp] =
rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
lemma bin_rsplit_aux_append: "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
apply (induct n m c bs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
apply (subst bin_rsplit_aux.simps)
apply (clarsimp split: prod.split)
done
lemma bin_rsplitl_aux_append: "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
apply (induct n m c bs rule: bin_rsplitl_aux.induct)
apply (subst bin_rsplitl_aux.simps)
apply (subst bin_rsplitl_aux.simps)
apply (clarsimp split: prod.split)
done
lemmas rsplit_aux_apps [where bs = "[]"] =
bin_rsplit_aux_append bin_rsplitl_aux_append
lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def
lemmas rsplit_aux_alts = rsplit_aux_apps
[unfolded append_Nil rsplit_def_auxs [symmetric]]
lemma bin_split_minus: "0 < n ⟹ bin_split (Suc (n - 1)) w = bin_split n w"
by auto
lemma bin_split_pred_simp [simp]:
"(0::nat) < numeral bin ⟹
bin_split (numeral bin) w =
(let (w1, w2) = bin_split (numeral bin - 1) ((λk::int. k div 2) w)
in (w1, of_bool (odd w) + 2 * w2))"
by (simp add: take_bit_rec drop_bit_rec mod_2_eq_odd)
lemma bin_rsplit_aux_simp_alt:
"bin_rsplit_aux n m c bs =
(if m = 0 ∨ n = 0 then bs
else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
apply (simp add: bin_rsplit_aux.simps [of n m c bs])
apply (subst rsplit_aux_alts)
apply (simp add: bin_rsplit_def)
done
lemmas bin_rsplit_simp_alt =
trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt]
lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
lemma bin_rsplit_size_sign' [rule_format]:
"n > 0 ⟹ rev sw = bin_rsplit n (nw, w) ⟹ ∀v∈set sw. (take_bit :: nat ⇒ int ⇒ int) n v = v"
apply (induct sw arbitrary: nw w)
apply clarsimp
apply clarsimp
apply (drule bthrs)
apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm)
apply clarify
apply simp
done
lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl
rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]]
lemma bin_nth_rsplit [rule_format] :
"n > 0 ⟹ m < n ⟹
∀w k nw.
rev sw = bin_rsplit n (nw, w) ⟶
k < size sw ⟶ (bit :: int ⇒ nat ⇒ bool) (sw ! k) m = (bit :: int ⇒ nat ⇒ bool) w (k * n + m)"
apply (induct sw)
apply clarsimp
apply clarsimp
apply (drule bthrs)
apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm)
apply (erule allE, erule impE, erule exI)
apply (case_tac k)
apply clarsimp
prefer 2
apply clarsimp
apply (erule allE)
apply (erule (1) impE)
apply (simp add: bit_drop_bit_eq ac_simps)
apply (simp add: bit_take_bit_iff ac_simps)
done
lemma bin_rsplit_all: "0 < nw ⟹ nw ≤ n ⟹ bin_rsplit n (nw, w) = [(take_bit :: nat ⇒ int ⇒ int) n w]"
by (auto simp: bin_rsplit_def rsplit_aux_simp2ls split: prod.split dest!: split_bintrunc)
lemma bin_rsplit_l [rule_format]:
"∀bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, (take_bit :: nat ⇒ int ⇒ int) m bin)"
apply (rule_tac a = "m" in wf_less_than [THEN wf_induct])
apply (simp (no_asm) add: bin_rsplitl_def bin_rsplit_def)
apply (rule allI)
apply (subst bin_rsplitl_aux.simps)
apply (subst bin_rsplit_aux.simps)
apply (clarsimp simp: Let_def split: prod.split)
apply (simp add: ac_simps)
apply (subst rsplit_aux_alts(1))
apply (subst rsplit_aux_alts(2))
apply clarsimp
unfolding bin_rsplit_def bin_rsplitl_def
apply (simp add: drop_bit_take_bit)
apply (case_tac ‹x < n›)
apply (simp_all add: not_less min_def)
done
lemma bin_rsplit_aux_len_le [rule_format] :
"∀ws m. n ≠ 0 ⟶ ws = bin_rsplit_aux n nw w bs ⟶
length ws ≤ m ⟷ nw + length bs * n ≤ m * n"
proof -
have *: R
if d: "i ≤ j ∨ m < j'"
and R1: "i * k ≤ j * k ⟹ R"
and R2: "Suc m * k' ≤ j' * k' ⟹ R"
for i j j' k k' m :: nat and R
using d
apply safe
apply (rule R1, erule mult_le_mono1)
apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
done
have **: "0 < sc ⟹ sc - n + (n + lb * n) ≤ m * n ⟷ sc + lb * n ≤ m * n"
for sc m n lb :: nat
apply safe
apply arith
apply (case_tac "sc ≥ n")
apply arith
apply (insert linorder_le_less_linear [of m lb])
apply (erule_tac k=n and k'=n in *)
apply arith
apply simp
done
show ?thesis
apply (induct n nw w bs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
apply (simp add: ** Let_def split: prod.split)
done
qed
lemma bin_rsplit_len_le: "n ≠ 0 ⟶ ws = bin_rsplit n (nw, w) ⟶ length ws ≤ m ⟷ nw ≤ m * n"
by (auto simp: bin_rsplit_def bin_rsplit_aux_len_le)
lemma bin_rsplit_aux_len:
"n ≠ 0 ⟹ length (bin_rsplit_aux n nw w cs) = (nw + n - 1) div n + length cs"
apply (induct n nw w cs rule: bin_rsplit_aux.induct)
apply (subst bin_rsplit_aux.simps)
apply (clarsimp simp: Let_def split: prod.split)
apply (erule thin_rl)
apply (case_tac m)
apply simp
apply (case_tac "m ≤ n")
apply (auto simp add: div_add_self2)
done
lemma bin_rsplit_len: "n ≠ 0 ⟹ length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
by (auto simp: bin_rsplit_def bin_rsplit_aux_len)
lemma bin_rsplit_aux_len_indep:
"n ≠ 0 ⟹ length bs = length cs ⟹
length (bin_rsplit_aux n nw v bs) =
length (bin_rsplit_aux n nw w cs)"
proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
case (1 n m w cs v bs)
show ?case
proof (cases "m = 0")
case True
with ‹length bs = length cs› show ?thesis by simp
next
case False
from "1.hyps" [of ‹bin_split n w› ‹drop_bit n w› ‹take_bit n w›] ‹m ≠ 0› ‹n ≠ 0›
have hyp: "⋀v bs. length bs = Suc (length cs) ⟹
length (bin_rsplit_aux n (m - n) v bs) =
length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs))"
using bin_rsplit_aux_len by fastforce
from ‹length bs = length cs› ‹n ≠ 0› show ?thesis
by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split)
qed
qed
lemma bin_rsplit_len_indep:
"n ≠ 0 ⟹ length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
apply (unfold bin_rsplit_def)
apply (simp (no_asm))
apply (erule bin_rsplit_aux_len_indep)
apply (rule refl)
done
lemma split_uint_lem: "bin_split n (uint w) = (a, b) ⟹
a = take_bit (LENGTH('a) - n) a ∧ b = take_bit (LENGTH('a)) b"
for w :: "'a::len word"
by transfer (simp add: drop_bit_take_bit ac_simps)
definition word_rsplit :: "'a::len word ⇒ 'b::len word list"
where "word_rsplit w = map word_of_int (bin_rsplit LENGTH('b) (LENGTH('a), uint w))"
lemma word_rsplit_no:
"(word_rsplit (numeral bin :: 'b::len word) :: 'a word list) =
map word_of_int (bin_rsplit (LENGTH('a::len))
(LENGTH('b), take_bit (LENGTH('b)) (numeral bin)))"
by (simp add: word_rsplit_def of_nat_take_bit)
lemmas word_rsplit_no_cl [simp] = word_rsplit_no
[unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
text ‹
This odd result arises from the fact that the statement of the
result implies that the decoded words are of the same type,
and therefore of the same length, as the original word.›
lemma word_rsplit_same: "word_rsplit w = [w]"
apply (simp add: word_rsplit_def bin_rsplit_all)
apply transfer
apply simp
done
lemma word_rsplit_empty_iff_size: "word_rsplit w = [] ⟷ size w = 0"
by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
split: prod.split)
lemma test_bit_rsplit:
"sw = word_rsplit w ⟹ m < size (hd sw) ⟹
k < length sw ⟹ bit (rev sw ! k) m = bit w (k * size (hd sw) + m)"
for sw :: "'a::len word list"
apply (unfold word_rsplit_def word_test_bit_def)
apply (rule trans)
apply (rule_tac f = "λx. bit x m" in arg_cong)
apply (rule nth_map [symmetric])
apply simp
apply (rule bin_nth_rsplit)
apply simp_all
apply (simp add : word_size rev_map)
apply (rule trans)
defer
apply (rule map_ident [THEN fun_cong])
apply (rule refl [THEN map_cong])
apply (simp add: unsigned_of_int take_bit_int_eq_self_iff)
using bin_rsplit_size_sign take_bit_int_eq_self_iff by blast
lemma test_bit_rsplit_alt:
‹bit ((word_rsplit w :: 'b::len word list) ! i) m ⟷
bit w ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)›
if ‹i < length (word_rsplit w :: 'b::len word list)› ‹m < size (hd (word_rsplit w :: 'b::len word list))› ‹0 < length (word_rsplit w :: 'b::len word list)›
for w :: ‹'a::len word›
apply (rule trans)
apply (rule test_bit_cong)
apply (rule rev_nth [of _ ‹rev (word_rsplit w)›, simplified rev_rev_ident])
apply simp
apply (rule that(1))
apply simp
apply (rule test_bit_rsplit)
apply (rule refl)
apply (rule asm_rl)
apply (rule that(2))
apply (rule diff_Suc_less)
apply (rule that(3))
done
lemma word_rsplit_len_indep [OF refl refl refl refl]:
"[u,v] = p ⟹ [su,sv] = q ⟹ word_rsplit u = su ⟹
word_rsplit v = sv ⟹ length su = length sv"
by (auto simp: word_rsplit_def bin_rsplit_len_indep)
lemma length_word_rsplit_size:
"n = LENGTH('a::len) ⟹
length (word_rsplit w :: 'a word list) ≤ m ⟷ size w ≤ m * n"
by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
lemmas length_word_rsplit_lt_size =
length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
lemma length_word_rsplit_exp_size:
"n = LENGTH('a::len) ⟹
length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
by (auto simp: word_rsplit_def word_size bin_rsplit_len)
lemma length_word_rsplit_even_size:
"n = LENGTH('a::len) ⟹ size w = m * n ⟹
length (word_rsplit w :: 'a word list) = m"
by (cases ‹LENGTH('a)›) (simp_all add: length_word_rsplit_exp_size div_nat_eqI)
lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
lemmas tdle = times_div_less_eq_dividend
lemmas dtle = xtrans(4) [OF tdle mult.commute]
lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
apply (rule word_eqI)
apply (clarsimp simp: test_bit_rcat word_size)
apply (subst refl [THEN test_bit_rsplit])
apply (simp_all add: word_size
refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
apply safe
apply (erule xtrans(7), rule dtle)+
done
lemma size_word_rsplit_rcat_size:
"word_rcat ws = frcw ⟹ size frcw = length ws * LENGTH('a)
⟹ length (word_rsplit frcw::'a word list) = length ws"
for ws :: "'a::len word list" and frcw :: "'b::len word"
by (cases ‹LENGTH('a)›) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)
lemma word_rsplit_rcat_size [OF refl]:
"word_rcat ws = frcw ⟹
size frcw = length ws * LENGTH('a) ⟹ word_rsplit frcw = ws"
for ws :: "'a::len word list"
apply (frule size_word_rsplit_rcat_size, assumption)
apply (clarsimp simp add : word_size)
apply (rule nth_equalityI, assumption)
apply clarsimp
apply (rule word_eqI [rule_format])
apply (rule trans)
apply (rule test_bit_rsplit_alt)
apply (clarsimp simp: word_size)+
apply (rule trans)
apply (rule test_bit_rcat [OF refl refl])
apply (simp add: word_size)
apply (subst rev_nth)
apply arith
apply (simp add: le0 [THEN [2] xtrans(7), THEN diff_Suc_less])
apply safe
apply (simp add: diff_mult_distrib)
apply (cases "size ws")
apply simp_all
done
lemma word_rsplit_upt:
"size x = LENGTH('a :: len) * n ⟹ n ≠ 0
⟹ word_rsplit x = map (λi. ucast (x >> (i * LENGTH('a))) :: 'a word) (rev [0 ..< n])"
apply (subgoal_tac "length (word_rsplit x :: 'a word list) = n")
apply (rule nth_equalityI, simp)
apply (intro allI word_eqI impI)
apply (simp add: test_bit_rsplit_alt word_size)
apply (simp add: nth_ucast bit_simps rev_nth field_simps)
apply (simp add: length_word_rsplit_exp_size word_size)
apply (subst diff_add_assoc)
apply (simp flip: less_eq_Suc_le)
apply simp
done
end