← 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/split-qs-properties.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/split-qs-properties.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
#|
 
4
 
 
5
  split-qs-properties.lisp
 
6
  ~~~~~~~~~~~~~~~~~~~~~~~~
 
7
 
 
8
In this book we make clear the relation between split-qs and the functions walk
 
9
and merge-func we described earlier. These properties will allow us to reason
 
10
when we prove that sort-qs is equal to in-situ-qsort-fn using sort-qs as the
 
11
induction hint.
 
12
 
 
13
|#
 
14
 
 
15
(include-book "programs")
 
16
(include-book "merge-intermediate")
 
17
(include-book "extraction")
 
18
(include-book "arithmetic/top-with-meta" :dir :system)
 
19
 
 
20
(local
 
21
(in-theory (enable swap))
 
22
)
 
23
 
 
24
(local
 
25
(defthm arith-001
 
26
  (implies (and (not (natp (1- hi)))
 
27
                (natp hi))
 
28
           (equal hi 0))
 
29
  :rule-classes :forward-chaining)
 
30
)
 
31
 
 
32
 
 
33
(defthm walk-split-qs-equal
 
34
  (implies (and (natp lo)
 
35
                (natp hi))
 
36
           (equal (mv-nth 0 (split-qs lo hi splitter qs))
 
37
                  (+ lo (walk (extract-qs lo hi qs) splitter))))
 
38
  :hints (("Goal"
 
39
           :induct (split-qs lo hi splitter qs))))
 
40
        
 
41
 
 
42
 
 
43
(defthm split-qs-is-identity-for-below-range
 
44
  (implies (and (natp i)
 
45
                (natp lo)
 
46
                (natp hi)
 
47
                (< i lo))
 
48
           (equal (objsi i (mv-nth 1 (split-qs lo hi splitter qstor)))
 
49
                  (objsi i qstor))))
 
50
 
 
51
(defthm split-qs-is-identity-for-above-range
 
52
  (implies (and (natp i)
 
53
                (natp lo)
 
54
                (natp hi)
 
55
                (> i hi))
 
56
           (equal (objsi i (mv-nth 1 (split-qs lo hi splitter qstor)))
 
57
                  (objsi i qstor))))
 
58
 
 
59
(defthm merge-func-split-qs-equal
 
60
  (implies (and (natp lo)
 
61
                (natp hi))
 
62
           (equal (extract-qs lo hi (mv-nth 1 (split-qs lo hi splitter qs)))
 
63
                  (merge-func (extract-qs lo hi qs) splitter)))
 
64
  :hints (("Goal" 
 
65
           :induct (split-qs lo hi splitter qs))))
 
66
 
 
67
           
 
68
(in-theory (disable extract-qs-decrement-hi))
 
69
 
 
70
 
 
71
 
 
72
(in-theory (disable walk-split-qs-equal))
 
73