Email Gateway (Aug 18 2022 at 19:21): Email Gateway (Aug 18 2022 at 19:21):From: Lawrence Paulson <lp15@cam.ac.uk>
Is anybody aware of a formalisation of the hereditarily finite sets in Isabelle/HOL?
This would be a type hf along with constructors
empty :: hf
insert :: hf => hf => hf
with a membership relation defined by
member x (insert y z) == x=y | member x z
and also satisfying extensionality:
x=y <-> (ALL z. member z x = member z y)
(In Isabelle/ZF, the hereditarily finite sets are precisely the elements of Vset(nat).)
Larry
Email Gateway (Aug 18 2022 at 19:21):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Larry,
The FinFun formalisation in the AFP contains until Isabelle2011-1 defines such a type in theory FinFunSet. Adapting it to the pred/set-distinction, I recently (ID b7aa87989f3a) changed it from sets to predicates, so it is called FinFunPred in the development branch of the AFP.
Actually, it specialises the more general type 'a =>f 'b with constructors
finfun_const :: 'b => ('a =>f 'b)
finfun_update :: ('a =>f 'b) => 'a => 'b => ('a =>f 'b)
and an application operator finfun_apply :: ('a =>f 'b) => 'a => 'b
finfun_apply (finfun_update f x y) z = (if z = x then y else finfun_apply f z
f = g <--> (ALL x. finfun_apply f x = finfun_apply g x)
holds. FinFunSet (or FinFunPred) specialise 'b to bool and thus yield hereditarily finite sets or predicates.
Andreas
Email Gateway (Aug 18 2022 at 19:21):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks, but I believe that you are describing finite sets rather than hereditarily finite sets. I should have mentioned, the membership function should have the following type:
member :: hf => hf => bool
That is, we have one single type rather than separate types of sets and elements.
It sounds like this hasn't been formalised before...?
Larry
Email Gateway (Aug 18 2022 at 19:21):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Larry,
You are right, FinFun sets are ordinary finite sets or predicates.
Andreas
Email Gateway (Aug 18 2022 at 19:21):From: Brian Huffman <huffman@in.tum.de>
I don't know of a pre-existing formalization, but I couldn't resist
looking for a way to formalize this myself. I found an approach that
looks promising:
Start with a "raw" tree datatype using lists instead of finite sets:
datatype hf0 = Node "hf0 list"
(or equivalently, datatype hf0 = Empty | Insert hf0 hf0)
Define a linear order on type hf0 using a lexicographic order on the
lists. Then define a predicate "normal :: hf0 => bool" asserting that
all lists in the whole tree are in strict sorted order. Finally,
define type hf as a subtype:
typedef hf = "{a. normal a}"
I got as far as defining insert and member on type hf, but I didn't
prove extensionality. For this, I guess you would need a lemma stating
that "set xs = set ys ==> xs = ys" for strictly sorted lists xs and
ys. There might be some relevant stuff in List.thy already, but I'm
not sure.
Email Gateway (Aug 18 2022 at 19:22):From: Andrei Popescu <uuomul@yahoo.com>
Dear Larry,
We (Dmitriy Traytel, Jasmin Blanchette and myself) are prototyping a new (co)datatype package for Isabelle/HOL allowing for nonfree type constructors. With this package, hereditarily finite sets can simply be defined as
datatype hfset = Fold hfset fset
where 'a fset is the type of finite sets, as defined, e.g., in HOL/Quotient_Examples/FSet.
The package proves the expected distinctness, cases, induction and recursion theorems. However, it is currently in a rather raw form. I have used the package to define the type "hfset". To avoid any dependency on our files, I have extracted the relevant types, constants and theorems in the attached theory HFSET.thy that only depends on HOL/Quotient_Examples/FSet. If you are interested, we can also send you the proved version including its prerequisites.
The package can also be used to define things like finite possibly non-well-founded sets, as
codatatype hfset = Fold hfset fset
or heredinarily k-sets, where k is a fixed cardinal.
All the best, Andrei
PS: The attached paper describes the new package.
HFSET.thy
codat.pdf
Last updated: Apr 20 2024 at 08:16 UTC