Express that a function is constant on a set

Question

I’m trying to express that a function f is constant on a set S, with value r My first idea was

f ` S = {r}

but that does not work, as S can be empty. So I am currently working with

f ` S ⊆ {r}

and it works okish, but I have the impression that this is still not ideal for the standard automation. In particular, auto would fail leaving this goal (irrelevant facts erased)

 2. ⋀xa. thunks (delete x Γ) ⊆ thunks Γ ⟹
         ae ` thunks Γ ⊆ {up⋅0} ⟹
         xa ∈ thunks (delete x Γ) ⟹
         ae xa = up⋅0

Sledgehammer of course has no problem (metis image_eqI singletonD subsetCE), but there are a few occurrences of this. (In general, ⊆ does not seem to work with auto as good as I’d expect).

There there a better way to express this, i.e. one that can be used by auto more easily when occurring as an assumption?

Answer 1

I didn't try it, since I didn't have any examples handy. But you might try the following setup.

definition "const f S r ≡ ∀x ∈ S. f x = r"

Which is equivalent to your definition:

lemma
  "const f S r ⟷ f ` S ⊆ {r}"
  by (auto simp: const_def)

Then employ the following simp rule:

lemma [simp]:
  "const f S r ⟹ x ∈ S ⟹ f x = r"
  by (simp add: const_def)