; To certify this book:
; (ld "defpkg.lisp")
; (certify-book "powerset-examples" 1)
(in-package "S")
(include-book "set-theory")
; Here is the definition of powerset.
(defmap scons-to-every (e s)
:for x :in s :map (scons e x))
(defun powerset (s)
(cond ((ur-elementp s) (brace nil))
(t (union (powerset (scdr s))
(scons-to-every (scar s)
(powerset (scdr s)))))))
; Powerset builds a set.
(defthm setp-powerset
(setp (powerset s)))
; In fact, it builds a set of sets. We have to define that concept
; and prove that it admits = as a congruence.
(defun set-of-setsp (p)
(if (ur-elementp p)
t
(and (setp (scar p))
(set-of-setsp (scdr p)))))
; Since set-of-setsp is a predicate, we use the canonicalize method.
(defx :strategy :congruence (set-of-setsp p) 1 :method :canonicalize)
; Powerset builds a set of sets.
(defthm set-of-setsp-powerset
(set-of-setsp (powerset b)))
; Here is the fundamental fact about membership in scons-to-every.
(defthm mem-scons-to-every
(implies (and (setp p)
(set-of-setsp p)
(setp s1))
(iff (mem s1 (scons-to-every e p))
(and (mem e s1)
(or (mem s1 p)
(mem (diff s1 (brace e)) p))))))
; The following function is used to tell ACL2 how to induct in the
; next theorem. It says: induct on b and assume two inductive hypotheses.
(defun induction-hint (a b)
(if (ur-elementp b)
(list a b)
(list (induction-hint a (scdr b)) ; hyp 1
(induction-hint (diff a (brace (scar b))) (scdr b))))) ; hyp 2
; The powerset contains precisely the subsets.
(defthm powerset-property
(implies (setp e)
(iff (mem e (powerset s))
(subsetp e s)))
:hints (("Goal" :induct (induction-hint e s))))
; The next lemma is needed for the final defx command.
(defthm subsetp-scons-to-every-powerset
(implies (and (set-of-setsp s)
(subsetp s (powerset b))
(mem e b))
(subsetp (scons-to-every e s)
(powerset b)))
:hints (("Goal" :induct (scons-to-every e s))))
; This command establishes that powerset admits = as a congruence.
(defx :strategy :congruence (powerset s) 1 :method :subsetp)