Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

COUNTABLE_LIST_UNIV (new) and CARD_COUNTABLE_CONG (fixed) #1269

Merged
merged 1 commit into from
Jul 11, 2024
Merged

COUNTABLE_LIST_UNIV (new) and CARD_COUNTABLE_CONG (fixed) #1269

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 39 additions & 7 deletions src/pred_set/src/more_theories/cardinalScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ open HolKernel Parse boolLib bossLib mesonLib
open boolSimps pred_setTheory set_relationTheory tautLib

open prim_recTheory arithmeticTheory numTheory numLib pairTheory
open optionTheory sumTheory ind_typeTheory wellorderTheory;
open optionTheory sumTheory ind_typeTheory wellorderTheory hurdUtils;

val _ = new_theory "cardinal";

Expand Down Expand Up @@ -3005,13 +3005,19 @@ Proof
metis_tac[FINITE_EXPONENT_SETEXP_COUNTABLE]
QED

val CARD_EQ_COUNTABLE = store_thm ("CARD_EQ_COUNTABLE",
``!s:'a->bool t:'a->bool. COUNTABLE t /\ s =_c t ==> COUNTABLE s``,
REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]);
(* NOTE: Changed the type of β€˜t’ to β€˜:'b->bool’ (was: 'a->bool) *)
Theorem CARD_EQ_COUNTABLE :
!s:'a->bool t:'b->bool. COUNTABLE t /\ s =_c t ==> COUNTABLE s
Proof
REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]
QED

val CARD_COUNTABLE_CONG = store_thm ("CARD_COUNTABLE_CONG",
``!s:'a->bool t:'a->bool. s =_c t ==> (COUNTABLE s <=> COUNTABLE t)``,
REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]);
(* NOTE: Changed the type of β€˜t’ to β€˜:'b->bool’ (was: 'a->bool) *)
Theorem CARD_COUNTABLE_CONG :
!s:'a->bool t:'b->bool. s =_c t ==> (COUNTABLE s <=> COUNTABLE t)
Proof
REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN MESON_TAC[CARD_LE_COUNTABLE]
QED

val COUNTABLE_RESTRICT = store_thm ("COUNTABLE_RESTRICT",
``!s P. COUNTABLE s ==> COUNTABLE {x | x IN s /\ P x}``,
Expand Down Expand Up @@ -3187,6 +3193,32 @@ Proof
ASM_SET_TAC[]
QED

(* cf. listTheory.INFINITE_LIST_UNIV |- INFINITE univ(:'a list) *)
Theorem COUNTABLE_LIST_UNIV :
countable univ(:'a) ==> countable univ(:'a list)
Proof
rw [UNIV_list]
>> MP_TAC (INST [β€œA :'a set” |-> β€œuniv(:'a)”] list_BIGUNION_EXP)
>> qmatch_abbrev_tac β€˜list univ(:'a) =~ s ==> _’
>> DISCH_TAC
>> Suff β€˜countable s’
>- (MP_TAC (Q.SPEC β€˜s’ (INST_TYPE [β€œ:'b” |-> β€œ:num # (num -> 'a)”]
(ISPEC β€œlist univ(:'a)” CARD_EQ_COUNTABLE))) \\
rw [])
>> qunabbrev_tac β€˜s’
>> MATCH_MP_TAC COUNTABLE_BIGUNION >> rw []
>> MATCH_MP_TAC COUNTABLE_CROSS >> rw []
>> rw [countable_setexp]
QED

Theorem COUNTABLE_LIST_UNIV' :
FINITE univ(:'a) ==> countable univ(:'a list)
Proof
DISCH_TAC
>> MATCH_MP_TAC COUNTABLE_LIST_UNIV
>> MATCH_MP_TAC FINITE_IMP_COUNTABLE >> art []
QED

Definition BIGPRODi_def:
BIGPRODi (A : 'i -> ('a -> bool) option) =
{tup : 'i -> 'a option |
Expand Down
2 changes: 0 additions & 2 deletions src/pred_set/src/more_theories/topologyScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ open boolSimps simpLib mesonLib metisLib pairTheory pairLib tautLib combinTheory

val _ = new_theory "topology";

fun MESON ths tm = prove(tm,MESON_TAC ths);
fun METIS ths tm = prove(tm,METIS_TAC ths);

fun K_TAC _ = ALL_TAC;
Expand All @@ -41,7 +40,6 @@ fun wrap a = [a];
Theorem IMP_CONJ = cardinalTheory.CONJ_EQ_IMP
Theorem IMP_IMP = boolTheory.AND_IMP_INTRO
Theorem FINITE_SUBSET = pred_setTheory.SUBSET_FINITE_I
Theorem LE_0 = arithmeticTheory.ZERO_LESS_EQ

Theorem FINITE_INDUCT_STRONG :
!P:('a->bool)->bool.
Expand Down
1 change: 0 additions & 1 deletion src/pred_set/src/more_theories/wellorderScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ val _ = new_theory "wellorder"
val _ = temp_delsimps ["NORMEQ_CONV"]

fun K_TAC _ = ALL_TAC;
fun MESON ths tm = prove(tm,MESON_TAC ths);
fun METIS ths tm = prove(tm,METIS_TAC ths);

fun SET_TAC L =
Expand Down
10 changes: 6 additions & 4 deletions src/real/analysis/real_topologyScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16547,12 +16547,14 @@ val UNCOUNTABLE_REAL = store_thm ("UNCOUNTABLE_REAL",
REWRITE_TAC[CANTOR_THM_UNIV] THEN MATCH_MP_TAC CARD_EQ_IMP_LE THEN
ONCE_REWRITE_TAC[CARD_EQ_SYM] THEN REWRITE_TAC[CARD_EQ_REAL]);

val CARD_EQ_REAL_IMP_UNCOUNTABLE = store_thm ("CARD_EQ_REAL_IMP_UNCOUNTABLE",
``!s:real->bool. s =_c univ(:real) ==> ~COUNTABLE s``,
Theorem CARD_EQ_REAL_IMP_UNCOUNTABLE :
!s:real->bool. s =_c univ(:real) ==> ~COUNTABLE s
Proof
GEN_TAC THEN STRIP_TAC THEN
DISCH_THEN (MP_TAC o SPEC ``univ(:real)`` o MATCH_MP
DISCH_THEN (MP_TAC o ISPEC ``univ(:real)`` o MATCH_MP
(SIMP_RULE std_ss [CONJ_EQ_IMP] CARD_EQ_COUNTABLE)) THEN
REWRITE_TAC[UNCOUNTABLE_REAL] THEN ASM_MESON_TAC[CARD_EQ_SYM]);
REWRITE_TAC[UNCOUNTABLE_REAL] THEN ASM_MESON_TAC[CARD_EQ_SYM]
QED

(* ------------------------------------------------------------------------- *)
(* Cardinalities of various useful sets. *)
Expand Down