CODEWITHSUNDEEP
isabelletheorem-proving
DianaPrince
DianaPrince

Reputation: 101

Isabelle/HOL restrict codomain

I am sorry for asking so many Isabelle questions lately. Right now I have a type problem.

I want to use a type_synonym introduced in a AFP-theory.

type_synonym my_fun = "nat ⇒ real"

I have a locale in my own theory where:

fixes n :: nat

and f :: "my_fun"

and A :: "nat set"

defines A: "A ≡ {0..n}"

However, in my use case the output of the function f is always a natural number in the set {0..n}. I want to impose this as a condition (or is there a better way to do it?). The only way I found was to:

assumes "∀v. ∃ i. f v = i ∧ i ∈ A"

since

assumes "∀v. f v ∈ A"

does not work.

If I let Isabelle show me the involved types it seems alright to me:

∀v::nat. ∃i::nat. (f::nat ⇒ real) v = real i ∧ i ∈ (A::nat set)

But of course now I cannot type something like this:

have "f ` {0..10} ⊆ A"

But I have to prove this. I understand where this problem comes from. However, I do not know how to proceed in a case like this. What is the normal way to deal with it? I would like to use my_fun as it has the same meaning as in my theory.

Thank you (again).

Upvotes: 1

Views: 150

Answers (1)

user9716869 - supports Ukraine
user9716869 - supports Ukraine

Reputation: 1941

If you look closely at ∀v::nat. ∃i::nat. (f::nat ⇒ real) v = real i ∧ i ∈ (A::nat set), you will be able to see the mechanism that was used for making the implicit type conversion between nat and real: it is the abbreviation real (this invokes of_nat defined for semiring_1 in Nat.thy) that appears in the statement of the assumption in the context of the locale.

Of course, you can use the same mechanism explicitly. For example, you can define A::real set as A ≡ image real {0..n} instead of A::nat set as A ≡ {0..n}. Then you can use range f ⊆ A instead of assumes "∀v. ∃ i. f v = i ∧ i ∈ A”. However, I doubt that there is a universally accepted correct way to do it: it depends on what exactly you are trying to achieve. Nonetheless, for the sake of the argument, your locale could look like this:

type_synonym my_fun = "nat ⇒ real"

locale myloc_basis =
  fixes n :: nat

abbreviation (in myloc_basis) A where "A ≡ image real {0..n}"

locale myloc = myloc_basis +
  fixes f :: "my_fun"
  assumes range: "range f ⊆ A"

lemma (in myloc) "f ` {0..10} ⊆ A"
  using range by auto

I want to impose this as a condition (or is there a better way to do it?).

The answer depends on what is known about f. If only a condition on the range of f is known, as the statement of your question seems to suggest, then, I guess, you can only state is as an assumption.

As a side note, to the best of my knowledge, defines is considered to be obsolete and it is best to avoid using it in the specifications of a locale: stackoverflow.com/questions/56497678.

Upvotes: 1

Related Questions