Theory MSOinHOL_deep

theory MSOinHOL_deep
  imports MSOinHOL_preliminaries
begin

text ‹Deep embedding of monadic second-order logic (MSO) in HOL.›

text ‹Two binders: ‹∃⇧^d› ranges over individuals;
  ‹∃⇧^d⇩₂› ranges over monadic predicates.
  ‹X⇧^d(x)› is the monadic predication atom ``predicate ‹X›
  holds of individual ‹x›''.›

datatype ℱ =
    AtmD R V V    ("_⇧^d'(_,_')")                       ―‹relational atom ‹r(x,y)››
  | PrdD V2 V     ("_⇧^d'(_')")                         ―‹monadic predication atom ‹X(x)››
  | NegD ℱ       ("¬⇧^d _" [58] 59)                    ―‹negation›
  | AndD ℱ ℱ     (infixr "∧⇧^d" 56)                 ―‹conjunction›
  | ExD V ℱ      ("∃⇧^d_. _")                          ―‹first-order existential›
  | ExD2 V2 ℱ    ("∃⇧^d⇩₂_. _")                          ―‹second-order (monadic) existential›

text ‹Further connectives as derived definitions.›

definition OrD (infixr "∨⇧^d" 54)
  where "φ ∨⇧^d ψ ≡ ¬⇧^d(¬⇧^dφ ∧⇧^d ¬⇧^dψ)"

definition ImpD (infixr "⊃⇧^d" 55)
  where "φ ⊃⇧^d ψ ≡ ¬⇧^dφ ∨⇧^d ψ"

definition IffD (infixr "⟷⇧^d" 54)
  where "φ ⟷⇧^d ψ ≡ (φ ⊃⇧^d ψ) ∧⇧^d (ψ ⊃⇧^d φ)"

definition AllD ("∀⇧^d_. _")
  where "∀⇧^dx. φ ≡ ¬⇧^d(∃⇧^dx. ¬⇧^dφ)"

definition AllD2 ("∀⇧^d⇩₂_. _")
  where "∀⇧^d⇩₂X. φ ≡ ¬⇧^d(∃⇧^d⇩₂X. ¬⇧^dφ)"

text ‹Relative truth in a model.  The first-order existential ranges over the
  individual domain ‹D›; the second-order existential ranges over the
  collection ‹E› of admissible monadic sets.›

primrec RelativeTruthD :: "ℐ ⇒ 𝒟 ⇒ 𝒫 ⇒ ℰ ⇒ 𝒢 ⇒ ℱ ⇒ bool"
    ("⟨_,_,_⟩,_,_ ⊨⇧^d _" [10,10,10,10,10] 100)
  where
    "⟨I,D,E⟩,g,G ⊨⇧^d (r⇧^d(x,y)) = I r (g x) (g y)"
  | "⟨I,D,E⟩,g,G ⊨⇧^d (X⇧^d(x)) = (G X) (g x)"
  | "⟨I,D,E⟩,g,G ⊨⇧^d (¬⇧^dφ) = (¬ ⟨I,D,E⟩,g,G ⊨⇧^d φ)"
  | "⟨I,D,E⟩,g,G ⊨⇧^d (φ ∧⇧^d ψ) = (⟨I,D,E⟩,g,G ⊨⇧^d φ ∧ ⟨I,D,E⟩,g,G ⊨⇧^d ψ)"
  | "⟨I,D,E⟩,g,G ⊨⇧^d (∃⇧^dx. φ) = (∃d:D. ⟨I,D,E⟩,g[x←d],G ⊨⇧^d φ)"
  | "⟨I,D,E⟩,g,G ⊨⇧^d (∃⇧^d⇩₂X. φ) = (∃S:E. ⟨I,D,E⟩,g,G⟨X←S⟩ ⊨⇧^d φ)"

text ‹Validity: true in every model, every domain-respecting first- and
  second-order assignment.›

definition ValD ("⊨⇧^d _" 9)
  where "⊨⇧^d φ ≡ ∀I D E g G. g into D ⟶ G into E ⟶ ⟨I,D,E⟩,g,G ⊨⇧^d φ"

text ‹Auxiliary ``full-domain'' notion of validity: assignments range over
  the full types (‹Univ› on ‹D› and on ‹D ⇒ bool›).›

definition ValD' ("⊨⇧^d'' _" 9)
  where "⊨⇧^d' φ ≡ ∀I g G. ⟨I,Univ,Univ⟩,g,G ⊨⇧^d φ"

text ‹General validity implies full-domain validity.›

lemma Val: "⊨⇧^d φ ⟹ ⊨⇧^d' φ"
  using ValD'_def ValD_def by simp

text ‹Bag of definitions for collective unfolding.›

named_theorems DefD
lemmas [DefD] = OrD_def ImpD_def IffD_def AllD_def AllD2_def ValD_def ValD'_def

end