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