1(***************************************************************************
2 *
3 *  intExtensionScript.sml
4 *
5 *  extension of the theory of integers
6 *  Jens Brandt
7 *
8 ***************************************************************************)
9
10open HolKernel boolLib Parse bossLib;
11
12(* interactive mode
13app load ["integerTheory","intLib",
14"ringLib", "pairTheory",
15        "integerRingTheory","integerRingLib",
16        "schneiderUtils"];
17*)
18open
19        arithmeticTheory pairTheory
20        integerTheory intLib
21        ringTheory ringLib integerRingLib
22        schneiderUtils;
23
24val _ = new_theory "intExtension";
25
26(*--------------------------------------------------------------------------*
27   operations
28 *--------------------------------------------------------------------------*)
29
30val SGN_def = Define `SGN x = (if x = 0i then 0i else (if x < 0i then ~1 else 1i))`;
31
32(*--------------------------------------------------------------------------
33   linking ABS and SGN: |- ABS x = x * SGN x, |- ABS x * SGN x = x
34 *--------------------------------------------------------------------------*)
35
36val ABS_EQ_MUL_SGN = store_thm ("ABS_EQ_MUL_SGN", ``ABS x = x * SGN x``,
37  REWRITE_TAC [INT_ABS, SGN_def] THEN
38  REPEAT COND_CASES_TAC THEN
39  ASM_SIMP_TAC int_ss [GSYM INT_NEG_RMUL]) ;
40
41val MUL_ABS_SGN = store_thm ("MUL_ABS_SGN", ``ABS x * SGN x = x``,
42  REWRITE_TAC [INT_ABS, SGN_def] THEN
43  REPEAT COND_CASES_TAC THEN
44  ASM_SIMP_TAC int_ss []) ;
45
46(*--------------------------------------------------------------------------
47   INT_MUL_POS_SIGN: thm
48   |- !a b. 0 < a ==> 0 < b ==> 0 < a * b
49 *--------------------------------------------------------------------------*)
50
51val INT_MUL_POS_SIGN =
52let
53        val lemma01 = #2 (EQ_IMP_RULE (CONJUNCT1 (SPEC_ALL INT_MUL_SIGN_CASES)));
54in
55        store_thm("INT_MUL_POS_SIGN", ``!a:int b:int. 0i<a ==> 0i<b ==> 0i<a * b``, RW_TAC int_ss[lemma01])
56end;
57
58(*--------------------------------------------------------------------------
59   INT_NE_IMP_LTGT: thm
60   |- !x. ~(x = 0) = (0 < x) \/ (x < 0)
61 *--------------------------------------------------------------------------*)
62
63Theorem INT_NE_IMP_LTGT: !x. x <> 0i <=> 0i<x \/ x<0i
64Proof
65        GEN_TAC THEN
66        EQ_TAC THENL
67        [
68                REWRITE_TAC[IMP_DISJ_THM] THEN
69                PROVE_TAC[INT_LT_TOTAL]
70        ,
71                PROVE_TAC[INT_LT_IMP_NE]
72        ]
73QED
74
75(*--------------------------------------------------------------------------
76   INT_NOTGT_IMP_EQLT : thm
77   |- !n. ~(n < 0) = (0 = n) \/ 0 < n
78 *--------------------------------------------------------------------------*)
79
80Theorem INT_NOTGT_IMP_EQLT: !n. ~(n < 0i) <=> (0i = n) \/ 0i < n
81Proof
82        GEN_TAC THEN
83        EQ_TAC THEN
84        STRIP_TAC THENL
85        [
86                LEFT_DISJ_TAC THEN
87                PROVE_TAC[INT_LT_TOTAL]
88        ,
89                PROVE_TAC[INT_LT_IMP_NE]
90        ,
91                PROVE_TAC[INT_LT_GT]
92        ]
93QED
94
95(*--------------------------------------------------------------------------
96   INT_NO_ZERODIV : thm
97   |- !x y. (x = 0) \/ (y = 0) = (x * y = 0)
98 *--------------------------------------------------------------------------*)
99
100Theorem INT_NO_ZERODIV: !x y. (x = 0i) \/ (y = 0i) = (x * y = 0i)
101Proof
102        REPEAT GEN_TAC THEN
103        ASM_CASES_TAC ``x=0i`` THEN
104        ASM_CASES_TAC ``y=0i`` THEN
105        RW_TAC int_ss[INT_MUL_LZERO, INT_MUL_RZERO] THEN
106        REWRITE_TAC[INT_NE_IMP_LTGT] THEN
107        REWRITE_TAC[INT_MUL_SIGN_CASES] THEN
108        PROVE_TAC[INT_LT_TOTAL]
109QED
110
111(*--------------------------------------------------------------------------
112   INT_NOTPOS0_NEG : thm
113   |- !a. ~(0 < a) ==> ~(a = 0) ==> 0 < ~a
114 *--------------------------------------------------------------------------*)
115
116val INT_NOTPOS0_NEG = store_thm("INT_NOTPOS0_NEG", ``!a. ~(0i<a) ==> ~(a=0i) ==> 0i<~a``,
117        REPEAT STRIP_TAC THEN
118        ONCE_REWRITE_TAC[GSYM INT_NEG_0] THEN
119        REWRITE_TAC[INT_LT_NEG] THEN
120        PROVE_TAC[INT_LT_TOTAL] );
121
122(*--------------------------------------------------------------------------
123   INT_NOT0_MUL : thm
124   |- !a b. ~(a = 0) ==> ~(b = 0) ==> ~(a * b = 0)
125 *--------------------------------------------------------------------------*)
126
127val INT_NOT0_MUL = store_thm("INT_NOT0_MUL", ``!a b. ~(a=0i) ==> ~(b=0i) ==> ~(a*b=0i)``,
128        PROVE_TAC[INT_NO_ZERODIV] );
129
130(*--------------------------------------------------------------------------
131   INT_GT0_IMP_NOT0 : thm
132   |- !a. 0 < a ==> ~(a = 0)
133 *--------------------------------------------------------------------------*)
134
135val INT_GT0_IMP_NOT0 = store_thm("INT_GT0_IMP_NOT0",``!a. 0i<a ==> ~(a=0i)``,
136        REPEAT STRIP_TAC THEN
137        ASM_CASES_TAC ``a = 0i`` THEN
138        ASM_CASES_TAC ``a < 0i`` THEN
139        PROVE_TAC[INT_LT_ANTISYM,INT_LT_TOTAL] );
140
141(*--------------------------------------------------------------------------
142   INT_NOTLTEQ_GT : thm
143   |- !a. ~(a < 0) ==> ~(a = 0) ==> 0 < a
144 *--------------------------------------------------------------------------*)
145
146val INT_NOTLTEQ_GT = store_thm("INT_NOTLTEQ_GT", ``!a. ~(a<0i) ==> ~(a=0i) ==> 0i<a``,
147        REPEAT STRIP_TAC THEN
148        PROVE_TAC[INT_LT_TOTAL] );
149
150(*--------------------------------------------------------------------------
151   INT_ABS_NOT0POS : thm
152   |- !x. ~(x = 0) ==> 0 < ABS x
153 *--------------------------------------------------------------------------*)
154
155val INT_ABS_NOT0POS = store_thm("INT_ABS_NOT0POS", ``!x:int. ~(x = 0i) ==> 0i < ABS x``,
156        REPEAT STRIP_TAC THEN
157        REWRITE_TAC[INT_ABS] THEN
158        ASM_CASES_TAC ``x<0i`` THENL
159        [
160                RW_TAC int_ss[] THEN
161                ONCE_REWRITE_TAC[GSYM INT_NEG_0] THEN
162                REWRITE_TAC[INT_LT_NEG] THEN
163                PROVE_TAC[]
164        ,
165                RW_TAC int_ss[] THEN
166                UNDISCH_TAC ``~(x < 0i)`` THEN
167                UNDISCH_TAC ``~(x = 0i)`` THEN
168                REWRITE_TAC[IMP_DISJ_THM] THEN
169                PROVE_TAC[INT_LT_TOTAL]
170        ]);
171
172(*--------------------------------------------------------------------------
173   INT_SGN_NOTPOSNEG : thm
174   |- !x. ~(SGN x = ~1) ==> ~(SGN x = 1) ==> (SGN x = 0)
175 *--------------------------------------------------------------------------*)
176
177val INT_SGN_NOTPOSNEG = store_thm("INT_SGN_NOTPOSNEG", ``!x. ~(SGN x = ~1) ==> ~(SGN x = 1) ==> (SGN x = 0)``,
178        GEN_TAC THEN
179        REWRITE_TAC[SGN_def] THEN
180        RW_TAC int_ss[] );
181
182(*--------------------------------------------------------------------------
183   INT_SGN_CASES : thm
184   |- !x P.
185        ((SGN x = ~1) /\ (x < 0) ==> P) /\
186        ((SGN x = 0i) /\ (x = 0) ==> P) /\
187        ((SGN x = 1i) /\ (0 < x) ==> P) ==> P
188 *--------------------------------------------------------------------------*)
189
190val INT_SGN_CASES = store_thm
191  ("INT_SGN_CASES", ``!x P. ((SGN x = ~1) /\ (x < 0) ==> P) /\
192                            ((SGN x = 0i) /\ (x = 0) ==> P) /\
193                            ((SGN x = 1i) /\ (0 < x) ==> P) ==> P``,
194        REPEAT GEN_TAC THEN
195        ASM_CASES_TAC ``(SGN x = ~1) /\ (x < 0)`` THEN
196        UNDISCH_HD_TAC THEN
197        ASM_CASES_TAC ``(SGN x = 1i) /\ (0 < x)`` THEN
198        UNDISCH_HD_TAC THEN
199        REWRITE_TAC[SGN_def] THEN
200        REWRITE_TAC[DE_MORGAN_THM] THEN
201        RW_TAC int_ss[] THEN
202        PROVE_TAC[INT_LT_TOTAL, INT_SGN_NOTPOSNEG] );
203
204(*--------------------------------------------------------------------------
205   LESS_IMP_NOT_0 : thm
206   |- !n. 0 < n ==> ~(n = 0)
207 *--------------------------------------------------------------------------*)
208
209val LESS_IMP_NOT_0 = store_thm("LESS_IMP_NOT_0", ``!n:int. 0i<n ==> ~(n=0i)``,
210        GEN_TAC THEN
211        ASM_CASES_TAC ``n=0i``
212        THEN RW_TAC int_ss[] );
213
214(*--------------------------------------------------------------------------
215 *  INT_EQ_RMUL_EXP : thm
216 *  |- !a b n. 0<n ==> ((a=b) = (a*n=b*n))
217 *--------------------------------------------------------------------------*)
218
219val INT_EQ_RMUL_EXP = store_thm("INT_EQ_RMUL_EXP", ``!a:int b:int n:int. 0<n ==> ((a=b) = (a*n=b*n))``,
220        REPEAT STRIP_TAC
221        THEN EQ_TAC
222        THEN ASSUME_TAC (prove(``0i<n ==> ~(n=0i)``, ASM_CASES_TAC ``n=0i`` THEN RW_TAC int_ss[]))
223        THEN ASSUME_TAC (SPEC ``n:int`` (SPEC ``b:int`` (SPEC ``a:int`` INT_EQ_RMUL_IMP)))
224        THEN RW_TAC int_ss[] );
225
226(*--------------------------------------------------------------------------
227   INT_LT_RMUL_EXP : thm
228   |- !a b n. !a b n. 0 < n ==> ((a < b) = (a * n < b * n))
229 *--------------------------------------------------------------------------*)
230
231val INT_LT_RMUL_EXP = store_thm("INT_LT_RMUL_EXP", ``!a:int b:int n:int. 0<n ==> ((a<b) = (a*n<b*n))``,
232        REPEAT STRIP_TAC THEN
233        ASSUME_TAC (UNDISCH_ALL (GSYM (SPEC ``b:int`` (SPEC ``a:int`` (SPEC ``n:int`` INT_LT_MONO))))) THEN
234        RW_TAC int_ss[INT_MUL_SYM] );
235
236(*--------------------------------------------------------------------------
237   INT_GT_RMUL_EXP : thm
238   |- !a b n. 0 < n ==> ((a > b) = (a * n > b * n))
239 *--------------------------------------------------------------------------*)
240
241val INT_GT_RMUL_EXP = store_thm("INT_GT_RMUL_EXP", ``!a:int b:int n:int. 0<n ==> ((a>b) = (a*n>b*n))``,
242        REPEAT STRIP_TAC THEN
243        REWRITE_TAC[int_gt] THEN
244        ASSUME_TAC (UNDISCH_ALL (GSYM (SPEC ``a:int`` (SPEC ``b:int`` (SPEC ``n:int`` INT_LT_MONO))))) THEN
245        RW_TAC int_ss[INT_MUL_SYM] );
246
247(*--------------------------------------------------------------------------
248   INT_ABS_CALCULATE_NEG : thm
249   |- !a. a<0 ==> (ABS(a) = ~a)
250 *--------------------------------------------------------------------------*)
251
252val INT_ABS_CALCULATE_NEG = store_thm("INT_ABS_CALCULATE_NEG", ``!a. a<0 ==> (ABS(a) = ~a)``,
253        GEN_TAC THEN
254        STRIP_TAC THEN
255        RW_TAC int_ss[INT_ABS] );
256
257(*--------------------------------------------------------------------------
258   INT_ABS_CALCULATE_0 : thm
259   |- ABS 0i = 0i
260 *--------------------------------------------------------------------------*)
261
262val INT_ABS_CALCULATE_0 = store_thm("INT_ABS_CALCULATE_0", ``ABS 0i = 0i``,
263        RW_TAC int_ss[INT_ABS] );
264
265(*--------------------------------------------------------------------------
266   INT_ABS_CALCULATE_POS : thm
267   |- !a. 0<a ==> (ABS(a) = a)
268 *--------------------------------------------------------------------------*)
269
270val INT_ABS_CALCULATE_POS = store_thm("INT_ABS_CALCULATE_POS", ``!a. 0<a ==> (ABS(a) = a)``,
271        GEN_TAC THEN
272        STRIP_TAC THEN
273        RW_TAC int_ss[INT_ABS, INT_LT_GT] );
274
275(*--------------------------------------------------------------------------
276   INT_NOT0_SGNNOT0 : thm
277   |- !x. ~(x = 0) ==> ~(SGN x = 0)
278 *--------------------------------------------------------------------------*)
279
280val INT_NOT0_SGNNOT0 = store_thm("INT_NOT0_SGNNOT0", ``!x. ~(x = 0) ==> ~(SGN x = 0)``,
281        REPEAT GEN_TAC THEN
282        STRIP_TAC THEN
283        MATCH_MP_TAC (SPEC ``x:int`` INT_SGN_CASES) THEN
284        REPEAT CONJ_TAC THEN
285        STRIP_TAC  THEN
286        RW_TAC intLib.int_ss [] );
287
288(*--------------------------------------------------------------------------
289   INT_SGN_CLAUSES : thm
290   |- !x. (SGN x = ~1) =
291          (x < 0)) /\ ((SGN x = 0i) = (x = 0)) /\ ((SGN x = 1i) = (x > 0)
292 *--------------------------------------------------------------------------*)
293
294val INT_SGN_CLAUSES = store_thm("INT_SGN_CLAUSES", ``!x. ((SGN x = ~1) = (x < 0)) /\ ((SGN x = 0i) = (x = 0)) /\ ((SGN x = 1i) = (x > 0))``,
295        GEN_TAC THEN
296        RW_TAC int_ss[SGN_def] THEN
297        REWRITE_TAC[int_gt] THEN
298        PROVE_TAC[INT_LT_GT, INT_LT_TOTAL] );
299
300(*--------------------------------------------------------------------------
301   INT_SGN_MUL : thm
302   |- !x1 x2 y1 y2. (SGN x1 = y1) ==> (SGN x2 = y2) ==>
303                    (SGN (x1 * x2) = y1 * y2)
304 *--------------------------------------------------------------------------*)
305
306val INT_SGN_MUL = store_thm("INT_SGN_MUL", ``!x1 x2 y1 y2. (SGN x1 = y1) ==> (SGN x2 = y2) ==> (SGN (x1 * x2) = y1 * y2)``,
307        REPEAT GEN_TAC THEN
308        REWRITE_TAC[SGN_def] THEN
309        RW_TAC int_ss[] THEN
310        UNDISCH_ALL_TAC THEN
311        RW_TAC int_ss[INT_MUL_LZERO, INT_MUL_RZERO] THEN
312        PROVE_TAC[INT_NO_ZERODIV, INT_MUL_SIGN_CASES, INT_LT_ANTISYM, INT_LT_TOTAL] );
313
314(*--------------------------------------------------------------------------
315   INT_SGN_MUL2 : thm
316   |- !x y. SGN (x * y) = SGN x * SGN y
317 *--------------------------------------------------------------------------*)
318
319val INT_SGN_MUL2 = store_thm("INT_SGN_MUL2", ``!x y. SGN (x * y) = SGN x * SGN y``,
320        REPEAT GEN_TAC THEN
321        REWRITE_TAC[SGN_def] THEN
322        RW_TAC int_ss[] THEN
323        UNDISCH_ALL_TAC THEN
324        RW_TAC int_ss[INT_MUL_LZERO, INT_MUL_RZERO] THEN
325        PROVE_TAC[INT_NO_ZERODIV, INT_MUL_SIGN_CASES, INT_LT_ANTISYM, INT_LT_TOTAL] );
326
327(*--------------------------------------------------------------------------
328   INT_SGN_TOTAL : thm
329   |- !a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)
330 *--------------------------------------------------------------------------*)
331
332val INT_SGN_TOTAL = store_thm("INT_SGN_TOTAL",``!a. (SGN a = ~1) \/ (SGN a = 0) \/ (SGN a = 1)``,
333        GEN_TAC THEN
334        REWRITE_TAC[SGN_def] THEN
335        RW_TAC int_ss[] );
336
337(*--------------------------------------------------------------------------
338   INT_SGN_CASES : thm
339   |- !a P. ((SGN a = ~1) ==> P) /\ ((SGN a = 0i) ==> P) /\
340                                    ((SGN a = 1i) ==> P) ==> P
341 *--------------------------------------------------------------------------*)
342
343val INT_SGN_CASES = store_thm("INT_SGN_CASES", ``!a P. ((SGN a = ~1) ==> P) /\ ((SGN a = 0i) ==> P) /\ ((SGN a = 1i) ==> P) ==> P``,
344        REPEAT GEN_TAC THEN
345        ASM_CASES_TAC ``SGN a = ~1`` THEN
346        ASM_CASES_TAC ``SGN a = 0i`` THEN
347        ASM_CASES_TAC ``SGN a = 1i`` THEN
348        UNDISCH_ALL_TAC THEN
349        PROVE_TAC[INT_SGN_TOTAL] );
350
351(*--------------------------------------------------------------------------
352   INT_LT_ADD_NEG : thm
353   |- !x y. x < 0i /\ y < 0i ==> x + y < 0i
354 *--------------------------------------------------------------------------*)
355
356val INT_LT_ADD_NEG = store_thm("INT_LT_ADD_NEG", ``!x y. x < 0i /\ y < 0i ==> x + y < 0i``,
357        REWRITE_TAC[GSYM INT_NEG_GT0, INT_NEG_ADD] THEN
358        PROVE_TAC[INT_LT_ADD] );
359
360
361val _ = export_theory();
362