1open HolKernel Parse boolLib bossLib
2open vbgsetTheory
3open boolSimps
4
5val _ = new_theory "vbgnats"
6
7val vSUC_def = Define`vSUC x = x ��� {x}`
8
9val fromNat_def = Define`
10  (fromNat 0 = {}) ���
11  (fromNat (SUC n) = vSUC (fromNat n))
12`;
13val _ = add_numeral_form(#"v", SOME "fromNat")
14
15val inductive_def = Define`
16  inductive A ��� SET A ��� {} ��� A ��� ���x. x ��� A ��� vSUC x ��� A
17`;
18
19val Inductives_def = Define`
20  Inductives = SPEC0 (��A. {} ��� A ��� ���x. x ��� A ��� vSUC x ��� A)
21`;
22
23val inductive_Inductives = store_thm(
24  "inductive_Inductives",
25  ``inductive A ��� A ��� Inductives``,
26  srw_tac [][inductive_def, Inductives_def, SPEC0]);
27
28val Nats_def = Define`
29  Nats = SPEC0 (��n. ���s. inductive s ��� n ��� s)
30`;
31
32val EMPTY_IN_Nats = store_thm(
33  "EMPTY_IN_Nats",
34  ``{} ��� Nats``,
35  rw [Nats_def, SPEC0, inductive_def]);
36
37val vSUC_IN_Nats_I = store_thm(
38  "vSUC_IN_Nats_I",
39  ``n ��� Nats ��� vSUC n ��� Nats``,
40  rw [Nats_def, SPEC0, inductive_def, vSUC_def]);
41
42val SET_fromNat = store_thm(
43  "SET_fromNat",
44  ``SET (fromNat n)``,
45  Induct_on `n` >> srw_tac [][fromNat_def, vSUC_def]);
46val _ = export_rewrites ["SET_fromNat"]
47
48val fromNat_in_Nats = store_thm(
49  "fromNat_in_Nats",
50  ``���n. fromNat n ��� Nats``,
51  Induct THEN SRW_TAC [][fromNat_def] THENL [
52    SRW_TAC [][Nats_def, SPEC0] THEN
53    fs [inductive_def],
54    fs [Nats_def, SPEC0, vSUC_def] >>
55    fs [inductive_def, vSUC_def]
56  ]);
57val _ = export_rewrites ["fromNat_in_Nats"]
58
59val NOT_IN_0 = store_thm(
60  "NOT_IN_0",
61  ``x ��� 0``,
62  SRW_TAC [][fromNat_def]);
63val _ = export_rewrites ["NOT_IN_0"]
64
65val vSUC_NOT_0 = store_thm(
66  "vSUC_NOT_0",
67  ``vSUC n ��� 0``,
68  SRW_TAC [][vSUC_def, EXTENSION] THEN
69  Cases_on `n = 0` THEN SRW_TAC [][] THENL [
70    Q.EXISTS_TAC `0` THEN SRW_TAC [][],
71    METIS_TAC [fromNat_def, EMPTY_UNIQUE]
72  ]);
73val _ = export_rewrites ["vSUC_NOT_0"]
74
75val Nats_SET = store_thm(
76  "Nats_SET",
77  ``SET Nats``,
78  match_mp_tac SUBSETS_ARE_SETS >>
79  strip_assume_tac INFINITY >>
80  qexists_tac `w` >> simp [SUBSET_def] >>
81  qx_gen_tac `n` >> rw [Nats_def] >>
82  first_assum match_mp_tac >> simp [inductive_def] >> conj_tac
83    >- metis_tac [EMPTY_UNIQUE] >>
84  qx_gen_tac `e` >> strip_tac >>
85  `���y. y ��� w ��� ���u. u ��� y ��� u ��� e ��� (u = e)` by metis_tac[] >>
86  qsuff_tac `vSUC e = y` >- rw[] >>
87  rw [vSUC_def, Once EXTENSION] >> metis_tac [SET_def]);
88
89val Nats_inductive = store_thm(
90  "Nats_inductive",
91  ``Nats ��� Inductives``,
92  rw [SPEC0, SUBSET_def, Inductives_def, Nats_SET, EMPTY_IN_Nats,
93      vSUC_IN_Nats_I]);
94
95val Nats_least_inductive = store_thm(
96  "Nats_least_inductive",
97  ``P ��� Inductives ��� Nats ��� P``,
98  rw[Inductives_def, SUBSET_def] >>
99  fs [Nats_def, inductive_def])
100
101val Nats_SETs = prove(``n ��� Nats ��� SET n``, metis_tac [SET_def])
102val _ = augment_srw_ss [rewrites [Nats_SETs]]
103(*
104Higher order logic wins here: can capture all possible predicates.
105Can simplify to membership of a set S by making the predicate P be just that.
106 ��� ���P. P 0 ��� (���x. P x ��� x ��� Nats ��� P (vSUC x)) ��� ���u. u ��� Nats ��� P u
107*)
108val nat_induction = save_thm(
109  "nat_induction",
110  Nats_least_inductive
111      |> SIMP_RULE(srw_ss())[SUBSET_def,Inductives_def,SPEC0]
112      |> Q.GEN `P`
113      |> Q.SPEC `SPEC0 P ��� Nats`
114      |> SIMP_RULE (srw_ss() ++ CONJ_ss)
115                   [Nats_SET, EMPTY_IN_Nats, vSUC_IN_Nats_I,
116                    GSYM fromNat_def]
117      |> Q.GEN `P`);
118val _ = IndDefLib.export_rule_induction "nat_induction"
119
120val transitive_def = Define`
121  transitive X ��� ���x. x ��� X ��� x ��� X
122`;
123
124val transitive_ALT = store_thm(
125  "transitive_ALT",
126  ``transitive X ��� ���x y. x ��� y ��� y ��� X ��� x ��� X``,
127  rw [transitive_def] >> metis_tac [SUBSET_def]);
128
129val Nats_transitive = store_thm(
130  "Nats_transitive",
131  ``���n. n ��� Nats ��� transitive n``,
132  ho_match_mp_tac nat_induction >> conj_tac >> rw[transitive_def] >>
133  fs [vSUC_def, SUBSET_def] >> metis_tac []);
134
135(* pointless given axiom of foundation - in its absence, this proof works
136val Nats_not_selfmembers = store_thm(
137  "Nats_not_selfmembers",
138  ``���n. n ��� Nats ��� n ��� n``,
139  ho_match_mp_tac nat_induction >> rw[vSUC_def] >| [
140    strip_tac >> `n ��� n ��� {n}` by rw[] >>
141    metis_tac [Nats_transitive, transitive_ALT],
142    rw[Once EXTENSION] >> metis_tac []
143  ]);
144*)
145
146val pre_IN_vSUC = store_thm(
147  "pre_IN_vSUC",
148  ``SET n ��� n ��� vSUC n``,
149  rw[vSUC_def]);
150
151val SET_vSUC = store_thm(
152  "SET_vSUC",
153  ``SET (vSUC n) = SET n``,
154  rw[vSUC_def, EQ_IMP_THM]);
155val _ = export_rewrites ["SET_vSUC"]
156
157(* doing this the longwinded way, with appeals to foundation all over the
158   place gives a stronger rewrite rule without requiring n and m to be ��� Nats *)
159val vSUC_11 = store_thm(
160  "vSUC_11",
161  ``���n m. ((vSUC n = vSUC m) ��� (n = m))``,
162  rw[EQ_IMP_THM] >> Cases_on `SET n` >| [
163    fs[vSUC_def] >> rw[EXTENSION] >>
164    `SET m` by metis_tac [UNION_SET_CLOSED, SET_INSERT, EMPTY_SET] >>
165    first_assum (qspec_then `x` mp_tac o
166                 SIMP_RULE (srw_ss()) [Once EXTENSION]) >>
167    simp[] >>
168    Cases_on `x ��� n` >> simp[] >| [
169      rw[DISJ_IMP_THM] >> strip_tac >> rw[] >>
170      first_assum (qspec_then `n` mp_tac o
171                   SIMP_RULE (srw_ss()) [Once EXTENSION]) >>
172      rw[] >> metis_tac [IN_ANTISYM, IN_REFL],
173      Cases_on `x = n` >> simp[DISJ_IMP_THM] >> strip_tac >> rw[] >>
174      first_assum (qspec_then `m` mp_tac o
175                   SIMP_RULE (srw_ss()) [Once EXTENSION]) >>
176      rw[] >> metis_tac [IN_ANTISYM, IN_REFL]
177    ],
178
179    fs[vSUC_def] >>
180    `��SET m` by metis_tac [UNION_SET_CLOSED, SET_INSERT, EMPTY_SET] >>
181    `({n} = {}) ��� ({m} = {})`
182       by metis_tac [INSERT_def, PCLASS_SINGC_EMPTY, EMPTY_UNION] >>
183    fs[]
184  ]);
185val _ = export_rewrites ["vSUC_11"]
186
187val Nats_CASES = store_thm(
188  "Nats_CASES",
189  ``���n. n ��� Nats ��� (n = 0) ��� ���m. m ��� Nats ��� (n = vSUC m)``,
190  simp_tac (srw_ss() ++ DNF_ss)[EQ_IMP_THM, vSUC_IN_Nats_I] >>
191  Induct_on `n ��� Nats` >> metis_tac []);
192
193val vSUC_IN_NATS = store_thm(
194  "vSUC_IN_NATS",
195  ``���n. vSUC n ��� Nats ��� n ��� Nats``,
196  simp[EQ_IMP_THM, vSUC_IN_Nats_I] >>
197  qsuff_tac `���m. m ��� Nats ��� ���n. (m = vSUC n) ��� n ��� Nats` >- metis_tac [] >>
198  Induct_on `m ��� Nats` >> simp[]);
199val _ = export_rewrites ["vSUC_IN_NATS"]
200
201(* less than or equal *)
202val nle_def = Define`
203  nle = SPEC0 (��p. ���P. (���x. x ��� Nats ��� ���0��x��� ��� P) ���
204                       (���x y. x ��� Nats ��� y ��� Nats ��� ���x��y��� ��� P ���
205                              ���vSUC x��vSUC y��� ��� P) ���
206                       p ��� P)
207`;
208
209val _ = overload_on ("<=", ``��x y. ���x��y��� ��� nle``)
210val _ = overload_on ("<", ``��x:vbgc y. �� (y ��� x)``)
211
212val ZERO_LE = store_thm(
213  "ZERO_LE",
214  ``���n. n ��� Nats ��� 0 ��� n``,
215  rw [nle_def]);
216val _ = export_rewrites ["ZERO_LE"]
217
218val nle_Nats = store_thm(
219  "nle_Nats",
220  ``n ��� m ��� n ��� Nats ��� m ��� Nats``,
221  rw[nle_def] >> pop_assum (qspec_then `Nats �� Nats` mp_tac) >>
222  asm_simp_tac (srw_ss() ++ CONJ_ss)[CROSS_def]);
223
224val nle_induct = store_thm(
225  "nle_induct",
226  ``(���n. n ��� Nats ��� P 0 n) ���
227    (���n m. n ��� Nats ��� m ��� Nats ��� P n m ��� P (vSUC n) (vSUC m)) ���
228    ���n m. n ��� m ��� P n m``,
229  rw[nle_def] >>
230  qsuff_tac `���n��m��� ��� SPEC0 (��p. ���x y. (p = ���x��y���) ��� P x y)` >-
231    simp_tac (srw_ss()) [] >>
232  pop_assum match_mp_tac >> simp[]);
233val _ = IndDefLib.export_rule_induction "nle_induct"
234
235val vSUC_LE_I = store_thm(
236  "vSUC_LE_I",
237  ``n ��� m ��� vSUC n ��� vSUC m``,
238  strip_tac >> imp_res_tac nle_Nats >>
239  fs[nle_def]);
240
241val LE_CASES = store_thm(
242  "LE_CASES",
243  ``n ��� m ��� (n = 0) ��� m ��� Nats ���
244            ���n0 m0. n0 ��� Nats ��� m0 ��� Nats ��� (n = vSUC n0) ���
245                    (m = vSUC m0) ��� n0 ��� m0``,
246  Tactical.REVERSE EQ_TAC >- (rw[] >> rw[vSUC_LE_I]) >>
247  map_every qid_spec_tac [`m`, `n`] >> ho_match_mp_tac nle_induct >>
248  srw_tac [CONJ_ss][vSUC_LE_I] >> rw[vSUC_LE_I]);
249
250val vSUC_LE1 = store_thm(
251  "vSUC_LE1",
252  ``vSUC n ��� vSUC m ��� n ��� m``,
253  eq_tac >-
254     (asm_simp_tac (srw_ss() ++ CONJ_ss)
255                   [SimpL ``(==>)``, Once LE_CASES] >> rw[]) >>
256  rw[vSUC_LE_I]);
257val _ = export_rewrites ["vSUC_LE1"]
258
259val vSUC_ZERO_LE = store_thm(
260  "vSUC_ZERO_LE",
261  ``�� (vSUC n ��� 0)``,
262  rw[Once LE_CASES]);
263val _ = export_rewrites ["vSUC_ZERO_LE"]
264
265val LE_REFL0 = prove(
266  ``���n. n ��� Nats ��� n ��� n``,
267  ho_match_mp_tac nat_induction >> rw[vSUC_LE_I])
268
269val LE_REFL = store_thm(
270  "LE_REFL",
271  ``n ��� n ��� n ��� Nats``,
272  metis_tac [nle_Nats, LE_REFL0]);
273val _ = export_rewrites ["LE_REFL"]
274
275val LE_ANTISYM0 = prove(
276  ``���n m. n ��� m ��� m ��� n ��� (m = n)``,
277  ho_match_mp_tac nle_induct >> simp[vSUC_LE1] >>
278  rw[Once LE_CASES]);
279
280val LE_ANTISYM = store_thm(
281  "LE_ANTISYM",
282  ``���n m. n ��� m ��� m ��� n ��� (m = n)``,
283  metis_tac [LE_ANTISYM0]);
284
285val LE_TRANS = store_thm(
286  "LE_TRANS",
287  ``���x y z. x ��� y ��� y ��� z ��� x ��� z``,
288  qsuff_tac `���x y. x ��� y ��� ���z. y ��� z ��� x ��� z` >- metis_tac [] >>
289  ho_match_mp_tac nle_induct >> rw[] >|[
290    `z ��� Nats` by metis_tac [nle_Nats] >> rw[],
291    pop_assum mp_tac >>
292    asm_simp_tac (srw_ss() ++ CONJ_ss) [SimpL ``(==>)``, Once LE_CASES] >>
293    asm_simp_tac (srw_ss() ++ DNF_ss)[]
294  ]);
295
296val LE_TOTAL = store_thm(
297  "LE_TOTAL",
298  ``���n m. n ��� Nats ��� m ��� Nats ��� n ��� m ��� m ��� n``,
299  qsuff_tac `���n. n ��� Nats ��� ���m. m ��� Nats ��� n ��� m ��� m ��� n` >- metis_tac[] >>
300  ho_match_mp_tac nat_induction >> rw[] >>
301  qspec_then `m` mp_tac Nats_CASES >> rw[] >> rw[]);
302
303
304val LESS_ZERO = store_thm(
305  "LESS_ZERO",
306  ``m ��� 0 ��� (m = 0)``,
307  rw[Once LE_CASES]);
308val _ = export_rewrites ["LESS_ZERO"]
309
310val LE_LT_EQ0 = prove(
311  ``���m n. m ��� n ��� m < n ��� (m = n)``,
312  Induct_on `m ��� n` >> rw[] >> metis_tac []);
313
314(* DON'T USE THIS AS A REWRITE!
315
316   It loops because the m < n on the right is really just ~(n <= m) *)
317val LE_LT_EQ = store_thm(
318  "LE_LT_EQ",
319  ``���m n. m ��� n ��� m ��� Nats ��� n ��� Nats ��� (m < n ��� (m = n))``,
320  metis_tac [LE_LT_EQ0, LE_REFL, LE_TOTAL, nle_Nats]);
321
322val LE_DISCRETE = store_thm(
323  "LE_DISCRETE",
324  ``���m n. m ��� Nats ��� n ��� Nats ��� m ��� n ��� vSUC n ��� m``,
325  qsuff_tac `���m. m ��� Nats ��� ���n. n ��� Nats ��� m ��� n ��� vSUC n ��� m` >- metis_tac[]>>
326  Induct_on `m ��� Nats` >> rw[] >> qspec_then `n` mp_tac Nats_CASES >>
327  asm_simp_tac (srw_ss() ++ DNF_ss)[DISJ_IMP_THM]);
328
329val complete_induction = store_thm(
330  "complete_induction",
331  ``���P.
332      (���n. (���m. m ��� Nats ��� m < n ��� P m) ��� P n) ��� ���n. n ��� Nats ��� P n``,
333  gen_tac >> strip_tac >>
334  qsuff_tac `���n. n ��� Nats ��� ���m. m ��� n ��� P m`
335    >- metis_tac [LE_REFL] >>
336  Induct_on `n ��� Nats` >> srw_tac [CONJ_ss][] >>
337  Cases_on `m ��� n` >- metis_tac [] >>
338  `m = vSUC n` by metis_tac [LE_DISCRETE, LE_LT_EQ] >> rw[] >>
339  metis_tac [LE_DISCRETE]);
340
341val rwt = SUBSET_def |> Q.SPECL [`B`, `Nats`] |> EQ_IMP_RULE |> #1 |> UNDISCH
342
343(* ��� B ��� Nats ��� (���n. n ��� B) ��� ���n. n ��� B ��� ���m. m ��� B ��� n ��� m *)
344val Nats_least_element = save_thm(
345  "Nats_least_element",
346  complete_induction |> Q.SPEC `��n. n ��� B`
347                     |> CONV_RULE CONTRAPOS_CONV
348                     |> SIMP_RULE bool_ss []
349                     |> CONV_RULE
350                          (RAND_CONV (ONCE_DEPTH_CONV CONTRAPOS_CONV))
351                     |> SIMP_RULE (srw_ss() ++ CONJ_ss) [rwt]
352                     |> SIMP_RULE bool_ss [Once CONJ_COMM]
353                     |> DISCH_ALL
354                     |> REWRITE_RULE [AND_IMP_INTRO]);
355
356
357
358val _ = export_theory()
359