Theory Abstract_Renaming_Apart

theory Abstract_Renaming_Apart
  imports Main
begin

section ‹Abstract Renaming›

locale renaming_apart =
  fixes
    renaming :: "'a set ⇒ 'a ⇒ 'a"
  assumes
    renaming_correct: "finite V ⟹ renaming V x ∉ V" and
    inj_renaming: "finite V ⟹ inj (renaming V)"


subsection ‹Interpretation to Prove That Assumptions Are Consistent›

experiment begin

definition renaming_apart_nats where
  "renaming_apart_nats V = (let m = Max V in (λx. Suc (x + m)))"

interpretation renaming_apart_nats: renaming_apart renaming_apart_nats
proof unfold_locales
  show "⋀V x. finite V ⟹ renaming_apart_nats V x ∉ V"
    unfolding renaming_apart_nats_def Let_def by (meson Max.coboundedI Suc_le_lessD not_add_less2)
next
  show "⋀V. inj (renaming_apart_nats V)"
    unfolding renaming_apart_nats_def Let_def by (rule injI) simp
qed

end

end