*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] FuncSet without extensional?*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Sun, 19 Sep 2010 00:13:44 +0200*In-reply-to*: <4C951E07.7050702@in.tum.de>*References*: <1284833910.14778.10.camel@kirk> <4C951E07.7050702@in.tum.de>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Hi, points taken. I’ll try with a definition homr here, combining hom and extensional. But assuming one would give hom or iso more structure (e.g. a group structure), then demanding extensionality would be required, e.g. for the uniqueness of \<one>. BTW, are there already theories about uncountable sets? I’d need, as a lemma, the fact that the M* (the set of finite words) of a uncountably infinte set M has the same cardinality. Thanks, Joachim Am Samstag, den 18.09.2010, 22:16 +0200 schrieb Tobias Nipkow: > Since this is a library theory, you can expect a number of client > theories to break if you make such a drastic change. For example > > lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" > > within FuncSet would no longer hold, although it is a standard law about > function spaces. > > At the moment users have the choice: they can always adjoin > "extensional" in their context if needed. Your suggestion deprives them > of that choice. > > Tobias > > Joachim Breitner schrieb: > > Hi, > > > > I was trying to prove the statement that there is a bijection between > > Hom(F(X),C2) and Pow(X). I started with > > "∃ f. bij_betw f (Pow X) (hom (ℱ\<^bsub>X\<^esub>) C2)" > > and it went relatively well... until I noticed that hom is not suitable > > here. Group.hom is defined via FuncSet.Pi, which has the following > > definition: > > > > Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where > > "Pi A B = {f. ∀x. x ∈ A --> f x ∈ B x}" > > (With an abbreviation A -> B). > > > > This means that for example ({} -> {}) is not a one-element-set, but is > > actually the set UNIV::('a -> 'b). > > > > Right below the definition of Pi, there is a predicate specifying that > > functions are undefined outside their definition: > > > > definition > > extensional :: "'a set => ('a => 'b) set" where > > "extensional A = {f. ∀x. x~:A --> f x = undefined}" > > > > For my current goal, it would be great if this were part of the > > definition of Pi. Would this be generally useful? Or are there hard > > reasons not to require "extensional A" for function in "A -> B"? > > > > Thanks, > > Joachim > > > > > > -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de

**Attachment:
signature.asc**

**Follow-Ups**:**[isabelle] Cardinality in HOL (Was: FuncSet without extensional?)***From:*Joachim Breitner

**References**:**[isabelle] FuncSet without extensional?***From:*Joachim Breitner

**Re: [isabelle] FuncSet without extensional?***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] FuncSet without extensional?
- Next by Date: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)
- Previous by Thread: Re: [isabelle] FuncSet without extensional?
- Next by Thread: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)
- Cl-isabelle-users September 2010 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