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, ‹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: "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
end