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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
(* Taken from Library/prime.ml *)
prioritize_num();;
(* ------------------------------------------------------------------------- *)
(* HOL88 compatibility (since all this is a port of old HOL88 stuff). *)
(* ------------------------------------------------------------------------- *)
let MULT_MONO_EQ = prove
(`!m i n. ((SUC n) * m = (SUC n) * i) <=> (m = i)`,
REWRITE_TAC[EQ_MULT_LCANCEL; NOT_SUC]);;
let LESS_ADD_1 = prove
(`!m n. n < m ==> (?p. m = n + (p + 1))`,
REWRITE_TAC[LT_EXISTS; ADD1; ADD_ASSOC]);;
let LESS_ADD_SUC = ARITH_RULE `!m n. m < (m + (SUC n))`;;
let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;;
let LESS_MONO_ADD = ARITH_RULE `!m n p. m < n ==> (m + p) < (n + p)`;;
let LESS_EQ_0 = prove
(`!n. n <= 0 <=> (n = 0)`,
REWRITE_TAC[LE]);;
let LESS_LESS_CASES = ARITH_RULE `!m n. (m = n) \/ m < n \/ n < m`;;
let LESS_ADD_NONZERO = ARITH_RULE `!m n. ~(n = 0) ==> m < (m + n)`;;
let NOT_EXP_0 = prove
(`!m n. ~((SUC n) EXP m = 0)`,
REWRITE_TAC[EXP_EQ_0; NOT_SUC]);;
let LESS_THM = ARITH_RULE `!m n. m < (SUC n) <=> (m = n) \/ m < n`;;
let NOT_LESS_0 = ARITH_RULE `!n. ~(n < 0)`;;
let ZERO_LESS_EXP = prove
(`!m n. 0 < ((SUC n) EXP m)`,
REWRITE_TAC[LT_NZ; NOT_EXP_0]);;
(* ------------------------------------------------------------------------- *)
(* General arithmetic lemmas. *)
(* ------------------------------------------------------------------------- *)
let MULT_FIX = prove(
`!x y. (x * y = x) <=> (x = 0) \/ (y = 1)`,
REPEAT GEN_TAC THEN
STRUCT_CASES_TAC(SPEC `x:num` num_CASES) THEN
REWRITE_TAC[MULT_CLAUSES; NOT_SUC] THEN
REWRITE_TAC[GSYM(el 4 (CONJUNCTS (SPEC_ALL MULT_CLAUSES)))] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) (* MMA: this is a problem !!!!)
[GSYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN
MATCH_ACCEPT_TAC MULT_MONO_EQ);;
let LESS_EQ_MULT = prove(
`!m n p q. m <= n /\ p <= q ==> (m * p) <= (n * q)`,
REPEAT GEN_TAC THEN
DISCH_THEN(STRIP_ASSUME_TAC o REWRITE_RULE[LE_EXISTS]) THEN
ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB;
GSYM ADD_ASSOC; LE_ADD]);;
let LESS_MULT = prove(
`!m n p q. m < n /\ p < q ==> (m * p) < (n * q)`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN
((CHOOSE_THEN SUBST_ALL_TAC) o MATCH_MP LESS_ADD_1)) THEN
REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
REWRITE_TAC[GSYM ADD1; MULT_CLAUSES; ADD_CLAUSES; GSYM ADD_ASSOC] THEN
ONCE_REWRITE_TAC[GSYM (el 3 (CONJUNCTS ADD_CLAUSES))] THEN
MATCH_ACCEPT_TAC LESS_ADD_SUC);;
let MULT_LCANCEL = prove(
`!a b c. ~(a = 0) /\ (a * b = a * c) ==> (b = c)`,
REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC `a:num` num_CASES) THEN
REWRITE_TAC[NOT_SUC; MULT_MONO_EQ]);;
let LT_POW2_REFL = prove
(`!n. n < 2 EXP n`,
INDUCT_TAC THEN REWRITE_TAC[EXP] THEN TRY(POP_ASSUM MP_TAC) THEN ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Properties of the exponential function. *)
(* ------------------------------------------------------------------------- *)
let EXP_0 = prove
(`!n. 0 EXP (SUC n) = 0`,
REWRITE_TAC[EXP; MULT_CLAUSES]);;
let EXP_MONO_LT_SUC = prove
(`!n x y. (x EXP (SUC n)) < (y EXP (SUC n)) <=> (x < y)`,
REWRITE_TAC[EXP_MONO_LT; NOT_SUC]);;
let EXP_MONO_LE_SUC = prove
(`!x y n. (x EXP (SUC n)) <= (y EXP (SUC n)) <=> x <= y`,
REWRITE_TAC[EXP_MONO_LE; NOT_SUC]);;
let EXP_MONO_EQ_SUC = prove
(`!x y n. (x EXP (SUC n) = y EXP (SUC n)) <=> (x = y)`,
REWRITE_TAC[EXP_MONO_EQ; NOT_SUC]);;
let EXP_EXP = prove
(`!x m n. (x EXP m) EXP n = x EXP (m * n)`,
REWRITE_TAC[EXP_MULT]);;
(* ------------------------------------------------------------------------- *)
(* More ad-hoc arithmetic lemmas unlikely to be useful elsewhere. *)
(* ------------------------------------------------------------------------- *)
let DIFF_LEMMA = prove(
`!a b. a < b ==> (a = 0) \/ (a + (b - a)) < (a + b)`,
REPEAT GEN_TAC THEN
DISJ_CASES_TAC(SPEC `a:num` LESS_0_CASES) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN
DISJ2_TAC THEN REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM (CONJUNCT1 ADD_CLAUSES)] THEN
REWRITE_TAC[ADD_ASSOC] THEN
REPEAT(MATCH_MP_TAC LESS_MONO_ADD) THEN POP_ASSUM ACCEPT_TAC);;
let NOT_EVEN_EQ_ODD = prove(
`!m n. ~(2 * m = SUC(2 * n))`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN; EVEN_MULT; ARITH]);;
let CANCEL_TIMES2 = prove(
`!x y. (2 * x = 2 * y) <=> (x = y)`,
REWRITE_TAC[num_CONV `2`; MULT_MONO_EQ]);;
let EVEN_SQUARE = prove(
`!n. EVEN(n) ==> ?x. n EXP 2 = 4 * x`,
GEN_TAC THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
EXISTS_TAC `m * m` THEN REWRITE_TAC[EXP_2] THEN
REWRITE_TAC[SYM(REWRITE_CONV[ARITH] `2 * 2`)] THEN
REWRITE_TAC[MULT_AC]);;
let ODD_SQUARE = prove(
`!n. ODD(n) ==> ?x. n EXP 2 = (4 * x) + 1`,
GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN
ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
REWRITE_TAC[GSYM ADD1; SUC_INJ] THEN
EXISTS_TAC `(m * m) + m` THEN
REWRITE_TAC(map num_CONV [`4`; `3`; `2`; `1`]) THEN
REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
REWRITE_TAC[ADD_AC]);;
let DIFF_SQUARE = prove(
`!x y. (x EXP 2) - (y EXP 2) = (x + y) * (x - y)`,
REPEAT GEN_TAC THEN
DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THENL
[SUBGOAL_THEN `(x * x) <= (y * y)` MP_TAC THENL
[MATCH_MP_TAC LESS_EQ_MULT THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM SUB_EQ_0] THEN
REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES]];
POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
REWRITE_TAC[GSYM ADD_ASSOC; ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [ADD_SYM] THEN
AP_TERM_TAC THEN MATCH_ACCEPT_TAC MULT_SYM]);;
let ADD_IMP_SUB = prove(
`!x y z. (x + y = z) ==> (x = z - y)`,
REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
REWRITE_TAC[ADD_SUB]);;
let ADD_SUM_DIFF = prove(
`!v w. v <= w ==> ((w + v) - (w - v) = 2 * v) /\
((w + v) + (w - v) = 2 * w)`,
REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
REWRITE_TAC[MULT_2; GSYM ADD_ASSOC] THEN
ONCE_REWRITE_TAC[ADD_SYM] THEN
REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB; GSYM ADD_ASSOC]);;
let EXP_4 = prove(
`!n. n EXP 4 = (n EXP 2) EXP 2`,
GEN_TAC THEN REWRITE_TAC[EXP_EXP] THEN
REWRITE_TAC[ARITH]);;
|
