Theory MSOinHOL_faithfulness_locale

theory MSOinHOL_faithfulness_locale
  imports
    MSOinHOL_deep
    MSOinHOL_shallow
    MSOinHOL_shallow_minimal_locale
    MSOinHOL_deep_subst_lemma
begin

text ‹Translation from deep to maximal shallow (transparent: both use
  named-variable binders).›

fun DpToShS ("⟦_⟧")
  where
    "⟦r⇧^d(x,y)⟧ = r⇧^s(x,y)"
  | "⟦X⇧^d(x)⟧ = X⇧^s(x)"
  | "⟦¬⇧^dφ⟧ = ¬⇧^s⟦φ⟧"
  | "⟦φ ∧⇧^d ψ⟧ = ⟦φ⟧ ∧⇧^s ⟦ψ⟧"
  | "⟦∃⇧^dv. φ⟧ = (∃⇧^sv. ⟦φ⟧)"
  | "⟦∃⇧^d⇩₂V. φ⟧ = (∃⇧^s⇩₂V. ⟦φ⟧)"

text ‹Translation from deep to minimal shallow (within the locale
  ‹MinS›): each binder is bridged by safe substitution into a HOL-level
  binder---first-order via ‹[v←⇩_rd]›, second-order via
  ‹[V←⇩_r⇩₂D]›.›

fun (in MinS) DpToShM ("⦇_⦈")
  where
    "⦇r⇧^d(x,y)⦈ = r⇧^m(x,y)"
  | "⦇X⇧^d(x)⦈ = X⇧^m(x)"
  | "⦇¬⇧^dφ⦈ = ¬⇧^m⦇φ⦈"
  | "⦇φ ∧⇧^d ψ⦈ = ⦇φ⦈ ∧⇧^m ⦇ψ⦈"
  | "⦇∃⇧^dv. φ⦈ = (∃⇧^md. ⦇[v ←⇩_r d](φ)⦈)"
  | "⦇∃⇧^d⇩₂V. φ⦈ = (∃⇧^m⇩₂D. ⦇[V ←⇩_r⇩₂ D](φ)⦈)"

text ‹Faithfulness deep ‹⟷› maximal shallow.  Pointwise first; global
  by unfolding validity.›

theorem FaithfulSDlem:
  "(⟨I,D,E⟩,g,G ⊨⇧^s ⟦φ⟧) ⟷ (⟨I,D,E⟩,g,G ⊨⇧^d φ)"
  by (induct φ arbitrary: g G; auto simp: DefS DefD)

theorem FaithfulSD: "(⊨⇧^s ⟦φ⟧) ⟷ (⊨⇧^d φ)"
  by (simp add: FaithfulSDlem ValD_def ValS_def)

text ‹Faithfulness deep ‹⟷› minimal shallow, parametrised by the
  locale, relative to the ranges of ‹gg› and ‹GG›.›

context MinS
begin

theorem FaithfulMDlem:
  "⦇φ⦈ ⟷ (⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧^d φ)"
  by (induct φ rule: QInduct; simp add: DefD DefM) blast+

theorem FaithfulMD:
  "(⊨⇧^m ⦇φ⦈) ⟷ (⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧^d φ)"
  using FaithfulMDlem by (simp add: ValM_def)

text ‹Faithfulness minimal shallow ‹⟷› maximal shallow, parametrised by
  the locale, relative to the ranges of ‹gg› and ‹GG›; obtained by
  composing @{thm [source] FaithfulSDlem} and @{thm [source] FaithfulMDlem}.›

theorem FaithfulMSlem:
  "⦇φ⦈ ⟷ (⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧^s ⟦φ⟧)"
  using FaithfulSDlem FaithfulMDlem by auto

theorem FaithfulMS:
  "(⊨⇧^m ⦇φ⦈) ⟷ (⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧^s ⟦φ⟧)"
  using FaithfulMSlem by (simp add: ValM_def)

end

text ‹Global faithfulness: a formula holds in every minimal interpretation
  of ‹MinS› iff it holds in every model whose first- and second-order
  domains are exactly the ranges of the chosen assignments.›

theorem FaithfulMS_all:
  "(∀II gg GG. MinS.ValM (MinS.DpToShM II gg GG φ)) = (∀I g G. ⟨I,Range g,Range G⟩,g,G ⊨⇧^d φ)"
  by (simp add: MinS.FaithfulMD)

text ‹One direction toward full deep validity: deep validity transfers to
  every minimal interpretation.  The converse is the (second-order)
  surjectivity problem discussed in the paper.›

theorem Deep_to_MinS:
  "(⊨⇧^d φ) ⟹ (∀II gg GG. MinS.ValM (MinS.DpToShM II gg GG φ))"
  by (metis (mono_tags, lifting) MinS.FaithfulMD ValD_def)

text ‹Consistency check.›

lemma True nitpick[satisfy] oops

end