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