*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] domain of function*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Fri, 16 Feb 2007 12:57:52 +0100*Cc*: "Kobayashi, Hidetsune" <hd_coba at yahoo.co.jp>*In-reply-to*: <45D4DC3D.5000206@yahoo.co.jp>*References*: <45D4DC3D.5000206@yahoo.co.jp>*User-agent*: KMail/1.8

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

**Follow-Ups**:**Re: [isabelle] domain of function***From:*Kobayashi, Hidetsune

**References**:**[isabelle] domain of function***From:*Kobayashi, Hidetsune

- Previous by Date: Re: [isabelle] Accessing split-theorems on ML-level
- Next by Date: Re: [isabelle] domain of function
- Previous by Thread: [isabelle] domain of function
- Next by Thread: Re: [isabelle] domain of function
- Cl-isabelle-users February 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list