# Re: [isabelle] domain of function

```On Thursday 15 February 2007 23:18, Kobayashi, Hidetsune wrote:
> Let A be a naive set, then is it true that
> arbitrary \<in> A ?

Not necessarily.  You can think of "arbitrary" as a completely unspecified
constant, so unless A = UNIV, you won't be able to prove arbitrary \<in> A.
(Note that you won't be able to prove arbitrary \<notin> A either, unless A =
\<emptyset>.)

> The question arose when I tryed to prove the following:
>
> constdefs
> domain_test::"['a set, nat, nat => 'a] => bool"
> "domain_test A n f == f \<in> extensional {j. j \<le> n} \<and>
> (\<forall>j \<le> n. f j \<in> A)"
>
> lemma test:"[| domain_test A n f; domain_test A m f |] ==> n = m"
>
> Is this lemma true? If this is true, is there any proof?

Assuming that extensional is defined as

"extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}",

the lemma is not true.  The problem is once again that "arbitrary" is just a
name for some specific value; it is not a value on its own that's somehow
magically different from all other values.  So "f j = arbitrary" and "f j
\<in> A" may both be true.

If you want to model partial functions, then another possibility is to use the
"'a option" datatype, with constructors "None" and "Some 'a".  The following
lemma is indeed true, because "None" is provably different from "Some a":

constdefs
domain_test' :: "['a set, nat, nat => 'a] => bool"
"domain_test' A n f == (\<forall>j. n < j --> f j = None) \<and>
(\<forall>j\<le>n. \<exists>a\<in>A. f j = Some a)"

lemma: "[| domain_test' A n f; domain_test' A m f |] ==> n = m"

See theory HOL/Map (http://isabelle.in.tum.de/dist/library/HOL/Map.html) for
existing related syntax and lemmas.  I'm not sure however how well this
approach would go together with the Algebra theories.

Best,
Tjark

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.