← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/mu-calculus/book/fixpoints.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/mu-calculus/book/fixpoints.lisp
 
1
(in-package "SETS")
 
2
(include-book "sets")
 
3
 
 
4
(encapsulate 
 
5
 ((f (X) t)
 
6
  (S () t))
 
7
 
 
8
 (local (defun f (X)
 
9
          (declare (ignore X))
 
10
          nil))
 
11
 
 
12
 (local (defun S ()
 
13
          nil))
 
14
 
 
15
 (defthm f-is-monotonic
 
16
   (implies (=< X Y)
 
17
            (=< (f X) (f Y))))
 
18
 
 
19
 (defthm S-is-top
 
20
   (=< (f X) (set-union X (S)))))
 
21
 
 
22
; applyf is constrained, so we don't care about its guards.
 
23
(defun applyf (X n)
 
24
  (declare (xargs :measure (nfix n)))
 
25
  (if (zp n)
 
26
      X
 
27
    (if (== X (f X))
 
28
        X
 
29
      (applyf (f X) (1- n)))))
 
30
 
 
31
(defabbrev lfpf ()
 
32
  (applyf nil (cardinality (S))))
 
33
 
 
34
(defabbrev gfpf ()
 
35
  (applyf (S) (cardinality (S))))