src/HOL/Word/Word.thy

   apply (simp add: word_rcat_def bin_rcat_def rev_map)
   apply transfer
   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"
 
 

 subsection \<open>Split and cat\<close>
 
 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)))"
   apply (simp add: word_size not_less; transfer)
        apply (auto simp add: bit_concat_bit_iff bit_take_bit_iff)

   apply (drule test_bit_split)
   apply safe
    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>
   for ws :: \<open>'a::len word list\<close>
   apply (simp add: concat_bit_eq push_bit_eq_mult)

   for wl :: "'a::len word list"
   by (simp add: word_size word_rcat_def bin_rcat_def foldl_map rev_map bit_horner_sum_uint_exp_iff)
     (simp add: test_bit_eq_bit)
 
 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>
 
 lemma word_rotr_word_rotr_eq: