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
|
; Arithmetic-5 Library
; Written by Robert Krug
; Copyright/License:
; See the LICENSE file at the top level of the arithmetic-5 library.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; if-normalization.lisp
;;;
;;; We have found it useful to normalize if expressions involving
;;; arithmetic operators.
;;;
;;; I probably shouldn't be calling this normalization, since all we
;;; are really doing is lifting if expressions over certain arithmetic
;;; expressions. Perhaps in some future cleanup I will rename this
;;; file.
;;;
;;; Note: Some documentation on just how this is useful would be nice.
;;; Where (when) do if expressions get introduced? Why does this
;;; lifting help? What fails if this is disabled?
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(include-book "building-blocks")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defthm |(+ (if a b c) x)|
(implies (syntaxp (ok-to-lift-p a))
(equal (+ (if a b c) x)
(if a (+ b x) (+ c x)))))
(defthm |(+ x (if a b c))|
(implies (syntaxp (ok-to-lift-p a))
(equal (+ x (if a b c))
(if a (+ x b) (+ x c)))))
(defthm |(- (if a b c))|
(implies (syntaxp (ok-to-lift-p a))
(equal (- (if a b c))
(if a (- b) (- c)))))
(defthm |(* (if a b c) x)|
(implies (syntaxp (ok-to-lift-p a))
(equal (* (if a b c) x)
(if a (* b x) (* c x)))))
(defthm |(* x (if a b c))|
(implies (syntaxp (ok-to-lift-p a))
(equal (* x (if a b c))
(if a (* x b) (* x c)))))
(defthm |(/ (if a b c))|
(implies (syntaxp (ok-to-lift-p a))
(equal (/ (if a b c))
(if a (/ b) (/ c)))))
(defthm |(expt (if a b c) x)|
(implies (syntaxp (ok-to-lift-p a))
(equal (expt (if a b c) x)
(if a (expt b x) (expt c x)))))
(defthm |(expt x (if a b c))|
(implies (syntaxp (ok-to-lift-p a))
(equal (expt x (if a b c))
(if a (expt x b) (expt x c)))))
(defthm |(equal x (if a b c))|
(implies (syntaxp (ok-to-lift-p a))
(equal (equal x (if a b c))
(if a (equal x b) (equal x c)))))
(defthm |(equal (if a b c) x)|
(implies (syntaxp (ok-to-lift-p a))
(equal (equal (if a b c) x)
(if a (equal b x) (equal c x)))))
(defthm |(< x (if a b c))|
(implies (syntaxp (ok-to-lift-p a))
(equal (< x (if a b c))
(if a (< x b) (< x c)))))
(defthm |(< (if a b c) x)|
(implies (syntaxp (ok-to-lift-p a))
(equal (< (if a b c) x)
(if a (< b x) (< c x)))))
|
