blob: 20787a411338fb2f2a69b4cce5c86fe22a95952c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
(in-package "ACL2")
(include-book "remove-nth")
(include-book "perm")
(include-book "std/util/bstar" :dir :system)
(local (include-book "system/random" :dir :system))
(local (include-book "tools/mv-nth" :dir :system))
(local (include-book "std/lists/len" :dir :system))
(defun shuffle (x state)
(declare (xargs :stobjs state
:measure (len x)
:guard (true-listp x)))
(if (endp x)
(mv nil state)
(b* (((mv i state) (random$ (len x) state))
((mv result state) (shuffle (remove-nth i x) state)))
(mv (cons (nth i x) result) state))))
(local
(defthm nth-member
(implies (and (consp x)
(equal (nth i x) e)
(< i (len x)))
(member-equal e x))
:rule-classes ((:rewrite :match-free :all)
(:forward-chaining :match-free :all))))
(local
(defthm remove-nth-remove1
(implies (and (consp x)
(< i (len x)))
(perm (remove-nth i x)
(remove1 (nth i x) (double-rewrite x))))
:hints (("Goal" :induct (remove-nth i x))
("Subgoal *1/3.8'"
:cases ((consp (cdr x)))))))
(local
(defthm member-nth
(implies (and (consp x)
(< i (len x)))
(member (nth i x) x))))
(defthm perm-shuffle
(perm (mv-nth 0 (shuffle x state)) (double-rewrite x)))
|
