#|
Copyright (C) 1994 by Alex Bronstein and Carolyn Talcott.  All Rights
Reserved.
You may copy and distribute verbatim copies of this Nqthm-1992 event script as
you receive it, in any medium, including embedding it verbatim in derivative
works, provided that you conspicuously and appropriately publish on each copy
a valid copyright notice "Copyright (C) 1994 by Alex Bronstein and Carolyn
Talcott.  All Rights Reserved."
NO WARRANTY
Alex Bronstein and Carolyn Talcott PROVIDE 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 Alex Bronstein or Carolyn Talcott 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 library "mlp" using the compiled version.

; macc.bm
;  Circuit is similar to acc, but uses multiplication instead of
; addition, i.e. it's a multiplying accumulator.  It's expressed in CSXA form,
; which is the form we've currently settled on.
; NOTE that it has to be initialized with 1 in order to function right! See
; prod0 for what happens with 0-initialization...
;
;;; DEFINITION OF CIRCUIT:
#|
(setq sysd '(sy-macc ( x)
(Ymacc S Times x Ymacc2)

(Ymacc2 R 1 Ymacc)
))
(setq macc '(
; BM DEFINITIONS and A2 LEMMAS, generated by BMSYSD:
|#
; comb_times.bm: Times combinational element.
; U7-DONE
; no character function def since BM already knows about Times..
; Everything below generated by:     (bmcomb 'times '() '(x y))

Definition: s-times (x, y) = if empty (x) then e

else a (s-times (p (x), p (y)), l (x) ∗ l (y)) endif

;; A2-Begin-S-TIMES

Theorem: a2-empty-s-times empty (s-times (x, y)) = empty (x)

Theorem: a2-e-s-times (s-times (x, y) = e) = empty (x)

Theorem: a2-lp-s-times len (s-times (x, y)) = len (x)

Theorem: a2-lpe-s-times eqlen (s-times (x, y), x)

Theorem: a2-ic-s-times (len (x) = len (y)) → (s-times (i (c x, x), i (c y, y)) = i (c x ∗ c y, s-times (x, y)))

Theorem: a2-lc-s-times (¬ empty (x)) → (l (s-times (x, y)) = (l (x) ∗ l (y)))

Theorem: a2-pc-s-times p (s-times (x, y)) = s-times (p (x), p (y))

Theorem: a2-hc-s-times ((¬ empty (x)) ∧ (len (x) = len (y))) → (h (s-times (x, y)) = (h (x) ∗ h (y)))

Theorem: a2-bc-s-times (len (x) = len (y)) → (b (s-times (x, y)) = s-times (b (x), b (y)))

Theorem: a2-bnc-s-times (len (x) = len (y)) → (bn (n, s-times (x, y)) = s-times (bn (n, x), bn (n, y)))

;; A2-End-S-TIMES
; eof:comb_times.bm

Definition: topor-sy-macc (ln) = if ln = 'ymacc then 1

elseif ln = 'ymacc2 then 0 else 0 endif

Definition: sy-macc (ln, x) = if ln = 'ymacc then s-times (x, sy-macc ('ymacc2, x))

elseif ln = 'ymacc2

then if empty (x) then e

else i (1, sy-macc ('ymacc, p (x))) endif else sfix (x) endif

;; A2-Begin-SY-MACC

Theorem: a2-empty-sy-macc empty (sy-macc (ln, x)) = empty (x)

Theorem: a2-e-sy-macc (sy-macc (ln, x) = e) = empty (x)

Theorem: a2-lp-sy-macc len (sy-macc (ln, x)) = len (x)

Theorem: a2-lpe-sy-macc eqlen (sy-macc (ln, x), x)

Theorem: a2-pc-sy-macc p (sy-macc (ln, x)) = sy-macc (ln, p (x))

;; A2-End-SY-MACC
;;; SPEC definition:

Definition: numer-macc (x) = if empty (x) then 1

else numer-macc (p (x)) ∗ l (x) endif

; this is the standard extension from last-char-fun to MLP-string-fun.

Definition: spec-macc (x) = if empty (x) then e

else a (spec-macc (p (x)), numer-macc (x)) endif

;;; Circuit CORRECTNESS:
; Macc-correct-ax is a "predicative correctness statement", i.e. what we would
; do if we didn't have functional equality as a specification method, but
; instead used a purely axiomatic approach.

Theorem: macc-correct-ax (¬ empty (x)) → (l (sy-macc ('ymacc, x)) = numer-macc (x))

; to go to a functional equality once we have the "last" (ax) statement is
; a trivial induction, if we start out with an P-L split which is unnatural
; for BM, so we force it w/ a USE hint of A-p-l-split
; We really would like to use it as a one-time rewrite, but it's a looping
; rule, so we can't.  Instead we have to use it in USE hints, which in case
; of induction, makes things more complex than they should.

Theorem: a-p-l-split (¬ empty (x)) → (sy-macc ('ymacc, x)

= a (p (sy-macc ('ymacc, x)), l (sy-macc ('ymacc, x))))

Theorem: macc-correct sy-macc ('ymacc, x) = spec-macc (x)

; eof: macc.bm

Index

a, 2, 4 a-p-l-split, 4 a2-bc-s-times, 3 a2-bnc-s-times, 3 a2-e-s-times, 2 a2-e-sy-macc, 3 a2-empty-s-times, 2 a2-empty-sy-macc, 3 a2-hc-s-times, 2 a2-ic-s-times, 2 a2-lc-s-times, 2 a2-lp-s-times, 2 a2-lp-sy-macc, 3 a2-lpe-s-times, 2 a2-lpe-sy-macc, 3 a2-pc-s-times, 2 a2-pc-sy-macc, 3

b, 3 bn, 3

e, 2–4 empty, 2–4 eqlen, 2, 3

h, 2

i, 2, 3

l, 2, 4 len, 2, 3

macc-correct, 4 macc-correct-ax, 4

numer-macc, 4

p, 2–4

s-times, 2, 3 sfix, 3 spec-macc, 4 sy-macc, 3, 4

topor-sy-macc, 3