Theory Fresh_Int

section ‹Fresh identifier generation for integers›

theory Fresh_Int
  imports Fresh
begin

text ‹Function ‹fresh› does not follow the "find element closest to ‹x› outside of ‹X› requirement.
If ‹x < 0›, a fresh negative value is produced by repeated ‹-1›.
Similarly if ‹x ≥ 0› with ‹+1›.
›

function fresh_pos :: "int set ⇒ int ⇒ int" where
"fresh_pos X x = (if x ∉ X ∨ infinite X then x else fresh_pos X (x+1))"
by auto
termination
  by(relation "measure (λ(X,x). nat(Max X + 1 - x))") (simp_all)

function fresh_neg :: "int set ⇒ int ⇒ int" where
"fresh_neg X x = (if x ∉ X ∨ infinite X then x else fresh_neg X (x-1))"
by auto
termination
  by(relation "measure (λ(X,x). nat(- Min X + x + 1))") (simp_all)

lemma fresh_pos_notIn: "finite X ⟹ fresh_pos X x ∉ X"
  by (induct X x rule: fresh_pos.induct) auto

lemma fresh_neg_notIn: "finite X ⟹ fresh_neg X x ∉ X"
  by (induct X x rule: fresh_neg.induct) auto

instantiation int :: fresh
begin

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

definition fresh_int :: "int set ⇒ int ⇒ int" where
"fresh_int X x ≡ if x < 0 then fresh_neg X x else fresh_pos X x"

instance
proof (standard, goal_cases)
  case (1 F x)
  then show ?case unfolding fresh_int_def
    by (metis fresh_pos_notIn fresh_neg_notIn)
next
  case (2 x A)
  then show ?case unfolding fresh_int_def by simp
qed

end (* instantiation *)

instantiation int :: fresh0
begin

definition fresh0_default_int :: nat where
"fresh0_default_int ≡ 0"

instance ..

end (* instantiation *)

text ‹Code generation›

lemma fresh_pos_list[code]:
  "fresh_pos (set xs) x =
     (if x ∉ set xs then x else fresh_pos (set xs) (x+1))"
  by (simp)

lemma fresh_neg_list[code]:
  "fresh_neg (set xs) x =
     (if x ∉ set xs then x else fresh_neg (set xs) (x-1))"
  by (simp)

text ‹Some tests: ›

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

end