Theory Suffix

theory Suffix
  imports Main
begin

section ‹Suffix›

abbreviation suffix :: "'a list ⇒ nat ⇒ 'a list"
  where
"suffix xs i ≡ drop i xs"

lemma suffixes_neq:
  "⟦i < length s; j < length s; i ≠ j⟧ ⟹ suffix s i ≠ suffix s j"
  by (metis diff_diff_cancel length_drop less_or_eq_imp_le)

lemma distinct_suffixes:
  "⟦distinct xs; ∀x ∈ set xs. x < length s⟧ ⟹ distinct (map (suffix s) xs)"
  by (simp add: distinct_conv_nth suffixes_neq)

lemma suffix_eq_index:
  "⟦i < length xs; j < length xs; suffix xs i = suffix xs j⟧ ⟹ i = j"
  by (metis diff_diff_cancel le_eq_less_or_eq length_drop)

lemma suffix_neq_nil:
  "i < length s ⟹ suffix s i ≠ []"
  by simp

lemma suffix_map:
  "suffix (map f xs) i = map f (suffix xs i)"
  by (simp add: drop_map)

lemma set_suffix_subset:
  "set (suffix s i) ⊆ set s"
  by (simp add: set_drop_subset)
lemma suffix_cons_suc:
  "suffix (a # xs) (Suc i) = suffix xs i"
  by simp

lemma suffix_app:
  "i < length xs ⟹ suffix (xs @ ys) i = suffix xs i @ ys"
  by simp

lemma suffix_cons_ex:
  "i < length T ⟹ ∃x xs. suffix T i = x # xs ∧ x = T ! i"
  by (metis Cons_nth_drop_Suc)

lemma suffix_cons_Suc:
  "i < length T ⟹ suffix T i = T ! i # suffix T (Suc i)"
  by (metis Cons_nth_drop_Suc)

lemma suffix_cons_app:
  "suffix T i = as @ bs ⟹ suffix T (i + length as) = bs"
  by (metis add.commute append_eq_conv_conj drop_drop)

lemma suffix_0:
  "suffix T 0 = T"
  by simp

end