1(* Define the type of hereditarily finite sets. 2 3 Single (recursive) constructor is 4 5 fromSet : hfs set -> hfs 6 7 where the set must be finite. (Perhaps an argument to have a finite set 8 type in the core distribution?) 9 10 Because there is just one constructor, there is a total inverse to 11 fromSet, called toSet 12 13 toSet : hfs -> hfs set 14 15 where we have 16 17 fromSet (toSet h) = h 18 19 Future work: 20 - define empty hfs value 21 - define other operations such as insert, intersection, union and 22 cardinality 23 - prove induction principle 24 - prove recursion principle 25 26 The type is defined via a cute bijection (due to Ackermann 27 according to Wikipedia) with the natural numbers. 28 29 Inspired to do this by Larry Paulson's talk about using h.f. sets 30 as part of a mechanisation of automata theory at CADE 2015. There (in 31 Isabelle/HOL), the type definition mechanism can create the type 32 directly so the Ackermann bijection is not required. 33*) 34 35open HolKernel Parse boolLib bossLib; 36 37open lcsymtacs 38open pred_setTheory 39 40val _ = new_theory "hfs"; 41 42val _ = ParseExtras.tight_equality() 43 44val _ = temp_overload_on ("mk", ``SUM_IMAGE ((EXP) 2)``) 45 46val numeq_wlog = prove( 47 ``���P. (���n m. P n m ��� P m n) ��� (���n m. P n m ��� n ��� m) ��� 48 (���n m. P n m ��� (n = m))``, 49 metis_tac [DECIDE ``���n m. n ��� m ��� m ��� n ��� m = n``]); 50 51val strictly_increasing_SUC_extends = prove( 52 ``(���n. f n < f (n + 1)) ��� (���n m. n < m ��� f n < f m)``, 53 strip_tac >> Induct_on `m` >> simp[] >> rpt strip_tac >> 54 rename1 `n < SUC m` >> 55 `n = m ��� n < m` by simp[] >> 56 simp[arithmeticTheory.ADD1] >> 57 metis_tac [DECIDE ``���m n p. m < n ��� n < p ��� m < p``]); 58 59val strictly_increasing_injective = prove( 60 ``(���n. f n < f (n + 1)) ��� ���n1 n2. f n1 = f n2 ��� n1 = n2``, 61 simp[EQ_IMP_THM] >> rpt strip_tac >> 62 qspec_then `��n m. f n = f m` (irule o BETA_RULE) numeq_wlog >> 63 qexists_tac `f` >> simp[] >> spose_not_then strip_assume_tac >> 64 rename1 `��(n ��� m)` >> `m < n` by simp[] >> 65 `f m < f n` by metis_tac [strictly_increasing_SUC_extends] >> 66 metis_tac[DECIDE ``��(x < x)``]); 67 68val strictly_increasing_nobounds = prove( 69 ``(���n. f n < f (n + 1)) ��� ���b. ���n. b < f n``, 70 rpt strip_tac >> spose_not_then strip_assume_tac >> 71 rename1 `bnd < f _` >> 72 `���n. f n ��� bnd` by metis_tac[DECIDE ``��(x < y) ��� y ��� x``] >> 73 `���n m. f n = f m ��� n = m` by metis_tac[strictly_increasing_injective] >> 74 `INJ f (count (bnd + 2)) (count (bnd + 1))` 75 by simp[INJ_DEF, DECIDE ``x < y + 1 ��� x ��� y``] >> 76 `FINITE (count (bnd + 1))` by simp[] >> 77 `CARD (count (bnd + 1)) < CARD (count (bnd + 2))` by simp[] >> 78 metis_tac[PHP]); 79 80val TWO_EXP_BOUNDS = prove( 81 ``���n. ���j. n < 2 ** j``, 82 match_mp_tac strictly_increasing_nobounds >> simp[arithmeticTheory.EXP_ADD]); 83 84val bound_exists = prove( 85 ``���n. n < 2 ** (LEAST m. n < 2 ** m) ��� 86 ���p. p < (LEAST m. n < 2 ** m) ��� 2 ** p ��� n``, 87 qx_gen_tac `n` >> 88 qspec_then `��m. n < 2 ** m` 89 (match_mp_tac o SIMP_RULE (srw_ss()) [arithmeticTheory.NOT_LESS]) 90 whileTheory.LEAST_EXISTS_IMP >> 91 metis_tac[TWO_EXP_BOUNDS]); 92 93val mk_minimum = prove( 94 ``���s. FINITE s ��� ���j. j ��� s ��� 2 ** j ��� mk s``, 95 ho_match_mp_tac FINITE_INDUCT >> simp[] >> 96 dsimp[SUM_IMAGE_THM, DELETE_NON_ELEMENT_RWT] >> 97 rpt strip_tac >> res_tac >> simp[]); 98 99val mk_onto = prove( 100 ``���n. ���s. FINITE s ��� mk s = n``, 101 completeInduct_on `n` >> 102 qspec_then `n` strip_assume_tac bound_exists >> 103 qabbrev_tac `m = LEAST m. n < 2 EXP m` >> 104 Cases_on `m = 0` 105 >- (fs[] >> `n = 0` by simp[] >> qexists_tac `���` >> 106 simp[SUM_IMAGE_THM]) >> 107 `m - 1 < m` by simp[] >> 108 `2 ** (m - 1) ��� n` by simp[] >> 109 qabbrev_tac `M = 2 ** (m - 1)` >> 110 `0 < M` by simp[Abbr`M`] >> 111 `n - M < n` by simp[] >> 112 `���s0. FINITE s0 ��� mk s0 = n - M` by metis_tac[] >> 113 qexists_tac `(m - 1) INSERT s0` >> 114 simp[SUM_IMAGE_THM] >> 115 Cases_on `m - 1 ��� s0` 116 >- (`M ��� mk s0` by metis_tac[mk_minimum] >> 117 `2 * M ��� n` by simp[] >> 118 `2 * M = 2 ** m` suffices_by simp[] >> 119 simp[Abbr`M`] >> fs[GSYM arithmeticTheory.EXP] >> 120 `SUC (m - 1) = m` by simp[] >> lfs[]) >> 121 simp[DELETE_NON_ELEMENT_RWT]); 122 123val split_sets = prove( 124 ``s1 = (s1 ��� s2) ��� (s1 DIFF s2)``, 125 simp[EXTENSION] >> metis_tac[]); 126 127val DISJOINT_DIFF = prove( 128 ``DISJOINT (s1 DIFF s2) (s2 DIFF s1)``, 129 simp[DISJOINT_DEF, EXTENSION] >> metis_tac[]); 130 131val DIFF_NONEMPTY = prove( 132 ``s1 ��� s2 ��� s1 DIFF s2 ��� ��� ��� s2 DIFF s1 ��� ���``, 133 simp[EXTENSION] >> metis_tac[]); 134 135val disjoint_inequal_has_maximum = prove( 136 ``FINITE s1 ��� FINITE s2 ��� DISJOINT s1 s2 ��� s1 ��� s2 ��� 137 (���m. m ��� s1 ��� (���n. n ��� s2 ��� n < m)) ��� 138 (���m. m ��� s2 ��� (���n. n ��� s1 ��� n < m))``, 139 Cases_on `s1 = ���` 140 >- (simp[] >> strip_tac >> 141 `���m s0. s2 = m INSERT s0` by metis_tac[SET_CASES] >> dsimp[]) >> 142 Cases_on `s2 = ���` >> simp[] 143 >- (`���m s0. s1 = m INSERT s0` by metis_tac[SET_CASES] >> dsimp[]) >> 144 qabbrev_tac `m1 = MAX_SET s1` >> 145 qabbrev_tac `m2 = MAX_SET s2` >> 146 strip_tac >> 147 `m1 ��� s1 ��� (���a. a ��� s1 ��� a ��� m1) ��� m2 ��� s2 ��� (���b. b ��� s2 ��� b ��� m2)` 148 by metis_tac[MAX_SET_DEF] >> 149 Cases_on `m1 < m2` 150 >- (disj2_tac >> qexists_tac `m2` >> simp[] >> rpt strip_tac >> res_tac >> 151 simp[]) >> 152 disj1_tac >> qexists_tac `m1` >> simp[] >> rpt strip_tac >> 153 `m1 ��� m2` by (strip_tac >> fs[DISJOINT_DEF, EXTENSION] >> metis_tac[]) >> 154 res_tac >> simp[]); 155 156val topdown_induct = prove( 157 ``P ��� ��� 158 (���e s0. P s0 ��� e ��� s0 ��� (���n. n ��� s0 ��� n < e) ��� FINITE s0 ��� 159 P (e INSERT s0)) ��� 160 (���s. FINITE s ��� P s)``, 161 strip_tac >> gen_tac >> Induct_on `CARD s` 162 >- (rpt strip_tac >> `s = ���` by metis_tac[CARD_EQ_0] >> simp[]) >> 163 rpt strip_tac >> `s ��� ���` by (strip_tac >> fs[]) >> 164 qabbrev_tac `M = MAX_SET s` >> 165 `M ��� s ��� ���n. n ��� s ��� n ��� M` by metis_tac[MAX_SET_DEF] >> 166 `s = M INSERT (s DELETE M)` by metis_tac[INSERT_DELETE] >> 167 qabbrev_tac `s0 = s DELETE M` >> 168 `M ��� s0 ��� FINITE s0` by simp[Abbr`s0`] >> 169 rename1 `SUC n = CARD s` >> 170 `CARD s = SUC (CARD s0)` by simp[] >> 171 `n = CARD s0` by simp[] >> 172 `P s0` by metis_tac[] >> 173 `���n. n ��� s0 ��� n < M` 174 by (fs[] >> metis_tac[DECIDE ``x ��� y ��� x ��� y ��� x < y``]) >> 175 metis_tac[]); 176 177val mk_upper_bound = prove( 178 ``���s. FINITE s ��� ���b. (���n. n ��� s ��� n < b) ��� mk s < 2 ** b``, 179 ho_match_mp_tac topdown_induct >> 180 dsimp[SUM_IMAGE_THM, DELETE_NON_ELEMENT_RWT] >> rpt strip_tac >> 181 rename1 `e ��� s` >> 182 `mk s < 2 ** e` by metis_tac[] >> 183 rename1 `e < b` >> 184 `���d. b = SUC d + e` by metis_tac[arithmeticTheory.LESS_STRONG_ADD] >> 185 simp[arithmeticTheory.EXP_ADD, arithmeticTheory.EXP] >> 186 match_mp_tac arithmeticTheory.LESS_LESS_EQ_TRANS >> 187 qexists_tac `2 * 2 ** e` >> simp[]); 188 189val mk_11 = prove( 190 ``FINITE s1 ��� FINITE s2 ��� (mk s1 = mk s2 ��� s1 = s2)``, 191 simp[EQ_IMP_THM] >> rpt strip_tac >> 192 spose_not_then strip_assume_tac >> 193 qabbrev_tac `c = s1 ��� s2` >> 194 qabbrev_tac `t1 = s1 DIFF s2` >> 195 qabbrev_tac `t2 = s2 DIFF s1` >> 196 `s1 = c ��� t1 ��� s2 = c ��� t2` by metis_tac[split_sets, INTER_COMM] >> 197 `FINITE c ��� FINITE t1 ��� FINITE t2` by simp[Abbr`c`, Abbr`t1`, Abbr`t2`] >> 198 `c ��� t1 = ��� ��� c ��� t2 = ���` 199 by (simp[Abbr`c`, Abbr`t1`, Abbr`t2`, EXTENSION] >> metis_tac[]) >> 200 `mk s1 = mk c + mk t1 ��� mk s2 = mk c + mk t2` 201 by (rpt BasicProvers.VAR_EQ_TAC >> 202 Q.UNDISCH_THEN `mk (c ��� t1) = mk (c ��� t2)` kall_tac >> 203 simp[SUM_IMAGE_UNION, SUM_IMAGE_THM]) >> 204 `mk t1 = mk t2` by simp[] >> 205 `DISJOINT t1 t2` by metis_tac[DISJOINT_DIFF] >> 206 `t1 ��� t2` by metis_tac[] >> 207 `(���m1. m1 ��� t1 ��� (���n. n ��� t2 ��� n < m1)) ��� 208 (���m2. m2 ��� t2 ��� (���n. n ��� t1 ��� n < m2))` 209 by metis_tac[disjoint_inequal_has_maximum] 210 >- (`mk t2 < 2 ** m1` by metis_tac[mk_upper_bound] >> 211 `2 ** m1 ��� mk t1` by metis_tac[mk_minimum] >> lfs[]) >> 212 `mk t1 < 2 ** m2` by metis_tac[mk_upper_bound] >> 213 `2 ** m2 ��� mk t2` by metis_tac[mk_minimum] >> lfs[]) 214 215val mk_BIJ = prove( 216 ``BIJ mk {s | FINITE s} univ(:num)``, 217 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, mk_11, mk_onto]); 218 219val hfs = new_type_definition( 220 "hfs", 221 prove(``?x:num. (\x. T) x``, simp[])) 222 223val HFS_TYBIJ = 224 define_new_type_bijections { ABS = "mkHFS", REP = "destHFS", 225 name = "HFS_TYBIJ", tyax = hfs} 226 |> SIMP_RULE (srw_ss()) [] 227 228val mkHFS_11 = store_thm( 229 "mkHFS_11[simp]", 230 ``mkHFS n1 = mkHFS n2 ��� n1 = n2``, 231 metis_tac[HFS_TYBIJ]); 232 233val destHFS_11 = store_thm( 234 "destHFS_11[simp]", 235 ``destHFS h1 = destHFS h2 ��� h1 = h2``, 236 metis_tac[HFS_TYBIJ]); 237 238val toSet_def = Define` 239 toSet hfs = IMAGE mkHFS (LINV mk { s | FINITE s } (destHFS hfs)) 240`; 241 242val LINV_mk_11 = store_thm( 243 "LINV_mk_11[simp]", 244 ``LINV mk {s | FINITE s} x = LINV mk {s | FINITE s} y ��� x = y``, 245 `BIJ (LINV mk {s | FINITE s}) univ(:num) { s | FINITE s}` 246 by simp[BIJ_LINV_BIJ, mk_BIJ] >> 247 fs[BIJ_DEF, INJ_DEF, EQ_IMP_THM]); 248 249val toSet_11 = store_thm( 250 "toSet_11[simp]", 251 ``toSet h1 = toSet h2 ��� h1 = h2``, 252 simp[toSet_def, IMAGE_11]); 253 254val FINITE_toSet = store_thm( 255 "FINITE_toSet[simp]", 256 ``FINITE (toSet h)``, 257 simp[toSet_def] >> 258 `BIJ (LINV mk {s | FINITE s}) univ(:num) { s | FINITE s}` 259 by simp[BIJ_LINV_BIJ, mk_BIJ] >> 260 fs[BIJ_DEF, INJ_DEF]); 261 262val fromSet_def = Define` 263 fromSet s = mkHFS (mk (IMAGE destHFS s)) 264`; 265 266val fromSet_toSet = store_thm( 267 "fromSet_toSet", 268 ``fromSet (toSet h) = h``, 269 simp[fromSet_def, toSet_def] >> simp[GSYM IMAGE_COMPOSE] >> 270 simp[combinTheory.o_DEF, HFS_TYBIJ] >> 271 strip_assume_tac (MATCH_MP BIJ_LINV_INV mk_BIJ) >> fs[HFS_TYBIJ]); 272 273val LINV_mk = prove( 274 ``���s. FINITE s ��� (LINV mk { s | FINITE s} (mk s) = s)``, 275 rpt strip_tac >> irule LINV_DEF >> simp[INJ_DEF, mk_11] >> 276 qexists_tac `IMAGE mk {s | FINITE s}` >> simp[]); 277 278val toSet_fromSet = Q.store_thm( 279 "toSet_fromSet", 280 `���hs. FINITE hs ��� (toSet (fromSet hs) = hs)`, 281 Induct_on `FINITE` >> csimp[toSet_def, fromSet_def, LINV_mk, HFS_TYBIJ]); 282 283val fromSet_11 = Q.store_thm( 284 "fromSet_11", 285 `FINITE s1 ��� FINITE s2 ��� ((fromSet s1 = fromSet s2) ��� (s1 = s2))`, 286 metis_tac[toSet_fromSet]); 287 288val hINSERT_def = Define` 289 hINSERT h1 h2 = fromSet (h1 INSERT toSet h2) 290`; 291 292val hEMPTY_def = Define`hEMPTY = fromSet ���` 293 294val hf_CASES = Q.store_thm( 295 "hf_CASES", 296 `���h. (h = hEMPTY) ��� ���h1 h2. h = hINSERT h1 h2`, 297 gen_tac >> 298 simp_tac bool_ss [GSYM toSet_11, hEMPTY_def, hINSERT_def, toSet_fromSet, 299 FINITE_EMPTY, FINITE_INSERT, FINITE_toSet] >> 300 `toSet h = ��� ��� ���e s. toSet h = e INSERT s` by metis_tac[SET_CASES] >> 301 simp[] >> 302 `FINITE (toSet h)` by simp[] >> 303 `FINITE s` by metis_tac[FINITE_INSERT] >> 304 map_every qexists_tac [`e`, `fromSet s`] >> simp[toSet_fromSet]) 305 306val hINSERT_NEQ_hEMPTY = Q.store_thm( 307 "hINSERT_NEQ_hEMPTY[simp]", 308 `hINSERT h hs ��� hEMPTY`, 309 simp[hINSERT_def, hEMPTY_def, fromSet_11]); 310 311val hINSERT_hINSERT = Q.store_thm( 312 "hINSERT_hINSERT", 313 `hINSERT x (hINSERT x s) = hINSERT x s`, 314 simp[hINSERT_def, toSet_fromSet]); 315 316val hINSERT_COMMUTES = Q.store_thm( 317 "hINSERT_COMMUTES", 318 `hINSERT x (hINSERT y s) = hINSERT y (hINSERT x s)`, 319 simp[hINSERT_def, toSet_fromSet] >> metis_tac[INSERT_COMM]); 320 321val hIN_def = Define` 322 hIN h hs ��� (hINSERT h hs = hs) 323`; 324 325val hIN_toSet = Q.store_thm( 326 "hIN_toSet", 327 `hIN h hs ��� h ��� toSet hs`, 328 simp[hIN_def, hINSERT_def] >> eq_tac 329 >- (disch_then (mp_tac o Q.AP_TERM `toSet`) >> 330 simp_tac bool_ss [toSet_fromSet, FINITE_INSERT, FINITE_toSet] >> 331 simp[ABSORPTION]) >> 332 simp[ABSORPTION, fromSet_toSet]); 333 334val hIN_hEMPTY = Q.store_thm( 335 "hIN_hEMPTY[simp]", 336 `��(hIN h hEMPTY)`, 337 simp[hIN_def]); 338 339val hIN_hINSERT = Q.store_thm( 340 "hIN_hINSERT[simp]", 341 `hIN h1 (hINSERT h2 hs) ��� (h1 = h2) ��� hIN h1 hs`, 342 simp[hIN_def] >> simp[hINSERT_def, fromSet_11, toSet_fromSet] >> 343 simp[GSYM ABSORPTION, EQ_IMP_THM] >> rpt strip_tac >> simp[] >> 344 metis_tac[toSet_11, toSet_fromSet, ABSORPTION, FINITE_INSERT, FINITE_toSet]); 345 346val _ = hide "mk" 347 348val _ = export_theory(); 349