# HG changeset patch
# User haftmann
# Date 1602766519 -7200
# Node ID ab32922f139bc9f1f52952f71c5104129ed9d7c3
# Parent  e4d707eb7d1bff22384271f7121d14f9e89ee39f
factored out singular operation into separate theory

diff -r e4d707eb7d1b -r ab32922f139b src/HOL/Word/Bits_Int.thy
--- 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
diff -r e4d707eb7d1b -r ab32922f139b src/HOL/Word/More_Word.thy
--- 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]
diff -r e4d707eb7d1b -r ab32922f139b src/HOL/Word/Word.thy
--- 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>
 
diff -r e4d707eb7d1b -r ab32922f139b src/HOL/Word/Word_rsplit.thy
--- /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