1

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?

1
  • Using !! x. x ∈ S ⟹ f x = r seem to work okaish, and better than ∀ x ∈ S. f x = r, at least in situations where auto’s limits are stressed... Sep 30, 2014 at 10:17

2 Answers 2

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)
5
  • @JoachimBreitner Oh sorry, you just wrote something similar in a comment (after I started typing my answer) ;)
    – chris
    Sep 30, 2014 at 10:26
  • It’s not similar; you introduce a new name and rely on the simplifier to make the connection. It might work well if both assumptions of the simp-lemma are readily available, but it still might be weaker than using the meta-implication directly, which can be used by auto to “try things out”. Sep 30, 2014 at 10:33
  • You can also use the [simp] lemma as a destruction rule with auto. If all your use cases require the instance only for solving equalities in the conclusion, you could also use the similar rule const f S r ==> x : S ==> r = r' ==> f x = r' as an elimination rule. My feeling is that a separate constant with proper intro/elim/dest rules works better than the solution with image, because image requires several reasoning steps that you could combine in a single one for a constant of your own. Sep 30, 2014 at 14:41
  • I tried the above, but that rule makes the simplifier loop. Maybe I have more luck with an elim rule. Oct 30, 2014 at 13:12
  • The elim rule did not quite cut it for me, but I had more luck with [dest]: "const_on f S x ⟹ y ∈ S ⟹ f y = x", at least in this instance. And in most but the most simple cases I have to use fastforce instead of auto. This is still mostly guesswork here... Nov 6, 2014 at 9:35
1

The Analysis library defines

definition constant_on  (infixl "(constant'_on)" 50)
  where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.