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

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. From this alone one cannot prove that the corresponding Universe is infinite. 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 (?!). 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.)

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. 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.

If someone could confirm or refute the above that would be great.

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.

Many Thanks,
Frank

--
 Dr Dipl.-Inform. Frank Zeyda
 Research Associate
 High Integrity Systems Engineering Group
 Department of Computer Science
 University of York (UK)
 Email: ze...@cs.york.ac.uk
 Phone: 0044-(0)1904-433244
 WWW: http://www-users.cs.york.ac.uk/~zeyda/


--
 Dr Dipl.-Inform. Frank Zeyda
 Research Associate
 High Integrity Systems Engineering Group
 Department of Computer Science
 University of York (UK)
 Email: ze...@cs.york.ac.uk
 Phone: 0044-(0)1904-433244
 WWW: http://www-users.cs.york.ac.uk/~zeyda/

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to