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
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
