Theory MSOinHOL_experiments_classic_elementary

theory MSOinHOL_experiments_classic_elementary
  imports
    MSOinHOL_deep
    MSOinHOL_shallow
    MSOinHOL_shallow_minimal_elementary
begin

text ‹Extra simp rules for derived quantifiers / connectives.›

lemma ren_for_subst2_simp_All [simp]:
  "ren_for_subst2 X Z (∀⇧d⇩2Y. φ) =
     (if Y = Z ∧ X free2_in φ
      then let f = max (fresh2 φ) (Z+1); φ' = [Y←⇩2f](φ)
           in (∀⇧d⇩2f. ren_for_subst2 X Z φ')
      else ∀⇧d⇩2Y. ren_for_subst2 X Z φ)"
  unfolding DefD by (auto simp: Let_def)

lemma subst2_all [simp]:
  "[X←⇩2Z](∀⇧d⇩2Y. φ) =
     (if X = Y then (∀⇧d⇩2Y. φ) else (∀⇧d⇩2Y. [X←⇩2Z](φ)))"
  unfolding DefD by (auto simp: Let_def)

lemma free2_in_equiv [simp]:
  "X free2_in (φ ⟷⇧d ψ) = (X free2_in φ ∨ X free2_in ψ)"
  by (auto simp add: DefD)

lemma free2_in_all [simp]:
  "X free2_in (∀⇧dy. φ) = (X free2_in φ)"
  by (simp add: AllD_def)

lemma free2_in_all2 [simp]:
  "X free2_in (∀⇧d⇩2Y. φ) = (X free2_in φ ∧ X ≠ Y)"
  by (metis AllD2_def is_free2.simps)

text ‹Some abbreviations for variables.›

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)›

text ‹Under @{text "⊨⇧d'"}: witnesses supplied via @{text exI}.›

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 intersection_d':
  "⊨⇧d' (∃⇧d⇩2Z. ∀⇧dx. (Z⇧d(x) ⟷⇧d (X⇧d(x) ∧⇧d Y⇧d(x))))"
  by (simp add: comprehension_schema)

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 ‹Transfer to the elementary minimal embedding›

text ‹Via the @{text DpToShS} normal-form and @{text ValidM_if_ValidD'}.›

lemma compl_m_DpToSh:
  "⦇∀⇧d⇩2X. ∃⇧d⇩2Z. ∀⇧dx. (Z⇧d(x) ⟷⇧d ¬⇧d X⇧d(x))⦈ = (∀⇧m⇩2X. ∃⇧m⇩2Z. ∀⇧mx. (Z⇧m(x) ⟷⇧m ¬⇧m X⇧m(x)))"
  by (auto simp add: ren_subst2_def ren_subst_def Let_def)
     (auto simp: DefD DefM ren_subst_def)

lemma compl_m_valid:
  "⊨⇧m (∀⇧m⇩2X. ∃⇧m⇩2Z. ∀⇧mx. (Z⇧m(x) ⟷⇧m ¬⇧m X⇧m(x)))"
  using compl_m_DpToSh ValidM_if_ValidD'[OF complement_d] by simp

lemma inters_m_DpToSh':
  "⦇∃⇧d⇩2Z. ∀⇧dx. (Z⇧d(x) ⟷⇧d (X⇧d(x) ∧⇧d Y⇧d(x)))⦈ = (∃⇧m⇩2Z. ∀⇧mx. (Z⇧m(x) ⟷⇧m (X⇧m(x) ∧⇧m Y⇧m(x))))"
  by (auto simp add: ren_subst2_def ren_subst_def Let_def)
     (auto simp: DefD DefM ren_subst_def)

lemma DpToSh_alleqI:
  "(⋀d. ⦇[X ←⇩r⇩2 d](φ)⦈ = ψ d) ⟹ ⦇∀⇧d⇩2X. φ⦈ = (∀⇧m⇩2X. ψ X)"
  by simp

lemma all_m_eqI:
  "(⋀X. φ X = ψ X) ⟹ (∀⇧m⇩2X. φ X) = (∀⇧m⇩2X. ψ X)"
  by presburger

lemmas DpToSh_simps = DefM Let_def ren_subst_def DefD ren_subst2_def

lemma intersect_m_DpToSh:
  "⦇∀⇧d⇩2X. ∀⇧d⇩2Y. ∃⇧d⇩2Z. ∀⇧dx. (Z⇧d(x) ⟷⇧d (X⇧d(x) ∧⇧d Y⇧d(x)))⦈ = (∀⇧m⇩2X. ∀⇧m⇩2Y. ∃⇧m⇩2Z. ∀⇧mx. (Z⇧m(x) ⟷⇧m (X⇧m(x) ∧⇧m Y⇧m(x))))"
  ― ‹Push @{term DpToShM} through the two outer set quantifiers and split on
      whether the fresh index @{term d} chosen by the renaming coincides with
      @{term Z}, with @{term Y}, or with neither.  Each case is discharged
      inside its own @{text subgoal} block, so no @{text auto} step silently
      hands its leftover goals to the next one.›
  apply (rule DpToSh_alleqI,
         simp only: ren_subst2_def subst2_all ren_for_subst2_simp_All,
         simp)
  subgoal for d
    apply (cases "d = Z", simp, rule all_m_eqI)
    subgoal by (auto simp: DpToSh_simps)
    apply (simp, cases "d = Y", simp)
    subgoal by (auto simp: DpToSh_simps; metis)
        ― ‹Remaining case @{text "d ∉ {Y,Z}"}: normalise the renamed body and offer
      the bound predicate @{term D} as the existential witness.  The fresh index
      @{term "max Z (max d Y)"} exceeds both @{term Y} and @{term d}, so the two
      guarded substitutions collapse.  Normalisation and the witness step are
      kept together in one @{text subgoal}, so any change in the shape of the
      @{text auto}-normalised goal fails here rather than downstream.›
    apply (simp, rule all_m_eqI)
    subgoal for da
      apply (auto simp: ren_subst2_def ren_subst_def Let_def)
      subgoal apply (auto simp: DpToSh_simps)
        subgoal for D
          apply (rule exI[where x=D])
          apply (subgoal_tac "Suc (max Z (max d Y)) ≠ d" "max Z (max d Y) ≠ Y")
            apply simp
           apply simp
          apply (simp add: le_imp_less_Suc max.coboundedI2)
          done
        done
      by (auto simp: DpToSh_simps)
    done
  done

lemma intersection_m_valid:
  "⊨⇧m (∀⇧m⇩2X. ∀⇧m⇩2Y. ∃⇧m⇩2Z. ∀⇧mx. (Z⇧m(x) ⟷⇧m (X⇧m(x) ∧⇧m Y⇧m(x))))"
  using ValM_def ValidM_if_ValidD' intersection_d intersect_m_DpToSh
  by blast

text ‹Reachability and 2-colorability remain refuted in the elementary
  minimal embedding.›

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 oops

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 oops

end