Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 21 Jun 1993 05:51:18 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02273;
          Sun, 20 Jun 93 21:38:32 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA02268; Sun, 20 Jun 93 21:38:29 -0700
Received: from toadflax.cs.ucdavis.edu by leopard.cs.uidaho.edu (16.7/1.34) 
          id AA05360; Sun, 20 Jun 93 21:40:54 -0700
Received: by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.3) id AA13884;
          Sun, 20 Jun 93 21:38:46 PDT
Date: Sun, 20 Jun 93 21:38:46 PDT
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9306210438.AA13884@toadflax.cs.ucdavis.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: CASES vs. INDUCT



I'm afraid that I'm going about something the "wrong" way because
I don't know the easy way:

If I have a type without recursive constructor:

   (1)   Thing = cons1 | cons2 num | cons3 num num ...

and I need to prove something like

   (2)   ! t:Thing. P t

Although it seems "natural" that I should chose CASES_THENL here, I find
that INDUCT_THEN works much more nicely. The former would give me the
existence theorems as an assumption, whereas induction neatly lays out
universally quantified subgoals for each case (albeit from the "induction" 
viewpoint hey are all base cases since the type isn't recursive...). 

Quite often, when trying to prove something like (2) "by construction",
all I want to do is crack open that !t.P into subgoals

  P(cons1) and !n. P(cons2 n) and !n n' P(cons3 n n')

and show how each case holds. Is this a silly use of INDUCT_THEN ? Is there
a more natural way to "rewrite" !t. P t into the possibilities for t, 
universally quantified? 

Rob