Theory MSOinHOL_experiments_locale

theory MSOinHOL_experiments_locale
  imports MSOinHOL_faithfulness_locale
begin

text ‹Demonstration: minimal-shallow proofs that hold in every
  interpretation of the ‹MinS› locale transfer to validity in the model
  class whose domains are the assignment ranges.›

text ‹Derived rule: from validity in every minimal interpretation to
  range-relative deep validity.›

lemmas MinS_to_Deep = FaithfulMS_all[THEN iffD1, rule_format]

text ‹Cosmetic locale-level rewrite rules for derived connectives under
  ‹DpToShM›.›

lemma (in MinS) OrM_simp [DefM]: "⦇φ ∨⇧d ψ⦈ = ⦇φ⦈ ∨⇧m ⦇ψ⦈"
  by (simp add: OrD_def OrM_def)

lemma (in MinS) ImpM_simp [DefM]: "⦇φ ⊃⇧d ψ⦈ = ⦇φ⦈ ⊃⇧m ⦇ψ⦈"
  by (simp add: ImpD_def DefM)

text ‹Example: a membership tautology proved using only minimal-shallow
  infrastructure.›

lemma (in MinS) Mem_MinS: "⊨⇧m ⦇(P⇧d(x,x)) ⊃⇧d (P⇧d(x,x))⦈"
  by (auto simp: DefM)

text ‹Transfer to the range-relative deep embedding requires no further
  work.›

lemma "⟨I,Range g,Range G⟩,g,G ⊨⇧d ((P⇧d(x,x)) ⊃⇧d (P⇧d(x,x)))"
  by (rule MinS_to_Deep) (blast intro: MinS.Mem_MinS)

end