Theory Fresh_Infinite

section ‹Fresh identifier generation for infinite types›

theory Fresh_Infinite
  imports Fresh
begin

text ‹This is a default fresh operator for infinite types
for which more specific (smarter) alternatives are not (yet) available. ›


definition (in infinite) fresh :: "'a set ⇒ 'a ⇒ 'a" where
"fresh xs x ≡ if x ∉ xs ∨ infinite xs then x else (SOME y. y ∉ xs)"

sublocale infinite < fresh where fresh = fresh
apply standard
  subgoal unfolding fresh_def
  by (metis ex_new_if_finite local.infinite_UNIV someI_ex)
  subgoal unfolding fresh_def by simp .

end