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