Theory Prefix

theory Prefix
  imports Main
begin

section ‹Prefix Definition›

abbreviation prefix :: "'a list ⇒ nat ⇒ 'a list"
  where
"prefix xs i ≡ take i xs"

lemma prefix_neq:
  assumes "i < length s"
  and     "j < length s"
  and     "i ≠ j"
shows "prefix s i ≠ prefix s j"
  by (metis assms length_take less_imp_le min_absorb2)

lemma not_prefix_app:
  "(∀k. s1 ≠ prefix s2 k) ⟷ (∀xs. s2 ≠ s1 @ xs)"
  by (metis append_eq_conv_conj append_take_drop_id)

lemma not_prefix_imp_not_nil:
  "∀k. s1 ≠ prefix s2 k ⟹ s1 ≠ []"
  by (metis take0)

end