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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
(in-package "ACL2")
; cert_param: (uses-acl2r)
; Added by Matt K. for v2-7.
(add-match-free-override :once t)
(set-match-free-default :once)
(encapsulate
;; Constrain the functions ifn, ifn-domain-p, and ifn-range-p
;; so that ifn is a 1-1 and onto function from ifn-domain-p to
;; ifn-range-p.
((ifn (x) t)
(ifn-domain-p (x) t)
(ifn-range-p (y) t)
;(ifn-is-onto-predicate-witness (y) t)
)
(local
(defun ifn (x) x))
(local
(defun ifn-domain-p (x)
(realp x)))
(local
(defun ifn-range-p (x)
(realp x)))
;; We restrict the domain and range to the reals.
(defthm ifn-domain-real
(implies (ifn-domain-p x)
(realp x)))
(defthm ifn-range-real
(implies (ifn-range-p x)
(realp x)))
;; The function maps the domain into the range.
(defthm ifn-domain-into-range
(implies (ifn-domain-p x)
(ifn-range-p (ifn x))))
;; The function ifn must be 1-1.
(defthm ifn-is-1-1
(implies (and (ifn-domain-p x1)
(ifn-domain-p x2)
(equal (ifn x1) (ifn x2)))
(equal x1 x2))
:rule-classes nil)
;; The function ifn is onto.
(defun-sk ifn-is-onto-predicate (y)
(exists (x)
(and (ifn-domain-p x)
(equal (ifn x) y))))
(defthm ifn-is-onto
(implies (ifn-range-p y)
(ifn-is-onto-predicate y))
:hints (("Goal"
:use ((:instance ifn-is-onto-predicate-suff (x y) (y y)))))
)
)
(defchoose ifn-inverse (x) (y)
(if (ifn-range-p y)
(and (ifn-domain-p x)
(equal (ifn x) y))
(realp x)))
(defthm ifn-inverse-exists
(implies (ifn-range-p y)
(and (ifn-domain-p (ifn-inverse y))
(equal (ifn (ifn-inverse y)) y)))
:hints (("Goal"
:use ((:instance ifn-inverse (x (ifn-is-onto-predicate-witness y)) (y y))
(:instance ifn-is-onto-predicate (y y))))))
(defthm ifn-inverse-is-real
(realp (ifn-inverse y))
:hints (("Goal"
:cases ((ifn-range-p y)))
("Subgoal 2"
:use ((:instance ifn-inverse
(x 0)
(y y)))))
:rule-classes (:rewrite :type-prescription)
)
(defthm ifn-inverse-unique
(implies (and (ifn-range-p y)
(ifn-domain-p x)
(equal (ifn x) y))
(equal (ifn-inverse y) x))
:hints (("Goal"
:use ((:instance ifn-inverse-exists (y y))
(:instance ifn-is-1-1 (x1 x) (x2 (ifn-inverse y)))
))))
(defthm ifn-inverse-inverse-exists
(implies (ifn-domain-p x)
(equal (ifn-inverse (ifn x)) x))
:hints (("Goal"
:use ((:instance ifn-inverse-unique
(x x)
(y (ifn x))))
:in-theory (disable ifn-inverse-unique))))
(defthm ifn-inverse-is-1-to-1
(implies (and (ifn-range-p y1)
(ifn-range-p y2)
(equal (ifn-inverse y1)
(ifn-inverse y2)))
(equal y1 y2))
:hints (("Goal"
:use ((:instance ifn-inverse-exists (y y1))
(:instance ifn-inverse-exists (y y2)))
:in-theory (disable ifn-inverse-exists)))
:rule-classes nil)
|
