; 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)