countable_typesScript.sml

1Theory countable_types
2Ancestors
3  bool pred_set
4Libs
5  Tactic Tactical
6
7Theorem unit_countable:
8  countable (UNIV : unit set)
9Proof
10  simp [countable_def, INJ_DEF]
11QED
12
13Theorem list_countable:
14  countable Lset <=> countable (BIGUNION (IMAGE set Lset))
15Proof
16  EQ_TAC \\ rw []
17  >- (
18    irule bigunion_countable
19    \\ simp [PULL_EXISTS, image_countable, finite_countable]
20  )
21  \\ qspec_then `IMAGE (\n. {xs | LENGTH xs = n /\
22        EVERY (\x. x IN BIGUNION (IMAGE set Lset)) xs}) UNIV`
23    mp_tac bigunion_countable
24  \\ simp []
25  \\ reverse impl_tac
26  >- (
27    rw [] \\ drule_then irule subset_countable
28    \\ simp [SUBSET_DEF, PULL_EXISTS, listTheory.EVERY_MEM]
29    \\ metis_tac []
30  )
31  \\ simp [PULL_EXISTS]
32  \\ Induct
33  \\ simp []
34  \\ csimp []
35  \\ dxrule_then dxrule cross_countable
36  \\ rw []
37  \\ qspec_then `\xs. (TL xs, HD xs)` irule inj_countable
38  \\ first_assum (irule_at Any)
39  \\ simp [INJ_IFF, listTheory.LENGTH_CONS, PULL_EXISTS]
40  \\ metis_tac []
41QED
42
43Theorem countable_split:
44  ! (X : 'a set) (f : 'a -> (num list # 'a list)) (m : 'a -> num).
45  INJ f X UNIV /\
46  (!x y. x IN X /\ MEM y (SND (f x)) ==> y IN X /\ m y < m x)
47  ==>
48  countable X
49Proof
50  rw []
51  \\ qspec_then `IMAGE (\n. {x | m x < n /\ x IN X}) UNIV`
52    mp_tac bigunion_countable
53  \\ simp []
54  \\ impl_tac
55  >- (
56    simp [PULL_EXISTS]
57    \\ Induct
58    \\ simp []
59    \\ qspec_then `f` irule inj_countable
60    \\ qexists_tac `f`
61    \\ qexists_tac `UNIV CROSS {xs | EVERY (\x. m x < n /\ x IN X) xs}`
62    \\ irule_at Any cross_countable
63    \\ simp [list_countable]
64    \\ drule_then (irule_at Any) subset_countable
65    \\ fs [SUBSET_DEF, PULL_EXISTS, INJ_DEF, listTheory.EVERY_MEM]
66    \\ rw []
67    \\ res_tac
68    \\ simp []
69  )
70  >- (
71    rw []
72    \\ drule_then irule subset_countable
73    \\ simp [SUBSET_DEF, PULL_EXISTS]
74    \\ metis_tac [prim_recTheory.LESS_SUC_REFL]
75  )
76QED