;; Requires sets.

Event: Start with the library "sets".

;; Alists, March 1990.  Most of the definitions and some of the lemmas
;; were contributed by Bill Bevier; the rest are by Matt Kaufmann.
;; Functions defined here:
;; (deftheory alist-defns
;;   (alistp domain range value bind rembind invert mapping
;;           restrict co-restrict))

Definition: alistp (x) = if listp (x) then listp (car (x)) ∧ alistp (cdr (x))

else x = nil endif

Theorem: alistp-implies-properp alistp (x) → properp (x)

Theorem: alistp-nlistp (x ≃ nil) → (alistp (x) = (x = nil))

Theorem: alistp-cons alistp (cons (a, x)) = (listp (a) ∧ alistp (x))

Event: Disable alistp.

Theorem: alistp-append alistp (append (x, y)) = (alistp (fix-properp (x)) ∧ alistp (y))

Definition: domain (map) = if listp (map)

then if listp (car (map)) then cons (car (car (map)), domain (cdr (map)))

else domain (cdr (map)) endif else nil endif

Theorem: properp-domain properp (domain (map))

Theorem: domain-append domain (append (x, y)) = append (domain (x), domain (y))

Theorem: domain-nlistp (map ≃ nil) → (domain (map) = nil)

Theorem: domain-cons domain (cons (a, map)) = if listp (a) then cons (car (a), domain (map))

else domain (map) endif

Theorem: member-domain-sufficiency (cons (a, x) ∈ y) → (a ∈ domain (y))

Theorem: subsetp-domain subsetp (x, y) → subsetp (domain (x), domain (y))

Event: Disable domain.

Definition: range (map) = if listp (map)

then if listp (car (map)) then cons (cdr (car (map)), range (cdr (map)))

else range (cdr (map)) endif else nil endif

Theorem: properp-range properp (range (map))

Theorem: range-append range (append (s1 , s2 )) = append (range (s1 ), range (s2 ))

Theorem: range-nlistp (map ≃ nil) → (range (map) = nil)

Theorem: range-cons range (cons (a, map)) = if listp (a) then cons (cdr (a), range (map))

else range (map) endif

Event: Disable range.

;; BOUNDP has been eliminated in favor of membership in domain.
;; Notice that I have to talk about things like disjointness of
;; domains anyhow.  New definition body would be (member x (domain map)).

;(defn boundp (x map)
;  (if (listp map)
;      (if (listp (car map))
;          (if (equal x (caar map))
;              t
;            (boundp x (cdr map)))
;        (boundp x (cdr map)))
;    f))

Definition: value (x, map) = if listp (map)

then if listp (car (map)) ∧ (x = caar (map)) then cdar (map)

else value (x, cdr (map)) endif else 0 endif

Theorem: value-nlistp (map ≃ nil) → (value (x, map) = 0)

Theorem: value-cons value (x, cons (pair, map)) = if listp (pair) ∧ (x = car (pair)) then cdr (pair)

else value (x, map) endif

Event: Disable value.

Definition: bind (x, v, map) = if listp (map)

then if listp (car (map))

then if x = caar (map) then cons (cons (x, v), cdr (map)) else cons (car (map), bind (x, v, cdr (map))) endif

else cons (car (map), bind (x, v, cdr (map))) endif else cons (cons (x, v), nil) endif

Definition: rembind (x, map) = if listp (map)

then if listp (car (map))

then if x = caar (map) then cdr (map)

else cons (car (map), rembind (x, cdr (map))) endif else cons (car (map), rembind (x, cdr (map))) endif

else nil endif Definition: invert (map) = if listp (map)

then if listp (car (map))

then cons (cons (cdr (car (map)), car (car (map))), invert (cdr (map))) else invert (cdr (map)) endif

else nil endif

Theorem: properp-invert properp (invert (map))

Theorem: invert-nlistp (map ≃ nil) → (invert (map) = nil)

Theorem: invert-cons invert (cons (pair, map)) = if listp (pair) then cons (cons (cdr (pair), car (pair)), invert (map))

else invert (map) endif

Theorem: value-invert-not-member-of-domain ((g ∈ range (sg)) ∧ disjoint (domain (s), domain (sg))) → (value (g, invert (sg)) ∉ domain (s))

Event: Disable invert.

Definition: mapping (map) = (alistp (map) ∧ setp (domain (map)))

;; For when we disable mapping:

Theorem: mapping-implies-alistp mapping (map) → alistp (map)

Theorem: mapping-implies-setp-domain mapping (map) → setp (domain (map))

Definition: restrict (s, new-domain) = if listp (s)

then if listp (car (s)) ∧ (caar (s) ∈ new-domain) then cons (car (s), restrict (cdr (s), new-domain)) else restrict (cdr (s), new-domain) endif

else nil endif

Definition: co-restrict (s, new-domain)

= if listp (s)

then if listp (car (s)) ∧ (caar (s) ∉ new-domain) then cons (car (s), co-restrict (cdr (s), new-domain)) else co-restrict (cdr (s), new-domain) endif

else nil endif

Event: Let us define the theory alist-defns to consist of the following events: alistp, domain, range, value, bind, rembind, invert, mapping, restrict, co-restrict.

;;;;; alist lemmas
; DOMAIN
;; The following was proved in the course of the final run through
;; the generalization proof.  The one after it isn't needed but
;; seems like it's worth proving too.  Actually now I see that
;; some other lemmas are now obsolete, so I'll put these both
;; early in the file and delete the others.

Theorem: domain-restrict domain (restrict (s, dom)) = intersection (domain (s), dom)

Theorem: domain-co-restrict domain (co-restrict (s, dom)) = set-diff (domain (s), dom)

Theorem: domain-bind domain (bind (x, v, map)) = if x ∈ domain (map) then domain (map)

else append (domain (map), list (x)) endif

Theorem: domain-rembind domain (rembind (x, map)) = delete (x, domain (map))

Theorem: domain-invert domain (invert (map)) = range (map)

; RANGE

Theorem: range-invert range (invert (map)) = domain (map)

; BOUNDP

Theorem: boundp-bind (x ∈ domain (bind (y, v, map))) = ((x = y) ∨ (x ∈ domain (map)))

Theorem: boundp-rembind mapping (map) → ((x ∈ domain (rembind (y, map)))

= if x = y then f else x ∈ domain (map) endif)

Theorem: boundp-subsetp (subsetp (map1 , map2 ) ∧ (name ∈ domain (map1 ))) → (name ∈ domain (map2 ))

Theorem: disjoint-domain-singleton (disjoint (domain (s), list (x)) = (x ∉ domain (s))) ∧ (disjoint (list (x), domain (s)) = (x ∉ domain (s)))

Theorem: boundp-value-invert (x ∈ range (map)) → (value (x, invert (map)) ∈ domain (map))

; VALUE

Theorem: value-when-not-bound (name ∉ domain (map)) → (value (name, map) = 0)

Theorem: value-bind value (x, bind (y, v, map)) = if x = y then v

else value (x, map) endif

Theorem: value-rembind mapping (map) → (value (x, rembind (y, map))

= if x = y then 0 else value (x, map) endif)

Theorem: value-append value (x, append (s1 , s2 )) = if x ∈ domain (s1 ) then value (x, s1 )

else value (x, s2 ) endif

Theorem: value-value-invert ((x ∈ range (s)) ∧ mapping (s)) → (value (value (x, invert (s)), s) = x)

; MAPPING

Theorem: mapping-append mapping (append (s1 , s2 )) = (disjoint (domain (s1 ), domain (s2 ))

∧ mapping (fix-properp (s1 )) ∧ mapping (s2 ))

Event: Disable mapping.

;; RESTRICT and CO-RESTRICT

Theorem: alistp-restrict alistp (restrict (s, r))

Theorem: alistp-co-restrict alistp (co-restrict (s, r))

Theorem: value-restrict ((a ∈ r) ∧ (a ∈ domain (s))) → (value (a, restrict (s, r)) = value (a, s))

Theorem: value-co-restrict ((a ∉ r) ∧ (a ∈ domain (s))) → (value (a, co-restrict (s, r)) = value (a, s))

Theorem: mapping-restrict mapping (s) → mapping (restrict (s, x))

Theorem: mapping-co-restrict mapping (s) → mapping (co-restrict (s, x))

Event: Disable restrict.

Event: Disable co-restrict.

Event: Make the library "alists".

Index

alist-defns, 5 alistp, 1, 4, 7 alistp-append, 1 alistp-co-restrict, 7 alistp-cons, 1 alistp-implies-properp, 1 alistp-nlistp, 1 alistp-restrict, 7

bind, 3, 5, 6 boundp-bind, 6 boundp-rembind, 6 boundp-subsetp, 6 boundp-value-invert, 6

co-restrict, 4, 5, 7

delete, 5 disjoint, 4, 6, 7 disjoint-domain-singleton, 6 domain, 1, 2, 4–7 domain-append, 2 domain-bind, 5 domain-co-restrict, 5 domain-cons, 2 domain-invert, 5 domain-nlistp, 2 domain-rembind, 5 domain-restrict, 5

fix-properp, 1, 7

intersection, 5 invert, 4–6 invert-cons, 4 invert-nlistp, 4

mapping, 4, 6, 7 mapping-append, 7 mapping-co-restrict, 7 mapping-implies-alistp, 4 mapping-implies-setp-domain, 4 mapping-restrict, 7 member-domain-sufficiency, 2

properp, 1, 2, 4 properp-domain, 1 properp-invert, 4 properp-range, 2

range, 2, 4–6 range-append, 2 range-cons, 2 range-invert, 5 range-nlistp, 2 rembind, 3, 5, 6 restrict, 4, 5, 7

set-diff, 5 setp, 4 subsetp, 2, 6 subsetp-domain, 2

value, 3, 4, 6, 7 value-append, 6 value-bind, 6 value-co-restrict, 7 value-cons, 3 value-invert-not-member-of-domai

n, 4 value-nlistp, 3 value-rembind, 6 value-restrict, 7 value-value-invert, 6 value-when-not-bound, 6