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.