Email Gateway (Aug 22 2022 at 20:56): Email Gateway (Aug 22 2022 at 20:56):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’d like to announce the following new AFP entry.
Enjoy,
René
Zermelo Fraenkel Set Theory in Higher-Order Logic
by Lawrence C. Paulson
This entry is a new formalisation of ZFC set theory in Isabelle/HOL. It is logically equivalent to Obua's HOLZF; the point is to have the closest possible integration with the rest of Isabelle/HOL, minimising the amount of new notations and exploiting type classes.
There is a type V of sets and a function elts :: V => V set mapping a set to its elements. Classes simply have type V set, and a predicate identifies the small classes: those that correspond to actual sets. Type classes connected with orders and lattices are used to minimise the amount of new notation for concepts such as the subset relation, union and intersection. Basic concepts — Cartesian products, disjoint sums, natural numbers, functions, etc. — are formalised.
More advanced set-theoretic concepts, such as transfinite induction, ordinals, cardinals and the transitive closure of a set, are also provided. The definition of addition and multiplication for general sets (not just ordinals) follows Kirby.
The theory provides two type classes with the aim of facilitating developments that combine V with other Isabelle/HOL types: embeddable, the class of types that can be injected into V (including V itself as well as V*V, etc.), and small, the class of types that correspond to some ZF set.
Email Gateway (Aug 22 2022 at 20:57):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
I’m very happy about this submission, which in particular defines small
types that are closed under function space construction, using the class
system and integrating everything with standard Isabelle/HOL
infrastructure. Thanks a lot to the author.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:57):From: "Dr. Brendan Patrick Mahony" <mahonybp@tpg.com.au>
Congrats on this.
Are there plans to integrate into the datatype package?
In particular, automatic instance proofs for small class closure?
Presumably these follow from the instances already proved, but the datatype representation is confusing to some of us.
Any thoughts on cardinality and the standard HOL semantics?
Cheers,
Brendan
Email Gateway (Aug 22 2022 at 20:57):From: Lawrence Paulson <lp15@cam.ac.uk>
I hope the datatype developers might be persuaded to help with this, at least after these type classes turn out to be useful.
You see, although it occurred to me that they might be useful, I wasn’t able to think up any convincing applications. I’d be glad to hear what you want to use it for.
Larry
Email Gateway (Aug 22 2022 at 20:57):From: Peter Lammich <lammich@in.tum.de>
Hi,
when I saw this entry, a few applications immediately struck my mind.
Apart from HOL models (already mentioned here), it can also be used to
model heaps with arbitrary (small) data on it, similar as
Imperative/HOL does for countable data right now. It would allow a
straightforward extension of Imperative/HOL to support references to
functions.
Less straightforward, but important for my applications, I could store
abstract data types (e.g. sets, sets of sets, etc) on the heap, and
later refine them to more concrete types. Extending my refinement
framework to allow refinement on the heap has been stopped by
difficulties to express the abstract heap so far.
Note that the "deriving"-tool should be straightforward to extend to
infer the "small" typeclass, like it already does for "countable".
Email Gateway (Aug 22 2022 at 20:57):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Larry wrote:
I hope the datatype developers might be persuaded to help with this, at least after these type classes turn out to be useful.
Peter wrote:
Note that the "deriving"-tool should be straightforward to extend to infer the "small" typeclass, like it already does for "countable".
Indeed. I just want to emphasize that such tools can be developed as plugins, without the participation of the datatype developers. Of course, I'd be ready to help to explain the relevant (undocumented) APIs to whoever is willing to implement extensions. I know some users (e.g. in Innsbruck) made sense of the APIs even without help, so it shouldn't be too difficult to master them with a bit of help.
Jasmin
Email Gateway (Aug 22 2022 at 20:58):From: Dominique Unruh <unruh@ut.ee>
Hi,
Note that the "deriving"-tool should be straightforward to extend to infer the "small" typeclass, like it already does for "countable".
I would like to point out that I have already written such a tool (not
in AFP) for a very similar type class (called "universe").
https://github.com/dominique-unruh/qrhl-tool/blob/master/isabelle-thys/Universe.thy
There you can just write "derive universe XXX" for almost any defined
type XXX.
(And I am using it to define a heap with arbitrary types, as Larry
suggested.)
It currently includes ZFHOL instead, but it should be easy to port it to
the new AFP entry.
If anyone has concrete interest in that, I'd be happy to port it to the
new ZF AFP entry. (Otherwise I just put it on my TODO list for "sometime".)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 20:58):From: "Dr. Brendan Patrick Mahony" <mahonybp@tpg.com.au>
Well, the number one thing would to use “string => V” (or some variation thereof) as a tractable model for hierarchical records which would then serve as vehicle for hierarchical abstract systems modelling activities. Existing Isabelle structuring features (theories, locales, records, tuples) are "sort of adequate” for modelling a given well understood system interface instance, but are a positive pain for discussing the mathematics of or even characterising classes of systems and their relationships. Reuse, refactoring and system abstraction …
(BTW well founded sets maybe need a more distinctive type name than V)
Brendan
Last updated: Apr 26 2024 at 04:17 UTC