Theory Prefix

theory Prefix
imports Main
begin

(* 
  Prefixes and Prefix Closure of traces 
*)
definition prefix :: "'e list ⇒ 'e list ⇒ bool" (infixl "≼" 100)
where
"(l1 ≼ l2) ≡ (∃l3. l1 @ l3 = l2)" 

definition prefixclosed :: "('e list) set ⇒ bool"
where
"prefixclosed tr ≡ (∀l1 ∈ tr. ∀l2. l2 ≼ l1 ⟶ l2 ∈ tr)"

(* the empty list is a prefix of every list *)
lemma empty_prefix_of_all: "[] ≼ l" 
  using prefix_def [of "[]" l] by simp

(* the empty list is in any non-empty prefix-closed set *)
lemma empty_trace_contained: "⟦ prefixclosed tr ; tr ≠ {} ⟧ ⟹ [] ∈ tr"
proof -
  assume 1: "prefixclosed tr" and
         2: "tr ≠ {}"
  then obtain l1 where "l1 ∈ tr" 
    by auto
  with 1 have "∀l2. l2 ≼ l1 ⟶ l2 ∈ tr" 
    by (simp add: prefixclosed_def)
  thus "[] ∈ tr" 
    by (simp add: empty_prefix_of_all)
qed

(* the prefix-predicate is transitive *)
lemma transitive_prefix: "⟦ l1 ≼ l2 ; l2 ≼ l3 ⟧ ⟹ l1 ≼ l3"
  by (auto simp add: prefix_def)

end