(* An alternative approach to creating finite sets as a quotient of lists. *) (* This takes the extensionality principle as the definition of equivalence.*) (* Composed and contributed by Dr. Michael Norrish. *) (* June 24, 2005. *) open HolKernel Parse boolLib bossLib BasicProvers listTheory quotientLib val _ = new_theory "ext_finite_set"; fun Store_Thm(n,t,tac) = store_thm(n,t,tac) before BasicProvers.export_rewrites [n] val leq_def = Define`leq x y = !e:'a. MEM e x = MEM e y` val leq_refl = Store_Thm( "leq_refl", ``!x :'a list. leq x x``, SRW_TAC [] [leq_def]); val leq_sym = Store_Thm( "leq_sym", ``!x y :'a list. leq x y ==> leq y x``, SRW_TAC [] [leq_def]); val leq_trans = Store_Thm( "leq_trans", ``!x y z :'a list. leq x y /\ leq y z ==> leq x z``, SRW_TAC [] [leq_def]); (* functions on representatives *) (* insertion is represented by :: *) val NOT_NIL_EQUIV_CONS = store_thm( "NOT_NIL_EQUIV_CONS", ``~(leq [] ((a:'a)::A))``, SRW_TAC [boolSimps.DNF_ss] [leq_def]); val NIL_RSP = store_thm( "NIL_RSP", ``leq ([]:'a list) []``, SRW_TAC [] [leq_def]); val CONS_RSP = store_thm( "CONS_RSP", ``!x:'a A B. leq A B ==> leq (x::A) (x::B)``, SRW_TAC [] [leq_def]); (* membership is represented by MEM *) val MEM_RSP = store_thm( "MEM_RSP", ``!X Y x:'a. leq X Y ==> (MEM x X = MEM x Y)``, SRW_TAC [] [leq_def]); val NO_MEM_NIL = Store_Thm( "NO_MEM_NIL", ``!A. (!a:'a. ~(MEM a A)) = (A = [])``, Induct_on `A` THEN SRW_TAC [] [] THEN PROVE_TAC []); val NONE_MEM_NIL = store_thm( "NONE_MEM_NIL", ``!A. (!a:'a. ~(MEM a A)) = (leq A [])``, SRW_TAC [] [leq_def]); val MEM_CONS = store_thm( "MEM_CONS", ``!A (a:'a). MEM a A ==> leq (a :: A) A``, SRW_TAC [] [leq_def] THEN PROVE_TAC []); val CONS_LEFT_COMM = prove( ``!A x y:'a. leq (x::y::A) (y::x::A)``, SRW_TAC [] [leq_def] THEN PROVE_TAC []); val CONS_LEFT_IDEM = prove( ``!A x:'a. leq (x::x::A) (x::A)``, SRW_TAC [] [leq_def] THEN PROVE_TAC []); val finite_set1_strong_cases = store_thm( "finite_set1_strong_cases", ``!X. (X = []) \/ ?(a:'a) Y. ~MEM a Y /\ leq X (a::Y)``, Induct THEN FULL_SIMP_TAC (srw_ss()) [leq_def] THEN METIS_TAC [MEM]); (* Delete1 *) val Delete1_def = Define `($Delete1 [] x = []) /\ ($Delete1 ((a:'a) :: A) x = if a = x then $Delete1 A x else a :: ($Delete1 A x))`; val _ = export_rewrites ["Delete1_def"] val _ = add_infix ("Delete1", 500, HOLgrammars.LEFT); val MEM_Delete1 = store_thm ( "MEM_Delete1", ``!A (a:'a) x. MEM x (A Delete1 a) = MEM x A /\ ~(x = a)``, Induct THEN SRW_TAC[][] THEN PROVE_TAC []); val MEM_Delete1_IDENT = Store_Thm( "MEM_Delete1_IDENT", ``!A (a:'a). ~(MEM a (A Delete1 a))``, Induct_on `A` THEN SRW_TAC [][]); val NOT_MEM_Delete1_IDENT = store_thm( "NOT_MEM_Delete1_IDENT", ``!A (b:'a). ~MEM b A ==> (A Delete1 b = A)``, Induct_on `A` THEN SRW_TAC [][]); val Delete1_RSP = store_thm( "Delete1_RSP", ``!A B (a:'a). leq A B ==> (leq (A Delete1 a) (B Delete1 a))``, SRW_TAC [] [leq_def,MEM_Delete1]); val CONS_Delete1 = store_thm( "CONS_Delete1", ``!A (a:'a). leq (a :: (A Delete1 a)) (if MEM a A then A else a::A)``, SRW_TAC [] [leq_def, MEM_Delete1] THEN PROVE_TAC []); val MEM_CONS_Delete1 = store_thm ("MEM_CONS_Delete1", ``!A (a:'a). MEM a A ==> leq (a :: (A Delete1 a)) A``, PROVE_TAC [CONS_Delete1] ); val finite_set1_Delete1_cases1 = store_thm ("finite_set1_Delete1_cases1", ``!X. (X = []) \/ ?a:'a. leq X (a :: (X Delete1 a))``, Cases THEN SRW_TAC [][leq_def, MEM_Delete1] THEN METIS_TAC []); val finite_set1_Delete1_cases = store_thm ("finite_set1_Delete1_cases", ``!X. (X = []) \/ ?a:'a. MEM a X /\ leq X (a :: (X Delete1 a))``, PROVE_TAC[finite_set1_Delete1_cases1,MEM,MEM_RSP] ); (* Card1 *) val Card1_def = Define `(Card1 ([]) = 0) /\ (Card1 ((a:'a) :: A) = if MEM a A then Card1 A else SUC (Card1 A))`; val _ = export_rewrites ["Card1_def"] val NOT_MEM_Card1 = store_thm ("NOT_MEM_Card1", ``!A:'a list a. ~(MEM a A) ==> (Card1 (a :: A) = SUC (Card1 A))``, RW_TAC std_ss [Card1_def] ); val Card1_SUC = store_thm ( "Card1_SUC", ``!A n. (Card1 A = SUC n) ==> ?(a:'a) B. ~(MEM a B) /\ leq A (a :: B)``, Induct THEN SRW_TAC [][] THENL [ PROVE_TAC [MEM_CONS, leq_trans, leq_sym], PROVE_TAC [leq_refl] ]); val MEM_Card1_NOT_0 = store_thm( "MEM_Card1_NOT_0", ``!A a. MEM (a:'a) A ==> ~(Card1 A = 0)``, Induct_on `A` THEN SRW_TAC [][] THEN PROVE_TAC []); val Card1_CONS_GT_0 = store_thm ( "Card1_CONS_GT_0", ``!A (a:'a). 0 < Card1 (a :: A)``, METIS_TAC [MEM, arithmeticTheory.NOT_ZERO_LT_ZERO, MEM_Card1_NOT_0]); val Card1_Delete1 = store_thm( "Card1_Delete1", ``!A (a:'a). Card1 (A Delete1 a) = if MEM a A then Card1 A - 1 else Card1 A``, Induct_on `A` THEN SRW_TAC [][MEM_Delete1] THEN SRW_TAC [][] THEN PROVE_TAC [MEM_Card1_NOT_0, DECIDE ``~(x = 0) ==> (SUC (x - 1) = x)``]); val Card1_RSP = store_thm ( "Card1_RSP", ``!A B:'a list. leq A B ==> (Card1 A = Card1 B)``, SIMP_TAC (srw_ss()) [leq_def] THEN Induct THEN SRW_TAC [][] THENL [ PROVE_TAC [], `MEM h B /\ ~(Card1 B = 0)` by PROVE_TAC [MEM_Card1_NOT_0] THEN Q_TAC SUFF_TAC `Card1 A = Card1 (B Delete1 h)` THEN1 SRW_TAC [numSimps.ARITH_ss][Card1_Delete1] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][MEM_Delete1] THEN PROVE_TAC [] ]); val Card1_0 = store_thm( "Card1_0", ``!A:'a list. (Card1 A = 0) = (A = [])``, Induct_on `A` THEN SRW_TAC [][] THEN PROVE_TAC [NO_MEM_NIL]); (* list2set *) val list2set_thm = prove( ``(LIST_TO_SET ([]:'a list) = {}) /\ (!h:'a t. LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t)``, SRW_TAC [][pred_setTheory.EXTENSION]); val list2set_RSP = store_thm( "list2set_RSP", ``!A B:'a list. leq A B ==> (LIST_TO_SET A = LIST_TO_SET B)``, SRW_TAC [][leq_def, pred_setTheory.EXTENSION]); (* fold *) val Fold1_def = Define` (Fold1 f (z:'b) [] = z) /\ (Fold1 f z ((a:'a)::A) = if (!u v w. f u (f v w) = f v (f u w)) then if MEM a A then Fold1 f z A else f a (Fold1 f z A) else z) ` ; val MEM_lcommuting_Fold1 = store_thm( "MEM_lcommuting_Fold1", ``!B f (z:'b) (h:'a). (!u v w. f u (f v w) = f v (f u w)) /\ MEM h B ==> (Fold1 f z B = f h (Fold1 f z (B Delete1 h)))``, Induct_on `B` THEN SRW_TAC [][Fold1_def, MEM_Delete1] THENL [ PROVE_TAC [], PROVE_TAC [NOT_MEM_Delete1_IDENT], PROVE_TAC [] ]); val Fold1_RSP = store_thm( "Fold1_RSP", ``!A B:'a list f (z:'b). leq A B ==> (Fold1 f z A = Fold1 f z B)``, REWRITE_TAC [leq_def] THEN Induct THEN SRW_TAC [][Fold1_def] THENL [ PROVE_TAC [], `MEM h B` by PROVE_TAC [] THEN `Fold1 f z B = f h (Fold1 f z (B Delete1 h))` by PROVE_TAC [MEM_lcommuting_Fold1] THEN SRW_TAC [][] THEN AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][MEM_Delete1] THEN PROVE_TAC [], Cases_on `B` THEN SRW_TAC [][Fold1_def] ]); val APPEND_RSP = store_thm( "APPEND_RSP", ``!A1 A2 B1 B2:'a list. leq A1 A2 /\ leq B1 B2 ==> leq (APPEND A1 B1) (APPEND A2 B2)``, SRW_TAC [][leq_def]); val Inter1_def = Define `($Inter1 ([]) B = []) /\ ($Inter1 ((a:'a) :: A) B = if MEM a B then a :: ($Inter1 A B) else $Inter1 A B)`; val _ = add_infix ("Inter1", 600, HOLgrammars.LEFT); val MEM_Inter1 = store_thm ("MEM_Inter1", ``!A B (x:'a). MEM x (A Inter1 B) = MEM x A /\ MEM x B``, Induct THEN SRW_TAC [][Inter1_def] THEN PROVE_TAC [] ); val Inter1_RSP = store_thm ("Inter1_RSP", ``!A1 A2 B1 B2:'a list. leq A1 A2 /\ leq B1 B2 ==> leq (A1 Inter1 B1) (A2 Inter1 B2)``, SRW_TAC [][leq_def, MEM_Inter1]); (* do the quotient *) val leq_equiv = save_thm("leq_equiv", refl_sym_trans_equiv leq_refl leq_sym leq_trans); val equivs = [leq_equiv]; val fnlist = [{def_name="Empty_def", fname="Empty", func= ``[] :'a list``, fixity=Prefix}, {def_name="Insert_def", fname="Insert", func= ``CONS :'a -> 'a list -> 'a list``, fixity=Infixr 490}, {def_name="In_def", fname="In", func= ``MEM :'a -> 'a list -> bool``, fixity=Infix(NONASSOC,425)}, {def_name="Card_def", fname="Card", func= ``Card1 :'a list -> num``, fixity=Prefix}, {def_name="Delete_def", fname="Delete", func= ``$Delete1 :'a list -> 'a -> 'a list``, fixity=Infixl 500}, {def_name="Union_def", fname="Union", func= ``APPEND :'a list -> 'a list -> 'a list``, fixity=Infixl 500}, {def_name="Inter_def", fname="Inter", func= ``$Inter1 :'a list -> 'a list -> 'a list``, fixity=Infixl 600}, {def_name="Fold_def", fname="Fold", func= ``Fold1 :('a -> 'b -> 'b) -> 'b -> 'a list -> 'b``, fixity=Prefix}, {def_name="fset2set_def", fname="fset2set", func= ``LIST_TO_SET :'a list -> 'a -> bool``, fixity=Prefix} ]; (* ==================================================== *) (* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *) (* ==================================================== *) val _ = quotient.chatting := true; (* Causes display of quotient as built *) val [finite_set_cases, Insert_LEFT_COMM, Insert_LEFT_IDEM, In, NONE_In_Empty, In_Insert, finite_set_strong_cases, Card, NOT_In_Card, Card_SUC, Card_Insert_GT_0, In_Card_NOT_0, NOT_Empty_Insert, Delete_def, In_Delete, Card_Delete, Insert_Delete, In_Insert_Delete, finite_set_Delete_cases, Union, In_Union, Inter, In_Inter, Fold, fset2set, finite_set_EXTENSION, finite_set_INDUCT ] = define_quotient_types {types = [{name = "finite_set", equiv = leq_equiv}], defs = fnlist, tyop_equivs = [], tyop_quotients = [FUN_QUOTIENT], tyop_simps = [FUN_REL_EQ, FUN_MAP_I], respects = [NIL_RSP, CONS_RSP, MEM_RSP, Card1_RSP, Delete1_RSP, APPEND_RSP, Inter1_RSP, Fold1_RSP, list2set_RSP], poly_preserves = [FORALL_PRS, EXISTS_PRS, COND_PRS], poly_respects = [RES_FORALL_RSP, RES_EXISTS_RSP, COND_RSP], old_thms = [list_CASES, CONS_LEFT_COMM, CONS_LEFT_IDEM, MEM, NONE_MEM_NIL, MEM_CONS, finite_set1_strong_cases, Card1_def, NOT_MEM_Card1, Card1_SUC, Card1_CONS_GT_0, MEM_Card1_NOT_0, NOT_NIL_EQUIV_CONS, Delete1_def, MEM_Delete1, Card1_Delete1, CONS_Delete1, MEM_CONS_Delete1, finite_set1_Delete1_cases, APPEND, MEM_APPEND, Inter1_def, MEM_Inter1, Fold1_def, list2set_thm, leq_def, list_INDUCT] }; val _ = map save_thm [("finite_set_cases",finite_set_cases), ("Insert_LEFT_COMM",Insert_LEFT_COMM), ("Insert_LEFT_IDEM",Insert_LEFT_IDEM), ("In",In), ("NONE_In_Empty",NONE_In_Empty), ("In_Insert",In_Insert), ("finite_set_strong_cases",finite_set_strong_cases), ("Card",Card), ("NOT_In_Card",NOT_In_Card), ("Card_SUC",Card_SUC), ("Card_Insert_GT_0",Card_Insert_GT_0), ("In_Card_NOT_0",In_Card_NOT_0), ("NOT_Empty_Insert",NOT_Empty_Insert), ("Delete_def",Delete_def), ("In_Delete",In_Delete), ("Card_Delete",Card_Delete), ("Insert_Delete",Insert_Delete), ("In_Insert_Delete",In_Insert_Delete), ("finite_set_Delete_cases",finite_set_Delete_cases), ("Union",Union), ("In_Union",In_Union), ("Inter",Inter), ("In_Inter",In_Inter), ("Fold",Fold), ("fset2set",fset2set), ("finite_set_EXTENSION",finite_set_EXTENSION), ("finite_set_INDUCT",finite_set_INDUCT) ]; val _ = export_theory(); val _ = html_theory "ext_finite_set";