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; Wed, 19 May 1993 16:42:27 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28674;
          Wed, 19 May 93 08:31:24 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA28669; Wed, 19 May 93 08:31:20 -0700
Received: from localhost by panther.cs.uidaho.edu with SMTP 
          id AA05534 (5.65c/IDA-1.4.4 for info-hol@ted.cs.uidaho.edu);
          Wed, 19 May 1993 08:31:38 -0700
Message-Id: <199305191531.AA05534@panther.cs.uidaho.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Re: First-Order Reasoning and HOL
In-Reply-To: Your message of Wed, 19 May 93 14:38:48 +0700. <9305191239.AA28435@ted.cs.uidaho.edu>
Date: Wed, 19 May 93 08:31:37 -0700
From: Phil Windley <windley@panther.cs.uidaho.edu>
X-Mts: smtp


On Wed, 19 May 93 14:38:48 +0700, schneide@ira.uka.de wrote:
+------------
| Nuprl and Veritas both have dependent types, but HOL has nothing of the
| mentioned tactics.


Tom mentioned his paper on doing dependent types in HOL---recommended.

Another avenue is using restricted quantifiers.  They cannot be used to
model *every* dependent type, but for many applications of dependent types
(such as those demonstrated by Hanna in Veritas), they provide
specifications that are just as succinct and readable.  Wai Wong's library
on restricted quantification provides the needed proof support.

I have duplicated Hanna's factorization theorem for iterated arithmetic
hardware structures in HOL.  The notation looks almost identical. 

For example, here are the definition of factorizable and the factorization
theorem:

    "! (R:num -> num -> num -> * -> * -> bool) .
     factorizable R = 
      ! m k ::pos .
      ! a0 b0 ::N m .
      ! a1 b1 ::N k .
      ! c d :* .
      ! a b .
      let a = a0 + (a1 * m) and
          b = b0 + (b1 * m) in (
      (? e . (R k a1 b1 c e) /\ (R m a0 b0 e d)) ==>
      (R (k * m) a b c d))"

    "! w .
     ! m :: pos .
     ! (R:num -> num -> num -> * -> * -> bool) .
     ! A B :: V m .
     ! c d .
     (factorizable R) /\
     (proper R) ==>
     ((fold w (R m) A B c d) ==> (R (m EXP w) (VAL(m,w) A) (VAL(m,w) B) c d))"

Compare this to the definition and theorem in 

	Hanna, F. K., N. Daeche, and M. Longley, "Specification
        and Verification using Dependent Types," IEEE Transactions
        on Software Engineering, 16(9), September 1990.]

I'd be happy to send a copy of the complete proof file to anyone whose
interested.

--phil--