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, 22 Feb 1993 22:31:43 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12413;
          Mon, 22 Feb 93 14:19:36 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA12407;
          Mon, 22 Feb 93 14:19:26 -0800
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Mon, 22 Feb 1993 22:18:42 +0000
To: coe@edu.uidaho.cs.leopard (Mike Coe)
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: set library
In-Reply-To: Your message of Mon, 22 Feb 93 13:56:38 -0800. <9302222156.AA27064@leopard.cs.uidaho.edu>
Date: Mon, 22 Feb 93 22:18:37 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.301:22.02.93.22.18.45"@cl.cam.ac.uk>


Hi, you write:

> If I have the following on my assumption list
>
> "~(Op4p( s(t + 1))
>    IN {32,34,56,57,54,48,51,50,53,52,49,55})
>
> how can I infer that
>
> ~(Op4p (s(t+1)) IN {32})
>
> this seems obvious.

Indeed, the theorem can be proved quite easily by rewriting the assumptions and
conclusion with the theorem |IN_INSERT|:

  IN_INSERT = |- !x y s. x IN (y INSERT s) = (x = y) \/ x IN s

remembering that finite set enumerations are just syntax for repeated
|INSERT|s. Viz:

  load_library `sets`;;

  set_goal(["~(Op4p( s(t + 1):*) IN {32,34,56,57,54,48,51,50,53,52,49,55})"],
           "~(Op4p( s(t + 1):*) IN {32})");;

  e(RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT; DE_MORGAN_THM]) THEN
    ASM_REWRITE_TAC[IN_INSERT]);;

  let thm = top_thm();;

John.