*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] domain of function*From*: "Kobayashi, Hidetsune" <hd_coba at yahoo.co.jp>*Date*: Fri, 16 Feb 2007 07:18:37 +0900*User-agent*: Mozilla Thunderbird 0.8 (Windows/20040913)

Hello! Let A be a naive set, then is it true that arbitrary \<in> A ? 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? Hidetsune Kobayashi

**Follow-Ups**:**Re: [isabelle] domain of function***From:*Tjark Weber

- Previous by Date: [isabelle] Post-doc positions at NIA - NASA LaRC
- Next by Date: [isabelle] 1st Call for Papers SecReT 2007
- Previous by Thread: [isabelle] Post-doc positions at NIA - NASA LaRC
- 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