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 elements.
The ‹fresh› operator takes a set of items to be avoided, ‹X›, 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 ‹X›).

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.

A subclass ‹fresh0› provides function ‹fresh0 :: 'a set ⇒ 'a› that does not require
an initial item.
›

class fresh =
  fixes fresh :: "'a set ⇒ 'a ⇒ 'a"
  assumes fresh_notIn: "finite F ⟹ fresh F x ∉ F"
  and fresh_eq: "x ∉ A ⟹ fresh A x = x"
begin

text ‹Generate a list of fresh names ‹[a', b', c', …]› given the list ‹[a, b, c, …]›:›

fun freshs :: "'a set ⇒ 'a list ⇒ 'a list" where
"freshs X [] = []" |
"freshs X (a#as) = (let a' = fresh X a in a' # freshs (insert a' X) as)"

lemma length_freshs: "finite X ⟹ length(freshs X as) = length as"
by(induction as arbitrary: X)(auto simp: fresh_notIn Let_def)

lemma freshs_disj: "finite X ⟹ X ∩ set(freshs X as) = {}"
proof(induction as arbitrary: X)
  case Cons
  then show ?case using fresh_notIn by(auto simp add: Let_def)
qed simp

lemma freshs_distinct: "finite X ⟹ distinct (freshs X as)"
proof(induction as arbitrary: X)
  case (Cons a as)
  then show ?case
    using freshs_disj[of "insert (fresh X a) X" as] fresh_notIn by(auto simp add: Let_def)
qed simp

end

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 local.fresh_notIn by auto

class fresh0 = fresh +
fixes fresh0_default :: "'a"
begin

definition fresh0 :: "'a set ⇒ 'a" where
"fresh0 X = fresh X fresh0_default"

lemma fresh0_notIn: "finite F ⟹ fresh0 F ∉ F"
unfolding fresh0_def by(rule fresh_notIn)

end

end