Theory Fresh_Identifiers.Fresh

section ‹The type class fresh›

theory Fresh
  imports Main

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 classfresh 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 classfresh to classinfinite 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