Theory PMLinHOL_shallow

section‹Shallow embedding of PML in HOL (maximal)\label{sec:pmlinhol_shallow_max}›
 
theory PMLinHOL_shallow    (* Christoph Benzmüller, 2025 *)
  imports PMLinHOL_preliminaries 
begin

―‹Shallow embedding (of propositional modal logic in HOL)›
type_synonym σ = "𝒲⇒ℛ⇒𝒱⇒𝗐⇒bool"
definition AtmS::"𝒮⇒σ" ("_⇧^s") where "a⇧^s ≡ λW R V w. V a w"
definition NegS::"σ⇒σ" ("¬⇧^s") where "¬⇧^s φ ≡ λW R V w. ¬(φ W R V w)"
definition ImpS::"σ⇒σ⇒σ" (infixr "⊃⇧^s" 93) where "φ ⊃⇧^s ψ ≡ λW R V w. (φ W R V w) ⟶ (ψ W R V w)"
definition BoxS::"σ⇒σ" ("□⇧^s") where "□⇧^s φ ≡ λW R V w. ∀v:W. R w v ⟶ (φ W R V v)" 

―‹Further logical connectives as definitions›
definition OrS (infixr "∨⇧^s" 92) where "φ ∨⇧^s ψ ≡ ¬⇧^sφ ⊃⇧^s ψ"
definition AndS (infixr "∧⇧^s" 95) where "φ ∧⇧^s ψ ≡ ¬⇧^s(φ ⊃⇧^s ¬⇧^sψ)"
definition DiaS ("◇⇧^s") where "◇⇧^sφ ≡ ¬⇧^s (□⇧^s (¬⇧^sφ)) "
definition TopS ("⊤⇧^s") where "⊤⇧^s ≡p⇧^s ⊃⇧^s p⇧^s"
definition BotS ("⊥⇧^s") where "⊥⇧^s ≡ ¬⇧^s ⊤⇧^s"

―‹Definition of truth of a formula relative to a model ‹⟨W,R,V⟩› and possible world w›
definition RelativeTruthS::"𝒲⇒ℛ⇒𝒱⇒𝗐⇒σ⇒bool" ("⟨_,_,_⟩,_⊨⇧^s _") where "⟨W,R,V⟩,w ⊨⇧^s φ ≡ φ W R V w"

―‹Definition of validity›
definition ValS ("⊨⇧^s _") where "⊨⇧^s φ ≡ ∀W R V. ∀w:W. ⟨W,R,V⟩,w ⊨⇧^s φ"

―‹Collection of definitions in a bag called DefS›
named_theorems DefS declare AtmS_def[DefS,simp] NegS_def[DefS,simp] ImpS_def[DefS,simp] BoxS_def[DefS,simp] OrS_def[DefS,simp] AndS_def[DefS,simp] DiaS_def[DefS,simp] TopS_def[DefS,simp] BotS_def[DefS,simp] RelativeTruthS_def[DefS,simp] ValS_def[DefS,simp]
end