Vocabulary (part of Section 2.1)

@[reducible, inline]

abbrev Vocab : Type

Equations

• Vocab = Finset (ℕ ⊕ ℕ)

def Vocab.atomProps : Vocab → Finset ℕ

Equations

• X.atomProps = Finset.biUnion X fun (x : ℕ ⊕ ℕ) => match x with | Sum.inl n => {n} | Sum.inr val => ∅

def Vocab.atomProgs : Vocab → Finset ℕ

Equations

• X.atomProgs = Finset.biUnion X fun (x : ℕ ⊕ ℕ) => match x with | Sum.inl val => ∅ | Sum.inr n => {n}

def Program.voc : Program → Vocab

Equations

• (·n).voc = {Sum.inr n}
• (α;'β).voc = α.voc ∪ β.voc
• (α⋓β).voc = α.voc ∪ β.voc
• (∗α).voc = α.voc
• (?'φ).voc = φ.voc

def Formula.voc : Formula → Vocab

Equations

• Formula.bottom.voc = ∅
• (·n).voc = {Sum.inl n}
• (~φ).voc = φ.voc
• (φ⋀ψ).voc = φ.voc ∪ ψ.voc
• (⌈α⌉φ).voc = α.voc ∪ φ.voc

def Vocab.fromList (L : List Vocab) : Vocab

Equations

• Vocab.fromList L = L.toFinset.sup id

@[reducible, inline]

abbrev List.fvoc (L : List Formula) : Vocab

Equations

• L.fvoc = Vocab.fromList (List.map Formula.voc L)

@[reducible, inline]

abbrev List.pvoc (L : List Program) : Vocab

Equations

• L.pvoc = Vocab.fromList (List.map Program.voc L)

@[simp]

theorem Vocab.fromList_append {L R : List Vocab} : fromList (L ++ R) = fromList L ∪ fromList R

theorem Vocab.fromList_map_iff {α : Type u_1} (n : ℕ ⊕ ℕ) (L : List α) (f : α → Vocab) : n ∈ fromList (List.map f L) ↔ ∃ x ∈ L, n ∈ f x

theorem Vocab.fromListFormula_map_iff (n : ℕ ⊕ ℕ) (L : List Formula) : n ∈ fromList (List.map Formula.voc L) ↔ ∃ φ ∈ L, n ∈ φ.voc

theorem Vocab.fromListProgram_map_iff {vocabOfProgram : Program → Vocab} (n : ℕ ⊕ ℕ) (L : List Program) : n ∈ fromList (List.map vocabOfProgram L) ↔ ∃ α ∈ L, n ∈ vocabOfProgram α

theorem Formula.voc_boxes {δ : List Program} {φ : Formula} : (⌈⌈δ⌉⌉φ).voc = δ.pvoc ∪ φ.voc

def LoadFormula.voc (lf : LoadFormula) : Vocab

Equations

• lf.voc = lf.unload.voc

def NegLoadFormula.voc (nlf : NegLoadFormula) : Vocab

Equations

• nlf.voc = (negUnload nlf).voc

def testsOfProgram : Program → List Formula

Test(α)

Equations

• testsOfProgram (·a) = []
• testsOfProgram (?'τ) = [τ]
• testsOfProgram (α;'β) = testsOfProgram α ++ testsOfProgram β
• testsOfProgram (α⋓β) = testsOfProgram α ++ testsOfProgram β
• testsOfProgram (∗α) = testsOfProgram α

def subprograms : Program → List Program

Prog(α)

Equations

• subprograms (·a) = [·a]
• subprograms (?'τ) = [?'τ]
• subprograms (α;'β) = [α;'β] ++ subprograms α ++ subprograms β
• subprograms (α⋓β) = [α⋓β] ++ subprograms α ++ subprograms β
• subprograms (∗α) = [∗α] ++ subprograms α

@[simp]

theorem subprograms.refl {α : Program} : α ∈ subprograms α

theorem subprograms_voc {α β : Program} : β ∈ subprograms α → β.voc ⊆ α.voc

theorem testsOfProgram.voc (α : Program) {τ : Formula} (τ_in : τ ∈ testsOfProgram α) : τ.voc ⊆ α.voc

Fresh variables

def freshVarForm : Formula → ℕ

Get a fresh atomic proposition x not occuring in ψ.

Equations

• freshVarForm Formula.bottom = 0
• freshVarForm (·n) = n + 1
• freshVarForm (~φ) = freshVarForm φ
• freshVarForm (φ⋀ψ) = max (freshVarForm φ) (freshVarForm ψ)
• freshVarForm (⌈α⌉φ) = max (freshVarProg α) (freshVarForm φ)

def freshVarProg : Program → ℕ

Get a fresh atomic proposition x not occuring in α.

Equations

• freshVarProg (·n) = 0
• freshVarProg (α;'β) = max (freshVarProg α) (freshVarProg β)
• freshVarProg (α⋓β) = max (freshVarProg α) (freshVarProg β)
• freshVarProg (∗α) = freshVarProg α
• freshVarProg (?'φ) = freshVarForm φ

theorem freshVarForm_is_larger (φ : Formula) (n : ℕ) : n ∈ φ.voc.atomProps → n < freshVarForm φ

theorem freshVarProg_is_larger (α : Program) (n : ℕ) : n ∈ α.voc.atomProps → n < freshVarProg α

theorem freshVarForm_is_fresh (φ : Formula) : Sum.inl (freshVarForm φ) ∉ φ.voc

theorem freshVarProg_is_fresh (α : Program) : Sum.inl (freshVarProg α) ∉ α.voc