src/ZF/Arith.ML
 author paulson Fri Jan 29 17:08:20 1999 +0100 (1999-01-29) changeset 6163 be8234f37e48 parent 6153 bff90585cce5 child 7499 23e090051cb8 permissions -rw-r--r--
expandshort
 paulson@1793 ` 1` ```(* Title: ZF/Arith.ML ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@1461 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1992 University of Cambridge ``` clasohm@0 ` 5` paulson@1609 ` 6` ```Arithmetic operators and their definitions ``` clasohm@0 ` 7` clasohm@0 ` 8` ```Proofs about elementary arithmetic: addition, multiplication, etc. ``` clasohm@0 ` 9` ```*) ``` clasohm@0 ` 10` clasohm@0 ` 11` ```(*"Difference" is subtraction of natural numbers. ``` clasohm@0 ` 12` ``` There are no negative numbers; we have ``` clasohm@0 ` 13` ``` m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n. ``` clasohm@0 ` 14` ``` Also, rec(m, 0, %z w.z) is pred(m). ``` clasohm@0 ` 15` ```*) ``` clasohm@0 ` 16` paulson@2469 ` 17` ```Addsimps [rec_type, nat_0_le, nat_le_refl]; ``` lcp@25 ` 18` ```val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]; ``` clasohm@0 ` 19` paulson@5137 ` 20` ```Goal "[| 0 EX j: nat. k = succ(j)"; ``` paulson@1708 ` 21` ```by (etac rev_mp 1); ``` paulson@6070 ` 22` ```by (induct_tac "k" 1); ``` paulson@2469 ` 23` ```by (Simp_tac 1); ``` paulson@3016 ` 24` ```by (Blast_tac 1); ``` paulson@1708 ` 25` ```val lemma = result(); ``` paulson@1708 ` 26` paulson@1708 ` 27` ```(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *) ``` paulson@1708 ` 28` ```bind_thm ("zero_lt_natE", lemma RS bexE); ``` paulson@1708 ` 29` paulson@1708 ` 30` clasohm@0 ` 31` ```(** Addition **) ``` clasohm@0 ` 32` paulson@6070 ` 33` ```Goal "[| m:nat; n:nat |] ==> m #+ n : nat"; ``` paulson@6070 ` 34` ```by (induct_tac "m" 1); ``` paulson@6070 ` 35` ```by Auto_tac; ``` paulson@6070 ` 36` ```qed "add_type"; ``` paulson@6070 ` 37` ```Addsimps [add_type]; ``` paulson@6153 ` 38` ```AddTCs [add_type]; ``` paulson@2469 ` 39` clasohm@0 ` 40` ```(** Multiplication **) ``` clasohm@0 ` 41` paulson@6070 ` 42` ```Goal "[| m:nat; n:nat |] ==> m #* n : nat"; ``` paulson@6070 ` 43` ```by (induct_tac "m" 1); ``` paulson@6070 ` 44` ```by Auto_tac; ``` paulson@6070 ` 45` ```qed "mult_type"; ``` paulson@6070 ` 46` ```Addsimps [mult_type]; ``` paulson@6153 ` 47` ```AddTCs [mult_type]; ``` clasohm@0 ` 48` paulson@2469 ` 49` clasohm@0 ` 50` ```(** Difference **) ``` clasohm@0 ` 51` paulson@6070 ` 52` ```Goal "[| m:nat; n:nat |] ==> m #- n : nat"; ``` paulson@6070 ` 53` ```by (induct_tac "n" 1); ``` paulson@6070 ` 54` ```by Auto_tac; ``` paulson@6070 ` 55` ```by (fast_tac (claset() addIs [nat_case_type]) 1); ``` paulson@6070 ` 56` ```qed "diff_type"; ``` paulson@6070 ` 57` ```Addsimps [diff_type]; ``` paulson@6153 ` 58` ```AddTCs [diff_type]; ``` clasohm@0 ` 59` paulson@6070 ` 60` ```Goal "n:nat ==> 0 #- n = 0"; ``` paulson@6070 ` 61` ```by (induct_tac "n" 1); ``` paulson@6070 ` 62` ```by Auto_tac; ``` paulson@6070 ` 63` ```qed "diff_0_eq_0"; ``` clasohm@0 ` 64` paulson@6070 ` 65` ```(*Must simplify BEFORE the induction: else we get a critical pair*) ``` paulson@6070 ` 66` ```Goal "[| m:nat; n:nat |] ==> succ(m) #- succ(n) = m #- n"; ``` paulson@6070 ` 67` ```by (Asm_simp_tac 1); ``` paulson@6070 ` 68` ```by (induct_tac "n" 1); ``` paulson@6070 ` 69` ```by Auto_tac; ``` paulson@6070 ` 70` ```qed "diff_succ_succ"; ``` clasohm@0 ` 71` paulson@6070 ` 72` ```Addsimps [diff_0_eq_0, diff_succ_succ]; ``` paulson@2469 ` 73` paulson@6070 ` 74` ```(*This defining property is no longer wanted*) ``` paulson@6070 ` 75` ```Delsimps [diff_SUCC]; ``` clasohm@0 ` 76` clasohm@0 ` 77` ```val prems = goal Arith.thy ``` lcp@25 ` 78` ``` "[| m:nat; n:nat |] ==> m #- n le m"; ``` lcp@25 ` 79` ```by (rtac (prems MRS diff_induct) 1); ``` lcp@25 ` 80` ```by (etac leE 3); ``` clasohm@0 ` 81` ```by (ALLGOALS ``` paulson@5529 ` 82` ``` (asm_simp_tac (simpset() addsimps prems @ [le_iff, nat_into_Ord]))); ``` clasohm@760 ` 83` ```qed "diff_le_self"; ``` clasohm@0 ` 84` clasohm@0 ` 85` ```(*** Simplification over add, mult, diff ***) ``` clasohm@0 ` 86` clasohm@0 ` 87` ```val arith_typechecks = [add_type, mult_type, diff_type]; ``` clasohm@0 ` 88` clasohm@0 ` 89` clasohm@0 ` 90` ```(*** Addition ***) ``` clasohm@0 ` 91` clasohm@0 ` 92` ```(*Associative law for addition*) ``` paulson@6070 ` 93` ```Goal "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"; ``` paulson@6070 ` 94` ```by (induct_tac "m" 1); ``` paulson@6070 ` 95` ```by Auto_tac; ``` paulson@6070 ` 96` ```qed "add_assoc"; ``` clasohm@0 ` 97` clasohm@0 ` 98` ```(*The following two lemmas are used for add_commute and sometimes ``` clasohm@0 ` 99` ``` elsewhere, since they are safe for rewriting.*) ``` paulson@6070 ` 100` ```Goal "m:nat ==> m #+ 0 = m"; ``` paulson@6070 ` 101` ```by (induct_tac "m" 1); ``` paulson@6070 ` 102` ```by Auto_tac; ``` paulson@6070 ` 103` ```qed "add_0_right"; ``` clasohm@0 ` 104` paulson@6070 ` 105` ```Goal "m:nat ==> m #+ succ(n) = succ(m #+ n)"; ``` paulson@6070 ` 106` ```by (induct_tac "m" 1); ``` paulson@6070 ` 107` ```by Auto_tac; ``` paulson@6070 ` 108` ```qed "add_succ_right"; ``` paulson@2469 ` 109` paulson@2469 ` 110` ```Addsimps [add_0_right, add_succ_right]; ``` clasohm@0 ` 111` clasohm@0 ` 112` ```(*Commutative law for addition*) ``` paulson@6070 ` 113` ```Goal "[| m:nat; n:nat |] ==> m #+ n = n #+ m"; ``` paulson@6070 ` 114` ```by (induct_tac "n" 1); ``` paulson@6070 ` 115` ```by Auto_tac; ``` paulson@6070 ` 116` ```qed "add_commute"; ``` lcp@435 ` 117` lcp@437 ` 118` ```(*for a/c rewriting*) ``` paulson@6070 ` 119` ```Goal "[| m:nat; n:nat |] ==> m#+(n#+k)=n#+(m#+k)"; ``` paulson@6070 ` 120` ```by (asm_simp_tac (simpset() addsimps [add_assoc RS sym, add_commute]) 1); ``` paulson@6070 ` 121` ```qed "add_left_commute"; ``` lcp@435 ` 122` lcp@435 ` 123` ```(*Addition is an AC-operator*) ``` lcp@435 ` 124` ```val add_ac = [add_assoc, add_commute, add_left_commute]; ``` clasohm@0 ` 125` clasohm@0 ` 126` ```(*Cancellation law on the left*) ``` paulson@6070 ` 127` ```Goal "[| k #+ m = k #+ n; k:nat |] ==> m=n"; ``` paulson@6070 ` 128` ```by (etac rev_mp 1); ``` paulson@6070 ` 129` ```by (induct_tac "k" 1); ``` paulson@6070 ` 130` ```by Auto_tac; ``` clasohm@760 ` 131` ```qed "add_left_cancel"; ``` clasohm@0 ` 132` clasohm@0 ` 133` ```(*** Multiplication ***) ``` clasohm@0 ` 134` clasohm@0 ` 135` ```(*right annihilation in product*) ``` paulson@6070 ` 136` ```Goal "m:nat ==> m #* 0 = 0"; ``` paulson@6070 ` 137` ```by (induct_tac "m" 1); ``` paulson@6070 ` 138` ```by Auto_tac; ``` paulson@6070 ` 139` ```qed "mult_0_right"; ``` clasohm@0 ` 140` clasohm@0 ` 141` ```(*right successor law for multiplication*) ``` paulson@6070 ` 142` ```Goal "[| m:nat; n:nat |] ==> m #* succ(n) = m #+ (m #* n)"; ``` paulson@6070 ` 143` ```by (induct_tac "m" 1); ``` paulson@6070 ` 144` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac))); ``` paulson@6070 ` 145` ```qed "mult_succ_right"; ``` paulson@2469 ` 146` paulson@2469 ` 147` ```Addsimps [mult_0_right, mult_succ_right]; ``` clasohm@0 ` 148` paulson@5137 ` 149` ```Goal "n:nat ==> 1 #* n = n"; ``` paulson@2469 ` 150` ```by (Asm_simp_tac 1); ``` paulson@1793 ` 151` ```qed "mult_1"; ``` paulson@1793 ` 152` paulson@5137 ` 153` ```Goal "n:nat ==> n #* 1 = n"; ``` paulson@2469 ` 154` ```by (Asm_simp_tac 1); ``` paulson@1793 ` 155` ```qed "mult_1_right"; ``` paulson@1793 ` 156` paulson@6070 ` 157` ```Addsimps [mult_1, mult_1_right]; ``` paulson@6070 ` 158` clasohm@0 ` 159` ```(*Commutative law for multiplication*) ``` paulson@6070 ` 160` ```Goal "[| m:nat; n:nat |] ==> m #* n = n #* m"; ``` paulson@6070 ` 161` ```by (induct_tac "m" 1); ``` paulson@6070 ` 162` ```by Auto_tac; ``` paulson@6070 ` 163` ```qed "mult_commute"; ``` clasohm@0 ` 164` clasohm@0 ` 165` ```(*addition distributes over multiplication*) ``` paulson@6070 ` 166` ```Goal "[| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"; ``` paulson@6070 ` 167` ```by (induct_tac "m" 1); ``` paulson@6070 ` 168` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym]))); ``` paulson@6070 ` 169` ```qed "add_mult_distrib"; ``` clasohm@0 ` 170` clasohm@0 ` 171` ```(*Distributive law on the left; requires an extra typing premise*) ``` paulson@6070 ` 172` ```Goal "[| m:nat; n:nat; k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"; ``` paulson@6070 ` 173` ```by (induct_tac "m" 1); ``` paulson@6070 ` 174` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac))); ``` paulson@6070 ` 175` ```qed "add_mult_distrib_left"; ``` clasohm@0 ` 176` clasohm@0 ` 177` ```(*Associative law for multiplication*) ``` paulson@6070 ` 178` ```Goal "[| m:nat; n:nat; k:nat |] ==> (m #* n) #* k = m #* (n #* k)"; ``` paulson@6070 ` 179` ```by (induct_tac "m" 1); ``` paulson@6070 ` 180` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))); ``` paulson@6070 ` 181` ```qed "mult_assoc"; ``` clasohm@0 ` 182` lcp@437 ` 183` ```(*for a/c rewriting*) ``` paulson@6070 ` 184` ```Goal "[| m:nat; n:nat; k:nat |] ==> m #* (n #* k) = n #* (m #* k)"; ``` paulson@6070 ` 185` ```by (rtac (mult_commute RS trans) 1); ``` paulson@6070 ` 186` ```by (rtac (mult_assoc RS trans) 3); ``` paulson@6070 ` 187` ```by (rtac (mult_commute RS subst_context) 6); ``` paulson@6070 ` 188` ```by (REPEAT (ares_tac [mult_type] 1)); ``` paulson@6070 ` 189` ```qed "mult_left_commute"; ``` lcp@437 ` 190` lcp@437 ` 191` ```val mult_ac = [mult_assoc,mult_commute,mult_left_commute]; ``` lcp@437 ` 192` clasohm@0 ` 193` clasohm@0 ` 194` ```(*** Difference ***) ``` clasohm@0 ` 195` paulson@6070 ` 196` ```Goal "m:nat ==> m #- m = 0"; ``` paulson@6070 ` 197` ```by (induct_tac "m" 1); ``` paulson@6070 ` 198` ```by Auto_tac; ``` paulson@6070 ` 199` ```qed "diff_self_eq_0"; ``` clasohm@0 ` 200` lcp@25 ` 201` ```(*Addition is the inverse of subtraction*) ``` paulson@5137 ` 202` ```Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m"; ``` lcp@25 ` 203` ```by (forward_tac [lt_nat_in_nat] 1); ``` lcp@127 ` 204` ```by (etac nat_succI 1); ``` lcp@25 ` 205` ```by (etac rev_mp 1); ``` clasohm@0 ` 206` ```by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); ``` paulson@2469 ` 207` ```by (ALLGOALS Asm_simp_tac); ``` clasohm@760 ` 208` ```qed "add_diff_inverse"; ``` clasohm@0 ` 209` paulson@5504 ` 210` ```Goal "[| n le m; m:nat |] ==> (m#-n) #+ n = m"; ``` paulson@5504 ` 211` ```by (forward_tac [lt_nat_in_nat] 1); ``` paulson@5504 ` 212` ```by (etac nat_succI 1); ``` paulson@5504 ` 213` ```by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1); ``` paulson@5504 ` 214` ```qed "add_diff_inverse2"; ``` paulson@5504 ` 215` paulson@1609 ` 216` ```(*Proof is IDENTICAL to that above*) ``` paulson@5137 ` 217` ```Goal "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)"; ``` paulson@1609 ` 218` ```by (forward_tac [lt_nat_in_nat] 1); ``` paulson@1609 ` 219` ```by (etac nat_succI 1); ``` paulson@1609 ` 220` ```by (etac rev_mp 1); ``` paulson@1609 ` 221` ```by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); ``` paulson@2469 ` 222` ```by (ALLGOALS Asm_simp_tac); ``` paulson@1609 ` 223` ```qed "diff_succ"; ``` paulson@1609 ` 224` paulson@5341 ` 225` ```Goal "[| m: nat; n: nat |] ==> 0 < n #- m <-> m (n#+m) #- n = m"; ``` paulson@6070 ` 235` ```by (induct_tac "n" 1); ``` paulson@6070 ` 236` ```by Auto_tac; ``` clasohm@760 ` 237` ```qed "diff_add_inverse"; ``` clasohm@0 ` 238` paulson@5137 ` 239` ```Goal "[| m:nat; n:nat |] ==> (m#+n) #- n = m"; ``` lcp@437 ` 240` ```by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1); ``` lcp@437 ` 241` ```by (REPEAT (ares_tac [diff_add_inverse] 1)); ``` clasohm@760 ` 242` ```qed "diff_add_inverse2"; ``` lcp@437 ` 243` paulson@5137 ` 244` ```Goal "[| k:nat; m: nat; n: nat |] ==> (k#+m) #- (k#+n) = m #- n"; ``` paulson@6070 ` 245` ```by (induct_tac "k" 1); ``` paulson@2469 ` 246` ```by (ALLGOALS Asm_simp_tac); ``` paulson@1708 ` 247` ```qed "diff_cancel"; ``` paulson@1708 ` 248` paulson@5137 ` 249` ```Goal "[| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n"; ``` paulson@1708 ` 250` ```val add_commute_k = read_instantiate [("n","k")] add_commute; ``` wenzelm@4091 ` 251` ```by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1); ``` paulson@1708 ` 252` ```qed "diff_cancel2"; ``` paulson@1708 ` 253` paulson@6070 ` 254` ```Goal "[| m:nat; n:nat |] ==> n #- (n#+m) = 0"; ``` paulson@6070 ` 255` ```by (induct_tac "n" 1); ``` paulson@6070 ` 256` ```by Auto_tac; ``` clasohm@760 ` 257` ```qed "diff_add_0"; ``` clasohm@0 ` 258` paulson@1708 ` 259` ```(** Difference distributes over multiplication **) ``` paulson@1708 ` 260` paulson@5137 ` 261` ```Goal "[| m:nat; n: nat; k:nat |] ==> (m #- n) #* k = (m #* k) #- (n #* k)"; ``` paulson@1708 ` 262` ```by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); ``` wenzelm@4091 ` 263` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel]))); ``` paulson@1708 ` 264` ```qed "diff_mult_distrib" ; ``` paulson@1708 ` 265` paulson@5137 ` 266` ```Goal "[| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)"; ``` paulson@1708 ` 267` ```val mult_commute_k = read_instantiate [("m","k")] mult_commute; ``` wenzelm@4091 ` 268` ```by (asm_simp_tac (simpset() addsimps ``` paulson@1793 ` 269` ``` [mult_commute_k, diff_mult_distrib]) 1); ``` paulson@1708 ` 270` ```qed "diff_mult_distrib2" ; ``` paulson@1708 ` 271` clasohm@0 ` 272` ```(*** Remainder ***) ``` clasohm@0 ` 273` paulson@5137 ` 274` ```Goal "[| 0 m #- n < m"; ``` lcp@25 ` 275` ```by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); ``` clasohm@0 ` 276` ```by (etac rev_mp 1); ``` clasohm@0 ` 277` ```by (etac rev_mp 1); ``` clasohm@0 ` 278` ```by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); ``` paulson@6070 ` 279` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self]))); ``` clasohm@760 ` 280` ```qed "div_termination"; ``` clasohm@0 ` 281` clasohm@1461 ` 282` ```val div_rls = (*for mod and div*) ``` lcp@25 ` 283` ``` nat_typechecks @ ``` lcp@25 ` 284` ``` [Ord_transrec_type, apply_type, div_termination RS ltD, if_type, ``` lcp@435 ` 285` ``` nat_into_Ord, not_lt_iff_le RS iffD1]; ``` lcp@25 ` 286` paulson@6070 ` 287` ```val div_ss = simpset() addsimps [nat_into_Ord, div_termination RS ltD, ``` paulson@6070 ` 288` ``` not_lt_iff_le RS iffD2]; ``` clasohm@0 ` 289` clasohm@0 ` 290` ```(*Type checking depends upon termination!*) ``` paulson@5137 ` 291` ```Goalw [mod_def] "[| 0 m mod n : nat"; ``` lcp@25 ` 292` ```by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); ``` clasohm@760 ` 293` ```qed "mod_type"; ``` paulson@6153 ` 294` ```AddTCs [mod_type]; ``` clasohm@0 ` 295` paulson@5137 ` 296` ```Goal "[| 0 m mod n = m"; ``` clasohm@0 ` 297` ```by (rtac (mod_def RS def_transrec RS trans) 1); ``` lcp@25 ` 298` ```by (asm_simp_tac div_ss 1); ``` clasohm@760 ` 299` ```qed "mod_less"; ``` clasohm@0 ` 300` paulson@5137 ` 301` ```Goal "[| 0 m mod n = (m#-n) mod n"; ``` lcp@25 ` 302` ```by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); ``` clasohm@0 ` 303` ```by (rtac (mod_def RS def_transrec RS trans) 1); ``` lcp@25 ` 304` ```by (asm_simp_tac div_ss 1); ``` clasohm@760 ` 305` ```qed "mod_geq"; ``` clasohm@0 ` 306` paulson@2469 ` 307` ```Addsimps [mod_type, mod_less, mod_geq]; ``` paulson@2469 ` 308` clasohm@0 ` 309` ```(*** Quotient ***) ``` clasohm@0 ` 310` clasohm@0 ` 311` ```(*Type checking depends upon termination!*) ``` wenzelm@5067 ` 312` ```Goalw [div_def] ``` paulson@5147 ` 313` ``` "[| 0 m div n : nat"; ``` lcp@25 ` 314` ```by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); ``` clasohm@760 ` 315` ```qed "div_type"; ``` paulson@6153 ` 316` ```AddTCs [div_type]; ``` clasohm@0 ` 317` paulson@5137 ` 318` ```Goal "[| 0 m div n = 0"; ``` clasohm@0 ` 319` ```by (rtac (div_def RS def_transrec RS trans) 1); ``` lcp@25 ` 320` ```by (asm_simp_tac div_ss 1); ``` clasohm@760 ` 321` ```qed "div_less"; ``` clasohm@0 ` 322` paulson@5137 ` 323` ```Goal "[| 0 m div n = succ((m#-n) div n)"; ``` lcp@25 ` 324` ```by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); ``` clasohm@0 ` 325` ```by (rtac (div_def RS def_transrec RS trans) 1); ``` lcp@25 ` 326` ```by (asm_simp_tac div_ss 1); ``` clasohm@760 ` 327` ```qed "div_geq"; ``` clasohm@0 ` 328` paulson@2469 ` 329` ```Addsimps [div_type, div_less, div_geq]; ``` paulson@2469 ` 330` paulson@1609 ` 331` ```(*A key result*) ``` paulson@5137 ` 332` ```Goal "[| 0 (m div n)#*n #+ m mod n = m"; ``` lcp@25 ` 333` ```by (etac complete_induct 1); ``` lcp@437 ` 334` ```by (excluded_middle_tac "x succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))"; ``` paulson@1609 ` 348` ```by (etac complete_induct 1); ``` paulson@1609 ` 349` ```by (excluded_middle_tac "succ(x) m mod n < n"; ``` paulson@1609 ` 364` ```by (etac complete_induct 1); ``` paulson@1609 ` 365` ```by (excluded_middle_tac "x k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"; ``` paulson@1609 ` 376` ```by (subgoal_tac "k mod 2: 2" 1); ``` wenzelm@4091 ` 377` ```by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2); ``` paulson@1623 ` 378` ```by (dtac ltD 1); ``` paulson@5137 ` 379` ```by Auto_tac; ``` paulson@1609 ` 380` ```qed "mod2_cases"; ``` paulson@1609 ` 381` paulson@5137 ` 382` ```Goal "m:nat ==> succ(succ(m)) mod 2 = m mod 2"; ``` paulson@1609 ` 383` ```by (subgoal_tac "m mod 2: 2" 1); ``` wenzelm@4091 ` 384` ```by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2); ``` wenzelm@4091 ` 385` ```by (asm_simp_tac (simpset() addsimps [mod_succ] setloop Step_tac) 1); ``` paulson@1609 ` 386` ```qed "mod2_succ_succ"; ``` paulson@1609 ` 387` paulson@5137 ` 388` ```Goal "m:nat ==> (m#+m) mod 2 = 0"; ``` paulson@6070 ` 389` ```by (induct_tac "m" 1); ``` wenzelm@4091 ` 390` ```by (simp_tac (simpset() addsimps [mod_less]) 1); ``` wenzelm@4091 ` 391` ```by (asm_simp_tac (simpset() addsimps [mod2_succ_succ, add_succ_right]) 1); ``` paulson@1609 ` 392` ```qed "mod2_add_self"; ``` paulson@1609 ` 393` clasohm@0 ` 394` lcp@25 ` 395` ```(**** Additional theorems about "le" ****) ``` clasohm@0 ` 396` paulson@5137 ` 397` ```Goal "[| m:nat; n:nat |] ==> m le m #+ n"; ``` paulson@6070 ` 398` ```by (induct_tac "m" 1); ``` paulson@2469 ` 399` ```by (ALLGOALS Asm_simp_tac); ``` clasohm@760 ` 400` ```qed "add_le_self"; ``` lcp@14 ` 401` paulson@5137 ` 402` ```Goal "[| m:nat; n:nat |] ==> m le n #+ m"; ``` paulson@2033 ` 403` ```by (stac add_commute 1); ``` lcp@25 ` 404` ```by (REPEAT (ares_tac [add_le_self] 1)); ``` clasohm@760 ` 405` ```qed "add_le_self2"; ``` lcp@14 ` 406` paulson@1708 ` 407` ```(*** Monotonicity of Addition ***) ``` lcp@14 ` 408` paulson@1708 ` 409` ```(*strict, in 1st argument; proof is by rule induction on 'less than'*) ``` paulson@5137 ` 410` ```Goal "[| i i#+k < j#+k"; ``` lcp@25 ` 411` ```by (forward_tac [lt_nat_in_nat] 1); ``` lcp@127 ` 412` ```by (assume_tac 1); ``` lcp@25 ` 413` ```by (etac succ_lt_induct 1); ``` wenzelm@4091 ` 414` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI]))); ``` clasohm@760 ` 415` ```qed "add_lt_mono1"; ``` lcp@14 ` 416` lcp@14 ` 417` ```(*strict, in both arguments*) ``` paulson@5137 ` 418` ```Goal "[| i i#+k < j#+l"; ``` lcp@25 ` 419` ```by (rtac (add_lt_mono1 RS lt_trans) 1); ``` lcp@25 ` 420` ```by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); ``` paulson@2033 ` 421` ```by (EVERY [stac add_commute 1, ``` paulson@2033 ` 422` ``` stac add_commute 3, ``` clasohm@1461 ` 423` ``` rtac add_lt_mono1 5]); ``` lcp@25 ` 424` ```by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); ``` clasohm@760 ` 425` ```qed "add_lt_mono"; ``` lcp@14 ` 426` lcp@25 ` 427` ```(*A [clumsy] way of lifting < monotonicity to le monotonicity *) ``` paulson@5325 ` 428` ```val lt_mono::ford::prems = Goal ``` clasohm@1461 ` 429` ``` "[| !!i j. [| i f(i) < f(j); \ ``` clasohm@1461 ` 430` ```\ !!i. i:k ==> Ord(f(i)); \ ``` clasohm@1461 ` 431` ```\ i le j; j:k \ ``` lcp@25 ` 432` ```\ |] ==> f(i) le f(j)"; ``` lcp@14 ` 433` ```by (cut_facts_tac prems 1); ``` paulson@3016 ` 434` ```by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1); ``` clasohm@760 ` 435` ```qed "Ord_lt_mono_imp_le_mono"; ``` lcp@14 ` 436` lcp@25 ` 437` ```(*le monotonicity, 1st argument*) ``` paulson@5137 ` 438` ```Goal "[| i le j; j:nat; k:nat |] ==> i#+k le j#+k"; ``` wenzelm@3840 ` 439` ```by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1); ``` lcp@435 ` 440` ```by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1)); ``` clasohm@760 ` 441` ```qed "add_le_mono1"; ``` lcp@14 ` 442` lcp@25 ` 443` ```(* le monotonicity, BOTH arguments*) ``` paulson@5137 ` 444` ```Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l"; ``` lcp@25 ` 445` ```by (rtac (add_le_mono1 RS le_trans) 1); ``` lcp@25 ` 446` ```by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); ``` paulson@2033 ` 447` ```by (EVERY [stac add_commute 1, ``` paulson@2033 ` 448` ``` stac add_commute 3, ``` clasohm@1461 ` 449` ``` rtac add_le_mono1 5]); ``` lcp@25 ` 450` ```by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); ``` clasohm@760 ` 451` ```qed "add_le_mono"; ``` paulson@1609 ` 452` paulson@1708 ` 453` ```(*** Monotonicity of Multiplication ***) ``` paulson@1708 ` 454` paulson@5137 ` 455` ```Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k"; ``` paulson@1708 ` 456` ```by (forward_tac [lt_nat_in_nat] 1); ``` paulson@6070 ` 457` ```by (induct_tac "k" 2); ``` wenzelm@4091 ` 458` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); ``` paulson@1708 ` 459` ```qed "mult_le_mono1"; ``` paulson@1708 ` 460` paulson@1708 ` 461` ```(* le monotonicity, BOTH arguments*) ``` paulson@5137 ` 462` ```Goal "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l"; ``` paulson@1708 ` 463` ```by (rtac (mult_le_mono1 RS le_trans) 1); ``` paulson@1708 ` 464` ```by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); ``` paulson@2033 ` 465` ```by (EVERY [stac mult_commute 1, ``` paulson@2033 ` 466` ``` stac mult_commute 3, ``` paulson@1708 ` 467` ``` rtac mult_le_mono1 5]); ``` paulson@1708 ` 468` ```by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); ``` paulson@1708 ` 469` ```qed "mult_le_mono"; ``` paulson@1708 ` 470` paulson@1708 ` 471` ```(*strict, in 1st argument; proof is by induction on k>0*) ``` paulson@5137 ` 472` ```Goal "[| i k#*i < k#*j"; ``` paulson@1793 ` 473` ```by (etac zero_lt_natE 1); ``` paulson@1708 ` 474` ```by (forward_tac [lt_nat_in_nat] 2); ``` paulson@2469 ` 475` ```by (ALLGOALS Asm_simp_tac); ``` paulson@6070 ` 476` ```by (induct_tac "x" 1); ``` wenzelm@4091 ` 477` ```by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono]))); ``` paulson@1708 ` 478` ```qed "mult_lt_mono2"; ``` paulson@1708 ` 479` paulson@5137 ` 480` ```Goal "[| i i#*c < j#*c"; ``` paulson@4839 ` 481` ```by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1); ``` paulson@4839 ` 482` ```qed "mult_lt_mono1"; ``` paulson@4839 ` 483` paulson@5137 ` 484` ```Goal "[| m: nat; n: nat |] ==> 0 < m#*n <-> 0 m#*n = 1 <-> m=1 & n=1"; ``` wenzelm@4091 ` 489` ```by (best_tac (claset() addEs [natE] addss (simpset())) 1); ``` paulson@1793 ` 490` ```qed "mult_eq_1_iff"; ``` paulson@1793 ` 491` paulson@1708 ` 492` ```(*Cancellation law for division*) ``` paulson@5137 ` 493` ```Goal "[| 0 (k#*m) div (k#*n) = m div n"; ``` paulson@1708 ` 494` ```by (eres_inst_tac [("i","m")] complete_induct 1); ``` paulson@1708 ` 495` ```by (excluded_middle_tac "x \ ``` paulson@1708 ` 506` ```\ (k#*m) mod (k#*n) = k #* (m mod n)"; ``` paulson@1708 ` 507` ```by (eres_inst_tac [("i","m")] complete_induct 1); ``` paulson@1708 ` 508` ```by (excluded_middle_tac "x n=1 | m=0"; ``` paulson@1793 ` 520` ```by (rtac disjCI 1); ``` paulson@1793 ` 521` ```by (dtac sym 1); ``` paulson@1793 ` 522` ```by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I])); ``` paulson@6070 ` 523` ```by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 2); ``` paulson@6070 ` 524` ```by Auto_tac; ``` paulson@1793 ` 525` ```qed "mult_eq_self_implies_10"; ``` paulson@1708 ` 526` paulson@2469 ` 527` ```(*Thanks to Sten Agerholm*) ``` paulson@5504 ` 528` ```Goal "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k"; ``` paulson@2493 ` 529` ```by (etac rev_mp 1); ``` paulson@6070 ` 530` ```by (induct_tac "m" 1); ``` paulson@2469 ` 531` ```by (Asm_simp_tac 1); ``` paulson@3736 ` 532` ```by Safe_tac; ``` wenzelm@4091 ` 533` ```by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt,nat_into_Ord]) 1); ``` paulson@2469 ` 534` ```qed "add_le_elim1"; ``` paulson@2469 ` 535` paulson@5504 ` 536` ```Goal "[| m EX k: nat. n = succ(m#+k)"; ``` paulson@5504 ` 537` ```by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1); ``` paulson@6163 ` 538` ```by (etac rev_mp 1); ``` paulson@6070 ` 539` ```by (induct_tac "n" 1); ``` paulson@5504 ` 540` ```by (ALLGOALS (simp_tac (simpset() addsimps [le_iff]))); ``` paulson@5504 ` 541` ```by (blast_tac (claset() addSEs [leE] ``` paulson@5504 ` 542` ``` addSIs [add_0_right RS sym, add_succ_right RS sym]) 1); ``` paulson@5504 ` 543` ```qed_spec_mp "less_imp_Suc_add"; ```