Return-Path: <guttman@linus.mitre.org>
To: imps@linus.mitre.org
Cc: guttman@linus.mitre.org
Subject: New version of Imps, improved simplifier 
X-Postal-Address: MITRE, Mail Stop A118 
X-Postal-Address: 202 Burlington Rd. 
X-Postal-Address: Bedford, MA 01730-1420 USA
X-Telephone-Number: 617 271 2654; Fax 617 271 3816
Return-Receipt-To: guttman@linus.mitre.org
Date: Mon, 14 Feb 1994 16:53:16 -0500
From: "Joshua D. Guttman" <guttman@linus.mitre.org>

A new version of Imps is now available for ftp at math.harvard.edu.  The
theory library has been extended somewhat.  However, the main change is in
the simplifier's treatment of conditional expressions and undefinedness.

If-then-else terms in which either the consequent or the alternative is
necessarily undefined arise in several ways, sometimes by simplification
itself, and sometimes from the Imps representation of generic objects such as
sets and sequences.  The simplifier, which generally avoids making
case-splits on its own, was previously not too clever about formulas
containing terms of this kind.

It now handles them very well.  It implements the additional rules given
below.  For the sake of compatibility, or to check how libraries of proofs
change, I've included procedures to toggle between the old and the new
versions.  

To do so, type 

(use-old-constructor-simplifiers) or 
(use-new-constructor-simplifiers)

to the *tea* buffer.  The *new* ones are now the default.  

	Josh
~~~~~~~~~~~~~~~~

A.  For equalities: (?sigma is an undefined term with syntactic sort sigma.) 

;; Implements the rules:
;;
;; 1.  if(A, s, ?sigma) = t   iff  A and s = t
;; 2.  if(A, ?sigma, s) = t   iff  not(A) and s = t
;; 3.  t = if(A, s, ?sigma)   iff  A and t = s
;; 4.  t = if(A, ?sigma, s)   iff  not(A) and t = s

B.  For quasi-equalities [ s == t means ((#(s) or #(t)) implies s=t),
			   where in turn # means "is defined". ]

;; Implements the rules:
;;
;; 1.  if(A, s, ?sigma) == t iff if_form(A, s == t, not(#(t)))
;; 2.  if(A, ?sigma, s) == t iff if_form(A, not(#(t)), s == t)
;; 3.  When s is necessarily defined:
;;      if(A, u, s) == t     iff if_form(A, u == t, s=t)
;; 4.  When u is necessarily defined:
;;      if(A, u, s) == t     iff if_form(A, u=t, s == t)
;;
;; And the symmetrical cases in which the conditional is on the right hand
;; side.    

C.  For definedness assertions:

;; Implements the rules:
;;
;; 1.  #(if(A, s, ?sigma)) iff A and #(s)
;; 2.  #(if(A, ?sigma, s)) iff not(A) and #(s)
;; 3.  When s is necessarily defined:
;;     #(if(A, s, t))      iff A implies #(t)
;; 4.    When t is necessarily defined:
;;     #(if(A, s, t))      iff not(A) implies #(s)

D.  For sort-definedness assertions:

;; Implements the rules:
;;
;; 1.  When t is necessarily not defined in sigma:
;;     #(if(A, s, t), sigma) iff A and #(s, sigma)
;; 2.  When s is necessarily not defined in sigma:
;;     #(if(A, s, t), sigma) iff not(A) and #(s)
;; 3.  When s is necessarily defined in sigma:
;;     #(if(A, s, t))      iff A implies #(t, sigma)
;; 4.  When t is necessarily defined in sigma:
;;     #(if(A, s, t))      iff not(A) implies #(s, sigma)

E.  For atomic predications:

;; Implements the rules for PREDICATES P:
;;
;; 1.  P(... if(A, s, ?sigma) ...) iff A and P(... s ...)
;; 2.  P(... if(A, ?sigma, s) ...) iff not(A) and P(... s ...)
;; 

F.  For function applications: 

;; Implements the rules for FUNCTIONS f:
;;
;; 1.  f(... if(A, s, ?sigma) ...)  == if(A, f(... s ...), ?tau)
;; 2.  f(... if(A, ?sigma, s) ...)  == if(not(A), f(... s ...), ?tau)
;;
;; where tau is the range sort of f.