MatchingLogic.Localization

def MatchingLogic.localize {S : Signature} {Var : Type} (Γ : Set (Pattern S Var)) : Set (Pattern S Var)

Definition 6 (localization). Δ_Γ := {[p]γ | γ ∈ Γ, p ∈ E*}.

Equations

• MatchingLogic.localize Γ = {ψ : MatchingLogic.Pattern S Var | ∃ γ ∈ Γ, ∃ (p : List (MatchingLogic.Coord S)), ψ = MatchingLogic.boxes p γ}

theorem MatchingLogic.subset_localize {S : Signature} {Var : Type} (Γ : Set (Pattern S Var)) : Γ ⊆ localize Γ

Γ ⊆ Δ_Γ, by taking p = ε.

theorem MatchingLogic.closed_of_mem_localize {S : Signature} {Var : Type} {Γ : Set (Pattern S Var)} (hΓ : ∀ γ ∈ Γ, Closed γ) (ψ : Pattern S Var) : ψ ∈ localize Γ → Closed ψ

Every member of Δ_Γ is closed when every member of Γ is, so ⟦Δ_Γ⟧ is well defined.

theorem MatchingLogic.denoteSet_localize {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (Γ : Set (Pattern S Var)) : M.denoteSet ρ (localize Γ) = {u : M.carrier | ∀ (v : M.carrier), Relation.ReflTransGen M.Step u v → v ∈ M.denoteSet ρ Γ}

Lemma 8. ⟦Δ_Γ⟧ = {u | ⇝*[u] ⊆ ⟦Γ⟧}.

theorem MatchingLogic.backwardClosed_denoteSet_localize {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (Γ : Set (Pattern S Var)) : M.BackwardClosed (M.denoteSet ρ (localize Γ)) ∧ M.denoteSet ρ (localize Γ) ⊆ M.denoteSet ρ Γ

Lemma 8, second half: ⟦Δ_Γ⟧ is backward closed and contained in ⟦Γ⟧.

theorem MatchingLogic.denoteSet_localize_greatest {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (Γ : Set (Pattern S Var)) {U : Set M.carrier} (hU : M.BackwardClosed U) (hUΓ : U ⊆ M.denoteSet ρ Γ) : U ⊆ M.denoteSet ρ (localize Γ)

Lemma 8, third half: it is the largest such set.

theorem MatchingLogic.satSet_localize_iff {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) {Γ : Set (Pattern S Var)} : M.SatSet (localize Γ) ↔ M.SatSet Γ

M ⊨ Γ and M ⊨ Δ_Γ are equivalent: localizing does not change the models. Proved here from Lemma 4 rather than from necessitation.

theorem MatchingLogic.globalCons_of_localCons_localize {S : Signature} {Var : Type} [DecidableEq Var] {Γ : Set (Pattern S Var)} {φ : Pattern S Var} (h : LocalCons (localize Γ) φ) : GlobalCons Γ φ

Lemma 7. If Δ_Γ ⊨loc φ then Γ ⊨ φ.