src/ZF/Arith.thy
 author wenzelm Sat Nov 04 19:17:19 2017 +0100 (21 months ago) changeset 67006 b1278ed3cd46 parent 61798 27f3c10b0b50 child 69587 53982d5ec0bb permissions -rw-r--r--
prefer main entry points of HOL;
 paulson@9654 ` 1` ```(* Title: ZF/Arith.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 3` ``` Copyright 1992 University of Cambridge ``` clasohm@0 ` 4` ```*) ``` clasohm@0 ` 5` paulson@13163 ` 6` ```(*"Difference" is subtraction of natural numbers. ``` paulson@13163 ` 7` ``` There are no negative numbers; we have ``` paulson@13163 ` 8` ``` m #- n = 0 iff m<=n and m #- n = succ(k) iff m>n. ``` paulson@46820 ` 9` ``` Also, rec(m, 0, %z w.z) is pred(m). ``` paulson@13163 ` 10` ```*) ``` paulson@13163 ` 11` wenzelm@60770 ` 12` ```section\Arithmetic Operators and Their Definitions\ ``` paulson@13328 ` 13` haftmann@16417 ` 14` ```theory Arith imports Univ begin ``` paulson@6070 ` 15` wenzelm@60770 ` 16` ```text\Proofs about elementary arithmetic: addition, multiplication, etc.\ ``` paulson@13328 ` 17` wenzelm@24893 ` 18` ```definition ``` wenzelm@24893 ` 19` ``` pred :: "i=>i" (*inverse of succ*) where ``` paulson@13361 ` 20` ``` "pred(y) == nat_case(0, %x. x, y)" ``` paulson@6070 ` 21` wenzelm@24893 ` 22` ```definition ``` wenzelm@24893 ` 23` ``` natify :: "i=>i" (*coerces non-nats to nats*) where ``` paulson@9491 ` 24` ``` "natify == Vrecursor(%f a. if a = succ(pred(a)) then succ(f`pred(a)) ``` paulson@9491 ` 25` ``` else 0)" ``` paulson@6070 ` 26` clasohm@0 ` 27` ```consts ``` paulson@13163 ` 28` ``` raw_add :: "[i,i]=>i" ``` paulson@13163 ` 29` ``` raw_diff :: "[i,i]=>i" ``` paulson@13163 ` 30` ``` raw_mult :: "[i,i]=>i" ``` paulson@9492 ` 31` paulson@9492 ` 32` ```primrec ``` paulson@9492 ` 33` ``` "raw_add (0, n) = n" ``` paulson@9492 ` 34` ``` "raw_add (succ(m), n) = succ(raw_add(m, n))" ``` clasohm@0 ` 35` paulson@6070 ` 36` ```primrec ``` paulson@13163 ` 37` ``` raw_diff_0: "raw_diff(m, 0) = m" ``` paulson@13163 ` 38` ``` raw_diff_succ: "raw_diff(m, succ(n)) = ``` paulson@13163 ` 39` ``` nat_case(0, %x. x, raw_diff(m, n))" ``` paulson@9491 ` 40` paulson@9491 ` 41` ```primrec ``` paulson@9492 ` 42` ``` "raw_mult(0, n) = 0" ``` paulson@9492 ` 43` ``` "raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))" ``` paulson@13163 ` 44` wenzelm@24893 ` 45` ```definition ``` wenzelm@24893 ` 46` ``` add :: "[i,i]=>i" (infixl "#+" 65) where ``` paulson@9492 ` 47` ``` "m #+ n == raw_add (natify(m), natify(n))" ``` paulson@9491 ` 48` wenzelm@24893 ` 49` ```definition ``` wenzelm@24893 ` 50` ``` diff :: "[i,i]=>i" (infixl "#-" 65) where ``` paulson@9492 ` 51` ``` "m #- n == raw_diff (natify(m), natify(n))" ``` clasohm@0 ` 52` wenzelm@24893 ` 53` ```definition ``` wenzelm@24893 ` 54` ``` mult :: "[i,i]=>i" (infixl "#*" 70) where ``` paulson@9492 ` 55` ``` "m #* n == raw_mult (natify(m), natify(n))" ``` paulson@9492 ` 56` wenzelm@24893 ` 57` ```definition ``` wenzelm@24893 ` 58` ``` raw_div :: "[i,i]=>i" where ``` paulson@13163 ` 59` ``` "raw_div (m, n) == ``` paulson@9492 ` 60` ``` transrec(m, %j f. if ji" where ``` paulson@13163 ` 64` ``` "raw_mod (m, n) == ``` paulson@9492 ` 65` ``` transrec(m, %j f. if ji" (infixl "div" 70) where ``` paulson@9492 ` 69` ``` "m div n == raw_div (natify(m), natify(n))" ``` paulson@9491 ` 70` wenzelm@24893 ` 71` ```definition ``` wenzelm@24893 ` 72` ``` mod :: "[i,i]=>i" (infixl "mod" 70) where ``` paulson@9492 ` 73` ``` "m mod n == raw_mod (natify(m), natify(n))" ``` paulson@9491 ` 74` paulson@13163 ` 75` ```declare rec_type [simp] ``` paulson@13163 ` 76` ``` nat_0_le [simp] ``` paulson@13163 ` 77` paulson@13163 ` 78` paulson@14060 ` 79` ```lemma zero_lt_lemma: "[| 0 nat |] ==> \j\nat. k = succ(j)" ``` paulson@13163 ` 80` ```apply (erule rev_mp) ``` paulson@13163 ` 81` ```apply (induct_tac "k", auto) ``` paulson@13163 ` 82` ```done ``` paulson@13163 ` 83` paulson@46820 ` 84` ```(* @{term"[| 0 < k; k \ nat; !!j. [| j \ nat; k = succ(j) |] ==> Q |] ==> Q"} *) ``` wenzelm@45608 ` 85` ```lemmas zero_lt_natE = zero_lt_lemma [THEN bexE] ``` paulson@13163 ` 86` paulson@13163 ` 87` wenzelm@61798 ` 88` ```subsection\\natify\, the Coercion to @{term nat}\ ``` paulson@13163 ` 89` paulson@13163 ` 90` ```lemma pred_succ_eq [simp]: "pred(succ(y)) = y" ``` paulson@13163 ` 91` ```by (unfold pred_def, auto) ``` paulson@13163 ` 92` paulson@13163 ` 93` ```lemma natify_succ: "natify(succ(x)) = succ(natify(x))" ``` paulson@13163 ` 94` ```by (rule natify_def [THEN def_Vrecursor, THEN trans], auto) ``` paulson@13163 ` 95` paulson@13163 ` 96` ```lemma natify_0 [simp]: "natify(0) = 0" ``` paulson@13163 ` 97` ```by (rule natify_def [THEN def_Vrecursor, THEN trans], auto) ``` paulson@13163 ` 98` paulson@46820 ` 99` ```lemma natify_non_succ: "\z. x \ succ(z) ==> natify(x) = 0" ``` paulson@13163 ` 100` ```by (rule natify_def [THEN def_Vrecursor, THEN trans], auto) ``` paulson@13163 ` 101` paulson@14060 ` 102` ```lemma natify_in_nat [iff,TC]: "natify(x) \ nat" ``` paulson@13163 ` 103` ```apply (rule_tac a=x in eps_induct) ``` paulson@14060 ` 104` ```apply (case_tac "\z. x = succ(z)") ``` paulson@13163 ` 105` ```apply (auto simp add: natify_succ natify_non_succ) ``` paulson@13163 ` 106` ```done ``` paulson@13163 ` 107` paulson@14060 ` 108` ```lemma natify_ident [simp]: "n \ nat ==> natify(n) = n" ``` paulson@13163 ` 109` ```apply (induct_tac "n") ``` paulson@13163 ` 110` ```apply (auto simp add: natify_succ) ``` paulson@13163 ` 111` ```done ``` paulson@13163 ` 112` paulson@14060 ` 113` ```lemma natify_eqE: "[|natify(x) = y; x \ nat|] ==> x=y" ``` paulson@13163 ` 114` ```by auto ``` paulson@13163 ` 115` paulson@13163 ` 116` paulson@13163 ` 117` ```(*** Collapsing rules: to remove natify from arithmetic expressions ***) ``` paulson@13163 ` 118` paulson@13163 ` 119` ```lemma natify_idem [simp]: "natify(natify(x)) = natify(x)" ``` paulson@13163 ` 120` ```by simp ``` paulson@13163 ` 121` paulson@13163 ` 122` ```(** Addition **) ``` paulson@13163 ` 123` paulson@13163 ` 124` ```lemma add_natify1 [simp]: "natify(m) #+ n = m #+ n" ``` paulson@13163 ` 125` ```by (simp add: add_def) ``` paulson@13163 ` 126` paulson@13163 ` 127` ```lemma add_natify2 [simp]: "m #+ natify(n) = m #+ n" ``` paulson@13163 ` 128` ```by (simp add: add_def) ``` paulson@13163 ` 129` paulson@13163 ` 130` ```(** Multiplication **) ``` paulson@13163 ` 131` paulson@13163 ` 132` ```lemma mult_natify1 [simp]: "natify(m) #* n = m #* n" ``` paulson@13163 ` 133` ```by (simp add: mult_def) ``` paulson@13163 ` 134` paulson@13163 ` 135` ```lemma mult_natify2 [simp]: "m #* natify(n) = m #* n" ``` paulson@13163 ` 136` ```by (simp add: mult_def) ``` paulson@13163 ` 137` paulson@13163 ` 138` ```(** Difference **) ``` paulson@13163 ` 139` paulson@13163 ` 140` ```lemma diff_natify1 [simp]: "natify(m) #- n = m #- n" ``` paulson@13163 ` 141` ```by (simp add: diff_def) ``` paulson@13163 ` 142` paulson@13163 ` 143` ```lemma diff_natify2 [simp]: "m #- natify(n) = m #- n" ``` paulson@13163 ` 144` ```by (simp add: diff_def) ``` paulson@13163 ` 145` paulson@13163 ` 146` ```(** Remainder **) ``` paulson@13163 ` 147` paulson@13163 ` 148` ```lemma mod_natify1 [simp]: "natify(m) mod n = m mod n" ``` paulson@13163 ` 149` ```by (simp add: mod_def) ``` paulson@13163 ` 150` paulson@13163 ` 151` ```lemma mod_natify2 [simp]: "m mod natify(n) = m mod n" ``` paulson@13163 ` 152` ```by (simp add: mod_def) ``` paulson@13163 ` 153` paulson@13163 ` 154` paulson@13163 ` 155` ```(** Quotient **) ``` paulson@13163 ` 156` paulson@13163 ` 157` ```lemma div_natify1 [simp]: "natify(m) div n = m div n" ``` paulson@13163 ` 158` ```by (simp add: div_def) ``` paulson@13163 ` 159` paulson@13163 ` 160` ```lemma div_natify2 [simp]: "m div natify(n) = m div n" ``` paulson@13163 ` 161` ```by (simp add: div_def) ``` paulson@13163 ` 162` paulson@13163 ` 163` wenzelm@60770 ` 164` ```subsection\Typing rules\ ``` paulson@13163 ` 165` paulson@13163 ` 166` ```(** Addition **) ``` paulson@13163 ` 167` paulson@14060 ` 168` ```lemma raw_add_type: "[| m\nat; n\nat |] ==> raw_add (m, n) \ nat" ``` paulson@13163 ` 169` ```by (induct_tac "m", auto) ``` paulson@13163 ` 170` paulson@14060 ` 171` ```lemma add_type [iff,TC]: "m #+ n \ nat" ``` paulson@13163 ` 172` ```by (simp add: add_def raw_add_type) ``` paulson@13163 ` 173` paulson@13163 ` 174` ```(** Multiplication **) ``` paulson@13163 ` 175` paulson@14060 ` 176` ```lemma raw_mult_type: "[| m\nat; n\nat |] ==> raw_mult (m, n) \ nat" ``` paulson@13163 ` 177` ```apply (induct_tac "m") ``` paulson@13163 ` 178` ```apply (simp_all add: raw_add_type) ``` paulson@13163 ` 179` ```done ``` paulson@13163 ` 180` paulson@14060 ` 181` ```lemma mult_type [iff,TC]: "m #* n \ nat" ``` paulson@13163 ` 182` ```by (simp add: mult_def raw_mult_type) ``` paulson@13163 ` 183` paulson@13163 ` 184` paulson@13163 ` 185` ```(** Difference **) ``` paulson@13163 ` 186` paulson@14060 ` 187` ```lemma raw_diff_type: "[| m\nat; n\nat |] ==> raw_diff (m, n) \ nat" ``` paulson@13173 ` 188` ```by (induct_tac "n", auto) ``` paulson@13163 ` 189` paulson@14060 ` 190` ```lemma diff_type [iff,TC]: "m #- n \ nat" ``` paulson@13163 ` 191` ```by (simp add: diff_def raw_diff_type) ``` paulson@13163 ` 192` paulson@13163 ` 193` ```lemma diff_0_eq_0 [simp]: "0 #- n = 0" ``` paulson@13163 ` 194` ```apply (unfold diff_def) ``` paulson@13163 ` 195` ```apply (rule natify_in_nat [THEN nat_induct], auto) ``` paulson@13163 ` 196` ```done ``` paulson@13163 ` 197` paulson@13163 ` 198` ```(*Must simplify BEFORE the induction: else we get a critical pair*) ``` paulson@13163 ` 199` ```lemma diff_succ_succ [simp]: "succ(m) #- succ(n) = m #- n" ``` paulson@13163 ` 200` ```apply (simp add: natify_succ diff_def) ``` paulson@13784 ` 201` ```apply (rule_tac x1 = n in natify_in_nat [THEN nat_induct], auto) ``` paulson@13163 ` 202` ```done ``` paulson@13163 ` 203` paulson@13163 ` 204` ```(*This defining property is no longer wanted*) ``` paulson@13163 ` 205` ```declare raw_diff_succ [simp del] ``` paulson@13163 ` 206` paulson@13163 ` 207` ```(*Natify has weakened this law, compared with the older approach*) ``` paulson@13163 ` 208` ```lemma diff_0 [simp]: "m #- 0 = natify(m)" ``` paulson@13163 ` 209` ```by (simp add: diff_def) ``` paulson@13163 ` 210` paulson@46820 ` 211` ```lemma diff_le_self: "m\nat ==> (m #- n) \ m" ``` paulson@46820 ` 212` ```apply (subgoal_tac " (m #- natify (n)) \ m") ``` paulson@13784 ` 213` ```apply (rule_tac [2] m = m and n = "natify (n) " in diff_induct) ``` paulson@13163 ` 214` ```apply (erule_tac [6] leE) ``` paulson@13163 ` 215` ```apply (simp_all add: le_iff) ``` paulson@13163 ` 216` ```done ``` paulson@13163 ` 217` paulson@13163 ` 218` wenzelm@60770 ` 219` ```subsection\Addition\ ``` paulson@13163 ` 220` paulson@13163 ` 221` ```(*Natify has weakened this law, compared with the older approach*) ``` paulson@13163 ` 222` ```lemma add_0_natify [simp]: "0 #+ m = natify(m)" ``` paulson@13163 ` 223` ```by (simp add: add_def) ``` paulson@13163 ` 224` paulson@13163 ` 225` ```lemma add_succ [simp]: "succ(m) #+ n = succ(m #+ n)" ``` paulson@13163 ` 226` ```by (simp add: natify_succ add_def) ``` paulson@13163 ` 227` paulson@14060 ` 228` ```lemma add_0: "m \ nat ==> 0 #+ m = m" ``` paulson@13163 ` 229` ```by simp ``` paulson@13163 ` 230` paulson@13163 ` 231` ```(*Associative law for addition*) ``` paulson@13163 ` 232` ```lemma add_assoc: "(m #+ n) #+ k = m #+ (n #+ k)" ``` paulson@13163 ` 233` ```apply (subgoal_tac "(natify(m) #+ natify(n)) #+ natify(k) = ``` paulson@13163 ` 234` ``` natify(m) #+ (natify(n) #+ natify(k))") ``` paulson@13163 ` 235` ```apply (rule_tac [2] n = "natify(m)" in nat_induct) ``` paulson@13163 ` 236` ```apply auto ``` paulson@13163 ` 237` ```done ``` paulson@13163 ` 238` paulson@13163 ` 239` ```(*The following two lemmas are used for add_commute and sometimes ``` paulson@13163 ` 240` ``` elsewhere, since they are safe for rewriting.*) ``` paulson@13163 ` 241` ```lemma add_0_right_natify [simp]: "m #+ 0 = natify(m)" ``` paulson@13163 ` 242` ```apply (subgoal_tac "natify(m) #+ 0 = natify(m)") ``` paulson@13163 ` 243` ```apply (rule_tac [2] n = "natify(m)" in nat_induct) ``` paulson@13163 ` 244` ```apply auto ``` paulson@13163 ` 245` ```done ``` paulson@13163 ` 246` paulson@13163 ` 247` ```lemma add_succ_right [simp]: "m #+ succ(n) = succ(m #+ n)" ``` paulson@13163 ` 248` ```apply (unfold add_def) ``` paulson@13163 ` 249` ```apply (rule_tac n = "natify(m) " in nat_induct) ``` paulson@13163 ` 250` ```apply (auto simp add: natify_succ) ``` paulson@13163 ` 251` ```done ``` paulson@13163 ` 252` paulson@14060 ` 253` ```lemma add_0_right: "m \ nat ==> m #+ 0 = m" ``` paulson@13163 ` 254` ```by auto ``` paulson@13163 ` 255` paulson@13163 ` 256` ```(*Commutative law for addition*) ``` paulson@13163 ` 257` ```lemma add_commute: "m #+ n = n #+ m" ``` paulson@13163 ` 258` ```apply (subgoal_tac "natify(m) #+ natify(n) = natify(n) #+ natify(m) ") ``` paulson@13163 ` 259` ```apply (rule_tac [2] n = "natify(m) " in nat_induct) ``` paulson@13163 ` 260` ```apply auto ``` paulson@13163 ` 261` ```done ``` paulson@13163 ` 262` paulson@13163 ` 263` ```(*for a/c rewriting*) ``` paulson@13163 ` 264` ```lemma add_left_commute: "m#+(n#+k)=n#+(m#+k)" ``` paulson@13163 ` 265` ```apply (rule add_commute [THEN trans]) ``` paulson@13163 ` 266` ```apply (rule add_assoc [THEN trans]) ``` paulson@13163 ` 267` ```apply (rule add_commute [THEN subst_context]) ``` paulson@13163 ` 268` ```done ``` paulson@13163 ` 269` paulson@13163 ` 270` ```(*Addition is an AC-operator*) ``` paulson@13163 ` 271` ```lemmas add_ac = add_assoc add_commute add_left_commute ``` paulson@13163 ` 272` paulson@13163 ` 273` ```(*Cancellation law on the left*) ``` paulson@13163 ` 274` ```lemma raw_add_left_cancel: ``` paulson@14060 ` 275` ``` "[| raw_add(k, m) = raw_add(k, n); k\nat |] ==> m=n" ``` paulson@13163 ` 276` ```apply (erule rev_mp) ``` paulson@13163 ` 277` ```apply (induct_tac "k", auto) ``` paulson@13163 ` 278` ```done ``` paulson@13163 ` 279` paulson@13163 ` 280` ```lemma add_left_cancel_natify: "k #+ m = k #+ n ==> natify(m) = natify(n)" ``` paulson@13163 ` 281` ```apply (unfold add_def) ``` paulson@13163 ` 282` ```apply (drule raw_add_left_cancel, auto) ``` paulson@13163 ` 283` ```done ``` paulson@13163 ` 284` paulson@13163 ` 285` ```lemma add_left_cancel: ``` paulson@14060 ` 286` ``` "[| i = j; i #+ m = j #+ n; m\nat; n\nat |] ==> m = n" ``` paulson@13163 ` 287` ```by (force dest!: add_left_cancel_natify) ``` paulson@13163 ` 288` paulson@13163 ` 289` ```(*Thanks to Sten Agerholm*) ``` paulson@46820 ` 290` ```lemma add_le_elim1_natify: "k#+m \ k#+n ==> natify(m) \ natify(n)" ``` paulson@46820 ` 291` ```apply (rule_tac P = "natify(k) #+m \ natify(k) #+n" in rev_mp) ``` paulson@13163 ` 292` ```apply (rule_tac [2] n = "natify(k) " in nat_induct) ``` paulson@13163 ` 293` ```apply auto ``` paulson@13163 ` 294` ```done ``` paulson@13163 ` 295` paulson@46820 ` 296` ```lemma add_le_elim1: "[| k#+m \ k#+n; m \ nat; n \ nat |] ==> m \ n" ``` paulson@13163 ` 297` ```by (drule add_le_elim1_natify, auto) ``` paulson@13163 ` 298` paulson@13163 ` 299` ```lemma add_lt_elim1_natify: "k#+m < k#+n ==> natify(m) < natify(n)" ``` paulson@13163 ` 300` ```apply (rule_tac P = "natify(k) #+m < natify(k) #+n" in rev_mp) ``` paulson@13163 ` 301` ```apply (rule_tac [2] n = "natify(k) " in nat_induct) ``` paulson@13163 ` 302` ```apply auto ``` paulson@13163 ` 303` ```done ``` paulson@13163 ` 304` paulson@14060 ` 305` ```lemma add_lt_elim1: "[| k#+m < k#+n; m \ nat; n \ nat |] ==> m < n" ``` paulson@13163 ` 306` ```by (drule add_lt_elim1_natify, auto) ``` paulson@13163 ` 307` paulson@46821 ` 308` ```lemma zero_less_add: "[| n \ nat; m \ nat |] ==> 0 < m #+ n \ (0Monotonicity of Addition\ ``` paulson@13163 ` 313` paulson@13163 ` 314` ```(*strict, in 1st argument; proof is by rule induction on 'less than'. ``` paulson@14060 ` 315` ``` Still need j\nat, for consider j = omega. Then we can have inat, but natify(j)=0, so the conclusion fails.*) ``` paulson@14060 ` 317` ```lemma add_lt_mono1: "[| inat |] ==> i#+k < j#+k" ``` paulson@13163 ` 318` ```apply (frule lt_nat_in_nat, assumption) ``` paulson@13163 ` 319` ```apply (erule succ_lt_induct) ``` paulson@13163 ` 320` ```apply (simp_all add: leI) ``` paulson@13163 ` 321` ```done ``` paulson@13163 ` 322` wenzelm@60770 ` 323` ```text\strict, in second argument\ ``` paulson@14060 ` 324` ```lemma add_lt_mono2: "[| inat |] ==> k#+i < k#+j" ``` paulson@14060 ` 325` ```by (simp add: add_commute [of k] add_lt_mono1) ``` paulson@13163 ` 326` wenzelm@61798 ` 327` ```text\A [clumsy] way of lifting < monotonicity to \\\ monotonicity\ ``` paulson@13163 ` 328` ```lemma Ord_lt_mono_imp_le_mono: ``` paulson@13163 ` 329` ``` assumes lt_mono: "!!i j. [| i f(i) < f(j)" ``` paulson@13163 ` 330` ``` and ford: "!!i. i:k ==> Ord(f(i))" ``` paulson@46820 ` 331` ``` and leij: "i \ j" ``` paulson@13163 ` 332` ``` and jink: "j:k" ``` paulson@46820 ` 333` ``` shows "f(i) \ f(j)" ``` paulson@46820 ` 334` ```apply (insert leij jink) ``` paulson@13163 ` 335` ```apply (blast intro!: leCI lt_mono ford elim!: leE) ``` paulson@13163 ` 336` ```done ``` paulson@13163 ` 337` wenzelm@61798 ` 338` ```text\\\\ monotonicity, 1st argument\ ``` paulson@46820 ` 339` ```lemma add_le_mono1: "[| i \ j; j\nat |] ==> i#+k \ j#+k" ``` paulson@46820 ` 340` ```apply (rule_tac f = "%j. j#+k" in Ord_lt_mono_imp_le_mono, typecheck) ``` paulson@13163 ` 341` ```apply (blast intro: add_lt_mono1 add_type [THEN nat_into_Ord])+ ``` paulson@13163 ` 342` ```done ``` paulson@13163 ` 343` wenzelm@61798 ` 344` ```text\\\\ monotonicity, both arguments\ ``` paulson@46820 ` 345` ```lemma add_le_mono: "[| i \ j; k \ l; j\nat; l\nat |] ==> i#+k \ j#+l" ``` paulson@13163 ` 346` ```apply (rule add_le_mono1 [THEN le_trans], assumption+) ``` paulson@13163 ` 347` ```apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+) ``` paulson@13163 ` 348` ```done ``` paulson@13163 ` 349` wenzelm@60770 ` 350` ```text\Combinations of less-than and less-than-or-equals\ ``` paulson@14060 ` 351` paulson@14060 ` 352` ```lemma add_lt_le_mono: "[| il; j\nat; l\nat |] ==> i#+k < j#+l" ``` paulson@14060 ` 353` ```apply (rule add_lt_mono1 [THEN lt_trans2], assumption+) ``` paulson@14060 ` 354` ```apply (subst add_commute, subst add_commute, rule add_le_mono1, assumption+) ``` paulson@14060 ` 355` ```done ``` paulson@14060 ` 356` paulson@14060 ` 357` ```lemma add_le_lt_mono: "[| i\j; knat; l\nat |] ==> i#+k < j#+l" ``` paulson@14060 ` 358` ```by (subst add_commute, subst add_commute, erule add_lt_le_mono, assumption+) ``` paulson@14060 ` 359` wenzelm@60770 ` 360` ```text\Less-than: in other words, strict in both arguments\ ``` paulson@14060 ` 361` ```lemma add_lt_mono: "[| inat; l\nat |] ==> i#+k < j#+l" ``` paulson@46820 ` 362` ```apply (rule add_lt_le_mono) ``` paulson@46820 ` 363` ```apply (auto intro: leI) ``` paulson@14060 ` 364` ```done ``` paulson@14060 ` 365` paulson@13163 ` 366` ```(** Subtraction is the inverse of addition. **) ``` paulson@13163 ` 367` paulson@13163 ` 368` ```lemma diff_add_inverse: "(n#+m) #- n = natify(m)" ``` paulson@13163 ` 369` ```apply (subgoal_tac " (natify(n) #+ m) #- natify(n) = natify(m) ") ``` paulson@13163 ` 370` ```apply (rule_tac [2] n = "natify(n) " in nat_induct) ``` paulson@13163 ` 371` ```apply auto ``` paulson@13163 ` 372` ```done ``` paulson@13163 ` 373` paulson@13163 ` 374` ```lemma diff_add_inverse2: "(m#+n) #- n = natify(m)" ``` paulson@13163 ` 375` ```by (simp add: add_commute [of m] diff_add_inverse) ``` paulson@13163 ` 376` paulson@13163 ` 377` ```lemma diff_cancel: "(k#+m) #- (k#+n) = m #- n" ``` paulson@13163 ` 378` ```apply (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = ``` paulson@13163 ` 379` ``` natify(m) #- natify(n) ") ``` paulson@13163 ` 380` ```apply (rule_tac [2] n = "natify(k) " in nat_induct) ``` paulson@13163 ` 381` ```apply auto ``` paulson@13163 ` 382` ```done ``` paulson@13163 ` 383` paulson@13163 ` 384` ```lemma diff_cancel2: "(m#+k) #- (n#+k) = m #- n" ``` paulson@13163 ` 385` ```by (simp add: add_commute [of _ k] diff_cancel) ``` paulson@13163 ` 386` paulson@13163 ` 387` ```lemma diff_add_0: "n #- (n#+m) = 0" ``` paulson@13163 ` 388` ```apply (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0") ``` paulson@13163 ` 389` ```apply (rule_tac [2] n = "natify(n) " in nat_induct) ``` paulson@13163 ` 390` ```apply auto ``` paulson@13163 ` 391` ```done ``` paulson@13163 ` 392` paulson@13361 ` 393` ```lemma pred_0 [simp]: "pred(0) = 0" ``` paulson@13361 ` 394` ```by (simp add: pred_def) ``` paulson@13361 ` 395` paulson@13361 ` 396` ```lemma eq_succ_imp_eq_m1: "[|i = succ(j); i\nat|] ==> j = i #- 1 & j \nat" ``` paulson@46820 ` 397` ```by simp ``` paulson@13361 ` 398` paulson@13361 ` 399` ```lemma pred_Un_distrib: ``` paulson@46820 ` 400` ``` "[|i\nat; j\nat|] ==> pred(i \ j) = pred(i) \ pred(j)" ``` paulson@46820 ` 401` ```apply (erule_tac n=i in natE, simp) ``` paulson@46820 ` 402` ```apply (erule_tac n=j in natE, simp) ``` paulson@13361 ` 403` ```apply (simp add: succ_Un_distrib [symmetric]) ``` paulson@13361 ` 404` ```done ``` paulson@13361 ` 405` paulson@13361 ` 406` ```lemma pred_type [TC,simp]: ``` paulson@13361 ` 407` ``` "i \ nat ==> pred(i) \ nat" ``` paulson@13361 ` 408` ```by (simp add: pred_def split: split_nat_case) ``` paulson@13361 ` 409` wenzelm@58860 ` 410` ```lemma nat_diff_pred: "[|i\nat; j\nat|] ==> i #- succ(j) = pred(i #- j)" ``` paulson@46820 ` 411` ```apply (rule_tac m=i and n=j in diff_induct) ``` paulson@13361 ` 412` ```apply (auto simp add: pred_def nat_imp_quasinat split: split_nat_case) ``` paulson@13361 ` 413` ```done ``` paulson@13361 ` 414` wenzelm@58860 ` 415` ```lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)" ``` paulson@13361 ` 416` ```apply (insert nat_diff_pred [of "natify(i)" "natify(j)"]) ``` paulson@46820 ` 417` ```apply (simp add: natify_succ [symmetric]) ``` paulson@13361 ` 418` ```done ``` paulson@13361 ` 419` paulson@13361 ` 420` ```lemma nat_diff_Un_distrib: ``` paulson@46820 ` 421` ``` "[|i\nat; j\nat; k\nat|] ==> (i \ j) #- k = (i#-k) \ (j#-k)" ``` paulson@46820 ` 422` ```apply (rule_tac n=k in nat_induct) ``` paulson@46820 ` 423` ```apply (simp_all add: diff_succ_eq_pred pred_Un_distrib) ``` paulson@13361 ` 424` ```done ``` paulson@13361 ` 425` paulson@13361 ` 426` ```lemma diff_Un_distrib: ``` paulson@46820 ` 427` ``` "[|i\nat; j\nat|] ==> (i \ j) #- k = (i#-k) \ (j#-k)" ``` paulson@13361 ` 428` ```by (insert nat_diff_Un_distrib [of i j "natify(k)"], simp) ``` paulson@13361 ` 429` wenzelm@60770 ` 430` ```text\We actually prove @{term "i #- j #- k = i #- (j #+ k)"}\ ``` paulson@13361 ` 431` ```lemma diff_diff_left [simplified]: ``` wenzelm@58860 ` 432` ``` "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)" ``` paulson@13361 ` 433` ```by (rule_tac m="natify(i)" and n="natify(j)" in diff_induct, auto) ``` paulson@13361 ` 434` paulson@13163 ` 435` paulson@13163 ` 436` ```(** Lemmas for the CancelNumerals simproc **) ``` paulson@13163 ` 437` paulson@46821 ` 438` ```lemma eq_add_iff: "(u #+ m = u #+ n) \ (0 #+ m = natify(n))" ``` paulson@13163 ` 439` ```apply auto ``` paulson@13163 ` 440` ```apply (blast dest: add_left_cancel_natify) ``` paulson@13163 ` 441` ```apply (simp add: add_def) ``` paulson@13163 ` 442` ```done ``` paulson@13163 ` 443` paulson@46821 ` 444` ```lemma less_add_iff: "(u #+ m < u #+ n) \ (0 #+ m < natify(n))" ``` paulson@13163 ` 445` ```apply (auto simp add: add_lt_elim1_natify) ``` paulson@13163 ` 446` ```apply (drule add_lt_mono1) ``` paulson@13163 ` 447` ```apply (auto simp add: add_commute [of u]) ``` paulson@13163 ` 448` ```done ``` paulson@13163 ` 449` paulson@13163 ` 450` ```lemma diff_add_eq: "((u #+ m) #- (u #+ n)) = ((0 #+ m) #- n)" ``` paulson@13163 ` 451` ```by (simp add: diff_cancel) ``` paulson@13163 ` 452` paulson@13163 ` 453` ```(*To tidy up the result of a simproc. Only the RHS will be simplified.*) ``` paulson@13163 ` 454` ```lemma eq_cong2: "u = u' ==> (t==u) == (t==u')" ``` paulson@13163 ` 455` ```by auto ``` paulson@13163 ` 456` paulson@46821 ` 457` ```lemma iff_cong2: "u \ u' ==> (t==u) == (t==u')" ``` paulson@13163 ` 458` ```by auto ``` paulson@13163 ` 459` paulson@13163 ` 460` wenzelm@60770 ` 461` ```subsection\Multiplication\ ``` paulson@13163 ` 462` paulson@13163 ` 463` ```lemma mult_0 [simp]: "0 #* m = 0" ``` paulson@13163 ` 464` ```by (simp add: mult_def) ``` paulson@13163 ` 465` paulson@13163 ` 466` ```lemma mult_succ [simp]: "succ(m) #* n = n #+ (m #* n)" ``` paulson@13163 ` 467` ```by (simp add: add_def mult_def natify_succ raw_mult_type) ``` paulson@13163 ` 468` paulson@13163 ` 469` ```(*right annihilation in product*) ``` paulson@13163 ` 470` ```lemma mult_0_right [simp]: "m #* 0 = 0" ``` paulson@13163 ` 471` ```apply (unfold mult_def) ``` paulson@13163 ` 472` ```apply (rule_tac n = "natify(m) " in nat_induct) ``` paulson@13163 ` 473` ```apply auto ``` paulson@13163 ` 474` ```done ``` paulson@13163 ` 475` paulson@13163 ` 476` ```(*right successor law for multiplication*) ``` paulson@13163 ` 477` ```lemma mult_succ_right [simp]: "m #* succ(n) = m #+ (m #* n)" ``` paulson@13163 ` 478` ```apply (subgoal_tac "natify(m) #* succ (natify(n)) = ``` paulson@13163 ` 479` ``` natify(m) #+ (natify(m) #* natify(n))") ``` paulson@13163 ` 480` ```apply (simp (no_asm_use) add: natify_succ add_def mult_def) ``` paulson@13163 ` 481` ```apply (rule_tac n = "natify(m) " in nat_induct) ``` paulson@13163 ` 482` ```apply (simp_all add: add_ac) ``` paulson@13163 ` 483` ```done ``` paulson@13163 ` 484` paulson@13163 ` 485` ```lemma mult_1_natify [simp]: "1 #* n = natify(n)" ``` paulson@13163 ` 486` ```by auto ``` paulson@13163 ` 487` paulson@13163 ` 488` ```lemma mult_1_right_natify [simp]: "n #* 1 = natify(n)" ``` paulson@13163 ` 489` ```by auto ``` paulson@13163 ` 490` paulson@14060 ` 491` ```lemma mult_1: "n \ nat ==> 1 #* n = n" ``` paulson@13163 ` 492` ```by simp ``` paulson@13163 ` 493` paulson@14060 ` 494` ```lemma mult_1_right: "n \ nat ==> n #* 1 = n" ``` paulson@13163 ` 495` ```by simp ``` paulson@13163 ` 496` paulson@13163 ` 497` ```(*Commutative law for multiplication*) ``` paulson@13163 ` 498` ```lemma mult_commute: "m #* n = n #* m" ``` paulson@13163 ` 499` ```apply (subgoal_tac "natify(m) #* natify(n) = natify(n) #* natify(m) ") ``` paulson@13163 ` 500` ```apply (rule_tac [2] n = "natify(m) " in nat_induct) ``` paulson@13163 ` 501` ```apply auto ``` paulson@13163 ` 502` ```done ``` paulson@13163 ` 503` paulson@13163 ` 504` ```(*addition distributes over multiplication*) ``` paulson@13163 ` 505` ```lemma add_mult_distrib: "(m #+ n) #* k = (m #* k) #+ (n #* k)" ``` paulson@13163 ` 506` ```apply (subgoal_tac "(natify(m) #+ natify(n)) #* natify(k) = ``` paulson@13163 ` 507` ``` (natify(m) #* natify(k)) #+ (natify(n) #* natify(k))") ``` paulson@13163 ` 508` ```apply (rule_tac [2] n = "natify(m) " in nat_induct) ``` paulson@13163 ` 509` ```apply (simp_all add: add_assoc [symmetric]) ``` paulson@13163 ` 510` ```done ``` paulson@13163 ` 511` paulson@13163 ` 512` ```(*Distributive law on the left*) ``` paulson@13163 ` 513` ```lemma add_mult_distrib_left: "k #* (m #+ n) = (k #* m) #+ (k #* n)" ``` paulson@13163 ` 514` ```apply (subgoal_tac "natify(k) #* (natify(m) #+ natify(n)) = ``` paulson@13163 ` 515` ``` (natify(k) #* natify(m)) #+ (natify(k) #* natify(n))") ``` paulson@13163 ` 516` ```apply (rule_tac [2] n = "natify(m) " in nat_induct) ``` paulson@13163 ` 517` ```apply (simp_all add: add_ac) ``` paulson@13163 ` 518` ```done ``` paulson@13163 ` 519` paulson@13163 ` 520` ```(*Associative law for multiplication*) ``` paulson@13163 ` 521` ```lemma mult_assoc: "(m #* n) #* k = m #* (n #* k)" ``` paulson@13163 ` 522` ```apply (subgoal_tac "(natify(m) #* natify(n)) #* natify(k) = ``` paulson@13163 ` 523` ``` natify(m) #* (natify(n) #* natify(k))") ``` paulson@13163 ` 524` ```apply (rule_tac [2] n = "natify(m) " in nat_induct) ``` paulson@13163 ` 525` ```apply (simp_all add: add_mult_distrib) ``` paulson@13163 ` 526` ```done ``` paulson@13163 ` 527` paulson@13163 ` 528` ```(*for a/c rewriting*) ``` paulson@13163 ` 529` ```lemma mult_left_commute: "m #* (n #* k) = n #* (m #* k)" ``` paulson@13163 ` 530` ```apply (rule mult_commute [THEN trans]) ``` paulson@13163 ` 531` ```apply (rule mult_assoc [THEN trans]) ``` paulson@13163 ` 532` ```apply (rule mult_commute [THEN subst_context]) ``` paulson@13163 ` 533` ```done ``` paulson@13163 ` 534` paulson@13163 ` 535` ```lemmas mult_ac = mult_assoc mult_commute mult_left_commute ``` paulson@13163 ` 536` paulson@13163 ` 537` paulson@13163 ` 538` ```lemma lt_succ_eq_0_disj: ``` paulson@14060 ` 539` ``` "[| m\nat; n\nat |] ``` paulson@46821 ` 540` ``` ==> (m < succ(n)) \ (m = 0 | (\j\nat. m = succ(j) & j < n))" ``` paulson@13163 ` 541` ```by (induct_tac "m", auto) ``` paulson@13163 ` 542` paulson@13163 ` 543` ```lemma less_diff_conv [rule_format]: ``` paulson@46821 ` 544` ``` "[| j\nat; k\nat |] ==> \i\nat. (i < j #- k) \ (i #+ k < j)" ``` paulson@13784 ` 545` ```by (erule_tac m = k in diff_induct, auto) ``` paulson@13163 ` 546` paulson@13163 ` 547` ```lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat ``` paulson@13163 ` 548` clasohm@0 ` 549` ```end ```