Theory MSOinHOL_faithfulness

theory MSOinHOL_faithfulness
  imports MSOinHOL_shallow_minimal
begin

text ‹Re-issuing the locale faithfulness theorems at the constants level.›

text ‹Deep ‹⟷› maximal shallow.›

theorem "(⟨I,D,E⟩,g,G ⊨⇧s ⟦φ⟧) ⟷ (⟨I,D,E⟩,g,G ⊨⇧d φ)"
  using FaithfulSDlem .

theorem "(⊨⇧s ⟦φ⟧) ⟷ (⊨⇧d φ)"
  using FaithfulSD .

text ‹Deep ‹⟷› minimal shallow, relative to the ranges of the chosen
  assignments ‹gg› and ‹GG›.›

theorem "⦇φ⦈ ⟷ (⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧d φ)"
  using FaithfulMDlem .

theorem "(⊨⇧m ⦇φ⦈) ⟷ (⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧d φ)"
  using FaithfulMD .

text ‹Minimal shallow ‹⟷› maximal shallow, again relative to the ranges
  of ‹gg› and ‹GG›; obtained by composing the two preceding bridges.›

theorem "⦇φ⦈ ⟷ (⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧s ⟦φ⟧)"
  using FaithfulMSlem .

theorem "(⊨⇧m ⦇φ⦈) ⟷ (⟨II,Range gg,Range GG⟩,gg,GG ⊨⇧s ⟦φ⟧)"
  using FaithfulMS .

text ‹Global form across all interpretations and the one-directional bridge
  to full deep validity.›

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

theorem "(⊨⇧d φ) ⟹ (∀II gg GG. (⊨⇧m (MinS.DpToShM II gg GG φ)))"
  using Deep_to_MinS by (simp add: MinS.ValM_def)

text ‹Consistency check.›

lemma True nitpick[satisfy] oops

end