Theory MSOinHOL_experiments_classic

theory MSOinHOL_experiments_classic
  imports
    MSOinHOL_deep
    MSOinHOL_shallow
    MSOinHOL_shallow_minimal
begin

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 ‹Boolean closure (B\"uchi 1960; Thomas 1997) under @{text "⊨⇧d'"}›

lemma complement_d:
  "⊨⇧d' (∀⇧d⇩2X. ∃⇧d⇩2Z. ∀⇧dx. (Z⇧d(x) ⟷⇧d ¬⇧d X⇧d(x)))"
  unfolding DefD
  apply (intro allI, simp add: SetMod_def EnvMod_def, intro allI)
  subgoal for S
    by (rule exI[of _ "λd. ¬ S d"]) (auto simp: SetMod_def EnvMod_def)
  done

lemma intersection_d:
  "⊨⇧d' (∀⇧d⇩2X. ∀⇧d⇩2Y. ∃⇧d⇩2Z. ∀⇧dx. (Z⇧d(x) ⟷⇧d (X⇧d(x) ∧⇧d Y⇧d(x))))"
  unfolding DefD
  apply (intro allI, simp add: SetMod_def EnvMod_def, intro allI)
  subgoal for S Sa
    by (rule exI[of _ "λd. S d ∧ Sa d"])
       (auto simp: SetMod_def EnvMod_def)
  done

lemma union_d:
  "⊨⇧d' (∀⇧d⇩2X. ∀⇧d⇩2Y. ∃⇧d⇩2Z. ∀⇧dx. (Z⇧d(x) ⟷⇧d (X⇧d(x) ∨⇧d Y⇧d(x))))"
  unfolding DefD
  apply (intro allI, simp add: SetMod_def EnvMod_def, intro allI)
  subgoal for S Sa
    by (rule exI[of _ "λd. S d ∨ Sa d"])
       (auto simp: SetMod_def EnvMod_def)
  done

subsubsection ‹Graph operations (Courcelle 2012)›

lemma separation_d:
  "⊨⇧d' (∀⇧d⇩2X. ∃⇧d⇩2Z. ∀⇧dx. (Z⇧d(x) ⟷⇧d (X⇧d(x) ∧⇧d P⇧d(x,x))))"
  unfolding DefD
  apply (intro allI, simp add: SetMod_def EnvMod_def, intro allI)
  subgoal for I S
    by (rule exI[of _ "λd. S d ∧ I P d d"])
       (auto simp: SetMod_def EnvMod_def)
  done

lemma image_d:
  "⊨⇧d' (∀⇧d⇩2X. ∃⇧d⇩2Y. ∀⇧dx. (Y⇧d(x) ⟷⇧d ∃⇧dy. (X⇧d(y) ∧⇧d P⇧d(y,x))))"
  unfolding DefD
  apply (intro allI, simp add: SetMod_def EnvMod_def, intro allI)
  subgoal for I S
    by (rule exI[of _ "λd. ∃d'. S d' ∧ I P d' d"])
       (auto simp: SetMod_def EnvMod_def)
  done

lemma preimage_d:
  "⊨⇧d' (∀⇧d⇩2X. ∃⇧d⇩2Y. ∀⇧dx. (Y⇧d(x) ⟷⇧d ∃⇧dy. (P⇧d(x,y) ∧⇧d X⇧d(y))))"
  unfolding DefD
  apply (intro allI, simp add: SetMod_def EnvMod_def, intro allI)
  subgoal for I S
    by (rule exI[of _ "λd. ∃d'. I P d d' ∧ S d'"])
       (auto simp: SetMod_def EnvMod_def)
  done

text ‹Reachability (Basin and Klarlund 1995): not universally valid;
  reflexive variant is.›

lemma reachability_not_valid_d:
  "⊨⇧d' (∀⇧d⇩2Z. ((Z⇧d(x) ∧⇧d (∀⇧du. (Z⇧d(u) ⊃⇧d ∀⇧dv. (P⇧d(u,v) ⊃⇧d Z⇧d(v))))) ⊃⇧d Z⇧d(y)))"
  unfolding DefD apply simp nitpick oops

lemma reachability_reflexive_d:
  "⊨⇧d' (∀⇧d⇩2Z. ((Z⇧d(x) ∧⇧d (∀⇧du. (Z⇧d(u) ⊃⇧d ∀⇧dv. (P⇧d(u,v) ⊃⇧d Z⇧d(v))))) ⊃⇧d Z⇧d(x)))"
  unfolding DefD by simp

text ‹2-colorability (Thomas 1997): refuted on the triangle ‹K⇩3›
  (the complete graph on three vertices).›

lemma two_colorability_not_valid_d:
  "⊨⇧d' (∃⇧d⇩2Z. ∀⇧dx. ∀⇧dy. (P⇧d(x,y) ⊃⇧d (Z⇧d(x) ⟷⇧d ¬⇧d Z⇧d(y))))"
  unfolding DefD apply simp nitpick oops

subsubsection ‹Maximal-shallow embedding›

text ‹Same landmarks in the maximal-shallow embedding: structurally
  identical proofs.›

lemma complement_s:
  "⊨⇧s' (∀⇧s⇩2X. ∃⇧s⇩2Z. ∀⇧sx. (Z⇧s(x) ⟷⇧s ¬⇧s X⇧s(x)))"
  unfolding DefS
  apply (intro allI, simp, intro allI)
  subgoal for S by (rule exI[of _ "λd. ¬ S d"]) auto
  done

lemma intersection_s:
  "⊨⇧s' (∀⇧s⇩2X. ∀⇧s⇩2Y. ∃⇧s⇩2Z. ∀⇧sx. (Z⇧s(x) ⟷⇧s (X⇧s(x) ∧⇧s Y⇧s(x))))"
  unfolding DefS
  apply (intro allI, simp, intro allI)
  subgoal for S Sa by (rule exI[of _ "λd. S d ∧ Sa d"]) auto
  done

lemma union_s:
  "⊨⇧s' (∀⇧s⇩2X. ∀⇧s⇩2Y. ∃⇧s⇩2Z. ∀⇧sx. (Z⇧s(x) ⟷⇧s (X⇧s(x) ∨⇧s Y⇧s(x))))"
  unfolding DefS
  apply (intro allI, simp, intro allI)
  subgoal for S Sa by (rule exI[of _ "λd. S d ∨ Sa d"]) auto
  done

lemma separation_s:
  "⊨⇧s' (∀⇧s⇩2X. ∃⇧s⇩2Z. ∀⇧sx. (Z⇧s(x) ⟷⇧s (X⇧s(x) ∧⇧s P⇧s(x,x))))"
  unfolding DefS
  apply (intro allI, simp, intro allI)
  subgoal for I S by (rule exI[of _ "λd. S d ∧ I P d d"]) auto
  done

lemma image_s:
  "⊨⇧s' (∀⇧s⇩2X. ∃⇧s⇩2Y. ∀⇧sx. (Y⇧s(x) ⟷⇧s (∃⇧sy. (X⇧s(y) ∧⇧s P⇧s(y,x)))))"
  unfolding DefS
  apply (intro allI, simp, intro allI)
  subgoal for I S
    by (rule exI[of _ "λd. ∃d'. S d' ∧ I P d' d"]) auto
  done

lemma preimage_s:
  "⊨⇧s' (∀⇧s⇩2X. ∃⇧s⇩2Y. ∀⇧sx. (Y⇧s(x) ⟷⇧s (∃⇧sy. (P⇧s(x,y) ∧⇧s X⇧s(y)))))"
  unfolding DefS
  apply (intro allI, simp, intro allI)
  subgoal for I S
    by (rule exI[of _ "λd. ∃d'. I P d d' ∧ S d'"]) auto
  done

lemma reachability_not_valid_s:
  "⊨⇧s' (∀⇧s⇩2Z. ((Z⇧s(x) ∧⇧s (∀⇧su. (Z⇧s(u) ⊃⇧s (∀⇧sv. (P⇧s(u,v) ⊃⇧s Z⇧s(v)))))) ⊃⇧s Z⇧s(y)))"
  unfolding DefS apply (intro allI) apply simp nitpick oops

lemma reachability_reflexive_s:
  "⊨⇧s' (∀⇧s⇩2Z. ((Z⇧s(x) ∧⇧s (∀⇧su. (Z⇧s(u) ⊃⇧s (∀⇧sv. (P⇧s(u,v) ⊃⇧s Z⇧s(v)))))) ⊃⇧s Z⇧s(x)))"
  unfolding DefS by simp

lemma two_colorability_not_valid_s:
  "⊨⇧s' (∃⇧s⇩2Z. ∀⇧sx. ∀⇧sy. (P⇧s(x,y) ⊃⇧s (Z⇧s(x) ⟷⇧s ¬⇧s Z⇧s(y))))"
  unfolding DefS apply (intro allI) apply simp nitpick oops

subsubsection ‹Minimal-shallow embedding›

text ‹Minimal embedding: SO quantifier ranges over the countable
  ‹Range GG› (via ‹nat›), not all of ‹Pow(D)›.  Nitpick can only certify
  a POTENTIAL countermodel.›

lemma complement_m_not_valid:
  "⊨⇧m (∀⇧m⇩2X. ∃⇧m⇩2Z. ∀⇧mx. (Z⇧m(x) ⟷⇧m ¬⇧m X⇧m(x)))"
  unfolding DefM nitpick[expect=potential] oops

lemma intersection_m_not_valid:
  "⊨⇧m (∀⇧m⇩2X. ∀⇧m⇩2Y. ∃⇧m⇩2Z. ∀⇧mx. (Z⇧m(x) ⟷⇧m (X⇧m(x) ∧⇧m Y⇧m(x))))"
  unfolding DefM nitpick[expect=potential] oops

lemma reachability_not_valid_m:
  "⊨⇧m (∀⇧m⇩2Z. ((Z⇧m(x) ∧⇧m (∀⇧mu. (Z⇧m(u) ⊃⇧m (∀⇧mv. (P⇧m(u,v) ⊃⇧m Z⇧m(v)))))) ⊃⇧m Z⇧m(y)))"
  unfolding DefM nitpick[expect=potential] oops

text ‹Reflexive reachability: the conclusion is the first conjunct of the
  antecedent; genuinely valid.›

lemma reachability_reflexive_m:
  "⊨⇧m (∀⇧m⇩2Z. ((Z⇧m(x) ∧⇧m (∀⇧mu. (Z⇧m(u) ⊃⇧m (∀⇧mv. (P⇧m(u,v) ⊃⇧m Z⇧m(v)))))) ⊃⇧m Z⇧m(x)))"
  unfolding DefM by simp

lemma two_colorability_not_valid_m:
  "⊨⇧m (∃⇧m⇩2Z. ∀⇧mx. ∀⇧my. (P⇧m(x,y) ⊃⇧m (Z⇧m(x) ⟷⇧m ¬⇧m Z⇧m(y))))"
  unfolding DefM nitpick[expect=potential] oops

end