Theory PMLinHOL_deep

section‹Deep embedding of PML in HOL\label{sec:pmlinhol_deep}›

theory PMLinHOL_deep              
 imports PMLinHOL_preliminaries    
begin 
―‹Deep embedding (of propositional modal logic in HOL)›
datatype PML = AtmD 𝒮 ("_⇧d") | NotD PML ("¬⇧d") | ImpD PML PML (infixr "⊃⇧d" 93) | BoxD PML ("□⇧d")

―‹Further logical connectives as definitions›
definition OrD (infixr "∨⇧d" 92) where "φ∨⇧dψ ≡ ¬⇧dφ ⊃⇧d ψ"
definition AndD (infixr "∧⇧d" 95) where "φ∧⇧dψ ≡ ¬⇧d(φ ⊃⇧d ¬⇧dψ)"
definition DiaD ("◇⇧d_") where "◇⇧dφ ≡ ¬⇧d(□⇧d(¬⇧dφ)) "
definition TopD ("⊤⇧d") where "⊤⇧d ≡ p⇧d ⊃⇧d p⇧d"
definition BotD ("⊥⇧d") where "⊥⇧d ≡ ¬⇧d ⊤⇧d"

―‹Definition of truth of a formula relative to a model ‹⟨W,R,V⟩› and possible world w›
primrec RelativeTruthD :: "𝒲⇒ℛ⇒𝒱⇒𝗐⇒PML⇒bool" ("⟨_,_,_⟩,_ ⊨⇧d _") where
    "⟨W,R,V⟩, w ⊨⇧d a⇧d  = (V a w)" 
  | "⟨W,R,V⟩, w ⊨⇧d ¬⇧dφ = (¬ ⟨W,R,V⟩, w ⊨⇧d φ)"
  | "⟨W,R,V⟩, w ⊨⇧d φ ⊃⇧d ψ = (⟨W,R,V⟩, w ⊨⇧d φ ⟶ ⟨W,R,V⟩, w ⊨⇧d ψ)"
  | "⟨W,R,V⟩, w ⊨⇧d □⇧dφ = (∀v:W. R w v ⟶ ⟨W,R,V⟩, v ⊨⇧d φ)"

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

―‹Collection of definitions in a bag called DefD›
named_theorems DefD declare OrD_def[DefD,simp] AndD_def[DefD,simp] DiaD_def[DefD,simp] TopD_def[DefD,simp] BotD_def[DefD,simp] RelativeTruthD_def[DefD,simp] ValD_def[DefD,simp]
end