Theory MSOinHOL_preliminaries

theory MSOinHOL_preliminaries
  imports Main
begin

text ‹Some global settings.›

nitpick_params [user_axioms, expect = genuine]

text ‹Declarations shared between the deep, maximal-shallow, and
  minimal-shallow embeddings of MSO in HOL.›

typedecl D                                                       ―‹Domain of individuals.›
type_synonym R   = nat                                  ―‹Binary relation symbols.›
type_synonym V   = nat                              ―‹First-order variable symbols.›
type_synonym V2  = nat                              ―‹Second-order variable symbols.›
type_synonym ℛ   = "D ⇒ D ⇒ bool"            ―‹Binary relations on individuals.›
type_synonym ℐ   = "R ⇒ ℛ"                    ―‹Interpretations of relation symbols.›
type_synonym ℰ   = "V ⇒ D"                    ―‹First-order variable assignments.›
type_synonym 𝒢   = "V2 ⇒ (D ⇒ bool)"    ―‹Second-order variable assignments.›
type_synonym 𝒟   = "D ⇒ bool"                       ―‹First-order domain restrictions.›
type_synonym 𝒫   = "(D ⇒ bool) ⇒ bool"       ―‹Second-order domain restrictions.›

text ‹Pointwise update of first-order variable assignments.›

definition EnvMod :: "ℰ ⇒ V ⇒ D ⇒ ℰ"  ("_[_ ← _]" [110,0,0] 110)
  where "g[x←d] ≡ λz. if z = x then d else g z"

text ‹Pointwise update of second-order variable assignments
  (distinct notation, angle brackets).›

definition SetMod :: "𝒢 ⇒ V2 ⇒ (D ⇒ bool) ⇒ 𝒢"
    ("_⟨_ ← _⟩" [110,0,0] 110)
  where "G⟨X←S⟩ ≡ λZ. if Z = X then S else G Z"

text ‹Standard lemmas about first-order variable-assignment update.›

lemma L1 [simp]: "x ≠ y ⟹ (g[y←d]) x = g x"
  by (simp add: EnvMod_def)

lemma L2: "a ≠ c ⟹ g[a←d⇩1][c←d⇩2] = g[c←d⇩2][a←d⇩1]"
  by (auto simp: EnvMod_def)

lemma L3 [simp]: "(g[a←d]) a = d"
  by (simp add: EnvMod_def)

lemma L4 [simp]: "g[a←d⇩1][a←d⇩2] = g[a←d⇩2]"
  by (auto simp: EnvMod_def)

text ‹Standard lemmas about second-order variable-assignment update.›

lemma M1 [simp]: "X ≠ Y ⟹ (G⟨Y←S⟩) X = G X"
  by (simp add: SetMod_def)

lemma M2: "A ≠ C ⟹ G⟨A←S⇩1⟩⟨C←S⇩2⟩ = G⟨C←S⇩2⟩⟨A←S⇩1⟩"
  by (auto simp: SetMod_def)

lemma M3 [simp]: "(G⟨A←S⟩) A = S"
  by (simp add: SetMod_def)

lemma M4 [simp]: "G⟨A←S⇩1⟩⟨A←S⇩2⟩ = G⟨A←S⇩2⟩"
  by (auto simp: SetMod_def)

text ‹Bounded quantifiers: ‹∀x:D. φ› stands for ‹∀x. D x ⟶ φ x› and
  ‹∃x:D. φ› stands for ‹∃x. D x ∧ φ x›.›

abbreviation "BAll D φ ≡ ∀x. D x ⟶ φ x"
syntax "BAll" :: "pttrn ⇒ logic ⇒ bool ⇒ bool"
    ("(3∀(_/:_)./_)" [0,0,10] 10)
translations "∀x:D. φ" ⇌ "CONST BAll D (λx. φ)"

abbreviation "BEx D φ ≡ ∃x. D x ∧ φ x"
syntax "BEx" :: "pttrn ⇒ logic ⇒ bool ⇒ bool"
    ("(3∃(_/:_)./_)" [0,0,10] 10)
translations "∃x:D. φ" ⇌ "CONST BEx D (λx. φ)"

text ‹Set-as-predicate operations, range, and the universal domain
  (polymorphic; used for both sorts).›

abbreviation "Into" (infix "into" 100)
  where "f into D ≡ ∀x. D (f x)"

abbreviation "Range"
  where "Range f ≡ λx. ∃y. x = f y"

abbreviation "Onto" (infix "onto" 100)
  where "f onto D ≡ D = Range f"

abbreviation "Subset" (infix "❙⊆" 100)
  where "A ❙⊆ B ≡ ∀x. A x ⟶ B x"

abbreviation "Union" (infixl "❙∪" 110)
  where "A ❙∪ B ≡ λx. A x ∨ B x"

abbreviation "Univ"
  where "Univ ≡ λx. True"

text ‹Surjectivity onto the universal predicate coincides with HOL
  surjectivity.›

lemma onto_Univ: "surj f = (f onto Univ)"
  by (auto simp: surj_def fun_eq_iff)

text ‹Backward implication; useful for stating equivalences in two
  directions.›

abbreviation Bimp (infixr "⟵" 50)
  where "φ ⟵ ψ ≡ ψ ⟶ φ"

end