(* Title: HOL/Library/Sublist.thy Author: Tobias Nipkow and Markus Wenzel, TU München Author: Christian Sternagel, JAIST Author: Manuel Eberl, TU München *) section ‹List prefixes, suffixes, and homeomorphic embedding› theory Sublist imports Main begin subsection ‹Prefix order on lists› definition prefix :: "'a list ⇒ 'a list ⇒ bool" where "prefix xs ys ⟷ (∃zs. ys = xs @ zs)" definition strict_prefix :: "'a list ⇒ 'a list ⇒ bool" where "strict_prefix xs ys ⟷ prefix xs ys ∧ xs ≠ ys" global_interpretation prefix_order: ordering prefix strict_prefix by standard (auto simp add: prefix_def strict_prefix_def)