Fischer-Ladner Closure

Here we define a closure on sets of formulas. Our main reference for this closure is Section 6.1 of [HKT2000] See also Definition 4.79 and Exercise 4.8.2 in [BRV2001]. An alternative version following the proof of Theorem 3.2 in [FL1979] but unfinished is in Unused/FischerLadnerViaPreForms.lean.

• [FL1979] Michael J. Fischer and Richard E. Ladner (1979): Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, vol 18, no 2, pp. 194--211. https://doi.org/10.1016/0022-0000(79)90046-1

• [BRV2001] Patrick Blackburn, Maarten de Rijke and Yde Venema (2001): Modal Logic. Cambridge University Press. https://www.mlbook.org/

• [HKT2000] David Harel, Dexter Kozen, and Jerzy Tiuryn (2000): Dynamic Logic. MIT Press, 2000.

Definition

def FL : Formula → List Formula

The Fischer-Ladner closure of a formula. See Section 6.1 of [HKT2000]. Note that there only implication is given. For our Formula type we also need to cover conjunction and negation. The main work is done by FLb, which also ensures termination.

Equations

• FL Formula.bottom = [⊥]
• FL (·p) = [·p]
• FL (φ⋀ψ) = [φ⋀ψ] ++ FL φ ++ FL ψ
• FL (⌈α⌉φ) = FLb α φ ++ FL φ
• FL (~φ) = [~φ] ++ FL φ

def FLb : Program → Formula → List Formula

The Fischer-Ladner closure of a box formula, not recursing into the formula after the box.

Equations

• FLb (·a) x✝ = [⌈·a⌉x✝]
• FLb (α⋓β) x✝ = [⌈α⋓β⌉x✝] ++ FLb α x✝ ++ FLb β x✝
• FLb (α;'β) x✝ = [⌈α;'β⌉x✝] ++ FLb α (⌈β⌉x✝) ++ FLb β x✝
• FLb (∗α) x✝ = [⌈∗α⌉x✝] ++ FLb α (⌈∗α⌉x✝)
• FLb (?'τ) x✝ = [⌈?'τ⌉x✝] ++ FL τ

Lemmas

@[simp]

theorem FL_refl {φ : Formula} : φ ∈ FL φ

@[simp]

theorem FLb_refl {α : Program} {φ : Formula} : (⌈α⌉φ) ∈ FLb α φ

theorem FL_trans {φ ψ : Formula} : ψ ∈ FL φ → FL ψ ⊆ FL φ

Lemma 6.1(i) from [HKT2000]

theorem FLb_trans {α : Program} {φ ψ : Formula} : ψ ∈ FLb α φ → FL ψ ⊆ FLb α φ ++ FL φ

Lemma 6.1(ii) from [HKT2000]

theorem FL_box_sub {φ : Formula} {α : Program} {ψ : Formula} : (⌈α⌉ψ) ∈ FL φ → ψ ∈ FL φ

theorem FL_box_test {φ τ ψ : Formula} : (⌈?'τ⌉ψ) ∈ FL φ → τ ∈ FL φ

theorem FL_box_cup {φ : Formula} {α β : Program} {ψ : Formula} : (⌈α⋓β⌉ψ) ∈ FL φ → (⌈α⌉ψ) ∈ FL φ ∧ (⌈β⌉ψ) ∈ FL φ

theorem FL_box_seq {φ : Formula} {α β : Program} {ψ : Formula} : (⌈α;'β⌉ψ) ∈ FL φ → (⌈α⌉⌈β⌉ψ) ∈ FL φ ∧ (⌈β⌉ψ) ∈ FL φ

theorem FL_box_star {φ : Formula} {α : Program} {ψ : Formula} : (⌈∗α⌉ψ) ∈ FL φ → (⌈α⌉⌈∗α⌉ψ) ∈ FL φ

def FLL (L : List Formula) : List Formula

Equations

• FLL L = List.flatMap FL L

@[simp]

theorem FLL_refl_sub {L : List Formula} : L ⊆ FLL L

theorem FLL_sub {L1 L2 : List Formula} : L1 ⊆ L2 → FLL L1 ⊆ FLL L2

@[simp]

theorem FLL_idem_ext {L : List Formula} {φ : Formula} : φ ∈ FLL (FLL L) → φ ∈ FLL L

theorem FLL_sub_FLL_iff_sub_FLL {L K : List Formula} : L ⊆ FLL K ↔ FLL L ⊆ FLL K

theorem FLL_append_eq {L K : List Formula} : FLL (L ++ K) = FLL L ++ FLL K

theorem FLL_ext {L1 L2 : List Formula} (h : ∀ (φ : Formula), φ ∈ L1 ↔ φ ∈ L2) (φ : Formula) : φ ∈ FLL L1 ↔ φ ∈ FLL L2

Being a member of the FL closure of a list does not depend on the position.

FL stays in the Vocabulary

theorem FL_stays_in_voc {φ ψ : Formula} (ψ_in_FL : ψ ∈ FL φ) : ψ.voc ⊆ φ.voc

theorem FLb_stays_in_voc {α : Program} {φ ψ : Formula} (ψ_in_FLb : ψ ∈ FLb α φ) : ψ.voc ⊆ α.voc ∪ φ.voc