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