← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/defexec/other-apps/qsort/final-theorem.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/defexec/other-apps/qsort/final-theorem.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
#|
 
4
 
 
5
  final-theorem.lisp
 
6
  ~~~~~~~~~~~~~~~~~~
 
7
 
 
8
We prove the final theorem about qsort here. After all that I had to do, this
 
9
should go like a breeze, except (maybe) for the hiccup when (length x) is equal
 
10
to 0. But this is not a big deal.
 
11
 
 
12
We mark the final theorem by a capital DEFTHM for easy look-up.
 
13
 
 
14
|#
 
15
 
 
16
(include-book "sort-qs-properties")
 
17
 
 
18
(local
 
19
(include-book "load-extract")
 
20
)
 
21
 
 
22
(local
 
23
(in-theory (disable alloc-qs load-qs))
 
24
)
 
25
 
 
26
(local
 
27
(in-theory (enable in-situ-equal-intermediate
 
28
                   intermediate-in-situ-qsort-equal-qsort))
 
29
)
 
30
 
 
31
(local
 
32
(defthm arith-001
 
33
  (implies (and (not (natp (1- l)))
 
34
                (natp l))
 
35
           (equal l 0))
 
36
  :rule-classes :forward-chaining)
 
37
)
 
38
 
 
39
(local
 
40
(defthm len-0-implies-not-consp
 
41
  (implies (equal (len x) 0)
 
42
           (not (consp x)))
 
43
  :hints (("Goal"
 
44
           :in-theory (enable len)))
 
45
  :rule-classes :forward-chaining)
 
46
)
 
47
 
 
48
(DEFTHM qsort-is-correct
 
49
  (implies (true-listp x)
 
50
           (equal (qsort x)
 
51
                  (isort x)))
 
52
  :hints (("Goal"
 
53
           :in-theory (disable natp-posp--1) ; needed for v2-8
 
54
           :cases ((not (natp (1- (len x))))))))
 
55
 
 
56
;; Finally, we add an mbe version of sort which is isort in the logic and is
 
57
;; qsort in under-the-hood execution.  This work is new, i.e., not included
 
58
;; in the 2002 ACL2 workshop supporting materials.
 
59
 
 
60
(defun sort-list (x)
 
61
  (declare (xargs :guard (true-listp x)))
 
62
  (mbe :logic (isort x) :exec (qsort x)))
 
63
 
 
64
(defthm sort-list-is-correct
 
65
  (and (ordp (sort-list x))
 
66
       (perm (sort-list x) x)))
 
67
 
 
68
;; We now prove that sort-list is idempotent by proving the property about
 
69
;; isort.
 
70
 
 
71
(defthm <<=-implies-equal
 
72
  (implies (and (<<= x y) (not (<< x y)))
 
73
           (equal x y))
 
74
  :rule-classes :forward-chaining)
 
75
 
 
76
(defthm ordp-isort
 
77
  (ordp (isort x)))
 
78
 
 
79
(in-theory (enable isort insert))
 
80
 
 
81
(in-theory (disable qsort-fn-equivalent-isort))
 
82
 
 
83
(defthm true-listp-isort
 
84
  (true-listp (isort x)))
 
85
 
 
86
(defthm insert-equals-cons
 
87
  (implies (and (ordp x) (<<= e (car x)) (true-listp x))
 
88
           (equal (insert e x) (cons e x))))
 
89
 
 
90
(defthm isort-idempotent-1
 
91
  (implies (and (ordp x) (true-listp x))
 
92
           (equal (isort x) x)))
 
93
 
 
94
(defthm isort-idempotent
 
95
  (equal (isort (isort x)) (isort x)))
 
96
 
 
97
(defthm sort-list-idempotent
 
98
  (equal (sort-list (sort-list x)) (sort-list x)))