Hi Thomas, thanks! Now I see the chances to solve my problem using sortingTheory.
--Chun Il 25/02/19 20:46, Thomas Sewell ha scritto: > I think that the set type here is irrelevant. You have a relation for > sorting elements in the range of f. Construct the list of applications > of f to 0..(n-1), sort that using the sort operation from sortingTheory, > and make g from the list index operator applied to that. > > Cheers, > Thomas. > > > > Sent from my Samsung Galaxy smartphone. > > > -------- Original message -------- > From: "Chun Tian (binghe)" <binghe.l...@gmail.com> > Date: 25/02/2019 15:02 (GMT+01:00) > To: HOL-info list <hol-info@lists.sourceforge.net> > Subject: [Hol-info] Sorting a finite sequence of disjoint sets? > > Hi, > > suppose I have a finite sequence of n disjoint sets, given by a function > (f :num -> ‘a -> bool), and their union is BIGUNION (IMAGE f (count n)), > and an order R (antisymmetric > , transitive) on these sets. > > Is it possible to assert the existence of another function (g :num -> ‘a > -> bool) such that: > > BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count n)) > > and > > !i j. i < n /\ j < n ==> R (g i) (g j) > > ? > > That’s, I want to “sort” these set according to this order. Does it > exist for sure? Is there anything from the existing “sortingTheory” > that I can leverage? > > Regards, > > Chun Tian >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
