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