Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <29766-0@swan.cl.cam.ac.uk>; Sun, 19 Jul 1992 06:29:46 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA18810; Sat, 18 Jul 92 22:18:31 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA18805; Sat, 18 Jul 92 22:18:24 -0700 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61c+YP/3.19) id AA25927; Sat, 18 Jul 92 22:19:27 -0700 Message-Id: <9207190519.AA25927@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs Subject: Generalizing an assoc. and comm. operation with id. to sets Date: Sat, 18 Jul 92 22:19:26 PDT From: chou@edu.ucla.cs In the following you can find the HOL code for generalizing an associative and commutative operation "op" with identity "id" to finite sets. A constant "ACI_OP : (** -> ** -> **) -> ** -> (* -> **) -> (* -> bool) -> **" is picked (via constant specification) such that: |- ? ACI_OP : (** -> ** -> **) -> ** -> (* -> **) -> (* -> bool) -> ** . ! op id . ASSOC_COMM_ID op id ==> ( ! f . ACI_OP op id f { } = id ) /\ ( ! f s x . FINITE s ==> ( ACI_OP op id f (x INSERT s) = (x IN s) => (ACI_OP op id f s) | (op (f x) (ACI_OP op id f s)) ) ) where ASSOC_COMM_ID has the obvious meaning. Summation and product over sets can now be defined using ACI_OP: |- set_SUM = ACI_OP $+ 0 |- set_PROD = ACI_OP $* 1 Maximum (minimum) can also be so generalized if there is a least (greatest) element in the type. The basic ideas below are stolen from Tom Melham's definition of cardinality (CARD) in the new `pred_sets` library. I would appreciate all comments. - Ching Tsun ============================ CUT HERE ======================================== new_theory `aci` ;; %----------------------------------------------------------------------------- Need the new `pred_sets` library by Tom Melham. -----------------------------------------------------------------------------% load_library `pred_sets` ;; %----------------------------------------------------------------------------- Miscellaneous ML functions. -----------------------------------------------------------------------------% let sing x = [x] ;; %----------------------------------------------------------------------------- (Stolen from Brian Graham.) -----------------------------------------------------------------------------% let SELECT_UNIQUE_RULE (x,y) th1 th2 = let Q = mk_abs (x, subst [x,y] (concl th1)) in let th1' = SUBST [SYM (BETA_CONV "^Q ^y"), "b:bool"] "b:bool" th1 in ( MP (SPECL ["$@ ^Q"; y] th2) (CONJ (CONV_RULE BETA_CONV (SELECT_INTRO th1')) th1) ) ;; let SELECT_UNIQUE_TAC:tactic (gl,g) = let Q,y = dest_eq g in let x,Qx = dest_select Q in let x' = variant (x.freesl(g.gl))x in let Qx' = subst [x', x] Qx in ([gl,subst [y,x]Qx; gl, "!^x ^x'. (^Qx /\ ^Qx') ==> (^x = ^x')"], (\thl. SELECT_UNIQUE_RULE (x,y) (hd thl) (hd (tl thl)))) ;; %----------------------------------------------------------------------------- "ASSOC_COMM_ID_DEF op id" holds iff "op" is an associative and commutative operation with identity "id". -----------------------------------------------------------------------------% let ASSOC_COMM_ID_DEF = new_definition(`ASSOC_COMM_ID_DEF`, " ASSOC_COMM_ID (op : ** -> ** -> **) (id : **) = ( ! a b c . (op a (op b c)) = (op (op a b) c) ) /\ ( ! a b . (op a b) = (op b a) ) /\ ( ! a . (op a id) = a ) ");; %----------------------------------------------------------------------------- The following is based on ideas stolen from Tom Melham's definition of cardinality ("CARD") in the library "pred_sets". -----------------------------------------------------------------------------% let REL = " REL : (** -> ** -> **) -> ** -> (* -> **) -> (* -> bool) -> ** -> num -> bool " ;; %----------------------------------------------------------------------------- "REL op id f s a n" holds iff set s has cardinality n and doing operation op on f(x)'s with x ranging over s has result a, where a = id if s = { }. -----------------------------------------------------------------------------% let ACI_REL_DEF = " ( ! op id f s a . ^REL op id f s a 0 = (s = { }) /\ (a = id) ) /\ ( ! op id f s a n . ^REL op id f s a (SUC n) = ? x b . x IN s /\ ^REL op id f (s DELETE x) b n /\ (a = op (f x) b) ) " ;; %----------------------------------------------------------------------------- Prove that relation "REL", as recursively defined above, exists. -----------------------------------------------------------------------------% let ACI_REL_EXISTS = prove_rec_fn_exists num_Axiom ACI_REL_DEF ;; %----------------------------------------------------------------------------- All lemmas below about "REL" assume "ASSOC_COMM_ID op id". -----------------------------------------------------------------------------% %----------------------------------------------------------------------------- "REL op id f s a 1" holds iff s = {x} and a = f(x) for some x. -----------------------------------------------------------------------------% let ACI_REL_1_LEMMA = PROVE( " ^ACI_REL_DEF ==> ! op id . ASSOC_COMM_ID op id ==> ! f s a . ^REL op id f s a (SUC 0) = ? x . (s = {x}) /\ (a = f x) " , ( DISCH_THEN \ ACI_REL_asm . REPEAT GEN_TAC THEN DISCH_THEN \ ASSOC_COMM_ID_asm . let [_; _; ID_asm] = (CONJUNCTS o PURE_ONCE_REWRITE_RULE [ASSOC_COMM_ID_DEF]) ASSOC_COMM_ID_asm in REPEAT GEN_TAC THEN PURE_REWRITE_TAC [ACI_REL_asm] THEN EQ_TAC THEN REPEAT STRIP_TAC THEN EXISTS_TAC "x : *" THENL [ IMP_RES_TAC DELETE_EQ_SING THEN ASM_REWRITE_TAC [ID_asm] ; EXISTS_TAC "id : **" THEN ASM_REWRITE_TAC [ID_asm; IN_SING; SING_DELETE] ] ) ) ;; %----------------------------------------------------------------------------- If "REL op id f s a (SUC n)" holds, then it does not matter which element of s to delete in the recursive definition of "REL". -----------------------------------------------------------------------------% let ACI_REL_SUC_LEMMA = PROVE( " ^ACI_REL_DEF ==> ! op id . ASSOC_COMM_ID op id ==> ! n f s a . ^REL op id f s a (SUC n) ==> ! x . x IN s ==> ? b . ^REL op id f (s DELETE x) b n /\ (a = op (f x) b) " , ( DISCH_THEN \ ACI_REL_asm . REPEAT GEN_TAC THEN DISCH_THEN \ ASSOC_COMM_ID_asm . let [ASSOC_asm; COMM_asm; ID_asm] = (CONJUNCTS o PURE_ONCE_REWRITE_RULE [ASSOC_COMM_ID_DEF]) ASSOC_COMM_ID_asm and SING_lemma = itlist (C MATCH_MP) [ASSOC_COMM_ID_asm; ACI_REL_asm] ACI_REL_1_LEMMA in INDUCT_TAC THENL [ PURE_REWRITE_TAC [SING_lemma; CONJUNCT1 ACI_REL_asm] THEN REPEAT (FILTER_STRIP_TAC "IN : * -> (* -> bool) -> bool") THEN ASM_REWRITE_TAC [IN_SING] THEN DISCH_TAC THEN EXISTS_TAC "id : **" THEN ASM_REWRITE_TAC [ID_asm; SING_DELETE] ; REPEAT GEN_TAC THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [ ] [ACI_REL_asm] THEN REPEAT STRIP_TAC THEN ASM_CASES_TAC "x' = x : *" THENL [ EXISTS_TAC "b : **" THEN ASM_REWRITE_TAC [ ] ; FIRST_ASSUM (ASSUME_TAC o NOT_EQ_SYM) THEN IMP_RES_TAC IN_DELETE THEN RES_TAC THEN EXISTS_TAC "(op : ** -> ** -> **) (f (x : *)) b'" THEN CONJ_TAC THENL [ PURE_REWRITE_TAC [ACI_REL_asm] THEN EXISTS_TAC "x : *" THEN EXISTS_TAC "b' : **" THEN PURE_ONCE_REWRITE_TAC [DELETE_COMM] THEN ASM_REWRITE_TAC [ ] ; ASM_REWRITE_TAC [ ] THEN CONV_TAC (AC_CONV (ASSOC_asm, COMM_asm)) ] ] ] ) ) ;; %----------------------------------------------------------------------------- Therefore, for any (op, id, f, s), there is at most one pair (a, n) such that "REL op id f s a n" holds. -----------------------------------------------------------------------------% let ACI_REL_UNIQUE_LEMMA = PROVE( " ^ACI_REL_DEF ==> ! op id . ASSOC_COMM_ID op id ==> ! n1 n2 f s a1 a2 . ^REL op id f s a1 n1 ==> ^REL op id f s a2 n2 ==> (a1 = a2) /\ (n1 = n2) " , ( REPEAT (FILTER_STRIP_TAC "n1 : num") THEN INDUCT_TAC THEN INDUCT_TAC THENL [ PURE_ASM_REWRITE_TAC [ ] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [ ] ; PURE_ASM_REWRITE_TAC [ ] THEN REPEAT STRIP_TAC THEN IMP_RES_TAC MEMBER_NOT_EMPTY ; PURE_ASM_REWRITE_TAC [ ] THEN REPEAT STRIP_TAC THEN IMP_RES_TAC MEMBER_NOT_EMPTY ; REPEAT GEN_TAC THEN DISCH_TAC THEN PURE_ASM_REWRITE_TAC [ ] THEN STRIP_TAC THEN IMP_RES_TAC ACI_REL_SUC_LEMMA THEN RES_TAC THEN FILTER_ASM_REWRITE_TAC ( let op = "op : ** -> ** -> **" and f = "f : * -> **" in C mem ["a1 = ^op(^f x)b'"; "a2 = ^op(^f x)b"; "b' = b : **"; "n1 = n2 : num"] ) [ ] ] ) ) ;; %----------------------------------------------------------------------------- Furthermore, if s is finite, then there must exist a pair (a, n) such that "REL op id f s a n" holds. -----------------------------------------------------------------------------% let ACI_REL_EXISTS_LEMMA = PROVE( " ^ACI_REL_DEF ==> ! op id . ASSOC_COMM_ID op id ==> ! f s . FINITE s ==> ? a n . ^REL op id f s a n " , ( REPEAT (FILTER_STRIP_TAC "s : * -> bool") THEN SET_INDUCT_TAC THENL [ EXISTS_TAC "id : **" THEN EXISTS_TAC "0" THEN ASM_REWRITE_TAC [ ] ; FIRST_ASSUM CHOOSE_TAC THEN FIRST_ASSUM CHOOSE_TAC THEN EXISTS_TAC "(op : ** -> ** -> **) (f (e : *)) a" THEN EXISTS_TAC "SUC n" THEN PURE_ASM_REWRITE_TAC [ ] THEN EXISTS_TAC "e : *" THEN EXISTS_TAC "a : **" THEN IMP_RES_TAC DELETE_NON_ELEMENT THEN ASM_REWRITE_TAC [IN_INSERT; DELETE_INSERT] ] ) ) ;; %----------------------------------------------------------------------------- Hence, if s is finite, then "@ b . ? n . REL op id f s b n" does have the desired property of satisfying "\ a . ? n . REL op id f s a n". -----------------------------------------------------------------------------% let ACI_REL_SELECT_LEMMA = PROVE( " ^ACI_REL_DEF ==> ! op id . ASSOC_COMM_ID op id ==> ! f s a . FINITE s ==> ( ( (@ b . ? n . ^REL op id f s b n) = a ) = ( ? n . ^REL op id f s a n) ) " , ( REPEAT STRIP_TAC THEN IMP_RES_TAC ACI_REL_EXISTS_LEMMA THEN EQ_TAC THENL [ DISCH_THEN (\asm. PURE_ONCE_REWRITE_TAC [SYM asm]) THEN CONV_TAC SELECT_CONV THEN ASM_REWRITE_TAC [ ] ; STRIP_TAC THEN SELECT_UNIQUE_TAC THENL [ EXISTS_TAC "n : num" THEN ASM_REWRITE_TAC [ ] ; REPEAT STRIP_TAC THEN IMP_RES_TAC ACI_REL_UNIQUE_LEMMA ] ] ) ) ;; %----------------------------------------------------------------------------- Now, prove that "\ op id f s . @ b . ? n . REL op id f s b n" defines the function that performs op on f(x)'s with x ranging over s, for any op and id such that "ASSOC_COMM_ID op id". -----------------------------------------------------------------------------% let ACI_OP_EXISTS = PROVE( " ? OP : (** -> ** -> **) -> ** -> (* -> **) -> (* -> bool) -> ** . ! op id . ASSOC_COMM_ID op id ==> ( ! f . OP op id f { } = id ) /\ ( ! f s x . FINITE s ==> ( OP op id f (x INSERT s) = (x IN s) => (OP op id f s) | (op (f x) (OP op id f s)) ) ) " , ( STRIP_ASSUME_TAC ACI_REL_EXISTS THEN EXISTS_TAC "\ op id f s . @ b . ? n . ^REL op id f s b n" THEN CONV_TAC (TOP_DEPTH_CONV BETA_CONV) THEN REPEAT STRIP_TAC THENL [ ASSUME_TAC (INST_TYPE [(":*", ":**")] FINITE_EMPTY) THEN IMP_RES_TAC ACI_REL_SELECT_LEMMA THEN PURE_ASM_REWRITE_TAC [ ] THEN EXISTS_TAC "0" THEN ASM_REWRITE_TAC [ ] ; IMP_RES_THEN (ASSUME_TAC o ISPEC "x : *") FINITE_INSERT THEN IMP_RES_TAC ACI_REL_SELECT_LEMMA THEN PURE_ASM_REWRITE_TAC [ ] THEN IMP_RES_TAC ACI_REL_EXISTS_LEMMA THEN ASM_CASES_TAC "(x : *) IN s" THEN ASM_REWRITE_TAC [ ] THENL [ IMP_RES_THEN (\th. REWRITE_TAC [th]) ABSORPTION THEN CONV_TAC SELECT_CONV THEN ASM_REWRITE_TAC [ ] ; FIRST_ASSUM (CHOOSE_TAC o SPEC_ALL) THEN FIRST_ASSUM CHOOSE_TAC THEN EXISTS_TAC "SUC n" THEN ASM_REWRITE_TAC [ ] THEN EXISTS_TAC "x : *" THEN EXISTS_TAC "a : **" THEN ASM_REWRITE_TAC [IN_INSERT; DELETE_INSERT] THEN IMP_RES_THEN (\th. ASM_REWRITE_TAC [th]) DELETE_NON_ELEMENT THEN AP_TERM_TAC THEN ASM_REWRITE_TAC [ ] ] ] ) ) ;; %----------------------------------------------------------------------------- Finally, introduce a constant ACI_OP for OP via a constant specification. -----------------------------------------------------------------------------% let ACI_OP_DEF = new_specification `ACI_OP_DEF` [(`constant`, `ACI_OP`)] ACI_OP_EXISTS ;; let ACI_OP = " ACI_OP : (** -> ** -> **) -> ** -> (* -> **) -> (* -> bool) -> ** " ;; %----------------------------------------------------------------------------- ACI_OP on singletons. -----------------------------------------------------------------------------% let ACI_OP_SING = prove_thm(`ACI_OP_SING`, " ! op id . ASSOC_COMM_ID op id ==> ! f x . ^ACI_OP op id f {x} = f x ", ( REPEAT STRIP_TAC THEN ASSUME_TAC (INST_TYPE [(":*", ":**")] FINITE_EMPTY) THEN IMP_RES_TAC ACI_OP_DEF THEN FIRST_ASSUM (ASSUME_TAC o el 3 o CONJUNCTS o PURE_ONCE_REWRITE_RULE [ASSOC_COMM_ID_DEF]) THEN ASM_REWRITE_TAC [NOT_IN_EMPTY] ) ) ;; %----------------------------------------------------------------------------- ACI_OP on unions. -----------------------------------------------------------------------------% let ACI_OP_UNION = prove_thm(`ACI_OP_UNION`, " ! op id . ASSOC_COMM_ID op id ==> ! f s . FINITE s ==> ! t . FINITE t ==> ( op (^ACI_OP op id f (s UNION t)) (^ACI_OP op id f (s INTER t)) = op (^ACI_OP op id f s) (^ACI_OP op id f t) ) ", ( REPEAT GEN_TAC THEN DISCH_THEN \ ASSOC_COMM_ID_asm . let [ASSOC_asm; COMM_asm; _] = (CONJUNCTS o PURE_ONCE_REWRITE_RULE [ASSOC_COMM_ID_DEF]) ASSOC_COMM_ID_asm in let AC_conv = AC_CONV (ASSOC_asm, COMM_asm) in let (LR_AC_TAC : thm_tactic) (th) (asl, g) = let th' = EQT_ELIM (AC_conv " ^(lhs g) = ^(lhs (concl th)) ") TRANS th TRANS EQT_ELIM (AC_conv " ^(rhs (concl th)) = ^(rhs g) ") in ACCEPT_TAC th' (asl, g) in let ACI_OP_asm = MATCH_MP ACI_OP_DEF ASSOC_COMM_ID_asm in GEN_TAC THEN SET_INDUCT_TAC THEN REPEAT STRIP_TAC THENL [ REWRITE_TAC [UNION_EMPTY; INTER_EMPTY; ACI_OP_asm] THEN CONV_TAC AC_conv ; RES_THEN (ASSUME_TAC o AP_TERM "(op : ** -> ** -> **) (f (e : *))") THEN REWRITE_TAC [INSERT_UNION; INSERT_INTER] THEN ASM_CASES_TAC "(e : *) IN t" THEN ASM_REWRITE_TAC [ ] THENL [ IMP_RES_THEN (ASSUME_TAC o ISPEC "t : * -> bool") INTER_FINITE THEN IMP_RES_THEN (ASM_REWRITE_TAC o append [IN_INTER] o sing) ACI_OP_asm ; IMP_RES_TAC FINITE_UNION THEN IMP_RES_THEN (ASM_REWRITE_TAC o append [IN_UNION] o sing) ACI_OP_asm ] THEN FIRST_ASSUM LR_AC_TAC ] ) ) ;; let ACI_OP_DISJOINT = prove_thm(`ACI_OP_DISJOINT`, " ! op id . ASSOC_COMM_ID op id ==> ! f s t . FINITE s /\ FINITE t /\ DISJOINT s t ==> ( (^ACI_OP op id f (s UNION t)) = op (^ACI_OP op id f s) (^ACI_OP op id f t) ) ", ( PURE_ONCE_REWRITE_TAC [DISJOINT_DEF] THEN REPEAT STRIP_TAC THEN REPEAT_GTCL IMP_RES_THEN (PURE_ONCE_REWRITE_TAC o sing o SYM o SPEC_ALL) ACI_OP_UNION THEN IMP_RES_THEN (ASM_REWRITE_TAC o sing) ACI_OP_DEF THEN IMP_RES_THEN (REWRITE_TAC o sing o assert (mem "id : **" o vars o concl)) ASSOC_COMM_ID_DEF ) ) ;;