Stream: General

Topic: Why can't we take the domain of an arbitrary function?

Alex Weisberger (Sep 17 2023 at 18:54):

For example, let's say I define a function type as:

type_synonym ('e, 's) transition = "'e => 's => 's"

and say I wanted to restrict valid transition functions in a lemma:

lemma fixes t :: "('e, 's) transition"
  assumes "dom t ⊆ D"
  ...

A dom function only exists on maps (from theory Map). It's very common to make propositions about the domain of functions, so is there some other way to do that, or is it more common to use Maps in that case?

Jan van Brügge (Sep 17 2023 at 18:58):

The function is called range not dom for functions

Mathias Fleury (Sep 17 2023 at 19:01):

If the question is about the domain: Isabelle functions are always total on the input domain. Therefore, it often happens that lemmas have assumptions on the domain of functions (often with invariants).

Alex Weisberger (Sep 17 2023 at 19:12):

Jan van Brügge said:

The function is called range not dom for functions

I don't think that's accurate. The range function returns the range, not the domain of a function.

Alex Weisberger (Sep 17 2023 at 19:12):

Mathias Fleury said:

If the question is about the domain: Isabelle functions are always total on the input domain. Therefore, it often happens that lemmas have assumptions on the domain of functions (often with invariants).

That's a good point about totality. That's why a Map might be more appropriate in this case - I want to add a restriction to the function domain.

Jan van Brügge (Sep 18 2023 at 10:19):

Sorry, I somehow read codom

Last updated: May 02 2024 at 08:19 UTC