Theory MSOinHOL_shallow

theory MSOinHOL_shallow
  imports MSOinHOL_preliminaries
begin

text ‹Maximal (heavyweight) shallow embedding of MSO in HOL; MSO formulas
  are HOL terms of the following type ‹σ›.›

type_synonym σ = "ℐ ⇒ 𝒟 ⇒ 𝒫 ⇒ ℰ ⇒ 𝒢 ⇒ bool"

text ‹The six primitive cases.›

definition AtmS :: "R ⇒ V ⇒ V ⇒ σ" ("_⇧^s'(_,_')")
  where "r⇧^s(x,y) ≡ λI D E g G. I r (g x) (g y)"

definition PrdS :: "V2 ⇒ V ⇒ σ" ("_⇧^s'(_')")
  where "X⇧^s(x) ≡ λI D E g G. (G X) (g x)"

definition NegS :: "σ ⇒ σ" ("¬⇧^s _" [58] 59)
  where "¬⇧^sφ ≡ λI D E g G. ¬ (φ I D E g G)"

definition AndS :: "σ ⇒ σ ⇒ σ" (infixr "∧⇧^s" 56)
  where "φ ∧⇧^s ψ ≡ λI D E g G. φ I D E g G ∧ ψ I D E g G"

definition ExS :: "V ⇒ σ ⇒ σ" ("∃⇧^s_. _" 53)
  where "∃⇧^sx. φ ≡ λI D E g G. ∃d:D. φ I D E (g[x←d]) G"

definition ExS2 :: "V2 ⇒ σ ⇒ σ" ("∃⇧^s⇩₂_. _" 53)
  where "∃⇧^s⇩₂X. φ ≡ λI D E g G. ∃S:E. φ I D E g (G⟨X←S⟩)"

text ‹Derived connectives.›

definition OrS :: "σ ⇒ σ ⇒ σ" (infixr "∨⇧^s" 54)
  where "φ ∨⇧^s ψ ≡ ¬⇧^s(¬⇧^sφ ∧⇧^s ¬⇧^sψ)"

definition ImpS :: "σ ⇒ σ ⇒ σ" (infixr "⊃⇧^s" 55)
  where "φ ⊃⇧^s ψ ≡ ¬⇧^sφ ∨⇧^s ψ"

definition IffS :: "σ ⇒ σ ⇒ σ" (infixr "⟷⇧^s" 54)
  where "φ ⟷⇧^s ψ ≡ (φ ⊃⇧^s ψ) ∧⇧^s (ψ ⊃⇧^s φ)"

definition AllS :: "V ⇒ σ ⇒ σ" ("∀⇧^s_. _" 53)
  where "∀⇧^sx. φ ≡ ¬⇧^s(∃⇧^sx. ¬⇧^sφ)"

definition AllS2 :: "V2 ⇒ σ ⇒ σ" ("∀⇧^s⇩₂_. _" 53)
  where "∀⇧^s⇩₂X. φ ≡ ¬⇧^s(∃⇧^s⇩₂X. ¬⇧^sφ)"

text ‹Relative truth and validity (mirroring the deep embedding).›

definition RelTruthS :: "ℐ ⇒ 𝒟 ⇒ 𝒫 ⇒ ℰ ⇒ 𝒢 ⇒ σ ⇒ bool"
    ("⟨_,_,_⟩,_,_ ⊨⇧^s _" [100,0,0,0,0] 100)
  where "⟨I,D,E⟩,g,G ⊨⇧^s φ ≡ φ I D E g G"

definition ValS :: "σ ⇒ bool" ("⊨⇧^s _" 9)
  where "⊨⇧^s φ ≡ ∀I D E g G. g into D ⟶ G into E ⟶ ⟨I,D,E⟩,g,G ⊨⇧^s φ"

text ‹Auxiliary ``full-domain'' notion of validity: assignments range over
  the full types.›

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

text ‹General validity implies full-domain validity.›

lemma Val_s: "⊨⇧^s φ ⟹ ⊨⇧^s' φ"
  using ValS'_def ValS_def by simp

text ‹Bag of definitions.›

named_theorems DefS
lemmas DefS_defs [DefS] =
  AtmS_def PrdS_def NegS_def AndS_def ExS_def ExS2_def
  OrS_def ImpS_def IffS_def AllS_def AllS2_def
  RelTruthS_def ValS_def ValS'_def

end