--- a/src/HOL/Word/Bits_Int.thy Fri Oct 16 19:34:37 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy Thu Oct 15 14:55:19 2020 +0200
@@ -511,6 +511,8 @@
definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
+value \<open>bin_rsplit 1705 (3, 88)\<close>
+
fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
where "bin_rsplitl_aux n m c bs =
(if m = 0 \<or> n = 0 then bs
--- a/src/HOL/Word/More_Word.thy Fri Oct 16 19:34:37 2020 +0200
+++ b/src/HOL/Word/More_Word.thy Thu Oct 15 14:55:19 2020 +0200
@@ -15,6 +15,7 @@
Misc_set_bit
Misc_lsb
Misc_Typedef
+ Word_rsplit
begin
declare signed_take_bit_Suc [simp]
--- a/src/HOL/Word/Word.thy Fri Oct 16 19:34:37 2020 +0200
+++ b/src/HOL/Word/Word.thy Thu Oct 15 14:55:19 2020 +0200
@@ -2283,9 +2283,6 @@
apply (simp add: horner_sum_foldr foldr_map comp_def)
done
-definition word_rsplit :: "'a::len word \<Rightarrow> 'b::len word list"
- where "word_rsplit w = map word_of_int (bin_rsplit (LENGTH('b)) (LENGTH('a), uint w))"
-
abbreviation (input) max_word :: \<open>'a::len word\<close>
\<comment> \<open>Largest representable machine integer.\<close>
where "max_word \<equiv> - 1"
@@ -4540,15 +4537,6 @@
lemmas word_split_bin' = word_split_def
lemmas word_cat_bin' = word_cat_eq
-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]]
-
lemma test_bit_cat [OF refl]:
"wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
(if n < size b then b !! n else a !! (n - size b)))"
@@ -4659,40 +4647,6 @@
apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
done
-text \<open>
- 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.\<close>
-
-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 = [] \<longleftrightarrow> 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 \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
- k < length sw \<Longrightarrow> (rev sw ! k) !! m = 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 = "\<lambda>x. bin_nth 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
- using bin_rsplit_size_sign take_bit_int_eq_self_iff by blast
-
lemma horner_sum_uint_exp_Cons_eq:
\<open>horner_sum uint (2 ^ LENGTH('a)) (w # ws) =
concat_bit LENGTH('a) (uint w) (horner_sum uint (2 ^ LENGTH('a)) ws)\<close>
@@ -4726,100 +4680,6 @@
lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
-lemma test_bit_rsplit_alt:
- \<open>(word_rsplit w :: 'b::len word list) ! i !! m \<longleftrightarrow>
- w !! ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)\<close>
- if \<open>i < length (word_rsplit w :: 'b::len word list)\<close> \<open>m < size (hd (word_rsplit w :: 'b::len word list))\<close> \<open>0 < length (word_rsplit w :: 'b::len word list)\<close>
- for w :: \<open>'a::len word\<close>
- apply (rule trans)
- apply (rule test_bit_cong)
- apply (rule rev_nth [of _ \<open>rev (word_rsplit w)\<close>, 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 \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
- word_rsplit v = sv \<Longrightarrow> length su = length sv"
- by (auto simp: word_rsplit_def bin_rsplit_len_indep)
-
-lemma length_word_rsplit_size:
- "n = LENGTH('a::len) \<Longrightarrow>
- length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> 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) \<Longrightarrow>
- 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) \<Longrightarrow> size w = m * n \<Longrightarrow>
- length (word_rsplit w :: 'a word list) = m"
- by (cases \<open>LENGTH('a)\<close>) (simp_all add: length_word_rsplit_exp_size div_nat_eqI)
-
-lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
-
-\<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
-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 \<Longrightarrow> size frcw = length ws * LENGTH('a)
- \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
- for ws :: "'a::len word list" and frcw :: "'b::len word"
- by (cases \<open>LENGTH('a)\<close>) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)
-
-lemma msrevs:
- "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
- "(k * n + m) mod n = m mod n"
- for n :: nat
- by (auto simp: add.commute)
-
-lemma word_rsplit_rcat_size [OF refl]:
- "word_rcat ws = frcw \<Longrightarrow>
- size frcw = length ws * LENGTH('a) \<Longrightarrow> 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
-
subsection \<open>Rotation\<close>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Word_rsplit.thy Thu Oct 15 14:55:19 2020 +0200
@@ -0,0 +1,149 @@
+(* Title: HOL/Word/Word_rsplit.thy
+ Author: Jeremy Dawson and Gerwin Klein, NICTA
+*)
+
+theory Word_rsplit
+ imports Bits_Int Word
+begin
+
+definition word_rsplit :: "'a::len word \<Rightarrow> '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 \<open>
+ 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.\<close>
+
+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 = [] \<longleftrightarrow> 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 \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
+ k < length sw \<Longrightarrow> (rev sw ! k) !! m = 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 = "\<lambda>x. bin_nth 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
+ using bin_rsplit_size_sign take_bit_int_eq_self_iff by blast
+
+lemma test_bit_rsplit_alt:
+ \<open>(word_rsplit w :: 'b::len word list) ! i !! m \<longleftrightarrow>
+ w !! ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)\<close>
+ if \<open>i < length (word_rsplit w :: 'b::len word list)\<close> \<open>m < size (hd (word_rsplit w :: 'b::len word list))\<close> \<open>0 < length (word_rsplit w :: 'b::len word list)\<close>
+ for w :: \<open>'a::len word\<close>
+ apply (rule trans)
+ apply (rule test_bit_cong)
+ apply (rule rev_nth [of _ \<open>rev (word_rsplit w)\<close>, 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 \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
+ word_rsplit v = sv \<Longrightarrow> length su = length sv"
+ by (auto simp: word_rsplit_def bin_rsplit_len_indep)
+
+lemma length_word_rsplit_size:
+ "n = LENGTH('a::len) \<Longrightarrow>
+ length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> 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) \<Longrightarrow>
+ 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) \<Longrightarrow> size w = m * n \<Longrightarrow>
+ length (word_rsplit w :: 'a word list) = m"
+ by (cases \<open>LENGTH('a)\<close>) (simp_all add: length_word_rsplit_exp_size div_nat_eqI)
+
+lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
+
+\<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
+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 \<Longrightarrow> size frcw = length ws * LENGTH('a)
+ \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
+ for ws :: "'a::len word list" and frcw :: "'b::len word"
+ by (cases \<open>LENGTH('a)\<close>) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)
+
+lemma msrevs:
+ "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
+ "(k * n + m) mod n = m mod n"
+ for n :: nat
+ by (auto simp: add.commute)
+
+lemma word_rsplit_rcat_size [OF refl]:
+ "word_rcat ws = frcw \<Longrightarrow>
+ size frcw = length ws * LENGTH('a) \<Longrightarrow> 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
+
+end
\ No newline at end of file