Theory PMLinHOL_shallow_minimal

section‹Shallow embedding of PML in HOL (minimal)\label{sec:pmlinhol_shallow_min}›

theory PMLinHOL_shallow_minimal (* Christoph Benzmüller, 2025 *)
imports PMLinHOL_preliminaries
begin

―‹The acessibility relation R and the valuation function V are introduced as constants at the meta-level HOL›
consts R::ℛ V::𝒱

―‹Shallow embedding (of propositional modal logic in HOL)›
type_synonym σ = "𝗐⇒bool"
definition AtmM::"𝒮⇒σ" ("_⇧^m") where "a⇧^m ≡ λw. V a w"
definition NegM::"σ⇒σ" ("¬⇧^m") where "¬⇧^m φ ≡ λw.¬φ w"
definition ImpM::"σ⇒σ⇒σ" (infixr "⊃⇧^m" 93) where "φ ⊃⇧^m ψ ≡ λw. φ w ⟶ ψ w"
definition BoxM::"σ⇒σ" ("□⇧^m") where "□⇧^m φ ≡ λw. ∀v. R w v ⟶ φ v" 

―‹Further logical connectives as definitions›
definition OrM (infixr "∨⇧^m" 92) where "φ ∨⇧^m ψ ≡ ¬⇧^mφ ⊃⇧^m ψ"
definition AndM (infixr "∧⇧^m" 95) where "φ ∧⇧^m ψ ≡ ¬⇧^m(φ ⊃⇧^m ¬⇧^mψ)"
definition DiaM ("◇⇧^m_") where "◇⇧^mφ ≡ ¬⇧^m (□⇧^m (¬⇧^mφ)) "
definition TopM ("⊤⇧^m") where "⊤⇧^m ≡ p⇧^m ⊃⇧^m p⇧^m"
definition BotM ("⊥⇧^m") where "⊥⇧^m ≡ ¬⇧^m ⊤⇧^m"

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

―‹Definition of validity›
definition ValM ("⊨⇧^m _") where "⊨⇧^m φ ≡ ∀w::𝗐. w ⊨⇧^m φ"

―‹Collection of definitions in a bag called DefM›
named_theorems DefM declare AtmM_def[DefM,simp] NegM_def[DefM,simp] ImpM_def[DefM,simp] BoxM_def[DefM,simp] OrM_def[DefM,simp] AndM_def[DefM,simp] DiaM_def[DefM,simp] TopM_def[DefM,simp] BotM_def[DefM,simp] RelativeTruthM_def[DefM,simp] ValM_def[DefM,simp]
end