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