Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 1 Jun 1993 13:48:52 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05800; Tue, 1 Jun 93 05:36:34 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from imec.be by ted.cs.uidaho.edu (16.6/1.34) id AA05745; Tue, 1 Jun 93 05:36:22 -0700 Received: from imec.be (imec) by imecgate.imec.be with SMTP (5.65c/IDA-1.4.4-IMEC); Tue, 1 Jun 1993 13:40:46 +0200 Date: Tue, 1 Jun 93 13:39:54 +0200 From: Catia Angelo Message-Id: <9306011139.AA20164@imec.be> Original-Received: by imec.be Tue, 1 Jun 93 13:39:54 +0200 PP-warning: Illegal Received field on preceding line To: info-hol@ted.cs.uidaho.edu Subject: MAX generalization Hi everybody, In order to reason about the phases of signals in Silage programs, I have made some definitions about the greatest of a list of natural numbers and I have also proved some theorems about them. My main interest was to develop an infra-structure to reason about inequalities involving the greatest of a list of natural numbers. Next I list the definitions, theorems and tactics that I used. If anybody is interested in having the code, I will be glad to share it. Catia Angelo catia@imec.be ------------------------------------------------------------------- Constants -- GRT ":(num)list -> (num -> num)" GREATEST ":(num)list -> num" GEQKL ":(num)list -> (num -> bool)" GKL ":(num)list -> (num -> bool)" Definitions -- GRT |- (!ref. GRT[]ref = ref) /\ (!hd tl ref. GRT(CONS hd tl)ref = GRT tl(hd < ref => ref | hd)) GREATEST |- !l. GREATEST l = GRT l 0 GEQKL |- (!k. GEQKL[]k = T) /\ (!h t k. GEQKL(CONS h t)k = k >= h /\ GEQKL t k) GKL |- (!k. GKL[]k = T) /\ (!h t k. GKL(CONS h t)k = k > h /\ GKL t k) Theorems -- GREATEST_N_ZERO |- !n. GREATEST[n;0] = n GRT_REF |- !l ref. k >= (GRT l ref) = k >= ref /\ k >= (GRT l 0) GRT_REF' |- !l ref. k > (GRT l ref) = k > ref /\ k > (GRT l 0) GREATEST_GEQKL |- !l k. k >= (GREATEST l) = GEQKL l k GREATEST_GKL |- !l k. ~(l = []) ==> (k > (GREATEST l) = GKL l k) GREATEST_GKL_CONS |- !k hd tl. k > (GREATEST(CONS hd tl)) = GKL(CONS hd tl)k GEQKL_CONS |- !tl hd k. GEQKL[hd]k /\ GEQKL tl k = GEQKL(CONS hd tl)k GEQKL_APP |- !l1 l2 k. GEQKL l1 k /\ GEQKL l2 k = GEQKL(APPEND l1 l2)k GREATEST_APP |- !l1 l2 k. k >= (GREATEST l1) /\ k >= (GREATEST l2) = k >= (GREATEST(APPEND l1 l2)) GEQKL_APP_SYM |- !l1 l2 k. GEQKL(APPEND l1 l2)k = GEQKL(APPEND l2 l1)k GREATEST_APP_SYM |- !l1 l2 k. k >= (GREATEST(APPEND l1 l2)) = k >= (GREATEST(APPEND l2 l1)) GEQKL_TRANS |- !l k1 k2. GEQKL l k1 /\ k2 >= k1 ==> GEQKL l k2 GEQKL_EVERY |- !l k. GEQKL l k = EVERY(\el. k >= el)l GREATEST_EVERY |- !l k. k >= (GREATEST l) = EVERY(\el. k >= el)l EVERY_GREATEST |- !l. EVERY(\el. (GREATEST l) >= el)l GREATEST_GRT |- !hd tl. GREATEST(CONS hd tl) = GRT tl hd REF_LESS_EQ_GRT |- !l ref. ref <= (GRT l ref) GRT_APPEND |- !l1 l2 k. k >= (GRT l1 0) /\ k >= (GRT l2 0) = k >= (GRT(APPEND l1 l2)0) GRT_APP_SYM |- !l1 l2 k. k >= (GRT(APPEND l1 l2)0) = k >= (GRT(APPEND l2 l1)0) GRT_EVERY |- !l k. k >= (GRT l 0) = EVERY(\el. k >= el)l GRT_CONS |- !hd tl. GRT(CONS hd tl)0 = GRT tl hd GRT_REF_IS_GRT_0_OR_REF |- !l h. GRT l h = (h < (GRT l 0) => GRT l 0 | h) GRT_REF_IS_GREATEST_OR_REF |- !l h. GRT l h = (h < (GREATEST l) => GREATEST l | h) GEQKL_GREATEST |- !l. GEQKL l(GREATEST l) GEQKL_GRT |- !l. GEQKL l(GRT l 0) GRT_0_LESS_EQ_GRT_REF |- !l ref. (GRT l 0) <= (GRT l ref) GEQKL_GRT' |- !l ref. GEQKL l(GRT l ref) GRT_TRANS |- !l k1 k2. (GRT l k1) <= k2 ==> (GRT l k2 = k2) GREATEST_TRANS |- (GREATEST l) <= k ==> (GRT l k = k) GREATEST_CONS |- !h t. GREATEST(CONS h t) = GREATEST[h;GREATEST t] GREATEST_OF_ONE |- !k. GREATEST[k] = k GREATEST_OF_K_AND_0 |- !k. GREATEST[k;0] = k GREATEST_OF_0_AND_K |- !k. GREATEST[0;k] = k PLUS_DISTRIB_GREATEST |- !l k. ~(l = []) ==> ((GREATEST l) + k = GREATEST(MAP(\el. el + k)l)) PLUS_DISTRIB_GREATEST_CONS |- !hd tl k. (GREATEST(CONS hd tl)) + k = GREATEST(MAP(\el. el + k)(CONS hd tl)) SUB_DISTRIB_GREATEST |- !l k. ~(l = []) ==> ((GREATEST l) - k = GREATEST(MAP(\el. el - k)l)) SUB_DISTRIB_GREATEST_CONS |- !hd tl k. (GREATEST(CONS hd tl)) - k = GREATEST(MAP(\el. el - k)(CONS hd tl)) GREATEST_OF_Ab |- !a b. (GREATEST[a;b]) >= a /\ (GREATEST[a;b]) >= b ========================================================================== I also got some tactics: %-----------------------------------------------------------------------% % FLAT_GREATEREQ_GREATEST_TAC: tactic % %-----------------------------------------------------------------------% % A ?- x >= (GREATEST[GREATEST[ch1;ch2];GREATEST[ch3;ch4]]) % % ==================================================================== % % A ?- (x >= ch1 /\ x >= ch2) /\ x >= ch3 /\ x >= ch4 % %-----------------------------------------------------------------------% %-----------------------------------------------------------------------% % FLAT_GREATER_GREATEST_TAC: tactic % %-----------------------------------------------------------------------% % A ?- x > (GREATEST[GREATEST[ch1;ch2];GREATEST[ch3;ch4]]) % % ==================================================================== % % A ?- (x > ch1 /\ x > ch2) /\ x > ch3 /\ x > ch4 % %-----------------------------------------------------------------------% %-----------------------------------------------------------------------% % EVERY_GREATEST_TAC: tactic % %-----------------------------------------------------------------------% % EVERY_GREATEST_TAC can solve goals of the form: % % A ?- GREATEST[ch1; ch2; ch3; ch4] >= GREATEST[GREATEST[ch1; ch2]; % % GREATEST[ch3; ch4]] % %-----------------------------------------------------------------------%