Theory Fresh_Identifiers.Fresh

section ‹The type class ‹fresh››

theory Fresh
  imports Main
begin

text ‹A type in this class comes with a mechanism to generate fresh
items. The fresh operator takes a list of items to be avoided, ‹xs›, and
a preferred element to be generated, ‹x›.

It is required that
implementations of fresh for specific types produce ‹x› if possible
(i.e., if not in ‹xs›).

While not required, it is also expected that, if ‹x› is not possible,
then implementation produces an element that is as close to ‹x› as
possible, given a notion of distance.
›

class fresh =
  fixes fresh :: "'a set ⇒ 'a ⇒ 'a"
  assumes fresh_notIn: "⋀ xs x. finite xs ⟹ fresh xs x ∉ xs"
  and fresh_eq: "⋀ xs x. x ∉ xs ⟹ fresh xs x = x"


text ‹The type class \<^class>‹fresh› is essentially the same as
the type class ‹infinite› but with an emphasis on fresh item generation.›

class infinite =
  assumes infinite_UNIV: "¬ finite (UNIV :: 'a set)"

text ‹We can subclass \<^class>‹fresh› to \<^class>‹infinite› since the latter
has no associated operators (in particular, no additional operators w.r.t.
the former).›

subclass (in fresh) infinite
  apply (standard)
  using finite_list local.fresh_notIn by auto

end