Theory MSOinHOL_subst_extras

theory MSOinHOL_subst_extras
  imports MSOinHOL_deep_subst_lemma
begin

text ‹Explicit rename-evaluation lemmas: renaming a bound variable to a
  fresh ‹f› and updating the assignment preserves truth---the semantic
  core behind ‹L21› / ‹N21›.›

text ‹First-order: rename ‹y› to a fresh ‹f›, then evaluate.›

lemma rename_eval:
  assumes "fresh φ ≤ f" and "y < f"
  shows "(⟨I,D,E⟩,g[f←d],G ⊨⇧d [y←f](φ)) = (⟨I,D,E⟩,g[y←d],G ⊨⇧d φ)"
proof -
  let ?g' = "g[f←d]"
  have fy: "f ≠ y" using assms(2) by simp
  have nf: "f not_free_in φ" using assms(1) by (meson L6 leD)
  have "f not_in φ" using assms(1) by (meson L5 L6 leD)
  hence sub: "f is_subst_for y in φ" by (rule L18)
  have swap: "?g'[y←d] = (g[y←d])[f←d]"
    using fy by (rule L2)
  have "(⟨I,D,E⟩,?g',G ⊨⇧d [y←f](φ)) = (⟨I,D,E⟩,?g'[y←(?g' f)],G ⊨⇧d φ)"
    using sub by (rule SubstitutionLemma)
  also have "… = (⟨I,D,E⟩,?g'[y←d],G ⊨⇧d φ)" by simp
  also have "… = (⟨I,D,E⟩,(g[y←d])[f←d],G ⊨⇧d φ)"
    using swap by simp
  also have "… = (⟨I,D,E⟩,g[y←d],G ⊨⇧d φ)"
    using nf by (simp add: L12)
  finally show ?thesis .
qed

text ‹Second-order: rename ‹Y› to a fresh ‹f›, then evaluate.  (The
  monadic-set twin of ‹rename_eval›.)›

lemma rename_eval2:
  assumes "fresh2 φ ≤ f" and "Y < f"
  shows "(⟨I,D,E⟩,g,G⟨f←S⟩ ⊨⇧d [Y←⇩2f](φ)) = (⟨I,D,E⟩,g,G⟨Y←S⟩ ⊨⇧d φ)"
proof -
  let ?G' = "G⟨f←S⟩"
  have fy: "f ≠ Y" using assms(2) by simp
  have nf: "f not_free2_in φ" using assms(1) by (meson N6 leD)
  have "f not2_in φ" using assms(1) by (meson N5 N6 leD)
  hence sub: "f is_subst2_for Y in φ" by (rule N18)
  have swap: "?G'⟨Y←S⟩ = G⟨Y←S⟩⟨f←S⟩"
    using fy by (rule M2)
  have "(⟨I,D,E⟩,g,?G' ⊨⇧d [Y←⇩2f](φ)) = (⟨I,D,E⟩,g,?G'⟨Y←(?G' f)⟩ ⊨⇧d φ)"
    using sub by (rule SubstitutionLemma2)
  also have "… = (⟨I,D,E⟩,g,?G'⟨Y←S⟩ ⊨⇧d φ)" by simp
  also have "… = (⟨I,D,E⟩,g,(G⟨Y←S⟩)⟨f←S⟩ ⊨⇧d φ)"
    using swap by simp
  also have "… = (⟨I,D,E⟩,g,G⟨Y←S⟩ ⊨⇧d φ)"
    using nf by (simp add: N12)
  finally show ?thesis .
qed

end