Theory Misc_Auxiliary

theory Misc_Auxiliary
imports Main
(*  Title:      HOL/Word/Misc_Auxiliary.thy
    Author:     Jeremy Dawson, NICTA
*)

section ‹Generic auxiliary›

theory Misc_Auxiliary
  imports Main
begin

subsection ‹Lemmas on list operations›

lemma butlast_power: "(butlast ^^ n) bl = take (length bl - n) bl"
  by (induct n) (auto simp: butlast_take)

lemma nth_rev: "n < length xs ⟹ rev xs ! n = xs ! (length xs - 1 - n)"
  using rev_nth by simp

lemma nth_rev_alt: "n < length ys ⟹ ys ! n = rev ys ! (length ys - Suc n)"
  by (simp add: nth_rev)

lemma hd_butlast: "length xs > 1 ⟹ hd (butlast xs) = hd xs"
  by (cases xs) auto

end