Theory MSOinHOL_shallow_minimal_locale

theory MSOinHOL_shallow_minimal_locale
  imports MSOinHOL_preliminaries
begin

text ‹Minimal (lightweight) shallow embedding of MSO in HOL, packaged as
  a locale.  Since MSO carries no world dependency, the formula type
  collapses to ‹bool›.›

locale MinS =
  fixes II :: ℐ and gg :: ℰ and GG :: 𝒢
begin

text ‹Six primitive cases.  ‹ExM›, ‹ExM2› are HOL binders over the
  symbol types ‹V›, ‹V2›; atoms consult ‹II› via ‹gg›, and
  membership consults ‹GG› via ‹gg›.›

definition AtmM :: "R ⇒ V ⇒ V ⇒ bool" ("_⇧m'(_,_')")
  where "r⇧m(x,y) ≡ II r (gg x) (gg y)"

definition PrdM :: "V2 ⇒ V ⇒ bool" ("_⇧m'(_')")
  where "X⇧m(x) ≡ (GG X) (gg x)"

definition NegM :: "bool ⇒ bool" ("¬⇧m _" [58] 59)
  where "¬⇧mφ ≡ ¬φ"

definition AndM :: "bool ⇒ bool ⇒ bool" (infixr "∧⇧m" 56)
  where "φ ∧⇧m ψ ≡ φ ∧ ψ"

definition ExM :: "(V ⇒ bool) ⇒ bool" (binder "∃⇧m" 53)
  where "∃⇧md. Φ d ≡ ∃d. Φ d"

definition ExM2 :: "(V2 ⇒ bool) ⇒ bool" (binder "∃⇧m⇩2" 53)
  where "∃⇧m⇩2D. Φ D ≡ ∃D. Φ D"

text ‹Derived connectives.›

definition OrM :: "bool ⇒ bool ⇒ bool" (infixr "∨⇧m" 54)
  where "φ ∨⇧m ψ ≡ ¬⇧m(¬⇧mφ ∧⇧m ¬⇧mψ)"

definition ImpM :: "bool ⇒ bool ⇒ bool" (infixr "⊃⇧m" 55)
  where "φ ⊃⇧m ψ ≡ ¬⇧mφ ∨⇧m ψ"

definition IffM :: "bool ⇒ bool ⇒ bool" (infixr "⟷⇧m" 54)
  where "φ ⟷⇧m ψ ≡ (φ ⊃⇧m ψ) ∧⇧m (ψ ⊃⇧m φ)"

definition AllM :: "(V ⇒ bool) ⇒ bool" (binder "∀⇧m" 53)
  where "∀⇧md. Φ d ≡ ∀d. Φ d"

definition AllM2 :: "(V2 ⇒ bool) ⇒ bool" (binder "∀⇧m⇩2" 53)
  where "∀⇧m⇩2D. Φ D ≡ ∀D. Φ D"

text ‹Relative truth and validity.  As the formula type is ‹bool›,
  validity is the identity.›

definition ValM :: "bool ⇒ bool" ("⊨⇧m _" 9)
  where "⊨⇧m φ ≡ φ"

text ‹Bag of definitions.›

named_theorems DefM
lemmas DefM_defs [DefM] =
  AtmM_def PrdM_def NegM_def AndM_def ExM_def ExM2_def
  OrM_def ImpM_def IffM_def AllM_def AllM2_def ValM_def

end

end