intExtensionScript.sml

1(***************************************************************************
2 *
3 *  intExtensionScript.sml
4 *
5 *  extension of the theory of integers
6 *  Jens Brandt
7 *
8 ***************************************************************************)
9Theory intExtension
10Ancestors
11  arithmetic pair integer
12Libs
13  intLib schneiderUtils
14
15
16(*--------------------------------------------------------------------------*
17   operations
18 *--------------------------------------------------------------------------*)
19
20Definition SGN_def:
21  SGN x = if x = 0i then 0i else if x < 0i then ~1 else 1i
22End
23
24(*--------------------------------------------------------------------------
25   INT_SGN_TOTAL : thm
26   |- !a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)
27 *--------------------------------------------------------------------------*)
28
29Theorem INT_SGN_TOTAL: !a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)
30Proof
31  RW_TAC int_ss[SGN_def]
32QED
33
34Theorem INT_SGN_CASES:
35  !a P. (SGN a = ~1 /\ a < 0 ==> P) /\ (SGN a = 0i /\ a = 0 ==> P) /\
36        (SGN a = 1i /\ 0 < a ==> P) ==> P
37Proof
38  rw[] >> qspec_then ‘a’ strip_assume_tac INT_SGN_TOTAL >> gvs[] >>
39  gvs[SGN_def,AllCaseEqs()] >> metis_tac[INT_LT_TOTAL]
40QED
41
42(*--------------------------------------------------------------------------
43   linking ABS and SGN: |- ABS x = x * SGN x, |- ABS x * SGN x = x
44 *--------------------------------------------------------------------------*)
45
46Theorem ABS_EQ_MUL_SGN: ABS x = x * SGN x
47Proof
48  rw[SGN_def, INT_ABS, GSYM INT_NEG_RMUL]
49QED
50
51Theorem MUL_ABS_SGN: ABS x * SGN x = x
52Proof
53  rw[INT_ABS, SGN_def]
54QED
55
56Theorem ABS_SGN:
57  ABS (SGN i) = if i = 0 then 0 else 1
58Proof
59  Cases_on `i` >> gvs[SGN_def]
60QED
61
62Theorem SGN_MUL_Num[simp]:
63  SGN i * &Num i = i
64Proof
65  Cases_on `i` >> gvs[SGN_def] >>
66  simp[INT_MUL_CALCULATE]
67QED
68
69(*--------------------------------------------------------------------------
70   INT_MUL_POS_SIGN: thm
71   |- !a b. 0 < a ==> 0 < b ==> 0 < a * b
72 *--------------------------------------------------------------------------*)
73
74Theorem INT_MUL_POS_SIGN: !a:int b:int. 0 < a ==> 0 < b ==> 0i < a * b
75Proof
76  rw[INT_MUL_SIGN_CASES]
77QED
78
79(*--------------------------------------------------------------------------
80   INT_NE_IMP_LTGT: thm
81   |- !x. ~(x = 0) = (0 < x) \/ (x < 0)
82 *--------------------------------------------------------------------------*)
83
84Theorem INT_NE_IMP_LTGT: !x:int. x <> 0 <=> 0 < x \/ x < 0
85Proof
86  metis_tac[INT_LT_TOTAL, INT_LT_REFL]
87QED
88
89(*--------------------------------------------------------------------------
90   INT_NOTGT_IMP_EQLT : thm
91   |- !n. ~(n < 0) = (0 = n) \/ 0 < n
92 *--------------------------------------------------------------------------*)
93
94Theorem INT_NOTGT_IMP_EQLT: !n:int. ~(n < 0) <=> (0 = n) \/ 0 < n
95Proof
96  metis_tac[INT_LT_TOTAL, INT_LT_REFL, INT_LT_TRANS]
97QED
98
99(*--------------------------------------------------------------------------
100   INT_NOTPOS0_NEG : thm
101   |- !a. ~(0 < a) ==> ~(a = 0) ==> 0 < ~a
102 *--------------------------------------------------------------------------*)
103
104Theorem INT_NOTPOS0_NEG:   !a. ~(0i<a) ==> ~(a=0i) ==> 0i<~a
105Proof
106        REPEAT STRIP_TAC THEN
107        ONCE_REWRITE_TAC[GSYM INT_NEG_0] THEN
108        REWRITE_TAC[INT_LT_NEG] THEN
109        PROVE_TAC[INT_LT_TOTAL]
110QED
111
112(*--------------------------------------------------------------------------
113   INT_NOT0_MUL : thm
114   |- !a b. ~(a = 0) ==> ~(b = 0) ==> ~(a * b = 0)
115 *--------------------------------------------------------------------------*)
116
117Theorem INT_NOT0_MUL: !a b. ~(a=0i) ==> ~(b=0i) ==> ~(a*b=0i)
118Proof
119  PROVE_TAC[INT_ENTIRE]
120QED
121
122(*--------------------------------------------------------------------------
123   INT_GT0_IMP_NOT0 : thm
124   |- !a. 0 < a ==> ~(a = 0)
125 *--------------------------------------------------------------------------*)
126
127Theorem INT_GT0_IMP_NOT0: !a. 0i<a ==> ~(a=0i)
128Proof
129        REPEAT STRIP_TAC THEN
130        ASM_CASES_TAC ``a = 0i`` THEN
131        ASM_CASES_TAC ``a < 0i`` THEN
132        PROVE_TAC[INT_LT_ANTISYM,INT_LT_TOTAL]
133QED
134
135(*--------------------------------------------------------------------------
136   INT_NOTLTEQ_GT : thm
137   |- !a. ~(a < 0) ==> ~(a = 0) ==> 0 < a
138 *--------------------------------------------------------------------------*)
139
140Theorem INT_NOTLTEQ_GT: !a:int. ~(a<0i) ==> a <> 0 ==> 0 < a
141Proof
142        PROVE_TAC[INT_LT_TOTAL]
143QED
144
145(*--------------------------------------------------------------------------
146   INT_ABS_NOT0POS : thm
147   |- !x. ~(x = 0) ==> 0 < ABS x
148 *--------------------------------------------------------------------------*)
149
150Theorem INT_ABS_NOT0POS = iffRL INT_ABS_0LT |> GEN_ALL
151
152(*--------------------------------------------------------------------------
153   INT_SGN_NOTPOSNEG : thm
154   |- !x. ~(SGN x = ~1) ==> ~(SGN x = 1) ==> (SGN x = 0)
155 *--------------------------------------------------------------------------*)
156
157Theorem INT_SGN_NOTPOSNEG: !x. ~(SGN x = ~1) ==> ~(SGN x = 1) ==> (SGN x = 0)
158Proof
159  rw[SGN_def]
160QED
161
162(*--------------------------------------------------------------------------
163   LESS_IMP_NOT_0 : thm
164   |- !n. 0 < n ==> ~(n = 0)
165 *--------------------------------------------------------------------------*)
166
167Theorem LESS_IMP_NOT_0:   !n:int. 0i<n ==> ~(n=0i)
168Proof
169        GEN_TAC THEN
170        ASM_CASES_TAC ``n=0i``
171        THEN RW_TAC int_ss[]
172QED
173
174(*--------------------------------------------------------------------------
175 *  INT_EQ_RMUL_EXP : thm
176 *  |- !a b n. 0<n ==> ((a=b) = (a*n=b*n))
177 *--------------------------------------------------------------------------*)
178
179Theorem INT_EQ_RMUL_EXP:   !a:int b:int n:int. 0<n ==> ((a=b) = (a*n=b*n))
180Proof
181        REPEAT STRIP_TAC
182        THEN EQ_TAC
183        THEN ASSUME_TAC (prove(``0i<n ==> ~(n=0i)``, ASM_CASES_TAC ``n=0i`` THEN RW_TAC int_ss[]))
184        THEN ASSUME_TAC (SPEC ``n:int`` (SPEC ``b:int`` (SPEC ``a:int`` INT_EQ_RMUL_IMP)))
185        THEN RW_TAC int_ss[]
186QED
187
188(*--------------------------------------------------------------------------
189   INT_LT_RMUL_EXP : thm
190   |- !a b n. !a b n. 0 < n ==> ((a < b) = (a * n < b * n))
191 *--------------------------------------------------------------------------*)
192
193Theorem INT_LT_RMUL_EXP:   !a:int b:int n:int. 0<n ==> ((a<b) = (a*n<b*n))
194Proof
195        REPEAT STRIP_TAC THEN
196        ASSUME_TAC (UNDISCH_ALL (GSYM (SPEC ``b:int`` (SPEC ``a:int`` (SPEC ``n:int`` INT_LT_MONO))))) THEN
197        RW_TAC int_ss[INT_MUL_SYM]
198QED
199
200(*--------------------------------------------------------------------------
201   INT_GT_RMUL_EXP : thm
202   |- !a b n. 0 < n ==> ((a > b) = (a * n > b * n))
203 *--------------------------------------------------------------------------*)
204
205Theorem INT_GT_RMUL_EXP:   !a:int b:int n:int. 0<n ==> ((a>b) = (a*n>b*n))
206Proof
207        REPEAT STRIP_TAC THEN
208        REWRITE_TAC[int_gt] THEN
209        ASSUME_TAC (UNDISCH_ALL (GSYM (SPEC ``a:int`` (SPEC ``b:int`` (SPEC ``n:int`` INT_LT_MONO))))) THEN
210        RW_TAC int_ss[INT_MUL_SYM]
211QED
212
213(*--------------------------------------------------------------------------
214   INT_ABS_CALCULATE_NEG : thm
215   |- !a. a<0 ==> (ABS(a) = ~a)
216 *--------------------------------------------------------------------------*)
217
218Theorem INT_ABS_CALCULATE_NEG:   !a. a<0 ==> (ABS(a) = ~a)
219Proof
220        GEN_TAC THEN
221        STRIP_TAC THEN
222        RW_TAC int_ss[INT_ABS]
223QED
224
225(*--------------------------------------------------------------------------
226   INT_ABS_CALCULATE_0 : thm
227   |- ABS 0i = 0i
228 *--------------------------------------------------------------------------*)
229
230Theorem INT_ABS_CALCULATE_0:   ABS 0i = 0i
231Proof
232        RW_TAC int_ss[INT_ABS]
233QED
234
235Theorem INT_ABS_CALCULATE_POS: !a. 0<a ==> (ABS(a) = a)
236Proof
237  RW_TAC int_ss[INT_ABS, INT_LT_GT]
238QED
239
240(*--------------------------------------------------------------------------
241   INT_NOT0_SGNNOT0 : thm
242   |- !x. ~(x = 0) ==> ~(SGN x = 0)
243 *--------------------------------------------------------------------------*)
244
245Theorem INT_NOT0_SGNNOT0:
246  !x. ~(x = 0) ==> ~(SGN x = 0)
247Proof
248  REPEAT GEN_TAC THEN STRIP_TAC THEN
249  MATCH_MP_TAC (SPEC ``x:int`` INT_SGN_CASES) THEN
250  REPEAT CONJ_TAC THEN
251  STRIP_TAC  THEN
252  RW_TAC intLib.int_ss []
253QED
254
255Theorem INT_SGN_CLAUSES:
256  !x. (SGN x = ~1 <=> x < 0) /\ (SGN x = 0i <=> x = 0) /\
257      (SGN x = 1i <=> 0 < x)
258Proof
259  GEN_TAC >> qspec_then ‘x’ strip_assume_tac INT_SGN_CASES >>
260  rpt conj_tac >> pop_assum irule >> simp[] >>
261  metis_tac[INT_LT_TRANS, INT_LT_REFL]
262QED
263
264Theorem INT_SGN_MUL2: !x y. SGN (x * y) = SGN x * SGN y
265Proof
266  REPEAT GEN_TAC THEN
267  REWRITE_TAC[SGN_def] THEN
268  RW_TAC int_ss[] THEN
269  UNDISCH_ALL_TAC THEN
270  RW_TAC int_ss[INT_MUL_LZERO, INT_MUL_RZERO] THEN
271  PROVE_TAC[INT_ENTIRE, INT_MUL_SIGN_CASES, INT_LT_ANTISYM, INT_LT_TOTAL]
272QED
273
274(*--------------------------------------------------------------------------
275   INT_LT_ADD_NEG : thm
276   |- !x y. x < 0i /\ y < 0i ==> x + y < 0i
277 *--------------------------------------------------------------------------*)
278
279Theorem INT_LT_ADD_NEG: !x y. x < 0i /\ y < 0i ==> x + y < 0i
280Proof
281        REWRITE_TAC[GSYM INT_NEG_GT0, INT_NEG_ADD] THEN
282        PROVE_TAC[INT_LT_ADD]
283QED
284
285