1(*---------------------------------------------------------------------------
2       Mapping finite sets into lists. Needs a constraint that 
3       the set is finite. One might think to introduce this 
4       function via a constant specification, but in this case, 
5       TFL technology makes an easy job of it.
6
7       Also, we define a "fold" for sets. Could be used for accumulating
8       function values through a set, e.g., summing a finite set of 
9       numbers.
10 ---------------------------------------------------------------------------*)
11
12app load ["bossLib", "pred_setTheory"]; 
13open pred_setTheory bossLib; 
14infix 8 by;
15
16(*---------------------------------------------------------------------------
17       Make definition of set2list function.
18 ---------------------------------------------------------------------------*)
19
20val set2list_defn = Hol_defn "set2list"
21  `set2list s = 
22     if FINITE s then 
23        if s={} then []
24        else CHOICE s :: set2list (REST s) 
25     else ARB`;
26
27(*---------------------------------------------------------------------------
28       Termination of set2list.
29 ---------------------------------------------------------------------------*)
30
31val (set2list_eqn0, set2list_ind) =
32 Defn.tprove (set2list_defn,
33   WF_REL_TAC `measure CARD` THEN 
34   PROVE_TAC [CARD_PSUBSET, REST_PSUBSET]);
35
36(*---------------------------------------------------------------------------
37      Desired recursion equation.
38
39      FINITE s |- set2list s = if s = {} then [] 
40                               else CHOICE s::set2list (REST s)
41
42 ---------------------------------------------------------------------------*)
43
44val set2list_eqn = ASM_REWRITE_RULE [ASSUME (Term`FINITE s`)] set2list_eqn0;
45
46
47(*---------------------------------------------------------------------------
48      Map a list into a set.
49 ---------------------------------------------------------------------------*)
50
51val list2set = 
52 Define 
53   `(list2set []     = {}) 
54 /\ (list2set (h::t) = h INSERT (list2set t))`;
55
56
57(*---------------------------------------------------------------------------
58            Some consequences
59 ---------------------------------------------------------------------------*)
60
61val set2list_inv = Q.prove
62(`!s. FINITE s ==> (list2set(set2list s) = s)`,
63 recInduct set2list_ind
64   THEN RW_TAC std_ss [] 
65   THEN ONCE_REWRITE_TAC [set2list_eqn]
66   THEN RW_TAC std_ss [list2set]
67   THEN PROVE_TAC [REST_DEF, FINITE_DELETE, CHOICE_INSERT_REST]);
68
69val set2list_CARD = Q.prove
70(`!s. FINITE s ==> (LENGTH (set2list s) = CARD s)`,
71 recInduct set2list_ind
72   THEN RW_TAC std_ss [] 
73   THEN ONCE_REWRITE_TAC [set2list_eqn]
74   THEN RW_TAC std_ss [listTheory.LENGTH,CARD_EMPTY]
75   THEN RW_TAC std_ss [REST_DEF, FINITE_DELETE]
76   THEN `FINITE (REST s)` by PROVE_TAC [REST_DEF,FINITE_DELETE]
77   THEN PROVE_TAC[CHOICE_INSERT_REST,CARD_INSERT,CHOICE_NOT_IN_REST,REST_DEF]);
78
79val set2list_IN_MEM = Q.prove
80(`!s. FINITE s ==> !x. x IN s = MEM x (set2list s)`,
81 recInduct set2list_ind
82   THEN RW_TAC std_ss [] 
83   THEN ONCE_REWRITE_TAC [set2list_eqn]
84   THEN RW_TAC std_ss [listTheory.MEM,NOT_IN_EMPTY]
85   THEN PROVE_TAC [REST_DEF, FINITE_DELETE, IN_INSERT, CHOICE_INSERT_REST]);
86
87
88(*---------------------------------------------------------------------------
89    A "fold" operation for sets ... unfortunately, totally useless, 
90    since CHOICE and REST don't actually give you things you can work
91    with.
92 ---------------------------------------------------------------------------*)
93
94val itset_defn = Hol_defn "itset"
95  `itset (s:'a->bool) (b:'b) = 
96     if FINITE s then 
97        if s={} then b
98        else itset (REST s) (f (CHOICE s) b)
99     else ARB`;
100
101(*---------------------------------------------------------------------------
102       Termination of itset.
103 ---------------------------------------------------------------------------*)
104
105val (itset_eqn0, itset_ind) =
106 Defn.tprove (itset_defn,
107   WF_REL_TAC `measure (CARD o FST)` THEN 
108   PROVE_TAC [CARD_PSUBSET, REST_PSUBSET]);
109
110(*---------------------------------------------------------------------------
111      Desired recursion equation.
112
113      FINITE s |- itset f s b = if s = {} then b 
114                                else itset f (REST s) (f (CHOICE s) b)
115 ---------------------------------------------------------------------------*)
116
117val itset_eqn = ASM_REWRITE_RULE [ASSUME (Term`FINITE s`)] itset_eqn0;
118