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.