#|
 Copyright (C) 1994 by John Cowles.  All Rights Reserved.
 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.
 NO WARRANTY
 John Cowles PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS
 IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT
 NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
 ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
 IN NO EVENT WILL John Cowles BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
 PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
 ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
 LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
 BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
 DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the initial nqthm theory.

;                          A NOTE ON SHELLS
;                                 by
;                             John Cowles
;                     Department of Computer Science
;                         University of Wyoming
; The following is intended to give the reader some insight into SHELLS.
; Intuitively a nonempty SEQUENCE is an ordered list, possibly with
;  duplicates, of objects, ( Obj1 Obj2 ... ObjN ).
; There are two ways to recursively decompose sequences.
;
;  1. A SEQUENCE is either the EMPTY-SEQUENCE or a pair < Obj,Seq >.
;
;  2. A SEQUENCE is either the EMPTY-SEQUENCE or a pair [ Seq,Obj ].

;
;  Here Obj is an object, Seq is a sequence, and EMPTY-SEQUENCE is
;  the unique sequence which contains no objects.  Different pairing
;  brackets, < > and [ ], are used to enphasize which of the
;  decompositions is being used.
; Here the Shell Principle is used with decomposition 1 above to
;  add sequences as a "new" data type.

Event: Add the shell cons-seq-first, with bottom object function symbol emptyseq, with recognizer function symbol seq-p, and 2 accessors: first, with type restriction (none-of) and default value empty-seq; final, with type restriction (one-of seq-p) and default value empty-seq.

; default value
; ( CONS-SEQ-FIRST Obj Seq )     returns < Obj,Seq >.
; ( CONS-SEQ-FIRST Obj Non-Seq ) returns < Obj,EMPTY-SEQUENCE >.
; ( EMPTY-SEQ ) returns the EMPTY-SEQUENCE.
; ( SEQ-P Seq )     returns T.
; ( SEQ-P Non-Seq ) reTurns F.
; ( FIRST < Obj,Seq > ) returns Obj.
; ( FIRST (EMPTY-SEQ) ) returns (EMPTY-SEQ).
; ( FIRST Non-Seq )     returns (EMPTY-SEQ).
; ( FINAL < Obj,Seq > ) returns Seq.
; ( FINAL (EMPTY-SEQ) ) returns (EMPTY-SEQ).
; ( FINAL Non-Seq )     returns (EMPTY-SEQ).
; ==================
; The next two functions "coerce" non-sequences into
;  behaving like the EMPTY-SEQUENCE.

Definition: empty-seq-p (s) = ((s = empty-seq) ∨ (¬ seq-p (s)))

Definition: coerce-seq (s) = if seq-p (s) then s

else empty-seq endif

; The next three functions implement sequence decomposion 2 above.
; ( CONS-SEQ-LAST Seq Obj )     returns [ Seq,Obj ].
; ( CONS-SEQ-LAST Non-Seq Obj ) returns [ (EMPTY-SEQ),Obj ].
;     Here [ (EMPTY-SEQ),Obj ] is identified with < Obj,(EMPTY-SEQ) >.
; ( INITIAL [ Seq,Obj ] ) returns Seq.
; ( INITIAL (EMPTY-SEQ) ) returns (EMPTY-SEQ).
; ( INITIAL Non-Seq )     returns (EMPTY-SEQ).
; ( LAST [ Seq,Obj ] ) returns Obj.
; ( LAST (EMPTY-SEQ) ) returns (EMPTY-SEQ).
; ( LAST Non-Seq )     returns (EMPTY-SEQ).

Definition: cons-seq-last (s, c) = if empty-seq-p (s) then cons-seq-first (c, s)

else cons-seq-first (first (s), cons-seq-last (final (s), c)) endif

Definition: initial (s) = if empty-seq-p (s) then empty-seq

elseif final (s) = empty-seq then empty-seq else cons-seq-first (first (s), initial (final (s))) endif

Definition: last (s) = if empty-seq-p (s) then empty-seq

elseif final (s) = empty-seq then first (s)

else last (final (s)) endif

; The next 12 rewrite rules and 1 elimination rule would have been
;  explicitly added as axioms to the data base by the shell principle
;  if sequence decomposition 2 had been used, in place of decomposition 1,
;  as the basis for the shell which added sequences as a new type.

Theorem: initial-cons-seq-last initial (cons-seq-last (s, c)) = if seq-p (s) then s

else empty-seq endif

Theorem: initial-nseq-p (¬ seq-p (s)) → (initial (s) = empty-seq)

Theorem: initial-type-restriction (¬ seq-p (s)) → (cons-seq-last (s, c) = cons-seq-last (empty-seq, c))

Theorem: initial-lessp (seq-p (s) ∧ (s ≠ empty-seq)) → (count (initial (s)) < count (s))

Theorem: initial-lesseqp count (s) ≮ count (initial (s))

Theorem: last-cons-seq-last last (cons-seq-last (s, c)) = c

Theorem: last-nseq-p (¬ seq-p (s)) → (last (s) = empty-seq)

Theorem: last-lessp (seq-p (s) ∧ (s ≠ empty-seq)) → (count (last (s)) < count (s))

Theorem: last-lesseqp count (s) ≮ count (last (s))

; The next two lemmas are obvious facts used only as
; hints for the proof of the lemma CONS-SEQ-LAST-EQUAL.

Theorem: initial-apply-equals (x = y) → (initial (x) = initial (y))

Theorem: last-apply-equals (x = y) → (last (x) = last (y))

Theorem: cons-seq-last-equal (cons-seq-last (s1 , c1 ) = cons-seq-last (s2 , c2 )) = (if seq-p (s1 )

then if seq-p (s2 ) then s1 = s2

else s1 = empty-seq endif elseif seq-p (s2 ) then empty-seq = s2 else t endif ∧ (c1 = c2 ))

Theorem: cons-seq-last-initial-last cons-seq-last (initial (s), last (s)) = if seq-p (s) ∧ (s ≠ empty-seq) then s

else cons-seq-last (empty-seq, empty-seq) endif

Theorem: initial-last-elim (seq-p (s) ∧ (s ≠ empty-seq)) → (cons-seq-last (initial (s), last (s)) = s)

Theorem: count-cons-seq-last count (cons-seq-last (s, c)) = (1 + (if seq-p (s) then count (s)

else 0 endif + count (c)))

; The next rewrite rule would, in effect, have been implicitly added
;  as an axiom to the data base by the shell principle if sequence
;  decomposition 2 had been used, in place of decomposition 1, as the
;  basis for the shell which added sequences as a new type.

Theorem: cons-seq-last-not-empty-seq cons-seq-last (s, c) ≠ empty-seq

;====================================================================
; The next two functions give different versions of REVERSE.

Definition: reverse1 (s) = if empty-seq-p (s) then s

else cons-seq-last (reverse1 (final (s)), first (s)) endif

Definition: reverse2 (s) = if empty-seq-p (s) then s

else cons-seq-first (last (s), reverse2 (initial (s))) endif

; Use the Theorem Prover to verify the following proposed theorems.
;
; 1. For i=1 and i=2, ( EQUAL (REVERSEi (REVERSEi S)) S )
;
; 2. ( EQUAL (REVERSE1 S) (REVERSE2 S) )
; ==================================================================
; The next four functions give different versions of CONCATENATION.

Definition: concat1 (s1 , s2 ) = if empty-seq-p (s1 ) then coerce-seq (s2 )

else cons-seq-first (first (s1 ), concat1 (final (s1 ), s2 )) endif Definition: concat2 (s1 , s2 ) = if empty-seq-p (s2 ) then coerce-seq (s1 )

else concat2 (cons-seq-last (s1 , first (s2 )), final (s2 )) endif

Definition: concat3 (s1 , s2 ) = if empty-seq-p (s2 ) then coerce-seq (s1 )

else cons-seq-last (concat3 (s1 , initial (s2 )), last (s2 )) endif

Definition: concat4 (s1 , s2 ) = if empty-seq-p (s1 ) then coerce-seq (s2 )

else concat4 (initial (s1 ), cons-seq-first (last (s1 ), s2 )) endif

; Use the Theorem Prover to verify the following proposed theorems.
;
; 1. For i=1, i=2, i=3, and i=4, CONCATi is associative.
;
; 2. For i=1 and i=2; and for j=1, j=2, j=3, and j=4;
;      ( EQUAL (REVERSEi (CONCATj S1 S2))
;              (CONCATj (REVERSEi S2) (REVERSEi S1)) )
;
; 3. For i and j such that 1 <= i < j <= 4,
;      ( EQUAL (CONCATi S1 S2) (CONCATj S1 S2) )

Index

coerce-seq, 2, 5, 6 concat1, 5 concat2, 6 concat3, 6 concat4, 6 cons-seq-first, 2, 3, 5, 6 cons-seq-last, 3–6 cons-seq-last-equal, 4 cons-seq-last-initial-last, 4 cons-seq-last-not-empty-seq, 5 count-cons-seq-last, 5

empty-seq, 2–5 empty-seq-p, 2, 3, 5, 6

final, 3, 5, 6 first, 3, 5, 6

initial, 3–6 initial-apply-equals, 4 initial-cons-seq-last, 3 initial-last-elim, 4 initial-lesseqp, 4 initial-lessp, 4 initial-nseq-p, 3 initial-type-restriction, 4

last, 3–6 last-apply-equals, 4 last-cons-seq-last, 4 last-lesseqp, 4 last-lessp, 4 last-nseq-p, 4

reverse1, 5 reverse2, 5

seq-p, 2–5