Dear Roger, Many thanks for the reply to my message.

## Advertising

> It seems odd for an alphabet to be a set of names, > it sounds more like a set of characters from which > one might form names as sequences.

`Yes, the initial model I used was more abstract in that NAMES did not`

`have an identity e.g. as a string. I recently changed the model to give`

`names a proper identity as a sequence of characters, so the below issue`

`does not exists anymore - infinity should be provable here. I was`

`interested to settle an answer nevertheless.`

> I'm puzzled where this came from. > In ProofPower when you introduce a given set NAME you get a > new HOL type z'NAME (as you say) about which nothing is specified > (but all types are non-empty), and you get a new Z constant NAME > defined by NAME = BBU. > BBU (the double bold U symbol) is difficult to unpick because > for Z it behaves as a primitive, but it is in fact the set of > all elements of the type x'NAME. The proof system knows enough > about BBU that you should not need to think about what's happening > underneath but simply understand that it is the set of all elements > of some type, and the type will be determined by type inference.

`Yes, when taking BBU apart one can verify that it is just an`

`abbreviation for Totality (instantiated for some suitable type), which`

`in turn is equated with Universe (instantiated for some suitable type).`

`(Actually that's not quite true, the actual Z characterisation of BBU is`

`"(Totality).1" but the tuple construction and selection will in effect`

`cancel each other out). The axiom for the universe is given by the the`

`definition of "Universe" in the HOL sets theory, and determine the`

`(sole) properties of the carrier set. It is what I was referring to.`

> Though it might be better in this case to use > > F NAME propersubsetof P NAME

`Great, that would be a better choice of infinity axiom to prove the`

`property I needed. As you suggest, there should be no issue about`

`writing the infinity axiom in a certain way, best to chose whatever is`

`more convenient for proof.`

> Yes. However, you should not really need to know any of the > stuff about how this is done in HOL. > The given sets are implemented as they should be in Z > and U is well understood by the Z proof contexts.

`Yes, I needed to dig a bit deeper just to verify what you confirmed in`

`the email, it might have been quicker to look at the Z standard ;-) . As`

`you said, in general there is no need to go down to the level of HOL`

`when reasoning about Z sets, but as a side note this appear not always`

`to be so. For example, to prove theorems about set or sequence`

`enumerations, e.g. all enumerated sets are finite, I had to decent to`

`the level of HOL. Also I have been developing some more elaborate`

`normalisation conversions for Z sets, and the constructor functions`

`sort_conv and poly_conv usually only work with HOL functions. (There is`

`a minor issue with poly_conv and sort_conv as these conversion only work`

`for functions whose types are fully qualified, I will posting another`

`message to make a suggestion here ;-) . Since the HOL choice functions`

`(Choose) is not lifted to Z sets, incorporating it in a prove benefits`

`from a conversion that either lifts all set expressions into Z or HOL`

`sets. My experience so far is that for the common stuff it is not`

`necessary to worry about underlying HOL encodings, but for the more`

`fancy things it is difficult to avoid it.`

> The place to look for theorems about finiteness is in > the maths examples, wrk073.pdf, not part of the standard > distribution. > However, this is all HOL, so to use it in Z you will need > to understand the relations between HOL and Z.

`Many thanks for the reference. Yes, no problem. I implemented two`

`conversions that negotiated between Z and HOL sets, hence it should be`

`easy to use HOL laws if needed.`

> However, I'm not convinced that you need it for the purposes > described. If you just add the constraint I mentioned above > then you should always be able to find new elements (I suppose > you need to know that the union of two finite sets is finite).

`I managed to find a general theorem in "z_numbers1" that states that the`

`generalised union of a finite number of finite sets is finite, for`

`convenience I specialised it for the binary case.`

> A proof context would be nice!

`Certainly, I will try and play around with this. Wrapping all relevant`

`theorems in a component proof context and maybe merging with sets_ext`

`could be a nice general solution.`

Thanks once more for the reply, Frank

`PS: Is there, or would it be worth, to maintain a common repository of`

`ProofPower utilities and extensions such as additional conversions,`

`tactics, proof context, normalisations, hacks, little examples "how to`

`do" stuff, etc. implemented and shared by its users? It may not be`

`appropriate to incorporate all of them into the standard distribution,`

`but maybe other users could nevertheless benefit from them (I would`

`certainly be happy to contribute, and be interested in other users'`

`contributions).`

Roger Bishop Jones wrote: > On Tuesday 16 June 2009 14:47:55 Frank Zeyda wrote: >> Dear ProofPower Users, >> >> I have a little observation which I would like to confirm. The problem >> is as follows. I defined a new Z type NAME by >> >> [NAME] >> >> and then introduced a set ALPHABET to refer to the subsets of NAME by >> >> ALPHABET == P NAME > > It seems odd for an alphabet to be a set of names, > it sounds more like a set of characters from which > one might form names as sequences. > >> At some point it showed to be necessary to construct fresh names for any >> given alphabet, i.e. which are not in the alphabet. In that, I attempted >> to prove the following theorem. >> >> FORALL a : ALPHABET @ (EXISTS n : NAME @ n \not \in a) >> >> I assumed it would be sufficient to restrict the set alphabet to finite >> subsets of name, for instance using the following definition for >> ALPHABET instead. >> >> ALPHABET == F NAME >> >> but I think this is not the case. For a new Z type, the defining axiom >> we obtain is that the Z type constant (i.e. NAME) is equal to the >> universe over a certain, newly introduced, HOL type (here z'NAME); a HOL >> constant "Universe" is used to refer to the carrier set of a HOL type. >> It guarantees that any x of the correct (HOL) type is an element of the >> respective (type-instantiated) Universe, that x is not an element of the >> empty set which I suppose excludes the case of an empty universe, and a >> property regarding the Insert functions to reason about enumerated sets. > > I'm puzzled where this came from. > In ProofPower when you introduce a given set NAME you get a > new HOL type z'NAME (as you say) about which nothing is specified > (but all types are non-empty), and you get a new Z constant NAME > defined by NAME = BBU. > BBU (the double bold U symbol) is difficult to unpick because > for Z it behaves as a primitive, but it is in fact the set of > all elements of the type x'NAME. The proof system knows enough > about BBU that you should not need to think about what's happening > underneath but simply understand that it is the set of all elements > of some type, and the type will be determined by type inference. > >> From this alone one cannot prove that the corresponding Universe is >> infinite. > > yes, it might be finite, for all anyone knows. > >> The underlying HOL type of the new Z type, i.e. here "z'NAME >> SET" I think defines a representation function that equates the type of >> a set with functions over some new HOL type into BOOL, but again I think >> this cannot be used to prove that "z'NAME SET" is infinite unless >> "z'NAME" is (?!). > > Yes. The HOL type constructor SET, which is used also for sets in > Z, is represented by propositional functions. In HOL SETs are > just different ways of talking about propositional functions. > (though you can introduce other kinds of set if you like)> > >> In that, I suppose if we want a Z type to be infinite, >> we need to explicitly state it, that is by an axiom along the lines of >> >> EXISTS f : z'NAME -> z'NAME @ (OneOne f) /\ ¬ Onto f >> >> (Similar to the infinity_axiom in the HOL theory init.) > > Though it might be better in this case to use > > F NAME propersubsetof P NAME > >> Or alternatively (maybe more useful when doing the proofs in Z rather >> than HOL) that there exists an injective Z function from N to the >> carrier set of the new type. The only type in ProofPower-Z that >> explicitly claims its infinite seems to be the type IND. > > Though there are many others which are easily seen to be. > e.g. N or seq T for any type T. > >> However, there >> seems no way to prove that for a newly introduce HOL type there is an >> injective function from IND to the elements of that. Even further, it >> seems not possible to prove that there are two distinct elements in a >> newly introduced Z type. For example, the consistency axioms for >> >> | x, y : NAME >> >> ------------- >> >> | x =/= y >> >> Appear not to be provable by the defining axiom for NAME, unless we >> introduce some axiom stating properties of the cardinality of NAME. > > All this is consistent (I believe) with the Z standard. > >> If someone could confirm or refute the above that would be great. > > Yes. However, you should not really need to know any of the > stuff about how this is done in HOL. > The given sets are implemented as they should be in Z > and U is well understood by the Z proof contexts. > >> As a side-issue, I realised the automatic proof support for finite sets >> is not as well developed as that for (possibly infinite) sets. I proved >> a couple of theorems that could be useful, for instance discharging that >> every enumerated set is finite. It may be worth introducing a new Z >> component proof context for finite sets. >

`> The place to look for theorems about finiteness is in the maths`

`examples, wrk073.pdf, not part of the standard`

> distribution. > However, this is all HOL, so to use it in Z you will need > to understand the relations between HOL and Z. > > However, I'm not convinced that you need it for the purposes > described. If you just add the constraint I mentioned above > then you should always be able to find new elements (I suppose > you need to know that the union of two finite sets is finite). > > A proof context would be nice! > > Roger Jones > > > _______________________________________________ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com