blob: 1ba5653439ebd8b4ff4fd7527cc6980854f07fc0 (
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
; Copyright (C) 2001 Georgia Institute of Technology
; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; Written by: Panagiotis Manolios who can be reached as follows.
; Email: manolios@cc.gatech.edu
; Postal Mail:
; College of Computing
; CERCS Lab
; Georgia Institute of Technology
; 801 Atlantic Drive
; Atlanta, Georgia 30332-0280 U.S.A.
(in-package "ACL2")
(include-book "perm-order")
(defun insert (a x)
(if (consp x)
(if (<<= a (car x))
(cons a x)
(cons (car x) (insert a (cdr x))))
(list a)))
(defun isort (x)
(if (consp x)
(insert (car x) (isort (cdr x)))
nil))
(defthm ordered-insert
(implies (orderedp y)
(orderedp (insert x y))))
(defthm ordered-sort
(orderedp (isort x)))
(defthm perm-insert
(perm (insert x y) (cons x y)))
(defthm perm-sort
(perm (isort x) x))
(defthm insert-insert
(equal (insert x (insert y z))
(insert y (insert x z)))
:rule-classes ((:rewrite :loop-stopper ((x y)))))
(defthm insert-in
(equal (isort (insert x y))
(isort (cons x y))))
(defthm insert-sort-remove
(implies (in x y)
(equal (insert x (isort (remove-el x y)))
(isort y))))
(defthm sort-canonical
(implies (and (perm x y)
;; Added for mod to ACL2 v2-8 that does better matching for calls of
;; equivalence relations against the current context, to avoid a rewriter
;; loop in the proof of mail:
(syntaxp (not (term-order x y))))
(equal (isort x)
(isort y))))
(defthm main
(equal (perm x y)
(equal (isort x)
(isort y)))
:hints (("goal"
:use ((:instance perm-sort (x y))
(:instance perm-sort))
:in-theory (disable perm-sort)))
:rule-classes nil)
(defthm main2
(implies (and (orderedp x)
(perm x y))
(equal (isort y)
x))
:rule-classes nil)
(defthm main3
(implies (and (orderedp x)
(orderedp y)
(perm x y))
(equal x y))
:hints (("goal"
:use ((:instance main2) (:instance main2 (x y)))))
:rule-classes nil)
|
