Theory ModalFilter

subsection‹ModalFilter.thy (Figure 5 of \cite{J75})›
text‹Set filter and ultrafilter formalized for our modal logic setting.›
theory ModalFilter imports HOMLinHOL
begin 

type_synonym τ="e⇒σ"
abbreviation Element::"τ⇒(τ⇒σ)⇒σ" (infix "❙∈" 90) where "φ❙∈S ≡ S φ"
abbreviation EmptySet::τ ("❙∅") where "❙∅ ≡ λx. ❙⊥" 
abbreviation UniversalSet::τ ("❙U") where "❙U ≡ λx. ❙⊤"
abbreviation Subset::"τ⇒τ⇒σ" (infix "❙⊆" 80) 
  where "φ❙⊆ψ ≡ ❙∀x.((φ x) ❙⊃ (ψ x))"
abbreviation SubsetE::"τ⇒τ⇒σ" (infix "❙⊆⇧E" 80) 
  where "φ❙⊆⇧Eψ ≡ ❙∀⇧Ex.((φ x) ❙⊃ (ψ x))"
abbreviation Intersection::"τ⇒τ⇒τ" (infix "❙⊓" 91) 
  where "φ❙⊓ψ ≡ λx.((φ x) ❙∧ (ψ x))"
abbreviation Inverse::"τ⇒τ" ("¯") 
  where "¯ψ ≡ λx. ❙¬(ψ x)" 
abbreviation "Filter Φ ≡ ❙U❙∈Φ ❙∧ ❙¬(❙∅❙∈Φ) ❙∧
  (❙∀φ ψ. φ❙∈Φ ❙∧ φ❙⊆⇧Eψ ❙⊃ ψ❙∈Φ) ❙∧ (❙∀φ ψ. φ❙∈Φ ❙∧ ψ❙∈Φ ❙⊃ φ❙⊓ψ❙∈Φ)"
abbreviation "UFilter Φ ≡ Filter Φ ❙∧ (❙∀φ. φ❙∈Φ ❙∨ (¯φ)❙∈Φ)"
abbreviation "FilterP Φ ≡ ❙U❙∈Φ ❙∧ ❙¬(❙∅❙∈Φ) ❙∧ (❙∀φ ψ. φ❙∈Φ ❙∧ φ❙⊆ψ ❙⊃ ψ❙∈Φ) ❙∧
  (❙∀φ ψ. φ❙∈Φ ❙∧ ψ❙∈Φ ❙⊃ φ❙⊓ψ❙∈Φ)"
abbreviation "UFilterP Φ ≡ FilterP Φ ❙∧ (❙∀φ. φ❙∈Φ ❙∨ (¯φ)❙∈Φ)"

end