# Re: [isabelle] domain of function

```
Thanks, Tjark. The lemma should be true, (if not,
~~~~
there is a function which is equal to a strict
^^^^^^^
restriction of itself).

Hidetsune

--- Tjark Weber <tjark.weber at gmx.de> wrote:

> 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
>
>

--------------------------------------
Start Yahoo! Auction now! Check out the cool campaign
http://pr.mail.yahoo.co.jp/auction/

```

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