Theory List_Lemmata

theory List_Lemmata imports Main begin

lemma last_take_Suc:
  "i < length l ⟹ last (take (Suc i) l) = l!i"
  by (simp add: take_Suc_conv_app_nth)

lemma list_eq: "(length xs = length ys ∧ (∀i<length xs. xs!i=ys!i)) = (xs=ys)"
  apply(rule iffI)
  apply clarify
  apply(erule nth_equalityI)
  apply simp+
  done

lemma nth_tl: "⟦ ys!0=a; ys≠[] ⟧ ⟹ ys=(a#(tl ys))"
  by (cases ys) simp_all

lemma nth_tl_if [rule_format]: "ys≠[] ⟶ ys!0=a ⟶ P ys ⟶ P (a#(tl ys))"
  by (induct ys) simp_all

lemma nth_tl_onlyif [rule_format]: "ys≠[] ⟶ ys!0=a ⟶ P (a#(tl ys)) ⟶ P ys"
  by (induct ys) simp_all

lemma drop_destruct:
  ‹Suc n ≤ length xs ⟹ drop n xs = hd (drop n xs) # drop (Suc n) xs›
  by (metis drop_Suc drop_eq_Nil hd_Cons_tl not_less_eq_eq tl_drop)

lemma drop_last:
  ‹xs ≠ [] ⟹ drop (length xs - 1) xs = [last xs]›
  by (metis append_butlast_last_id append_eq_conv_conj length_butlast)

end