veblenScript.sml

1Theory veblen
2Ancestors
3  ordinalBasic ordinal pred_set cardinal
4
5(* Material from Brian Huffman's AFP entry on Ordinal arithmetic *)
6
7Theorem better_induction:
8    !P. P 0 /\ (!a. P a ==> P a^+) /\
9        (!a. 0 < a /\ (!b. b < a ==> P b) ==> P (sup (preds a))) ==>
10        !a. P a
11Proof
12  gen_tac >> strip_tac >> match_mp_tac simple_ord_induction >> simp[] >>
13  qx_gen_tac `a` >> strip_tac >> fs[sup_preds_omax_NONE] >> metis_tac[]
14QED
15
16Definition closed_def:
17  closed A <=> !g. (!n:num. g n IN A) ==> sup { g n | n | T} IN A
18End
19
20Definition unbounded_def:
21  unbounded (A:'a ordinal set) = !a. ?b. b IN A /\ a < b
22End
23
24Definition club_def:  club A <=> closed A /\ unbounded A
25End
26
27Definition continuous_def:
28  continuous f <=>
29    !A:'a ordinal set.
30          A <<= univ(:'a inf) ==> f (sup A) = sup (IMAGE f A)
31End
32
33Definition strict_mono_def:
34  strict_mono f <=> !x y:'a ordinal. x < y ==> f x < f y
35End
36
37val dsimp = asm_simp_tac (srw_ss() ++ boolSimps.DNF_ss)
38
39Theorem nrange_IN_Uinf[simp]:
40    { f n | n:num | T} <<= univ(:'a inf)
41Proof
42  qsuff_tac `countable { f n | n | T }`
43  >- metis_tac[Unum_cle_Uinf, cardleq_TRANS, countable_thm] >>
44  simp[countable_surj] >> disj2_tac >> qexists_tac `f` >>
45  simp[SURJ_DEF] >> metis_tac[]
46QED
47
48Theorem increasing:
49    !f x. strict_mono f /\ continuous f ==> x <= f x
50Proof
51  ntac 3 strip_tac >> qid_spec_tac `x` >>
52  ho_match_mp_tac better_induction >> simp[] >> conj_tac
53  >- (qx_gen_tac `x` >> strip_tac >> simp[ordlt_SUC_DISCRETE] >>
54      qsuff_tac `x < f x^+`
55      >- (simp[ordle_lteq] >> rpt strip_tac >> fs[]) >>
56      match_mp_tac ordlet_TRANS >> qexists_tac `f x` >>
57      fs[strict_mono_def]) >>
58  qx_gen_tac `a` >> strip_tac >> fs[continuous_def, preds_inj_univ] >>
59  simp[sup_thm,preds_inj_univ] >> qx_gen_tac `b` >> Cases_on `a <= b` >>
60  simp[] >> fs[] >> match_mp_tac ordle_TRANS >> qexists_tac `f b` >>
61  simp[] >> match_mp_tac suple_thm >> simp[IMAGE_cardleq_rwt, preds_inj_univ]
62QED
63
64Theorem clubs_exist:
65    strict_mono (f:'a ordinal -> 'a ordinal) /\ continuous f ==>
66      club (IMAGE f univ(:'a ordinal))
67Proof
68  simp[club_def, closed_def, unbounded_def] >> rpt strip_tac >| [
69    qabbrev_tac `ss = { oleast x. g n = f x | n | T }` >>
70    qexists_tac `sup ss` >> `ss <<= univ(:'a inf)` by simp[Abbr`ss`] >>
71    `f (sup ss) = sup (IMAGE f ss)` by fs[continuous_def] >>
72    simp[] >> match_mp_tac sup_eq_sup >>
73    dsimp[IMAGE_cardleq_rwt] >> simp[] >> conj_tac
74    >- (dsimp[Abbr`ss`] >> qx_gen_tac `n` >> qexists_tac `n` >>
75        DEEP_INTRO_TAC oleast_intro >> simp[]) >>
76    dsimp[Abbr`ss`] >> qx_gen_tac `n` >> qexists_tac `n` >>
77    DEEP_INTRO_TAC oleast_intro >> simp[],
78    dsimp[] >> qexists_tac `a^+` >> match_mp_tac ordlet_TRANS >>
79    qexists_tac `f a` >> fs[strict_mono_def, increasing]
80  ]
81QED
82
83Theorem mono_natI:
84    (!n. f n : 'a ordinal <= f (SUC n)) ==> !m n. m <= n ==> f m <= f n
85Proof
86  strip_tac >> Induct_on `n` >> simp[] >> qx_gen_tac `m` >> strip_tac >>
87  Cases_on `m = SUC n` >- simp[] >>
88  `m <= n` by decide_tac >>
89  metis_tac[ordle_TRANS]
90QED
91
92Theorem sup_mem_INTER:
93    (!n. club (A n)) /\ (!n. A (SUC n) SUBSET A n) /\
94    (!n. f n IN A n) /\ (!m n. m <= n ==> f m <= f n) ==>
95    sup {f n | n | T} IN BIGINTER {A n | n | T}
96Proof
97  dsimp[] >> qx_gen_tac `k` >> strip_tac >>
98  `sup { f n | n | T} = sup { f (n + k) | n | T }`
99    by (match_mp_tac sup_eq_sup >> dsimp[] >> simp[] >> conj_tac
100        >- (qx_gen_tac `n` >> qexists_tac `n` >>
101            first_x_assum match_mp_tac >> decide_tac) >>
102        qx_gen_tac `n` >> qexists_tac `k + n` >> simp[]) >>
103  pop_assum SUBST1_TAC >>
104  qsuff_tac `!n. f (n + k) IN A k` >- fs[club_def, closed_def] >>
105  qx_gen_tac `n` >>
106  qsuff_tac `A (n + k) SUBSET A k` >- metis_tac [SUBSET_DEF] >>
107  Induct_on `n` >> simp[arithmeticTheory.ADD_CLAUSES] >>
108  metis_tac [SUBSET_TRANS, DECIDE ``x + y:num = y + x``]
109QED
110
111val smem' = sup_mem_INTER |> SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) []
112                          |> GEN_ALL
113
114Theorem oleast_leq:
115    !P a. P a ==> (oleast) P <= a
116Proof
117  ntac 3 strip_tac >> DEEP_INTRO_TAC oleast_intro >> metis_tac[]
118QED
119
120Theorem club_INTER:
121    (!n. club (A n)) /\ (!n. A (SUC n) SUBSET A n) ==>
122    club (BIGINTER {A n | n | T})
123Proof
124  strip_tac >> simp[club_def] >> conj_tac
125  >- (fs[closed_def, club_def] >> dsimp[]) >>
126  dsimp[club_def, closed_def, unbounded_def] >>
127  qx_gen_tac `a` >> rpt strip_tac >>
128  qexists_tac `sup {oleast b. b IN A n /\ a < b | n | T}` >>
129  conj_tac
130  >- (qx_gen_tac `n` >> ho_match_mp_tac smem' >> simp[] >>
131      conj_tac
132      >- (qx_gen_tac `n` >> DEEP_INTRO_TAC oleast_intro >> simp[] >>
133          fs[club_def, unbounded_def]) >>
134      ho_match_mp_tac mono_natI >> qx_gen_tac `n` >>
135      ho_match_mp_tac oleast_leq >>
136      conj_tac
137      >- (DEEP_INTRO_TAC oleast_intro >> conj_tac
138          >- fs[club_def, unbounded_def] >>
139          metis_tac[SUBSET_DEF]) >>
140      DEEP_INTRO_TAC oleast_intro >> conj_tac
141      >- fs[club_def, unbounded_def] >> simp[]) >>
142  simp[sup_thm] >> dsimp[] >> qexists_tac `n` >>
143  DEEP_INTRO_TAC oleast_intro >> simp[] >> fs[club_def, unbounded_def]
144QED
145