#|
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 initial thm theory.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  TH_ARITHMETIC.BM
;;;
;;; This file contains natural number arithmetic lemmas for BM.
;;;
;; FUNDAMENTAL:
; standard Nint-induction, which sometime we want to force

Definition: ari-add1-induct (n) = if n ≃ 0 then t

else ari-add1-induct (n − 1) endif

;; PLUS and TIMES: a lot of the basic stuff is in "linear
;; arithmetic" already.

Theorem: ari-plus-0-ident-r (x + 0) = fix (x)

Theorem: ari-plus-0-ident-l (0 + x) = fix (x)

Theorem: ari-times-0-cancel-r (y ∗ 0) = 0

Theorem: ari-times-0-cancel-l (0 ∗ y) = 0

; Note: each of the 4 previous lemmas has a corresponding strong
; version, which is more powerful, since it trivially implies the
; weak versions. But they are too AGRESSIVE because they trigger
; EVERY TIME we have a PLUS/TIMES expression, and generate a case
; disjunction as to whether one of the arguments is ZEROP, which
; may be totally irrelevant to the proof at hand. In fact, in
; testing just this arithmetic package with the strong or the weak
; axioms, and observing the proofs, the conclusion was that the
; proofs based on the weak theorems never reestablished the strong
; versions (as intermediate lemmas) and the theorems only triggered
; when they were guaranteed to be relevant, yielding fewer or equal
; number of case disjunctions, and significantly faster proofs.
; We therefore prove the strong theorems but keep them disabled, to
; be enabled explicitly when needed.

Theorem: ari-plus-0-ident-r2 (z ≃ 0) → ((x + z) = fix (x))

Event: Disable ari-plus-0-ident-r2.

Theorem: ari-plus-0-ident-l2 (z ≃ 0) → ((z + x) = fix (x))

Event: Disable ari-plus-0-ident-l2.

Theorem: ari-times-0-cancel-r2 (z ≃ 0) → ((y ∗ z) = 0)

Event: Disable ari-times-0-cancel-r2.

Theorem: ari-times-0-cancel-l2 (z ≃ 0) → ((z ∗ y) = 0)

Event: Disable ari-times-0-cancel-l2.

; now onto more properties..

Theorem: ari-times-0-equal ((x ∗ y) = 0) = ((x ≃ 0) ∨ (y ≃ 0))

Theorem: ari-times-1-ident (x ∗ 1) = fix (x)

Theorem: ari-times-add1 (z ∈ N) → ((y + (y ∗ z)) = (y ∗ (1 + z)))

; WARNING: ARI-times-commute sometime loops, so we leave it
; disabled.

Theorem: ari-times-commute (x ∗ y) = (y ∗ x)

Event: Disable ari-times-commute.

Theorem: ari-times-plus-distribute ((x ∗ x1 ) + (x ∗ x2 )) = (x ∗ (x1 + x2 ))

; WARNING: ARI-lessp-sub1 looped infinitely once (in remainder
; context). It does not seem to be used anywhere. So we leave it
; DISABLEd for ever.

Theorem: ari-lessp-sub1 ((p ≄ 0) ∧ (q ≄ 0)) → (((p − 1) < (q − 1)) = (p < q))

Event: Disable ari-lessp-sub1.

Theorem: ari-lessp-plus ((n + p) < (n + q)) = (p < q)

Theorem: ari-lessp-times (n ≄ 0) → (((n ∗ p) ≮ (n ∗ q)) = (p ≮ q))

Theorem: ari-lessp-times2 (n ≄ 0) → (((n ∗ p) < (n ∗ q)) = (p < q))

;; DIFFERENCE:

Theorem: ari-diff-less-0 (a ≮ b) → ((b − a) = 0)

Theorem: ari-lessp-diff (0 < (p − q)) = (q < p)

Theorem: ari-diff-not-0 ((x − y) = 0) = (y ≮ x)

Theorem: ari-diff-0 (x ≃ 0) → ((x − y) = 0)

Theorem: ari-times-diff-distribute ((x ∗ x1 ) − (x ∗ x2 )) = (x ∗ (x1 − x2 ))

Theorem: ari-diff-x-x-0 (x − x) = 0

; Difference recurses on both arguments, but sometime we need to
; recurse just on the first one.
; Note that this lemma also appears in Hunt's thesis (rn 451),
; p.119, but with "NIL" as BM-use.  It may interfere with regular
; diff-induction, in which case we'll disable it locally, or more
; drastically, disable here, and enable locally.

Theorem: ari-diff-add1 ((1 + n) − p) = if p < (1 + n) then 1 + (n − p)

else 0 endif

;; REMAINDER:
; ARI-lessp-remainder is fundamental.

Theorem: ari-lessp-remainder (p ≄ 0) → ((n mod p) < p)

; Note that the following phrasing found in Hunt's thesis, p.120,
; but even though it seems more powerful, it failed to allow BM to
; deduce a contradiction from (not (equal (rem n 4) 0..3)) so we
; stick with ours.
;(prove-lemma ARI-lessp-remainder (rewrite generalize)
;(equal (lessp (remainder n p) p)
;       (not (zerop p)))
;)
; Remainder recurses on both arguments, but sometime we need to
; recurse just on the first one.

Theorem: ari-remainder-add1 (p ≄ 0) → (((1 + n) mod p)

= if (n mod p) = (p − 1) then 0 else 1 + (n mod p) endif)

; This more specific version of the same in the case of remainder
; by 2 is true and provable, but does not help anything.  We leave
; it commented out, for future generations...
;
;(prove-lemma ARI-remainder-2-not (rewrite)
;(implies (and (numberp n) (numberp r))
;  (equal (not (equal (remainder n 2) r))
; (if (equal r 0) (equal (remainder n 2) 1)
;     (if (equal r 1) (equal (remainder n 2) 0)
;         T))))
;)
;;; eof: th_arithmetic.bm

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; STRINGADD.BM: string theory with <add,past,last> shell for BM.
;;;
;;; The normalization we are trying to achieve with all the basic
;;; theorems is:  I (all the way to the outside)... , then A...,
;;; then P & L (all the way in).

;;;
;;; Note that all the H/B stuff only comes into real play with
;;; pipelines. The rules of interaction with base constructors are
;;; defined in the H/B theory and a bit fuzzy (they came in late
;;; in the work, and are a bit ad-hoc).
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; String type definition:
; constructor: A, destructors: P, L, empty string: (e).

Event: Add the shell a, with bottom object function symbol e, with recognizer function symbol stringp, and 2 accessors: p, with type restriction (one-of stringp) and default value e; l, with type restriction (none-of) and default value e.

;PN: iterations of the P constructor, useful in specification, and
;    maybe in proofs. Note however that in hand proofs we use it
;    only as a macro, whereas the general definition is recursive
;    and hence may not always be expanded appropriately by BM.
;    Beware...

Definition: pn (n, x) = if n ≃ 0 then x

else pn (n − 1, p (x)) endif

; Empty: non-strings are treated as empty, which is a standard
; BM trick.

Definition: empty (x) = ((¬ stringp (x)) ∨ (x = e))

; These 3 lemmas allow running w/ empty DISABLED 99% of the time,
; winning big.

Theorem: str-empty-p empty (x) → empty (p (x))

; STR-Empty-Stringp was intended to deal w/ the silly case brought
; on by the (inappropriate when Empty disabled) P/L elimination
; theorem.  Instead it seems to be a LOSER: helping its purpose
; rarely, and triggering all over the place:

;(prove-lemma STR-Empty-Stringp (rewrite)
;(implies (not (empty x))
;  (stringp x))
;)

Theorem: str-empty-count (¬ empty (x)) → (count (p (x)) ≠ count (x))

; STR-P-L-Elim provides an elimination more suitable to running
; w/ empty disabled, than the shell P-L-Elim.  %%% BUT CURRENTLY BM
; REJECTS IT ON GROUNDS OF NOT BEING ABLE TO HANDLE MANY ELIM
; LEMMAS FOR ONE DESTRUCTOR. %%%
;
;(prove-lemma STR-P-L-Elim (ELIM)
;(implies (not (empty x))
;  (equal (A (P x) (L x))
; x))
;)
; Late decision, but helpful nonetheless:

Event: Disable empty.

Definition: len (x) = if empty (x) then 0

else 1 + len (p (x)) endif

; EQLEN was suggested by Shankar as a way to push BM toward a
; better, richer induction scheme.

Definition: eqlen (x, y) = if empty (x) ∧ empty (y) then t

elseif empty (x) ∨ empty (y) then f else eqlen (p (x), p (y)) endif

; the idea is that EQLEN(x,y) <=> |x| = |y| which can be proved,
; but should not be used in general..

Theorem: eqlen-is-equal-len eqlen (x, y) = (len (x) = len (y))

Event: Disable eqlen-is-equal-len.

; EQLEN-EMPTY is a KEY inference about EQLEN .

Theorem: eqlen-empty eqlen (x, y) → (empty (x) = empty (y))

;; Derived constructors:

Definition: i (u, x) = if empty (x) then a (e, u)

else a (i (u, p (x)), l (x)) endif

Definition: h (x) = if empty (x) then e

elseif empty (p (x)) then l (x)

else h (p (x)) endif

Definition: b (x) = if empty (x) then e

elseif empty (p (x)) then e else a (b (p (x)), l (x)) endif

; Bn is the iteration of B.  Same warnings as for Pn in
; th_stringadd.bm apply. Note however that for Pn we used a tail
; recursive (more efficient) def. whereas here we use a fully
; recursive def, less efficient, but usually easier to prove things
; about, since x is fixed in the recursion.  (Clearly, we got a
; little bit smarter in the many many months which separate the
; definition of Pn and Bn...)

Definition: bn (n, x) = if n ≃ 0 then x

else b (bn (n − 1, x)) endif

;;; Fundamental properties of the THEORY of STRINGS; all names
;;; prefixed w/ "STR".
;; NOT-EMPTY theorems, which clearly need to know about empty...:

Theorem: str-not-empty-a ¬ empty (a (x, u))

; the next 2 lemmas say almost the same thing, but both facts are
; helpful to BM

Theorem: str-not-e-i i (u, x) ≠ e

Theorem: str-not-empty-i ¬ empty (i (u, x))

;; key commutativity/distributivity properties of A/P/L with I:
; STR-A-I should never coexist with I as they will loop.

Theorem: str-a-i a (i (u, x), v) = i (u, a (x, v))

Event: Disable str-a-i.

; one additional lemma which is useful for running with I disabled
; is:

Theorem: str-i-e i (u, e) = a (e, u)

; The 2 theorems STR-P-I and STR-L-I can be written more
; "powerfully": however they trigger too "agressively" for my
; taste, and cause case disjunctions too early at times. So in
; general I keep the strong versions disabled.
; 2/4/89 note: that comment was written when the "2" versions
; where physically AFTER the weak versions. Now that they're
; before, we may be able to leave them enabled all the time, since
; BM will try the non-disjunctive rules first...

Theorem: str-p-i2 p (i (u, x)) = if empty (x) then e

else i (u, p (x)) endif

Event: Disable str-p-i2.

Theorem: str-l-i2 l (i (u, x)) = if empty (x) then u

else l (x) endif

Event: Disable str-l-i2.

; also, because of Fundamental Remark in THETA-PRF-35, need
; explicit bottom cases:

Theorem: str-p-i-e empty (x) → (p (i (u, x)) = e)

Theorem: str-p-i (¬ empty (x)) → (p (i (u, x)) = i (u, p (x)))

Theorem: str-l-i-e empty (x) → (l (i (u, x)) = u)

Theorem: str-l-i (¬ empty (x)) → (l (i (u, x)) = l (x))

;; properties (and assorted kludges) of LEN:
; STR-len0-empty helps, and the zero result is always re-obtainable
; as long as EMPTY and LEN are enabled.
; Note: we tried to also have the symmetric rule:
; (equal (equal 0 (len x)) (empty x))
; but 1: BM warned us it was useless, and 2: we tried it and it
; was useless.

Theorem: str-len0-empty (len (x) = 0) = empty (x)

; on rare occasions we may need the symmetric:
;(prove-lemma STR-empty-len0 (rewrite)
;(equal (empty x)
;       (equal (len x) 0))
;)
; but so far the only time we thought it might help (in PPLFadd,
; bypassing the impotent use of eq-len hyps by BM) it did not, so..
; STR-len-eq-empty is another symptom of us bad EQLEN handling...
; Also, it's only useful w/ LEN disabled, of course.

Theorem: str-len-eq-empty (len (x) = len (y)) → ((empty (y) = empty (x)) = t)

; this back-chaining helps on RARE occasions when you need think:
; "x can't be empty, we know its length is something (>0)", enable
; it then.
; Note that if you can disable len when you use it, it can help
; a lot...

Theorem: str-not-empty-len (0 < len (x)) → (¬ empty (x))

Event: Disable str-not-empty-len.

; STR-len-P is a hack for LEN in "backwards" contexts, loops
; w/ len, of course.

Theorem: str-len-p (0 < len (x)) → (len (p (x)) = (len (x) − 1))

Event: Disable str-len-p.

; This is also an "anti-definition" which is useful when we want to
; prevent LEN being around because of mindless case disjunctions...

Theorem: str-add1-len-p (¬ empty (x)) → ((1 + len (p (x))) = len (x))

Event: Disable str-add1-len-p.

; This should be used as last resort to force a case disjunction.
; Using it globally is like having L-I2 and P-I2 around: they
; trigger too agressively, preventing some bigger-formula thms to
; trigger, and failing.
; When used, LEN should be disabled, as they will loop together.

Theorem: str-add1-len-p2 (1 + len (p (x))) = if empty (x) then 1

else len (x) endif

Event: Disable str-add1-len-p2.

; Another hack which we may use instead of LEN is:
; Note however, that when testing on IC_times, it resulted to
; a passage to len0 to reduce to T instead of arithmetic, taking a
; lot more time, and different cases, but same total # cases.

Theorem: str-len-e empty (x) → (len (x) = 0)

Event: Disable str-len-e.

; This is yet another hack needed to run with LEN disabled. It's
; left on all the time because it won't trigger much.

Theorem: str-len-1 ((¬ empty (x)) ∧ empty (p (x))) → ((1 = len (x)) = t)

; STR-len-lessp-1-empty: general effect? doesn't hurt...

Theorem: str-len-lessp-1-empty (len (x) < 1) = empty (x)

Theorem: str-len-i len (i (u, x)) = (1 + len (x))

Theorem: str-len-p-i len (p (i (u, x))) = len (x)

Theorem: str-len-i-p (¬ empty (x)) → (len (i (u, p (x))) = len (x))

; STR-equal-len-P actually DOES help during IC-S-Plus.  It may hurt
; under other circumstances, so beware... Note also that the rule
; has to be written with the extra " equal ... t" so as not to be
; confused with an attempt to rewrite "len P x" .

Theorem: str-equal-len-p (len (x) = len (y)) → ((len (p (x)) = len (p (y))) = t)

;; Basic Properties of H/B , essentially what we would have gotten
;; in a shell.

Theorem: str-b-decreases (¬ empty (x)) → (count (b (x)) < count (x))

; The reverse of the following theorem would make a fine H/B ELIM
; thm if we ever need it.

Theorem: str-i-h-b (¬ empty (x)) → (i (h (x), b (x)) = x)

Theorem: str-h-i h (i (u, x)) = u

; STR-B-I should be changed to return: if (empty x) (e) x .
; Note: we could also use SFIX here, but we'd have to
; leave it enabled all the time, which so far we have avoided.

Theorem: str-b-i b (i (u, x)) = if stringp (x) then x

else e endif

; STR-Empty-B is useful because it eliminates a B, and links case
; disjunctions.

Theorem: str-empty-b empty (b (x)) = empty (p (x))

; STR-P-B is our usual P pushthrough

Theorem: str-p-b p (b (x)) = b (p (x))

; STR-L-B doesn't require induction, but it's sometimes useful..

Theorem: str-l-b (¬ empty (b (x))) → (l (b (x)) = l (x))

; STR-Bn-1 for some weird reason, BM doesn't get that by itself...

Theorem: str-bn-1 bn (1, x) = b (x)

; STR-Bn-E: if we used fix, we would have the more general:
;           if (empty x) ...

Theorem: str-bn-e bn (n, e) = e

Theorem: str-p-bn p (bn (n, x)) = bn (n, p (x))

; STR-B-Bn-I may not be in its most general form, and we pay for
; the fact that for n=0 we use "x" instead of sfix x:

Theorem: str-b-bn-i stringp (x) → (b (bn (n, i (u, x))) = bn (n, x))

;; properties of H/B w/ Len, probably should be copied largely
;; from above properties of L/P w/ Len.
; We have the weak version below, but it didn't trigger in
; len-Stut-R since we don't have a condition on empty(Stut-R x y).
; Keeping this one higher should have the right effect of only
; introducing the case disjunction when needed; it may also do it
; too much...

Theorem: str-len-b2 len (b (x)) = if empty (x) then 0

else len (x) − 1 endif

Theorem: str-len-b (¬ empty (x)) → (len (b (x)) = (len (x) − 1))

; STR-len-Bn needs ARIthmetic properties... and is the first such
; property which caused ARIthmetic to be loaded before string
; theory.

Theorem: str-len-bn len (bn (n, x)) = (len (x) − n)

; STR-Bn-empty not necessarily phrased in the most universally
; useful way..  Probably should be able to disable Bn here...

Theorem: str-bn-empty empty (bn (n, x)) = (len (x) < (1 + n))

; STR-L-Bn needs STR-Bn-Empty, hence its position here.

Theorem: str-l-bn (¬ empty (bn (n, x))) → (l (bn (n, x)) = l (x))

;;; END OF FUNDAMENTAL PROPERTIES.
;; at this point I is completely characterized, and since BM
;; rewrites formulas inside-out, its definition goes against our
;; normalization, hence:

Event: Disable i.

Event: Enable str-a-i.

;; and ditto, in general, for H and B:

Event: Disable h.

Event: Disable b.

; at this point we should rarely have to use LEN's definition
; anymore:

Event: Disable len.

; ??? Maybe we should enable: (enable STR-add1-len-P) here
; SFIX is the "type fixer" for BM.  We don't really use it much,
;      the only place is in SYSD definitions for the (uninteresting
;      case) when the line variable is none defined, and we could
;      use S-Id instead, but I think it would give it too much
;      meaning.
; old: (defn sfix (x) (if (stringp x) x (e)))
; new: proved equivalent to old, and computationally no worse, and
;      better suited to running with empty disabled:

Definition: sfix (x) = if empty (x) then e

else x endif

; BM doesn't figure that out right away for new def, so...

Theorem: sfix-stringp stringp (sfix (x))

; We prove the key A2 properties for sfix, just like a
; combinational, so they don't become an issue in A2-SYSD proofs..

Theorem: a2-e-sfix (sfix (x) = e) = empty (x)

Theorem: a2-empty-sfix empty (sfix (x)) = empty (x)

Theorem: a2-lp-sfix len (sfix (x)) = len (x)

Theorem: a2-lpe-sfix eqlen (sfix (x), x)

Theorem: a2-ic-sfix sfix (i (c x, x)) = i (c x, sfix (x))

Theorem: a2-lc-sfix (¬ empty (x)) → (l (sfix (x)) = l (x))

; HISTORICAL NOTE: the fact that we need EMPTY for A2-PC-Sfix is
; what held us back so long in A2-PC-Sysds, forcing us to allow
; EMPTY there, increasing entropy beyond belief...

Theorem: a2-pc-sfix p (sfix (x)) = sfix (p (x))

Theorem: a2-hc-sfix (¬ empty (x)) → (h (sfix (x)) = h (x))

Theorem: a2-bc-sfix b (sfix (x)) = sfix (b (x))

Theorem: a2-bnc-sfix bn (n, sfix (x)) = sfix (bn (n, x))

; for all thinkable purposes, sfix is sufficiently characterized:

Event: Disable sfix.

; eof: th_stringadd.bm

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; TH_STRSPEC.BM: additional string theory with string things
;;;     needed in SPECIFICATIONS, as opposed to just sysd
;;;     definitions.  This could just have been appended to
;;;     th_stringadd.bm, but it doesn't feel right, and has some
;;;     automatically generated pieces, so it didn't look as
;;;     "bottom" as Stringadd.
;;;
;;; Functions: S-IF, S-AND, S-OR, S-NOT, S-EQUAL, S-CONST, S-CONSTL
;;; Predicate: S-BOOLP
;;; Miscellaneous boolean identities extended to the S versions.
;;;
;;; Induction scheme induct-P,P2,P3,P4.
;;;
;;; BEWARE (when updating with new versions of Sugar for
;;; combinationals): Most A2's are automatically generated by
;;; Sugar, EXCEPT where expressely noted in the comments, in
;;; particular for: AND, OR, CONSTL .
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; S-IF is just the STAR of the logical If-Then-Else.  Paillet uses
;; it a lot.
;; The code below is Sugar generated by: (bmcomb 'if '() '(x y z))

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

else a (s-if (p (x), p (y), p (z)), if l (x) then l (y) else l (z) endif) endif

;; A2-Begin-S-IF

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

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

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

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

Theorem: a2-ic-s-if ((len (x) = len (y)) ∧ (len (y) = len (z))) → (s-if (i (c x, x), i (c y, y), i (c z, z))

= i (if c x then c y else c z endif, s-if (x, y, z)))

Theorem: a2-lc-s-if (¬ empty (x)) → (l (s-if (x, y, z))

= if l (x) then l (y) else l (z) endif)

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

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

= if h (x) then h (y) else h (z) endif)

Theorem: a2-bc-s-if ((len (x) = len (y)) ∧ (len (y) = len (z))) → (b (s-if (x, y, z)) = s-if (b (x), b (y), b (z)))

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

;; A2-End-S-IF

;; S-AND is just the STAR of the logical AND, put in because of

;; Paillet.
;; The code below is Sugar generated by: (bmcomb 'AND '() '(x y))
;; Note: we reenable AND by hand everywhere sugar disables it,
;; because it's necessary at least for IC and LC.

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

else a (s-and (p (x), p (y)), l (x) ∧ l (y)) endif

;; A2-Begin-S-AND

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-AND

;; S-OR is just the STAR of the logical OR, put in because of
;; Paillet.
;; The code below is Sugar generated by: (bmcomb 'OR '() '(x y))
;; Note: just like for AND we reenable OR by hand everywhere
;; because it's necessary at least for IC and LC.

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

else a (s-or (p (x), p (y)), l (x) ∨ l (y)) endif

;; A2-Begin-S-OR

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-OR

;; S-NOT is just the STAR of the logical NOT, put in because of
;; Paillet, but useful in tons of other places!
;; The code below is Sugar generated by: (bmcomb 'NOT '() '(x))

Definition: s-not (x) = if empty (x) then e

else a (s-not (p (x)), ¬ l (x)) endif

;; A2-Begin-S-NOT

Theorem: a2-empty-s-not empty (s-not (x)) = empty (x)

Theorem: a2-e-s-not (s-not (x) = e) = empty (x)

Theorem: a2-lp-s-not len (s-not (x)) = len (x)

Theorem: a2-lpe-s-not eqlen (s-not (x), x)

Theorem: a2-ic-s-not s-not (i (c x, x)) = i (¬ c x, s-not (x))

Theorem: a2-lc-s-not (¬ empty (x)) → (l (s-not (x)) = (¬ l (x)))

Theorem: a2-pc-s-not p (s-not (x)) = s-not (p (x))

Theorem: a2-hc-s-not (¬ empty (x)) → (h (s-not (x)) = (¬ h (x)))

Theorem: a2-bc-s-not b (s-not (x)) = s-not (b (x))

Theorem: a2-bnc-s-not bn (n, s-not (x)) = s-not (bn (n, x))

;; A2-End-S-NOT

;; S-EQUAL is just the STAR of the logical Equal.  Paillet uses it
;; a lot.
;; The code below is Sugar generated by: (bmcomb 'equal '() '(x y))

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

else a (s-equal (p (x), p (y)), l (x) = l (y)) endif

;; A2-Begin-S-EQUAL

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

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

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

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

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

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

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

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

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

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

;; A2-End-S-EQUAL

;; S-CONST: CONSTANT combinational element, takes VALue as
;;   parameter.  Even though in most circuits this will be 0 or 1,
;;   it makes no sense to hardwire it for BM.

Definition: const (val, u) = val

;we require at least one string argument (MLP sfuns)
; Everything until A2-End-S-CONST Sugar generated by:
;   (bmcomb 'const '(val) '(x))

Definition: s-const (val, x) = if empty (x) then e

else a (s-const (val, p (x)), const (val, l (x))) endif

;; A2-Begin-S-CONST

Theorem: a2-empty-s-const empty (s-const (val, x)) = empty (x)

Theorem: a2-e-s-const (s-const (val, x) = e) = empty (x)

Theorem: a2-lp-s-const len (s-const (val, x)) = len (x)

Theorem: a2-lpe-s-const eqlen (s-const (val, x), x)

Theorem: a2-ic-s-const s-const (val, i (c x, x)) = i (const (val, c x), s-const (val, x))

Theorem: a2-lc-s-const (¬ empty (x)) → (l (s-const (val, x)) = const (val, l (x)))

Theorem: a2-pc-s-const p (s-const (val, x)) = s-const (val, p (x))

Theorem: a2-hc-s-const (¬ empty (x)) → (h (s-const (val, x)) = const (val, h (x)))

Theorem: a2-bc-s-const b (s-const (val, x)) = s-const (val, b (x))

Theorem: a2-bnc-s-const bn (n, s-const (val, x)) = s-const (val, bn (n, x))

;; A2-End-S-CONST
; Additional lemmas which give the key properties of S-CONST:

Theorem: l-sconst (¬ empty (x)) → (l (s-const (val, x)) = val)

; Note that I-SConst remotely descends from the insadd experiment
; and the solution that David Goldschlag gave me to that problem
; then..

Theorem: i-sconst (¬ empty (x)) → (i (val, s-const (val, p (x))) = s-const (val, x))

;; S-CONSTL is like S-Const, except that the length is given
;; numerically, and so the definition does NOT follow the standard
;; S- def.  A2's are therefore generated by hand.

Definition: s-constl (val, n) = if n ≃ 0 then e

else a (s-constl (val, n − 1), val) endif

; we need to prove the fundamental sequentiality properties of
; S-Const, which are significantly DIFFERENT from the standard,
; although I've kept the names since they FUNCTION identically.

Theorem: a2-e-s-constl (s-constl (val, n) = e) = (n ≃ 0)

Theorem: a2-empty-s-constl empty (s-constl (val, n)) = (n ≃ 0)

Theorem: a2-lp-s-constl len (s-constl (val, n)) = fix (n)

; no LPE of course

Theorem: a2-lc-s-constl (n ≄ 0) → (l (s-constl (val, n)) = val)

Theorem: a2-pc-s-constl p (s-constl (val, n)) = s-constl (val, n − 1)

Theorem: a2-hc-s-constl (n ≄ 0) → (h (s-constl (val, n)) = val)

Theorem: a2-bc-s-constl b (s-constl (val, n)) = s-constl (val, n − 1)

; A2-BNC-S-ConstL is a bit deep...  We haven't needed it anywhere,
; but we prove it just to show off!  Yeeeahh!

Theorem: a2-bnc-s-constl bn (n, s-constl (val, m)) = s-constl (val, m − n)

; Back in multadd.bm (Paillet#7) we noticed that S-ConstL was quite
; virulent and counter-productive, i.e. failed proofs expensively,
; so:

Event: Disable s-constl.

;; BOOLP:
; Note: we experimented w/ Hunt's def: (or (truep u) (falsep u))
; and it doesn't seem to make any difference whatsoever, so we
; stick with ours.

Definition: boolp (u) = ((u = t) ∨ (u = f))

Definition: s-boolp (x) = if empty (x) then x = e

else boolp (l (x)) ∧ s-boolp (p (x)) endif

; Sometime we just want this weaker fact around, and disabling
; S-boolp saves big.
; Note that S-boolp-P is true even without the hypothesis:
; (not (empty x)). The question is whether we want it to be applied
; in cases when that hyp. is not known...

Theorem: s-boolp-p ((¬ empty (x)) ∧ s-boolp (x)) → s-boolp (p (x))

Event: Disable s-boolp-p.

;;; MISCELLANEOUS BOOLEAN IDENTITIES extended to S versions:

Theorem: s-and-x-x s-boolp (x) → (s-and (x, x) = x)

Theorem: s-or-not-x-x s-boolp (x) → (s-or (s-not (x), x) = s-const (t, x))

Theorem: s-and-x-t s-boolp (x) → (s-and (x, s-const (t, x)) = x)

;;; INDUCTION SCHEMES which correspond to our SYSD definitions and
;;; theory:

Definition: induct-p (x1 ) = if empty (x1 ) then t

else induct-p (p (x1 )) endif

Definition: induct-p2 (x1 , x2 ) = if empty (x1 ) then t

else induct-p2 (p (x1 ), p (x2 )) endif

Definition: induct-p3 (x1 , x2 , x3 ) = if empty (x1 ) then t

else induct-p3 (p (x1 ), p (x2 ), p (x3 )) endif

Definition: induct-p4 (x1 , x2 , x3 , x4 ) = if empty (x1 ) then t

else induct-p4 (p (x1 ), p (x2 ), p (x3 ), p (x4 )) endif

; eof: th_strspec.bm

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  TH_TYPES.BM
;;;
;;; This file contains TYPE defns & lemmas for Boyer-Moore, to deal
;;; with standard hardware coding of booleans, numbers, and others.
;;; as well of course as their star extensions.
;;;
;;; Type: NUMERIC BITS
;;;   bitp: predicate.
;;;   bibo: translator: bit to bool (positive logic)
;;;   bobi: translator: bool to bit (positive logic)
;;; Note: experimentation (bcdS, bcdSbi) has revealed that this is
;;;   a BAD way to represent bits.  Booleans are much better.  In
;;;   an industrial setting, this type could disappear.
;;;

Definition: bitp (u) = ((u = 0) ∨ (u = 1))

Definition: s-bitp (x) = if empty (x) then x = e

else bitp (l (x)) ∧ s-bitp (p (x)) endif

;; BIBO:

Definition: bibo (bi) = if bi = 0 then f

else t endif

; star extension generated by: (bmcomb 'bibo '() '(bi))

Definition: s-bibo (bi) = if empty (bi) then e

else a (s-bibo (p (bi)), bibo (l (bi))) endif

;; A2-Begin-S-BIBO

Theorem: a2-empty-s-bibo empty (s-bibo (bi)) = empty (bi)

Theorem: a2-e-s-bibo (s-bibo (bi) = e) = empty (bi)

Theorem: a2-lp-s-bibo len (s-bibo (bi)) = len (bi)

Theorem: a2-lpe-s-bibo eqlen (s-bibo (bi), bi)

Theorem: a2-ic-s-bibo s-bibo (i (c bi, bi)) = i (bibo (c bi), s-bibo (bi))

Theorem: a2-lc-s-bibo (¬ empty (bi)) → (l (s-bibo (bi)) = bibo (l (bi)))

Theorem: a2-pc-s-bibo p (s-bibo (bi)) = s-bibo (p (bi))

;; A2-End-S-BIBO
;; BOBI:

Definition: bobi (bo) = if bo then 1

else 0 endif

; star extension generated by: (bmcomb 'bobi '() '(bo))

Definition: s-bobi (bo) = if empty (bo) then e

else a (s-bobi (p (bo)), bobi (l (bo))) endif

;; A2-Begin-S-BOBI

Theorem: a2-empty-s-bobi empty (s-bobi (bo)) = empty (bo)

Theorem: a2-e-s-bobi (s-bobi (bo) = e) = empty (bo)

Theorem: a2-lp-s-bobi len (s-bobi (bo)) = len (bo)

Theorem: a2-lpe-s-bobi eqlen (s-bobi (bo), bo)

Theorem: a2-ic-s-bobi s-bobi (i (c bo, bo)) = i (bobi (c bo), s-bobi (bo))

Theorem: a2-lc-s-bobi (¬ empty (bo)) → (l (s-bobi (bo)) = bobi (l (bo)))

Theorem: a2-pc-s-bobi p (s-bobi (bo)) = s-bobi (p (bo))

;; A2-End-S-BOBI
;;; eof: th_types.bm

Event: Make the library "mlp" and compile it.

Index

a, 6, 8, 9, 17, 19–24, 27, 28 a2-bc-s-and, 19 a2-bc-s-const, 24 a2-bc-s-constl, 25 a2-bc-s-equal, 22 a2-bc-s-if, 18 a2-bc-s-not, 21 a2-bc-s-or, 20 a2-bc-sfix, 16 a2-bnc-s-and, 19 a2-bnc-s-const, 24 a2-bnc-s-constl, 25 a2-bnc-s-equal, 23 a2-bnc-s-if, 18 a2-bnc-s-not, 22 a2-bnc-s-or, 21 a2-bnc-sfix, 16 a2-e-s-and, 19 a2-e-s-bibo, 28 a2-e-s-bobi, 28 a2-e-s-const, 23 a2-e-s-constl, 24 a2-e-s-equal, 22 a2-e-s-if, 18 a2-e-s-not, 21 a2-e-s-or, 20 a2-e-sfix, 16 a2-empty-s-and, 19 a2-empty-s-bibo, 28 a2-empty-s-bobi, 28 a2-empty-s-const, 23 a2-empty-s-constl, 24 a2-empty-s-equal, 22 a2-empty-s-if, 18 a2-empty-s-not, 21 a2-empty-s-or, 20 a2-empty-sfix, 16 a2-hc-s-and, 19 a2-hc-s-const, 24 a2-hc-s-constl, 25 a2-hc-s-equal, 22 a2-hc-s-if, 18 a2-hc-s-not, 21 a2-hc-s-or, 20 a2-hc-sfix, 16 a2-ic-s-and, 19 a2-ic-s-bibo, 28 a2-ic-s-bobi, 29 a2-ic-s-const, 23 a2-ic-s-equal, 22 a2-ic-s-if, 18 a2-ic-s-not, 21 a2-ic-s-or, 20 a2-ic-sfix, 16 a2-lc-s-and, 19 a2-lc-s-bibo, 28 a2-lc-s-bobi, 29 a2-lc-s-const, 23 a2-lc-s-constl, 25 a2-lc-s-equal, 22 a2-lc-s-if, 18 a2-lc-s-not, 21 a2-lc-s-or, 20 a2-lc-sfix, 16 a2-lp-s-and, 19 a2-lp-s-bibo, 28 a2-lp-s-bobi, 29 a2-lp-s-const, 23 a2-lp-s-constl, 25 a2-lp-s-equal, 22 a2-lp-s-if, 18 a2-lp-s-not, 21 a2-lp-s-or, 20 a2-lp-sfix, 16 a2-lpe-s-and, 19 a2-lpe-s-bibo, 28 a2-lpe-s-bobi, 29 a2-lpe-s-const, 23 a2-lpe-s-equal, 22 a2-lpe-s-if, 18 a2-lpe-s-not, 21 a2-lpe-s-or, 20 a2-lpe-sfix, 16 a2-pc-s-and, 19 a2-pc-s-bibo, 28 a2-pc-s-bobi, 29 a2-pc-s-const, 23 a2-pc-s-constl, 25 a2-pc-s-equal, 22 a2-pc-s-if, 18 a2-pc-s-not, 21 a2-pc-s-or, 20 a2-pc-sfix, 16 ari-add1-induct, 2 ari-diff-0, 4 ari-diff-add1, 4 ari-diff-less-0, 4 ari-diff-not-0, 4 ari-diff-x-x-0, 4 ari-lessp-diff, 4 ari-lessp-plus, 4 ari-lessp-remainder, 5 ari-lessp-sub1, 3 ari-lessp-times, 4 ari-lessp-times2, 4 ari-plus-0-ident-l, 2 ari-plus-0-ident-l2, 2 ari-plus-0-ident-r, 2 ari-plus-0-ident-r2, 2 ari-remainder-add1, 5 ari-times-0-cancel-l, 2 ari-times-0-cancel-l2, 3 ari-times-0-cancel-r, 2 ari-times-0-cancel-r2, 3 ari-times-0-equal, 3 ari-times-1-ident, 3 ari-times-add1, 3 ari-times-commute, 3 ari-times-diff-distribute, 4 ari-times-plus-distribute, 3

b, 8, 13, 14, 16, 18–22, 24, 25 bibo, 27, 28 bitp, 27 bn, 8, 13–16, 18, 19, 21–25 bobi, 28, 29 boolp, 25

const, 23, 24

e, 6, 8–10, 13–25, 27, 28

empty, 6–29

eqlen, 7, 8, 16, 18–23, 28, 29

eqlen-empty, 8 eqlen-is-equal-len, 7

h, 8, 13, 16, 18–22, 24, 25

i, 8–10, 12–14, 16, 18–24, 28, 29 i-sconst, 24 induct-p, 26 induct-p2, 26 induct-p3, 26 induct-p4, 26

l, 8, 10, 13, 15–25, 27–29

l-sconst, 24

len, 7, 10–12, 14, 16, 18–23, 25, 28, 29

p, 6–14, 16–29

pn, 6

s-and, 19, 26 s-and-x-t, 26 s-and-x-x, 26 s-bibo, 27, 28 s-bitp, 27 s-bobi, 28, 29 s-boolp, 25, 26 s-boolp-p, 26 s-const, 23, 24, 26 s-constl, 24, 25 s-equal, 22, 23 s-if, 17, 18 s-not, 21, 22, 26 s-or, 20, 21, 26 s-or-not-x-x, 26 sfix, 15, 16 sfix-stringp, 16 str-a-i, 9 str-add1-len-p, 11 str-add1-len-p2, 11 str-b-bn-i, 14 str-b-decreases, 13 str-b-i, 13 str-bn-1, 13 str-bn-e, 14 str-bn-empty, 14 str-empty-b, 13 str-empty-count, 7 str-empty-p, 6 str-equal-len-p, 12 str-h-i, 13 str-i-e, 9 str-i-h-b, 13 str-l-b, 13 str-l-bn, 15 str-l-i, 10 str-l-i-e, 10 str-l-i2, 10 str-len-1, 12 str-len-b, 14 str-len-b2, 14 str-len-bn, 14 str-len-e, 12 str-len-eq-empty, 11 str-len-i, 12 str-len-i-p, 12 str-len-lessp-1-empty, 12 str-len-p, 11 str-len-p-i, 12 str-len0-empty, 10 str-not-e-i, 9 str-not-empty-a, 9 str-not-empty-i, 9 str-not-empty-len, 11 str-p-b, 13 str-p-bn, 14 str-p-i, 10 str-p-i-e, 10 str-p-i2, 9 stringp, 6, 13, 14, 16