Theory Fresh_Identifiers.Fresh_Nat

section ‹Fresh identifier generation for natural numbers›

theory Fresh_Nat
  imports Fresh
begin

text ‹Assuming x ≤ y›, fresh2 xs x y› returns an element
outside the interval (x,y)› that is fresh for xs› and closest to this interval,
favoring smaller elements: ›

function fresh2 :: "nat set  nat  nat  nat" where
"fresh2 xs x y =
 (if x  xs  infinite xs then x else
  if y  xs then y else
  fresh2 xs (x-1) (y+1))"
by auto
termination
  apply(relation "measure (λ(xs,x,y). (Max xs) + 1 - y)")
  by (simp_all add: Suc_diff_le)

lemma fresh2_notIn: "finite xs  fresh2 xs x y  xs"
  by (induct xs x y rule: fresh2.induct) auto

lemma fresh2_eq: "x  xs  fresh2 xs x y = x"
  by auto

declare fresh2.simps[simp del]

instantiation nat :: fresh
begin

text fresh xs x y› returns an element
that is fresh for xs› and closest to x›, favoring smaller elements: ›

definition fresh_nat :: "nat set  nat  nat" where
"fresh_nat xs x  fresh2 xs x x"

instance by standard (use fresh2_notIn fresh2_eq in auto simp add: fresh_nat_def)

end (* instantiation *)

text ‹Code generation›

lemma fresh2_list[code]:
  "fresh2 (set xs) x y =
     (if x  set xs then x else
      if y  set xs then y else
      fresh2 (set xs) (x-1) (y+1))"
  by (auto simp: fresh2.simps)

text ‹Some tests: ›

value "[fresh {} (1::nat),
        fresh {3,5,2,4} 3]"

end