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