Languages

This file contains the definition and operations on formal languages over an alphabet. Note strings are implemented as lists over the alphabet. The operations in this file define a Kleene algebra over the languages.

def Language (α : Type u_4) : Type u_4

A language is a set of strings over an alphabet.

instance instMembershipListLanguage {α : Type u_1} : Membership (List α) (Language α)

instance instSingletonListLanguage {α : Type u_1} : Singleton (List α) (Language α)

instance instInsertListLanguage {α : Type u_1} : Insert (List α) (Language α)

instance instCompleteAtomicBooleanAlgebraLanguage {α : Type u_1} : CompleteAtomicBooleanAlgebra (Language α)

instance Language.instZeroLanguage {α : Type u_1} : Zero (Language α)

Zero language has no elements.

instance Language.instOneLanguage {α : Type u_1} : One (Language α)

1 : Language α contains only one element [].

instance Language.instInhabitedLanguage {α : Type u_1} : Inhabited (Language α)

instance Language.instAddLanguage {α : Type u_1} : Add (Language α)

The sum of two languages is their union.

instance Language.instMulLanguage {α : Type u_1} : Mul (Language α)

The product of two languages l and m is the language made of the strings x ++ y where x ∈ l and y ∈ m.

theorem Language.zero_def {α : Type u_1} : 0 = ∅

theorem Language.one_def {α : Type u_1} : 1 = {[]}

theorem Language.add_def {α : Type u_1} (l : Language α) (m : Language α) : l + m = l ∪ m

theorem Language.mul_def {α : Type u_1} (l : Language α) (m : Language α) : l * m = Set.image2 (fun x x_1 => x ++ x_1) l m

instance Language.instKStarLanguage {α : Type u_1} : KStar (Language α)

The Kleene star of a language L is the set of all strings which can be written by concatenating strings from L.

theorem Language.kstar_def {α : Type u_1} (l : Language α) : KStar.kstar l = {x | ∃ L, x = List.join L ∧ ∀ (y : List α), y ∈ L → y ∈ l}

theorem Language.ext {α : Type u_1} {l : Language α} {m : Language α} (h : ∀ (x : List α), x ∈ l ↔ x ∈ m) : l = m

@[simp]

theorem Language.not_mem_zero {α : Type u_1} (x : List α) : ¬x ∈ 0

@[simp]

theorem Language.mem_one {α : Type u_1} (x : List α) : x ∈ 1 ↔ x = []

theorem Language.nil_mem_one {α : Type u_1} : [] ∈ 1

theorem Language.mem_add {α : Type u_1} (l : Language α) (m : Language α) (x : List α) : x ∈ l + m ↔ x ∈ l ∨ x ∈ m

theorem Language.mem_mul {α : Type u_1} {l : Language α} {m : Language α} {x : List α} : x ∈ l * m ↔ ∃ a b, a ∈ l ∧ b ∈ m ∧ a ++ b = x

theorem Language.append_mem_mul {α : Type u_1} {l : Language α} {m : Language α} {a : List α} {b : List α} : a ∈ l → b ∈ m → a ++ b ∈ l * m

theorem Language.mem_kstar {α : Type u_1} {l : Language α} {x : List α} : x ∈ KStar.kstar l ↔ ∃ L, x = List.join L ∧ ∀ (y : List α), y ∈ L → y ∈ l

theorem Language.join_mem_kstar {α : Type u_1} {l : Language α} {L : List (List α)} (h : ∀ (y : List α), y ∈ L → y ∈ l) : List.join L ∈ KStar.kstar l

theorem Language.nil_mem_kstar {α : Type u_1} (l : Language α) : [] ∈ KStar.kstar l

instance Language.instSemiring {α : Type u_1} : Semiring (Language α)

@[simp]

theorem Language.add_self {α : Type u_1} (l : Language α) : l + l = l

def Language.map {α : Type u_1} {β : Type u_2} (f : α → β) : Language α →+* Language β

Maps the alphabet of a language.

@[simp]

theorem Language.map_id {α : Type u_1} (l : Language α) : ↑(Language.map id) l = l

@[simp]

theorem Language.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (l : Language α) : ↑(Language.map g) (↑(Language.map f) l) = ↑(Language.map (g ∘ f)) l

theorem Language.kstar_def_nonempty {α : Type u_1} (l : Language α) : KStar.kstar l = {x | ∃ S, x = List.join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}

theorem Language.le_iff {α : Type u_1} (l : Language α) (m : Language α) : l ≤ m ↔ l + m = m

theorem Language.le_mul_congr {α : Type u_1} {l₁ : Language α} {l₂ : Language α} {m₁ : Language α} {m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂

theorem Language.le_add_congr {α : Type u_1} {l₁ : Language α} {l₂ : Language α} {m₁ : Language α} {m₂ : Language α} : l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ + l₂ ≤ m₁ + m₂

theorem Language.mem_iSup {α : Type u_1} {ι : Sort v} {l : ι → Language α} {x : List α} : x ∈ ⨆ (i : ι), l i ↔ ∃ i, x ∈ l i

theorem Language.iSup_mul {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) : (⨆ (i : ι), l i) * m = ⨆ (i : ι), l i * m

theorem Language.mul_iSup {α : Type u_1} {ι : Sort v} (l : ι → Language α) (m : Language α) : m * ⨆ (i : ι), l i = ⨆ (i : ι), m * l i

theorem Language.iSup_add {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : (⨆ (i : ι), l i) + m = ⨆ (i : ι), l i + m

theorem Language.add_iSup {α : Type u_1} {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : m + ⨆ (i : ι), l i = ⨆ (i : ι), m + l i

theorem Language.mem_pow {α : Type u_1} {l : Language α} {x : List α} {n : ℕ} : x ∈ l ^ n ↔ ∃ S, x = List.join S ∧ List.length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l

theorem Language.kstar_eq_iSup_pow {α : Type u_1} (l : Language α) : KStar.kstar l = ⨆ (i : ℕ), l ^ i

@[simp]

theorem Language.map_kstar {α : Type u_1} {β : Type u_2} (f : α → β) (l : Language α) : ↑(Language.map f) (KStar.kstar l) = KStar.kstar (↑(Language.map f) l)

theorem Language.mul_self_kstar_comm {α : Type u_1} (l : Language α) : KStar.kstar l * l = l * KStar.kstar l

@[simp]

theorem Language.one_add_self_mul_kstar_eq_kstar {α : Type u_1} (l : Language α) : 1 + l * KStar.kstar l = KStar.kstar l

@[simp]

theorem Language.one_add_kstar_mul_self_eq_kstar {α : Type u_1} (l : Language α) : 1 + KStar.kstar l * l = KStar.kstar l

instance Language.instKleeneAlgebraLanguage {α : Type u_1} : KleeneAlgebra (Language α)