Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Mon, 1 Mar 1993 21:42:06 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05037;
          Mon, 1 Mar 93 13:28:46 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Sun.COM by ted.cs.uidaho.edu (16.6/1.34) id AA05032;
          Mon, 1 Mar 93 13:28:40 -0800
Received: from Eng.Sun.COM (zigzag-bb.Corp.Sun.COM) by Sun.COM (4.1/SMI-4.1) 
          id AA26118; Mon, 1 Mar 93 13:28:19 PST
Received: from lara.Eng.Sun.COM by Eng.Sun.COM (4.1/SMI-4.1) id AA12705;
          Mon, 1 Mar 93 09:55:54 PST
Received: by lara.Eng.Sun.COM (4.1/SMI-4.1) id AA16991;
          Mon, 1 Mar 93 09:51:43 PST
Date: Mon, 1 Mar 93 09:51:43 PST
From: Paul.Loewenstein@COM.Sun.Eng (Paul Loewenstein)
Message-Id: <9303011751.AA16991@lara.Eng.Sun.COM>
To: info-hol@edu.uidaho.cs.ted
Cc: wishnu@nl.ruu.cs, Tom.Melham@uk.ac.cam.cl
In-Reply-To: Tom Melham's message of Mon, 01 Mar 93 17:05:51 +0000 <"swan.cl.ca.970:01.03.93.17.06.32"@cl.cam.ac.uk>
Subject: Finite Set
Content-Length: 1614


In contribution "koenig" (my proof of Koenig's lemma) there is
a definition of a finite set (expressed as its characteristic function):

The theorem Finite_EQ is useful for replacing any finite set by
a functional mapping of a finite set of natural numbers.


I do not guarantee the proof to run in the current version of HOL.
I also have a HOL90 version, which will be in the contrib of the
next HOL90 release.

let Bounded = new_definition (`Bounded`, "Bounded b P =
 (?f. (!x:*. P x ==> (?n. n < b /\ (x = f n))))");;

let Finite = new_definition (`Finite`,
  "Finite (P:*->bool) = (?b. Bounded b P)");;

% Finite can be expressed as an equality - useful for rewriting %

let Finite_EQ = TAC_PROOF (([],
  "!P. Finite P = (?b f. (!x:*. P x = (?n. n < b /\ (x = f n))))"),
 GEN_TAC THEN
 REWRITE_TAC[Finite;Bounded] THEN
 EQ_TAC THEN
 STRIP_TAC THENL
 [
  ASM_CASES_TAC "?x:*.P x" THENL
  [
   POP_ASSUM STRIP_ASSUME_TAC THEN
   EXISTS_TAC "b:num" THEN
   EXISTS_TAC "\n:num. P (f n) => f n | x:*" THEN
   BETA_TAC THEN
   GEN_TAC THEN
   EQ_TAC THENL
   [
    DISCH_THEN (\x. ASSUME_TAC x THEN ANTE_RES_THEN STRIP_ASSUME_TAC x) THEN
    EXISTS_TAC "n:num" THEN
    POP_ASSUM (ASSUME_TAC o SYM) THEN
    ASM_REWRITE_TAC[]
   ;
    STRIP_TAC THEN
    ASM_CASES_TAC "P ((f:num->*) n):bool" THEN
    ASM_REWRITE_TAC[]
   ]
  ;
   EXISTS_TAC "0" THEN
   POP_ASSUM (ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) THEN
   ASM_REWRITE_TAC[NOT_LESS_0]
  ]
 ;
  EXISTS_TAC "b:num" THEN
  EXISTS_TAC "f:num->*" THEN
  REPEAT STRIP_TAC THEN
  RES_TAC THEN
  EXISTS_TAC "n:num" THEN
  CONJ_TAC THEN
  FIRST_ASSUM ACCEPT_TAC
 ]);;