Theory Tools
section‹Tools›
theory Tools imports Main "HOL-Library.Sublist"
begin
subsection ‹ Prefixes, suffixes, and fragments ›
thm Cons_eq_appendI
lemma prefix_cons: "⟦prefix xs ys; zs = x # ys; prefix xs' (x # xs)⟧ ⟹ prefix xs' zs"
by (auto simp add: prefix_def Cons_eq_appendI)
lemma suffix_nonempty_extendable:
"⟦suffix xs l; xs ≠ l⟧ ⟹ ∃ x . suffix (x#xs) l"
apply (auto simp add: suffix_def)
by (metis append_butlast_last_id)
lemma set_suffix:
"⟦x ∈ set l'; suffix l' l⟧ ⟹ x ∈ set l"
by (auto simp add: suffix_def)
lemma set_prefix:
"⟦x ∈ set l'; prefix l' l⟧ ⟹ x ∈ set l"
by (auto simp add: prefix_def)
lemma set_suffix_elem: "suffix (x#xs) p ⟹ x ∈ set p"
by (meson list.set_intros(1) set_suffix)
lemma set_prefix_elem: "prefix (x#xs) p ⟹ x ∈ set p"
by (meson list.set_intros(1) set_prefix)
lemma Cons_suffix_set: "x ∈ set y ⟹ ∃ xs . suffix (x#xs) y"
using suffix_def by (metis split_list)
subsection ‹ Fragments ›
definition fragment :: "'a list ⇒ 'a list set ⇒ bool"
where "fragment xs St ⟷ (∃zs1 zs2. zs1 @ xs @ zs2 ∈ St)"
lemma fragmentI: "⟦ zs1 @ xs @ zs2 ∈ St ⟧ ⟹ fragment xs St"
by (auto simp add: fragment_def)
lemma fragmentE [elim]: "⟦fragment xs St; ⋀zs1 zs2. ⟦ zs1 @ xs @ zs2 ∈ St ⟧ ⟹ P ⟧ ⟹ P"
by (auto simp add: fragment_def)
lemma fragment_Nil [simp]: "fragment [] St ⟷ St ≠ {}"
by (force simp add: fragment_def dest: spec [where x="[]"])
lemma fragment_subset: "⟦St ⊆ St'; fragment l St⟧ ⟹ fragment l St'"
by(auto simp add: fragment_def)
lemma fragment_prefix: "⟦prefix l' l; fragment l St⟧ ⟹ fragment l' St"
by(auto simp add: fragment_def prefix_def) blast
lemma fragment_suffix: "⟦suffix l' l; fragment l St⟧ ⟹ fragment l' St"
by(auto simp add: fragment_def suffix_def)
(metis append.assoc)
lemma fragment_self [simp, intro]: "⟦l ∈ St⟧ ⟹ fragment l St"
by(auto simp add: fragment_def intro!: exI [where x="[]"])
lemma fragment_prefix_self [simp, intro]:
"⟦l ∈ St; prefix l' l⟧ ⟹ fragment l' St"
using fragment_prefix fragment_self by blast
lemma fragment_suffix_self [simp, intro]:
"⟦l ∈ St; suffix l' l⟧ ⟹ fragment l' St"
using fragment_suffix fragment_self by metis
lemma fragment_is_prefix_suffix:
"fragment l St ⟹ ∃pre suff . prefix l pre ∧ suffix pre suff ∧ suff ∈ St"
by (meson fragment_def prefixI suffixI)
subsection ‹ Pair Fragments ›
definition pfragment :: "'a ⇒ ('b list) ⇒ ('a × ('b list)) set ⇒ bool"
where "pfragment a xs St ⟷ (∃zs1 zs2. (a, zs1 @ xs @ zs2) ∈ St)"
lemma pfragmentI: "⟦ (ainf, zs1 @ xs @ zs2) ∈ St ⟧ ⟹ pfragment ainf xs St"
by (auto simp add: pfragment_def)
lemma pfragmentE [elim]: "⟦pfragment ainf xs St; ⋀zs1 zs2. ⟦ (ainf, zs1 @ xs @ zs2) ∈ St ⟧ ⟹ P ⟧ ⟹ P"
by (auto simp add: pfragment_def)
lemma pfragment_prefix:
"pfragment ainf (xs @ ys) St ⟹ pfragment ainf xs St"
by(auto simp add: pfragment_def)
lemma pfragment_prefix':
"⟦pfragment ainf ys St; prefix xs ys⟧ ⟹ pfragment ainf xs St"
by(auto 3 4 simp add: pfragment_def prefix_def)
lemma pfragment_suffix: "⟦suffix l' l; pfragment ainf l St⟧ ⟹ pfragment ainf l' St"
by(auto simp add: pfragment_def suffix_def)
(metis append.assoc)
lemma pfragment_self [simp, intro]: "⟦(ainf, l) ∈ St⟧ ⟹ pfragment ainf l St"
by(auto simp add: pfragment_def intro!: exI [where x="[]"])
lemma pfragment_suffix_self [simp, intro]:
"⟦(ainf, l) ∈ St; suffix l' l⟧ ⟹ pfragment ainf l' St"
using pfragment_suffix pfragment_self by metis
lemma pfragment_self_eq:
"⟦pfragment ainf l S; ⋀zs1 zs2 . (ainf, zs1@l@zs2) ∈ S ⟹ (ainf, zs1@l'@zs2) ∈ S⟧ ⟹ pfragment ainf l' S"
by(auto simp add: pfragment_def)
lemma pfragment_self_eq_nil:
"⟦pfragment ainf l S; ⋀zs1 zs2 . (ainf, zs1@l@zs2) ∈ S ⟹ (ainf, l'@zs2) ∈ S⟧ ⟹ pfragment ainf l' S"
apply(auto simp add: pfragment_def)
apply(rule exI[of _ "[]"])
by auto
lemma pfragment_cons: "pfragment ainfo (x # fut) S ⟹ pfragment ainfo fut S"
apply(auto 3 4 simp add: pfragment_def)
subgoal for zs1 zs2
apply(rule exI[of _ "zs1@[x]"])
by auto
done
subsection ‹ Head and Tails ›
fun head where "head [] = None" | "head (x#xs) = Some x"
fun ifhead where "ifhead [] n = n" | "ifhead (x#xs) _ = Some x"
fun tail where "tail [] = None" | "tail xs = Some (last xs)"
lemma head_cons: "xs ≠ [] ⟹ head xs = Some (hd xs)" by(cases xs, auto)
lemma tail_cons: "xs ≠ [] ⟹ tail xs = Some (last xs)" by(cases xs, auto)
lemma tail_snoc: "tail (xs @ [x]) = Some x" by(cases xs, auto)
lemma "∀y ys . l ≠ ys @ [y] ⟹ l = []"
using rev_exhaust by blast
lemma tl_append2: "tl (pref @ [a, b]) = tl (pref @ [a])@[b]"
by(induction pref, auto)
end