Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: Andy.Gordon@uk.ac.cam.cl
Message-Id: <9202141042.AA11952@oxley>
Date: 14 Feb 1992 1041-WET (Friday)
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Restricted quantification
In-Reply-To: Message of Sat, 08 Feb 92 22:50:04 PST from chou@edu.ucla.cs <9202090650.AA17805@maui.cs.ucla.edu>

Ching Tsun asks:
    Has any of you experienced HOL hackers made serious use of
    restricted quantifications (i.e., things like !x::P.F[x])?
    I'd like to know how you think about them and what tools
    you have written to manipulate them.  Personally I have a
    feeling that restricted quantifications can be very useful.
    Yet I have so little experience with HOL that I fear my
    fondness of them was due entirely to the nice syntax and,
    as a practical matter, I really should eschew them.

I've found restricted universal quantifications to be perfect for giving
the semantics in HOL of a dataflow language I've been working with that
has declarations like the following,

    (i:1..64):: A[i] = B[i] * C[i]

This is meant to meant that for i ranging between 1 and 64, vector element
A[i] is to be the product of elements B[i] and C[i].  If I define a constant
TO to satisfy the equation,

    !m n i. (m TO n) i = (m <= i /\ i <= n)

then I can render the above declaration in HOL as

    !i :: 1 TO 64. A(i) = B(i) * C(i)

The alternative notation, without restricted quantifications, would be:

    !i. (m TO n)i ==> (A i = (B i) * (C i))

It seems better to go to a little trouble to prove some theorems about
restricted quantifications, and get the benefit of a HOL notation that is
almost the same as the dataflow language, than not.

I've taken a demand-driven approach to supporting restricted quantifications,
and only proved general theorems when it helped me get my work done, which
in this case was to do some program transformations.  Anyway, here is a
listing of a theory with some theorems about TO and restricted
quantifications that were useful in doing program transformations.  If you
or anyone else wants the source files I can supply them.

Do post a summary of opinions of and work done with restricted quantifications.

Andy Gordon.

The Theory range
Parents --  HOL
Constants --  TO ":num -> (num -> (num -> bool))"
Infixes --  TO ":num -> (num -> (num -> bool))"
Definitions --  TO  |- !m n. m TO n = (\x. m <= x /\ x <= n)
Theorems --
  TO_EMPTY  |- m > n ==> (m TO n = (\x. F))
  TO_SINGLE  |- m TO m = $= m
  TO_TOP_SPLIT
    |- !m n. m <= n ==> (m TO (SUC n) = (\x. (m TO n)x \/ (SUC n = x)))
  TO_BOTTOM_SPLIT
    |- !m n. m < n ==> (m TO n = (\x. (m = x) \/ ((SUC m) TO n)x))
  TO_MID_SPLIT
    |- !l m n.
        (m TO n)l ==> (m TO n = (\i. (m TO l)i \/ ((SUC l) TO n)i))
  TO_SHIFT  |- !m n. m TO n = ((SUC m) TO (SUC n)) o SUC
  TO_SHIFT_N  |- !m n k. m TO n = ((m + k) TO (n + k)) o (\i. i + k)
  R_ALL_CONJ_DIST
    |- !P Q R. (!i :: P. Q i /\ R i) = (!i :: P. Q i) /\ (!i :: P. R i)
  R_ALL_DISJ_DIST
    |- !P Q R.
        (!i :: \i. P i \/ Q i. R i) = (!i :: P. R i) /\ (!i :: Q. R i)
  R_ALL_UNIQUE  |- !P j. (!i :: $= j. P i) = P j
  R_ALL_SINGLE  |- !P m. (!i :: m TO m. P i) = P m
  R_ALL_TOP_SPLIT
    |- !P m n.
        m <= n ==>
        ((!i :: m TO (SUC n). P i) = (!i :: m TO n. P i) /\ P(SUC n))
  R_ALL_BOTTOM_SPLIT
    |- !P m n.
        m < n ==>
        ((!i :: m TO n. P i) = P m /\ (!i :: (SUC m) TO n. P i))
  R_ALL_MID_SPLIT
    |- !P m n l.
        (m TO n)l ==>
        ((!i :: m TO n. P i) =
         (!i :: m TO l. P i) /\ (!i :: (SUC l) TO n. P i))
  R_ALL_SHIFT_N
    |- !P m n k.
        (!i :: (m + k) TO (n + k). P i) = (!i :: m TO n. P(i + k))
  R_ALL_SHIFT
    |- !P m n.
        (!i :: (SUC m) TO (SUC n). P i) = (!i :: m TO n. P(SUC i))

******************** range ********************