Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sun, 19 Mar 1995 15:01:06 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA263164235; Sun, 19 Mar 1995 07:43:55 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA263134229; Sun, 19 Mar 1995 07:43:49 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Sun, 19 Mar 1995 14:41:51 +0000 To: Mike Coe Cc: info-hol@leopard.cs.byu.edu Subject: Re: HOL sets In-Reply-To: Your message of "Sat, 18 Mar 1995 16:44:51 CST." <199503182244.QAA08322@arcadia.sctc.com> Date: Sun, 19 Mar 1995 14:41:46 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:005140:950319144154"@cl.cam.ac.uk> Mike Coe writes: | [...] what I want is a function that will return the union | all of the sets in the set A. See the definition "UNIONS" below. I don't prove many interesting theorems, but it might be a starting point (it's for `pred_sets', although it should be easy to modify it for `sets'). This was excised from my info-hol posting of 22 Apr 94 which gave a basic theory of countable sets. Proper theory of cardinality coming real soon now... John. %----------------------------------------------------------------------------% % Arbitrary union. % %----------------------------------------------------------------------------% let UNIONS = new_definition(`UNIONS`, "UNIONS (s:(*->bool)->bool) = { x | ?p. p IN s /\ x IN p }");; let UNIONS_0 = prove_thm(`UNIONS_0`, "UNIONS {} = {} :*->bool", REWRITE_TAC[UNIONS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[NOT_IN_EMPTY]);; let UNIONS_1 = prove_thm(`UNIONS_1`, "!s:*->bool. UNIONS {s} = s", REWRITE_TAC[UNIONS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[IN_SING] THEN REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC "s:*->bool" THEN ASM_REWRITE_TAC[]);; let UNIONS_2 = prove_thm(`UNIONS_2`, "!(s:*->bool) t. UNIONS {s,t} = s UNION t", REWRITE_TAC[UNIONS; EXTENSION] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REWRITE_TAC[IN_INSERT; IN_SING; IN_UNION] THEN REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC[] THEN W(EXISTS_TAC o rand o hd o fst) THEN ASM_REWRITE_TAC[]);; let IN_UNIONS = prove_thm(`IN_UNIONS`, "!(x:*) G. x IN (UNIONS G) = ?s. x IN s /\ s IN G", REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS] THEN CONV_TAC(ONCE_DEPTH_CONV SET_SPEC_CONV) THEN AP_TERM_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC THEN MATCH_ACCEPT_TAC CONJ_SYM);;