1(* An alternative approach to creating finite sets as a quotient of lists. *) 2(* This takes the extensionality principle as the definition of equivalence.*) 3(* Composed and contributed by Michael Norrish. *) 4(* June 24, 2005. *) 5 6open HolKernel Parse boolLib bossLib BasicProvers listTheory quotientLib 7 8val _ = new_theory "ext_finite_set"; 9 10fun Store_Thm(n,t,tac) = store_thm(n,t,tac) before 11 export_rewrites [n] 12 13val leq_def = Define`leq x y = !e:'a. MEM e x = MEM e y` 14 15val leq_refl = Store_Thm( 16 "leq_refl", 17 ``!x :'a list. leq x x``, 18 SRW_TAC [] [leq_def]); 19 20val leq_sym = Store_Thm( 21 "leq_sym", 22 ``!x y :'a list. leq x y ==> leq y x``, 23 SRW_TAC [] [leq_def]); 24 25val leq_trans = Store_Thm( 26 "leq_trans", 27 ``!x y z :'a list. leq x y /\ leq y z ==> leq x z``, 28 SRW_TAC [] [leq_def]); 29 30(* functions on representatives *) 31 32(* insertion is represented by :: *) 33val NOT_NIL_EQUIV_CONS = store_thm( 34 "NOT_NIL_EQUIV_CONS", 35 ``~(leq [] ((a:'a)::A))``, 36 SRW_TAC [boolSimps.DNF_ss] [leq_def]); 37 38val NIL_RSP = store_thm( 39 "NIL_RSP", 40 ``leq ([]:'a list) []``, 41 SRW_TAC [] [leq_def]); 42 43val CONS_RSP = store_thm( 44 "CONS_RSP", 45 ``!x:'a A B. leq A B ==> leq (x::A) (x::B)``, 46 SRW_TAC [] [leq_def]); 47 48(* membership is represented by MEM *) 49val MEM_RSP = store_thm( 50 "MEM_RSP", 51 ``!X Y x:'a. leq X Y ==> (MEM x X = MEM x Y)``, 52 SRW_TAC [] [leq_def]); 53 54val NO_MEM_NIL = Store_Thm( 55 "NO_MEM_NIL", 56 ``!A. (!a:'a. ~(MEM a A)) = (A = [])``, 57 Induct_on `A` THEN SRW_TAC [] [] THEN PROVE_TAC []); 58 59val NONE_MEM_NIL = store_thm( 60 "NONE_MEM_NIL", 61 ``!A. (!a:'a. ~(MEM a A)) = (leq A [])``, 62 SRW_TAC [] [leq_def]); 63 64val MEM_CONS = store_thm( 65 "MEM_CONS", 66 ``!A (a:'a). MEM a A ==> leq (a :: A) A``, 67 SRW_TAC [] [leq_def] THEN PROVE_TAC []); 68 69val CONS_LEFT_COMM = prove( 70 ``!A x y:'a. leq (x::y::A) (y::x::A)``, 71 SRW_TAC [] [leq_def] THEN PROVE_TAC []); 72 73val CONS_LEFT_IDEM = prove( 74 ``!A x:'a. leq (x::x::A) (x::A)``, 75 SRW_TAC [] [leq_def] THEN PROVE_TAC []); 76 77val finite_set1_strong_cases = store_thm( 78 "finite_set1_strong_cases", 79 ``!X. (X = []) \/ ?(a:'a) Y. ~MEM a Y /\ leq X (a::Y)``, 80 Induct THEN FULL_SIMP_TAC (srw_ss()) [leq_def] THEN 81 METIS_TAC [MEM]); 82 83(* Delete1 *) 84val Delete1_def = Define 85 `($Delete1 [] x = []) /\ 86 ($Delete1 ((a:'a) :: A) x = if a = x then $Delete1 A x 87 else a :: ($Delete1 A x))`; 88val _ = export_rewrites ["Delete1_def"] 89 90val _ = add_infix ("Delete1", 500, HOLgrammars.LEFT); 91 92val MEM_Delete1 = store_thm ( 93 "MEM_Delete1", 94 ``!A (a:'a) x. MEM x (A Delete1 a) = MEM x A /\ ~(x = a)``, 95 Induct THEN SRW_TAC[][] THEN PROVE_TAC []); 96 97val MEM_Delete1_IDENT = Store_Thm( 98 "MEM_Delete1_IDENT", 99 ``!A (a:'a). ~(MEM a (A Delete1 a))``, 100 Induct_on `A` THEN SRW_TAC [][]); 101 102val NOT_MEM_Delete1_IDENT = store_thm( 103 "NOT_MEM_Delete1_IDENT", 104 ``!A (b:'a). ~MEM b A ==> (A Delete1 b = A)``, 105 Induct_on `A` THEN SRW_TAC [][]); 106 107val Delete1_RSP = store_thm( 108 "Delete1_RSP", 109 ``!A B (a:'a). leq A B ==> (leq (A Delete1 a) (B Delete1 a))``, 110 SRW_TAC [] [leq_def,MEM_Delete1]); 111 112val CONS_Delete1 = store_thm( 113 "CONS_Delete1", 114 ``!A (a:'a). leq (a :: (A Delete1 a)) (if MEM a A then A else a::A)``, 115 SRW_TAC [] [leq_def, MEM_Delete1] THEN PROVE_TAC []); 116 117val MEM_CONS_Delete1 = store_thm 118 ("MEM_CONS_Delete1", 119 ``!A (a:'a). MEM a A ==> leq (a :: (A Delete1 a)) A``, 120 PROVE_TAC [CONS_Delete1] 121 ); 122 123val finite_set1_Delete1_cases1 = store_thm 124 ("finite_set1_Delete1_cases1", 125 ``!X. (X = []) \/ ?a:'a. leq X (a :: (X Delete1 a))``, 126 Cases THEN SRW_TAC [][leq_def, MEM_Delete1] THEN METIS_TAC []); 127 128val finite_set1_Delete1_cases = store_thm 129 ("finite_set1_Delete1_cases", 130 ``!X. (X = []) \/ 131 ?a:'a. MEM a X /\ leq X (a :: (X Delete1 a))``, 132 PROVE_TAC[finite_set1_Delete1_cases1,MEM,MEM_RSP] 133 ); 134 135(* Card1 *) 136 137val Card1_def = Define 138 `(Card1 ([]) = 0) /\ 139 (Card1 ((a:'a) :: A) = if MEM a A then Card1 A else SUC (Card1 A))`; 140val _ = export_rewrites ["Card1_def"] 141 142val NOT_MEM_Card1 = store_thm 143 ("NOT_MEM_Card1", 144 ``!A:'a list a. ~(MEM a A) ==> 145 (Card1 (a :: A) = SUC (Card1 A))``, 146 RW_TAC std_ss [Card1_def] 147 ); 148 149val Card1_SUC = store_thm ( 150 "Card1_SUC", 151 ``!A n. (Card1 A = SUC n) ==> 152 ?(a:'a) B. ~(MEM a B) /\ leq A (a :: B)``, 153 Induct THEN SRW_TAC [][] THENL [ 154 PROVE_TAC [MEM_CONS, leq_trans, leq_sym], 155 PROVE_TAC [leq_refl] 156 ]); 157 158val MEM_Card1_NOT_0 = store_thm( 159 "MEM_Card1_NOT_0", 160 ``!A a. MEM (a:'a) A ==> ~(Card1 A = 0)``, 161 Induct_on `A` THEN SRW_TAC [][] THEN PROVE_TAC []); 162 163val Card1_CONS_GT_0 = store_thm ( 164 "Card1_CONS_GT_0", 165 ``!A (a:'a). 0 < Card1 (a :: A)``, 166 METIS_TAC [MEM, arithmeticTheory.NOT_ZERO_LT_ZERO, 167 MEM_Card1_NOT_0]); 168 169val Card1_Delete1 = store_thm( 170 "Card1_Delete1", 171 ``!A (a:'a). 172 Card1 (A Delete1 a) = if MEM a A then Card1 A - 1 else Card1 A``, 173 Induct_on `A` THEN SRW_TAC [][MEM_Delete1] THEN SRW_TAC [][] THEN 174 PROVE_TAC [MEM_Card1_NOT_0, DECIDE ``~(x = 0) ==> (SUC (x - 1) = x)``]); 175 176val Card1_RSP = store_thm ( 177 "Card1_RSP", 178 ``!A B:'a list. leq A B ==> (Card1 A = Card1 B)``, 179 SIMP_TAC (srw_ss()) [leq_def] THEN Induct THEN SRW_TAC [][] THENL [ 180 PROVE_TAC [], 181 `MEM h B /\ ~(Card1 B = 0)` by PROVE_TAC [MEM_Card1_NOT_0] THEN 182 Q_TAC SUFF_TAC `Card1 A = Card1 (B Delete1 h)` 183 THEN1 SRW_TAC [numSimps.ARITH_ss][Card1_Delete1] THEN 184 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][MEM_Delete1] THEN 185 PROVE_TAC [] 186 ]); 187 188val Card1_0 = store_thm( 189 "Card1_0", 190 ``!A:'a list. (Card1 A = 0) = (A = [])``, 191 Induct_on `A` THEN SRW_TAC [][] THEN PROVE_TAC [NO_MEM_NIL]); 192 193(* list2set *) 194val list2set_thm = prove( 195 ``(LIST_TO_SET ([]:'a list) = {}) /\ 196 (!h:'a t. LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t)``, 197 SRW_TAC [][pred_setTheory.EXTENSION]); 198 199val list2set_RSP = store_thm( 200 "list2set_RSP", 201 ``!A B:'a list. leq A B ==> (LIST_TO_SET A = LIST_TO_SET B)``, 202 SRW_TAC [][leq_def, pred_setTheory.EXTENSION]); 203 204(* fold *) 205 206val Fold1_def = Define` 207 (Fold1 f (z:'b) [] = z) /\ 208 (Fold1 f z ((a:'a)::A) = 209 if (!u v w. f u (f v w) = f v (f u w)) then 210 if MEM a A then Fold1 f z A 211 else f a (Fold1 f z A) 212 else z) 213` ; 214 215val MEM_lcommuting_Fold1 = store_thm( 216 "MEM_lcommuting_Fold1", 217 ``!B f (z:'b) (h:'a). 218 (!u v w. f u (f v w) = f v (f u w)) /\ MEM h B ==> 219 (Fold1 f z B = f h (Fold1 f z (B Delete1 h)))``, 220 Induct_on `B` THEN SRW_TAC [][Fold1_def, MEM_Delete1] THENL [ 221 PROVE_TAC [], 222 PROVE_TAC [NOT_MEM_Delete1_IDENT], 223 PROVE_TAC [] 224 ]); 225 226val Fold1_RSP = store_thm( 227 "Fold1_RSP", 228 ``!A B:'a list f (z:'b). leq A B ==> (Fold1 f z A = Fold1 f z B)``, 229 REWRITE_TAC [leq_def] THEN Induct THEN SRW_TAC [][Fold1_def] THENL [ 230 PROVE_TAC [], 231 `MEM h B` by PROVE_TAC [] THEN 232 `Fold1 f z B = f h (Fold1 f z (B Delete1 h))` 233 by PROVE_TAC [MEM_lcommuting_Fold1] THEN 234 SRW_TAC [][] THEN AP_TERM_TAC THEN 235 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][MEM_Delete1] THEN 236 PROVE_TAC [], 237 Cases_on `B` THEN SRW_TAC [][Fold1_def] 238 ]); 239 240val APPEND_RSP = store_thm( 241 "APPEND_RSP", 242 ``!A1 A2 B1 B2:'a list. leq A1 A2 /\ leq B1 B2 ==> 243 leq (APPEND A1 B1) (APPEND A2 B2)``, 244 SRW_TAC [][leq_def]); 245 246val Inter1_def = Define 247 `($Inter1 ([]) B = []) /\ 248 ($Inter1 ((a:'a) :: A) B = if MEM a B then a :: ($Inter1 A B) 249 else $Inter1 A B)`; 250 251val _ = add_infix ("Inter1", 600, HOLgrammars.LEFT); 252 253val MEM_Inter1 = store_thm 254 ("MEM_Inter1", 255 ``!A B (x:'a). 256 MEM x (A Inter1 B) = MEM x A /\ MEM x B``, 257 Induct 258 THEN SRW_TAC [][Inter1_def] 259 THEN PROVE_TAC [] 260 ); 261 262val Inter1_RSP = store_thm 263 ("Inter1_RSP", 264 ``!A1 A2 B1 B2:'a list. 265 leq A1 A2 /\ leq B1 B2 ==> 266 leq (A1 Inter1 B1) (A2 Inter1 B2)``, 267 SRW_TAC [][leq_def, MEM_Inter1]); 268 269(* do the quotient *) 270val leq_equiv = save_thm("leq_equiv", 271 refl_sym_trans_equiv leq_refl leq_sym leq_trans); 272 273val equivs = [leq_equiv]; 274 275 276val fnlist = 277 [{def_name="Empty_def", 278 fname="Empty", 279 func= ``[] :'a list``, 280 fixity=NONE}, 281 282 {def_name="Insert_def", 283 fname="Insert", 284 func= ``CONS :'a -> 'a list -> 'a list``, 285 fixity=SOME(Infixr 490)}, 286 287(* if desired, a membership constant for finite sets can be defined in 288 terms of fset2set: 289 290 fmem x s = x ��� fset2set s (UOK) 291 292 Alternatively, fmem could just be overloaded to a term of this form, as 293 is done in the finite_set version of this example. 294 295 The following doesn't work because MEM is not a constant (since f42df6bf5) 296 297 {def_name="In_def", 298 fname="In", 299 func= ``MEM :'a -> 'a list -> bool``, 300 fixity=SOME(Infix(NONASSOC,425))}, 301*) 302 303 {def_name="Card_def", 304 fname="Card", 305 func= ``Card1 :'a list -> num``, 306 fixity=NONE}, 307 308 {def_name="Delete_def", 309 fname="Delete", 310 func= ``$Delete1 :'a list -> 'a -> 'a list``, 311 fixity=SOME(Infixl 500)}, 312 313 {def_name="Union_def", 314 fname="Union", 315 func= ``APPEND :'a list -> 'a list -> 'a list``, 316 fixity=SOME(Infixl 500)}, 317 318 {def_name="Inter_def", 319 fname="Inter", 320 func= ``$Inter1 :'a list -> 'a list -> 'a list``, 321 fixity=SOME(Infixl 600)}, 322 323 {def_name="Fold_def", 324 fname="Fold", 325 func= ``Fold1 :('a -> 'b -> 'b) -> 'b -> 'a list -> 'b``, 326 fixity=NONE}, 327 328 {def_name="fset2set_def", 329 fname="fset2set", 330 func= ``LIST_TO_SET :'a list -> 'a -> bool``, 331 fixity=NONE} 332 ]; 333 334 335(* ==================================================== *) 336(* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *) 337(* ==================================================== *) 338 339val _ = quotient.chatting := true; (* Causes display of quotient as built *) 340 341 342val [finite_set_cases, Insert_LEFT_COMM, Insert_LEFT_IDEM, 343 In, NONE_In_Empty, In_Insert, finite_set_strong_cases, 344 Card, NOT_In_Card, Card_SUC, Card_Insert_GT_0, 345 In_Card_NOT_0, NOT_Empty_Insert, 346 Delete_def, In_Delete, Card_Delete, 347 Insert_Delete, In_Insert_Delete, finite_set_Delete_cases, 348 Union, In_Union, Inter, In_Inter, 349 Fold, fset2set, finite_set_EXTENSION, finite_set_INDUCT 350 ] = 351 352 define_quotient_types 353 354 {types = [{name = "finite_set", equiv = leq_equiv}], 355 defs = fnlist, 356 tyop_equivs = [], 357 tyop_quotients = [FUN_QUOTIENT], 358 tyop_simps = [FUN_REL_EQ, FUN_MAP_I], 359 respects = [NIL_RSP, CONS_RSP, Card1_RSP, Delete1_RSP, 360 APPEND_RSP, Inter1_RSP, Fold1_RSP, list2set_RSP], 361 poly_preserves = [FORALL_PRS, EXISTS_PRS, COND_PRS], 362 poly_respects = [RES_FORALL_RSP, RES_EXISTS_RSP, COND_RSP], 363 old_thms = [list_CASES, CONS_LEFT_COMM, CONS_LEFT_IDEM, 364 MEM, NONE_MEM_NIL, MEM_CONS, finite_set1_strong_cases, 365 Card1_def, NOT_MEM_Card1, Card1_SUC, Card1_CONS_GT_0, 366 MEM_Card1_NOT_0, NOT_NIL_EQUIV_CONS, 367 Delete1_def, MEM_Delete1, Card1_Delete1, 368 CONS_Delete1, MEM_CONS_Delete1, finite_set1_Delete1_cases, 369 APPEND, MEM_APPEND, Inter1_def, MEM_Inter1, 370 Fold1_def, list2set_thm, leq_def, list_INDUCT] 371 }; 372 373val _ = map save_thm 374 [("finite_set_cases",finite_set_cases), 375 ("Insert_LEFT_COMM",Insert_LEFT_COMM), 376 ("Insert_LEFT_IDEM",Insert_LEFT_IDEM), 377 ("In",In), 378 ("NONE_In_Empty",NONE_In_Empty), 379 ("In_Insert",In_Insert), 380 ("finite_set_strong_cases",finite_set_strong_cases), 381 ("Card",Card), 382 ("NOT_In_Card",NOT_In_Card), 383 ("Card_SUC",Card_SUC), 384 ("Card_Insert_GT_0",Card_Insert_GT_0), 385 ("In_Card_NOT_0",In_Card_NOT_0), 386 ("NOT_Empty_Insert",NOT_Empty_Insert), 387 ("Delete_def",Delete_def), 388 ("In_Delete",In_Delete), 389 ("Card_Delete",Card_Delete), 390 ("Insert_Delete",Insert_Delete), 391 ("In_Insert_Delete",In_Insert_Delete), 392 ("finite_set_Delete_cases",finite_set_Delete_cases), 393 ("Union",Union), 394 ("In_Union",In_Union), 395 ("Inter",Inter), 396 ("In_Inter",In_Inter), 397 ("Fold",Fold), 398 ("fset2set",fset2set), 399 ("finite_set_EXTENSION",finite_set_EXTENSION), 400 ("finite_set_INDUCT",finite_set_INDUCT) 401 ]; 402 403val _ = export_theory(); 404 405val _ = html_theory "ext_finite_set"; 406