1(* ===================================================================== *) 2(* FILE : arithmeticScript.sml *) 3(* DESCRIPTION : Definitions and properties of +,-,*,EXP, <=, >=, etc. *) 4(* Translated from hol88. *) 5(* *) 6(* AUTHORS : (c) Mike Gordon and *) 7(* Tom Melham, University of Cambridge *) 8(* DATE : 88.04.02 *) 9(* TRANSLATOR : Konrad Slind, University of Calgary *) 10(* DATE : September 15, 1991 *) 11(* ADDITIONS : December 22, 1992 *) 12(* ===================================================================== *) 13 14open HolKernel boolLib Parse 15 Prim_rec simpLib boolSimps metisLib BasicProvers; 16 17local 18 open OpenTheoryMap 19 val ns = ["Number", "Natural"] 20in 21 fun ot0 x y = OpenTheory_const_name 22 {const = {Thy = "arithmetic", Name = x}, name = (ns, y)} 23 fun ot x = ot0 x x 24 fun otunwanted x = OpenTheory_const_name 25 {const = {Thy = "arithmetic", Name = x}, 26 name = (["Unwanted"], "id")} 27end 28 29val _ = new_theory "arithmetic"; 30 31val _ = if !Globals.interactive then () else Feedback.emit_WARNING := false; 32 33val NOT_SUC = numTheory.NOT_SUC 34and INV_SUC = numTheory.INV_SUC 35and INDUCTION = numTheory.INDUCTION; 36 37val num_Axiom = prim_recTheory.num_Axiom; 38val INV_SUC_EQ = prim_recTheory.INV_SUC_EQ 39and LESS_REFL = prim_recTheory.LESS_REFL 40and SUC_LESS = prim_recTheory.SUC_LESS 41and NOT_LESS_0 = prim_recTheory.NOT_LESS_0 42and LESS_MONO = prim_recTheory.LESS_MONO 43and LESS_SUC_REFL = prim_recTheory.LESS_SUC_REFL 44and LESS_SUC = prim_recTheory.LESS_SUC 45and LESS_THM = prim_recTheory.LESS_THM 46and LESS_SUC_IMP = prim_recTheory.LESS_SUC_IMP 47and LESS_0 = prim_recTheory.LESS_0 48and EQ_LESS = prim_recTheory.EQ_LESS 49and SUC_ID = prim_recTheory.SUC_ID 50and NOT_LESS_EQ = prim_recTheory.NOT_LESS_EQ 51and LESS_NOT_EQ = prim_recTheory.LESS_NOT_EQ 52and LESS_SUC_SUC = prim_recTheory.LESS_SUC_SUC 53and PRE = prim_recTheory.PRE 54and RTC_IM_TC = prim_recTheory.RTC_IM_TC 55and TC_IM_RTC_SUC = prim_recTheory.TC_IM_RTC_SUC 56and LESS_ALT = prim_recTheory.LESS_ALT; 57 58(*---------------------------------------------------------------------------* 59 * The basic arithmetic operations. * 60 *---------------------------------------------------------------------------*) 61 62val ADD = new_recursive_definition 63 {name = "ADD", 64 rec_axiom = num_Axiom, 65 def = ���($+ 0 n = n) /\ 66 ($+ (SUC m) n = SUC ($+ m n))���}; 67 68val _ = set_fixity "+" (Infixl 500); 69val _ = ot "+" 70val _ = TeX_notation { hol = "+", TeX = ("\\ensuremath{+}", 1) }; 71 72(*---------------------------------------------------------------------------* 73 * Define NUMERAL, a tag put on numeric literals, and the basic constructors * 74 * of the "numeral type". * 75 *---------------------------------------------------------------------------*) 76 77val NUMERAL_DEF = new_definition("NUMERAL_DEF", ���NUMERAL (x:num) = x���); 78 79val ALT_ZERO = new_definition("ALT_ZERO", ���ZERO = 0���); 80 81local 82 open OpenTheoryMap 83in 84 val _ = OpenTheory_const_name {const = {Thy = "arithmetic", Name = "ZERO"}, 85 name = (["Number", "Natural"], "zero")} 86 val _ = OpenTheory_const_name {const = {Thy = "num", Name = "0"}, 87 name=(["Number", "Natural"], "zero")} 88end 89 90val BIT1 = new_definition("BIT1", ���BIT1 n = n + (n + SUC 0)���); 91val BIT2 = new_definition("BIT2", ���BIT2 n = n + (n + SUC (SUC 0))���); 92 93val _ = new_definition( 94 GrammarSpecials.nat_elim_term, 95 ``^(mk_var(GrammarSpecials.nat_elim_term, Type`:num->num`)) n = n``); 96 97val _ = otunwanted "NUMERAL" 98val _ = ot0 "BIT1" "bit1" 99val _ = ot0 "BIT2" "bit2" 100 101(*---------------------------------------------------------------------------* 102 * After this call, numerals parse into `NUMERAL( ... )` * 103 *---------------------------------------------------------------------------*) 104 105val _ = add_numeral_form (#"n", NONE); 106 107val _ = set_fixity "-" (Infixl 500); 108val _ = Unicode.unicode_version {u = UTF8.chr 0x2212, tmnm = "-"}; 109val _ = TeX_notation {hol = UTF8.chr 0x2212, TeX = ("\\ensuremath{-}", 1)} 110 111val SUB = new_recursive_definition 112 {name = "SUB", 113 rec_axiom = num_Axiom, 114 def = ���(0 - m = 0) /\ 115 (SUC m - n = if m < n then 0 else SUC(m - n))���}; 116 117val _ = ot "-" 118 119(* Also add concrete syntax for unary negation so that future numeric types 120 can use it. We can't do anything useful with it for the natural numbers 121 of course, but it seems like this is the best ancestral place for it. 122 123 Descendents wanting to use this will include at least 124 integer, real, words, rat 125*) 126val _ = add_rule { term_name = "numeric_negate", 127 fixity = Prefix 900, 128 pp_elements = [TOK "-"], 129 paren_style = OnlyIfNecessary, 130 block_style = (AroundEachPhrase, (PP.CONSISTENT,0))}; 131 132(* Similarly, add syntax for the injection from nats symbol (&). This isn't 133 required in this theory, but will be used by descendents. *) 134val _ = add_rule {term_name = GrammarSpecials.num_injection, 135 fixity = Prefix 900, 136 pp_elements = [TOK GrammarSpecials.num_injection], 137 paren_style = OnlyIfNecessary, 138 block_style = (AroundEachPhrase, (PP.CONSISTENT,0))}; 139(* overload it to the nat_elim term *) 140val _ = overload_on (GrammarSpecials.num_injection, 141 mk_const(GrammarSpecials.nat_elim_term, ���:num -> num���)) 142 143val _ = set_fixity "*" (Infixl 600); 144val _ = TeX_notation {hol = "*", TeX = ("\\HOLTokenProd{}", 1)} 145 146val MULT = new_recursive_definition 147 {name = "MULT", 148 rec_axiom = num_Axiom, 149 def = ���(0 * n = 0) /\ 150 (SUC m * n = (m * n) + n)���}; 151 152val _ = ot "*" 153 154val EXP = new_recursive_definition 155 {name = "EXP", 156 rec_axiom = num_Axiom, 157 def = ���($EXP m 0 = 1) /\ 158 ($EXP m (SUC n) = m * ($EXP m n))���}; 159 160val _ = ot0 "EXP" "^" 161val _ = set_fixity "EXP" (Infixr 700); 162val _ = add_infix("**", 700, HOLgrammars.RIGHT); 163val _ = overload_on ("**", Term`$EXP`); 164val _ = TeX_notation {hol = "**", TeX = ("\\HOLTokenExp{}", 2)} 165 166(* special-case squares and cubes *) 167val _ = add_rule {fixity = Suffix 2100, 168 term_name = UnicodeChars.sup_2, 169 block_style = (AroundEachPhrase,(PP.CONSISTENT, 0)), 170 paren_style = OnlyIfNecessary, 171 pp_elements = [TOK UnicodeChars.sup_2]} 172val _ = overload_on (UnicodeChars.sup_2, ���\x. x ** 2���) 173 174val _ = add_rule {fixity = Suffix 2100, 175 term_name = UnicodeChars.sup_3, 176 block_style = (AroundEachPhrase,(PP.CONSISTENT, 0)), 177 paren_style = OnlyIfNecessary, 178 pp_elements = [TOK UnicodeChars.sup_3]} 179val _ = overload_on (UnicodeChars.sup_3, ���\x. x ** 3���) 180 181val GREATER_DEF = new_definition("GREATER_DEF", ���$> m n = n < m���) 182val _ = set_fixity ">" (Infix(NONASSOC, 450)) 183val _ = TeX_notation {hol = ">", TeX = ("\\HOLTokenGt{}", 1)} 184val _ = ot ">" 185 186val LESS_OR_EQ = new_definition ("LESS_OR_EQ", ���$<= m n = m < n \/ (m = n)���) 187val _ = set_fixity "<=" (Infix(NONASSOC, 450)) 188val _ = Unicode.unicode_version { u = Unicode.UChar.leq, tmnm = "<="} 189val _ = TeX_notation {hol = Unicode.UChar.leq, TeX = ("\\HOLTokenLeq{}", 1)} 190val _ = TeX_notation {hol = "<=", TeX = ("\\HOLTokenLeq{}", 1)} 191val _ = ot "<=" 192 193val GREATER_OR_EQ = 194 new_definition("GREATER_OR_EQ", ���$>= m n = m > n \/ (m = n)���) 195val _ = set_fixity ">=" (Infix(NONASSOC, 450)) 196val _ = Unicode.unicode_version { u = Unicode.UChar.geq, tmnm = ">="}; 197val _ = TeX_notation {hol = ">=", TeX = ("\\HOLTokenGeq{}", 1)} 198val _ = TeX_notation {hol = Unicode.UChar.geq, TeX = ("\\HOLTokenGeq{}", 1)} 199val _ = ot ">=" 200 201val EVEN = new_recursive_definition 202 {name = "EVEN", 203 rec_axiom = num_Axiom, 204 def = ���(EVEN 0 = T) /\ 205 (EVEN (SUC n) = ~EVEN n)���}; 206val _ = ot0 "EVEN" "even" 207 208val ODD = new_recursive_definition 209 {name = "ODD", 210 rec_axiom = num_Axiom, 211 def = ���(ODD 0 = F) /\ 212 (ODD (SUC n) = ~ODD n)���}; 213val _ = ot0 "ODD" "odd" 214 215val [num_case_def] = Prim_rec.define_case_constant num_Axiom 216val _ = overload_on("case", ���num_CASE���) 217 218val FUNPOW = new_recursive_definition 219 {name = "FUNPOW", 220 rec_axiom = num_Axiom, 221 def = ���(FUNPOW f 0 x = x) /\ 222 (FUNPOW f (SUC n) x = FUNPOW f n (f x))���}; 223 224val NRC = new_recursive_definition { 225 name = "NRC", 226 rec_axiom = num_Axiom, 227 def = ���(NRC R 0 x y = (x = y)) /\ 228 (NRC R (SUC n) x y = ?z. R x z /\ NRC R n z y)���}; 229 230val _ = overload_on ("RELPOW", ���NRC���) 231val _ = overload_on ("NRC", ���NRC���) 232 233(*--------------------------------------------------------------------------- 234 THEOREMS 235 ---------------------------------------------------------------------------*) 236 237val ONE = store_thm ("ONE", ���1 = SUC 0���, 238 REWRITE_TAC [NUMERAL_DEF, BIT1, ALT_ZERO, ADD]); 239 240val TWO = store_thm ("TWO", ���2 = SUC 1���, 241 REWRITE_TAC [NUMERAL_DEF, BIT2, ONE, ADD, ALT_ZERO,BIT1]); 242 243val NORM_0 = store_thm ("NORM_0", ���NUMERAL ZERO = 0���, 244 REWRITE_TAC [NUMERAL_DEF, ALT_ZERO]); 245 246fun INDUCT_TAC g = INDUCT_THEN INDUCTION ASSUME_TAC g; 247 248val EQ_SYM_EQ' = INST_TYPE [alpha |-> Type`:num`] EQ_SYM_EQ; 249 250(*---------------------------------------------------------------------------*) 251(* Definition of num_case more suitable to call-by-value computations *) 252(*---------------------------------------------------------------------------*) 253 254val num_case_compute = store_thm ("num_case_compute", 255 ���!n. num_CASE n (f:'a) g = if n=0 then f else g (PRE n)���, 256 INDUCT_TAC THEN REWRITE_TAC [num_case_def,NOT_SUC,PRE]); 257 258(* --------------------------------------------------------------------- *) 259(* SUC_NOT = |- !n. ~(0 = SUC n) *) 260(* --------------------------------------------------------------------- *) 261 262val SUC_NOT = save_thm ("SUC_NOT", 263 GEN (���n:num���) (NOT_EQ_SYM (SPEC (���n:num���) NOT_SUC))); 264 265val ADD_0 = store_thm ("ADD_0", 266 ���!m. m + 0 = m���, 267 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); 268 269val ADD_SUC = store_thm ("ADD_SUC", 270 ���!m n. SUC(m + n) = (m + SUC n)���, 271 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); 272 273val ADD_CLAUSES = store_thm ("ADD_CLAUSES", 274 ���(0 + m = m) /\ 275 (m + 0 = m) /\ 276 (SUC m + n = SUC(m + n)) /\ 277 (m + SUC n = SUC(m + n))���, 278 REWRITE_TAC[ADD, ADD_0, ADD_SUC]); 279 280val ADD_SYM = store_thm ("ADD_SYM", 281 ���!m n. m + n = n + m���, 282 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_0, ADD, ADD_SUC]); 283 284val ADD_COMM = save_thm ("ADD_COMM", ADD_SYM); 285 286val ADD_ASSOC = store_thm ("ADD_ASSOC", 287 ���!m n p. m + (n + p) = (m + n) + p���, 288 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]); 289 290val num_CASES = store_thm ("num_CASES", 291 ���!m. (m = 0) \/ ?n. m = SUC n���, 292 INDUCT_TAC 293 THEN REWRITE_TAC[NOT_SUC] 294 THEN EXISTS_TAC (���(m:num)���) 295 THEN REWRITE_TAC[]); 296 297val NOT_ZERO_LT_ZERO = store_thm ("NOT_ZERO_LT_ZERO", 298 ���!n. ~(n = 0) = 0 < n���, 299 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `n` num_CASES) THEN 300 REWRITE_TAC [NOT_LESS_0, LESS_0, NOT_SUC]); 301 302val NOT_LT_ZERO_EQ_ZERO = store_thm( 303 "NOT_LT_ZERO_EQ_ZERO[simp]", 304 ���!n. ~(0 < n) <=> (n = 0)���, 305 REWRITE_TAC [GSYM NOT_ZERO_LT_ZERO]); 306 307val LESS_OR_EQ_ALT = store_thm ("LESS_OR_EQ_ALT", 308 ���$<= = RTC (\x y. y = SUC x)���, 309 REWRITE_TAC [FUN_EQ_THM, LESS_OR_EQ, relationTheory.RTC_CASES_TC, LESS_ALT] 310 THEN REPEAT (STRIP_TAC ORELSE EQ_TAC) 311 THEN ASM_REWRITE_TAC []) ; 312 313(* --------------------------------------------------------------------- *) 314(* LESS_ADD proof rewritten: TFM 90.O9.21 *) 315(* --------------------------------------------------------------------- *) 316 317val LESS_ADD = store_thm ("LESS_ADD", 318 ���!m n. n<m ==> ?p. p+n = m���, 319 INDUCT_TAC THEN GEN_TAC THEN 320 REWRITE_TAC[NOT_LESS_0,LESS_THM] THEN 321 REPEAT STRIP_TAC THENL 322 [EXISTS_TAC (���SUC 0���) THEN ASM_REWRITE_TAC[ADD], 323 RES_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN 324 EXISTS_TAC (���SUC p���) THEN REWRITE_TAC [ADD]]); 325 326val transitive_LESS = store_thm( 327 "transitive_LESS[simp]", 328 ���transitive $<���, 329 REWRITE_TAC [relationTheory.TC_TRANSITIVE, LESS_ALT]); 330 331val LESS_TRANS = store_thm ("LESS_TRANS", 332 ���!m n p. (m < n) /\ (n < p) ==> (m < p)���, 333 MATCH_ACCEPT_TAC 334 (REWRITE_RULE [relationTheory.transitive_def] transitive_LESS)) ; 335 336val LESS_ANTISYM = store_thm ("LESS_ANTISYM", 337 ���!m n. ~((m < n) /\ (n < m))���, 338 REPEAT STRIP_TAC 339 THEN IMP_RES_TAC LESS_TRANS 340 THEN IMP_RES_TAC LESS_REFL); 341 342(*--------------------------------------------------------------------------- 343 * |- !m n. SUC m < SUC n = m < n 344 *---------------------------------------------------------------------------*) 345 346val LESS_MONO_REV = save_thm ("LESS_MONO_REV", prim_recTheory.LESS_MONO_REV) ; 347val LESS_MONO_EQ = save_thm ("LESS_MONO_EQ", prim_recTheory.LESS_MONO_EQ) ; 348 349val LESS_EQ_MONO = store_thm ("LESS_EQ_MONO", 350 ���!n m. (SUC n <= SUC m) = (n <= m)���, 351 REWRITE_TAC [LESS_OR_EQ,LESS_MONO_EQ,INV_SUC_EQ]); 352 353val LESS_LESS_SUC = store_thm ("LESS_LESS_SUC", 354 ���!m n. ~((m < n) /\ (n < SUC m))���, 355 INDUCT_TAC THEN INDUCT_TAC THEN 356 ASM_REWRITE_TAC[LESS_MONO_EQ, LESS_EQ_MONO, LESS_0, NOT_LESS_0]) ; 357 358val transitive_measure = Q.store_thm ("transitive_measure", 359 `!f. transitive (measure f)`, 360 SRW_TAC [][relationTheory.transitive_def,prim_recTheory.measure_thm] 361 THEN MATCH_MP_TAC LESS_TRANS 362 THEN SRW_TAC [SatisfySimps.SATISFY_ss][]); 363 364val LESS_EQ = store_thm ("LESS_EQ", 365 ���!m n. (m < n) = (SUC m <= n)���, 366 REWRITE_TAC[LESS_OR_EQ_ALT, LESS_ALT, RTC_IM_TC]) ; 367 368val LESS_OR = store_thm ("LESS_OR", 369 ���!m n. m < n ==> SUC m <= n���, 370 REWRITE_TAC[LESS_EQ]) ; 371 372val LESS_SUC_EQ = LESS_OR; 373 374val OR_LESS = store_thm ("OR_LESS", 375 ���!m n. (SUC m <= n) ==> (m < n)���, 376 REWRITE_TAC[LESS_EQ]) ; 377 378val LESS_EQ_IFF_LESS_SUC = store_thm ("LESS_EQ_IFF_LESS_SUC", 379 ���!n m. (n <= m) = (n < (SUC m))���, 380 REWRITE_TAC[LESS_OR_EQ_ALT, LESS_ALT, TC_IM_RTC_SUC]) ; 381 382val LESS_EQ_IMP_LESS_SUC = store_thm ("LESS_EQ_IMP_LESS_SUC", 383 ���!n m. (n <= m) ==> (n < (SUC m))���, 384 REWRITE_TAC [LESS_EQ_IFF_LESS_SUC]) ; 385 386val ZERO_LESS_EQ = store_thm ("ZERO_LESS_EQ", 387 ���!n. 0 <= n���, 388 REWRITE_TAC [LESS_0,LESS_EQ_IFF_LESS_SUC]); 389 390val LESS_SUC_EQ_COR = store_thm ("LESS_SUC_EQ_COR", 391 ���!m n. ((m < n) /\ (~(SUC m = n))) ==> (SUC m < n)���, 392 CONV_TAC (ONCE_DEPTH_CONV SYM_CONV) THEN 393 INDUCT_TAC THEN INDUCT_TAC THEN 394 ASM_REWRITE_TAC [LESS_MONO_EQ, INV_SUC_EQ, LESS_0, NOT_LESS_0, 395 NOT_ZERO_LT_ZERO]) ; 396 397val LESS_NOT_SUC = store_thm ("LESS_NOT_SUC", 398 ���!m n. (m < n) /\ ~(n = SUC m) ==> SUC m < n���, 399 INDUCT_TAC THEN INDUCT_TAC THEN 400 ASM_REWRITE_TAC [LESS_MONO_EQ, INV_SUC_EQ, LESS_0, NOT_LESS_0, 401 NOT_ZERO_LT_ZERO]) ; 402 403val LESS_0_CASES = store_thm ("LESS_0_CASES", 404 ���!m. (0 = m) \/ 0<m���, 405 INDUCT_TAC 406 THEN REWRITE_TAC[LESS_0]); 407 408val LESS_CASES_IMP = store_thm ("LESS_CASES_IMP", 409 ���!m n. ~(m < n) /\ ~(m = n) ==> (n < m)���, 410 INDUCT_TAC THEN INDUCT_TAC THEN 411 ASM_REWRITE_TAC [LESS_MONO_EQ, INV_SUC_EQ, LESS_0, NOT_LESS_0]) ; 412 413val LESS_CASES = store_thm ("LESS_CASES", 414 ���!m n. (m < n) \/ (n <= m)���, 415 INDUCT_TAC THEN INDUCT_TAC THEN 416 ASM_REWRITE_TAC 417 [LESS_MONO_EQ, LESS_EQ_MONO, ZERO_LESS_EQ, LESS_0, NOT_LESS_0]) ; 418 419val ADD_INV_0 = store_thm ("ADD_INV_0", 420 ���!m n. (m + n = m) ==> (n = 0)���, 421 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES, INV_SUC_EQ]); 422 423val LESS_EQ_ADD = store_thm ("LESS_EQ_ADD", 424 ���!m n. m <= m + n���, 425 GEN_TAC 426 THEN REWRITE_TAC[LESS_OR_EQ] 427 THEN INDUCT_TAC 428 THEN ASM_REWRITE_TAC[ADD_CLAUSES] 429 THEN MP_TAC(ASSUME (���(m < (m + n)) \/ (m = (m + n))���)) 430 THEN STRIP_TAC 431 THENL 432 [IMP_RES_TAC LESS_SUC 433 THEN ASM_REWRITE_TAC[], 434 REWRITE_TAC[SYM(ASSUME (���m = m + n���)),LESS_SUC_REFL]]); 435 436val LESS_EQ_ADD_EXISTS = store_thm ("LESS_EQ_ADD_EXISTS", 437 ���!m n. n<=m ==> ?p. p+n = m���, 438 SIMP_TAC bool_ss [LESS_OR_EQ, DISJ_IMP_THM, FORALL_AND_THM, LESS_ADD] 439 THEN GEN_TAC 440 THEN EXISTS_TAC (���0���) 441 THEN REWRITE_TAC[ADD]); 442 443val LESS_STRONG_ADD = store_thm ("LESS_STRONG_ADD", 444 ���!m n. n < m ==> ?p. (SUC p)+n = m���, 445 REPEAT STRIP_TAC 446 THEN IMP_RES_TAC LESS_OR 447 THEN IMP_RES_TAC LESS_EQ_ADD_EXISTS 448 THEN EXISTS_TAC (���p:num���) 449 THEN FULL_SIMP_TAC bool_ss [ADD_CLAUSES]); 450 451val LESS_EQ_SUC_REFL = store_thm ("LESS_EQ_SUC_REFL", 452 ���!m. m <= SUC m���, 453 GEN_TAC 454 THEN REWRITE_TAC[LESS_OR_EQ,LESS_SUC_REFL]); 455 456val LESS_ADD_NONZERO = store_thm ("LESS_ADD_NONZERO", 457 ���!m n. ~(n = 0) ==> m < m + n���, 458 GEN_TAC 459 THEN INDUCT_TAC 460 THEN REWRITE_TAC[NOT_SUC,ADD_CLAUSES] 461 THEN ASM_CASES_TAC (���n = 0���) 462 THEN ASSUME_TAC(SPEC (���m + n���) LESS_SUC_REFL) 463 THEN RES_TAC 464 THEN IMP_RES_TAC LESS_TRANS 465 THEN ASM_REWRITE_TAC[ADD_CLAUSES,LESS_SUC_REFL]); 466 467val NOT_SUC_LESS_EQ_0 = store_thm ("NOT_SUC_LESS_EQ_0", 468 ���!n. ~(SUC n <= 0)���, 469 REWRITE_TAC [NOT_LESS_0, GSYM LESS_EQ]); 470 471val NOT_LESS = store_thm ("NOT_LESS", 472 ���!m n. ~(m < n) = (n <= m)���, 473 INDUCT_TAC THEN INDUCT_TAC THEN 474 ASM_REWRITE_TAC [LESS_MONO_EQ, LESS_EQ_MONO, 475 ZERO_LESS_EQ, LESS_0, NOT_LESS_0, NOT_SUC_LESS_EQ_0]) ; 476 477val NOT_LESS_EQUAL = store_thm ("NOT_LESS_EQUAL", 478 ���!m n. ~(m <= n) = n < m���, 479 REWRITE_TAC[GSYM NOT_LESS]); 480 481val LESS_EQ_ANTISYM = store_thm ("LESS_EQ_ANTISYM", 482 ���!m n. ~(m < n /\ n <= m)���, 483 INDUCT_TAC THEN INDUCT_TAC THEN 484 ASM_REWRITE_TAC [LESS_MONO_EQ, LESS_EQ_MONO, 485 ZERO_LESS_EQ, LESS_0, NOT_LESS_0, NOT_SUC_LESS_EQ_0]) ; 486 487val LESS_EQ_0 = store_thm ("LESS_EQ_0", 488 ���!n. (n <= 0) = (n = 0)���, 489 REWRITE_TAC [LESS_OR_EQ, NOT_LESS_0]) ; 490 491val _ = print "Now proving properties of subtraction\n" 492 493val SUB_0 = store_thm ("SUB_0", 494 ���!m. (0 - m = 0) /\ (m - 0 = m)���, 495 INDUCT_TAC 496 THEN ASM_REWRITE_TAC[SUB, NOT_LESS_0]); 497 498(* Non-confluence problem between SUB (snd clause) and LESS_MONO_EQ *) 499(* requires a change from hol2 proof. kls. *) 500 501val SUB_MONO_EQ = store_thm ("SUB_MONO_EQ", 502 ���!n m. (SUC n) - (SUC m) = (n - m)���, 503 INDUCT_TAC THENL 504 [REWRITE_TAC [SUB,LESS_0], 505 ONCE_REWRITE_TAC[SUB] THEN 506 PURE_ONCE_REWRITE_TAC[LESS_MONO_EQ] THEN 507 ASM_REWRITE_TAC[]]); 508 509val SUB_EQ_0 = store_thm ("SUB_EQ_0", 510 ���!m n. (m - n = 0) = (m <= n)���, 511 REPEAT INDUCT_TAC THEN 512 ASM_REWRITE_TAC [SUB_0, LESS_EQ_MONO, SUB_MONO_EQ, LESS_EQ_0, ZERO_LESS_EQ]); 513 514val ADD1 = store_thm ("ADD1", 515 ���!m. SUC m = m + 1���, 516 INDUCT_TAC THENL [ 517 REWRITE_TAC [ADD_CLAUSES, ONE], 518 ASM_REWRITE_TAC [] THEN REWRITE_TAC [ONE, ADD_CLAUSES] 519 ]); 520 521val SUC_SUB1 = store_thm ("SUC_SUB1", 522 ���!m. SUC m - 1 = m���, 523 INDUCT_TAC THENL [ 524 REWRITE_TAC [SUB, LESS_0, ONE], 525 PURE_ONCE_REWRITE_TAC[SUB] THEN 526 ASM_REWRITE_TAC[NOT_LESS_0, LESS_MONO_EQ, ONE] 527 ]); 528 529val PRE_SUB1 = store_thm ("PRE_SUB1", 530 ���!m. (PRE m = (m - 1))���, 531 GEN_TAC 532 THEN STRUCT_CASES_TAC(SPEC (���m:num���) num_CASES) 533 THEN ASM_REWRITE_TAC[PRE, CONJUNCT1 SUB, SUC_SUB1]); 534 535val MULT_0 = store_thm ("MULT_0", 536 ���!m. m * 0 = 0���, 537 INDUCT_TAC 538 THEN ASM_REWRITE_TAC[MULT,ADD_CLAUSES]); 539 540val MULT_SUC = store_thm ("MULT_SUC", 541 ���!m n. m * (SUC n) = m + m*n���, 542 INDUCT_TAC 543 THEN ASM_REWRITE_TAC[MULT,ADD_CLAUSES,ADD_ASSOC]); 544 545val MULT_LEFT_1 = store_thm ("MULT_LEFT_1", 546 ���!m. 1 * m = m���, 547 GEN_TAC THEN REWRITE_TAC[ONE, MULT,ADD_CLAUSES]); 548 549val MULT_RIGHT_1 = store_thm ("MULT_RIGHT_1", 550 ���!m. m * 1 = m���, 551 REWRITE_TAC [ONE] THEN INDUCT_TAC THEN 552 ASM_REWRITE_TAC[MULT, ADD_CLAUSES]); 553 554val MULT_CLAUSES = store_thm ("MULT_CLAUSES", 555 ���!m n. (0 * m = 0) /\ 556 (m * 0 = 0) /\ 557 (1 * m = m) /\ 558 (m * 1 = m) /\ 559 (SUC m * n = m * n + n) /\ 560 (m * SUC n = m + m * n)���, 561 REWRITE_TAC[MULT,MULT_0,MULT_LEFT_1,MULT_RIGHT_1,MULT_SUC]); 562 563val MULT_SYM = store_thm ("MULT_SYM", 564 ���!m n. m * n = n * m���, 565 INDUCT_TAC 566 THEN GEN_TAC 567 THEN ASM_REWRITE_TAC[MULT_CLAUSES,SPECL[���m*n���,���n:num���]ADD_SYM]); 568 569val MULT_COMM = save_thm ("MULT_COMM", MULT_SYM); 570 571val RIGHT_ADD_DISTRIB = store_thm ("RIGHT_ADD_DISTRIB", 572 ���!m n p. (m + n) * p = (m * p) + (n * p)���, 573 GEN_TAC 574 THEN GEN_TAC 575 THEN INDUCT_TAC 576 THEN ASM_REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES,ADD_ASSOC] 577 THEN REWRITE_TAC[SPECL[���m+(m*p)���,���n:num���]ADD_SYM,ADD_ASSOC] 578 THEN SUBST_TAC[SPEC_ALL ADD_SYM] 579 THEN REWRITE_TAC[]); 580 581(* A better proof of LEFT_ADD_DISTRIB would be using 582 MULT_SYM and RIGHT_ADD_DISTRIB *) 583val LEFT_ADD_DISTRIB = store_thm ("LEFT_ADD_DISTRIB", 584 ���!m n p. p * (m + n) = (p * m) + (p * n)���, 585 GEN_TAC 586 THEN GEN_TAC 587 THEN INDUCT_TAC 588 THEN ASM_REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES,SYM(SPEC_ALL ADD_ASSOC)] 589 THEN REWRITE_TAC[SPECL[���m:num���,���(p*n)+n���]ADD_SYM, 590 SYM(SPEC_ALL ADD_ASSOC)] 591 THEN SUBST_TAC[SPEC_ALL ADD_SYM] 592 THEN REWRITE_TAC[]); 593 594val MULT_ASSOC = store_thm ("MULT_ASSOC", 595 ���!m n p. m * (n * p) = (m * n) * p���, 596 INDUCT_TAC 597 THEN ASM_REWRITE_TAC[MULT_CLAUSES,RIGHT_ADD_DISTRIB]); 598 599val SUB_ADD = store_thm ("SUB_ADD", 600 ���!m n. (n <= m) ==> ((m - n) + n = m)���, 601 REPEAT INDUCT_TAC THEN 602 ASM_REWRITE_TAC[ADD_CLAUSES, SUB_0, SUB_MONO_EQ, LESS_EQ_MONO, 603 INV_SUC_EQ, LESS_EQ_0]) ; 604 605val PRE_SUB = store_thm ("PRE_SUB", 606 ���!m n. PRE(m - n) = (PRE m) - n���, 607 INDUCT_TAC 608 THEN GEN_TAC 609 THEN ASM_REWRITE_TAC[SUB,PRE] 610 THEN ASM_CASES_TAC (���m < n���) 611 THEN ASM_REWRITE_TAC 612 [PRE,LESS_OR_EQ, 613 SUBS[SPECL[���m-n���,���0���]EQ_SYM_EQ'] 614 (SPECL [���m:num���,���n:num���] SUB_EQ_0)]) 615 616val ADD_EQ_0 = store_thm ("ADD_EQ_0", 617 ���!m n. (m + n = 0) = (m = 0) /\ (n = 0)���, 618 INDUCT_TAC 619 THEN GEN_TAC 620 THEN ASM_REWRITE_TAC[ADD_CLAUSES,NOT_SUC]); 621 622val ADD_EQ_1 = store_thm ("ADD_EQ_1", 623 ���!m n. (m + n = 1) = (m = 1) /\ (n = 0) \/ (m = 0) /\ (n = 1)���, 624 INDUCT_TAC THENL [ 625 REWRITE_TAC [ADD_CLAUSES, ONE, GSYM NOT_SUC], 626 REWRITE_TAC [NOT_SUC, ADD_CLAUSES, ONE, INV_SUC_EQ, ADD_EQ_0] 627 ]); 628 629val ADD_INV_0_EQ = store_thm ("ADD_INV_0_EQ", 630 ���!m n. (m + n = m) = (n = 0)���, 631 REPEAT GEN_TAC 632 THEN EQ_TAC 633 THEN REWRITE_TAC[ADD_INV_0] 634 THEN STRIP_TAC 635 THEN ASM_REWRITE_TAC[ADD_CLAUSES]); 636 637val PRE_SUC_EQ = store_thm ("PRE_SUC_EQ", 638 ���!m n. 0<n ==> ((m = PRE n) = (SUC m = n))���, 639 INDUCT_TAC 640 THEN INDUCT_TAC 641 THEN REWRITE_TAC[PRE,LESS_REFL,INV_SUC_EQ]); 642 643val INV_PRE_EQ = store_thm ("INV_PRE_EQ", 644 ���!m n. 0<m /\ 0<n ==> ((PRE m = (PRE n)) = (m = n))���, 645 INDUCT_TAC 646 THEN INDUCT_TAC 647 THEN REWRITE_TAC[PRE,LESS_REFL,INV_SUC_EQ]); 648 649val LESS_SUC_NOT = store_thm ("LESS_SUC_NOT", 650 ���!m n. (m < n) ==> ~(n < SUC m)���, 651 REPEAT GEN_TAC 652 THEN ASM_REWRITE_TAC[NOT_LESS] 653 THEN REPEAT STRIP_TAC 654 THEN IMP_RES_TAC LESS_OR 655 THEN ASM_REWRITE_TAC[]); 656 657val ADD_EQ_SUB = store_thm ("ADD_EQ_SUB", 658 ���!m n p. (n <= p) ==> (((m + n) = p) = (m = (p - n)))���, 659 GEN_TAC THEN REPEAT INDUCT_TAC THEN 660 ASM_REWRITE_TAC [ADD_CLAUSES,SUB_MONO_EQ,INV_SUC_EQ,LESS_EQ_MONO, 661 SUB_0, NOT_SUC_LESS_EQ_0]) ; 662 663val LESS_MONO_ADD = store_thm ("LESS_MONO_ADD", 664 ���!m n p. (m < n) ==> (m + p) < (n + p)���, 665 GEN_TAC 666 THEN GEN_TAC 667 THEN INDUCT_TAC 668 THEN DISCH_TAC 669 THEN RES_TAC 670 THEN ASM_REWRITE_TAC[ADD_CLAUSES,LESS_MONO_EQ]); 671 672val LESS_MONO_ADD_INV = store_thm ("LESS_MONO_ADD_INV", 673 ���!m n p. (m + p) < (n + p) ==> (m < n)���, 674 GEN_TAC 675 THEN GEN_TAC 676 THEN INDUCT_TAC 677 THEN ASM_REWRITE_TAC[ADD_CLAUSES,LESS_MONO_EQ]); 678 679val LESS_MONO_ADD_EQ = store_thm ("LESS_MONO_ADD_EQ", 680 ���!m n p. ((m + p) < (n + p)) = (m < n)���, 681 REPEAT GEN_TAC 682 THEN EQ_TAC 683 THEN REWRITE_TAC[LESS_MONO_ADD,LESS_MONO_ADD_INV]); 684 685val LT_ADD_RCANCEL = save_thm ("LT_ADD_RCANCEL", LESS_MONO_ADD_EQ) 686val LT_ADD_LCANCEL = save_thm ("LT_ADD_LCANCEL", 687 ONCE_REWRITE_RULE [ADD_COMM] LT_ADD_RCANCEL) 688 689val EQ_MONO_ADD_EQ = store_thm ("EQ_MONO_ADD_EQ", 690 ���!m n p. ((m + p) = (n + p)) = (m = n)���, 691 GEN_TAC 692 THEN GEN_TAC 693 THEN INDUCT_TAC 694 THEN ASM_REWRITE_TAC[ADD_CLAUSES,INV_SUC_EQ]); 695 696val _ = print "Proving properties of <=\n" 697 698val LESS_EQ_MONO_ADD_EQ = store_thm ("LESS_EQ_MONO_ADD_EQ", 699 ���!m n p. ((m + p) <= (n + p)) = (m <= n)���, 700 REPEAT GEN_TAC 701 THEN REWRITE_TAC[LESS_OR_EQ] 702 THEN REPEAT STRIP_TAC 703 THEN REWRITE_TAC[LESS_MONO_ADD_EQ,EQ_MONO_ADD_EQ]); 704 705val LESS_EQ_TRANS = store_thm ("LESS_EQ_TRANS", 706 ���!m n p. (m <= n) /\ (n <= p) ==> (m <= p)���, 707 REWRITE_TAC[LESS_OR_EQ_ALT, REWRITE_RULE 708 [relationTheory.transitive_def] relationTheory.transitive_RTC]) ; 709 710val LESS_EQ_LESS_TRANS = store_thm ("LESS_EQ_LESS_TRANS", 711 ���!m n p. m <= n /\ n < p ==> m < p���, 712 REPEAT GEN_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN 713 ASM_CASES_TAC (���m:num = n���) THEN ASM_REWRITE_TAC[LESS_TRANS]); 714 715val LESS_LESS_EQ_TRANS = store_thm ("LESS_LESS_EQ_TRANS", 716 ���!m n p. m < n /\ n <= p ==> m < p���, 717 REPEAT GEN_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN 718 ASM_CASES_TAC (���n:num = p���) THEN ASM_REWRITE_TAC[LESS_TRANS]); 719 720(* % Proof modified for new IMP_RES_TAC [TFM 90.04.25] *) 721 722val LESS_EQ_LESS_EQ_MONO = store_thm ("LESS_EQ_LESS_EQ_MONO", 723 ���!m n p q. (m <= p) /\ (n <= q) ==> ((m + n) <= (p + q))���, 724 REPEAT STRIP_TAC THEN 725 let val th1 = snd(EQ_IMP_RULE (SPEC_ALL LESS_EQ_MONO_ADD_EQ)) 726 val th2 = PURE_ONCE_REWRITE_RULE [ADD_SYM] th1 727 in 728 IMP_RES_THEN (ASSUME_TAC o SPEC (���n:num���)) th1 THEN 729 IMP_RES_THEN (ASSUME_TAC o SPEC (���p:num���)) th2 THEN 730 IMP_RES_TAC LESS_EQ_TRANS 731 end); 732 733val LESS_EQ_REFL = store_thm ("LESS_EQ_REFL", 734 ���!m. m <= m���, 735 GEN_TAC 736 THEN REWRITE_TAC[LESS_OR_EQ]); 737 738val LESS_IMP_LESS_OR_EQ = store_thm ("LESS_IMP_LESS_OR_EQ", 739 ���!m n. (m < n) ==> (m <= n)���, 740 REPEAT STRIP_TAC 741 THEN ASM_REWRITE_TAC[LESS_OR_EQ]); 742 743val LESS_MONO_MULT = store_thm ("LESS_MONO_MULT", 744 ���!m n p. (m <= n) ==> ((m * p) <= (n * p))���, 745 GEN_TAC 746 THEN GEN_TAC 747 THEN INDUCT_TAC 748 THEN DISCH_TAC 749 THEN ASM_REWRITE_TAC 750 [ADD_CLAUSES,MULT_CLAUSES,LESS_EQ_MONO_ADD_EQ,LESS_EQ_REFL] 751 THEN RES_TAC 752 THEN IMP_RES_TAC(SPECL[���m:num���,���m*p���,���n:num���,���n*p���] 753 LESS_EQ_LESS_EQ_MONO) 754 THEN ASM_REWRITE_TAC[]); 755 756val LESS_MONO_MULT2 = store_thm ("LESS_MONO_MULT2", 757 ���!m n i j. m <= i /\ n <= j ==> m * n <= i * j���, 758 mesonLib.MESON_TAC [LESS_EQ_TRANS, LESS_MONO_MULT, MULT_COMM]); 759 760(* Proof modified for new IMP_RES_TAC [TFM 90.04.25] *) 761 762val RIGHT_SUB_DISTRIB = store_thm ("RIGHT_SUB_DISTRIB", 763 ���!m n p. (m - n) * p = (m * p) - (n * p)���, 764 REPEAT GEN_TAC THEN 765 ASM_CASES_TAC (���n <= m���) THENL 766 [let val imp = SPECL [���(m-n)*p���, 767 ���n*p���, 768 ���m*p���] ADD_EQ_SUB 769 in 770 IMP_RES_THEN (SUBST1_TAC o SYM o MP imp o SPEC (���p:num���)) 771 LESS_MONO_MULT THEN 772 REWRITE_TAC[SYM(SPEC_ALL RIGHT_ADD_DISTRIB)] THEN 773 IMP_RES_THEN SUBST1_TAC SUB_ADD THEN REFL_TAC 774 end, 775 IMP_RES_TAC (REWRITE_RULE[](AP_TERM (���$~���) 776 (SPEC_ALL NOT_LESS))) THEN 777 IMP_RES_TAC LESS_IMP_LESS_OR_EQ THEN 778 IMP_RES_THEN (ASSUME_TAC o SPEC (���p:num���)) LESS_MONO_MULT THEN 779 IMP_RES_TAC SUB_EQ_0 THEN 780 ASM_REWRITE_TAC[MULT_CLAUSES]]); 781 782val LEFT_SUB_DISTRIB = store_thm ("LEFT_SUB_DISTRIB", 783 ���!m n p. p * (m - n) = (p * m) - (p * n)���, 784 PURE_ONCE_REWRITE_TAC [MULT_SYM] THEN 785 REWRITE_TAC [RIGHT_SUB_DISTRIB]); 786 787(* The following theorem (and proof) are from tfm [rewritten TFM 90.09.21] *) 788val LESS_ADD_1 = store_thm ("LESS_ADD_1", 789 ���!m n. (n<m) ==> ?p. m = n + (p + 1)���, 790 REWRITE_TAC [ONE] THEN INDUCT_TAC THEN 791 REWRITE_TAC[NOT_LESS_0,LESS_THM] THEN 792 REPEAT STRIP_TAC THENL [ 793 EXISTS_TAC (���0���) THEN ASM_REWRITE_TAC [ADD_CLAUSES], 794 RES_THEN (STRIP_THM_THEN SUBST1_TAC) THEN 795 EXISTS_TAC (���SUC p���) THEN REWRITE_TAC [ADD_CLAUSES] 796]); 797 798(* ---------------------------------------------------------------------*) 799(* The following arithmetic theorems were added by TFM in 88.03.31 *) 800(* *) 801(* These are needed to build the recursive type definition package *) 802(* ---------------------------------------------------------------------*) 803 804val EXP_ADD = store_thm ("EXP_ADD", 805 ���!p q n. n EXP (p+q) = (n EXP p) * (n EXP q)���, 806 INDUCT_TAC THEN 807 ASM_REWRITE_TAC [EXP,ADD_CLAUSES,MULT_CLAUSES,MULT_ASSOC]); 808 809val NOT_ODD_EQ_EVEN = store_thm ("NOT_ODD_EQ_EVEN", 810 ���!n m. ~(SUC(n + n) = (m + m))���, 811 REPEAT (INDUCT_TAC THEN REWRITE_TAC [ADD_CLAUSES]) THENL 812 [MATCH_ACCEPT_TAC NOT_SUC, 813 REWRITE_TAC [INV_SUC_EQ,NOT_EQ_SYM (SPEC_ALL NOT_SUC)], 814 REWRITE_TAC [INV_SUC_EQ,NOT_SUC], 815 ASM_REWRITE_TAC [INV_SUC_EQ]]); 816 817val LESS_EQUAL_ANTISYM = store_thm ("LESS_EQUAL_ANTISYM", 818 ���!n m. n <= m /\ m <= n ==> (n = m)���, 819 REWRITE_TAC [LESS_OR_EQ] THEN 820 REPEAT STRIP_TAC THENL 821 [IMP_RES_TAC LESS_ANTISYM, 822 ASM_REWRITE_TAC[]]); 823 824val LESS_ADD_SUC = store_thm ("LESS_ADD_SUC", 825 ���!m n. m < m + SUC n���, 826 INDUCT_TAC THENL 827 [REWRITE_TAC [LESS_0,ADD_CLAUSES], 828 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [ADD_CLAUSES]) THEN 829 ASM_REWRITE_TAC [LESS_MONO_EQ,ADD_CLAUSES]]); 830 831(* Following proof revised for version 1.12 resolution. [TFM 91.01.18] *) 832val LESS_OR_EQ_ADD = store_thm ("LESS_OR_EQ_ADD", 833 ���!n m. n < m \/ ?p. n = p+m���, 834 REPEAT GEN_TAC THEN ASM_CASES_TAC (���n<m���) THENL 835 [DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC, 836 DISJ2_TAC THEN IMP_RES_TAC NOT_LESS THEN IMP_RES_TAC LESS_OR_EQ THENL 837 [CONV_TAC (ONCE_DEPTH_CONV SYM_CONV) THEN 838 IMP_RES_THEN MATCH_ACCEPT_TAC LESS_ADD, 839 EXISTS_TAC (���0���) THEN ASM_REWRITE_TAC [ADD]]]); 840 841(*----------------------------------------------------------------------*) 842(* Added TFM 88.03.31 *) 843(* *) 844(* Prove the well ordering property: *) 845(* *) 846(* |- !P. (?n. P n) ==> (?n. P n /\ (!m. m < n ==> ~P m)) *) 847(* *) 848(* I.e. considering P to be a set, that is the set of numbers, x , such *) 849(* that P(x), then every non-empty P has a smallest element. *) 850(* *) 851(* We first prove that, if there does NOT exist a smallest n such that *) 852(* P(n) is true, then for all n P is false of all numbers smaller than n.*) 853(* The main step is an induction on n. *) 854(*----------------------------------------------------------------------*) 855 856val lemma = TAC_PROOF(([], 857 ���(~?n. P n /\ !m. (m<n) ==> ~P m) ==> (!n m. (m<n) ==> ~P m)���), 858 CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) THEN 859 DISCH_TAC THEN 860 INDUCT_TAC THEN 861 REWRITE_TAC [NOT_LESS_0,LESS_THM] THEN 862 REPEAT (FILTER_STRIP_TAC (���P:num->bool���)) THENL 863 [POP_ASSUM SUBST1_TAC THEN DISCH_TAC,ALL_TAC] THEN 864 RES_TAC); 865 866(* We now prove the well ordering property. *) 867val WOP = store_thm ("WOP", 868 ���!P. (?n.P n) ==> (?n. P n /\ (!m. (m<n) ==> ~P m))���, 869 GEN_TAC THEN 870 CONV_TAC CONTRAPOS_CONV THEN 871 DISCH_THEN (ASSUME_TAC o MP lemma) THEN 872 CONV_TAC NOT_EXISTS_CONV THEN 873 GEN_TAC THEN 874 POP_ASSUM (MATCH_MP_TAC o SPECL [���SUC n���,���n:num���]) THEN 875 MATCH_ACCEPT_TAC LESS_SUC_REFL); 876 877val COMPLETE_INDUCTION = store_thm ("COMPLETE_INDUCTION", 878 ���!P. (!n. (!m. m < n ==> P m) ==> P n) ==> !n. P n���, 879 let val wopeta = CONV_RULE(ONCE_DEPTH_CONV ETA_CONV) WOP 880 in 881 GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN 882 CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN 883 DISCH_THEN(MP_TAC o MATCH_MP wopeta) THEN BETA_TAC THEN 884 REWRITE_TAC[NOT_IMP] THEN DISCH_THEN(X_CHOOSE_TAC (���n:num���)) THEN 885 EXISTS_TAC (���n:num���) THEN ASM_REWRITE_TAC[] 886 end); 887 888val FORALL_NUM_THM = Q.store_thm ("FORALL_NUM_THM", 889 `(!n. P n) = P 0 /\ !n. P n ==> P (SUC n)`, 890 METIS_TAC [INDUCTION]); 891 892(* ---------------------------------------------------------------------*) 893(* Some more theorems, mostly about subtraction. *) 894(* ---------------------------------------------------------------------*) 895 896val SUC_SUB = store_thm( 897 "SUC_SUB[simp]", 898 ���!a. SUC a - a = 1���, 899 INDUCT_TAC THENL [ 900 REWRITE_TAC [SUB, LESS_REFL, ONE], 901 ASM_REWRITE_TAC [SUB_MONO_EQ] 902 ]); 903 904val SUB_PLUS = store_thm ("SUB_PLUS", 905 ���!a b c. a - (b + c) = (a - b) - c���, 906 REPEAT INDUCT_TAC THEN 907 REWRITE_TAC [SUB_0,ADD_CLAUSES,SUB_MONO_EQ] THEN 908 PURE_ONCE_REWRITE_TAC [SYM (el 4 (CONJUNCTS ADD_CLAUSES))] THEN 909 PURE_ONCE_ASM_REWRITE_TAC [] THEN REFL_TAC); 910 911(* Statement of thm changed. 912**val INV_PRE_LESS = store_thm ("INV_PRE_LESS", 913** ���!m n. 0 < m /\ 0 < n ==> ((PRE m < PRE n) = (m < n))���, 914** REPEAT INDUCT_TAC THEN 915** REWRITE_TAC[LESS_REFL,SUB,LESS_0,PRE] THEN 916** MATCH_ACCEPT_TAC (SYM(SPEC_ALL LESS_MONO_EQ))); 917*) 918val INV_PRE_LESS = store_thm ("INV_PRE_LESS", 919 ���!m. 0 < m ==> !n. PRE m < PRE n = m < n���, 920 REPEAT (INDUCT_TAC THEN TRY DISCH_TAC) THEN 921 REWRITE_TAC[LESS_REFL,SUB,LESS_0,PRE,NOT_LESS_0] THEN 922 IMP_RES_TAC LESS_REFL THEN 923 MATCH_ACCEPT_TAC (SYM(SPEC_ALL LESS_MONO_EQ))); 924 925val INV_PRE_LESS_EQ = store_thm ("INV_PRE_LESS_EQ", 926 ���!n. 0 < n ==> !m. ((PRE m <= PRE n) = (m <= n))���, 927 INDUCT_TAC THEN 928 REWRITE_TAC [LESS_REFL,LESS_0,PRE] THEN 929 INDUCT_TAC THEN 930 REWRITE_TAC [PRE,ZERO_LESS_EQ] THEN 931 REWRITE_TAC [ADD1,LESS_EQ_MONO_ADD_EQ]); 932 933val PRE_LESS_EQ = Q.store_thm ("PRE_LESS_EQ", 934 `!n. m <= n ==> PRE m <= PRE n`, 935 INDUCT_TAC THEN1 936 (REWRITE_TAC [LESS_EQ_0] THEN DISCH_TAC THEN 937 ASM_REWRITE_TAC [LESS_EQ_REFL]) THEN 938 VALIDATE (CONV_TAC (DEPTH_CONV 939 (REWR_CONV_A (SPEC_ALL (UNDISCH (SPEC_ALL INV_PRE_LESS_EQ)))))) THEN 940 REWRITE_TAC [LESS_0]) ; 941 942val SUB_LESS_EQ = store_thm ("SUB_LESS_EQ", 943 ���!n m. (n - m) <= n���, 944 REWRITE_TAC [SYM(SPEC_ALL SUB_EQ_0),SYM(SPEC_ALL SUB_PLUS)] THEN 945 CONV_TAC (ONCE_DEPTH_CONV (REWR_CONV ADD_SYM)) THEN 946 REWRITE_TAC [SUB_EQ_0,LESS_EQ_ADD]); 947 948val SUB_EQ_EQ_0 = store_thm ("SUB_EQ_EQ_0", 949 ���!m n. (m - n = m) = ((m = 0) \/ (n = 0))���, 950 REPEAT INDUCT_TAC THEN 951 REWRITE_TAC [SUB_0,NOT_SUC] THEN 952 REWRITE_TAC [SUB] THEN 953 ASM_CASES_TAC (���m<SUC n���) THENL 954 [CONV_TAC (ONCE_DEPTH_CONV SYM_CONV) THEN ASM_REWRITE_TAC [NOT_SUC], 955 ASM_REWRITE_TAC [INV_SUC_EQ,NOT_SUC] THEN 956 IMP_RES_THEN (ASSUME_TAC o MATCH_MP OR_LESS) NOT_LESS THEN 957 IMP_RES_THEN (STRIP_THM_THEN SUBST1_TAC) LESS_ADD_1 THEN 958 REWRITE_TAC [ONE, ADD_CLAUSES, NOT_SUC]]); 959 960val SUB_LESS_0 = store_thm ("SUB_LESS_0", 961 ���!n m. (m < n) = 0 < (n - m)���, 962 REPEAT STRIP_TAC THEN EQ_TAC THENL 963 [DISCH_THEN (STRIP_THM_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN 964 REWRITE_TAC [ONE,ADD_CLAUSES,SUB] THEN 965 REWRITE_TAC [REWRITE_RULE [SYM(SPEC_ALL NOT_LESS)] LESS_EQ_ADD,LESS_0], 966 CONV_TAC CONTRAPOS_CONV THEN 967 REWRITE_TAC [NOT_LESS,LESS_OR_EQ,NOT_LESS_0,SUB_EQ_0]]); 968 969val SUB_LESS_OR = store_thm ("SUB_LESS_OR", 970 ���!m n. n < m ==> n <= (m - 1)���, 971 REPEAT GEN_TAC THEN 972 DISCH_THEN (STRIP_THM_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN 973 REWRITE_TAC [SYM (SPEC_ALL PRE_SUB1)] THEN 974 REWRITE_TAC [PRE,ONE,ADD_CLAUSES,LESS_EQ_ADD]); 975 976val LESS_SUB_ADD_LESS = store_thm ("LESS_SUB_ADD_LESS", 977 ���!n m i. (i < (n - m)) ==> ((i + m) < n)���, 978 INDUCT_TAC THENL 979 [REWRITE_TAC [SUB_0,NOT_LESS_0], 980 REWRITE_TAC [SUB] THEN REPEAT GEN_TAC THEN 981 ASM_CASES_TAC (���n < m���) THEN 982 ASM_REWRITE_TAC [NOT_LESS_0,LESS_THM] THEN 983 let fun tac th g = SUBST1_TAC th g 984 handle _ => ASSUME_TAC th g 985 in 986 DISCH_THEN (STRIP_THM_THEN tac) 987 end THENL 988 [DISJ1_TAC THEN MATCH_MP_TAC SUB_ADD THEN 989 ASM_REWRITE_TAC [SYM(SPEC_ALL NOT_LESS)], 990 RES_TAC THEN ASM_REWRITE_TAC[]]]); 991 992val TIMES2 = store_thm ("TIMES2", 993 ���!n. 2 * n = n + n���, 994 REWRITE_TAC [MULT_CLAUSES, NUMERAL_DEF, BIT2, ADD_CLAUSES,ALT_ZERO]); 995 996val LESS_MULT_MONO = store_thm ("LESS_MULT_MONO", 997 ���!m i n. ((SUC n) * m) < ((SUC n) * i) = (m < i)���, 998 REWRITE_TAC [MULT_CLAUSES] THEN 999 INDUCT_TAC THENL 1000 [INDUCT_TAC THEN REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES,LESS_0], 1001 INDUCT_TAC THENL 1002 [REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES,NOT_LESS_0], 1003 INDUCT_TAC THENL 1004 [REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES], 1005 REWRITE_TAC [LESS_MONO_EQ,ADD_CLAUSES,MULT_CLAUSES] THEN 1006 REWRITE_TAC [SYM(SPEC_ALL ADD_ASSOC)] THEN 1007 PURE_ONCE_REWRITE_TAC [ADD_SYM] THEN 1008 REWRITE_TAC [LESS_MONO_ADD_EQ] THEN 1009 REWRITE_TAC [ADD_ASSOC] THEN 1010 let val th = SYM(el 5 (CONJUNCTS(SPEC_ALL MULT_CLAUSES))) 1011 in 1012 PURE_ONCE_REWRITE_TAC [th] 1013 end THEN 1014 ASM_REWRITE_TAC[]]]]); 1015 1016val MULT_MONO_EQ = store_thm ("MULT_MONO_EQ", 1017 ���!m i n. (((SUC n) * m) = ((SUC n) * i)) = (m = i)���, 1018 REWRITE_TAC [MULT_CLAUSES] THEN 1019 INDUCT_TAC THENL 1020 [INDUCT_TAC THEN 1021 REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES, NOT_EQ_SYM(SPEC_ALL NOT_SUC)], 1022 INDUCT_TAC THENL 1023 [REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES,NOT_SUC], 1024 INDUCT_TAC THENL 1025 [REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES], 1026 REWRITE_TAC [INV_SUC_EQ,ADD_CLAUSES,MULT_CLAUSES] THEN 1027 REWRITE_TAC [SYM(SPEC_ALL ADD_ASSOC)] THEN 1028 PURE_ONCE_REWRITE_TAC [ADD_SYM] THEN 1029 REWRITE_TAC [EQ_MONO_ADD_EQ] THEN 1030 REWRITE_TAC [ADD_ASSOC] THEN 1031 let val th = SYM(el 5 (CONJUNCTS(SPEC_ALL MULT_CLAUSES))) 1032 in 1033 PURE_ONCE_REWRITE_TAC [th] 1034 end THEN 1035 ASM_REWRITE_TAC[]]]]); 1036 1037val MULT_SUC_EQ = store_thm ("MULT_SUC_EQ", 1038 ���!p m n. ((n * (SUC p)) = (m * (SUC p))) = (n = m)���, 1039 ONCE_REWRITE_TAC [MULT_COMM] THEN REWRITE_TAC [MULT_MONO_EQ]) ; 1040 1041val MULT_EXP_MONO = store_thm ("MULT_EXP_MONO", 1042 ���!p q n m.((n * ((SUC q) EXP p)) = (m * ((SUC q) EXP p))) = (n = m)���, 1043 INDUCT_TAC THENL 1044 [REWRITE_TAC [EXP,MULT_CLAUSES,ADD_CLAUSES], 1045 ASM_REWRITE_TAC [EXP,MULT_ASSOC,MULT_SUC_EQ]]); 1046 1047val EQ_ADD_LCANCEL = store_thm ("EQ_ADD_LCANCEL", 1048 ���!m n p. (m + n = m + p) = (n = p)���, 1049 INDUCT_TAC THEN ASM_REWRITE_TAC [ADD_CLAUSES, INV_SUC_EQ]); 1050 1051val EQ_ADD_RCANCEL = store_thm ("EQ_ADD_RCANCEL", 1052 ���!m n p. (m + p = n + p) = (m = n)���, 1053 ONCE_REWRITE_TAC[ADD_COMM] THEN MATCH_ACCEPT_TAC EQ_ADD_LCANCEL); 1054 1055val EQ_MULT_LCANCEL = store_thm ("EQ_MULT_LCANCEL[simp]", 1056 ���!m n p. (m * n = m * p) = (m = 0) \/ (n = p)���, 1057 INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES, NOT_SUC] THEN 1058 REPEAT INDUCT_TAC THEN 1059 ASM_REWRITE_TAC[MULT_CLAUSES, ADD_CLAUSES, GSYM NOT_SUC, NOT_SUC] THEN 1060 ASM_REWRITE_TAC[INV_SUC_EQ, GSYM ADD_ASSOC, EQ_ADD_LCANCEL]); 1061 1062val EQ_MULT_RCANCEL = store_thm( 1063 "EQ_MULT_RCANCEL[simp]", 1064 ���!m n p. (n * m = p * m) <=> (m = 0) \/ (n = p)���, 1065 ONCE_REWRITE_TAC [MULT_COMM] THEN REWRITE_TAC [EQ_MULT_LCANCEL]); 1066 1067val ADD_SUB = store_thm ("ADD_SUB", 1068 ���!a c. (a + c) - c = a���, 1069 GEN_TAC THEN INDUCT_TAC THEN 1070 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ]) ; 1071 1072val LESS_EQ_ADD_SUB = store_thm ("LESS_EQ_ADD_SUB", 1073 ���!c b. (c <= b) ==> !a. (((a + b) - c) = (a + (b - c)))���, 1074 REPEAT INDUCT_TAC THEN 1075 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ, 1076 NOT_SUC_LESS_EQ_0, LESS_EQ_MONO]) ; 1077 1078(* ---------------------------------------------------------------------*) 1079(* SUB_EQUAL_0 = |- !c. c - c = 0 *) 1080(* ---------------------------------------------------------------------*) 1081 1082val _ = print "More properties of subtraction...\n" 1083 1084val SUB_EQUAL_0 = save_thm ("SUB_EQUAL_0", 1085 REWRITE_RULE [ADD_CLAUSES] (SPEC (���0���) ADD_SUB)); 1086 1087val LESS_EQ_SUB_LESS = store_thm ("LESS_EQ_SUB_LESS", 1088 ���!a b. (b <= a) ==> !c. ((a - b) < c) = (a < (b + c))���, 1089 REPEAT INDUCT_TAC THEN 1090 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ, 1091 NOT_SUC_LESS_EQ_0, LESS_EQ_MONO, LESS_MONO_EQ]) ; 1092 1093val NOT_SUC_LESS_EQ = store_thm ("NOT_SUC_LESS_EQ", 1094 ���!n m.~(SUC n <= m) = (m <= n)���, 1095 REWRITE_TAC [SYM (SPEC_ALL LESS_EQ),NOT_LESS]); 1096 1097val SUB_SUB = store_thm ("SUB_SUB", 1098 ���!b c. (c <= b) ==> !a. ((a - (b - c)) = ((a + c) - b))���, 1099 REPEAT INDUCT_TAC THEN 1100 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ, 1101 NOT_SUC_LESS_EQ_0, LESS_EQ_MONO]) ; 1102 1103val LESS_IMP_LESS_ADD = store_thm ("LESS_IMP_LESS_ADD", 1104 ���!n m. n < m ==> !p. n < (m + p)���, 1105 REPEAT GEN_TAC THEN 1106 DISCH_THEN (STRIP_THM_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN 1107 REWRITE_TAC [SYM(SPEC_ALL ADD_ASSOC), ONE] THEN 1108 PURE_ONCE_REWRITE_TAC [ADD_CLAUSES] THEN 1109 PURE_ONCE_REWRITE_TAC [ADD_CLAUSES] THEN 1110 GEN_TAC THEN MATCH_ACCEPT_TAC LESS_ADD_SUC); 1111 1112val SUB_LESS_EQ_ADD = store_thm ("SUB_LESS_EQ_ADD", 1113 ���!m p. (m <= p) ==> !n. (((p - m) <= n) = (p <= (m + n)))���, 1114 REPEAT INDUCT_TAC THEN 1115 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ, 1116 NOT_SUC_LESS_EQ_0, LESS_EQ_MONO]) ; 1117 1118val SUB_LESS_SUC = store_thm ("SUB_LESS_SUC", 1119 ���!p m. p - m < SUC p���, 1120 REPEAT GEN_TAC THEN 1121 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN 1122 Q.EXISTS_TAC `p` THEN CONJ_TAC 1123 THENL [ MATCH_ACCEPT_TAC SUB_LESS_EQ, 1124 MATCH_ACCEPT_TAC LESS_SUC_REFL]) ; 1125 1126val SUB_NE_SUC = MATCH_MP LESS_NOT_EQ (SPEC_ALL SUB_LESS_SUC) ; 1127val SUB_LE_SUC = MATCH_MP LESS_IMP_LESS_OR_EQ (SPEC_ALL SUB_LESS_SUC) ; 1128 1129val SUB_CANCEL = store_thm ("SUB_CANCEL", 1130 ���!p n m. ((n <= p) /\ (m <= p)) ==> (((p - n) = (p - m)) = (n = m))���, 1131 REPEAT INDUCT_TAC THEN 1132 ASM_REWRITE_TAC [SUB_0, ZERO_LESS_EQ, SUB_MONO_EQ, LESS_EQ_MONO, INV_SUC_EQ, 1133 NOT_SUC_LESS_EQ_0, NOT_SUC, GSYM NOT_SUC, SUB_NE_SUC, GSYM SUB_NE_SUC]) ; 1134 1135val CANCEL_SUB = store_thm ("CANCEL_SUB", 1136 ���!p n m.((p <= n) /\ (p <= m)) ==> (((n - p) = (m - p)) = (n = m))���, 1137 REPEAT INDUCT_TAC THEN 1138 ASM_REWRITE_TAC [SUB_0, ZERO_LESS_EQ, SUB_MONO_EQ, LESS_EQ_MONO, INV_SUC_EQ, 1139 NOT_SUC_LESS_EQ_0]) ; 1140 1141val NOT_EXP_0 = store_thm ("NOT_EXP_0", 1142 ���!m n. ~(((SUC n) EXP m) = 0)���, 1143 INDUCT_TAC THEN REWRITE_TAC [EXP] THENL 1144 [REWRITE_TAC [NOT_SUC, ONE], 1145 STRIP_TAC THEN 1146 let val th = (SYM(el 2 (CONJUNCTS (SPECL [���SUC n���,���1���] 1147 MULT_CLAUSES)))) 1148 in 1149 SUBST1_TAC th 1150 end THEN REWRITE_TAC [MULT_MONO_EQ] THEN 1151 FIRST_ASSUM MATCH_ACCEPT_TAC]); 1152 1153val ZERO_LESS_EXP = store_thm ("ZERO_LESS_EXP", 1154 ���!m n. 0 < ((SUC n) EXP m)���, 1155 REPEAT STRIP_TAC THEN 1156 let val th = SPEC (���(SUC n) EXP m���) LESS_0_CASES 1157 fun tac th g = ASSUME_TAC (SYM th) g 1158 handle _ => ACCEPT_TAC th g 1159 in 1160 STRIP_THM_THEN tac th THEN 1161 IMP_RES_TAC NOT_EXP_0 1162 end); 1163 1164val ODD_OR_EVEN = store_thm ("ODD_OR_EVEN", 1165 ���!n. ?m. (n = (SUC(SUC 0) * m)) \/ (n = ((SUC(SUC 0) * m) + 1))���, 1166 REWRITE_TAC [ONE] THEN 1167 INDUCT_THEN INDUCTION STRIP_ASSUME_TAC THENL 1168 [EXISTS_TAC (���0���) THEN REWRITE_TAC [ADD_CLAUSES,MULT_CLAUSES], 1169 EXISTS_TAC (���m:num���) THEN ASM_REWRITE_TAC[ADD_CLAUSES], 1170 EXISTS_TAC (���SUC m���) THEN ASM_REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES]]); 1171 1172val LESS_EXP_SUC_MONO = store_thm ("LESS_EXP_SUC_MONO", 1173 ���!n m.((SUC(SUC m)) EXP n) < ((SUC(SUC m)) EXP (SUC n))���, 1174 INDUCT_TAC THEN PURE_ONCE_REWRITE_TAC [EXP] THENL 1175 [REWRITE_TAC [EXP,ADD_CLAUSES,MULT_CLAUSES,ONE,LESS_0, LESS_MONO_EQ], 1176 ASM_REWRITE_TAC [LESS_MULT_MONO]]); 1177 1178(*---------------------------------------------------------------------------*) 1179(* More arithmetic theorems, mainly concerning orderings [JRH 92.07.14] *) 1180(*---------------------------------------------------------------------------*) 1181 1182val LESS_LESS_CASES = store_thm ("LESS_LESS_CASES", 1183 ���!m n. (m = n) \/ (m < n) \/ (n < m)���, 1184 let val th = REWRITE_RULE[LESS_OR_EQ] 1185 (SPECL[(���m:num���), (���n:num���)] LESS_CASES) 1186 in REPEAT GEN_TAC THEN 1187 REPEAT_TCL DISJ_CASES_THEN (fn t => REWRITE_TAC[t]) th 1188 end); 1189 1190val GREATER_EQ = store_thm ("GREATER_EQ", 1191 ���!n m. n >= m = m <= n���, 1192 REPEAT GEN_TAC THEN REWRITE_TAC[GREATER_OR_EQ, GREATER_DEF, LESS_OR_EQ] THEN 1193 AP_TERM_TAC THEN MATCH_ACCEPT_TAC EQ_SYM_EQ); 1194 1195val LESS_EQ_CASES = store_thm ("LESS_EQ_CASES", 1196 ���!m n. m <= n \/ n <= m���, 1197 REPEAT GEN_TAC THEN 1198 DISJ_CASES_THEN2 (ASSUME_TAC o MATCH_MP LESS_IMP_LESS_OR_EQ) ASSUME_TAC 1199 (SPECL [(���m:num���), (���n:num���)] LESS_CASES) THEN ASM_REWRITE_TAC[]); 1200 1201val LESS_EQUAL_ADD = store_thm ("LESS_EQUAL_ADD", 1202 ���!m n. m <= n ==> ?p. n = m + p���, 1203 REPEAT GEN_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN 1204 DISCH_THEN(DISJ_CASES_THEN2 MP_TAC SUBST1_TAC) THENL 1205 [MATCH_ACCEPT_TAC(GSYM (ONCE_REWRITE_RULE[ADD_SYM] LESS_ADD)), 1206 EXISTS_TAC (���0���) THEN REWRITE_TAC[ADD_CLAUSES]]); 1207 1208val LESS_EQ_EXISTS = store_thm ("LESS_EQ_EXISTS", 1209 ���!m n. m <= n = ?p. n = m + p���, 1210 REPEAT GEN_TAC THEN EQ_TAC THENL 1211 [MATCH_ACCEPT_TAC LESS_EQUAL_ADD, 1212 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN MATCH_ACCEPT_TAC LESS_EQ_ADD]); 1213 1214val MULT_EQ_0 = store_thm ("MULT_EQ_0", 1215 ���!m n. (m * n = 0) = (m = 0) \/ (n = 0)���, 1216 REPEAT GEN_TAC THEN 1217 MAP_EVERY (STRUCT_CASES_TAC o C SPEC num_CASES) [(���m:num���),(���n:num���)] 1218 THEN REWRITE_TAC[MULT_CLAUSES, ADD_CLAUSES, NOT_SUC]); 1219 1220val MULT_EQ_1 = store_thm ("MULT_EQ_1", 1221 ���!x y. (x * y = 1) = (x = 1) /\ (y = 1)���, 1222 REPEAT GEN_TAC THEN 1223 MAP_EVERY (STRUCT_CASES_TAC o C SPEC num_CASES) 1224 [(���x:num���),(���y:num���)] THEN 1225 REWRITE_TAC[MULT_CLAUSES, ADD_CLAUSES, ONE, GSYM SUC_ID, INV_SUC_EQ, 1226 ADD_EQ_0,MULT_EQ_0] THEN EQ_TAC THEN STRIP_TAC THEN 1227 ASM_REWRITE_TAC[]); 1228 1229val MULT_EQ_ID = store_thm ("MULT_EQ_ID", 1230 ���!m n. (m * n = n) = (m=1) \/ (n=0)���, 1231 REPEAT GEN_TAC THEN 1232 STRUCT_CASES_TAC (SPEC ���m:num��� num_CASES) THEN 1233 REWRITE_TAC [MULT_CLAUSES,ONE,GSYM NOT_SUC,INV_SUC_EQ] THENL 1234 [METIS_TAC[], METIS_TAC [ADD_INV_0_EQ,MULT_EQ_0,ADD_SYM]]); 1235 1236val LESS_MULT2 = store_thm ("LESS_MULT2", 1237 ���!m n. 0 < m /\ 0 < n ==> 0 < (m * n)���, 1238 REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN 1239 REWRITE_TAC[NOT_LESS, LESS_EQ_0, DE_MORGAN_THM, MULT_EQ_0]); 1240 1241val ZERO_LESS_MULT = store_thm ("ZERO_LESS_MULT", 1242 ���!m n. 0 < m * n = 0 < m /\ 0 < n���, 1243 REPEAT GEN_TAC THEN 1244 Q.SPEC_THEN `m` STRUCT_CASES_TAC num_CASES THEN 1245 REWRITE_TAC [MULT_CLAUSES, LESS_REFL, LESS_0] THEN 1246 Q.SPEC_THEN `n` STRUCT_CASES_TAC num_CASES THEN 1247 REWRITE_TAC [MULT_CLAUSES, LESS_REFL, LESS_0, ADD_CLAUSES]); 1248 1249val ZERO_LESS_ADD = store_thm ("ZERO_LESS_ADD", 1250 ���!m n. 0 < m + n = 0 < m \/ 0 < n���, 1251 REPEAT GEN_TAC THEN 1252 Q.SPEC_THEN `m` STRUCT_CASES_TAC num_CASES THEN 1253 REWRITE_TAC [ADD_CLAUSES, LESS_REFL, LESS_0]); 1254 1255(*---------------------------------------------------------------------------*) 1256(* Single theorem about the factorial function [JRH 92.07.14] *) 1257(*---------------------------------------------------------------------------*) 1258 1259val FACT = new_recursive_definition 1260 {name = "FACT", 1261 rec_axiom = num_Axiom, 1262 def = ���(FACT 0 = 1) /\ 1263 (FACT (SUC n) = (SUC n) * FACT(n))���}; 1264 1265val FACT_LESS = store_thm ("FACT_LESS", 1266 ���!n. 0 < FACT n���, 1267 INDUCT_TAC THEN REWRITE_TAC[FACT, ONE, LESS_SUC_REFL] THEN 1268 MATCH_MP_TAC LESS_MULT2 THEN ASM_REWRITE_TAC[LESS_0]); 1269 1270(*---------------------------------------------------------------------------*) 1271(* Theorems about evenness and oddity [JRH 92.07.14] *) 1272(*---------------------------------------------------------------------------*) 1273 1274val _ = print "Theorems about evenness and oddity\n" 1275val EVEN_ODD = store_thm ("EVEN_ODD", 1276 ���!n. EVEN n = ~ODD n���, 1277 INDUCT_TAC THEN ASM_REWRITE_TAC[EVEN, ODD]); 1278 1279val ODD_EVEN = store_thm ("ODD_EVEN", 1280 ���!n. ODD n = ~(EVEN n)���, 1281 REWRITE_TAC[EVEN_ODD]); 1282 1283val EVEN_OR_ODD = store_thm ("EVEN_OR_ODD", 1284 ���!n. EVEN n \/ ODD n���, 1285 REWRITE_TAC[EVEN_ODD, REWRITE_RULE[DE_MORGAN_THM] NOT_AND]); 1286 1287val EVEN_AND_ODD = store_thm ("EVEN_AND_ODD", 1288 ���!n. ~(EVEN n /\ ODD n)���, 1289 REWRITE_TAC[ODD_EVEN, NOT_AND]); 1290 1291val EVEN_ADD = store_thm ("EVEN_ADD", 1292 ���!m n. EVEN(m + n) = (EVEN m = EVEN n)���, 1293 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES, EVEN] THEN 1294 BOOL_CASES_TAC (���EVEN m���) THEN REWRITE_TAC[]); 1295 1296val EVEN_MULT = store_thm ("EVEN_MULT", 1297 ���!m n. EVEN(m * n) = EVEN m \/ EVEN n���, 1298 INDUCT_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES, EVEN_ADD, EVEN] THEN 1299 BOOL_CASES_TAC (���EVEN m���) THEN REWRITE_TAC[]); 1300 1301val ODD_ADD = store_thm ("ODD_ADD", 1302 ���!m n. ODD(m + n) = ~(ODD m = ODD n)���, 1303 REPEAT GEN_TAC THEN REWRITE_TAC[ODD_EVEN, EVEN_ADD] THEN 1304 BOOL_CASES_TAC (���EVEN m���) THEN REWRITE_TAC[]); 1305 1306val ODD_MULT = store_thm ("ODD_MULT", 1307 ���!m n. ODD(m * n) = ODD(m) /\ ODD(n)���, 1308 REPEAT GEN_TAC THEN REWRITE_TAC[ODD_EVEN, EVEN_MULT, DE_MORGAN_THM]); 1309 1310val two = prove( 1311 ���2 = SUC 1���, 1312 REWRITE_TAC [NUMERAL_DEF, BIT1, BIT2] THEN 1313 ONCE_REWRITE_TAC [SYM (SPEC (���0���) NUMERAL_DEF)] THEN 1314 REWRITE_TAC [ADD_CLAUSES]); 1315 1316val EVEN_DOUBLE = store_thm ("EVEN_DOUBLE", 1317 ���!n. EVEN(2 * n)���, 1318 GEN_TAC THEN REWRITE_TAC[EVEN_MULT] THEN DISJ1_TAC THEN 1319 REWRITE_TAC[EVEN, ONE, two]); 1320 1321val ODD_DOUBLE = store_thm ("ODD_DOUBLE", 1322 ���!n. ODD(SUC(2 * n))���, 1323 REWRITE_TAC[ODD] THEN REWRITE_TAC[GSYM EVEN_ODD, EVEN_DOUBLE]); 1324 1325val EVEN_ODD_EXISTS = store_thm ("EVEN_ODD_EXISTS", 1326 ���!n. (EVEN n ==> ?m. n = 2 * m) /\ (ODD n ==> ?m. n = SUC(2 * m))���, 1327 REWRITE_TAC[ODD_EVEN] THEN INDUCT_TAC THEN REWRITE_TAC[EVEN] THENL 1328 [EXISTS_TAC (���0���) THEN REWRITE_TAC[MULT_CLAUSES], 1329 POP_ASSUM STRIP_ASSUME_TAC THEN CONJ_TAC THEN 1330 DISCH_THEN(fn th => FIRST_ASSUM(X_CHOOSE_THEN (���m:num���) SUBST1_TAC o 1331 C MATCH_MP th)) THENL 1332 [EXISTS_TAC (���SUC m���) THEN 1333 REWRITE_TAC[ONE, two, MULT_CLAUSES, ADD_CLAUSES], 1334 EXISTS_TAC (���m:num���) THEN REFL_TAC]]); 1335 1336val EVEN_EXISTS = store_thm ("EVEN_EXISTS", 1337 ���!n. EVEN n = ?m. n = 2 * m���, 1338 GEN_TAC THEN EQ_TAC THENL 1339 [REWRITE_TAC[EVEN_ODD_EXISTS], 1340 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN MATCH_ACCEPT_TAC EVEN_DOUBLE]); 1341 1342val ODD_EXISTS = store_thm ("ODD_EXISTS", 1343 ���!n. ODD n = ?m. n = SUC(2 * m)���, 1344 GEN_TAC THEN EQ_TAC THENL 1345 [REWRITE_TAC[EVEN_ODD_EXISTS], 1346 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN MATCH_ACCEPT_TAC ODD_DOUBLE]); 1347 1348val EVEN_EXP_IFF = Q.store_thm( 1349 "EVEN_EXP_IFF", 1350 `!n m. EVEN (m ** n) <=> 0 < n /\ EVEN m`, 1351 INDUCT_TAC THEN 1352 ASM_REWRITE_TAC [EXP, ONE, EVEN, EVEN_MULT, LESS_0, LESS_REFL] THEN 1353 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC []); 1354 1355val EVEN_EXP = Q.store_thm ("EVEN_EXP", 1356 `!m n. 0 < n /\ EVEN m ==> EVEN (m ** n)`, 1357 METIS_TAC[EVEN_EXP_IFF]); 1358 1359val ODD_EXP_IFF = Q.store_thm( 1360 "ODD_EXP_IFF", 1361 `!n m. ODD (m ** n) <=> (n = 0) \/ ODD m`, 1362 REWRITE_TAC [ODD_EVEN, EVEN_EXP_IFF, DE_MORGAN_THM, NOT_LT_ZERO_EQ_ZERO]); 1363 1364val ODD_EXP = Q.store_thm( 1365 "ODD_EXP", 1366 `!m n. 0 < n /\ ODD m ==> ODD (m ** n)`, 1367 METIS_TAC[ODD_EXP_IFF, NOT_LT_ZERO_EQ_ZERO]); 1368 1369(* --------------------------------------------------------------------- *) 1370(* Theorems moved from the "more_arithmetic" library [RJB 92.09.28] *) 1371(* --------------------------------------------------------------------- *) 1372 1373val EQ_LESS_EQ = store_thm ("EQ_LESS_EQ", 1374 ���!m n. (m = n) = ((m <= n) /\ (n <= m))���, 1375 REPEAT GEN_TAC THEN EQ_TAC 1376 THENL [STRIP_TAC THEN ASM_REWRITE_TAC [LESS_EQ_REFL], 1377 REWRITE_TAC [LESS_EQUAL_ANTISYM]]); 1378 1379val ADD_MONO_LESS_EQ = store_thm ("ADD_MONO_LESS_EQ", 1380 ���!m n p. (m + n) <= (m + p) = (n <= p)���, 1381 ONCE_REWRITE_TAC [ADD_SYM] 1382 THEN REWRITE_TAC [LESS_EQ_MONO_ADD_EQ]); 1383val LE_ADD_LCANCEL = save_thm ("LE_ADD_LCANCEL", ADD_MONO_LESS_EQ) 1384val LE_ADD_RCANCEL = save_thm ("LE_ADD_RCANCEL", 1385 ONCE_REWRITE_RULE [ADD_COMM] LE_ADD_LCANCEL) 1386 1387(* ---------------------------------------------------------------------*) 1388(* Theorems to support the arithmetic proof procedure [RJB 92.09.29]*) 1389(* ---------------------------------------------------------------------*) 1390 1391val _ = print "Theorems to support the arithmetic proof procedure\n" 1392val NOT_LEQ = store_thm ("NOT_LEQ", 1393 ���!m n. ~(m <= n) = (SUC n) <= m���, 1394 REWRITE_TAC [SYM (SPEC_ALL LESS_EQ)] THEN 1395 REWRITE_TAC [SYM (SPEC_ALL NOT_LESS)]); 1396 1397val NOT_NUM_EQ = store_thm ("NOT_NUM_EQ", 1398 ���!m n. ~(m = n) = (((SUC m) <= n) \/ ((SUC n) <= m))���, 1399 REWRITE_TAC [EQ_LESS_EQ,DE_MORGAN_THM,NOT_LEQ] THEN 1400 MATCH_ACCEPT_TAC DISJ_SYM); 1401 1402val NOT_GREATER = store_thm ("NOT_GREATER", 1403 ���!m n. ~(m > n) = (m <= n)���, 1404 REWRITE_TAC [GREATER_DEF,NOT_LESS]); 1405 1406val NOT_GREATER_EQ = store_thm ("NOT_GREATER_EQ", 1407 ���!m n. ~(m >= n) = (SUC m) <= n���, 1408 REWRITE_TAC [GREATER_EQ,NOT_LEQ]); 1409 1410val SUC_ONE_ADD = store_thm ("SUC_ONE_ADD", 1411 ���!n. SUC n = 1 + n���, 1412 GEN_TAC THEN 1413 ONCE_REWRITE_TAC [ADD1,ADD_SYM] THEN 1414 REFL_TAC); 1415 1416val SUC_ADD_SYM = store_thm ("SUC_ADD_SYM", 1417 ���!m n. SUC (m + n) = (SUC n) + m���, 1418 REPEAT GEN_TAC THEN 1419 REWRITE_TAC[ADD_CLAUSES] THEN 1420 AP_TERM_TAC THEN 1421 ACCEPT_TAC (SPEC_ALL ADD_SYM)); 1422 1423val NOT_SUC_ADD_LESS_EQ = store_thm ("NOT_SUC_ADD_LESS_EQ", 1424 ���!m n. ~(SUC (m + n) <= m)���, 1425 REPEAT GEN_TAC THEN 1426 REWRITE_TAC [SYM (SPEC_ALL LESS_EQ)] THEN 1427 REWRITE_TAC [NOT_LESS,LESS_EQ_ADD]); 1428 1429val MULT_LESS_EQ_SUC = 1430 let val th1 = SPEC (���b:num���) (SPEC (���c:num���) (SPEC (���a:num���) 1431 LESS_MONO_ADD)) 1432 val th2 = SPEC (���c:num���) (SPEC (���d:num���) (SPEC (���b:num���) 1433 LESS_MONO_ADD)) 1434 val th3 = ONCE_REWRITE_RULE [ADD_SYM] th2 1435 val th4 = CONJ (UNDISCH_ALL th1) (UNDISCH_ALL th3) 1436 val th5 = MATCH_MP LESS_TRANS th4 1437 val th6 = DISCH_ALL th5 1438 in 1439 store_thm ("MULT_LESS_EQ_SUC", 1440 ���!m n p. m <= n = ((SUC p) * m) <= ((SUC p) * n)���, 1441 REPEAT GEN_TAC THEN 1442 EQ_TAC THENL 1443 [ONCE_REWRITE_TAC [MULT_SYM] THEN 1444 REWRITE_TAC [LESS_MONO_MULT], 1445 CONV_TAC CONTRAPOS_CONV THEN 1446 REWRITE_TAC [SYM (SPEC_ALL NOT_LESS)] THEN 1447 SPEC_TAC ((���p:num���),(���p:num���)) THEN 1448 INDUCT_TAC THENL 1449 [REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES], 1450 STRIP_TAC THEN 1451 RES_TAC THEN 1452 ONCE_REWRITE_TAC [MULT_CLAUSES] THEN 1453 IMP_RES_TAC th6]]) 1454 end; 1455 1456val LE_MULT_LCANCEL = store_thm ("LE_MULT_LCANCEL", 1457 ���!m n p. m * n <= m * p = (m = 0) \/ n <= p���, 1458 REPEAT GEN_TAC THEN 1459 Q.SPEC_THEN `m` STRUCT_CASES_TAC num_CASES THENL [ 1460 REWRITE_TAC [LESS_EQ_REFL, MULT_CLAUSES], 1461 REWRITE_TAC [NOT_SUC, GSYM MULT_LESS_EQ_SUC] 1462 ]); 1463 1464val LE_MULT_RCANCEL = store_thm ("LE_MULT_RCANCEL", 1465 ���!m n p. m * n <= p * n = (n = 0) \/ m <= p���, 1466 ONCE_REWRITE_TAC [MULT_COMM] THEN REWRITE_TAC [LE_MULT_LCANCEL]); 1467 1468val LT_MULT_LCANCEL = store_thm ("LT_MULT_LCANCEL", 1469 ���!m n p. m * n < m * p = 0 < m /\ n < p���, 1470 REPEAT GEN_TAC THEN 1471 Q.SPEC_THEN `m` STRUCT_CASES_TAC num_CASES THENL [ 1472 REWRITE_TAC [MULT_CLAUSES, LESS_REFL], 1473 REWRITE_TAC [LESS_MULT_MONO, LESS_0] 1474 ]); 1475 1476val LT_MULT_RCANCEL = store_thm ("LT_MULT_RCANCEL", 1477 ���!m n p. m * n < p * n = 0 < n /\ m < p���, 1478 ONCE_REWRITE_TAC [MULT_COMM] THEN REWRITE_TAC [LT_MULT_LCANCEL]); 1479 1480(* |- (m < m * n = 0 < m /\ 1 < n) /\ (m < n * m = 0 < m /\ 1 < n) *) 1481val LT_MULT_CANCEL_LBARE = save_thm ( 1482 "LT_MULT_CANCEL_LBARE", 1483 CONJ 1484 (REWRITE_RULE [MULT_CLAUSES] (Q.SPECL [`m`, `1`, `n`] LT_MULT_LCANCEL)) 1485 (REWRITE_RULE [MULT_CLAUSES] (Q.SPECL [`1`,`m`, `n`] LT_MULT_RCANCEL))) 1486 1487val lt1_eq0 = prove( 1488 ���x < 1 = (x = 0)���, 1489 Q.SPEC_THEN `x` STRUCT_CASES_TAC num_CASES THEN 1490 REWRITE_TAC [ONE, LESS_0, NOT_LESS_0, LESS_MONO_EQ, NOT_SUC]) 1491 1492(* |- (m * n < m = 0 < m /\ (n = 0)) /\ (m * n < n = 0 < n /\ (m = 0)) *) 1493val LT_MULT_CANCEL_RBARE = save_thm ( 1494 "LT_MULT_CANCEL_RBARE", 1495 CONJ 1496 (REWRITE_RULE [MULT_CLAUSES, lt1_eq0] 1497 (Q.SPECL [`m`,`n`,`1`] LT_MULT_LCANCEL)) 1498 (REWRITE_RULE [MULT_CLAUSES, lt1_eq0] 1499 (Q.SPECL [`m`,`n`,`1`] LT_MULT_RCANCEL))) 1500 1501val le1_lt0 = prove(���1 <= n = 0 < n���, REWRITE_TAC [LESS_EQ, ONE]); 1502 1503(* |- (m <= m * n = (m = 0) \/ 0 < n) /\ (m <= n * m = (m = 0) \/ 0 < n) *) 1504val LE_MULT_CANCEL_LBARE = save_thm ( 1505 "LE_MULT_CANCEL_LBARE", 1506 CONJ 1507 (REWRITE_RULE [MULT_CLAUSES, le1_lt0] 1508 (Q.SPECL [`m`,`1`,`n`] LE_MULT_LCANCEL)) 1509 (REWRITE_RULE [MULT_CLAUSES, le1_lt0] 1510 (Q.SPECL [`1`,`m`,`n`] LE_MULT_RCANCEL))) 1511 1512(* |- (m * n <= m = (m = 0) \/ n <= 1) /\ (m * n <= n = (n = 0) \/ m <= 1) *) 1513val LE_MULT_CANCEL_RBARE = save_thm ( 1514 "LE_MULT_CANCEL_RBARE", 1515 CONJ 1516 (REWRITE_RULE [MULT_CLAUSES] (Q.SPECL [`m`,`n`,`1`] LE_MULT_LCANCEL)) 1517 (REWRITE_RULE [MULT_CLAUSES] (Q.SPECL [`m`,`n`,`1`] LE_MULT_RCANCEL))) 1518 1519val SUB_LEFT_ADD = store_thm ("SUB_LEFT_ADD", 1520 ���!m n p. m + (n - p) = (if (n <= p) then m else (m + n) - p)���, 1521 GEN_TAC THEN REPEAT INDUCT_TAC THEN 1522 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ, 1523 ZERO_LESS_EQ, NOT_SUC_LESS_EQ_0, LESS_EQ_MONO]) ; 1524 1525val SUB_RIGHT_ADD = store_thm ("SUB_RIGHT_ADD", 1526 ���!m n p. (m - n) + p = (if (m <= n) then p else (m + p) - n)���, 1527 INDUCT_TAC THEN INDUCT_TAC THEN 1528 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ, 1529 ZERO_LESS_EQ, NOT_SUC_LESS_EQ_0, LESS_EQ_MONO]) ; 1530 1531val SUB_LEFT_SUB = store_thm ("SUB_LEFT_SUB", 1532 ���!m n p. m - (n - p) = (if (n <= p) then m else (m + p) - n)���, 1533 GEN_TAC THEN REPEAT INDUCT_TAC THEN 1534 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ, 1535 ZERO_LESS_EQ, NOT_SUC_LESS_EQ_0, LESS_EQ_MONO]) ; 1536 1537val SUB_RIGHT_SUB = store_thm ("SUB_RIGHT_SUB", 1538 ���!m n p. (m - n) - p = m - (n + p)���, 1539 INDUCT_TAC THEN INDUCT_TAC THEN 1540 ASM_REWRITE_TAC [SUB_0,ADD_CLAUSES,SUB_MONO_EQ]) ; 1541 1542val SUB_LEFT_SUC = store_thm ("SUB_LEFT_SUC", 1543 ���!m n. SUC (m - n) = (if (m <= n) then (SUC 0) else (SUC m) - n)���, 1544 REPEAT GEN_TAC THEN 1545 ASM_CASES_TAC (���m <= n���) THENL 1546 [IMP_RES_THEN (fn th => ASM_REWRITE_TAC [th]) (SYM (SPEC_ALL SUB_EQ_0)), 1547 ASM_REWRITE_TAC [SUB] THEN 1548 ASSUM_LIST (MAP_EVERY (REWRITE_TAC o CONJUNCTS o 1549 (PURE_REWRITE_RULE [LESS_OR_EQ,DE_MORGAN_THM])))]); 1550 1551val pls = prove (���p <= m \/ p <= 0 = p <= m���, 1552 REWRITE_TAC [LESS_EQ_0] THEN 1553 EQ_TAC THEN REPEAT STRIP_TAC THEN 1554 ASM_REWRITE_TAC [ZERO_LESS_EQ]) ; 1555 1556val SUB_LEFT_LESS_EQ = store_thm ("SUB_LEFT_LESS_EQ", 1557 ���!m n p. (m <= (n - p)) = ((m + p) <= n) \/ (m <= 0)���, 1558 GEN_TAC THEN REPEAT INDUCT_TAC THEN 1559 ASM_REWRITE_TAC [ADD_CLAUSES, SUB_0, SUB_MONO_EQ, pls, 1560 ZERO_LESS_EQ, NOT_SUC_LESS_EQ_0, LESS_EQ_MONO, NOT_SUC]) ; 1561 1562val SUB_RIGHT_LESS_EQ = store_thm ("SUB_RIGHT_LESS_EQ", 1563 ���!m n p. ((m - n) <= p) = (m <= (n + p))���, 1564 INDUCT_TAC THEN INDUCT_TAC THEN 1565 ASM_REWRITE_TAC [SUB_0,ADD_CLAUSES, 1566 SUB_MONO_EQ, LESS_EQ_MONO, ZERO_LESS_EQ]) ; 1567 1568val SUB_LEFT_LESS = store_thm ("SUB_LEFT_LESS", 1569 ���!m n p. (m < (n - p)) = ((m + p) < n)���, 1570 REPEAT GEN_TAC THEN 1571 PURE_REWRITE_TAC [LESS_EQ,SYM (SPEC_ALL (CONJUNCT2 ADD))] THEN 1572 PURE_ONCE_REWRITE_TAC [SUB_LEFT_LESS_EQ] THEN 1573 REWRITE_TAC [SYM (SPEC_ALL LESS_EQ),NOT_LESS_0]); 1574 1575val SUB_RIGHT_LESS = 1576 let val BOOL_EQ_NOT_BOOL_EQ = prove( 1577 ���!x y. (x = y) = (~x = ~y)���, 1578 REPEAT GEN_TAC THEN 1579 BOOL_CASES_TAC (���x:bool���) THEN 1580 REWRITE_TAC []) 1581 in 1582 store_thm ("SUB_RIGHT_LESS", 1583 ���!m n p. ((m - n) < p) = ((m < (n + p)) /\ (0 < p))���, 1584 REPEAT GEN_TAC THEN 1585 PURE_ONCE_REWRITE_TAC [BOOL_EQ_NOT_BOOL_EQ] THEN 1586 PURE_REWRITE_TAC [DE_MORGAN_THM,NOT_LESS] THEN 1587 SUBST1_TAC (SPECL [(���n:num���),(���p:num���)] ADD_SYM) THEN 1588 REWRITE_TAC [SUB_LEFT_LESS_EQ]) 1589 end; 1590 1591val SUB_LEFT_GREATER_EQ = store_thm ("SUB_LEFT_GREATER_EQ", 1592 ���!m n p. (m >= (n - p)) = ((m + p) >= n)���, 1593 REWRITE_TAC [GREATER_EQ] THEN 1594 GEN_TAC THEN REPEAT INDUCT_TAC THEN 1595 ASM_REWRITE_TAC [SUB_0,ADD_CLAUSES, 1596 SUB_MONO_EQ, LESS_EQ_MONO, ZERO_LESS_EQ]) ; 1597 1598val SUB_RIGHT_GREATER_EQ = store_thm ("SUB_RIGHT_GREATER_EQ", 1599 ���!m n p. ((m - n) >= p) = ((m >= (n + p)) \/ (0 >= p))���, 1600 REWRITE_TAC [GREATER_EQ] THEN 1601 INDUCT_TAC THEN INDUCT_TAC THEN 1602 ASM_REWRITE_TAC [SUB_0,ADD_CLAUSES, SUB_MONO_EQ, 1603 LESS_EQ_MONO, ZERO_LESS_EQ, NOT_SUC_LESS_EQ_0, pls]) ; 1604 1605val SUB_LEFT_GREATER = store_thm ("SUB_LEFT_GREATER", 1606 ���!m n p. (m > (n - p)) = (((m + p) > n) /\ (m > 0))���, 1607 REPEAT GEN_TAC THEN 1608 PURE_ONCE_REWRITE_TAC [GREATER_DEF] THEN 1609 SUBST1_TAC (SPECL [(���m:num���),(���p:num���)] ADD_SYM) THEN 1610 REWRITE_TAC [SUB_RIGHT_LESS]); 1611 1612val SUB_RIGHT_GREATER = store_thm ("SUB_RIGHT_GREATER", 1613 ���!m n p. ((m - n) > p) = (m > (n + p))���, 1614 REPEAT GEN_TAC THEN 1615 PURE_ONCE_REWRITE_TAC [GREATER_DEF] THEN 1616 SUBST1_TAC (SPECL [(���n:num���),(���p:num���)] ADD_SYM) THEN 1617 REWRITE_TAC [SUB_LEFT_LESS]); 1618 1619val SUB_LEFT_EQ = store_thm ("SUB_LEFT_EQ", 1620 ���!m n p. (m = (n - p)) = ((m + p) = n) \/ ((m <= 0) /\ (n <= p))���, 1621 GEN_TAC THEN REPEAT INDUCT_TAC THEN 1622 ASM_REWRITE_TAC [SUB_0,ADD_CLAUSES, INV_SUC_EQ, 1623 SUB_MONO_EQ, LESS_EQ_MONO, ZERO_LESS_EQ, LESS_EQ_0, NOT_SUC]) ; 1624 1625val SUB_RIGHT_EQ = store_thm ("SUB_RIGHT_EQ", 1626 ���!m n p. ((m - n) = p) = (m = (n + p)) \/ ((m <= n) /\ (p <= 0))���, 1627 INDUCT_TAC THEN INDUCT_TAC THEN GEN_TAC THEN 1628 ASM_REWRITE_TAC [SUB_0,ADD_CLAUSES, INV_SUC_EQ, SUB_EQ_0, SUB_MONO_EQ, 1629 LESS_EQ_MONO, ZERO_LESS_EQ, LESS_EQ_0, NOT_SUC, GSYM NOT_SUC] THEN 1630 EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []) ; 1631 1632val LE = save_thm ("LE", 1633 CONJ LESS_EQ_0 1634 (prove(���(!m n. m <= SUC n = (m = SUC n) \/ m <= n)���, 1635 REPEAT GEN_TAC THEN 1636 CONV_TAC (DEPTH_CONV (LHS_CONV (REWR_CONV LESS_OR_EQ))) THEN 1637 REWRITE_TAC [GSYM LESS_EQ_IFF_LESS_SUC] THEN 1638 MATCH_ACCEPT_TAC DISJ_COMM))) ; 1639 1640val _ = print "Proving division\n" 1641 1642(* =====================================================================*) 1643(* Added TFM 90.05.24 *) 1644(* *) 1645(* Prove the division algorithm: *) 1646(* *) 1647(* |- !k n. n>0 ==> ?q r. k=qn+r /\ 0<= r < n *) 1648(* *) 1649(* The proof follows MacLane & Birkhoff, p29. *) 1650(* =====================================================================*) 1651 1652(* ---------------------------------------------------------------------*) 1653(* We first show that ?r q. k=qn+r. This is easy, with r=k and q=0. *) 1654(* ---------------------------------------------------------------------*) 1655 1656val exists_lemma = prove( 1657 ���?r q. (k=(q*n)+r)���, 1658 MAP_EVERY EXISTS_TAC [���k:num���,���0���] THEN 1659 REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES]); 1660 1661(* ---------------------------------------------------------------------*) 1662(* We now show, using the well ordering property, that there is a *) 1663(* SMALLEST n' such that ?q. k=qn+n'. This is the correct remainder. *) 1664(* *) 1665(* The theorem is: |- ?n'. (?q. k = q*n+n') /\ *) 1666(* (!y. y<n' ==> (!q. ~(k=q*n+y))) *) 1667(* ---------------------------------------------------------------------*) 1668val smallest_lemma = 1669 CONV_RULE (DEPTH_CONV NOT_EXISTS_CONV) 1670 (MATCH_MP (CONV_RULE (DEPTH_CONV BETA_CONV) 1671 (SPEC (���\r.?q.k=(q*n)+r���) WOP)) 1672 exists_lemma); 1673 1674(* We will need the lemma |- !m n. n <= m ==> (?p. m = n + p) *) 1675val leq_add_lemma = prove( 1676 ���!m n. (n<=m) ==> ?p.m=n+p���, 1677 REWRITE_TAC [LESS_OR_EQ] THEN 1678 REPEAT STRIP_TAC THENL 1679 [FIRST_ASSUM (STRIP_ASSUME_TAC o MATCH_MP LESS_ADD_1) THEN 1680 EXISTS_TAC (���p+1���) THEN 1681 FIRST_ASSUM ACCEPT_TAC, 1682 EXISTS_TAC (���0���) THEN 1683 ASM_REWRITE_TAC [ADD_CLAUSES]]); 1684 1685(* We will also need the lemma: |- k=qn+n+p ==> k=(q+1)*n+p *) 1686val k_expr_lemma = prove( 1687 ���(k=(q*n)+(n+p)) ==> (k=((q+1)*n)+p)���, 1688 REWRITE_TAC [RIGHT_ADD_DISTRIB,MULT_CLAUSES,ADD_ASSOC]); 1689 1690(* We will also need the lemma: [0<n] |- p < (n + p) *) 1691val less_add = TAC_PROOF(([���0<n���], ���p < (n + p)���), 1692 PURE_ONCE_REWRITE_TAC [ADD_SYM] THEN 1693 MATCH_MP_TAC LESS_ADD_NONZERO THEN 1694 IMP_RES_THEN (STRIP_THM_THEN SUBST1_TAC) LESS_ADD_1 THEN 1695 REWRITE_TAC [ADD_CLAUSES, ONE, NOT_SUC]); 1696 1697(* Now prove the desired theorem. *) 1698val DA = store_thm ("DA", 1699���!k n. 0<n ==> ?r q. (k=(q*n)+r) /\ r<n���, 1700 REPEAT STRIP_TAC THEN 1701 STRIP_ASSUME_TAC smallest_lemma THEN 1702 MAP_EVERY EXISTS_TAC [���n':num���,���q:num���] THEN 1703 ASM_REWRITE_TAC [] THEN 1704 DISJ_CASES_THEN CHECK_ASSUME_TAC 1705 (SPECL [���n':num���,���n:num���] LESS_CASES) THEN 1706 IMP_RES_THEN (STRIP_THM_THEN SUBST_ALL_TAC) leq_add_lemma THEN 1707 IMP_RES_TAC k_expr_lemma THEN 1708 ANTE_RES_THEN IMP_RES_TAC less_add); 1709 1710(* ---------------------------------------------------------------------*) 1711(* We can now define MOD and DIV to have the property given by DA. *) 1712(* We prove the existence of the required functions, and then define *) 1713(* MOD and DIV using a constant specification. *) 1714(* ---------------------------------------------------------------------*) 1715 1716(* First prove the existence of MOD. *) 1717val MOD_exists = prove( 1718 ���?MOD. !n. (0<n) ==> 1719 !k.?q.(k=((q * n)+(MOD k n))) /\ ((MOD k n) < n)���, 1720 EXISTS_TAC (���\k n. @r. ?q. (k = (q * n) + r) /\ r < n���) THEN 1721 REPEAT STRIP_TAC THEN 1722 IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC (���k:num���)) DA THEN 1723 CONV_TAC (TOP_DEPTH_CONV BETA_CONV) THEN 1724 CONV_TAC SELECT_CONV THEN 1725 MAP_EVERY EXISTS_TAC [���r:num���,���q:num���] THEN 1726 CONJ_TAC THEN FIRST_ASSUM ACCEPT_TAC); 1727 1728(* Now, prove the existence of MOD and DIV. *) 1729val MOD_DIV_exist = prove( 1730 ���?MOD DIV. 1731 !n. 0<n ==> 1732 !k. (k = ((DIV k n * n) + MOD k n)) /\ (MOD k n < n)���, 1733 STRIP_ASSUME_TAC MOD_exists THEN 1734 EXISTS_TAC (���MOD:num->num->num���) THEN 1735 EXISTS_TAC (���\k n. @q. (k = (q * n) + (MOD k n))���) THEN 1736 REPEAT STRIP_TAC THENL 1737 [CONV_TAC (TOP_DEPTH_CONV BETA_CONV) THEN 1738 CONV_TAC SELECT_CONV THEN 1739 RES_THEN (STRIP_ASSUME_TAC o SPEC (���k:num���)) THEN 1740 EXISTS_TAC (���q:num���) THEN 1741 FIRST_ASSUM ACCEPT_TAC, 1742 RES_THEN (STRIP_ASSUME_TAC o SPEC (���k:num���))]); 1743 1744(*--------------------------------------------------------------------------- 1745 Now define MOD and DIV by a constant specification. 1746 ---------------------------------------------------------------------------*) 1747 1748val DIVISION = new_specification ("DIVISION", ["MOD", "DIV"], MOD_DIV_exist); 1749 1750val _ = set_fixity "MOD" (Infixl 650); 1751val _ = set_fixity "DIV" (Infixl 600); 1752 1753val DIV2_def = new_definition("DIV2_def", ���DIV2 n = n DIV 2���); 1754 1755local 1756 open OpenTheoryMap 1757in 1758 val _ = OpenTheory_const_name 1759 {const = {Thy = "arithmetic", Name = "DIV2"}, 1760 name = (["HOL4", "arithmetic"], "DIV2")} 1761end 1762 1763(* ---------------------------------------------------------------------*) 1764(* Properties of MOD and DIV that don't depend on uniqueness. *) 1765(* ---------------------------------------------------------------------*) 1766 1767val MOD_ONE = store_thm ("MOD_ONE", 1768���!k. k MOD (SUC 0) = 0���, 1769 STRIP_TAC THEN 1770 MP_TAC (CONJUNCT2 (SPEC (���k:num���) 1771 (REWRITE_RULE [LESS_SUC_REFL] (SPEC (���SUC 0���) DIVISION)))) THEN 1772 REWRITE_TAC [LESS_THM,NOT_LESS_0]); 1773 1774(* |- x MOD 1 = 0 *) 1775val MOD_1 = save_thm ("MOD_1", REWRITE_RULE [SYM ONE] MOD_ONE); 1776 1777val DIV_LESS_EQ = store_thm ("DIV_LESS_EQ", 1778 ���!n. 0<n ==> !k. (k DIV n) <= k���, 1779 REPEAT STRIP_TAC THEN 1780 IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC (���k:num���)) DIVISION THEN 1781 FIRST_ASSUM (fn th => fn g => SUBST_OCCS_TAC [([2],th)] g) THEN 1782 REPEAT_TCL STRIP_THM_THEN MP_TAC (SPEC (���n:num���) num_CASES) THENL 1783 [IMP_RES_TAC LESS_NOT_EQ THEN 1784 DISCH_THEN (ASSUME_TAC o SYM) THEN 1785 RES_TAC, 1786 DISCH_THEN (fn th => SUBST_OCCS_TAC [([3],th)]) THEN 1787 REWRITE_TAC [MULT_CLAUSES] THEN 1788 REWRITE_TAC [SYM(SPEC_ALL ADD_ASSOC)] THEN 1789 MATCH_ACCEPT_TAC LESS_EQ_ADD]); 1790 1791(* ---------------------------------------------------------------------*) 1792(* Now, show that the quotient and remainder are unique. *) 1793(* *) 1794(* NB: the beastly proof given below of DIV_UNIQUE is definitely NOT *) 1795(* good HOL style. *) 1796(* ---------------------------------------------------------------------*) 1797 1798val lemma = prove( 1799 ���!x y z. x<y ==> ~(y + z = x)���, 1800 REPEAT STRIP_TAC THEN POP_ASSUM (SUBST_ALL_TAC o SYM) 1801 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[] 1802 THEN SPEC_TAC (���y:num���,���y:num���) 1803 THEN INDUCT_TAC THEN ASM_REWRITE_TAC [ADD_CLAUSES,NOT_LESS_0,LESS_MONO_EQ]); 1804 1805local val (eq,ls) = 1806 CONJ_PAIR (SPEC (���k:num���) 1807 (REWRITE_RULE [LESS_0] (SPEC (���SUC(r+p)���) DIVISION))) 1808in 1809val DIV_UNIQUE = store_thm ("DIV_UNIQUE", 1810 ���!n k q. (?r. (k = q*n + r) /\ r<n) ==> (k DIV n = q)���, 1811REPEAT GEN_TAC THEN 1812 DISCH_THEN (CHOOSE_THEN (CONJUNCTS_THEN2 1813 MP_TAC (STRIP_THM_THEN SUBST_ALL_TAC o MATCH_MP LESS_ADD_1))) THEN 1814 REWRITE_TAC [ONE,MULT_CLAUSES,ADD_CLAUSES] THEN 1815 DISCH_THEN 1816 (fn th1 => 1817 MATCH_MP_TAC LESS_EQUAL_ANTISYM THEN 1818 PURE_ONCE_REWRITE_TAC [SYM (SPEC_ALL NOT_LESS)] THEN CONJ_TAC THEN 1819 DISCH_THEN (fn th2 => 1820 MP_TAC (TRANS (SYM eq) th1) THEN STRIP_THM_THEN SUBST_ALL_TAC 1821 (MATCH_MP LESS_ADD_1 th2))) THEN REWRITE_TAC[] THENL 1822[MATCH_MP_TAC lemma, MATCH_MP_TAC (ONCE_REWRITE_RULE [EQ_SYM_EQ] lemma)] 1823 THEN REWRITE_TAC [MULT_CLAUSES,GSYM ADD_ASSOC, 1824 ONCE_REWRITE_RULE [ADD_SYM]LESS_MONO_ADD_EQ] 1825 THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o RAND_CONV) 1826 empty_rewrites [RIGHT_ADD_DISTRIB] 1827 THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) empty_rewrites [ADD_SYM] 1828 THEN REWRITE_TAC [GSYM ADD_ASSOC] 1829 THEN GEN_REWRITE_TAC (RAND_CONV) empty_rewrites [ADD_SYM] THEN 1830 REWRITE_TAC [GSYM ADD_ASSOC, ONCE_REWRITE_RULE [ADD_SYM]LESS_MONO_ADD_EQ] 1831 THENL 1832 [REWRITE_TAC[LEFT_ADD_DISTRIB] THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] 1833 THEN REWRITE_TAC [MULT_CLAUSES,GSYM ADD_ASSOC] 1834 THEN GEN_REWRITE_TAC (RAND_CONV) empty_rewrites [ADD_SYM] 1835 THEN REWRITE_TAC [GSYM ADD_ASSOC,ONE, 1836 REWRITE_RULE[ADD_CLAUSES] 1837 (ONCE_REWRITE_RULE [ADD_SYM] 1838 (SPECL [���0���,���n:num���,���r:num���]LESS_MONO_ADD_EQ))] 1839 THEN REWRITE_TAC [ADD_CLAUSES, LESS_0], 1840 1841 MATCH_MP_TAC LESS_LESS_EQ_TRANS THEN EXISTS_TAC (���SUC (r+p)���) 1842 THEN REWRITE_TAC 1843 [CONJUNCT2(SPEC_ALL(MATCH_MP DIVISION (SPEC(���r+p���) LESS_0)))] 1844 THEN REWRITE_TAC[LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB, 1845 MULT_CLAUSES,GSYM ADD_ASSOC,ADD1] 1846 THEN GEN_REWRITE_TAC (RAND_CONV) empty_rewrites [ADD_SYM] 1847 THEN REWRITE_TAC [GSYM ADD_ASSOC, 1848 ONCE_REWRITE_RULE [ADD_SYM]LESS_EQ_MONO_ADD_EQ] 1849 THEN GEN_REWRITE_TAC (RAND_CONV) empty_rewrites [ADD_SYM] 1850 THEN REWRITE_TAC [GSYM ADD_ASSOC, 1851 ONCE_REWRITE_RULE [ADD_SYM]LESS_EQ_MONO_ADD_EQ] 1852 THEN REWRITE_TAC[ZERO_LESS_EQ, 1853 REWRITE_RULE[ADD_CLAUSES] 1854 (SPECL [���1���,���0���,���p:num���]ADD_MONO_LESS_EQ)]]) 1855end; 1856 1857val lemma = prove( 1858 ���!n k q r. ((k = (q * n) + r) /\ r < n) ==> (k DIV n = q)���, 1859 REPEAT STRIP_TAC THEN 1860 MATCH_MP_TAC DIV_UNIQUE THEN 1861 EXISTS_TAC (���r:num���) THEN 1862 ASM_REWRITE_TAC []); 1863 1864val MOD_UNIQUE = store_thm ("MOD_UNIQUE", 1865 ���!n k r. (?q. (k = (q * n) + r) /\ r < n) ==> (k MOD n = r)���, 1866 REPEAT STRIP_TAC THEN 1867 MP_TAC (DISCH_ALL (SPEC (���k:num���) 1868 (UNDISCH (SPEC (���n:num���) DIVISION)))) THEN 1869 FIRST_ASSUM (fn th => fn g => 1870 let val thm = MATCH_MP LESS_ADD_1 th 1871 fun tcl t = (SUBST_OCCS_TAC [([1],t)]) 1872 in 1873 STRIP_THM_THEN tcl thm g 1874 end 1875 ) THEN 1876 REWRITE_TAC [LESS_0, ONE, ADD_CLAUSES] THEN 1877 IMP_RES_THEN (IMP_RES_THEN SUBST1_TAC) lemma THEN 1878 FIRST_ASSUM (fn th => fn g => SUBST_OCCS_TAC [([1],th)] g) THEN 1879 let val th = PURE_ONCE_REWRITE_RULE [ADD_SYM] EQ_MONO_ADD_EQ 1880 in 1881 PURE_ONCE_REWRITE_TAC [th] THEN 1882 DISCH_THEN (STRIP_THM_THEN (fn th => fn g => ACCEPT_TAC (SYM th) g)) 1883 end); 1884 1885(* ---------------------------------------------------------------------*) 1886(* Properties of MOD and DIV proved using uniqueness. *) 1887(* ---------------------------------------------------------------------*) 1888 1889val DIV_MULT = store_thm ("DIV_MULT", 1890 ���!n r. r < n ==> !q. (q*n + r) DIV n = q���, 1891 REPEAT GEN_TAC THEN 1892 REPEAT_TCL STRIP_THM_THEN SUBST1_TAC (SPEC (���n:num���) num_CASES) THENL 1893 [REWRITE_TAC [NOT_LESS_0], 1894 REPEAT STRIP_TAC THEN 1895 MATCH_MP_TAC DIV_UNIQUE THEN 1896 EXISTS_TAC (���r:num���) THEN 1897 ASM_REWRITE_TAC []]); 1898 1899val LESS_MOD = store_thm ("LESS_MOD", 1900 ���!n k. k < n ==> ((k MOD n) = k)���, 1901 REPEAT STRIP_TAC THEN 1902 MATCH_MP_TAC MOD_UNIQUE THEN 1903 EXISTS_TAC (���0���) THEN 1904 ASM_REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES]); 1905 1906val MOD_EQ_0 = store_thm ("MOD_EQ_0", 1907 ���!n. 0<n ==> !k. ((k * n) MOD n) = 0���, 1908 REPEAT STRIP_TAC THEN 1909 IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC (���k * n���)) DIVISION THEN 1910 MATCH_MP_TAC MOD_UNIQUE THEN 1911 EXISTS_TAC (���k:num���) THEN 1912 CONJ_TAC THENL 1913 [REWRITE_TAC [ADD_CLAUSES], FIRST_ASSUM ACCEPT_TAC]); 1914 1915val ZERO_MOD = store_thm ("ZERO_MOD", 1916 ���!n. 0<n ==> (0 MOD n = 0)���, 1917 REPEAT STRIP_TAC THEN 1918 IMP_RES_THEN (MP_TAC o SPEC (���0���)) MOD_EQ_0 THEN 1919 REWRITE_TAC [MULT_CLAUSES]); 1920 1921val ZERO_DIV = store_thm ("ZERO_DIV", 1922 ���!n. 0<n ==> (0 DIV n = 0)���, 1923 REPEAT STRIP_TAC THEN 1924 MATCH_MP_TAC DIV_UNIQUE THEN 1925 EXISTS_TAC (���0���) THEN 1926 ASM_REWRITE_TAC [MULT_CLAUSES,ADD_CLAUSES]); 1927 1928val MOD_MULT = store_thm ("MOD_MULT", 1929 ���!n r. r < n ==> !q. (q * n + r) MOD n = r���, 1930 REPEAT STRIP_TAC THEN 1931 MATCH_MP_TAC MOD_UNIQUE THEN 1932 EXISTS_TAC (���q:num���) THEN 1933 ASM_REWRITE_TAC [ADD_CLAUSES,MULT_CLAUSES]); 1934 1935val MOD_TIMES = store_thm ("MOD_TIMES", 1936 ���!n. 0<n ==> !q r. (((q * n) + r) MOD n) = (r MOD n)���, 1937 let fun SUBS th = SUBST_OCCS_TAC [([1],th)] 1938 in 1939 REPEAT STRIP_TAC THEN 1940 IMP_RES_THEN (TRY o SUBS o SPEC (���r:num���)) DIVISION THEN 1941 REWRITE_TAC [ADD_ASSOC,SYM(SPEC_ALL RIGHT_ADD_DISTRIB)] THEN 1942 IMP_RES_THEN (ASSUME_TAC o SPEC (���r:num���)) DIVISION THEN 1943 IMP_RES_TAC MOD_MULT THEN 1944 FIRST_ASSUM MATCH_ACCEPT_TAC 1945 end); 1946 1947val MOD_TIMES_SUB = store_thm ("MOD_TIMES_SUB", 1948 ���!n q r. 0 < n /\ 0 < q /\ r <= n ==> ((q * n - r) MOD n = (n - r) MOD n)���, 1949 NTAC 2 STRIP_TAC THEN 1950 STRUCT_CASES_TAC (Q.SPEC `q` num_CASES) THEN1 1951 REWRITE_TAC [NOT_LESS_0] THEN 1952 REPEAT STRIP_TAC THEN 1953 FULL_SIMP_TAC bool_ss [MULT,LESS_EQ_ADD_SUB,MOD_TIMES]); 1954 1955val MOD_PLUS = store_thm ("MOD_PLUS", 1956 ���!n. 0<n ==> !j k. (((j MOD n) + (k MOD n)) MOD n) = ((j+k) MOD n)���, 1957 let fun SUBS th = SUBST_OCCS_TAC [([2],th)] 1958 in 1959 REPEAT STRIP_TAC THEN 1960 IMP_RES_TAC MOD_TIMES THEN 1961 IMP_RES_THEN (TRY o SUBS o SPEC (���j:num���)) DIVISION THEN 1962 ASM_REWRITE_TAC [SYM(SPEC_ALL ADD_ASSOC)] THEN 1963 PURE_ONCE_REWRITE_TAC [ADD_SYM] THEN 1964 IMP_RES_THEN (TRY o SUBS o SPEC (���k:num���)) DIVISION THEN 1965 ASM_REWRITE_TAC [SYM(SPEC_ALL ADD_ASSOC)] 1966 end); 1967 1968val MOD_MOD = store_thm ("MOD_MOD", 1969 ���!n. 0<n ==> (!k. (k MOD n) MOD n = (k MOD n))���, 1970 REPEAT STRIP_TAC THEN 1971 MATCH_MP_TAC LESS_MOD THEN 1972 IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC (���k:num���)) DIVISION); 1973 1974(* LESS_DIV_EQ_ZERO = |- !r n. r < n ==> (r DIV n = 0) *) 1975 1976val LESS_DIV_EQ_ZERO = save_thm ("LESS_DIV_EQ_ZERO", 1977 GENL [(���r:num���),(���n:num���)] (DISCH_ALL (PURE_REWRITE_RULE[MULT,ADD] 1978 (SPEC (���0���)(UNDISCH_ALL (SPEC_ALL DIV_MULT)))))); 1979 1980(* MULT_DIV = |- !n q. 0 < n ==> ((q * n) DIV n = q) *) 1981 1982val MULT_DIV = save_thm ("MULT_DIV", 1983 GEN_ALL (PURE_REWRITE_RULE[ADD_0] 1984 (CONV_RULE RIGHT_IMP_FORALL_CONV 1985 (SPECL[(���n:num���),(���0���)] DIV_MULT)))); 1986 1987val ADD_DIV_ADD_DIV = store_thm ("ADD_DIV_ADD_DIV", 1988���!n. 0 < n ==> !x r. ((((x * n) + r) DIV n) = x + (r DIV n))���, 1989 CONV_TAC (REDEPTH_CONV RIGHT_IMP_FORALL_CONV) 1990 THEN REPEAT GEN_TAC THEN ASM_CASES_TAC (���r < n���) THENL[ 1991 IMP_RES_THEN SUBST1_TAC LESS_DIV_EQ_ZERO THEN DISCH_TAC 1992 THEN PURE_ONCE_REWRITE_TAC[ADD_0] 1993 THEN MATCH_MP_TAC DIV_MULT THEN FIRST_ASSUM ACCEPT_TAC, 1994 DISCH_THEN (CHOOSE_TAC o (MATCH_MP (SPEC (���r:num���) DA))) 1995 THEN POP_ASSUM (CHOOSE_THEN STRIP_ASSUME_TAC) 1996 THEN SUBST1_TAC (ASSUME (���r = (q * n) + r'���)) 1997 THEN PURE_ONCE_REWRITE_TAC[ADD_ASSOC] 1998 THEN PURE_ONCE_REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] 1999 THEN IMP_RES_THEN (fn t => REWRITE_TAC[t]) DIV_MULT]); 2000 2001val ADD_DIV_RWT = store_thm ("ADD_DIV_RWT", 2002 ���!n. 0 < n ==> 2003 !m p. (m MOD n = 0) \/ (p MOD n = 0) ==> 2004 ((m + p) DIV n = m DIV n + p DIV n)���, 2005 REPEAT STRIP_TAC THEN 2006 IMP_RES_THEN (ASSUME_TAC o GSYM) DIVISION THEN 2007 MATCH_MP_TAC DIV_UNIQUE THENL [ 2008 Q.EXISTS_TAC `p MOD n` THEN 2009 ASM_REWRITE_TAC [RIGHT_ADD_DISTRIB, GSYM ADD_ASSOC, EQ_ADD_RCANCEL] THEN 2010 SIMP_TAC bool_ss [Once (GSYM ADD_0), SimpRHS] THEN 2011 FIRST_X_ASSUM (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC [], 2012 Q.EXISTS_TAC `m MOD n` THEN 2013 ASM_REWRITE_TAC [RIGHT_ADD_DISTRIB] THEN 2014 Q.SUBGOAL_THEN `p DIV n * n = p` SUBST1_TAC THENL [ 2015 SIMP_TAC bool_ss [Once (GSYM ADD_0), SimpLHS] THEN 2016 FIRST_X_ASSUM (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC [], 2017 ALL_TAC 2018 ] THEN 2019 Q.SUBGOAL_THEN `m DIV n * n + p + m MOD n = m DIV n * n + m MOD n + p` 2020 (fn th => ASM_REWRITE_TAC [th]) THEN 2021 REWRITE_TAC [GSYM ADD_ASSOC, EQ_ADD_LCANCEL] THEN 2022 MATCH_ACCEPT_TAC ADD_COMM 2023 ]); 2024 2025val NOT_MULT_LESS_0 = prove( 2026 (���!m n. 0<m /\ 0<n ==> 0 < m*n���), 2027 REPEAT INDUCT_TAC THEN REWRITE_TAC[NOT_LESS_0] 2028 THEN STRIP_TAC THEN REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES,LESS_0]); 2029 2030val MOD_MULT_MOD = store_thm ("MOD_MULT_MOD", 2031���!m n. 0<n /\ 0<m ==> !x. ((x MOD (n * m)) MOD n = x MOD n)���, 2032REPEAT GEN_TAC THEN DISCH_TAC 2033 THEN FIRST_ASSUM (ASSUME_TAC o (MATCH_MP NOT_MULT_LESS_0)) THEN GEN_TAC 2034 THEN POP_ASSUM(CHOOSE_TAC o (MATCH_MP(SPECL[���x:num���,���m * n���] DA))) 2035 THEN POP_ASSUM (CHOOSE_THEN STRIP_ASSUME_TAC) 2036 THEN SUBST1_TAC (ASSUME(���x = (q * (n * m)) + r���)) 2037 THEN POP_ASSUM (SUBST1_TAC o (SPEC (���q:num���)) o MATCH_MP MOD_MULT) 2038 THEN PURE_ONCE_REWRITE_TAC [MULT_SYM] 2039 THEN PURE_ONCE_REWRITE_TAC [GSYM MULT_ASSOC] 2040 THEN PURE_ONCE_REWRITE_TAC [MULT_SYM] 2041 THEN STRIP_ASSUME_TAC (ASSUME (���0 < n /\ 0 < m���)) 2042 THEN PURE_ONCE_REWRITE_TAC[UNDISCH_ALL(SPEC_ALL MOD_TIMES)] 2043 THEN REFL_TAC); 2044 2045(* |- !q. q DIV (SUC 0) = q *) 2046val DIV_ONE = save_thm ("DIV_ONE", 2047 GEN_ALL (REWRITE_RULE[REWRITE_RULE[ONE] MULT_RIGHT_1] 2048 (MP (SPECL [(���SUC 0���), (���q:num���)] MULT_DIV) 2049 (SPEC (���0���) LESS_0)))); 2050 2051val DIV_1 = save_thm ("DIV_1", REWRITE_RULE [SYM ONE] DIV_ONE); 2052 2053val DIVMOD_ID = store_thm ("DIVMOD_ID", 2054 ���!n. 0 < n ==> (n DIV n = 1) /\ (n MOD n = 0)���, 2055 REPEAT STRIP_TAC THENL [ 2056 MATCH_MP_TAC DIV_UNIQUE THEN Q.EXISTS_TAC `0` THEN 2057 ASM_REWRITE_TAC [MULT_CLAUSES, ADD_CLAUSES], 2058 MATCH_MP_TAC MOD_UNIQUE THEN Q.EXISTS_TAC `1` THEN 2059 ASM_REWRITE_TAC [MULT_CLAUSES, ADD_CLAUSES] 2060 ]); 2061 2062val Less_lemma = prove( 2063 ���!m n. m<n ==> ?p. (n = m + p) /\ 0<p���, 2064 GEN_TAC THEN INDUCT_TAC THENL[ 2065 REWRITE_TAC[NOT_LESS_0], 2066 REWRITE_TAC[LESS_THM] 2067 THEN DISCH_THEN (DISJ_CASES_THEN2 SUBST1_TAC ASSUME_TAC) THENL[ 2068 EXISTS_TAC (���SUC 0���) 2069 THEN REWRITE_TAC[LESS_0,ADD_CLAUSES], 2070 RES_TAC THEN EXISTS_TAC (���SUC p���) 2071 THEN ASM_REWRITE_TAC[ADD_CLAUSES,LESS_0]]]); 2072 2073val Less_MULT_lemma = prove( 2074 (���!r m p. 0<p ==> r<m ==> r < p*m���), 2075 let val lem1 = MATCH_MP LESS_LESS_EQ_TRANS 2076 (CONJ (SPEC (���m:num���) LESS_SUC_REFL) 2077 (SPECL[(���SUC m���), (���p * (SUC m)���)] LESS_EQ_ADD)) 2078 in 2079 GEN_TAC THEN REPEAT INDUCT_TAC THEN REWRITE_TAC[NOT_LESS_0] 2080 THEN DISCH_TAC THEN REWRITE_TAC[LESS_THM] 2081 THEN DISCH_THEN (DISJ_CASES_THEN2 SUBST1_TAC ASSUME_TAC) 2082 THEN PURE_ONCE_REWRITE_TAC[MULT] 2083 THEN PURE_ONCE_REWRITE_TAC[ADD_SYM] THENL[ 2084 ACCEPT_TAC lem1, 2085 ACCEPT_TAC (MATCH_MP LESS_TRANS (CONJ (ASSUME (���r < m���)) lem1))] 2086 end); 2087 2088val Less_MULT_ADD_lemma = prove( 2089 ���!m n r r'. 0<m /\ 0<n /\ r<m /\ r'<n ==> r'*m + r < n*m���, 2090 REPEAT STRIP_TAC 2091 THEN CHOOSE_THEN STRIP_ASSUME_TAC (MATCH_MP Less_lemma (ASSUME (���r<m���))) 2092 THEN CHOOSE_THEN STRIP_ASSUME_TAC (MATCH_MP Less_lemma (ASSUME (���r'<n���))) 2093 THEN ASM_REWRITE_TAC[] 2094 THEN PURE_ONCE_REWRITE_TAC[RIGHT_ADD_DISTRIB] 2095 THEN PURE_ONCE_REWRITE_TAC[ADD_SYM] 2096 THEN PURE_ONCE_REWRITE_TAC[LESS_MONO_ADD_EQ] 2097 THEN SUBST1_TAC (SYM (ASSUME(���m = r + p���))) 2098 THEN IMP_RES_TAC Less_MULT_lemma); 2099 2100val DIV_DIV_DIV_MULT = store_thm ("DIV_DIV_DIV_MULT", 2101 ���!m n. 0<m /\ 0<n ==> !x. ((x DIV m) DIV n = x DIV (m * n))���, 2102 CONV_TAC (ONCE_DEPTH_CONV RIGHT_IMP_FORALL_CONV) THEN REPEAT STRIP_TAC 2103 THEN REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN2 SUBST1_TAC ASSUME_TAC) 2104 (SPEC (���x:num���) (MATCH_MP DA (ASSUME (���0 < m���)))) 2105 THEN REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN2 SUBST1_TAC ASSUME_TAC) 2106 (SPEC (���q:num���) (MATCH_MP DA (ASSUME (���0 < n���)))) 2107 THEN IMP_RES_THEN (fn t => REWRITE_TAC[t]) DIV_MULT 2108 THEN IMP_RES_THEN (fn t => REWRITE_TAC[t]) DIV_MULT 2109 THEN PURE_ONCE_REWRITE_TAC[RIGHT_ADD_DISTRIB] 2110 THEN PURE_ONCE_REWRITE_TAC[GSYM MULT_ASSOC] 2111 THEN PURE_ONCE_REWRITE_TAC[GSYM ADD_ASSOC] 2112 THEN ASSUME_TAC (MATCH_MP NOT_MULT_LESS_0 2113 (CONJ (ASSUME (���0 < n���)) (ASSUME (���0 < m���)))) 2114 THEN CONV_TAC ((RAND_CONV o RAND_CONV) (REWR_CONV MULT_SYM)) 2115 THEN CONV_TAC SYM_CONV THEN PURE_ONCE_REWRITE_TAC[ADD_INV_0_EQ] 2116 THEN FIRST_ASSUM (fn t => REWRITE_TAC[MATCH_MP ADD_DIV_ADD_DIV t]) 2117 THEN PURE_ONCE_REWRITE_TAC[ADD_INV_0_EQ] 2118 THEN MATCH_MP_TAC LESS_DIV_EQ_ZERO 2119 THEN IMP_RES_TAC Less_MULT_ADD_lemma); 2120 2121val POS_ADD = prove( 2122 ���!m n. 0<m+n = 0<m \/ 0<n���, 2123 REPEAT GEN_TAC 2124 THEN STRUCT_CASES_TAC (SPEC (���m:num���) num_CASES) 2125 THEN STRUCT_CASES_TAC (SPEC (���n:num���) num_CASES) 2126 THEN ASM_REWRITE_TAC[ADD_CLAUSES,prim_recTheory.LESS_0]); 2127 2128val POS_MULT = prove( 2129 ���!m n. 0<m*n = 0<m /\ 0<n���, 2130 REPEAT GEN_TAC 2131 THEN STRUCT_CASES_TAC (SPEC (���m:num���) num_CASES) 2132 THEN STRUCT_CASES_TAC (SPEC (���n:num���) num_CASES) 2133 THEN ASM_REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES,prim_recTheory.LESS_0]); 2134 2135local 2136 open prim_recTheory 2137in 2138 val SUC_PRE = store_thm ("SUC_PRE", 2139 ���0 < m <=> (SUC (PRE m) = m)���, 2140 STRUCT_CASES_TAC (SPEC (���m:num���) num_CASES) THEN 2141 REWRITE_TAC [PRE,NOT_LESS_0,LESS_0,NOT_SUC]) 2142end 2143 2144val LESS_MONO_LEM = 2145GEN_ALL 2146 (REWRITE_RULE [ADD_CLAUSES] 2147 (SPECL (map Term [`0`, `y:num`, `x:num`]) 2148 (ONCE_REWRITE_RULE[ADD_SYM]LESS_MONO_ADD))); 2149 2150val DIV_LESS = store_thm ("DIV_LESS", 2151 ���!n d. 0<n /\ 1<d ==> n DIV d < n���, 2152 REWRITE_TAC [ONE] THEN REPEAT STRIP_TAC 2153 THEN IMP_RES_TAC prim_recTheory.SUC_LESS 2154 THEN CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC 2155 (SPEC(���n:num���) (UNDISCH(SPEC(���d:num���) DIVISION))) 2156 THEN RULE_ASSUM_TAC (REWRITE_RULE [POS_ADD]) 2157 THEN MP_TAC (SPEC (���d:num���) ADD_DIV_ADD_DIV) THEN ASM_REWRITE_TAC[] 2158 THEN DISCH_THEN (fn th => REWRITE_TAC [th]) 2159 THEN MP_TAC (SPECL (map Term [`n MOD d`, `d:num`]) LESS_DIV_EQ_ZERO) 2160 THEN ASM_REWRITE_TAC [] 2161 THEN DISCH_THEN (fn th => REWRITE_TAC [th,ADD_CLAUSES]) 2162 THEN SUBGOAL_THEN (���?m. d = SUC m���) (CHOOSE_THEN SUBST_ALL_TAC) THENL 2163 [EXISTS_TAC (���PRE d���) THEN IMP_RES_TAC SUC_PRE THEN ASM_REWRITE_TAC[], 2164 REWRITE_TAC [MULT_CLAUSES,GSYM ADD_ASSOC] 2165 THEN MATCH_MP_TAC LESS_MONO_LEM 2166 THEN PAT_ASSUM (���x \/ y���) MP_TAC 2167 THEN REWRITE_TAC[POS_ADD,POS_MULT] THEN STRIP_TAC THENL 2168 [DISJ1_TAC THEN RULE_ASSUM_TAC (REWRITE_RULE[LESS_MONO_EQ]), ALL_TAC] 2169 THEN ASM_REWRITE_TAC[]]); 2170 2171val MOD_LESS = Q.store_thm ("MOD_LESS", 2172 `!m n. 0 < n ==> m MOD n < n`, 2173 METIS_TAC [DIVISION]); 2174 2175val ADD_MODULUS = Q.store_thm ("ADD_MODULUS", 2176`(!n x. 0 < n ==> ((x + n) MOD n = x MOD n)) /\ 2177 (!n x. 0 < n ==> ((n + x) MOD n = x MOD n))`, 2178 METIS_TAC [ADD_SYM,MOD_PLUS,DIVMOD_ID,MOD_MOD,ADD_CLAUSES]); 2179 2180val ADD_MODULUS_LEFT = save_thm ("ADD_MODULUS_LEFT",CONJUNCT1 ADD_MODULUS); 2181val ADD_MODULUS_RIGHT = save_thm ("ADD_MODULUS_RIGHT",CONJUNCT2 ADD_MODULUS); 2182 2183val DIV_P = store_thm ("DIV_P", 2184 ���!P p q. 0 < q ==> 2185 (P (p DIV q) = ?k r. (p = k * q + r) /\ r < q /\ P k)���, 2186 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 2187 MAP_EVERY Q.EXISTS_TAC [`p DIV q`, `p MOD q`] THEN 2188 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC DIVISION THEN 2189 FIRST_ASSUM ACCEPT_TAC, 2190 Q.SUBGOAL_THEN `p DIV q = k` (fn th => SUBST1_TAC th THEN 2191 FIRST_ASSUM ACCEPT_TAC) THEN 2192 MATCH_MP_TAC DIV_UNIQUE THEN Q.EXISTS_TAC `r` THEN ASM_REWRITE_TAC [] 2193 ]); 2194 2195val DIV_P_UNIV = store_thm ("DIV_P_UNIV", 2196 ���!P m n. 0 < n ==> (P (m DIV n) = !q r. (m = q * n + r) /\ r < n ==> P q)���, 2197 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2198 Q_TAC SUFF_TAC `m DIV n = q` 2199 THEN1 (DISCH_THEN (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC []) THEN 2200 MATCH_MP_TAC DIV_UNIQUE THEN Q.EXISTS_TAC `r` THEN ASM_REWRITE_TAC [], 2201 FIRST_X_ASSUM MATCH_MP_TAC THEN Q.EXISTS_TAC `m MOD n` THEN 2202 MATCH_MP_TAC DIVISION THEN ASM_REWRITE_TAC [] 2203 ]); 2204 2205val MOD_P = store_thm ("MOD_P", 2206 ���!P p q. 0 < q ==> 2207 (P (p MOD q) = ?k r. (p = k * q + r) /\ r < q /\ P r)���, 2208 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 2209 MAP_EVERY Q.EXISTS_TAC [`p DIV q`, `p MOD q`] THEN 2210 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC DIVISION THEN 2211 FIRST_ASSUM ACCEPT_TAC, 2212 Q.SUBGOAL_THEN `p MOD q = r` (fn th => SUBST1_TAC th THEN 2213 FIRST_ASSUM ACCEPT_TAC) THEN 2214 MATCH_MP_TAC MOD_UNIQUE THEN Q.EXISTS_TAC `k` THEN ASM_REWRITE_TAC [] 2215 ]); 2216 2217val MOD_P_UNIV = store_thm ("MOD_P_UNIV", 2218 ���!P m n. 0 < n ==> 2219 (P (m MOD n) = !q r. (m = q * n + r) /\ r < n ==> P r)���, 2220 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2221 Q_TAC SUFF_TAC `m MOD n = r` 2222 THEN1 (DISCH_THEN (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC []) THEN 2223 MATCH_MP_TAC MOD_UNIQUE THEN Q.EXISTS_TAC `q` THEN ASM_REWRITE_TAC [], 2224 FIRST_X_ASSUM MATCH_MP_TAC THEN Q.EXISTS_TAC `m DIV n` THEN 2225 MATCH_MP_TAC DIVISION THEN ASM_REWRITE_TAC [] 2226 ]); 2227 2228(* Could generalise this to work over arbitrary operators by making the 2229 commutativity and associativity theorems parameters. It seems OTT 2230 enough as it is. *) 2231fun move_var_left s = let 2232 val v = mk_var(s, ���:num���) 2233 val th1 = GSYM (SPEC v MULT_COMM) (* xv = vx *) 2234 val th2 = GSYM (SPEC v MULT_ASSOC) (* (vx)y = v(xy) *) 2235 val th3 = CONV_RULE (* x(vy) = v(xy) *) 2236 (STRIP_QUANT_CONV 2237 (LAND_CONV (LAND_CONV (REWR_CONV MULT_COMM) THENC 2238 REWR_CONV (GSYM MULT_ASSOC)))) th2 2239in 2240 (* The complicated conversion at the heart of this could be replaced with 2241 REWRITE_CONV if that procedure was modified to dynamically throw 2242 away rewrites that on instantiation turn out to be loops, which it 2243 could do by wrapping its REWR_CONVs in CHANGED_CONVs. Perhaps this 2244 would be inefficient. *) 2245 FREEZE_THEN 2246 (fn th1 => FREEZE_THEN 2247 (fn th2 => FREEZE_THEN 2248 (fn th3 => CONV_TAC 2249 (REDEPTH_CONV 2250 (FIRST_CONV 2251 (map (CHANGED_CONV o REWR_CONV) 2252 [th1, th2, th3])))) th3) th2) th1 2253end 2254 2255val MOD_TIMES2 = store_thm ("MOD_TIMES2", 2256 ���!n. 0 < n ==> 2257 !j k. (j MOD n * k MOD n) MOD n = (j * k) MOD n���, 2258 REPEAT STRIP_TAC THEN 2259 IMP_RES_THEN (Q.SPEC_THEN `j` STRIP_ASSUME_TAC) DIVISION THEN 2260 IMP_RES_THEN (Q.SPEC_THEN `k` STRIP_ASSUME_TAC) DIVISION THEN 2261 Q.ABBREV_TAC `q = j DIV n` THEN POP_ASSUM (K ALL_TAC) THEN 2262 Q.ABBREV_TAC `r = j MOD n` THEN POP_ASSUM (K ALL_TAC) THEN 2263 Q.ABBREV_TAC `u = k DIV n` THEN POP_ASSUM (K ALL_TAC) THEN 2264 Q.ABBREV_TAC `v = k MOD n` THEN POP_ASSUM (K ALL_TAC) THEN 2265 NTAC 2 (FIRST_X_ASSUM SUBST_ALL_TAC) THEN 2266 REWRITE_TAC [LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB, ADD_ASSOC] THEN 2267 move_var_left "n" THEN REWRITE_TAC [GSYM LEFT_ADD_DISTRIB] THEN 2268 ONCE_REWRITE_TAC [MULT_COMM] THEN 2269 IMP_RES_THEN (fn th => REWRITE_TAC [th]) MOD_TIMES); 2270 2271val MOD_COMMON_FACTOR = store_thm ("MOD_COMMON_FACTOR", 2272 ���!n p q. 0 < n /\ 0 < q ==> (n * (p MOD q) = (n * p) MOD (n * q))���, 2273 REPEAT STRIP_TAC THEN Q.SPEC_THEN `q` MP_TAC DIVISION THEN 2274 ASM_REWRITE_TAC [] THEN DISCH_THEN (Q.SPEC_THEN `p` STRIP_ASSUME_TAC) THEN 2275 Q.ABBREV_TAC `u = p DIV q` THEN POP_ASSUM (K ALL_TAC) THEN 2276 Q.ABBREV_TAC `v = p MOD q` THEN POP_ASSUM (K ALL_TAC) THEN 2277 FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC [LEFT_ADD_DISTRIB] THEN 2278 move_var_left "u" THEN 2279 ASM_SIMP_TAC bool_ss [MOD_TIMES, LESS_MULT2] THEN 2280 SUFF_TAC ���n * v < n * q��� THENL [mesonLib.MESON_TAC [LESS_MOD], 2281 ALL_TAC] THEN 2282 SUFF_TAC ���?m. n = SUC m��� THENL [ 2283 STRIP_TAC THEN ASM_REWRITE_TAC [LESS_MULT_MONO], 2284 mesonLib.ASM_MESON_TAC [LESS_REFL, num_CASES] 2285 ]); 2286 2287val X_MOD_Y_EQ_X = store_thm ("X_MOD_Y_EQ_X", 2288 ���!x y. 0 < y ==> ((x MOD y = x) = x < y)���, 2289 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 2290 mesonLib.ASM_MESON_TAC [DIVISION], 2291 STRIP_TAC THEN MATCH_MP_TAC MOD_UNIQUE THEN 2292 Q.EXISTS_TAC `0` THEN ASM_REWRITE_TAC [MULT_CLAUSES, ADD_CLAUSES] 2293 ]); 2294 2295val DIV_LE_MONOTONE = store_thm ("DIV_LE_MONOTONE", 2296 ���!n x y. 0 < n /\ x <= y ==> x DIV n <= y DIV n���, 2297 REPEAT STRIP_TAC THEN 2298 Q.SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THENL [ 2299 ASM_REWRITE_TAC [NOT_ZERO_LT_ZERO], 2300 ALL_TAC 2301 ] THEN 2302 Q.SPEC_THEN `n` MP_TAC DIVISION THEN ASM_REWRITE_TAC [] THEN 2303 DISCH_THEN (fn th => Q.SPEC_THEN `x` STRIP_ASSUME_TAC th THEN 2304 Q.SPEC_THEN `y` STRIP_ASSUME_TAC th) THEN 2305 Q.ABBREV_TAC `q = x DIV n` THEN POP_ASSUM (K ALL_TAC) THEN 2306 Q.ABBREV_TAC `r = y DIV n` THEN POP_ASSUM (K ALL_TAC) THEN 2307 Q.ABBREV_TAC `d = x MOD n` THEN POP_ASSUM (K ALL_TAC) THEN 2308 Q.ABBREV_TAC `e = y MOD n` THEN POP_ASSUM (K ALL_TAC) THEN 2309 SRW_TAC [][] THEN CCONTR_TAC THEN 2310 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [NOT_LEQ]) THEN (* SUC r < q *) 2311 Q.SPECL_THEN [`SUC r`, `n`, `q`] MP_TAC LE_MULT_RCANCEL THEN 2312 ASM_REWRITE_TAC [] THEN STRIP_TAC THEN (* SUC r * n <= q * n *) 2313 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [MULT_CLAUSES]) THEN 2314 (* r * n + n <= q * n *) 2315 Q.SPECL_THEN [`e`, `n`, `r * n`] MP_TAC LT_ADD_LCANCEL THEN 2316 ASM_REWRITE_TAC [] THEN STRIP_TAC THEN (* r * n + e < r * n + n *) 2317 Q.SPECL_THEN [`q * n`, `d`] ASSUME_TAC LESS_EQ_ADD THEN 2318 (* q * n <= q * n + d *) 2319 Q.SUBGOAL_THEN `r * n + e < r * n + e` (CONTR_TAC o MATCH_MP LESS_REFL) THEN 2320 MATCH_MP_TAC LESS_LESS_EQ_TRANS THEN Q.EXISTS_TAC `q * n + d` THEN 2321 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC LESS_LESS_EQ_TRANS THEN 2322 Q.EXISTS_TAC `r * n + n` THEN ASM_REWRITE_TAC [] THEN 2323 MATCH_MP_TAC LESS_EQ_TRANS THEN Q.EXISTS_TAC `q * n` THEN 2324 ASM_REWRITE_TAC []); 2325 2326val LE_LT1 = store_thm ("LE_LT1", 2327 ���!x y. x <= y = x < y + 1���, 2328 REWRITE_TAC [LESS_OR_EQ, GSYM ADD1, 2329 IMP_ANTISYM_RULE (SPEC_ALL prim_recTheory.LESS_LEMMA1) 2330 (SPEC_ALL prim_recTheory.LESS_LEMMA2)] THEN 2331 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC []) 2332 2333val X_LE_DIV = store_thm ("X_LE_DIV", 2334 ���!x y z. 0 < z ==> (x <= y DIV z = x * z <= y)���, 2335 REPEAT STRIP_TAC THEN 2336 Q.SPEC_THEN `z` MP_TAC DIVISION THEN 2337 ASM_REWRITE_TAC [] THEN 2338 DISCH_THEN (Q.SPEC_THEN `y` STRIP_ASSUME_TAC) THEN 2339 Q.ABBREV_TAC `q = y DIV z` THEN 2340 Q.ABBREV_TAC `r = y MOD z` THEN ASM_REWRITE_TAC [] THEN EQ_TAC THENL [ 2341 STRIP_TAC THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 2342 Q.EXISTS_TAC `q * z` THEN 2343 ASM_SIMP_TAC bool_ss [LE_MULT_RCANCEL, LESS_EQ_ADD], 2344 STRIP_TAC THEN REWRITE_TAC [LE_LT1] THEN 2345 Q_TAC SUFF_TAC `x * z < (q + 1) * z` 2346 THEN1 SIMP_TAC bool_ss [LT_MULT_RCANCEL] THEN 2347 REWRITE_TAC [RIGHT_ADD_DISTRIB, 2348 MULT_CLAUSES] THEN 2349 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN 2350 Q.EXISTS_TAC `q * z + r` THEN 2351 ASM_SIMP_TAC bool_ss [LT_ADD_LCANCEL] 2352 ]); 2353 2354val X_LT_DIV = store_thm ("X_LT_DIV", 2355 ���!x y z. 0 < z ==> (x < y DIV z = (x + 1) * z <= y)���, 2356 REPEAT STRIP_TAC THEN 2357 Q.SPEC_THEN `z` MP_TAC DIVISION THEN 2358 ASM_REWRITE_TAC [] THEN 2359 DISCH_THEN (Q.SPEC_THEN `y` STRIP_ASSUME_TAC) THEN 2360 Q.ABBREV_TAC `q = y DIV z` THEN 2361 Q.ABBREV_TAC `r = y MOD z` THEN ASM_REWRITE_TAC [] THEN EQ_TAC THENL [ 2362 STRIP_TAC THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 2363 Q.EXISTS_TAC `q * z` THEN 2364 ASM_SIMP_TAC bool_ss [LE_MULT_RCANCEL, LESS_EQ_ADD] THEN 2365 ASM_SIMP_TAC bool_ss [LE_LT1, LT_ADD_RCANCEL], 2366 STRIP_TAC THEN 2367 CCONTR_TAC THEN 2368 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [NOT_LESS]) THEN 2369 Q.SUBGOAL_THEN `(x + 1) * z <= x * z + r` ASSUME_TAC THENL [ 2370 MATCH_MP_TAC LESS_EQ_TRANS THEN 2371 Q.EXISTS_TAC `q * z + r` THEN 2372 ASM_SIMP_TAC bool_ss [LE_ADD_RCANCEL, LE_MULT_RCANCEL], 2373 POP_ASSUM MP_TAC THEN 2374 ASM_REWRITE_TAC [RIGHT_ADD_DISTRIB, MULT_CLAUSES, 2375 LE_ADD_LCANCEL, GSYM NOT_LESS, 2376 LT_ADD_LCANCEL] 2377 ] 2378 ]); 2379 2380val DIV_LT_X = store_thm ("DIV_LT_X", 2381 ���!x y z. 0 < z ==> (y DIV z < x = y < x * z)���, 2382 REPEAT STRIP_TAC THEN 2383 REWRITE_TAC [GSYM NOT_LESS_EQUAL] THEN 2384 AP_TERM_TAC THEN MATCH_MP_TAC X_LE_DIV THEN 2385 ASM_REWRITE_TAC []); 2386 2387val DIV_LE_X = store_thm ("DIV_LE_X", 2388 ���!x y z. 0 < z ==> (y DIV z <= x = y < (x + 1) * z)���, 2389 REPEAT STRIP_TAC THEN 2390 CONV_TAC (FORK_CONV (REWR_CONV (GSYM NOT_LESS), 2391 REWR_CONV (GSYM NOT_LESS_EQUAL))) THEN 2392 AP_TERM_TAC THEN MATCH_MP_TAC X_LT_DIV THEN 2393 ASM_REWRITE_TAC []); 2394 2395val DIV_EQ_X = store_thm ("DIV_EQ_X", 2396 ���!x y z. 0 < z ==> ((y DIV z = x) = x * z <= y /\ y < SUC x * z)���, 2397 SIMP_TAC bool_ss [EQ_LESS_EQ,DIV_LE_X,X_LE_DIV,GSYM ADD1, 2398 AC CONJ_COMM CONJ_ASSOC]); 2399 2400val DIV_MOD_MOD_DIV = store_thm ("DIV_MOD_MOD_DIV", 2401 ���!m n k. 0 < n /\ 0 < k ==> ((m DIV n) MOD k = (m MOD (n * k)) DIV n)���, 2402 REPEAT STRIP_TAC THEN 2403 Q.SUBGOAL_THEN `0 < n * k` ASSUME_TAC THENL [ 2404 ASM_REWRITE_TAC [ZERO_LESS_MULT], 2405 ALL_TAC 2406 ] THEN 2407 Q.SPEC_THEN `n * k` MP_TAC DIVISION THEN 2408 ASM_REWRITE_TAC [] THEN DISCH_THEN (Q.SPEC_THEN `m` STRIP_ASSUME_TAC) THEN 2409 Q.ABBREV_TAC `q = m DIV (n * k)` THEN 2410 Q.ABBREV_TAC `r = m MOD (n * k)` THEN 2411 markerLib.RM_ALL_ABBREVS_TAC THEN 2412 ASM_REWRITE_TAC [] THEN 2413 Q.SUBGOAL_THEN `q * (n * k) = (q * k) * n` SUBST1_TAC THENL [ 2414 SIMP_TAC bool_ss [AC MULT_ASSOC MULT_COMM], 2415 ALL_TAC 2416 ] THEN ASM_SIMP_TAC bool_ss [ADD_DIV_ADD_DIV, MOD_TIMES] THEN 2417 MATCH_MP_TAC LESS_MOD THEN ASM_SIMP_TAC bool_ss [DIV_LT_X] THEN 2418 FULL_SIMP_TAC bool_ss [AC MULT_ASSOC MULT_COMM]); 2419 2420(* useful if x and z are both constants *) 2421val MULT_EQ_DIV = store_thm ("MULT_EQ_DIV", 2422 ���0 < x ==> ((x * y = z) = (y = z DIV x) /\ (z MOD x = 0))���, 2423 STRIP_TAC THEN EQ_TAC THENL [ 2424 DISCH_THEN (SUBST_ALL_TAC o SYM) THEN 2425 ONCE_REWRITE_TAC [MULT_COMM] THEN 2426 ASM_SIMP_TAC bool_ss [MOD_EQ_0, MULT_DIV], 2427 Q.SPEC_THEN `x` MP_TAC DIVISION THEN ASM_REWRITE_TAC [] THEN 2428 DISCH_THEN (Q.SPEC_THEN `z` STRIP_ASSUME_TAC) THEN 2429 REPEAT STRIP_TAC THEN 2430 FULL_SIMP_TAC bool_ss [ADD_CLAUSES, MULT_COMM] THEN 2431 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN FIRST_ASSUM ACCEPT_TAC 2432 ]); 2433 2434(* as they are here *) 2435val NUMERAL_MULT_EQ_DIV = store_thm ("NUMERAL_MULT_EQ_DIV", 2436 ���((NUMERAL (BIT1 x) * y = NUMERAL z) = 2437 (y = NUMERAL z DIV NUMERAL (BIT1 x)) /\ 2438 (NUMERAL z MOD NUMERAL(BIT1 x) = 0)) /\ 2439 ((NUMERAL (BIT2 x) * y = NUMERAL z) = 2440 (y = NUMERAL z DIV NUMERAL (BIT2 x)) /\ 2441 (NUMERAL z MOD NUMERAL(BIT2 x) = 0))���, 2442 CONJ_TAC THEN MATCH_MP_TAC MULT_EQ_DIV THEN 2443 REWRITE_TAC [NUMERAL_DEF, BIT1, BIT2, ADD_CLAUSES, LESS_0]); 2444 2445val MOD_EQ_0_DIVISOR = Q.store_thm ("MOD_EQ_0_DIVISOR", 2446`0 < n ==> ((k MOD n = 0) = (?d. k = d * n))`, 2447DISCH_TAC THEN 2448EQ_TAC THEN1 ( 2449 DISCH_TAC THEN 2450 EXISTS_TAC ���k DIV n��� THEN 2451 MATCH_MP_TAC EQ_SYM THEN 2452 SRW_TAC [][Once MULT_SYM] THEN 2453 MATCH_MP_TAC (MP_CANON (DISCH_ALL (#2(EQ_IMP_RULE (UNDISCH MULT_EQ_DIV))))) THEN 2454 SRW_TAC [][] ) THEN 2455SRW_TAC [][] THEN SRW_TAC [][MOD_EQ_0]) 2456 2457val MOD_SUC = Q.store_thm ("MOD_SUC", 2458`0 < y /\ (SUC x <> (SUC (x DIV y)) * y) ==> ((SUC x) MOD y = SUC (x MOD y))`, 2459STRIP_TAC THEN 2460MATCH_MP_TAC MOD_UNIQUE THEN 2461Q.EXISTS_TAC `x DIV y` THEN 2462`x = x DIV y * y + x MOD y` by PROVE_TAC [DIVISION] THEN 2463`x MOD y < y` by PROVE_TAC [MOD_LESS] THEN 2464FULL_SIMP_TAC bool_ss [prim_recTheory.INV_SUC_EQ,ADD_CLAUSES,MULT_CLAUSES] THEN 2465MATCH_MP_TAC LESS_NOT_SUC THEN 2466CONJ_TAC THEN1 FIRST_ASSUM ACCEPT_TAC THEN 2467SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 2468`SUC x = SUC (x DIV y * y + x MOD y)` by ( 2469 AP_TERM_TAC THEN FIRST_ASSUM ACCEPT_TAC ) THEN 2470FULL_SIMP_TAC bool_ss [ADD_SUC] THEN 2471PROVE_TAC [] ) 2472 2473val MOD_SUC_IFF = Q.store_thm ("MOD_SUC_IFF", 2474 `0 < y ==> ((SUC x MOD y = SUC (x MOD y)) <=> (SUC x <> SUC (x DIV y) * y))`, 2475 PROVE_TAC [MOD_SUC,SUC_NOT,MOD_EQ_0]) 2476 2477val ONE_MOD = Q.store_thm ("ONE_MOD", 2478 `1 < n ==> (1 MOD n = 1)`, 2479 STRIP_TAC THEN 2480 `0 < n` by ( 2481 MATCH_MP_TAC LESS_TRANS THEN 2482 EXISTS_TAC ���1��� THEN 2483 SRW_TAC [][LESS_SUC_REFL,ONE] ) THEN 2484 SUFF_TAC ���SUC 0 MOD n = SUC (0 MOD n)��� THEN1 2485 SRW_TAC [][ZERO_MOD,ONE] THEN 2486 MATCH_MP_TAC MOD_SUC THEN 2487 SRW_TAC [][ZERO_DIV,MULT,ADD,LESS_NOT_EQ,GSYM ONE]) 2488 2489val ONE_MOD_IFF = Q.store_thm ("ONE_MOD_IFF", 2490 `1 < n <=> 0 < n /\ (1 MOD n = 1)`, 2491 EQ_TAC THEN1 ( 2492 SRW_TAC [][ONE_MOD] THEN 2493 MATCH_MP_TAC LESS_TRANS THEN 2494 EXISTS_TAC ���1��� THEN 2495 SRW_TAC [][LESS_SUC_REFL,ONE] ) THEN 2496 STRUCT_CASES_TAC (SPEC ���n:num��� num_CASES) THEN1 ( 2497 SIMP_TAC bool_ss [LESS_REFL] ) THEN 2498 SIMP_TAC bool_ss [ONE] THEN 2499 STRIP_TAC THEN 2500 MATCH_MP_TAC LESS_MONO THEN 2501 Q.MATCH_RENAME_TAC `0 < m` THEN 2502 FULL_STRUCT_CASES_TAC (SPEC ���m:num��� num_CASES) THEN1 ( 2503 FULL_SIMP_TAC bool_ss [MOD_ONE,SUC_NOT] ) THEN 2504 SIMP_TAC bool_ss [LESS_0]) 2505 2506val MOD_LESS_EQ = Q.store_thm ("MOD_LESS_EQ", 2507 `0 < y ==> x MOD y <= x`, 2508 STRIP_TAC THEN 2509 Cases_on `x < y` THEN1 ( 2510 MATCH_MP_TAC (snd (EQ_IMP_RULE (SPEC_ALL LESS_OR_EQ))) THEN 2511 DISJ2_TAC THEN 2512 MATCH_MP_TAC LESS_MOD THEN 2513 POP_ASSUM ACCEPT_TAC ) THEN 2514 MATCH_MP_TAC LESS_EQ_TRANS THEN 2515 Q.EXISTS_TAC `y` THEN 2516 CONJ_TAC THEN1 ( 2517 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN 2518 MATCH_MP_TAC MOD_LESS THEN 2519 FIRST_ASSUM ACCEPT_TAC ) THEN 2520 IMP_RES_TAC NOT_LESS) 2521 2522val MOD_LIFT_PLUS = Q.store_thm ("MOD_LIFT_PLUS", 2523 `0 < n /\ k < n - x MOD n ==> ((x + k) MOD n = x MOD n + k)`, 2524 Q.ID_SPEC_TAC `k` THEN INDUCT_TAC THEN1 ( 2525 SIMP_TAC bool_ss [ADD_0] ) THEN 2526 STRIP_TAC THEN 2527 `x + SUC k = SUC (x + k)` by ( 2528 SIMP_TAC bool_ss [ADD_CLAUSES] ) THEN 2529 `k < n - x MOD n` by ( 2530 MATCH_MP_TAC prim_recTheory.SUC_LESS THEN 2531 FIRST_ASSUM ACCEPT_TAC ) THEN 2532 FULL_SIMP_TAC bool_ss [] THEN 2533 MATCH_MP_TAC EQ_TRANS THEN 2534 Q.EXISTS_TAC `SUC (x MOD n + k)` THEN 2535 CONJ_TAC THEN1 ( 2536 MATCH_MP_TAC EQ_TRANS THEN 2537 Q.EXISTS_TAC `SUC ((x + k) MOD n)` THEN 2538 CONJ_TAC THEN1 ( 2539 MATCH_MP_TAC MOD_SUC THEN 2540 CONJ_TAC THEN1 FIRST_ASSUM ACCEPT_TAC THEN 2541 FULL_SIMP_TAC bool_ss [ADD_SYM,ADD,SUB_LEFT_LESS,MULT_CLAUSES] THEN 2542 `SUC ((k + x) MOD n + (k + x) DIV n * n) < n + (k + x) DIV n * n` 2543 by PROVE_TAC [LESS_MONO_ADD,ADD_SUC,ADD_SYM] THEN 2544 PROVE_TAC [DIVISION,ADD_SYM,LESS_REFL]) THEN 2545 AP_TERM_TAC THEN 2546 FIRST_ASSUM ACCEPT_TAC) THEN 2547 SIMP_TAC bool_ss [ADD_SUC]) 2548 2549val MOD_LIFT_PLUS_IFF = Q.store_thm ("MOD_LIFT_PLUS_IFF", 2550 `0 < n ==> (((x + k) MOD n = x MOD n + k) = (k < n - x MOD n))`, 2551 PROVE_TAC [SUB_LEFT_LESS,ADD_SYM,MOD_LESS,MOD_LIFT_PLUS]) 2552 2553(* ---------------------------------------------------------------------- 2554 Some additional theorems (nothing to do with DIV and MOD) 2555 ---------------------------------------------------------------------- *) 2556 2557val num_case_cong = 2558 save_thm ("num_case_cong", Prim_rec.case_cong_thm num_CASES num_case_def); 2559 2560val SUC_ELIM_THM = store_thm ("SUC_ELIM_THM", 2561 (���!P. (!n. P (SUC n) n) = (!n. (0 < n ==> P n (n-1)))���), 2562 GEN_TAC THEN EQ_TAC THENL [ 2563 REPEAT STRIP_TAC THEN 2564 FIRST_ASSUM (MP_TAC o SPEC (���n-1���)) THEN 2565 SIMP_TAC bool_ss [SUB_LEFT_SUC, ONE, SUB_MONO_EQ, SUB_0, 2566 GSYM NOT_LESS] THEN 2567 COND_CASES_TAC THENL [ 2568 STRIP_ASSUME_TAC (SPECL [���n:num���, ���SUC 0���] LESS_LESS_CASES) 2569 THENL [ 2570 FULL_SIMP_TAC bool_ss [], 2571 IMP_RES_TAC LESS_LESS_SUC 2572 ], 2573 REWRITE_TAC [] 2574 ], 2575 REPEAT STRIP_TAC THEN 2576 FIRST_ASSUM (MP_TAC o SPEC (���n+1���)) THEN 2577 SIMP_TAC bool_ss [GSYM ADD1, SUC_SUB1, LESS_0] 2578 ]); 2579 2580val SUC_ELIM_NUMERALS = store_thm ("SUC_ELIM_NUMERALS", 2581 ���!f g. (!n. g (SUC n) = f n (SUC n)) = 2582 (!n. g (NUMERAL (BIT1 n)) = 2583 f (NUMERAL (BIT1 n) - 1) (NUMERAL (BIT1 n))) /\ 2584 (!n. g (NUMERAL (BIT2 n)) = 2585 f (NUMERAL (BIT1 n)) (NUMERAL (BIT2 n)))���, 2586 REPEAT GEN_TAC THEN EQ_TAC THEN 2587 SIMP_TAC bool_ss [NUMERAL_DEF, BIT1, BIT2, ALT_ZERO, 2588 ADD_CLAUSES, SUB_MONO_EQ, SUB_0] THEN 2589 REPEAT STRIP_TAC THEN 2590 Q.SPEC_THEN `n` STRIP_ASSUME_TAC EVEN_OR_ODD THEN 2591 POP_ASSUM (Q.X_CHOOSE_THEN `m` SUBST_ALL_TAC o 2592 REWRITE_RULE [EVEN_EXISTS, ODD_EXISTS, TIMES2]) THEN 2593 ASM_REWRITE_TAC []); 2594 2595val ADD_SUBR2 = prove( 2596 ���!m n. m - (m + n) = 0���, 2597 REWRITE_TAC [SUB_EQ_0, LESS_EQ_ADD]); 2598 2599val SUB_ELIM_THM = store_thm ("SUB_ELIM_THM", 2600 ���P (a - b) = !d. ((b = a + d) ==> P 0) /\ ((a = b + d) ==> P d)���, 2601 DISJ_CASES_TAC(SPECL [���a:num���, ���b:num���] LESS_EQ_CASES) THEN 2602 FIRST_ASSUM(X_CHOOSE_TAC (���e:num���) o REWRITE_RULE[LESS_EQ_EXISTS]) THEN 2603 ASM_REWRITE_TAC[ADD_SUB, ONCE_REWRITE_RULE [ADD_SYM] ADD_SUB, ADD_SUBR2] THEN 2604 REWRITE_TAC [ONCE_REWRITE_RULE [ADD_SYM] EQ_MONO_ADD_EQ] THEN 2605 CONV_TAC (DEPTH_CONV FORALL_AND_CONV) THEN 2606 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [EQ_SYM_EQ] THEN 2607 REWRITE_TAC[GSYM ADD_ASSOC, ADD_INV_0_EQ, ADD_EQ_0] THENL 2608 [EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 2609 FIRST_ASSUM(fn th => MATCH_MP_TAC th THEN EXISTS_TAC (���e:num���)), 2610 EQ_TAC THENL 2611 [DISCH_TAC THEN CONJ_TAC THEN GEN_TAC THEN 2612 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN SUBST_ALL_TAC), 2613 DISCH_THEN(MATCH_MP_TAC o CONJUNCT2)]] THEN 2614 ASM_REWRITE_TAC[]); 2615 2616val PRE_ELIM_THM = store_thm ("PRE_ELIM_THM", 2617 ���P (PRE n) = !m. ((n = 0) ==> P 0) /\ ((n = SUC m) ==> P m)���, 2618 SPEC_TAC(���n:num���,���n:num���) THEN INDUCT_TAC THEN 2619 REWRITE_TAC[NOT_SUC, INV_SUC_EQ, GSYM NOT_SUC, PRE] THEN 2620 EQ_TAC THEN REPEAT STRIP_TAC THENL 2621 [FIRST_ASSUM(SUBST1_TAC o SYM) THEN FIRST_ASSUM ACCEPT_TAC, 2622 FIRST_ASSUM MATCH_MP_TAC THEN REFL_TAC]); 2623 2624val _ = print "Additional properties of EXP\n" 2625 2626val MULT_INCREASES = store_thm ("MULT_INCREASES", 2627 ���!m n. 1 < m /\ 0 < n ==> SUC n <= m * n���, 2628 INDUCT_TAC THENL [ 2629 REWRITE_TAC [NOT_LESS_0], 2630 REWRITE_TAC [MULT, GSYM LESS_EQ] THEN REPEAT STRIP_TAC THEN 2631 ONCE_REWRITE_TAC [ADD_COMM] THEN MATCH_MP_TAC LESS_ADD_NONZERO THEN 2632 REWRITE_TAC [MULT_EQ_0] THEN STRIP_TAC THEN 2633 POP_ASSUM SUBST_ALL_TAC THEN 2634 RULE_ASSUM_TAC (REWRITE_RULE [ONE, LESS_REFL]) THEN 2635 FIRST_ASSUM ACCEPT_TAC 2636 ]); 2637 2638val EXP_ALWAYS_BIG_ENOUGH = store_thm ("EXP_ALWAYS_BIG_ENOUGH", 2639 ���!b. 1 < b ==> !n. ?m. n <= b EXP m���, 2640 GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THENL [ 2641 REWRITE_TAC [ZERO_LESS_EQ], 2642 POP_ASSUM STRIP_ASSUME_TAC THEN 2643 Q.ASM_CASES_TAC `SUC n <= b EXP m` THENL [ 2644 mesonLib.ASM_MESON_TAC [], 2645 SUBGOAL_THEN ���n = b EXP m��� STRIP_ASSUME_TAC THENL [ 2646 POP_ASSUM (MP_TAC o REWRITE_RULE [GSYM LESS_EQ]) THEN 2647 POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [LESS_OR_EQ]) THEN 2648 ASM_REWRITE_TAC [], 2649 ALL_TAC 2650 ] THEN 2651 Q.EXISTS_TAC `SUC m` THEN REWRITE_TAC [EXP] THEN 2652 POP_ASSUM SUBST_ALL_TAC THEN MATCH_MP_TAC MULT_INCREASES THEN 2653 ASM_REWRITE_TAC [] THEN 2654 REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC (Q.SPEC `b` num_CASES) THENL [ 2655 IMP_RES_TAC NOT_LESS_0, 2656 REWRITE_TAC [GSYM NOT_ZERO_LT_ZERO, NOT_EXP_0] 2657 ] 2658 ] 2659 ]); 2660 2661val EXP_EQ_0 = store_thm ("EXP_EQ_0", 2662 ���!n m. (n EXP m = 0) = (n = 0) /\ (0 < m)���, 2663 REPEAT GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `m` num_CASES) THEN 2664 REWRITE_TAC [EXP, GSYM NOT_ZERO_LT_ZERO, ONE, NOT_SUC, MULT_EQ_0] THEN 2665 EQ_TAC THEN STRIP_TAC THENL [ 2666 REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC (Q.SPEC `n` num_CASES) THEN 2667 REWRITE_TAC [] THEN IMP_RES_TAC NOT_EXP_0, 2668 ASM_REWRITE_TAC [] 2669 ]); 2670 2671val ZERO_LT_EXP = store_thm ("ZERO_LT_EXP", 2672 ���0 < x EXP y = 0 < x \/ (y = 0)���, 2673 METIS_TAC [NOT_ZERO_LT_ZERO, EXP_EQ_0]); 2674 2675val EXP_1 = store_thm ("EXP_1", 2676 ���!n. (1 EXP n = 1) /\ (n EXP 1 = n)���, 2677 CONV_TAC (QUANT_CONV (FORK_CONV (ALL_CONV, REWRITE_CONV [ONE]))) THEN 2678 REWRITE_TAC [EXP, MULT_CLAUSES] THEN 2679 INDUCT_TAC THEN ASM_REWRITE_TAC [MULT_EQ_1, EXP]); 2680 2681val EXP_EQ_1 = store_thm ("EXP_EQ_1", 2682 ���!n m. (n EXP m = 1) = (n = 1) \/ (m = 0)���, 2683 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 2684 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `m` THEN INDUCT_TAC THEN 2685 REWRITE_TAC [EXP, MULT_EQ_1] THEN STRIP_TAC THEN 2686 ASM_REWRITE_TAC [], 2687 ASM_REWRITE_TAC [EXP_1], 2688 ASM_REWRITE_TAC [EXP] 2689 ]); 2690 2691(* theorems about exponentiation where the base is held constant *) 2692val expbase_le_mono = prove( 2693 ���1 < b /\ m <= n ==> b ** m <= b ** n���, 2694 STRIP_TAC THEN 2695 Q.SUBGOAL_THEN `?q. n = m + q` STRIP_ASSUME_TAC THEN1 2696 METIS_TAC [LESS_EQUAL_ADD] THEN 2697 SRW_TAC [][EXP_ADD] THEN 2698 SRW_TAC [][Once (GSYM MULT_RIGHT_1), SimpLHS] THEN 2699 ASM_REWRITE_TAC [LE_MULT_LCANCEL, EXP_EQ_0, ONE, GSYM LESS_EQ, 2700 ZERO_LT_EXP] THEN 2701 METIS_TAC [ONE, LESS_TRANS, LESS_0]) 2702 2703val expbase_lt_mono = prove( 2704 ���1 < b /\ m < n ==> b ** m < b ** n���, 2705 STRIP_TAC THEN 2706 Q.SUBGOAL_THEN `?q. n = m + q` STRIP_ASSUME_TAC THEN1 2707 METIS_TAC [LESS_ADD, ADD_COMM] THEN 2708 SRW_TAC [][EXP_ADD] THEN 2709 SRW_TAC [][Once (GSYM MULT_RIGHT_1), SimpLHS] THEN 2710 ASM_REWRITE_TAC [LT_MULT_LCANCEL, ZERO_LT_EXP] THEN 2711 Q.SUBGOAL_THEN `0 < b` ASSUME_TAC 2712 THEN1 METIS_TAC [ONE, LESS_TRANS, LESS_0] THEN 2713 Q.SUBGOAL_THEN `1 < b ** q \/ b ** q < 1 \/ (b ** q = 1)` STRIP_ASSUME_TAC 2714 THEN1 METIS_TAC [LESS_CASES, LESS_OR_EQ] THEN 2715 ASM_REWRITE_TAC [] THENL [ 2716 Q.SUBGOAL_THEN `b ** q = 0` ASSUME_TAC THEN1 2717 METIS_TAC [LESS_MONO_EQ, NOT_LESS_0, num_CASES, ONE] THEN 2718 FULL_SIMP_TAC (srw_ss()) [EXP_EQ_0, NOT_LESS_0], 2719 FULL_SIMP_TAC (srw_ss()) [EXP_EQ_1] THEN 2720 FULL_SIMP_TAC (srw_ss()) [LESS_REFL, ADD_CLAUSES] 2721 ]); 2722 2723val EXP_BASE_LE_MONO = store_thm ("EXP_BASE_LE_MONO", 2724 ���!b. 1 < b ==> !n m. b ** m <= b ** n = m <= n���, 2725 METIS_TAC [expbase_lt_mono, expbase_le_mono, NOT_LESS_EQUAL]); 2726val EXP_BASE_LT_MONO = store_thm ("EXP_BASE_LT_MONO", 2727 ���!b. 1 < b ==> !n m. b ** m < b ** n = m < n���, 2728 METIS_TAC [expbase_lt_mono, expbase_le_mono, NOT_LESS]); 2729 2730val EXP_BASE_INJECTIVE = store_thm ("EXP_BASE_INJECTIVE", 2731 ���!b. 1 < b ==> !n m. (b EXP n = b EXP m) = (n = m)���, 2732 METIS_TAC [LESS_EQUAL_ANTISYM, LESS_EQ_REFL, EXP_BASE_LE_MONO]); 2733 2734val EXP_BASE_LEQ_MONO_IMP = store_thm ("EXP_BASE_LEQ_MONO_IMP", 2735 ���!n m b. 0 < b /\ m <= n ==> b ** m <= b ** n���, 2736 REPEAT STRIP_TAC THEN 2737 IMP_RES_TAC LESS_EQUAL_ADD THEN ASM_REWRITE_TAC [EXP_ADD] THEN 2738 SRW_TAC [][Once (GSYM MULT_RIGHT_1), SimpLHS] THEN 2739 ASM_REWRITE_TAC [LE_MULT_LCANCEL, EXP_EQ_0, ONE, GSYM LESS_EQ] THEN 2740 FULL_SIMP_TAC bool_ss [GSYM NOT_ZERO_LT_ZERO, EXP_EQ_0]); 2741 2742(* |- m <= n ==> SUC b ** m <= SUC b ** n *) 2743val EXP_BASE_LEQ_MONO_SUC_IMP = save_thm ( 2744 "EXP_BASE_LEQ_MONO_SUC_IMP", 2745 (REWRITE_RULE [LESS_0] o Q.INST [`b` |-> `SUC b`] o SPEC_ALL) 2746 EXP_BASE_LEQ_MONO_IMP); 2747 2748val EXP_BASE_LE_IFF = store_thm ("EXP_BASE_LE_IFF", 2749 ���b ** m <= b ** n <=> 2750 (b = 0) /\ (n = 0) \/ (b = 0) /\ 0 < m \/ (b = 1) \/ 1 < b /\ m <= n���, 2751 Q.SPEC_THEN `b` STRUCT_CASES_TAC num_CASES THEN 2752 ASM_REWRITE_TAC [NOT_SUC, NOT_LESS_0] THENL [ 2753 Q.SPEC_THEN `m` STRUCT_CASES_TAC num_CASES THEN 2754 ASM_REWRITE_TAC [LESS_REFL, EXP, ONE, SUC_NOT] THENL [ 2755 Q.SPEC_THEN `n` STRUCT_CASES_TAC num_CASES THEN 2756 ASM_REWRITE_TAC [NOT_SUC, EXP, ONE, LESS_EQ_REFL, MULT_CLAUSES, 2757 NOT_SUC_LESS_EQ_0], 2758 ASM_REWRITE_TAC [LESS_0, MULT_CLAUSES, ZERO_LESS_EQ] 2759 ], 2760 EQ_TAC THENL [ 2761 ASM_CASES_TAC ���1 < SUC n'��� THEN SRW_TAC [][EXP_BASE_LE_MONO] THEN 2762 FULL_SIMP_TAC (srw_ss()) [ONE, LESS_MONO_EQ, INV_SUC_EQ, 2763 GSYM NOT_ZERO_LT_ZERO], 2764 STRIP_TAC THEN ASM_REWRITE_TAC [EXP_1, LESS_EQ_REFL] THEN 2765 MATCH_MP_TAC EXP_BASE_LEQ_MONO_IMP THEN ASM_REWRITE_TAC [LESS_0] 2766 ] 2767 ]); 2768 2769val X_LE_X_EXP = store_thm ("X_LE_X_EXP", 2770 ���0 < n ==> x <= x ** n���, 2771 Q.SPEC_THEN `n` STRUCT_CASES_TAC num_CASES THEN 2772 REWRITE_TAC [EXP, LESS_REFL, LESS_0] THEN 2773 Q.SPEC_THEN `x` STRUCT_CASES_TAC num_CASES THEN 2774 REWRITE_TAC [ZERO_LESS_EQ, LE_MULT_CANCEL_LBARE, NOT_SUC, ZERO_LT_EXP, 2775 LESS_0]); 2776 2777val X_LT_EXP_X = Q.store_thm ("X_LT_EXP_X", 2778 `1 < b ==> x < b ** x`, 2779 Q.ID_SPEC_TAC `x` THEN INDUCT_TAC THEN1 2780 SIMP_TAC bool_ss [LESS_0,EXP,ONE] THEN 2781 STRIP_TAC THEN 2782 FULL_SIMP_TAC bool_ss [] THEN 2783 Cases_on `x = 0` THEN1 2784 ASM_SIMP_TAC bool_ss [EXP,MULT_RIGHT_1,SYM ONE] THEN 2785 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN 2786 EXISTS_TAC ���x + x��� THEN 2787 CONJ_TAC THEN1 ( 2788 SIMP_TAC bool_ss [ADD1,ADD_MONO_LESS_EQ] THEN 2789 SIMP_TAC bool_ss [ONE] THEN 2790 MATCH_MP_TAC LESS_OR THEN 2791 PROVE_TAC [NOT_ZERO_LT_ZERO] ) THEN 2792 SIMP_TAC bool_ss [EXP] THEN 2793 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN 2794 EXISTS_TAC ���b * x��� THEN 2795 CONJ_TAC THEN1 ( 2796 SIMP_TAC bool_ss [GSYM TIMES2] THEN 2797 MATCH_MP_TAC LESS_MONO_MULT THEN 2798 SIMP_TAC bool_ss [TWO] THEN 2799 MATCH_MP_TAC LESS_OR THEN 2800 FIRST_ASSUM ACCEPT_TAC ) THEN 2801 SIMP_TAC bool_ss [LT_MULT_LCANCEL] THEN 2802 CONJ_TAC THEN1 ( 2803 MATCH_MP_TAC LESS_TRANS THEN 2804 EXISTS_TAC ���1��� THEN 2805 ASM_SIMP_TAC bool_ss [ONE,prim_recTheory.LESS_0_0] ) THEN 2806 FIRST_ASSUM ACCEPT_TAC) 2807 2808local fun Cases_on q = Q.SPEC_THEN q STRUCT_CASES_TAC num_CASES in 2809 2810val ZERO_EXP = Q.store_thm ("ZERO_EXP", 2811 `0 ** x = if x = 0 then 1 else 0`, 2812 Cases_on `x` THEN 2813 SIMP_TAC bool_ss [EXP,numTheory.NOT_SUC,MULT]) 2814 2815val X_LT_EXP_X_IFF = Q.store_thm ("X_LT_EXP_X_IFF", 2816 `x < b ** x <=> 1 < b \/ (x = 0)`, 2817 EQ_TAC THEN1 ( 2818 Cases_on `b` THEN1 ( 2819 Cases_on `x` THEN 2820 SIMP_TAC bool_ss [ZERO_EXP,SUC_NOT,NOT_LESS_0] ) THEN 2821 Q.MATCH_RENAME_TAC `x < SUC b ** x ==> 1 < SUC b \/ (x = 0)` THEN 2822 Cases_on `b` THEN1 ( 2823 SIMP_TAC bool_ss [EXP_1,SYM ONE] THEN 2824 SIMP_TAC bool_ss [ONE,LESS_THM,NOT_LESS_0] ) THEN 2825 SIMP_TAC bool_ss [LESS_MONO_EQ,ONE,LESS_0] ) THEN 2826 STRIP_TAC THEN1 ( 2827 POP_ASSUM MP_TAC THEN ACCEPT_TAC X_LT_EXP_X) THEN 2828 ASM_SIMP_TAC bool_ss [EXP,ONE,LESS_0]) 2829 end 2830 2831(* theorems about exponentiation where the exponent is held constant *) 2832val LT_MULT_IMP = prove( 2833 ���a < b /\ x < y ==> a * x < b * y���, 2834 STRIP_TAC THEN 2835 Q.SUBGOAL_THEN `0 < y` ASSUME_TAC THEN1 METIS_TAC [NOT_ZERO_LT_ZERO, 2836 NOT_LESS_0] THEN 2837 METIS_TAC [LE_MULT_LCANCEL, LT_MULT_RCANCEL, LESS_EQ_LESS_TRANS, 2838 LESS_OR_EQ]) 2839val LE_MULT_IMP = prove( 2840 ���a <= b /\ x <= y ==> a * x <= b * y���, 2841 METIS_TAC [LE_MULT_LCANCEL, LE_MULT_RCANCEL, LESS_EQ_TRANS]); 2842 2843val EXP_LT_MONO_0 = prove( 2844 ���!n. 0 < n ==> !a b. a < b ==> a EXP n < b EXP n���, 2845 INDUCT_TAC THEN SRW_TAC [][NOT_LESS_0, LESS_0, EXP] THEN 2846 Q.SPEC_THEN `n` STRIP_ASSUME_TAC num_CASES THEN 2847 FULL_SIMP_TAC (srw_ss()) [EXP, MULT_CLAUSES, LESS_0] THEN 2848 SRW_TAC [][LT_MULT_IMP]) 2849 2850val EXP_LE_MONO_0 = prove( 2851 ���!n. 0 < n ==> !a b. a <= b ==> a EXP n <= b EXP n���, 2852 INDUCT_TAC THEN SRW_TAC [][EXP, LESS_EQ_REFL] THEN 2853 Q.SPEC_THEN `n` STRIP_ASSUME_TAC num_CASES THEN 2854 FULL_SIMP_TAC (srw_ss()) [EXP, MULT_CLAUSES, LESS_0] THEN 2855 SRW_TAC [][LE_MULT_IMP]); 2856 2857val EXP_EXP_LT_MONO = store_thm ("EXP_EXP_LT_MONO", 2858 ���!a b. a EXP n < b EXP n = a < b /\ 0 < n���, 2859 METIS_TAC [EXP_LT_MONO_0, NOT_LESS, EXP_LE_MONO_0, EXP, LESS_REFL, 2860 NOT_ZERO_LT_ZERO]); 2861 2862val EXP_EXP_LE_MONO = store_thm ("EXP_EXP_LE_MONO", 2863 ���!a b. a EXP n <= b EXP n = a <= b \/ (n = 0)���, 2864 METIS_TAC [EXP_LE_MONO_0, NOT_LESS_EQUAL, EXP_LT_MONO_0, EXP, LESS_EQ_REFL, 2865 NOT_ZERO_LT_ZERO]); 2866 2867val EXP_EXP_INJECTIVE = store_thm ("EXP_EXP_INJECTIVE", 2868 ���!b1 b2 x. (b1 EXP x = b2 EXP x) = (x = 0) \/ (b1 = b2)���, 2869 METIS_TAC [EXP_EXP_LE_MONO, LESS_EQUAL_ANTISYM, LESS_EQ_REFL]); 2870 2871val EXP_SUB = Q.store_thm ("EXP_SUB", 2872 `!p q n. 0 < n /\ q <= p ==> (n ** (p - q) = n ** p DIV n ** q)`, 2873 REPEAT STRIP_TAC THEN 2874 ���0 < n ** p /\ 0 < n ** q��� via 2875 (STRIP_ASSUME_TAC (Q.SPEC`n` num_CASES) THEN 2876 RW_TAC bool_ss [] THEN 2877 FULL_SIMP_TAC bool_ss [ZERO_LESS_EXP,LESS_REFL]) THEN 2878 RW_TAC bool_ss [DIV_P] THEN 2879 Q.EXISTS_TAC `0` THEN 2880 RW_TAC bool_ss [GSYM EXP_ADD,ADD_CLAUSES] THEN 2881 METIS_TAC [SUB_ADD]); 2882 2883val EXP_SUB_NUMERAL = store_thm ("EXP_SUB_NUMERAL", 2884 ���0 < n ==> 2885 (n ** (NUMERAL (BIT1 x)) DIV n = n ** (NUMERAL (BIT1 x) - 1)) /\ 2886 (n ** (NUMERAL (BIT2 x)) DIV n = n ** (NUMERAL (BIT1 x)))���, 2887 REPEAT STRIP_TAC THENL [ 2888 Q.SPECL_THEN [`NUMERAL (BIT1 x)`, `1`, `n`] (MP_TAC o GSYM) EXP_SUB THEN 2889 REWRITE_TAC [EXP_1] THEN DISCH_THEN MATCH_MP_TAC THEN 2890 ASM_REWRITE_TAC [NUMERAL_DEF, BIT1, ALT_ZERO, ADD_CLAUSES, 2891 LESS_EQ_MONO, ZERO_LESS_EQ], 2892 Q.SPECL_THEN [`NUMERAL (BIT2 x)`, `1`, `n`] (MP_TAC o GSYM) EXP_SUB THEN 2893 REWRITE_TAC [EXP_1] THEN 2894 Q.SUBGOAL_THEN `NUMERAL (BIT2 x) - 1 = NUMERAL (BIT1 x)` SUBST1_TAC THENL[ 2895 REWRITE_TAC [NUMERAL_DEF, BIT1, BIT2, ALT_ZERO, ADD_CLAUSES, 2896 SUB_MONO_EQ, SUB_0], 2897 ALL_TAC 2898 ] THEN DISCH_THEN MATCH_MP_TAC THEN 2899 ASM_REWRITE_TAC [NUMERAL_DEF, BIT2, BIT1, ALT_ZERO, ADD_CLAUSES, 2900 LESS_EQ_MONO, ZERO_LESS_EQ] 2901 ]); 2902val _ = export_rewrites ["EXP_SUB_NUMERAL"] 2903 2904val EXP_BASE_MULT = store_thm ("EXP_BASE_MULT", 2905 ���!z x y. (x * y) ** z = (x ** z) * (y ** z)���, 2906 INDUCT_TAC THEN 2907 ASM_SIMP_TAC bool_ss [EXP, MULT_CLAUSES, AC MULT_ASSOC MULT_COMM]); 2908 2909val EXP_EXP_MULT = store_thm ("EXP_EXP_MULT", 2910 ���!z x y. x ** (y * z) = (x ** y) ** z���, 2911 INDUCT_TAC THEN ASM_REWRITE_TAC [EXP, MULT_CLAUSES, EXP_1, EXP_ADD]); 2912 2913(* ********************************************************************** *) 2914(* Maximum and minimum *) 2915(* ********************************************************************** *) 2916 2917val _ = print "Minimums and maximums\n" 2918 2919val MAX = new_definition("MAX_DEF", ���MAX m n = if m < n then n else m���); 2920val MIN = new_definition("MIN_DEF", ���MIN m n = if m < n then m else n���); 2921 2922val ARW = RW_TAC bool_ss 2923 2924val MAX_COMM = store_thm ("MAX_COMM", 2925 ���!m n. MAX m n = MAX n m���, 2926 ARW [MAX] THEN FULL_SIMP_TAC bool_ss [NOT_LESS] THEN 2927 IMP_RES_TAC LESS_ANTISYM THEN IMP_RES_TAC LESS_EQUAL_ANTISYM); 2928 2929val MIN_COMM = store_thm ("MIN_COMM", 2930 ���!m n. MIN m n = MIN n m���, 2931 ARW [MIN] THEN FULL_SIMP_TAC bool_ss [NOT_LESS] THEN 2932 IMP_RES_TAC LESS_ANTISYM THEN IMP_RES_TAC LESS_EQUAL_ANTISYM); 2933 2934val MAX_ASSOC = store_thm ("MAX_ASSOC", 2935 ���!m n p. MAX m (MAX n p) = MAX (MAX m n) p���, 2936 SIMP_TAC bool_ss [MAX] THEN 2937 PROVE_TAC [NOT_LESS, LESS_EQ_TRANS, LESS_TRANS]); 2938 2939val MIN_ASSOC = store_thm ("MIN_ASSOC", 2940 ���!m n p. MIN m (MIN n p) = MIN (MIN m n) p���, 2941 SIMP_TAC bool_ss [MIN] THEN 2942 PROVE_TAC [NOT_LESS, LESS_EQ_TRANS, LESS_TRANS]); 2943 2944val MIN_MAX_EQ = store_thm ("MIN_MAX_EQ", 2945 ���!m n. (MIN m n = MAX m n) = (m = n)���, 2946 SIMP_TAC bool_ss [MAX, MIN] THEN 2947 PROVE_TAC [NOT_LESS, LESS_EQUAL_ANTISYM, LESS_ANTISYM]); 2948 2949val MIN_MAX_LT = store_thm ("MIN_MAX_LT", 2950 ���!m n. (MIN m n < MAX m n) = ~(m = n)���, 2951 SIMP_TAC bool_ss [MAX, MIN] THEN 2952 PROVE_TAC [LESS_REFL, NOT_LESS, LESS_OR_EQ]); 2953 2954val MIN_MAX_LE = store_thm ("MIN_MAX_LE", 2955 ���!m n. MIN m n <= MAX m n���, 2956 SIMP_TAC bool_ss [MAX, MIN] THEN 2957 PROVE_TAC [LESS_OR_EQ, NOT_LESS]); 2958 2959val MIN_MAX_PRED = store_thm ("MIN_MAX_PRED", 2960 ���!P m n. P m /\ P n ==> P (MIN m n) /\ P (MAX m n)���, 2961 PROVE_TAC [MIN, MAX]); 2962 2963val MIN_LT = store_thm ("MIN_LT", 2964 ���!n m p. (MIN m n < p = m < p \/ n < p) /\ 2965 (p < MIN m n = p < m /\ p < n)���, 2966 SIMP_TAC bool_ss [MIN] THEN 2967 PROVE_TAC [NOT_LESS, LESS_OR_EQ, LESS_ANTISYM, LESS_TRANS]); 2968 2969val MAX_LT = store_thm ("MAX_LT", 2970 ���!n m p. (p < MAX m n = p < m \/ p < n) /\ 2971 (MAX m n < p = m < p /\ n < p)���, 2972 SIMP_TAC bool_ss [MAX] THEN 2973 PROVE_TAC [NOT_LESS, LESS_OR_EQ, LESS_ANTISYM, LESS_TRANS]); 2974 2975val MIN_LE = store_thm ("MIN_LE", 2976 ���!n m p. (MIN m n <= p = m <= p \/ n <= p) /\ 2977 (p <= MIN m n = p <= m /\ p <= n)���, 2978 SIMP_TAC bool_ss [MIN] THEN 2979 PROVE_TAC [LESS_OR_EQ, NOT_LESS, LESS_TRANS]); 2980 2981val MAX_LE = store_thm ("MAX_LE", 2982 ���!n m p. (p <= MAX m n = p <= m \/ p <= n) /\ 2983 (MAX m n <= p = m <= p /\ n <= p)���, 2984 SIMP_TAC bool_ss [MAX] THEN 2985 PROVE_TAC [LESS_OR_EQ, NOT_LESS, LESS_TRANS]); 2986 2987val MIN_0 = store_thm ("MIN_0", 2988 ���!n. (MIN n 0 = 0) /\ (MIN 0 n = 0)���, 2989 REWRITE_TAC [MIN] THEN 2990 PROVE_TAC [NOT_LESS_0, NOT_LESS, LESS_OR_EQ]); 2991 2992val MAX_0 = store_thm ("MAX_0", 2993 ���!n. (MAX n 0 = n) /\ (MAX 0 n = n)���, 2994 REWRITE_TAC [MAX] THEN 2995 PROVE_TAC [NOT_LESS_0, NOT_LESS, LESS_OR_EQ]); 2996 2997val MAX_EQ_0 = store_thm( 2998 "MAX_EQ_0[simp]", 2999 ���(MAX m n = 0) <=> (m = 0) /\ (n = 0)���, 3000 SRW_TAC[][MAX,EQ_IMP_THM] THEN 3001 FULL_SIMP_TAC (srw_ss()) [NOT_LESS_0, NOT_LESS]); 3002 3003val MIN_EQ_0 = store_thm( 3004 "MIN_EQ_0[simp]", 3005 ���(MIN m n = 0) <=> (m = 0) \/ (n = 0)���, 3006 SRW_TAC[][MIN,EQ_IMP_THM] THEN 3007 FULL_SIMP_TAC (srw_ss()) [NOT_LESS_0, NOT_LESS]); 3008 3009val MIN_IDEM = store_thm ("MIN_IDEM", 3010 ���!n. MIN n n = n���, 3011 PROVE_TAC [MIN]); 3012 3013val MAX_IDEM = store_thm ("MAX_IDEM", 3014 ���!n. MAX n n = n���, 3015 PROVE_TAC [MAX]); 3016 3017val EXISTS_GREATEST = store_thm ("EXISTS_GREATEST", 3018 ���!P. (?x. P x) /\ (?x:num. !y. y > x ==> ~P y) = 3019 ?x. P x /\ !y. y > x ==> ~P y���, 3020 GEN_TAC THEN EQ_TAC THENL 3021 [REWRITE_TAC[GREATER_DEF] THEN 3022 DISCH_THEN (CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN 3023 SUBGOAL_THEN 3024 (���(?x. !y. x < y ==> ~P y) = (?x. (\x. !y. x < y ==> ~P y) x)���) 3025 SUBST1_TAC THENL 3026 [BETA_TAC THEN REFL_TAC, 3027 DISCH_THEN (MP_TAC o MATCH_MP WOP) 3028 THEN BETA_TAC THEN CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) 3029 THEN STRIP_TAC THEN EXISTS_TAC (���n:num���) THEN ASM_REWRITE_TAC[] 3030 THEN NTAC 2 (POP_ASSUM MP_TAC) 3031 THEN STRUCT_CASES_TAC (SPEC (���n:num���) num_CASES) 3032 THEN REPEAT STRIP_TAC THENL 3033 [UNDISCH_THEN (���!y. 0 < y ==> ~P y���) 3034 (MP_TAC o CONV_RULE (ONCE_DEPTH_CONV CONTRAPOS_CONV)) 3035 THEN REWRITE_TAC[] THEN STRIP_TAC THEN RES_TAC 3036 THEN MP_TAC (SPEC (���x:num���) LESS_0_CASES) 3037 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (SUBST_ALL_TAC o SYM) 3038 THEN ASM_REWRITE_TAC[], 3039 POP_ASSUM (MP_TAC o SPEC (���n':num���)) 3040 THEN REWRITE_TAC [prim_recTheory.LESS_SUC_REFL] 3041 THEN DISCH_THEN (CHOOSE_THEN MP_TAC) 3042 THEN SUBGOAL_THEN (���!x y. ~(x ==> ~y) = x /\ y���) 3043 (fn th => REWRITE_TAC[th] THEN STRIP_TAC) THENL 3044 [REWRITE_TAC [NOT_IMP], 3045 UNDISCH_THEN (���!y. SUC n' < y ==> ~P y���) 3046 (MP_TAC o CONV_RULE (ONCE_DEPTH_CONV CONTRAPOS_CONV) 3047 o SPEC (���y:num���)) 3048 THEN ASM_REWRITE_TAC[NOT_LESS,LESS_OR_EQ] 3049 THEN DISCH_THEN (DISJ_CASES_THEN2 ASSUME_TAC SUBST_ALL_TAC) 3050 THENL [IMP_RES_TAC LESS_LESS_SUC, ASM_REWRITE_TAC[]]]]], 3051 REPEAT STRIP_TAC THEN EXISTS_TAC (���x:num���) THEN ASM_REWRITE_TAC[]]); 3052 3053val EXISTS_NUM = store_thm ("EXISTS_NUM", 3054 ���!P. (?n. P n) = P 0 \/ (?m. P (SUC m))���, 3055 PROVE_TAC [num_CASES]); 3056 3057val FORALL_NUM = store_thm ("FORALL_NUM", 3058 ���!P. (!n. P n) = P 0 /\ !n. P (SUC n)���, 3059 PROVE_TAC [num_CASES]); 3060 3061val BOUNDED_FORALL_THM = Q.store_thm ("BOUNDED_FORALL_THM", 3062 `!c. 0<c ==> ((!n. n < c ==> P n) = P (c-1) /\ !n. n < (c-1) ==> P n)`, 3063 RW_TAC boolSimps.bool_ss [] THEN EQ_TAC THENL 3064 [REPEAT STRIP_TAC 3065 THEN FIRST_ASSUM MATCH_MP_TAC THENL 3066 [METIS_TAC [ONE,LESS_ADD_SUC,ADD_SYM,SUB_RIGHT_LESS], 3067 MATCH_MP_TAC LESS_LESS_EQ_TRANS 3068 THEN Q.EXISTS_TAC `c-1` 3069 THEN ASM_REWRITE_TAC [SUB_LESS_EQ,SUB_LEFT_LESS]], 3070 METIS_TAC [SUB_LESS_OR,LESS_OR_EQ]]); 3071 3072val BOUNDED_EXISTS_THM = Q.store_thm ("BOUNDED_EXISTS_THM", 3073 `!c. 0<c ==> ((?n. n < c /\ P n) = P (c-1) \/ ?n. n < (c-1) /\ P n)`, 3074 REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL 3075 [METIS_TAC [SUB_LESS_OR,LESS_REFL,LESS_EQ_LESS_TRANS,LESS_LESS_CASES], 3076 METIS_TAC [num_CASES,LESS_REFL,SUC_SUB1,LESS_SUC_REFL], 3077 METIS_TAC [SUB_LEFT_LESS,ADD1,SUC_LESS]]); 3078 3079(*---------------------------------------------------------------------------*) 3080(* Theorems about sequences *) 3081(*---------------------------------------------------------------------------*) 3082 3083val transitive_monotone = Q.store_thm ("transitive_monotone", 3084 `!R f. transitive R /\ (!n. R (f n) (f (SUC n))) ==> 3085 !m n. m < n ==> R (f m) (f n)`, 3086 NTAC 3 STRIP_TAC THEN INDUCT_TAC THEN 3087 (INDUCT_TAC THEN1 REWRITE_TAC [NOT_LESS_0]) 3088 THEN1 ( 3089 POP_ASSUM MP_TAC THEN 3090 Q.SPEC_THEN `n` STRUCT_CASES_TAC num_CASES THEN 3091 METIS_TAC [LESS_0,relationTheory.transitive_def]) THEN 3092 METIS_TAC [LESS_THM,relationTheory.transitive_def]) 3093 3094val STRICTLY_INCREASING_TC = save_thm ("STRICTLY_INCREASING_TC", 3095 (* !f. (!n. f n < f (SUC n)) ==> !m n. m < n ==> f m < f n *) 3096 transitive_monotone |> Q.ISPEC `$<` |> 3097 SIMP_RULE bool_ss [ 3098 Q.prove(`transitive $<`, 3099 METIS_TAC [relationTheory.transitive_def,LESS_TRANS])]) 3100 3101val STRICTLY_INCREASING_ONE_ONE = Q.store_thm ("STRICTLY_INCREASING_ONE_ONE", 3102 `!f. (!n. f n < f (SUC n)) ==> ONE_ONE f`, 3103 REWRITE_TAC [ONE_ONE_THM] THEN 3104 METIS_TAC [STRICTLY_INCREASING_TC,NOT_LESS,LESS_OR_EQ,LESS_EQUAL_ANTISYM]) 3105 3106val ONE_ONE_INV_IMAGE_BOUNDED = Q.store_thm ("ONE_ONE_INV_IMAGE_BOUNDED", 3107 `ONE_ONE (f:num->num) ==> !b. ?a. !x. f x <= b ==> x <= a`, 3108 REWRITE_TAC [ONE_ONE_THM] THEN DISCH_TAC THEN INDUCT_TAC 3109 THENL [ 3110 (* case b of 0 *) 3111 REWRITE_TAC [LESS_EQ_0] THEN Q.ASM_CASES_TAC `?z. f z = 0` 3112 THENL [ 3113 POP_ASSUM CHOOSE_TAC THEN 3114 Q.EXISTS_TAC `z` THEN REPEAT STRIP_TAC THEN 3115 VALIDATE (FIRST_X_ASSUM 3116 (ASSUME_TAC o UNDISCH o Q.SPECL [`x`, `z`])) THEN 3117 ASM_REWRITE_TAC [LESS_EQ_REFL], 3118 Q.EXISTS_TAC `0` THEN REPEAT STRIP_TAC THEN RES_TAC], 3119 3120 (* case b of SUC b *) 3121 POP_ASSUM CHOOSE_TAC THEN REWRITE_TAC [LE] THEN 3122 Q.ASM_CASES_TAC `?z. f z = SUC b` 3123 THENL [ 3124 POP_ASSUM CHOOSE_TAC THEN 3125 Q.EXISTS_TAC `MAX a z` THEN 3126 REWRITE_TAC [MAX_LE] THEN REPEAT STRIP_TAC 3127 THENL [ 3128 VALIDATE (FIRST_X_ASSUM 3129 (ASSUME_TAC o UNDISCH o Q.SPECL [`x`, `z`])) THEN 3130 ASM_REWRITE_TAC [LESS_EQ_REFL], 3131 RES_TAC THEN ASM_REWRITE_TAC []], 3132 Q.EXISTS_TAC `a` THEN REPEAT STRIP_TAC THEN RES_TAC] ]) ; 3133 3134val ONE_ONE_UNBOUNDED = Q.store_thm ("ONE_ONE_UNBOUNDED", 3135`!f. ONE_ONE (f:num->num) ==> !b.?n. b < f n`, 3136 REPEAT STRIP_TAC THEN 3137 POP_ASSUM (CHOOSE_TAC o Q.SPEC `b` o 3138 MATCH_MP ONE_ONE_INV_IMAGE_BOUNDED) THEN 3139 Q.EXISTS_TAC `SUC a` THEN 3140 REWRITE_TAC [GSYM NOT_LESS_EQUAL] THEN 3141 DISCH_TAC THEN RES_TAC THEN 3142 POP_ASSUM (ACCEPT_TAC o REWRITE_RULE [GSYM LESS_EQ, LESS_REFL])) ; 3143 3144val STRICTLY_INCREASING_UNBOUNDED = Q.store_thm("STRICTLY_INCREASING_UNBOUNDED", 3145 `!f. (!n. f n < f (SUC n)) ==> !b.?n. b < f n`, 3146 METIS_TAC [STRICTLY_INCREASING_ONE_ONE,ONE_ONE_UNBOUNDED]) 3147 3148val STRICTLY_DECREASING_TC = Q.prove( 3149 `!f. (!n. f (SUC n) < f n) ==> !m n. m < n ==> f n < f m`, 3150 NTAC 2 STRIP_TAC THEN 3151 (transitive_monotone |> Q.ISPECL [`\x y. y < x`,`f:num->num`] |> 3152 SIMP_RULE bool_ss [] |> MATCH_MP_TAC) THEN 3153 SRW_TAC [][relationTheory.transitive_def] THEN 3154 METIS_TAC [LESS_TRANS]) 3155 3156val STRICTLY_DECREASING_ONE_ONE = Q.prove( 3157 `!f. (!n. f (SUC n) < f n) ==> ONE_ONE f`, 3158 SRW_TAC [] [ONE_ONE_THM] THEN 3159 METIS_TAC [STRICTLY_DECREASING_TC,NOT_LESS,LESS_OR_EQ,LESS_EQUAL_ANTISYM]) 3160 3161val NOT_STRICTLY_DECREASING = Q.store_thm ("NOT_STRICTLY_DECREASING", 3162 `!f. ~(!n. f (SUC n) < f n)`, 3163 NTAC 2 STRIP_TAC THEN 3164 IMP_RES_TAC STRICTLY_DECREASING_TC THEN 3165 IMP_RES_TAC STRICTLY_DECREASING_ONE_ONE THEN 3166 IMP_RES_TAC ONE_ONE_UNBOUNDED THEN 3167 POP_ASSUM (Q.SPEC_THEN `f 0` STRIP_ASSUME_TAC) THEN 3168 Q.SPEC_THEN `n` STRIP_ASSUME_TAC num_CASES THEN1 3169 METIS_TAC [LESS_NOT_EQ] THEN 3170 METIS_TAC [LESS_ANTISYM,LESS_0]) 3171 3172(* Absolute difference *) 3173val ABS_DIFF_def = new_definition ("ABS_DIFF_def", 3174 ���ABS_DIFF n m = if n < m then m - n else n - m���) 3175 3176val ABS_DIFF_SYM = Q.store_thm ("ABS_DIFF_SYM", 3177 `!n m. ABS_DIFF n m = ABS_DIFF m n`, 3178 SRW_TAC [][ABS_DIFF_def] THEN 3179 METIS_TAC [LESS_ANTISYM,NOT_LESS,LESS_OR_EQ]) 3180 3181val ABS_DIFF_COMM = save_thm ("ABS_DIFF_COMM",ABS_DIFF_SYM) 3182 3183val ABS_DIFF_EQS = Q.store_thm ("ABS_DIFF_EQS", 3184 `!n. ABS_DIFF n n = 0`, 3185 SRW_TAC [][ABS_DIFF_def,SUB_EQUAL_0]) 3186val _ = export_rewrites ["ABS_DIFF_EQS"] 3187 3188val ABS_DIFF_EQ_0 = Q.store_thm ("ABS_DIFF_EQ_0", 3189 `!n m. (ABS_DIFF n m = 0) <=> (n = m)`, 3190 SRW_TAC [][ABS_DIFF_def,LESS_OR_EQ,SUB_EQ_0] THEN 3191 METIS_TAC [LESS_ANTISYM]) 3192 3193val ABS_DIFF_ZERO = Q.store_thm ("ABS_DIFF_ZERO", 3194 `!n. (ABS_DIFF n 0 = n) /\ (ABS_DIFF 0 n = n)`, 3195 SRW_TAC [][ABS_DIFF_def,SUB_0] THEN 3196 METIS_TAC [NOT_LESS_0,NOT_ZERO_LT_ZERO]) 3197val _ = export_rewrites ["ABS_DIFF_ZERO"] 3198 3199val ABS_DIFF_SUC = Q.store_thm ("ABS_DIFF_SUC", 3200 `!n m. (ABS_DIFF (SUC n) (SUC m)) = (ABS_DIFF n m)`, 3201 REWRITE_TAC [ABS_DIFF_def, LESS_MONO_EQ, SUB_MONO_EQ]) ; 3202 3203fun owr commth = CONV_RULE (ONCE_DEPTH_CONV (REWR_CONV commth)) ; 3204 3205val LESS_EQ_TRANS' = REWRITE_RULE [GSYM AND_IMP_INTRO] LESS_EQ_TRANS ; 3206val AND_IMP_INTRO' = owr CONJ_COMM AND_IMP_INTRO ; 3207val LESS_EQ_TRANS'' = REWRITE_RULE [GSYM AND_IMP_INTRO'] LESS_EQ_TRANS ; 3208val LESS_EQ_ADD' = owr ADD_COMM LESS_EQ_ADD ; 3209val LESS_EQ_SUC_REFL' = SPEC_ALL LESS_EQ_SUC_REFL ; 3210 3211val leq_ss = MATCH_MP (MATCH_MP LESS_EQ_TRANS'' LESS_EQ_SUC_REFL') 3212 LESS_EQ_SUC_REFL' ; 3213 3214val imp_leq_ss = MATCH_MP LESS_EQ_TRANS'' leq_ss ; 3215 3216val ABS_DIFF_SUC_LE = Q.store_thm ("ABS_DIFF_SUC_LE", 3217 `!x z. ABS_DIFF x (SUC z) <= SUC (ABS_DIFF x z)`, 3218 REPEAT INDUCT_TAC THEN 3219 ASM_REWRITE_TAC [ABS_DIFF_ZERO, ABS_DIFF_SUC, ADD, ADD_0, GSYM ADD_SUC, 3220 LESS_EQ_REFL, LESS_EQ_MONO, ZERO_LESS_EQ, leq_ss]) ; 3221 3222val ABS_DIFF_PLUS_LE = Q.store_thm ("ABS_DIFF_PLUS_LE", 3223 `!x z y. ABS_DIFF x (y + z) <= y + (ABS_DIFF x z)`, 3224 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC 3225 THEN REWRITE_TAC [ADD, LESS_EQ_REFL] 3226 THEN MATCH_MP_TAC (MATCH_MP LESS_EQ_TRANS' (SPEC_ALL ABS_DIFF_SUC_LE)) 3227 THEN ASM_REWRITE_TAC [LESS_EQ_MONO]) ; 3228 3229val ABS_DIFF_PLUS_LE' = owr ADD_COMM ABS_DIFF_PLUS_LE ; 3230val [ADT_splemx, ADT_splemx'] = 3231 map (owr ABS_DIFF_COMM) [ABS_DIFF_PLUS_LE, ABS_DIFF_PLUS_LE'] ; 3232 3233val ABS_DIFF_LE_SUM = Q.store_thm ("ABS_DIFF_LE_SUM", 3234 `ABS_DIFF x z <= x + z`, 3235 REWRITE_TAC [ABS_DIFF_def] THEN COND_CASES_TAC 3236 THEN MATCH_MP_TAC (MATCH_MP LESS_EQ_TRANS' (SPEC_ALL SUB_LESS_EQ)) 3237 THEN REWRITE_TAC [LESS_EQ_ADD, LESS_EQ_ADD']) ; 3238 3239val ABS_DIFF_LE_SUM' = owr ADD_COMM ABS_DIFF_LE_SUM ; 3240 3241val [ADT_sslem, ADT_sslem'] = map (MATCH_MP imp_leq_ss) 3242 [ABS_DIFF_LE_SUM, ABS_DIFF_LE_SUM'] ; 3243 3244val ABS_DIFF_TRIANGLE_lem = Q.store_thm ("ABS_DIFF_TRIANGLE_lem", 3245 `!x y. x <= ABS_DIFF x y + y`, 3246 REPEAT INDUCT_TAC THEN 3247 ASM_REWRITE_TAC [ABS_DIFF_ZERO, ABS_DIFF_SUC, ADD, ADD_0, GSYM ADD_SUC, 3248 LESS_EQ_REFL, LESS_EQ_MONO, ZERO_LESS_EQ]) ; 3249 3250val ABS_DIFF_TRIANGLE_lem' = 3251 owr ABS_DIFF_COMM (owr ADD_COMM ABS_DIFF_TRIANGLE_lem) ; 3252 3253val ABS_DIFF_TRIANGLE = Q.store_thm ("ABS_DIFF_TRIANGLE", 3254`!x y z. ABS_DIFF x z <= ABS_DIFF x y + ABS_DIFF y z`, 3255 REPEAT INDUCT_TAC THEN 3256 ASM_REWRITE_TAC [ABS_DIFF_ZERO, ABS_DIFF_SUC, ADD, ADD_0, GSYM ADD_SUC, 3257 LESS_EQ_REFL, LESS_EQ_MONO, ZERO_LESS_EQ, 3258 ABS_DIFF_TRIANGLE_lem, ABS_DIFF_TRIANGLE_lem', ADT_sslem]) ; 3259 3260val ABS_DIFF_ADD_SAME = Q.store_thm ("ABS_DIFF_ADD_SAME", 3261 `!n m p. ABS_DIFF (n + p) (m + p) = ABS_DIFF n m`, 3262 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC 3263 THEN ASM_REWRITE_TAC [ADD_0, GSYM ADD_SUC, ABS_DIFF_SUC]) ; 3264 3265val LE_SUB_RCANCEL = Q.store_thm ("LE_SUB_RCANCEL", 3266 `!m n p. n - m <= p - m <=> n <= m \/ n <= p`, 3267 REPEAT INDUCT_TAC THEN 3268 ASM_REWRITE_TAC [ LESS_EQ_REFL, LESS_EQ_MONO, ZERO_LESS_EQ, 3269 NOT_SUC_LESS_EQ_0, SUB_MONO_EQ, SUB_0, SUB_EQ_0, LESS_EQ_0]) ; 3270 3271val LT_SUB_RCANCEL = Q.store_thm ("LT_SUB_RCANCEL", 3272 `!m n p. n - m < p - m <=> n < p /\ m < p`, 3273 REPEAT GEN_TAC THEN 3274 REWRITE_TAC [GSYM NOT_LESS_EQUAL, LE_SUB_RCANCEL, DE_MORGAN_THM] THEN 3275 MATCH_ACCEPT_TAC CONJ_COMM) ; 3276 3277val LE_SUB_LCANCEL = Q.store_thm ("LE_SUB_LCANCEL", 3278 `!z y x. x - y <= x - z = z <= y \/ x <= y`, 3279 REPEAT INDUCT_TAC THEN 3280 ASM_REWRITE_TAC [ SUB_MONO_EQ, LESS_EQ_MONO, LESS_EQ_REFL, 3281 SUB_0, NOT_SUC_LESS_EQ_0, ZERO_LESS_EQ, 3282 NOT_SUC_LESS_EQ, SUB_LESS_EQ, SUB_LE_SUC]) ; 3283 3284val LT_SUB_LCANCEL = Q.store_thm ("LT_SUB_LCANCEL", 3285 `!z y x. x - y < x - z = z < y /\ z < x`, 3286 REWRITE_TAC [GSYM NOT_LESS_EQUAL, LE_SUB_LCANCEL, DE_MORGAN_THM]) ; 3287 3288val ABS_DIFF_SUMS = Q.store_thm ("ABS_DIFF_SUMS", 3289`!n1 n2 m1 m2. ABS_DIFF (n1 + n2) (m1 + m2) <= ABS_DIFF n1 m1 + ABS_DIFF n2 m2`, 3290 REPEAT INDUCT_TAC THEN 3291 ASM_REWRITE_TAC [ABS_DIFF_ZERO, ABS_DIFF_SUC, ADD, ADD_0, GSYM ADD_SUC, 3292 LESS_EQ_REFL, LESS_EQ_MONO, ZERO_LESS_EQ, ADT_sslem', ADT_sslem] 3293 THENL [ 3294 REWRITE_TAC [GSYM (CONJUNCT2 ADD), ABS_DIFF_PLUS_LE], 3295 REWRITE_TAC [ADD_SUC, ABS_DIFF_PLUS_LE'], 3296 REWRITE_TAC [GSYM (CONJUNCT2 ADD), ADT_splemx], 3297 REWRITE_TAC [ADD_SUC, ADT_splemx'] ]) ; 3298 3299(* ********************************************************************** *) 3300val _ = print "Miscellaneous theorems\n" 3301(* ********************************************************************** *) 3302 3303val FUNPOW_SUC = store_thm ("FUNPOW_SUC", 3304 ���!f n x. FUNPOW f (SUC n) x = f (FUNPOW f n x)���, 3305 GEN_TAC 3306 THEN INDUCT_TAC 3307 THENL [REWRITE_TAC [FUNPOW], 3308 ONCE_REWRITE_TAC [FUNPOW] 3309 THEN ASM_REWRITE_TAC []]); 3310 3311val FUNPOW_0 = store_thm ("FUNPOW_0", 3312 ���FUNPOW f 0 x = x���, 3313 REWRITE_TAC [FUNPOW]); 3314val _ = export_rewrites ["FUNPOW_0"] 3315 3316val FUNPOW_ADD = store_thm ("FUNPOW_ADD", 3317 ���!m n. FUNPOW f (m + n) x = FUNPOW f m (FUNPOW f n x)���, 3318 INDUCT_TAC THENL [ 3319 REWRITE_TAC [ADD_CLAUSES, FUNPOW], 3320 ASM_REWRITE_TAC [ADD_CLAUSES,FUNPOW_SUC] 3321 ]); 3322 3323val FUNPOW_1 = store_thm ("FUNPOW_1", 3324 ���FUNPOW f 1 x = f x���, 3325 REWRITE_TAC [FUNPOW, ONE]); 3326val _ = export_rewrites ["FUNPOW_1"] 3327 3328val NRC_0 = save_thm ("NRC_0", CONJUNCT1 NRC); 3329val _ = export_rewrites ["NRC_0"] 3330 3331val NRC_1 = store_thm ("NRC_1", 3332 ���NRC R 1 x y = R x y���, 3333 SRW_TAC [][ONE, NRC]); 3334val _ = export_rewrites ["NRC_1"] 3335 3336val NRC_ADD_I = store_thm ("NRC_ADD_I", 3337 ���!m n x y z. NRC R m x y /\ NRC R n y z ==> NRC R (m + n) x z���, 3338 INDUCT_TAC THEN SRW_TAC [][NRC, ADD] THEN METIS_TAC []); 3339 3340val NRC_ADD_E = store_thm ("NRC_ADD_E", 3341 ���!m n x z. NRC R (m + n) x z ==> ?y. NRC R m x y /\ NRC R n y z���, 3342 INDUCT_TAC THEN SRW_TAC [][NRC, ADD] THEN METIS_TAC []); 3343 3344val NRC_ADD_EQN = store_thm ("NRC_ADD_EQN", 3345 ���NRC R (m + n) x z = ?y. NRC R m x y /\ NRC R n y z���, 3346 METIS_TAC [NRC_ADD_I, NRC_ADD_E]); 3347 3348val NRC_SUC_RECURSE_LEFT = store_thm ("NRC_SUC_RECURSE_LEFT", 3349 ���NRC R (SUC n) x y = ?z. NRC R n x z /\ R z y���, 3350 METIS_TAC [NRC_1, NRC_ADD_EQN, ADD1]); 3351 3352val NRC_RTC = store_thm ("NRC_RTC", 3353 ���!n x y. NRC R n x y ==> RTC R x y���, 3354 INDUCT_TAC THEN SRW_TAC [][NRC, relationTheory.RTC_RULES] THEN 3355 METIS_TAC [relationTheory.RTC_RULES]); 3356 3357val RTC_NRC = store_thm ("RTC_NRC", 3358 ���!x y. RTC R x y ==> ?n. NRC R n x y���, 3359 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 3360 PROVE_TAC [NRC] (* METIS_TAC bombs *)); 3361 3362val RTC_eq_NRC = store_thm ("RTC_eq_NRC", 3363 ���!R x y. RTC R x y = ?n. NRC R n x y���, 3364 PROVE_TAC[RTC_NRC, NRC_RTC]); 3365 3366val TC_eq_NRC = store_thm ("TC_eq_NRC", 3367 ���!R x y. TC R x y = ?n. NRC R (SUC n) x y���, 3368 REWRITE_TAC [relationTheory.EXTEND_RTC_TC_EQN, RTC_eq_NRC, NRC] THEN 3369 PROVE_TAC[]); 3370 3371val LESS_EQUAL_DIFF = store_thm ("LESS_EQUAL_DIFF", 3372 ���!m n : num. m <= n ==> ?k. m = n - k���, 3373 REPEAT GEN_TAC 3374 THEN SPEC_TAC (���m:num���, ���m:num���) 3375 THEN SPEC_TAC (���n:num���, ���n:num���) 3376 THEN INDUCT_TAC 3377 THENL [REWRITE_TAC [LESS_EQ_0, SUB_0], 3378 REWRITE_TAC [LE] 3379 THEN PROVE_TAC [SUB_0, SUB_MONO_EQ]]); 3380 3381val MOD_2 = store_thm ("MOD_2", 3382 ���!n. n MOD 2 = if EVEN n then 0 else 1���, 3383 GEN_TAC 3384 THEN MATCH_MP_TAC MOD_UNIQUE 3385 THEN ASM_CASES_TAC ���EVEN n��� 3386 THEN POP_ASSUM MP_TAC 3387 THEN REWRITE_TAC [EVEN_EXISTS, GSYM ODD_EVEN, ODD_EXISTS, ADD1] 3388 THEN STRIP_TAC 3389 THEN POP_ASSUM SUBST1_TAC 3390 THEN Q.EXISTS_TAC `m` 3391 THENL [PROVE_TAC [MULT_COMM, ADD_0, TWO, prim_recTheory.LESS_0], 3392 (KNOW_TAC ���(?m' : num. 2 * m + 1 = 2 * m') = F��� 3393 THEN1 PROVE_TAC [EVEN_EXISTS, ODD_EXISTS, ADD1, EVEN_ODD]) 3394 THEN DISCH_THEN (fn th => REWRITE_TAC [th]) 3395 THEN PROVE_TAC [MULT_COMM, ONE, TWO, prim_recTheory.LESS_0, 3396 LESS_MONO_EQ]]); 3397 3398val EVEN_MOD2 = store_thm ("EVEN_MOD2", 3399 ���!x. EVEN x = (x MOD 2 = 0)���, 3400 PROVE_TAC [MOD_2, SUC_NOT, ONE]); 3401 3402val GSYM_MOD_PLUS' = GSYM (SPEC_ALL (UNDISCH_ALL (SPEC_ALL MOD_PLUS))) ; 3403val MOD_LESS' = UNDISCH (Q.SPECL [`a`, `n`] MOD_LESS) ; 3404 3405val SUC_MOD_lem = Q.prove ( 3406 `0 < n ==> (SUC a MOD n = if SUC (a MOD n) = n then 0 else SUC (a MOD n))`, 3407 DISCH_TAC THEN REWRITE_TAC [SUC_ONE_ADD] THEN 3408 CONV_TAC (LHS_CONV (REWR_CONV_A GSYM_MOD_PLUS')) THEN 3409 MP_TAC (Q.SPECL [`n`, `1`] LESS_LESS_CASES) THEN STRIP_TAC 3410 THENL [ ASM_REWRITE_TAC [MOD_1, ADD_0], 3411 RULE_ASSUM_TAC (REWRITE_RULE 3412 [GSYM LESS_EQ_IFF_LESS_SUC, ONE, LESS_EQ_0]) THEN 3413 FULL_SIMP_TAC bool_ss [NOT_LESS_0], 3414 IMP_RES_TAC LESS_MOD THEN ASM_REWRITE_TAC [] THEN 3415 COND_CASES_TAC THEN1 ASM_SIMP_TAC bool_ss [DIVMOD_ID] THEN 3416 irule LESS_MOD THEN ASSUME_TAC MOD_LESS' THEN 3417 RULE_ASSUM_TAC (REWRITE_RULE [GSYM SUC_ONE_ADD, Once LESS_EQ, 3418 Once LESS_OR_EQ]) THEN 3419 REWRITE_TAC [GSYM SUC_ONE_ADD] THEN 3420 FIRST_X_ASSUM DISJ_CASES_TAC THEN 3421 FULL_SIMP_TAC bool_ss [NOT_LESS_0] ]) ; 3422 3423val SUC_MOD = store_thm ("SUC_MOD", 3424 ���!n a b. 0 < n ==> ((SUC a MOD n = SUC b MOD n) = (a MOD n = b MOD n))���, 3425 ASM_SIMP_TAC bool_ss [SUC_MOD_lem] THEN 3426 REPEAT STRIP_TAC THEN 3427 REVERSE EQ_TAC THEN1 SIMP_TAC bool_ss [] THEN 3428 REPEAT COND_CASES_TAC THEN 3429 REWRITE_TAC [numTheory.NOT_SUC, SUC_NOT, INV_SUC_EQ] THEN 3430 ASM_REWRITE_TAC [Once (GSYM INV_SUC_EQ)]) ; 3431 3432val ADD_MOD = Q.store_thm ("ADD_MOD", 3433 `!n a b p. (0 < n:num) ==> 3434 (((a + p) MOD n = (b + p) MOD n) = 3435 (a MOD n = b MOD n))`, 3436GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN HO_MATCH_MP_TAC INDUCTION 3437 THEN SIMP_TAC bool_ss [ADD_CLAUSES, SUC_MOD]); 3438 3439(*---------------------------------------------------------------------------*) 3440(* We should be able to use "by" construct at this phase of development, *) 3441(* surely? *) 3442(*---------------------------------------------------------------------------*) 3443 3444val MOD_ELIM = Q.store_thm ("MOD_ELIM", 3445 `!P x n. 0 < n /\ P x /\ (!y. P (y + n) ==> P y) ==> P (x MOD n)`, 3446 GEN_TAC THEN HO_MATCH_MP_TAC COMPLETE_INDUCTION 3447 THEN REPEAT STRIP_TAC 3448 THEN ASM_CASES_TAC (���x >= n���) THENL 3449 [���P ((x - n) MOD n):bool��� via 3450 (Q.PAT_ASSUM `!x'. A x' ==> !n. Q x' n` (MP_TAC o Q.SPEC `x-n`) THEN 3451 ���x-n < x��� via FULL_SIMP_TAC bool_ss 3452 [GREATER_OR_EQ,SUB_RIGHT_LESS,GREATER_DEF] THEN 3453 METIS_TAC [NOT_ZERO_LT_ZERO,ADD_SYM,LESS_ADD_NONZERO,LESS_TRANS, 3454 SUB_ADD,GREATER_OR_EQ,GREATER_DEF,LESS_OR_EQ,SUB_RIGHT_LESS]) 3455 THEN ���?z. x = z + n��� via (Q.EXISTS_TAC `x - n` THEN 3456 METIS_TAC [SUB_ADD,GREATER_OR_EQ,GREATER_DEF,LESS_OR_EQ]) 3457 THEN RW_TAC bool_ss [] 3458 THEN METIS_TAC [SUB_ADD,GREATER_OR_EQ,GREATER_DEF,LESS_OR_EQ,ADD_MODULUS], 3459 METIS_TAC [LESS_MOD,NOT_LESS,LESS_OR_EQ,GREATER_OR_EQ, GREATER_DEF]]); 3460 3461val DOUBLE_LT = store_thm ("DOUBLE_LT", 3462 ���!p q. 2 * p + 1 < 2 * q = 2 * p < 2 * q���, 3463 REPEAT GEN_TAC 3464 THEN (EQ_TAC THEN1 PROVE_TAC [ADD1, prim_recTheory.SUC_LESS]) 3465 THEN STRIP_TAC 3466 THEN SIMP_TAC boolSimps.bool_ss [GSYM ADD1] 3467 THEN MATCH_MP_TAC LESS_NOT_SUC 3468 THEN ASM_REWRITE_TAC [] 3469 THEN PROVE_TAC [EVEN_ODD, EVEN_DOUBLE, ODD_DOUBLE]); 3470 3471val EXP2_LT = store_thm ("EXP2_LT", 3472 ���!m n. n DIV 2 < 2 ** m = n < 2 ** SUC m���, 3473 REPEAT GEN_TAC 3474 THEN MP_TAC (Q.SPEC `2` DIVISION) 3475 THEN (KNOW_TAC ���0n < 2��� THEN1 REWRITE_TAC [TWO, prim_recTheory.LESS_0]) 3476 THEN SIMP_TAC boolSimps.bool_ss [] 3477 THEN STRIP_TAC 3478 THEN DISCH_THEN (MP_TAC o Q.SPEC `n`) 3479 THEN DISCH_THEN (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [th]))) 3480 THEN ONCE_REWRITE_TAC [MULT_COMM] 3481 THEN SIMP_TAC boolSimps.bool_ss [EXP, MOD_2] 3482 THEN (ASM_CASES_TAC ���EVEN n��� THEN ASM_SIMP_TAC boolSimps.bool_ss []) 3483 THENL [REWRITE_TAC [TWO, ADD_0, LESS_MULT_MONO], 3484 REWRITE_TAC [DOUBLE_LT] 3485 THEN REWRITE_TAC [TWO, ADD_0, LESS_MULT_MONO]]); 3486 3487val SUB_LESS = Q.store_thm ("SUB_LESS", 3488 `!m n. 0 < n /\ n <= m ==> m-n < m`, 3489 REPEAT STRIP_TAC THEN 3490 ���?p. m = p+n��� via METIS_TAC [LESS_EQ_EXISTS,ADD_SYM] 3491 THEN RW_TAC bool_ss [ADD_SUB] 3492 THEN METIS_TAC [LESS_ADD_NONZERO,NOT_ZERO_LT_ZERO]); 3493 3494val SUB_MOD = Q.store_thm ("SUB_MOD", 3495 `!m n. 0<n /\ n <= m ==> ((m-n) MOD n = m MOD n)`, 3496 METIS_TAC [ADD_MODULUS,ADD_SUB,LESS_EQ_EXISTS,ADD_SYM]); 3497 3498fun Cases (asl,g) = 3499 let val (v,_) = dest_forall g 3500 in GEN_TAC THEN STRUCT_CASES_TAC (SPEC v num_CASES) 3501 end (asl,g); 3502 3503fun Cases_on v (asl,g) = STRUCT_CASES_TAC (SPEC v num_CASES) (asl,g); 3504 3505val ONE_LT_MULT_IMP = Q.store_thm ("ONE_LT_MULT_IMP", 3506 `!p q. 1 < p /\ 0 < q ==> 1 < p * q`, 3507 REPEAT Cases THEN 3508 RW_TAC bool_ss [MULT_CLAUSES,ADD_CLAUSES] THENL 3509 [METIS_TAC [LESS_REFL], 3510 POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC THEN 3511 RW_TAC bool_ss [ONE,LESS_MONO_EQ] THEN 3512 METIS_TAC [LESS_IMP_LESS_ADD, ADD_ASSOC]]); 3513 3514val ONE_LT_MULT = Q.store_thm ("ONE_LT_MULT", 3515 `!x y. 1 < x * y = 0 < x /\ 1 < y \/ 0 < y /\ 1 < x`, 3516 REWRITE_TAC [ONE] THEN INDUCT_TAC THEN 3517 RW_TAC bool_ss [ADD_CLAUSES, MULT_CLAUSES,LESS_REFL,LESS_0] THENL 3518 [METIS_TAC [NOT_SUC_LESS_EQ_0,LESS_OR_EQ], 3519 Cases_on ���y:num��� THEN 3520 RW_TAC bool_ss [MULT_CLAUSES,ADD_CLAUSES,LESS_REFL, 3521 LESS_MONO_EQ,ZERO_LESS_ADD,LESS_0] THEN 3522 METIS_TAC [ZERO_LESS_MULT]]); 3523 3524val ONE_LT_EXP = Q.store_thm ("ONE_LT_EXP", 3525 `!x y. 1 < x ** y = 1 < x /\ 0 < y`, 3526 GEN_TAC THEN INDUCT_TAC THEN 3527 RW_TAC bool_ss [EXP,ONE_LT_MULT,LESS_REFL,LESS_0,ZERO_LT_EXP] THEN 3528 METIS_TAC [SUC_LESS, ONE]); 3529 3530(*---------------------------------------------------------------------------*) 3531(* Calculating DIV and MOD by repeated subtraction. We define a *) 3532(* tail-recursive function DIVMOD by wellfounded recursion. We hand-roll the *) 3533(* definition and induction theorem, because, as of now, tfl is not *) 3534(* at this point in the build. *) 3535(*---------------------------------------------------------------------------*) 3536 3537val findq_lemma = prove( 3538 ���~(n = 0) /\ ~(m < 2 * n) ==> m - 2 * n < m - n���, 3539 REPEAT STRIP_TAC THEN 3540 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [NOT_LESS]) THEN 3541 SRW_TAC [][SUB_LEFT_LESS, SUB_RIGHT_ADD, SUB_RIGHT_LESS, ADD_CLAUSES, 3542 SUB_LEFT_ADD] 3543 THENL [ 3544 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN Q.EXISTS_TAC `n` THEN 3545 ASM_REWRITE_TAC [] THEN 3546 SIMP_TAC bool_ss [Once (GSYM MULT_LEFT_1), SimpLHS] THEN 3547 REWRITE_TAC [LT_MULT_RCANCEL] THEN 3548 REWRITE_TAC [TWO,ONE,LESS_MONO_EQ,prim_recTheory.LESS_0] THEN 3549 PROVE_TAC [NOT_ZERO_LT_ZERO], 3550 3551 Q.SUBGOAL_THEN `2 * n <= 1 * n` MP_TAC 3552 THEN1 PROVE_TAC [LESS_EQ_TRANS, MULT_LEFT_1] THEN 3553 ASM_REWRITE_TAC [LE_MULT_RCANCEL, TWO, ONE, LESS_EQ_MONO, 3554 NOT_SUC_LESS_EQ_0], 3555 3556 Q_TAC SUFF_TAC `n < 2 * n` THEN1 3557 PROVE_TAC [ADD_COMM, LT_ADD_LCANCEL] THEN 3558 Q_TAC SUFF_TAC `1 * n < 2 * n` THEN1 SRW_TAC [][MULT_CLAUSES] THEN 3559 SRW_TAC [][LT_MULT_RCANCEL] THENL [ 3560 PROVE_TAC [NOT_ZERO_LT_ZERO], 3561 SRW_TAC [][ONE,TWO, LESS_MONO_EQ, prim_recTheory.LESS_0] 3562 ], 3563 3564 PROVE_TAC [NOT_LESS_EQUAL] 3565 ]); 3566 3567val findq_thm = let 3568 open pairTheory relationTheory 3569 val M = ���\f (a,m,n). if n = 0 then a 3570 else let d = 2 * n 3571 in 3572 if m < d then a else f (2 * a, m, d)��� 3573 val measure = ���measure (\ (a:num,m:num,n:num). m - n)��� 3574 val defn = new_definition("findq_def", ���findq = WFREC ^measure ^M���) 3575 val th0 = MP (MATCH_MP WFREC_COROLLARY defn) 3576 (ISPEC (rand measure) prim_recTheory.WF_measure) 3577 val lemma = prove( 3578 ���~(n = 0) ==> ((let d = 2 * n in if m < d then x 3579 else if m - d < m - n then f d else z) = 3580 (let d = 2 * n in if m < d then x else f d))���, 3581 LET_ELIM_TAC THEN Q.ASM_CASES_TAC `m < d` THEN ASM_REWRITE_TAC [] THEN 3582 Q.UNABBREV_TAC `d` THEN SRW_TAC [][findq_lemma]) 3583in 3584 save_thm ("findq_thm", 3585 SIMP_RULE (srw_ss()) [RESTRICT_DEF, prim_recTheory.measure_thm, 3586 lemma] 3587 (Q.SPEC `(a,m,n)` th0)) 3588end 3589 3590val findq_eq_0 = store_thm ("findq_eq_0", 3591 ���!a m n. (findq (a, m, n) = 0) = (a = 0)���, 3592 REPEAT GEN_TAC THEN 3593 Q_TAC SUFF_TAC 3594 `!x a m n. (x = m - n) ==> ((findq (a, m, n) = 0) = (a = 0))` THEN1 3595 SRW_TAC [][] THEN 3596 HO_MATCH_MP_TAC COMPLETE_INDUCTION THEN REPEAT STRIP_TAC THEN 3597 ONCE_REWRITE_TAC [findq_thm] THEN SRW_TAC [][LET_THM] THEN 3598 RULE_ASSUM_TAC (SIMP_RULE (bool_ss ++ boolSimps.DNF_ss) []) THEN 3599 FIRST_X_ASSUM (Q.SPECL_THEN [`2 * a`, `m`, `2 * n`] MP_TAC) THEN 3600 SRW_TAC [][findq_lemma, MULT_EQ_0, TWO, ONE, NOT_SUC]); 3601 3602val findq_divisor = store_thm ("findq_divisor", 3603 ���n <= m ==> findq (a, m, n) * n <= a * m���, 3604 Q_TAC SUFF_TAC 3605 `!x a m n. (x = m - n) /\ n <= m ==> 3606 findq (a, m, n) * n <= a * m` THEN1 3607 SRW_TAC [][] THEN 3608 HO_MATCH_MP_TAC COMPLETE_INDUCTION THEN SRW_TAC [boolSimps.DNF_ss][] THEN 3609 ONCE_REWRITE_TAC [findq_thm] THEN 3610 SRW_TAC [][LET_THM, MULT_CLAUSES, ZERO_LESS_EQ, LE_MULT_LCANCEL, 3611 LESS_IMP_LESS_OR_EQ] THEN 3612 FIRST_X_ASSUM (Q.SPECL_THEN [`2 * a`, `m`, `2 * n`] MP_TAC) THEN 3613 ASM_SIMP_TAC (srw_ss())[findq_lemma, GSYM NOT_LESS] THEN 3614 Q.SUBGOAL_THEN `findq (2 * a,m,2 * n) * (2 * n) = 3615 2 * (findq (2 * a, m, 2 * n) * n)` SUBST_ALL_TAC THEN1 3616 SRW_TAC [][AC MULT_COMM MULT_ASSOC] THEN 3617 Q.SUBGOAL_THEN `2 * a * m = 2 * (a * m)` SUBST_ALL_TAC THEN1 3618 SRW_TAC [][AC MULT_COMM MULT_ASSOC] THEN 3619 SRW_TAC [][LT_MULT_LCANCEL, TWO, ONE, prim_recTheory.LESS_0]); 3620 3621val divmod_lemma = prove( 3622 ���~(n = 0) /\ ~(m < n) ==> m - n * findq (1, m, n) < m���, 3623 SRW_TAC [][NOT_LESS, SUB_RIGHT_LESS, NOT_ZERO_LT_ZERO] THENL [ 3624 ONCE_REWRITE_TAC [ADD_COMM] THEN MATCH_MP_TAC LESS_ADD_NONZERO THEN 3625 SRW_TAC [][MULT_EQ_0, ONE, NOT_SUC, findq_eq_0] THEN 3626 SRW_TAC [][NOT_ZERO_LT_ZERO], 3627 PROVE_TAC [LESS_LESS_EQ_TRANS] 3628 ]); 3629 3630(*---------------------------------------------------------------------------*) 3631(* DIVMOD (a,m,n) = if n = 0 then (0,0) else *) 3632(* if m < n then (a, m) else *) 3633(* let q = findq (1, m, n) *) 3634(* in DIVMOD (a + q, m - n * q, n) *) 3635(*---------------------------------------------------------------------------*) 3636 3637val DIVMOD_THM = let 3638 open relationTheory pairTheory 3639 val M = ���\f (a,m,n). if n = 0 then (0,0) 3640 else if m < n then (a, m) 3641 else let q = findq (1, m, n) 3642 in 3643 f (a + q, m - n * q, n)��� 3644 val measure = ���measure ((FST o SND) : num#num#num -> num)��� 3645 val defn = new_definition("DIVMOD_DEF", ���DIVMOD = WFREC ^measure ^M���) 3646 val th0 = REWRITE_RULE [prim_recTheory.WF_measure] 3647 (MATCH_MP WFREC_COROLLARY defn) 3648 val th1 = SIMP_RULE (srw_ss()) [RESTRICT_DEF, prim_recTheory.measure_thm] 3649 (Q.SPEC `(a,m,n)` th0) 3650 val lemma = prove( 3651 ���~(n = 0) /\ ~(m < n) ==> 3652 ((let q = findq (1,m,n) in if m - n * q < m then f q else z) = 3653 (let q = findq (1,m,n) in f q))���, 3654 SRW_TAC [][LET_THM, divmod_lemma]) 3655in 3656 save_thm ("DIVMOD_THM", SIMP_RULE (srw_ss()) [lemma] th1) 3657end 3658 3659(*---------------------------------------------------------------------------*) 3660(* Correctness of DIVMOD *) 3661(*---------------------------------------------------------------------------*) 3662 3663val core_divmod_sub_lemma = prove( 3664 ���0 < n /\ n * q <= m ==> 3665 (m - n * q = if m < (q + 1) * n then m MOD n 3666 else m DIV n * n + m MOD n - q * n)���, 3667 REPEAT STRIP_TAC THEN COND_CASES_TAC THENL [ 3668 ASM_SIMP_TAC (srw_ss()) [SUB_RIGHT_EQ] THEN DISJ1_TAC THEN 3669 Q_TAC SUFF_TAC `m DIV n = q` THEN1 PROVE_TAC [DIVISION, MULT_COMM] THEN 3670 MATCH_MP_TAC DIV_UNIQUE THEN 3671 Q.EXISTS_TAC `m - n * q` THEN 3672 SRW_TAC [][SUB_LEFT_ADD] THENL [ 3673 PROVE_TAC [LESS_EQUAL_ANTISYM, MULT_COMM], 3674 METIS_TAC [ADD_COMM, MULT_COMM, ADD_SUB], 3675 SRW_TAC [][SUB_RIGHT_LESS] THEN 3676 FULL_SIMP_TAC (srw_ss()) [RIGHT_ADD_DISTRIB, MULT_CLAUSES, 3677 AC MULT_COMM MULT_ASSOC, 3678 AC ADD_COMM ADD_ASSOC] 3679 ], 3680 3681 ASM_SIMP_TAC (srw_ss()) [GSYM DIVISION] THEN 3682 SIMP_TAC (srw_ss()) [AC MULT_COMM MULT_ASSOC] 3683 ]); 3684 3685val MOD_SUB = store_thm ("MOD_SUB", 3686 ���0 < n /\ n * q <= m ==> ((m - n * q) MOD n = m MOD n)���, 3687 REPEAT STRIP_TAC THEN MATCH_MP_TAC MOD_UNIQUE THEN 3688 Q.EXISTS_TAC `m DIV n - q` THEN 3689 Q.SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THEN1 SRW_TAC [][NOT_ZERO_LT_ZERO] THEN 3690 ASM_SIMP_TAC (srw_ss()) [RIGHT_SUB_DISTRIB, DIVISION, SUB_RIGHT_ADD, 3691 LE_MULT_RCANCEL, DIV_LE_X, core_divmod_sub_lemma]); 3692 3693val DIV_SUB = store_thm ("DIV_SUB", 3694 ���0 < n /\ n * q <= m ==> ((m - n * q) DIV n = m DIV n - q)���, 3695 REPEAT STRIP_TAC THEN 3696 MATCH_MP_TAC DIV_UNIQUE THEN Q.EXISTS_TAC `m MOD n` THEN 3697 Q.SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THEN1 SRW_TAC [][NOT_ZERO_LT_ZERO] THEN 3698 ASM_SIMP_TAC (srw_ss()) [DIVISION, RIGHT_SUB_DISTRIB, SUB_RIGHT_ADD, 3699 LE_MULT_RCANCEL, DIV_LE_X, core_divmod_sub_lemma]); 3700 3701val DIVMOD_CORRECT = Q.store_thm ("DIVMOD_CORRECT", 3702 `!m n a. 0<n ==> (DIVMOD (a,m,n) = (a + (m DIV n), m MOD n))`, 3703 HO_MATCH_MP_TAC COMPLETE_INDUCTION THEN 3704 SRW_TAC [DNF_ss][AND_IMP_INTRO] THEN 3705 PURE_ONCE_REWRITE_TAC [DIVMOD_THM] THEN 3706 RW_TAC bool_ss [] THENL [ 3707 METIS_TAC [LESS_REFL], 3708 METIS_TAC [LESS_REFL], 3709 METIS_TAC [LESS_DIV_EQ_ZERO,ADD_CLAUSES], 3710 METIS_TAC [LESS_MOD,ADD_CLAUSES], 3711 FIRST_X_ASSUM (Q.SPECL_THEN [`m - n * q`, `n`, `a + q`] MP_TAC) THEN 3712 ASM_SIMP_TAC (srw_ss()) [SUB_RIGHT_LESS] THEN 3713 Q.SUBGOAL_THEN `m < n * q + m` ASSUME_TAC THENL [ 3714 SIMP_TAC bool_ss [SimpRHS, Once ADD_COMM] THEN 3715 MATCH_MP_TAC LESS_ADD_NONZERO THEN 3716 SRW_TAC [][MULT_EQ_0, Abbr`q`, findq_eq_0, ONE, NOT_SUC], 3717 ALL_TAC 3718 ] THEN ASM_REWRITE_TAC [] THEN 3719 Q.SUBGOAL_THEN `0 < m` ASSUME_TAC THEN1 3720 PROVE_TAC [NOT_LESS, LESS_LESS_EQ_TRANS] THEN 3721 ASM_REWRITE_TAC [] THEN 3722 DISCH_THEN SUBST_ALL_TAC THEN 3723 Q.SUBGOAL_THEN `n * q <= m` ASSUME_TAC THEN1 3724 METIS_TAC [findq_divisor, NOT_LESS, MULT_LEFT_1, MULT_COMM] THEN 3725 Q.SUBGOAL_THEN `q <= m DIV n` ASSUME_TAC THEN1 3726 SRW_TAC [][X_LE_DIV, MULT_COMM] THEN 3727 SRW_TAC [][] THENL [ 3728 ONCE_REWRITE_TAC [GSYM ADD_ASSOC] THEN 3729 REWRITE_TAC [EQ_ADD_LCANCEL] THEN 3730 ASM_SIMP_TAC (srw_ss()) [DIV_SUB] THEN 3731 SRW_TAC [][SUB_LEFT_ADD] THEN1 METIS_TAC [LESS_EQUAL_ANTISYM] THEN 3732 METIS_TAC [ADD_SUB, ADD_COMM], 3733 ASM_SIMP_TAC (srw_ss()) [MOD_SUB] 3734 ] 3735 ]); 3736 3737(*---------------------------------------------------------------------------*) 3738(* For calculation *) 3739(*---------------------------------------------------------------------------*) 3740 3741val DIVMOD_CALC = Q.store_thm ("DIVMOD_CALC", 3742 `(!m n. 0<n ==> (m DIV n = FST(DIVMOD(0, m, n)))) /\ 3743 (!m n. 0<n ==> (m MOD n = SND(DIVMOD(0, m, n))))`, 3744 SRW_TAC [][DIVMOD_CORRECT,ADD_CLAUSES]); 3745 3746(* ---------------------------------------------------------------------- 3747 Support for using congruential rewriting and MOD 3748 ---------------------------------------------------------------------- *) 3749 3750val MODEQ_DEF = new_definition( 3751 "MODEQ_DEF", 3752 ���MODEQ n m1 m2 = ?a b. a * n + m1 = b * n + m2���); 3753 3754val MODEQ_0_CONG = store_thm ("MODEQ_0_CONG", 3755 ���MODEQ 0 m1 m2 <=> (m1 = m2)���, 3756 SRW_TAC [][MODEQ_DEF, MULT_CLAUSES, ADD_CLAUSES]); 3757 3758val MODEQ_NONZERO_MODEQUALITY = store_thm ("MODEQ_NONZERO_MODEQUALITY", 3759 ���0 < n ==> (MODEQ n m1 m2 <=> (m1 MOD n = m2 MOD n))���, 3760 SRW_TAC [][MODEQ_DEF] THEN 3761 Q.SPEC_THEN `n` (fn th => th |> UNDISCH |> ASSUME_TAC) DIVISION THEN 3762 POP_ASSUM (fn th => Q.SPEC_THEN `m1` STRIP_ASSUME_TAC th THEN 3763 Q.SPEC_THEN `m2` STRIP_ASSUME_TAC th) THEN 3764 MAP_EVERY Q.ABBREV_TAC [`q1 = m1 DIV n`, `r1 = m1 MOD n`, 3765 `q2 = m2 DIV n`, `r2 = m2 MOD n`] THEN 3766 markerLib.RM_ALL_ABBREVS_TAC THEN SRW_TAC [][EQ_IMP_THM] THENL [ 3767 `(a * n + (q1 * n + r1)) MOD n = r1` 3768 by (MATCH_MP_TAC MOD_UNIQUE THEN Q.EXISTS_TAC `a + q1` THEN 3769 SIMP_TAC (srw_ss()) [MULT_ASSOC, RIGHT_ADD_DISTRIB, ADD_ASSOC] THEN 3770 SRW_TAC [][]) THEN 3771 POP_ASSUM (SUBST1_TAC o SYM) THEN 3772 MATCH_MP_TAC MOD_UNIQUE THEN Q.EXISTS_TAC `b + q2` THEN 3773 SRW_TAC [][ADD_ASSOC, RIGHT_ADD_DISTRIB], 3774 MAP_EVERY Q.EXISTS_TAC [`q2`, `q1`] THEN 3775 SRW_TAC [][AC ADD_ASSOC ADD_COMM] 3776 ]); 3777 3778val MODEQ_THM = store_thm ("MODEQ_THM", 3779 ���MODEQ n m1 m2 <=> (n = 0) /\ (m1 = m2) \/ 0 < n /\ (m1 MOD n = m2 MOD n)���, 3780 METIS_TAC [MODEQ_0_CONG, MODEQ_NONZERO_MODEQUALITY, NOT_ZERO_LT_ZERO]); 3781 3782val MODEQ_INTRO_CONG = store_thm ("MODEQ_INTRO_CONG", 3783 ���0 < n ==> MODEQ n e0 e1 ==> (e0 MOD n = e1 MOD n)���, 3784 METIS_TAC [MODEQ_NONZERO_MODEQUALITY]); 3785 3786val MODEQ_PLUS_CONG = store_thm ("MODEQ_PLUS_CONG", 3787 ���MODEQ n x0 x1 ==> MODEQ n y0 y1 ==> MODEQ n (x0 + y0) (x1 + y1)���, 3788 Q.ID_SPEC_TAC `n` THEN SIMP_TAC (srw_ss() ++ DNF_ss)[MODEQ_THM, LESS_REFL] THEN 3789 SRW_TAC [][Once (GSYM MOD_PLUS)] THEN SRW_TAC [][MOD_PLUS]); 3790 3791val MODEQ_MULT_CONG = store_thm ("MODEQ_MULT_CONG", 3792 ���MODEQ n x0 x1 ==> MODEQ n y0 y1 ==> MODEQ n (x0 * y0) (x1 * y1)���, 3793 Q.ID_SPEC_TAC `n` THEN SIMP_TAC (srw_ss() ++ DNF_ss)[MODEQ_THM, LESS_REFL] THEN 3794 SRW_TAC [][Once (GSYM MOD_TIMES2)] THEN SRW_TAC [][MOD_TIMES2]); 3795 3796val MODEQ_REFL = store_thm ("MODEQ_REFL", 3797 ���!x. MODEQ n x x���, 3798 SRW_TAC [][MODEQ_THM, GSYM NOT_ZERO_LT_ZERO]); 3799 3800val MODEQ_SUC_CONG = store_thm("MODEQ_SUC_CONG", 3801 ���MODEQ n x y ==> MODEQ n (SUC x) (SUC y)���, 3802 SRW_TAC[][ADD1] >> irule MODEQ_PLUS_CONG >> SRW_TAC [][MODEQ_REFL]); 3803 3804val MODEQ_EXP_CONG = store_thm( 3805 "MODEQ_EXP_CONG", 3806 ���MODEQ n x y ==> MODEQ n (x EXP e) (y EXP e)���, 3807 Q.ID_SPEC_TAC `e` >> 3808 INDUCT_TAC >> SRW_TAC[][EXP, MODEQ_REFL] >> 3809 irule MODEQ_MULT_CONG >> SRW_TAC[][]) 3810 3811val EXP_MOD = save_thm( 3812 "EXP_MOD", 3813 MODEQ_EXP_CONG |> SIMP_RULE bool_ss [GSYM NOT_LT_ZERO_EQ_ZERO, 3814 ASSUME ���0 < n���, MODEQ_THM] 3815 |> INST [���y:num��� |-> ���x MOD n���, ���e1:num��� |-> ���e:num���, 3816 ���e2:num��� |-> ���e:num���] 3817 |> SIMP_RULE bool_ss [MATCH_MP MOD_MOD (ASSUME ���0 < n���)] 3818 |> SYM |> DISCH_ALL) 3819 3820val MODEQ_SYM = store_thm ("MODEQ_SYM", 3821 ���MODEQ n x y <=> MODEQ n y x���, 3822 SRW_TAC [][MODEQ_THM] THEN METIS_TAC []); 3823 3824val MODEQ_TRANS = store_thm ("MODEQ_TRANS", 3825 ���!x y z. MODEQ n x y /\ MODEQ n y z ==> MODEQ n x z���, 3826 Q.ID_SPEC_TAC `n` THEN SIMP_TAC (srw_ss() ++ DNF_ss) [MODEQ_THM, LESS_REFL]); 3827 3828val MODEQ_NUMERAL = store_thm ("MODEQ_NUMERAL", 3829 ���(NUMERAL n <= NUMERAL m ==> 3830 MODEQ (NUMERAL (BIT1 n)) (NUMERAL (BIT1 m)) 3831 (NUMERAL (BIT1 m) MOD NUMERAL (BIT1 n))) /\ 3832 (NUMERAL n <= NUMERAL m ==> 3833 MODEQ (NUMERAL (BIT1 n)) (NUMERAL (BIT2 m)) 3834 (NUMERAL (BIT2 m) MOD NUMERAL (BIT1 n))) /\ 3835 (NUMERAL n <= NUMERAL m ==> 3836 MODEQ (NUMERAL (BIT2 n)) (NUMERAL (BIT2 m)) 3837 (NUMERAL (BIT2 m) MOD NUMERAL (BIT2 n))) /\ 3838 (NUMERAL n < NUMERAL m ==> 3839 MODEQ (NUMERAL (BIT2 n)) (NUMERAL (BIT1 m)) 3840 (NUMERAL (BIT1 m) MOD NUMERAL (BIT2 n)))���, 3841 SIMP_TAC (srw_ss()) 3842 [MODEQ_NONZERO_MODEQUALITY, BIT1, BIT2, ADD_CLAUSES, ALT_ZERO, 3843 NUMERAL_DEF, MOD_MOD, LESS_0]) 3844 3845val MODEQ_MOD = store_thm ("MODEQ_MOD", 3846 ���0 < n ==> MODEQ n (x MOD n) x���, 3847 SIMP_TAC (srw_ss()) [MODEQ_NONZERO_MODEQUALITY, MOD_MOD]); 3848 3849val MODEQ_0 = store_thm ("MODEQ_0", 3850 ���0 < n ==> MODEQ n n 0���, 3851 SIMP_TAC (srw_ss()) [MODEQ_NONZERO_MODEQUALITY, DIVMOD_ID, ZERO_MOD]); 3852 3853val modss = simpLib.add_relsimp {refl = MODEQ_REFL, trans = MODEQ_TRANS, 3854 weakenings = [MODEQ_INTRO_CONG], 3855 subsets = [], 3856 rewrs = [MODEQ_NUMERAL, MODEQ_MOD, MODEQ_0]} 3857 (srw_ss()) ++ 3858 SSFRAG {dprocs = [], ac = [], rewrs = [], 3859 congs = [MODEQ_PLUS_CONG, MODEQ_MULT_CONG, MODEQ_SUC_CONG], 3860 filter = NONE, convs = [], name = NONE} 3861 3862val result1 = 3863 SIMP_CONV modss [ASSUME ���0 < 6���, LESS_EQ_REFL, ASSUME ���2 < 3���, 3864 DIVMOD_ID, MULT_CLAUSES, ADD_CLAUSES, 3865 ASSUME ���7 MOD 6 = 1���] ���(6 * x + 7 + 6 * y) MOD 6���; 3866 3867val result2 = 3868 SIMP_CONV modss 3869 [ASSUME ���0 < n���, MULT_CLAUSES, ADD_CLAUSES] 3870 ���(4 + 3 * n + 1) MOD n��� 3871 3872(* ---------------------------------------------------------------------- 3873 set up characterisation as a standard algebraic type 3874 ---------------------------------------------------------------------- *) 3875 3876val num_case_eq = Q.store_thm( 3877 "num_case_eq", 3878 ���(num_CASE n zc sc = v) <=> 3879 (n = 0) /\ (zc = v) \/ ?x. (n = SUC x) /\ (sc x = v)���, 3880 Q.SPEC_THEN ���n��� STRUCT_CASES_TAC num_CASES THEN 3881 SRW_TAC [][num_case_def, SUC_NOT, INV_SUC_EQ]); 3882 3883val _ = TypeBase.export 3884 [TypeBasePure.mk_datatype_info_no_simpls 3885 {ax=TypeBasePure.ORIG prim_recTheory.num_Axiom, 3886 case_def=num_case_def, 3887 case_cong=num_case_cong, 3888 case_eq = num_case_eq, 3889 induction=TypeBasePure.ORIG numTheory.INDUCTION, 3890 nchotomy=num_CASES, 3891 size=SOME(���\x:num. x���, TypeBasePure.ORIG boolTheory.REFL_CLAUSE), 3892 encode=NONE, 3893 fields=[], 3894 accessors=[], 3895 updates=[], 3896 recognizers=[], 3897 destructors=[CONJUNCT2(prim_recTheory.PRE)], 3898 lift=SOME(mk_var("numSyntax.lift_num",���:'type -> num -> 'term���)), 3899 one_one=SOME prim_recTheory.INV_SUC_EQ, 3900 distinct=SOME numTheory.NOT_SUC}]; 3901 3902val datatype_num = store_thm( 3903 "datatype_num", 3904 ���DATATYPE (num 0 SUC)���, 3905 REWRITE_TAC[DATATYPE_TAG_THM]); 3906 3907val _ = export_theory() 3908