Theory MSOinHOL_experiments_extra

theory MSOinHOL_experiments_extra
  imports
    MSOinHOL_deep
    MSOinHOL_shallow
    MSOinHOL_shallow_minimal
begin

text ‹Additional MSO landmarks complementing the experiments in
  @{text MSOinHOL_experiments_classic}: 3-colorability, vertex cover,
  transitivity, symmetry and triangle existence, each replicated across
  the deep, maximal-shallow and minimal-shallow embeddings.›

abbreviation "(x::V) ≡ 1"
abbreviation "(y::V) ≡ 2"
abbreviation "(z::V) ≡ 3"
abbreviation "(u::V) ≡ 4"
abbreviation "(v::V) ≡ 5"
abbreviation "(X::V2) ≡ 1"
abbreviation "(Y::V2) ≡ 2"
abbreviation "(Z::V2) ≡ 3"

consts P :: R

subsubsection ‹Deep embedding (under @{text "⊨⇧d'"})›

text ‹3-colorability (Thomas 1997): refuted on @{text ‹K⇩4›}
  (the complete graph on four vertices, which needs four colors).
  Generalisation of @{text two_colorability_not_valid_d}.›

lemma three_colorability_not_valid_d:
  "⊨⇧d' (∃⇧d⇩2X. ∃⇧d⇩2Y. ∃⇧d⇩2Z. ((∀⇧du. (X⇧d(u) ∨⇧d Y⇧d(u) ∨⇧d Z⇧d(u))) ∧⇧d (∀⇧du. ∀⇧dv. (P⇧d(u,v) ⊃⇧d ((¬⇧d (X⇧d(u) ∧⇧d X⇧d(v))) ∧⇧d (¬⇧d (Y⇧d(u) ∧⇧d Y⇧d(v))) ∧⇧d (¬⇧d (Z⇧d(u) ∧⇧d Z⇧d(v))))))))"
  unfolding DefD apply simp nitpick oops

text ‹Vertex cover existence: the predicate @{text Univ} is a witness, so
  the schema is universally valid.›

lemma vertex_cover_valid_d:
  "⊨⇧d' (∃⇧d⇩2X. ∀⇧du. ∀⇧dv. (P⇧d(u,v) ⊃⇧d (X⇧d(u) ∨⇧d X⇧d(v))))"
  unfolding DefD
  apply (intro allI, simp add: SetMod_def EnvMod_def)
  by (rule exI[of _ "Univ"]) (auto simp: SetMod_def EnvMod_def)

text ‹Transitivity of @{text P}: not universally valid; refuted by any
  3-path @{text ‹a → b → c›} without the closing edge @{text ‹a → c›}.›

lemma transitivity_not_valid_d:
  "⊨⇧d' (∀⇧dx. ∀⇧dy. ∀⇧dz. (P⇧d(x,y) ⊃⇧d (P⇧d(y,z) ⊃⇧d P⇧d(x,z))))"
  unfolding DefD apply simp nitpick oops

text ‹Symmetric extension: stating @{text P} is symmetric is also not
  universally valid; refuted by any directed edge without its converse.›

lemma symmetry_not_valid_d:
  "⊨⇧d' (∀⇧dx. ∀⇧dy. (P⇧d(x,y) ⊃⇧d P⇧d(y,x)))"
  unfolding DefD apply simp nitpick oops

text ‹Existence of a triangle: not universally valid; refuted on any
  triangle-free graph (e.g. the empty graph).›

lemma triangle_exists_not_valid_d:
  "⊨⇧d' (∃⇧dx. ∃⇧dy. ∃⇧dz. (P⇧d(x,y) ∧⇧d P⇧d(y,z) ∧⇧d P⇧d(x,z)))"
  unfolding DefD apply simp nitpick oops

text ‹Existence of an edge: refuted on the empty graph.›

lemma has_edge_not_valid_d:
  "⊨⇧d' (∃⇧dx. ∃⇧dy. P⇧d(x,y))"
  unfolding DefD apply simp nitpick oops

text ‹Loop-freeness: stating @{text P} has no self-loops is refuted by any
  graph with a fixed point.›

lemma loop_free_not_valid_d:
  "⊨⇧d' (∀⇧dx. ¬⇧d P⇧d(x,x))"
  unfolding DefD apply simp nitpick oops

subsubsection ‹Maximal-shallow embedding (under @{text "⊨⇧s'"})›

lemma three_colorability_not_valid_s:
  "⊨⇧s' (∃⇧s⇩2X. ∃⇧s⇩2Y. ∃⇧s⇩2Z. ((∀⇧su. (X⇧s(u) ∨⇧s Y⇧s(u) ∨⇧s Z⇧s(u))) ∧⇧s (∀⇧su. ∀⇧sv. (P⇧s(u,v) ⊃⇧s ((¬⇧s (X⇧s(u) ∧⇧s X⇧s(v))) ∧⇧s (¬⇧s (Y⇧s(u) ∧⇧s Y⇧s(v))) ∧⇧s (¬⇧s (Z⇧s(u) ∧⇧s Z⇧s(v))))))))"
  unfolding DefS apply (intro allI) apply simp nitpick oops

lemma vertex_cover_valid_s:
  "⊨⇧s' (∃⇧s⇩2X. ∀⇧su. ∀⇧sv. (P⇧s(u,v) ⊃⇧s (X⇧s(u) ∨⇧s X⇧s(v))))"
  unfolding DefS
  apply (intro allI, simp)
  by (rule exI[of _ "Univ"]) auto

lemma transitivity_not_valid_s:
  "⊨⇧s' (∀⇧sx. ∀⇧sy. ∀⇧sz. (P⇧s(x,y) ⊃⇧s (P⇧s(y,z) ⊃⇧s P⇧s(x,z))))"
  unfolding DefS apply (intro allI) apply simp nitpick oops

lemma symmetry_not_valid_s:
  "⊨⇧s' (∀⇧sx. ∀⇧sy. (P⇧s(x,y) ⊃⇧s P⇧s(y,x)))"
  unfolding DefS apply (intro allI) apply simp nitpick oops

lemma triangle_exists_not_valid_s:
  "⊨⇧s' (∃⇧sx. ∃⇧sy. ∃⇧sz. (P⇧s(x,y) ∧⇧s P⇧s(y,z) ∧⇧s P⇧s(x,z)))"
  unfolding DefS apply (intro allI) apply simp nitpick oops

lemma has_edge_not_valid_s:
  "⊨⇧s' (∃⇧sx. ∃⇧sy. P⇧s(x,y))"
  unfolding DefS apply (intro allI) apply simp nitpick oops

lemma loop_free_not_valid_s:
  "⊨⇧s' (∀⇧sx. ¬⇧s P⇧s(x,x))"
  unfolding DefS apply (intro allI) apply simp nitpick oops

subsubsection ‹Minimal-shallow embedding (under @{text "⊨⇧m"})›

text ‹In the minimal embedding the second-order existential ranges over
  the (countable) assignment range, so even formulae that hold under the
  full second-order domain (such as vertex cover) need not hold here.
  @{text nitpick} can certify a POTENTIAL countermodel only.›

lemma three_colorability_not_valid_m:
  "⊨⇧m (∃⇧m⇩2X. ∃⇧m⇩2Y. ∃⇧m⇩2Z. ((∀⇧mu. (X⇧m(u) ∨⇧m Y⇧m(u) ∨⇧m Z⇧m(u))) ∧⇧m (∀⇧mu. ∀⇧mv. (P⇧m(u,v) ⊃⇧m ((¬⇧m (X⇧m(u) ∧⇧m X⇧m(v))) ∧⇧m (¬⇧m (Y⇧m(u) ∧⇧m Y⇧m(v))) ∧⇧m (¬⇧m (Z⇧m(u) ∧⇧m Z⇧m(v))))))))"
  unfolding DefM nitpick[expect=potential] oops

lemma vertex_cover_not_valid_m:
  "⊨⇧m (∃⇧m⇩2X. ∀⇧mu. ∀⇧mv. (P⇧m(u,v) ⊃⇧m (X⇧m(u) ∨⇧m X⇧m(v))))"
  unfolding DefM oops

text ‹Explicit refutability of the vertex-cover schema in the minimal
  embedding: with @{text II} interpreting @{text P} as the complete
  relation and @{text GG} mapping every symbol to the empty set, no
  symbol-indexed @{text X} can cover any edge.›

lemma vertex_cover_refutable_m:
  "∃(II'::ℐ) (gg'::ℰ) (GG'::𝒢).
     ¬ (∃X. ∀u. ∀v. II' P (gg' u) (gg' v) ⟶ (GG' X) (gg' u) ∨ (GG' X) (gg' v))"
  by (rule exI[of _ "λr a b. True"],
      rule exI[of _ "λ_. undefined"],
      rule exI[of _ "λZ d. False"]) simp

lemma transitivity_not_valid_m:
  "⊨⇧m (∀⇧mx. ∀⇧my. ∀⇧mz. (P⇧m(x,y) ⊃⇧m (P⇧m(y,z) ⊃⇧m P⇧m(x,z))))"
  unfolding DefM nitpick oops

lemma symmetry_not_valid_m:
  "⊨⇧m (∀⇧mx. ∀⇧my. (P⇧m(x,y) ⊃⇧m P⇧m(y,x)))"
  unfolding DefM nitpick oops

lemma triangle_exists_not_valid_m:
  "⊨⇧m (∃⇧mx. ∃⇧my. ∃⇧mz. (P⇧m(x,y) ∧⇧m P⇧m(y,z) ∧⇧m P⇧m(x,z)))"
  unfolding DefM oops

text ‹Explicit refutability: with @{text II} interpreting @{text P} as
  the empty relation no triangle can exist.›

lemma triangle_exists_refutable_m:
  "∃(II'::ℐ) (gg'::ℰ).
     ¬ (∃x. ∃y. ∃z. II' P (gg' x) (gg' y) ∧ II' P (gg' y) (gg' z) ∧ II' P (gg' x) (gg' z))"
  by (rule exI[of _ "λr a b. False"], rule exI[of _ "λ_. undefined"]) simp

lemma has_edge_not_valid_m:
  "⊨⇧m (∃⇧mx. ∃⇧my. P⇧m(x,y))"
  unfolding DefM nitpick oops

lemma loop_free_not_valid_m:
  "⊨⇧m (∀⇧mx. ¬⇧m P⇧m(x,x))"
  unfolding DefM nitpick oops

end