listCardinalityScript.sml
1Theory listCardinality[bare]
2Ancestors pair cardinal list pred_set
3Libs
4 HolKernel Parse boolLib BasicProvers QLib metisLib
5 TotalDefn simpLib boolSimps pred_setLib
6
7fun simp ths = ASM_SIMP_TAC (srw_ss()) ths
8val metis_tac = METIS_TAC
9fun gvs ths =
10 global_simp_tac{elimvars = true, droptrues = true, strip = true,
11 oldestfirst = false} (srw_ss()) ths
12fun rw ths = SRW_TAC[]ths
13
14
15(* ----------------------------------------------------------------------
16 cardinality type results
17 ---------------------------------------------------------------------- *)
18
19Definition list_def:
20 list A = { l | !e. MEM e l ==> e IN A }
21End
22
23Theorem list_EMPTY[simp]: list {} = { [] }
24Proof
25 simp[list_def, EXTENSION] >> Cases >> simp[SF DNF_ss]
26QED
27
28Theorem list_SING: list {e} =~ univ(:num)
29Proof
30 simp[cardeq_def] >> qexists_tac `LENGTH` >>
31 simp[list_def, BIJ_IFF_INV] >>
32 qexists_tac `GENLIST (K e)` >> simp[MEM_GENLIST, SF DNF_ss] >>
33 Induct >> simp[GENLIST_CONS]
34QED
35
36Theorem UNIV_list:
37 univ(:'a list) = list (univ(:'a))
38Proof simp[EXTENSION, list_def]
39QED
40
41Theorem list_BIGUNION_EXP:
42 list A =~ BIGUNION (IMAGE (\n. {n} CROSS (A ** count n)) univ(:num))
43Proof
44 match_mp_tac cardleq_ANTISYM >> simp[cardleq_def] >> conj_tac
45 >- (simp[INJ_DEF, list_def, SF DNF_ss] >>
46 qexists ‘\l. (LENGTH l, (λn. if n < LENGTH l then EL n l else ARB))’ >>
47 simp[] >>
48 conj_tac
49 >- (qx_gen_tac `l` >> strip_tac >>
50 simp[set_exp_def] >> metis_tac[MEM_EL]) >>
51 simp[FUN_EQ_THM, LIST_EQ_REWRITE] >>
52 metis_tac[numLib.DECIDE ``(x = y) <=> ~(x < y) /\ ~(y < x)``]) >>
53 qexists ‘λ(n,f). GENLIST f n’ >>
54 simp[INJ_DEF, set_exp_def, FORALL_PROD, PULL_EXISTS] >> conj_tac
55 >- simp[list_def, MEM_GENLIST, PULL_EXISTS] >>
56 rpt gen_tac >> strip_tac >>
57 disch_then (fn th => assume_tac th >> mp_tac (Q.AP_TERM ‘LENGTH’ th)) >>
58 simp_tac (srw_ss()) [] >> strip_tac >> gvs[] >>
59 gvs[LIST_EQ_REWRITE] >> metis_tac[]
60QED
61
62Theorem set_exp_count:
63 A ** count n =~ { l | (LENGTH l = n) /\ !e. MEM e l ==> e IN A }
64Proof
65 simp[cardeq_def, BIJ_IFF_INV] >>
66 qexists `\f. GENLIST f n` >> simp[MEM_GENLIST] >>
67 conj_tac
68 >- (qx_gen_tac `f` >> simp[set_exp_def, SF DNF_ss] >> rpt strip_tac >>
69 res_tac >> simp[]) >>
70 qexists ‘λl m. if m < n then EL m l else ARB’ >> rpt conj_tac
71 >- (simp[] >> qx_gen_tac `l` >> strip_tac >>
72 simp[set_exp_def] >> metis_tac [MEM_EL])
73 >- (qx_gen_tac `f` >> rw[set_exp_def] >> simp[FUN_EQ_THM] >>
74 qx_gen_tac `m` >> rw[] >> res_tac >> simp[]) >>
75 simp[combinTheory.o_ABS_R] >> qx_gen_tac `l` >> strip_tac >>
76 match_mp_tac LIST_EQ >> simp[]
77QED
78
79Theorem INFINITE_A_list_BIJ_A:
80 INFINITE A ==> list A =~ A
81Proof
82 strip_tac >>
83 assume_tac list_BIGUNION_EXP >>
84 `BIGUNION (IMAGE (\n. {n} CROSS (A ** count n)) univ(:num)) =~ A`
85 suffices_by metis_tac[cardeq_TRANS] >>
86 match_mp_tac cardleq_ANTISYM >> reverse conj_tac
87 >- (simp[cardleq_def] >>
88 qexists_tac ‘\e. (1, λn. if n = 0 then e else ARB)’ >>
89 simp[INJ_DEF, set_exp_def, PULL_EXISTS] >>
90 simp[FUN_EQ_THM] >> metis_tac[]) >>
91 match_mp_tac CARD_BIGUNION >> simp[SF DNF_ss] >> conj_tac
92 >- simp[IMAGE_cardleq_rwt, GSYM INFINITE_Unum] >>
93 qx_gen_tac `n` >> Cases_on `0 < n` >> gvs[]
94 >- metis_tac[CARDEQ_SUBSET_CARDLEQ, exp_count_cardeq, cardeq_SYM,
95 CARDEQ_CROSS_1, cardeq_TRANS] >>
96 simp[EMPTY_set_exp, INFINITE_cardleq_INSERT]
97QED
98
99(* cf. INFINITE_LIST_UNIV |- INFINITE univ(:'a list) *)
100Theorem COUNTABLE_LIST_UNIV :
101 countable univ(:'a) ==> countable univ(:'a list)
102Proof
103 rw [UNIV_list] >>
104 qspec_then ‘univ(:'a)’ mp_tac (GEN_ALL list_BIGUNION_EXP) >>
105 qmatch_abbrev_tac ‘list univ(:'a) =~ s ==> _’ >>
106 strip_tac >>
107 ‘countable s’ suffices_by metis_tac[CARD_EQ_COUNTABLE] >>
108 qunabbrev_tac ‘s’ >>
109 irule COUNTABLE_BIGUNION >> rw [] >>
110 irule COUNTABLE_CROSS >>
111 rw [countable_setexp]
112QED
113
114Theorem COUNTABLE_LIST_UNIV' :
115 FINITE univ(:'a) ==> countable univ(:'a list)
116Proof
117 simp[FINITE_IMP_COUNTABLE, COUNTABLE_LIST_UNIV]
118QED