Definition. Rule Induction, Automation, Structured Proofs › List subsequence relation [isa-002C]

inductive subsequence :: ‹'a list ⇒ 'a list ⇒ bool› where ss_empty: ‹subsequence [] []› | ss_keep: ‹subsequence xs ys ⟹ subsequence (x#xs) (x#ys)› | ss_drop: ‹subsequence xs ys ⟹ subsequence xs (y#ys)›