Theory 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