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