1(* Title: HOL/Nat.thy 2 Author: Tobias Nipkow 3 Author: Lawrence C Paulson 4 Author: Markus Wenzel 5*) 6 7section \<open>Natural numbers\<close> 8 9theory Nat 10imports Inductive Typedef Fun Rings 11begin 12 13subsection \<open>Type \<open>ind\<close>\<close> 14 15typedecl ind 16 17axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \<Rightarrow> ind" 18 \<comment> \<open>The axiom of infinity in 2 parts:\<close> 19 where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y" 20 and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" 21 22 23subsection \<open>Type nat\<close> 24 25text \<open>Type definition\<close> 26 27inductive Nat :: "ind \<Rightarrow> bool" 28 where 29 Zero_RepI: "Nat Zero_Rep" 30 | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)" 31 32typedef nat = "{n. Nat n}" 33 morphisms Rep_Nat Abs_Nat 34 using Nat.Zero_RepI by auto 35 36lemma Nat_Rep_Nat: "Nat (Rep_Nat n)" 37 using Rep_Nat by simp 38 39lemma Nat_Abs_Nat_inverse: "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n" 40 using Abs_Nat_inverse by simp 41 42lemma Nat_Abs_Nat_inject: "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m" 43 using Abs_Nat_inject by simp 44 45instantiation nat :: zero 46begin 47 48definition Zero_nat_def: "0 = Abs_Nat Zero_Rep" 49 50instance .. 51 52end 53 54definition Suc :: "nat \<Rightarrow> nat" 55 where "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" 56 57lemma Suc_not_Zero: "Suc m \<noteq> 0" 58 by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI 59 Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat) 60 61lemma Zero_not_Suc: "0 \<noteq> Suc m" 62 by (rule not_sym) (rule Suc_not_Zero) 63 64lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y" 65 by (rule iffI, rule Suc_Rep_inject) simp_all 66 67lemma nat_induct0: 68 assumes "P 0" 69 and "\<And>n. P n \<Longrightarrow> P (Suc n)" 70 shows "P n" 71 using assms 72 apply (unfold Zero_nat_def Suc_def) 73 apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close> 74 apply (erule Nat_Rep_Nat [THEN Nat.induct]) 75 apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst]) 76 done 77 78free_constructors case_nat for "0 :: nat" | Suc pred 79 where "pred (0 :: nat) = (0 :: nat)" 80 apply atomize_elim 81 apply (rename_tac n, induct_tac n rule: nat_induct0, auto) 82 apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject' Rep_Nat_inject) 83 apply (simp only: Suc_not_Zero) 84 done 85 86\<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> 87setup \<open>Sign.mandatory_path "old"\<close> 88 89old_rep_datatype "0 :: nat" Suc 90 apply (erule nat_induct0) 91 apply assumption 92 apply (rule nat.inject) 93 apply (rule nat.distinct(1)) 94 done 95 96setup \<open>Sign.parent_path\<close> 97 98\<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> 99setup \<open>Sign.mandatory_path "nat"\<close> 100 101declare old.nat.inject[iff del] 102 and old.nat.distinct(1)[simp del, induct_simp del] 103 104lemmas induct = old.nat.induct 105lemmas inducts = old.nat.inducts 106lemmas rec = old.nat.rec 107lemmas simps = nat.inject nat.distinct nat.case nat.rec 108 109setup \<open>Sign.parent_path\<close> 110 111abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" 112 where "rec_nat \<equiv> old.rec_nat" 113 114declare nat.sel[code del] 115 116hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close> 117hide_fact 118 nat.case_eq_if 119 nat.collapse 120 nat.expand 121 nat.sel 122 nat.exhaust_sel 123 nat.split_sel 124 nat.split_sel_asm 125 126lemma nat_exhaust [case_names 0 Suc, cases type: nat]: 127 "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P" 128 \<comment> \<open>for backward compatibility -- names of variables differ\<close> 129 by (rule old.nat.exhaust) 130 131lemma nat_induct [case_names 0 Suc, induct type: nat]: 132 fixes n 133 assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)" 134 shows "P n" 135 \<comment> \<open>for backward compatibility -- names of variables differ\<close> 136 using assms by (rule nat.induct) 137 138hide_fact 139 nat_exhaust 140 nat_induct0 141 142ML \<open> 143val nat_basic_lfp_sugar = 144 let 145 val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global @{theory} @{type_name nat}); 146 val recx = Logic.varify_types_global @{term rec_nat}; 147 val C = body_type (fastype_of recx); 148 in 149 {T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]], 150 ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}} 151 end; 152\<close> 153 154setup \<open> 155let 156 fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt = 157 ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt) 158 | basic_lfp_sugars_of bs arg_Ts callers callssss ctxt = 159 BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt; 160in 161 BNF_LFP_Rec_Sugar.register_lfp_rec_extension 162 {nested_simps = [], special_endgame_tac = K (K (K (K no_tac))), is_new_datatype = K (K true), 163 basic_lfp_sugars_of = basic_lfp_sugars_of, rewrite_nested_rec_call = NONE} 164end 165\<close> 166 167text \<open>Injectiveness and distinctness lemmas\<close> 168 169context cancel_ab_semigroup_add 170begin 171 172lemma inj_on_add [simp]: 173 "inj_on (plus a) A" 174proof (rule inj_onI) 175 fix b c 176 assume "a + b = a + c" 177 then have "a + b - a = a + c - a" 178 by (simp only:) 179 then show "b = c" 180 by simp 181qed 182 183lemma inj_on_add' [simp]: 184 "inj_on (\<lambda>b. b + a) A" 185 using inj_on_add [of a A] by (simp add: add.commute [of _ a]) 186 187lemma bij_betw_add [simp]: 188 "bij_betw (plus a) A B \<longleftrightarrow> plus a ` A = B" 189 by (simp add: bij_betw_def) 190 191end 192 193text \<open>Translation lemmas\<close> 194 195context ab_group_add 196begin 197 198lemma surj_plus [simp]: "surj (plus a)" 199 by (auto intro: range_eqI [of b "plus a" "b - a" for b] simp add: algebra_simps) 200 201end 202 203lemma translation_Compl: 204 fixes a :: "'a::ab_group_add" 205 shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)" 206 apply (auto simp: image_iff) 207 apply (rule_tac x="x - a" in bexI, auto) 208 done 209 210lemma translation_UNIV: 211 fixes a :: "'a::ab_group_add" 212 shows "range (\<lambda>x. a + x) = UNIV" 213 by (fact surj_plus) 214 215lemma translation_diff: 216 fixes a :: "'a::ab_group_add" 217 shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)" 218 by auto 219 220lemma translation_Int: 221 fixes a :: "'a::ab_group_add" 222 shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)" 223 by auto 224 225context semidom_divide 226begin 227 228lemma inj_on_mult: 229 "inj_on (times a) A" if "a \<noteq> 0" 230proof (rule inj_onI) 231 fix b c 232 assume "a * b = a * c" 233 then have "a * b div a = a * c div a" 234 by (simp only:) 235 with that show "b = c" 236 by simp 237qed 238 239end 240 241lemma inj_Suc [simp]: 242 "inj_on Suc N" 243 by (simp add: inj_on_def) 244 245lemma bij_betw_Suc [simp]: 246 "bij_betw Suc M N \<longleftrightarrow> Suc ` M = N" 247 by (simp add: bij_betw_def) 248 249lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R" 250 by (rule notE) (rule Suc_not_Zero) 251 252lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R" 253 by (rule Suc_neq_Zero) (erule sym) 254 255lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y" 256 by (rule inj_Suc [THEN injD]) 257 258lemma n_not_Suc_n: "n \<noteq> Suc n" 259 by (induct n) simp_all 260 261lemma Suc_n_not_n: "Suc n \<noteq> n" 262 by (rule not_sym) (rule n_not_Suc_n) 263 264text \<open>A special form of induction for reasoning about @{term "m < n"} and @{term "m - n"}.\<close> 265lemma diff_induct: 266 assumes "\<And>x. P x 0" 267 and "\<And>y. P 0 (Suc y)" 268 and "\<And>x y. P x y \<Longrightarrow> P (Suc x) (Suc y)" 269 shows "P m n" 270proof (induct n arbitrary: m) 271 case 0 272 show ?case by (rule assms(1)) 273next 274 case (Suc n) 275 show ?case 276 proof (induct m) 277 case 0 278 show ?case by (rule assms(2)) 279 next 280 case (Suc m) 281 from \<open>P m n\<close> show ?case by (rule assms(3)) 282 qed 283qed 284 285 286subsection \<open>Arithmetic operators\<close> 287 288instantiation nat :: comm_monoid_diff 289begin 290 291primrec plus_nat 292 where 293 add_0: "0 + n = (n::nat)" 294 | add_Suc: "Suc m + n = Suc (m + n)" 295 296lemma add_0_right [simp]: "m + 0 = m" 297 for m :: nat 298 by (induct m) simp_all 299 300lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)" 301 by (induct m) simp_all 302 303declare add_0 [code] 304 305lemma add_Suc_shift [code]: "Suc m + n = m + Suc n" 306 by simp 307 308primrec minus_nat 309 where 310 diff_0 [code]: "m - 0 = (m::nat)" 311 | diff_Suc: "m - Suc n = (case m - n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k)" 312 313declare diff_Suc [simp del] 314 315lemma diff_0_eq_0 [simp, code]: "0 - n = 0" 316 for n :: nat 317 by (induct n) (simp_all add: diff_Suc) 318 319lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n" 320 by (induct n) (simp_all add: diff_Suc) 321 322instance 323proof 324 fix n m q :: nat 325 show "(n + m) + q = n + (m + q)" by (induct n) simp_all 326 show "n + m = m + n" by (induct n) simp_all 327 show "m + n - m = n" by (induct m) simp_all 328 show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc) 329 show "0 + n = n" by simp 330 show "0 - n = 0" by simp 331qed 332 333end 334 335hide_fact (open) add_0 add_0_right diff_0 336 337instantiation nat :: comm_semiring_1_cancel 338begin 339 340definition One_nat_def [simp]: "1 = Suc 0" 341 342primrec times_nat 343 where 344 mult_0: "0 * n = (0::nat)" 345 | mult_Suc: "Suc m * n = n + (m * n)" 346 347lemma mult_0_right [simp]: "m * 0 = 0" 348 for m :: nat 349 by (induct m) simp_all 350 351lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)" 352 by (induct m) (simp_all add: add.left_commute) 353 354lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)" 355 for m n k :: nat 356 by (induct m) (simp_all add: add.assoc) 357 358instance 359proof 360 fix k n m q :: nat 361 show "0 \<noteq> (1::nat)" 362 by simp 363 show "1 * n = n" 364 by simp 365 show "n * m = m * n" 366 by (induct n) simp_all 367 show "(n * m) * q = n * (m * q)" 368 by (induct n) (simp_all add: add_mult_distrib) 369 show "(n + m) * q = n * q + m * q" 370 by (rule add_mult_distrib) 371 show "k * (m - n) = (k * m) - (k * n)" 372 by (induct m n rule: diff_induct) simp_all 373qed 374 375end 376 377 378subsubsection \<open>Addition\<close> 379 380text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close> 381 382lemma add_is_0 [iff]: "m + n = 0 \<longleftrightarrow> m = 0 \<and> n = 0" 383 for m n :: nat 384 by (cases m) simp_all 385 386lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 \<or> m = 0 \<and> n = Suc 0" 387 by (cases m) simp_all 388 389lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 \<or> m = 0 \<and> n = Suc 0" 390 by (rule trans, rule eq_commute, rule add_is_1) 391 392lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0" 393 for m n :: nat 394 by (induct m) simp_all 395 396lemma plus_1_eq_Suc: 397 "plus 1 = Suc" 398 by (simp add: fun_eq_iff) 399 400lemma Suc_eq_plus1: "Suc n = n + 1" 401 by simp 402 403lemma Suc_eq_plus1_left: "Suc n = 1 + n" 404 by simp 405 406 407subsubsection \<open>Difference\<close> 408 409lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k" 410 by (simp add: diff_diff_add) 411 412lemma diff_Suc_1 [simp]: "Suc n - 1 = n" 413 by simp 414 415 416subsubsection \<open>Multiplication\<close> 417 418lemma mult_is_0 [simp]: "m * n = 0 \<longleftrightarrow> m = 0 \<or> n = 0" for m n :: nat 419 by (induct m) auto 420 421lemma mult_eq_1_iff [simp]: "m * n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0" 422proof (induct m) 423 case 0 424 then show ?case by simp 425next 426 case (Suc m) 427 then show ?case by (induct n) auto 428qed 429 430lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0" 431 apply (rule trans) 432 apply (rule_tac [2] mult_eq_1_iff) 433 apply fastforce 434 done 435 436lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" 437 for m n :: nat 438 unfolding One_nat_def by (rule mult_eq_1_iff) 439 440lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" 441 for m n :: nat 442 unfolding One_nat_def by (rule one_eq_mult_iff) 443 444lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0" 445 for k m n :: nat 446proof - 447 have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n" 448 proof (induct n arbitrary: m) 449 case 0 450 then show "m = 0" by simp 451 next 452 case (Suc n) 453 then show "m = Suc n" 454 by (cases m) (simp_all add: eq_commute [of 0]) 455 qed 456 then show ?thesis by auto 457qed 458 459lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0" 460 for k m n :: nat 461 by (simp add: mult.commute) 462 463lemma Suc_mult_cancel1: "Suc k * m = Suc k * n \<longleftrightarrow> m = n" 464 by (subst mult_cancel1) simp 465 466 467subsection \<open>Orders on @{typ nat}\<close> 468 469subsubsection \<open>Operation definition\<close> 470 471instantiation nat :: linorder 472begin 473 474primrec less_eq_nat 475 where 476 "(0::nat) \<le> n \<longleftrightarrow> True" 477 | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)" 478 479declare less_eq_nat.simps [simp del] 480 481lemma le0 [iff]: "0 \<le> n" for 482 n :: nat 483 by (simp add: less_eq_nat.simps) 484 485lemma [code]: "0 \<le> n \<longleftrightarrow> True" 486 for n :: nat 487 by simp 488 489definition less_nat 490 where less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m" 491 492lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> m" 493 by (simp add: less_eq_nat.simps(2)) 494 495lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n" 496 unfolding less_eq_Suc_le .. 497 498lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0" 499 for n :: nat 500 by (induct n) (simp_all add: less_eq_nat.simps(2)) 501 502lemma not_less0 [iff]: "\<not> n < 0" 503 for n :: nat 504 by (simp add: less_eq_Suc_le) 505 506lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False" 507 for n :: nat 508 by simp 509 510lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n" 511 by (simp add: less_eq_Suc_le) 512 513lemma less_Suc_eq_le [code]: "m < Suc n \<longleftrightarrow> m \<le> n" 514 by (simp add: less_eq_Suc_le) 515 516lemma Suc_less_eq2: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')" 517 by (cases m) auto 518 519lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n" 520 by (induct m arbitrary: n) (simp_all add: less_eq_nat.simps(2) split: nat.splits) 521 522lemma Suc_leD: "Suc m \<le> n \<Longrightarrow> m \<le> n" 523 by (cases n) (auto intro: le_SucI) 524 525lemma less_SucI: "m < n \<Longrightarrow> m < Suc n" 526 by (simp add: less_eq_Suc_le) (erule Suc_leD) 527 528lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n" 529 by (simp add: less_eq_Suc_le) (erule Suc_leD) 530 531instance 532proof 533 fix n m q :: nat 534 show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" 535 proof (induct n arbitrary: m) 536 case 0 537 then show ?case 538 by (cases m) (simp_all add: less_eq_Suc_le) 539 next 540 case (Suc n) 541 then show ?case 542 by (cases m) (simp_all add: less_eq_Suc_le) 543 qed 544 show "n \<le> n" 545 by (induct n) simp_all 546 then show "n = m" if "n \<le> m" and "m \<le> n" 547 using that by (induct n arbitrary: m) 548 (simp_all add: less_eq_nat.simps(2) split: nat.splits) 549 show "n \<le> q" if "n \<le> m" and "m \<le> q" 550 using that 551 proof (induct n arbitrary: m q) 552 case 0 553 show ?case by simp 554 next 555 case (Suc n) 556 then show ?case 557 by (simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify, 558 simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify, 559 simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits) 560 qed 561 show "n \<le> m \<or> m \<le> n" 562 by (induct n arbitrary: m) 563 (simp_all add: less_eq_nat.simps(2) split: nat.splits) 564qed 565 566end 567 568instantiation nat :: order_bot 569begin 570 571definition bot_nat :: nat 572 where "bot_nat = 0" 573 574instance 575 by standard (simp add: bot_nat_def) 576 577end 578 579instance nat :: no_top 580 by standard (auto intro: less_Suc_eq_le [THEN iffD2]) 581 582 583subsubsection \<open>Introduction properties\<close> 584 585lemma lessI [iff]: "n < Suc n" 586 by (simp add: less_Suc_eq_le) 587 588lemma zero_less_Suc [iff]: "0 < Suc n" 589 by (simp add: less_Suc_eq_le) 590 591 592subsubsection \<open>Elimination properties\<close> 593 594lemma less_not_refl: "\<not> n < n" 595 for n :: nat 596 by (rule order_less_irrefl) 597 598lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n" 599 for m n :: nat 600 by (rule not_sym) (rule less_imp_neq) 601 602lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t" 603 for s t :: nat 604 by (rule less_imp_neq) 605 606lemma less_irrefl_nat: "n < n \<Longrightarrow> R" 607 for n :: nat 608 by (rule notE, rule less_not_refl) 609 610lemma less_zeroE: "n < 0 \<Longrightarrow> R" 611 for n :: nat 612 by (rule notE) (rule not_less0) 613 614lemma less_Suc_eq: "m < Suc n \<longleftrightarrow> m < n \<or> m = n" 615 unfolding less_Suc_eq_le le_less .. 616 617lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)" 618 by (simp add: less_Suc_eq) 619 620lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0" 621 for n :: nat 622 unfolding One_nat_def by (rule less_Suc0) 623 624lemma Suc_mono: "m < n \<Longrightarrow> Suc m < Suc n" 625 by simp 626 627text \<open>"Less than" is antisymmetric, sort of.\<close> 628lemma less_antisym: "\<not> n < m \<Longrightarrow> n < Suc m \<Longrightarrow> m = n" 629 unfolding not_less less_Suc_eq_le by (rule antisym) 630 631lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" 632 for m n :: nat 633 by (rule linorder_neq_iff) 634 635 636subsubsection \<open>Inductive (?) properties\<close> 637 638lemma Suc_lessI: "m < n \<Longrightarrow> Suc m \<noteq> n \<Longrightarrow> Suc m < n" 639 unfolding less_eq_Suc_le [of m] le_less by simp 640 641lemma lessE: 642 assumes major: "i < k" 643 and 1: "k = Suc i \<Longrightarrow> P" 644 and 2: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P" 645 shows P 646proof - 647 from major have "\<exists>j. i \<le> j \<and> k = Suc j" 648 unfolding less_eq_Suc_le by (induct k) simp_all 649 then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i" 650 by (auto simp add: less_le) 651 with 1 2 show P by auto 652qed 653 654lemma less_SucE: 655 assumes major: "m < Suc n" 656 and less: "m < n \<Longrightarrow> P" 657 and eq: "m = n \<Longrightarrow> P" 658 shows P 659 apply (rule major [THEN lessE]) 660 apply (rule eq) 661 apply blast 662 apply (rule less) 663 apply blast 664 done 665 666lemma Suc_lessE: 667 assumes major: "Suc i < k" 668 and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P" 669 shows P 670 apply (rule major [THEN lessE]) 671 apply (erule lessI [THEN minor]) 672 apply (erule Suc_lessD [THEN minor]) 673 apply assumption 674 done 675 676lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n" 677 by simp 678 679lemma less_trans_Suc: 680 assumes le: "i < j" 681 shows "j < k \<Longrightarrow> Suc i < k" 682proof (induct k) 683 case 0 684 then show ?case by simp 685next 686 case (Suc k) 687 with le show ?case 688 by simp (auto simp add: less_Suc_eq dest: Suc_lessD) 689qed 690 691text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{prop "n = m \<or> n < m"}.\<close> 692lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m" 693 by (simp only: not_less less_Suc_eq_le) 694 695lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m" 696 by (simp only: not_le Suc_le_eq) 697 698text \<open>Properties of "less than or equal".\<close> 699 700lemma le_imp_less_Suc: "m \<le> n \<Longrightarrow> m < Suc n" 701 by (simp only: less_Suc_eq_le) 702 703lemma Suc_n_not_le_n: "\<not> Suc n \<le> n" 704 by (simp add: not_le less_Suc_eq_le) 705 706lemma le_Suc_eq: "m \<le> Suc n \<longleftrightarrow> m \<le> n \<or> m = Suc n" 707 by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq) 708 709lemma le_SucE: "m \<le> Suc n \<Longrightarrow> (m \<le> n \<Longrightarrow> R) \<Longrightarrow> (m = Suc n \<Longrightarrow> R) \<Longrightarrow> R" 710 by (drule le_Suc_eq [THEN iffD1], iprover+) 711 712lemma Suc_leI: "m < n \<Longrightarrow> Suc m \<le> n" 713 by (simp only: Suc_le_eq) 714 715text \<open>Stronger version of \<open>Suc_leD\<close>.\<close> 716lemma Suc_le_lessD: "Suc m \<le> n \<Longrightarrow> m < n" 717 by (simp only: Suc_le_eq) 718 719lemma less_imp_le_nat: "m < n \<Longrightarrow> m \<le> n" for m n :: nat 720 unfolding less_eq_Suc_le by (rule Suc_leD) 721 722text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close> 723lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq 724 725 726text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close> 727 728lemma less_or_eq_imp_le: "m < n \<or> m = n \<Longrightarrow> m \<le> n" 729 for m n :: nat 730 unfolding le_less . 731 732lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n" 733 for m n :: nat 734 by (rule le_less) 735 736text \<open>Useful with \<open>blast\<close>.\<close> 737lemma eq_imp_le: "m = n \<Longrightarrow> m \<le> n" 738 for m n :: nat 739 by auto 740 741lemma le_refl: "n \<le> n" 742 for n :: nat 743 by simp 744 745lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" 746 for i j k :: nat 747 by (rule order_trans) 748 749lemma le_antisym: "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n" 750 for m n :: nat 751 by (rule antisym) 752 753lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n" 754 for m n :: nat 755 by (rule less_le) 756 757lemma le_neq_implies_less: "m \<le> n \<Longrightarrow> m \<noteq> n \<Longrightarrow> m < n" 758 for m n :: nat 759 unfolding less_le .. 760 761lemma nat_le_linear: "m \<le> n \<or> n \<le> m" 762 for m n :: nat 763 by (rule linear) 764 765lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] 766 767lemma le_less_Suc_eq: "m \<le> n \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m" 768 unfolding less_Suc_eq_le by auto 769 770lemma not_less_less_Suc_eq: "\<not> n < m \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m" 771 unfolding not_less by (rule le_less_Suc_eq) 772 773lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq 774 775lemma not0_implies_Suc: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m" 776 by (cases n) simp_all 777 778lemma gr0_implies_Suc: "n > 0 \<Longrightarrow> \<exists>m. n = Suc m" 779 by (cases n) simp_all 780 781lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0" 782 for m n :: nat 783 by (cases n) simp_all 784 785lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n" 786 for n :: nat 787 by (cases n) simp_all 788 789text \<open>This theorem is useful with \<open>blast\<close>\<close> 790lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" 791 for n :: nat 792 by (rule neq0_conv[THEN iffD1]) iprover 793 794lemma gr0_conv_Suc: "0 < n \<longleftrightarrow> (\<exists>m. n = Suc m)" 795 by (fast intro: not0_implies_Suc) 796 797lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0" 798 for n :: nat 799 using neq0_conv by blast 800 801lemma Suc_le_D: "Suc n \<le> m' \<Longrightarrow> \<exists>m. m' = Suc m" 802 by (induct m') simp_all 803 804text \<open>Useful in certain inductive arguments\<close> 805lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)" 806 by (cases m) simp_all 807 808lemma All_less_Suc: "(\<forall>i < Suc n. P i) = (P n \<and> (\<forall>i < n. P i))" 809by (auto simp: less_Suc_eq) 810 811lemma All_less_Suc2: "(\<forall>i < Suc n. P i) = (P 0 \<and> (\<forall>i < n. P(Suc i)))" 812by (auto simp: less_Suc_eq_0_disj) 813 814lemma Ex_less_Suc: "(\<exists>i < Suc n. P i) = (P n \<or> (\<exists>i < n. P i))" 815by (auto simp: less_Suc_eq) 816 817lemma Ex_less_Suc2: "(\<exists>i < Suc n. P i) = (P 0 \<or> (\<exists>i < n. P(Suc i)))" 818by (auto simp: less_Suc_eq_0_disj) 819 820 821subsubsection \<open>Monotonicity of Addition\<close> 822 823lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n - Suc 0) = n" 824 by (simp add: diff_Suc split: nat.split) 825 826lemma Suc_diff_1 [simp]: "0 < n \<Longrightarrow> Suc (n - 1) = n" 827 unfolding One_nat_def by (rule Suc_pred) 828 829lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n" 830 for k m n :: nat 831 by (induct k) simp_all 832 833lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n" 834 for k m n :: nat 835 by (induct k) simp_all 836 837lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0" 838 for m n :: nat 839 by (auto dest: gr0_implies_Suc) 840 841text \<open>strict, in 1st argument\<close> 842lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k" 843 for i j k :: nat 844 by (induct k) simp_all 845 846text \<open>strict, in both arguments\<close> 847lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l" 848 for i j k l :: nat 849 apply (rule add_less_mono1 [THEN less_trans], assumption+) 850 apply (induct j) 851 apply simp_all 852 done 853 854text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close> 855lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)" 856proof (induct n) 857 case 0 858 then show ?case by simp 859next 860 case Suc 861 then show ?case 862 by (simp add: order_le_less) 863 (blast elim!: less_SucE intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric]) 864qed 865 866lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)" 867 for k l :: nat 868 by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add) 869 870text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close> 871lemma mult_less_mono2: 872 fixes i j :: nat 873 assumes "i < j" and "0 < k" 874 shows "k * i < k * j" 875 using \<open>0 < k\<close> 876proof (induct k) 877 case 0 878 then show ?case by simp 879next 880 case (Suc k) 881 with \<open>i < j\<close> show ?case 882 by (cases k) (simp_all add: add_less_mono) 883qed 884 885text \<open>Addition is the inverse of subtraction: 886 if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close> 887lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m - n) = m" 888 for m n :: nat 889 by (induct m n rule: diff_induct) simp_all 890 891lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)" 892 for m n :: nat 893 using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex) 894 895text \<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>.\<close> 896 897instance nat :: linordered_semidom 898proof 899 fix m n q :: nat 900 show "0 < (1::nat)" 901 by simp 902 show "m \<le> n \<Longrightarrow> q + m \<le> q + n" 903 by simp 904 show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" 905 by (simp add: mult_less_mono2) 906 show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" 907 by simp 908 show "n \<le> m \<Longrightarrow> (m - n) + n = m" 909 by (simp add: add_diff_inverse_nat add.commute linorder_not_less) 910qed 911 912instance nat :: dioid 913 by standard (rule nat_le_iff_add) 914 915declare le0[simp del] \<comment> \<open>This is now @{thm zero_le}\<close> 916declare le_0_eq[simp del] \<comment> \<open>This is now @{thm le_zero_eq}\<close> 917declare not_less0[simp del] \<comment> \<open>This is now @{thm not_less_zero}\<close> 918declare not_gr0[simp del] \<comment> \<open>This is now @{thm not_gr_zero}\<close> 919 920instance nat :: ordered_cancel_comm_monoid_add .. 921instance nat :: ordered_cancel_comm_monoid_diff .. 922 923 924subsubsection \<open>@{term min} and @{term max}\<close> 925 926lemma mono_Suc: "mono Suc" 927 by (rule monoI) simp 928 929lemma min_0L [simp]: "min 0 n = 0" 930 for n :: nat 931 by (rule min_absorb1) simp 932 933lemma min_0R [simp]: "min n 0 = 0" 934 for n :: nat 935 by (rule min_absorb2) simp 936 937lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)" 938 by (simp add: mono_Suc min_of_mono) 939 940lemma min_Suc1: "min (Suc n) m = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min n m'))" 941 by (simp split: nat.split) 942 943lemma min_Suc2: "min m (Suc n) = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min m' n))" 944 by (simp split: nat.split) 945 946lemma max_0L [simp]: "max 0 n = n" 947 for n :: nat 948 by (rule max_absorb2) simp 949 950lemma max_0R [simp]: "max n 0 = n" 951 for n :: nat 952 by (rule max_absorb1) simp 953 954lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)" 955 by (simp add: mono_Suc max_of_mono) 956 957lemma max_Suc1: "max (Suc n) m = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max n m'))" 958 by (simp split: nat.split) 959 960lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))" 961 by (simp split: nat.split) 962 963lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)" 964 for m n q :: nat 965 by (simp add: min_def not_le) 966 (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans) 967 968lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)" 969 for m n q :: nat 970 by (simp add: min_def not_le) 971 (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans) 972 973lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)" 974 for m n q :: nat 975 by (simp add: max_def) 976 977lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)" 978 for m n q :: nat 979 by (simp add: max_def) 980 981lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)" 982 for m n q :: nat 983 by (simp add: max_def not_le) 984 (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans) 985 986lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)" 987 for m n q :: nat 988 by (simp add: max_def not_le) 989 (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans) 990 991 992subsubsection \<open>Additional theorems about @{term "(\<le>)"}\<close> 993 994text \<open>Complete induction, aka course-of-values induction\<close> 995 996instance nat :: wellorder 997proof 998 fix P and n :: nat 999 assume step: "(\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n" for n :: nat 1000 have "\<And>q. q \<le> n \<Longrightarrow> P q" 1001 proof (induct n) 1002 case (0 n) 1003 have "P 0" by (rule step) auto 1004 with 0 show ?case by auto 1005 next 1006 case (Suc m n) 1007 then have "n \<le> m \<or> n = Suc m" 1008 by (simp add: le_Suc_eq) 1009 then show ?case 1010 proof 1011 assume "n \<le> m" 1012 then show "P n" by (rule Suc(1)) 1013 next 1014 assume n: "n = Suc m" 1015 show "P n" by (rule step) (rule Suc(1), simp add: n le_simps) 1016 qed 1017 qed 1018 then show "P n" by auto 1019qed 1020 1021 1022lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0" 1023 for P :: "nat \<Rightarrow> bool" 1024 by (rule Least_equality[OF _ le0]) 1025 1026lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))" 1027 apply (cases n) 1028 apply auto 1029 apply (frule LeastI) 1030 apply (drule_tac P = "\<lambda>x. P (Suc x)" in LeastI) 1031 apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") 1032 apply (erule_tac [2] Least_le) 1033 apply (cases "LEAST x. P x") 1034 apply auto 1035 apply (drule_tac P = "\<lambda>x. P (Suc x)" in Least_le) 1036 apply (blast intro: order_antisym) 1037 done 1038 1039lemma Least_Suc2: "P n \<Longrightarrow> Q m \<Longrightarrow> \<not> P 0 \<Longrightarrow> \<forall>k. P (Suc k) = Q k \<Longrightarrow> Least P = Suc (Least Q)" 1040 by (erule (1) Least_Suc [THEN ssubst]) simp 1041 1042lemma ex_least_nat_le: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k" 1043 for P :: "nat \<Rightarrow> bool" 1044 apply (cases n) 1045 apply blast 1046 apply (rule_tac x="LEAST k. P k" in exI) 1047 apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex) 1048 done 1049 1050lemma ex_least_nat_less: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (k + 1)" 1051 for P :: "nat \<Rightarrow> bool" 1052 apply (cases n) 1053 apply blast 1054 apply (frule (1) ex_least_nat_le) 1055 apply (erule exE) 1056 apply (case_tac k) 1057 apply simp 1058 apply (rename_tac k1) 1059 apply (rule_tac x=k1 in exI) 1060 apply (auto simp add: less_eq_Suc_le) 1061 done 1062 1063lemma nat_less_induct: 1064 fixes P :: "nat \<Rightarrow> bool" 1065 assumes "\<And>n. \<forall>m. m < n \<longrightarrow> P m \<Longrightarrow> P n" 1066 shows "P n" 1067 using assms less_induct by blast 1068 1069lemma measure_induct_rule [case_names less]: 1070 fixes f :: "'a \<Rightarrow> 'b::wellorder" 1071 assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x" 1072 shows "P a" 1073 by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step) 1074 1075text \<open>old style induction rules:\<close> 1076lemma measure_induct: 1077 fixes f :: "'a \<Rightarrow> 'b::wellorder" 1078 shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a" 1079 by (rule measure_induct_rule [of f P a]) iprover 1080 1081lemma full_nat_induct: 1082 assumes step: "\<And>n. (\<forall>m. Suc m \<le> n \<longrightarrow> P m) \<Longrightarrow> P n" 1083 shows "P n" 1084 by (rule less_induct) (auto intro: step simp:le_simps) 1085 1086text\<open>An induction rule for establishing binary relations\<close> 1087lemma less_Suc_induct [consumes 1]: 1088 assumes less: "i < j" 1089 and step: "\<And>i. P i (Suc i)" 1090 and trans: "\<And>i j k. i < j \<Longrightarrow> j < k \<Longrightarrow> P i j \<Longrightarrow> P j k \<Longrightarrow> P i k" 1091 shows "P i j" 1092proof - 1093 from less obtain k where j: "j = Suc (i + k)" 1094 by (auto dest: less_imp_Suc_add) 1095 have "P i (Suc (i + k))" 1096 proof (induct k) 1097 case 0 1098 show ?case by (simp add: step) 1099 next 1100 case (Suc k) 1101 have "0 + i < Suc k + i" by (rule add_less_mono1) simp 1102 then have "i < Suc (i + k)" by (simp add: add.commute) 1103 from trans[OF this lessI Suc step] 1104 show ?case by simp 1105 qed 1106 then show "P i j" by (simp add: j) 1107qed 1108 1109text \<open> 1110 The method of infinite descent, frequently used in number theory. 1111 Provided by Roelof Oosterhuis. 1112 \<open>P n\<close> is true for all natural numbers if 1113 \<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close> 1114 \<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists 1115 a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>. 1116\<close> 1117 1118lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool" 1119 \<comment> \<open>compact version without explicit base case\<close> 1120 by (induct n rule: less_induct) auto 1121 1122lemma infinite_descent0 [case_names 0 smaller]: 1123 fixes P :: "nat \<Rightarrow> bool" 1124 assumes "P 0" 1125 and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m" 1126 shows "P n" 1127 apply (rule infinite_descent) 1128 using assms 1129 apply (case_tac "n > 0") 1130 apply auto 1131 done 1132 1133text \<open> 1134 Infinite descent using a mapping to \<open>nat\<close>: 1135 \<open>P x\<close> is true for all \<open>x \<in> D\<close> if there exists a \<open>V \<in> D \<Rightarrow> nat\<close> and 1136 \<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close> 1137 \<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove 1138 there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>. 1139\<close> 1140corollary infinite_descent0_measure [case_names 0 smaller]: 1141 fixes V :: "'a \<Rightarrow> nat" 1142 assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x" 1143 and 2: "\<And>x. V x > 0 \<Longrightarrow> \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y" 1144 shows "P x" 1145proof - 1146 obtain n where "n = V x" by auto 1147 moreover have "\<And>x. V x = n \<Longrightarrow> P x" 1148 proof (induct n rule: infinite_descent0) 1149 case 0 1150 with 1 show "P x" by auto 1151 next 1152 case (smaller n) 1153 then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto 1154 with 2 obtain y where "V y < V x \<and> \<not> P y" by auto 1155 with * obtain m where "m = V y \<and> m < n \<and> \<not> P y" by auto 1156 then show ?case by auto 1157 qed 1158 ultimately show "P x" by auto 1159qed 1160 1161text \<open>Again, without explicit base case:\<close> 1162lemma infinite_descent_measure: 1163 fixes V :: "'a \<Rightarrow> nat" 1164 assumes "\<And>x. \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y" 1165 shows "P x" 1166proof - 1167 from assms obtain n where "n = V x" by auto 1168 moreover have "\<And>x. V x = n \<Longrightarrow> P x" 1169 proof (induct n rule: infinite_descent, auto) 1170 show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x 1171 using assms and that by auto 1172 qed 1173 ultimately show "P x" by auto 1174qed 1175 1176text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close> 1177lemma less_mono_imp_le_mono: 1178 fixes f :: "nat \<Rightarrow> nat" 1179 and i j :: nat 1180 assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j" 1181 and "i \<le> j" 1182 shows "f i \<le> f j" 1183 using assms by (auto simp add: order_le_less) 1184 1185 1186text \<open>non-strict, in 1st argument\<close> 1187lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k" 1188 for i j k :: nat 1189 by (rule add_right_mono) 1190 1191text \<open>non-strict, in both arguments\<close> 1192lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l" 1193 for i j k l :: nat 1194 by (rule add_mono) 1195 1196lemma le_add2: "n \<le> m + n" 1197 for m n :: nat 1198 by simp 1199 1200lemma le_add1: "n \<le> n + m" 1201 for m n :: nat 1202 by simp 1203 1204lemma less_add_Suc1: "i < Suc (i + m)" 1205 by (rule le_less_trans, rule le_add1, rule lessI) 1206 1207lemma less_add_Suc2: "i < Suc (m + i)" 1208 by (rule le_less_trans, rule le_add2, rule lessI) 1209 1210lemma less_iff_Suc_add: "m < n \<longleftrightarrow> (\<exists>k. n = Suc (m + k))" 1211 by (iprover intro!: less_add_Suc1 less_imp_Suc_add) 1212 1213lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m" 1214 for i j m :: nat 1215 by (rule le_trans, assumption, rule le_add1) 1216 1217lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j" 1218 for i j m :: nat 1219 by (rule le_trans, assumption, rule le_add2) 1220 1221lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m" 1222 for i j m :: nat 1223 by (rule less_le_trans, assumption, rule le_add1) 1224 1225lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j" 1226 for i j m :: nat 1227 by (rule less_le_trans, assumption, rule le_add2) 1228 1229lemma add_lessD1: "i + j < k \<Longrightarrow> i < k" 1230 for i j k :: nat 1231 by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1) 1232 1233lemma not_add_less1 [iff]: "\<not> i + j < i" 1234 for i j :: nat 1235 apply (rule notI) 1236 apply (drule add_lessD1) 1237 apply (erule less_irrefl [THEN notE]) 1238 done 1239 1240lemma not_add_less2 [iff]: "\<not> j + i < i" 1241 for i j :: nat 1242 by (simp add: add.commute) 1243 1244lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n" 1245 for k m n :: nat 1246 by (rule order_trans [of _ "m + k"]) (simp_all add: le_add1) 1247 1248lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n" 1249 for k m n :: nat 1250 apply (simp add: add.commute) 1251 apply (erule add_leD1) 1252 done 1253 1254lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R" 1255 for k m n :: nat 1256 by (blast dest: add_leD1 add_leD2) 1257 1258text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close> 1259lemma less_add_eq_less: "\<And>k. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n" 1260 for l m n :: nat 1261 by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps) 1262 1263 1264subsubsection \<open>More results about difference\<close> 1265 1266lemma Suc_diff_le: "n \<le> m \<Longrightarrow> Suc m - n = Suc (m - n)" 1267 by (induct m n rule: diff_induct) simp_all 1268 1269lemma diff_less_Suc: "m - n < Suc m" 1270 apply (induct m n rule: diff_induct) 1271 apply (erule_tac [3] less_SucE) 1272 apply (simp_all add: less_Suc_eq) 1273 done 1274 1275lemma diff_le_self [simp]: "m - n \<le> m" 1276 for m n :: nat 1277 by (induct m n rule: diff_induct) (simp_all add: le_SucI) 1278 1279lemma less_imp_diff_less: "j < k \<Longrightarrow> j - n < k" 1280 for j k n :: nat 1281 by (rule le_less_trans, rule diff_le_self) 1282 1283lemma diff_Suc_less [simp]: "0 < n \<Longrightarrow> n - Suc i < n" 1284 by (cases n) (auto simp add: le_simps) 1285 1286lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)" 1287 for i j k :: nat 1288 by (induct j k rule: diff_induct) simp_all 1289 1290lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k" 1291 for i j k :: nat 1292 by (fact diff_add_assoc [symmetric]) 1293 1294lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i) - k = (j - k) + i" 1295 for i j k :: nat 1296 by (simp add: ac_simps) 1297 1298lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j - k + i = j + i - k" 1299 for i j k :: nat 1300 by (fact diff_add_assoc2 [symmetric]) 1301 1302lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)" 1303 for i j k :: nat 1304 by auto 1305 1306lemma diff_is_0_eq [simp]: "m - n = 0 \<longleftrightarrow> m \<le> n" 1307 for m n :: nat 1308 by (induct m n rule: diff_induct) simp_all 1309 1310lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0" 1311 for m n :: nat 1312 by (rule iffD2, rule diff_is_0_eq) 1313 1314lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n" 1315 for m n :: nat 1316 by (induct m n rule: diff_induct) simp_all 1317 1318lemma less_imp_add_positive: 1319 assumes "i < j" 1320 shows "\<exists>k::nat. 0 < k \<and> i + k = j" 1321proof 1322 from assms show "0 < j - i \<and> i + (j - i) = j" 1323 by (simp add: order_less_imp_le) 1324qed 1325 1326text \<open>a nice rewrite for bounded subtraction\<close> 1327lemma nat_minus_add_max: "n - m + m = max n m" 1328 for m n :: nat 1329 by (simp add: max_def not_le order_less_imp_le) 1330 1331lemma nat_diff_split: "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)" 1332 for a b :: nat 1333 \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close> 1334 by (cases "a < b") (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym]) 1335 1336lemma nat_diff_split_asm: "P (a - b) \<longleftrightarrow> \<not> (a < b \<and> \<not> P 0 \<or> (\<exists>d. a = b + d \<and> \<not> P d))" 1337 for a b :: nat 1338 \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close> 1339 by (auto split: nat_diff_split) 1340 1341lemma Suc_pred': "0 < n \<Longrightarrow> n = Suc(n - 1)" 1342 by simp 1343 1344lemma add_eq_if: "m + n = (if m = 0 then n else Suc ((m - 1) + n))" 1345 unfolding One_nat_def by (cases m) simp_all 1346 1347lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m - 1) * n))" 1348 for m n :: nat 1349 by (cases m) simp_all 1350 1351lemma Suc_diff_eq_diff_pred: "0 < n \<Longrightarrow> Suc m - n = m - (n - 1)" 1352 by (cases n) simp_all 1353 1354lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" 1355 by (cases m) simp_all 1356 1357lemma Let_Suc [simp]: "Let (Suc n) f \<equiv> f (Suc n)" 1358 by (fact Let_def) 1359 1360 1361subsubsection \<open>Monotonicity of multiplication\<close> 1362 1363lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k" 1364 for i j k :: nat 1365 by (simp add: mult_right_mono) 1366 1367lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j" 1368 for i j k :: nat 1369 by (simp add: mult_left_mono) 1370 1371text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close> 1372lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l" 1373 for i j k l :: nat 1374 by (simp add: mult_mono) 1375 1376lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k" 1377 for i j k :: nat 1378 by (simp add: mult_strict_right_mono) 1379 1380text \<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that there are no negative numbers.\<close> 1381lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n" 1382 for m n :: nat 1383proof (induct m) 1384 case 0 1385 then show ?case by simp 1386next 1387 case (Suc m) 1388 then show ?case by (cases n) simp_all 1389qed 1390 1391lemma one_le_mult_iff [simp]: "Suc 0 \<le> m * n \<longleftrightarrow> Suc 0 \<le> m \<and> Suc 0 \<le> n" 1392proof (induct m) 1393 case 0 1394 then show ?case by simp 1395next 1396 case (Suc m) 1397 then show ?case by (cases n) simp_all 1398qed 1399 1400lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n" 1401 for k m n :: nat 1402 apply (safe intro!: mult_less_mono1) 1403 apply (cases k) 1404 apply auto 1405 apply (simp add: linorder_not_le [symmetric]) 1406 apply (blast intro: mult_le_mono1) 1407 done 1408 1409lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n" 1410 for k m n :: nat 1411 by (simp add: mult.commute [of k]) 1412 1413lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" 1414 for k m n :: nat 1415 by (simp add: linorder_not_less [symmetric], auto) 1416 1417lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" 1418 for k m n :: nat 1419 by (simp add: linorder_not_less [symmetric], auto) 1420 1421lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \<longleftrightarrow> m < n" 1422 by (subst mult_less_cancel1) simp 1423 1424lemma Suc_mult_le_cancel1: "Suc k * m \<le> Suc k * n \<longleftrightarrow> m \<le> n" 1425 by (subst mult_le_cancel1) simp 1426 1427lemma le_square: "m \<le> m * m" 1428 for m :: nat 1429 by (cases m) (auto intro: le_add1) 1430 1431lemma le_cube: "m \<le> m * (m * m)" 1432 for m :: nat 1433 by (cases m) (auto intro: le_add1) 1434 1435text \<open>Lemma for \<open>gcd\<close>\<close> 1436lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" 1437 for m n :: nat 1438 apply (drule sym) 1439 apply (rule disjCI) 1440 apply (rule linorder_cases) 1441 defer 1442 apply assumption 1443 apply (drule mult_less_mono2) 1444 apply auto 1445 done 1446 1447lemma mono_times_nat: 1448 fixes n :: nat 1449 assumes "n > 0" 1450 shows "mono (times n)" 1451proof 1452 fix m q :: nat 1453 assume "m \<le> q" 1454 with assms show "n * m \<le> n * q" by simp 1455qed 1456 1457text \<open>The lattice order on @{typ nat}.\<close> 1458 1459instantiation nat :: distrib_lattice 1460begin 1461 1462definition "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min" 1463 1464definition "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max" 1465 1466instance 1467 by intro_classes 1468 (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def 1469 intro: order_less_imp_le antisym elim!: order_trans order_less_trans) 1470 1471end 1472 1473 1474subsection \<open>Natural operation of natural numbers on functions\<close> 1475 1476text \<open> 1477 We use the same logical constant for the power operations on 1478 functions and relations, in order to share the same syntax. 1479\<close> 1480 1481consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" 1482 1483abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80) 1484 where "f ^^ n \<equiv> compow n f" 1485 1486notation (latex output) 1487 compower ("(_\<^bsup>_\<^esup>)" [1000] 1000) 1488 1489text \<open>\<open>f ^^ n = f \<circ> \<dots> \<circ> f\<close>, the \<open>n\<close>-fold composition of \<open>f\<close>\<close> 1490 1491overloading 1492 funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" 1493begin 1494 1495primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" 1496 where 1497 "funpow 0 f = id" 1498 | "funpow (Suc n) f = f \<circ> funpow n f" 1499 1500end 1501 1502lemma funpow_0 [simp]: "(f ^^ 0) x = x" 1503 by simp 1504 1505lemma funpow_Suc_right: "f ^^ Suc n = f ^^ n \<circ> f" 1506proof (induct n) 1507 case 0 1508 then show ?case by simp 1509next 1510 fix n 1511 assume "f ^^ Suc n = f ^^ n \<circ> f" 1512 then show "f ^^ Suc (Suc n) = f ^^ Suc n \<circ> f" 1513 by (simp add: o_assoc) 1514qed 1515 1516lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right 1517 1518text \<open>For code generation.\<close> 1519 1520definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" 1521 where funpow_code_def [code_abbrev]: "funpow = compow" 1522 1523lemma [code]: 1524 "funpow (Suc n) f = f \<circ> funpow n f" 1525 "funpow 0 f = id" 1526 by (simp_all add: funpow_code_def) 1527 1528hide_const (open) funpow 1529 1530lemma funpow_add: "f ^^ (m + n) = f ^^ m \<circ> f ^^ n" 1531 by (induct m) simp_all 1532 1533lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)" 1534 for f :: "'a \<Rightarrow> 'a" 1535 by (induct n) (simp_all add: funpow_add) 1536 1537lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)" 1538proof - 1539 have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp 1540 also have "\<dots> = (f ^^ n \<circ> f ^^ 1) x" by (simp only: funpow_add) 1541 also have "\<dots> = (f ^^ n) (f x)" by simp 1542 finally show ?thesis . 1543qed 1544 1545lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)" 1546 for f :: "'a \<Rightarrow> 'a" 1547 by (induct n) simp_all 1548 1549lemma Suc_funpow[simp]: "Suc ^^ n = ((+) n)" 1550 by (induct n) simp_all 1551 1552lemma id_funpow[simp]: "id ^^ n = id" 1553 by (induct n) simp_all 1554 1555lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B" 1556 for f :: "'a \<Rightarrow> ('a::order)" 1557 by (induct n arbitrary: A B) 1558 (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def) 1559 1560lemma funpow_mono2: 1561 assumes "mono f" 1562 and "i \<le> j" 1563 and "x \<le> y" 1564 and "x \<le> f x" 1565 shows "(f ^^ i) x \<le> (f ^^ j) y" 1566 using assms(2,3) 1567proof (induct j arbitrary: y) 1568 case 0 1569 then show ?case by simp 1570next 1571 case (Suc j) 1572 show ?case 1573 proof(cases "i = Suc j") 1574 case True 1575 with assms(1) Suc show ?thesis 1576 by (simp del: funpow.simps add: funpow_simps_right monoD funpow_mono) 1577 next 1578 case False 1579 with assms(1,4) Suc show ?thesis 1580 by (simp del: funpow.simps add: funpow_simps_right le_eq_less_or_eq less_Suc_eq_le) 1581 (simp add: Suc.hyps monoD order_subst1) 1582 qed 1583qed 1584 1585lemma inj_fn[simp]: 1586 fixes f::"'a \<Rightarrow> 'a" 1587 assumes "inj f" 1588 shows "inj (f^^n)" 1589proof (induction n) 1590 case Suc thus ?case using inj_comp[OF assms Suc.IH] by (simp del: comp_apply) 1591qed simp 1592 1593lemma surj_fn[simp]: 1594 fixes f::"'a \<Rightarrow> 'a" 1595 assumes "surj f" 1596 shows "surj (f^^n)" 1597proof (induction n) 1598 case Suc thus ?case by (simp add: comp_surj[OF Suc.IH assms] del: comp_apply) 1599qed simp 1600 1601lemma bij_fn[simp]: 1602 fixes f::"'a \<Rightarrow> 'a" 1603 assumes "bij f" 1604 shows "bij (f^^n)" 1605by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]]) 1606 1607 1608subsection \<open>Kleene iteration\<close> 1609 1610lemma Kleene_iter_lpfp: 1611 fixes f :: "'a::order_bot \<Rightarrow> 'a" 1612 assumes "mono f" 1613 and "f p \<le> p" 1614 shows "(f ^^ k) bot \<le> p" 1615proof (induct k) 1616 case 0 1617 show ?case by simp 1618next 1619 case Suc 1620 show ?case 1621 using monoD[OF assms(1) Suc] assms(2) by simp 1622qed 1623 1624lemma lfp_Kleene_iter: 1625 assumes "mono f" 1626 and "(f ^^ Suc k) bot = (f ^^ k) bot" 1627 shows "lfp f = (f ^^ k) bot" 1628proof (rule antisym) 1629 show "lfp f \<le> (f ^^ k) bot" 1630 proof (rule lfp_lowerbound) 1631 show "f ((f ^^ k) bot) \<le> (f ^^ k) bot" 1632 using assms(2) by simp 1633 qed 1634 show "(f ^^ k) bot \<le> lfp f" 1635 using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp 1636qed 1637 1638lemma mono_pow: "mono f \<Longrightarrow> mono (f ^^ n)" 1639 for f :: "'a \<Rightarrow> 'a::complete_lattice" 1640 by (induct n) (auto simp: mono_def) 1641 1642lemma lfp_funpow: 1643 assumes f: "mono f" 1644 shows "lfp (f ^^ Suc n) = lfp f" 1645proof (rule antisym) 1646 show "lfp f \<le> lfp (f ^^ Suc n)" 1647 proof (rule lfp_lowerbound) 1648 have "f (lfp (f ^^ Suc n)) = lfp (\<lambda>x. f ((f ^^ n) x))" 1649 unfolding funpow_Suc_right by (simp add: lfp_rolling f mono_pow comp_def) 1650 then show "f (lfp (f ^^ Suc n)) \<le> lfp (f ^^ Suc n)" 1651 by (simp add: comp_def) 1652 qed 1653 have "(f ^^ n) (lfp f) = lfp f" for n 1654 by (induct n) (auto intro: f lfp_fixpoint) 1655 then show "lfp (f ^^ Suc n) \<le> lfp f" 1656 by (intro lfp_lowerbound) (simp del: funpow.simps) 1657qed 1658 1659lemma gfp_funpow: 1660 assumes f: "mono f" 1661 shows "gfp (f ^^ Suc n) = gfp f" 1662proof (rule antisym) 1663 show "gfp f \<ge> gfp (f ^^ Suc n)" 1664 proof (rule gfp_upperbound) 1665 have "f (gfp (f ^^ Suc n)) = gfp (\<lambda>x. f ((f ^^ n) x))" 1666 unfolding funpow_Suc_right by (simp add: gfp_rolling f mono_pow comp_def) 1667 then show "f (gfp (f ^^ Suc n)) \<ge> gfp (f ^^ Suc n)" 1668 by (simp add: comp_def) 1669 qed 1670 have "(f ^^ n) (gfp f) = gfp f" for n 1671 by (induct n) (auto intro: f gfp_fixpoint) 1672 then show "gfp (f ^^ Suc n) \<ge> gfp f" 1673 by (intro gfp_upperbound) (simp del: funpow.simps) 1674qed 1675 1676lemma Kleene_iter_gpfp: 1677 fixes f :: "'a::order_top \<Rightarrow> 'a" 1678 assumes "mono f" 1679 and "p \<le> f p" 1680 shows "p \<le> (f ^^ k) top" 1681proof (induct k) 1682 case 0 1683 show ?case by simp 1684next 1685 case Suc 1686 show ?case 1687 using monoD[OF assms(1) Suc] assms(2) by simp 1688qed 1689 1690lemma gfp_Kleene_iter: 1691 assumes "mono f" 1692 and "(f ^^ Suc k) top = (f ^^ k) top" 1693 shows "gfp f = (f ^^ k) top" 1694 (is "?lhs = ?rhs") 1695proof (rule antisym) 1696 have "?rhs \<le> f ?rhs" 1697 using assms(2) by simp 1698 then show "?rhs \<le> ?lhs" 1699 by (rule gfp_upperbound) 1700 show "?lhs \<le> ?rhs" 1701 using Kleene_iter_gpfp[OF assms(1)] gfp_unfold[OF assms(1)] by simp 1702qed 1703 1704 1705subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close> 1706 1707context semiring_1 1708begin 1709 1710definition of_nat :: "nat \<Rightarrow> 'a" 1711 where "of_nat n = (plus 1 ^^ n) 0" 1712 1713lemma of_nat_simps [simp]: 1714 shows of_nat_0: "of_nat 0 = 0" 1715 and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" 1716 by (simp_all add: of_nat_def) 1717 1718lemma of_nat_1 [simp]: "of_nat 1 = 1" 1719 by (simp add: of_nat_def) 1720 1721lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n" 1722 by (induct m) (simp_all add: ac_simps) 1723 1724lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n" 1725 by (induct m) (simp_all add: ac_simps distrib_right) 1726 1727lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x" 1728 by (induct x) (simp_all add: algebra_simps) 1729 1730primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" 1731 where 1732 "of_nat_aux inc 0 i = i" 1733 | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close> 1734 1735lemma of_nat_code: "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0" 1736proof (induct n) 1737 case 0 1738 then show ?case by simp 1739next 1740 case (Suc n) 1741 have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1" 1742 by (induct n) simp_all 1743 from this [of 0] have "of_nat_aux (\<lambda>i. i + 1) n 1 = of_nat_aux (\<lambda>i. i + 1) n 0 + 1" 1744 by simp 1745 with Suc show ?case 1746 by (simp add: add.commute) 1747qed 1748 1749lemma of_nat_of_bool [simp]: 1750 "of_nat (of_bool P) = of_bool P" 1751 by auto 1752 1753end 1754 1755declare of_nat_code [code] 1756 1757context ring_1 1758begin 1759 1760lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n" 1761 by (simp add: algebra_simps of_nat_add [symmetric]) 1762 1763end 1764 1765text \<open>Class for unital semirings with characteristic zero. 1766 Includes non-ordered rings like the complex numbers.\<close> 1767 1768class semiring_char_0 = semiring_1 + 1769 assumes inj_of_nat: "inj of_nat" 1770begin 1771 1772lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n" 1773 by (auto intro: inj_of_nat injD) 1774 1775text \<open>Special cases where either operand is zero\<close> 1776 1777lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n" 1778 by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0]) 1779 1780lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0" 1781 by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0]) 1782 1783lemma of_nat_1_eq_iff [simp]: "1 = of_nat n \<longleftrightarrow> n=1" 1784 using of_nat_eq_iff by fastforce 1785 1786lemma of_nat_eq_1_iff [simp]: "of_nat n = 1 \<longleftrightarrow> n=1" 1787 using of_nat_eq_iff by fastforce 1788 1789lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \<noteq> 0" 1790 unfolding of_nat_eq_0_iff by simp 1791 1792lemma of_nat_0_neq [simp]: "0 \<noteq> of_nat (Suc n)" 1793 unfolding of_nat_0_eq_iff by simp 1794 1795end 1796 1797class ring_char_0 = ring_1 + semiring_char_0 1798 1799context linordered_nonzero_semiring 1800begin 1801 1802lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n" 1803 by (induct n) simp_all 1804 1805lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0" 1806 by (simp add: not_less) 1807 1808lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j" 1809 by (auto simp: le_iff_add intro!: add_increasing2) 1810 1811lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n" 1812proof(induct m n rule: diff_induct) 1813 case (1 m) then show ?case 1814 by auto 1815next 1816 case (2 n) then show ?case 1817 by (simp add: add_pos_nonneg) 1818next 1819 case (3 m n) 1820 then show ?case 1821 by (auto simp: add_commute [of 1] add_mono1 not_less add_right_mono leD) 1822qed 1823 1824lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n" 1825 by (simp add: not_less [symmetric] linorder_not_less [symmetric]) 1826 1827lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n" 1828 by simp 1829 1830lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n" 1831 by simp 1832 1833text \<open>Every \<open>linordered_nonzero_semiring\<close> has characteristic zero.\<close> 1834 1835subclass semiring_char_0 1836 by standard (auto intro!: injI simp add: eq_iff) 1837 1838text \<open>Special cases where either operand is zero\<close> 1839 1840lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0" 1841 by (rule of_nat_le_iff [of _ 0, simplified]) 1842 1843lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n" 1844 by (rule of_nat_less_iff [of 0, simplified]) 1845 1846end 1847 1848 1849context linordered_semidom 1850begin 1851subclass linordered_nonzero_semiring .. 1852subclass semiring_char_0 .. 1853end 1854 1855 1856context linordered_idom 1857begin 1858 1859lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n" 1860 unfolding abs_if by auto 1861 1862lemma sgn_of_nat [simp]: 1863 "sgn (of_nat n) = of_bool (n > 0)" 1864 by simp 1865 1866end 1867 1868lemma of_nat_id [simp]: "of_nat n = n" 1869 by (induct n) simp_all 1870 1871lemma of_nat_eq_id [simp]: "of_nat = id" 1872 by (auto simp add: fun_eq_iff) 1873 1874 1875subsection \<open>The set of natural numbers\<close> 1876 1877context semiring_1 1878begin 1879 1880definition Nats :: "'a set" ("\<nat>") 1881 where "\<nat> = range of_nat" 1882 1883lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>" 1884 by (simp add: Nats_def) 1885 1886lemma Nats_0 [simp]: "0 \<in> \<nat>" 1887 apply (simp add: Nats_def) 1888 apply (rule range_eqI) 1889 apply (rule of_nat_0 [symmetric]) 1890 done 1891 1892lemma Nats_1 [simp]: "1 \<in> \<nat>" 1893 apply (simp add: Nats_def) 1894 apply (rule range_eqI) 1895 apply (rule of_nat_1 [symmetric]) 1896 done 1897 1898lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>" 1899 apply (auto simp add: Nats_def) 1900 apply (rule range_eqI) 1901 apply (rule of_nat_add [symmetric]) 1902 done 1903 1904lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>" 1905 apply (auto simp add: Nats_def) 1906 apply (rule range_eqI) 1907 apply (rule of_nat_mult [symmetric]) 1908 done 1909 1910lemma Nats_cases [cases set: Nats]: 1911 assumes "x \<in> \<nat>" 1912 obtains (of_nat) n where "x = of_nat n" 1913 unfolding Nats_def 1914proof - 1915 from \<open>x \<in> \<nat>\<close> have "x \<in> range of_nat" unfolding Nats_def . 1916 then obtain n where "x = of_nat n" .. 1917 then show thesis .. 1918qed 1919 1920lemma Nats_induct [case_names of_nat, induct set: Nats]: "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x" 1921 by (rule Nats_cases) auto 1922 1923end 1924 1925 1926subsection \<open>Further arithmetic facts concerning the natural numbers\<close> 1927 1928lemma subst_equals: 1929 assumes "t = s" and "u = t" 1930 shows "u = s" 1931 using assms(2,1) by (rule trans) 1932 1933ML_file "Tools/nat_arith.ML" 1934 1935simproc_setup nateq_cancel_sums 1936 ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") = 1937 \<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close> 1938 1939simproc_setup natless_cancel_sums 1940 ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") = 1941 \<open>fn phi => try o Nat_Arith.cancel_less_conv\<close> 1942 1943simproc_setup natle_cancel_sums 1944 ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") = 1945 \<open>fn phi => try o Nat_Arith.cancel_le_conv\<close> 1946 1947simproc_setup natdiff_cancel_sums 1948 ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") = 1949 \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close> 1950 1951context order 1952begin 1953 1954lemma lift_Suc_mono_le: 1955 assumes mono: "\<And>n. f n \<le> f (Suc n)" 1956 and "n \<le> n'" 1957 shows "f n \<le> f n'" 1958proof (cases "n < n'") 1959 case True 1960 then show ?thesis 1961 by (induct n n' rule: less_Suc_induct) (auto intro: mono) 1962next 1963 case False 1964 with \<open>n \<le> n'\<close> show ?thesis by auto 1965qed 1966 1967lemma lift_Suc_antimono_le: 1968 assumes mono: "\<And>n. f n \<ge> f (Suc n)" 1969 and "n \<le> n'" 1970 shows "f n \<ge> f n'" 1971proof (cases "n < n'") 1972 case True 1973 then show ?thesis 1974 by (induct n n' rule: less_Suc_induct) (auto intro: mono) 1975next 1976 case False 1977 with \<open>n \<le> n'\<close> show ?thesis by auto 1978qed 1979 1980lemma lift_Suc_mono_less: 1981 assumes mono: "\<And>n. f n < f (Suc n)" 1982 and "n < n'" 1983 shows "f n < f n'" 1984 using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono) 1985 1986lemma lift_Suc_mono_less_iff: "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m" 1987 by (blast intro: less_asym' lift_Suc_mono_less [of f] 1988 dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1]) 1989 1990end 1991 1992lemma mono_iff_le_Suc: "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" 1993 unfolding mono_def by (auto intro: lift_Suc_mono_le [of f]) 1994 1995lemma antimono_iff_le_Suc: "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)" 1996 unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f]) 1997 1998lemma mono_nat_linear_lb: 1999 fixes f :: "nat \<Rightarrow> nat" 2000 assumes "\<And>m n. m < n \<Longrightarrow> f m < f n" 2001 shows "f m + k \<le> f (m + k)" 2002proof (induct k) 2003 case 0 2004 then show ?case by simp 2005next 2006 case (Suc k) 2007 then have "Suc (f m + k) \<le> Suc (f (m + k))" by simp 2008 also from assms [of "m + k" "Suc (m + k)"] have "Suc (f (m + k)) \<le> f (Suc (m + k))" 2009 by (simp add: Suc_le_eq) 2010 finally show ?case by simp 2011qed 2012 2013 2014text \<open>Subtraction laws, mostly by Clemens Ballarin\<close> 2015 2016lemma diff_less_mono: 2017 fixes a b c :: nat 2018 assumes "a < b" and "c \<le> a" 2019 shows "a - c < b - c" 2020proof - 2021 from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0" 2022 by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps) 2023 then show ?thesis by simp 2024qed 2025 2026lemma less_diff_conv: "i < j - k \<longleftrightarrow> i + k < j" 2027 for i j k :: nat 2028 by (cases "k \<le> j") (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex) 2029 2030lemma less_diff_conv2: "k \<le> j \<Longrightarrow> j - k < i \<longleftrightarrow> j < i + k" 2031 for j k i :: nat 2032 by (auto dest: le_Suc_ex) 2033 2034lemma le_diff_conv: "j - k \<le> i \<longleftrightarrow> j \<le> i + k" 2035 for j k i :: nat 2036 by (cases "k \<le> j") (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex) 2037 2038lemma diff_diff_cancel [simp]: "i \<le> n \<Longrightarrow> n - (n - i) = i" 2039 for i n :: nat 2040 by (auto dest: le_Suc_ex) 2041 2042lemma diff_less [simp]: "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m" 2043 for i n :: nat 2044 by (auto dest: less_imp_Suc_add) 2045 2046text \<open>Simplification of relational expressions involving subtraction\<close> 2047 2048lemma diff_diff_eq: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n" 2049 for m n k :: nat 2050 by (auto dest!: le_Suc_ex) 2051 2052hide_fact (open) diff_diff_eq 2053 2054lemma eq_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n" 2055 for m n k :: nat 2056 by (auto dest: le_Suc_ex) 2057 2058lemma less_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n" 2059 for m n k :: nat 2060 by (auto dest!: le_Suc_ex) 2061 2062lemma le_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n" 2063 for m n k :: nat 2064 by (auto dest!: le_Suc_ex) 2065 2066lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> a" 2067 for a b c :: nat 2068 by (force dest: le_Suc_ex) 2069 2070 2071text \<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close> 2072 2073lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l" 2074 for m n l :: nat 2075 by (auto dest: less_imp_le less_imp_Suc_add split: nat_diff_split) 2076 2077lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m" 2078 for m n l :: nat 2079 by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split: nat_diff_split) 2080 2081lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m" 2082 for m n l :: nat 2083 by (auto dest: less_imp_Suc_add split: nat_diff_split) 2084 2085lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n" 2086 for m n :: nat 2087 by (simp split: nat_diff_split) 2088 2089lemma min_diff: "min (m - i) (n - i) = min m n - i" 2090 for m n i :: nat 2091 by (cases m n rule: le_cases) 2092 (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono) 2093 2094lemma inj_on_diff_nat: 2095 fixes k :: nat 2096 assumes "\<And>n. n \<in> N \<Longrightarrow> k \<le> n" 2097 shows "inj_on (\<lambda>n. n - k) N" 2098proof (rule inj_onI) 2099 fix x y 2100 assume a: "x \<in> N" "y \<in> N" "x - k = y - k" 2101 with assms have "x - k + k = y - k + k" by auto 2102 with a assms show "x = y" by (auto simp add: eq_diff_iff) 2103qed 2104 2105text \<open>Rewriting to pull differences out\<close> 2106 2107lemma diff_diff_right [simp]: "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j" 2108 for i j k :: nat 2109 by (fact diff_diff_right) 2110 2111lemma diff_Suc_diff_eq1 [simp]: 2112 assumes "k \<le> j" 2113 shows "i - Suc (j - k) = i + k - Suc j" 2114proof - 2115 from assms have *: "Suc (j - k) = Suc j - k" 2116 by (simp add: Suc_diff_le) 2117 from assms have "k \<le> Suc j" 2118 by (rule order_trans) simp 2119 with diff_diff_right [of k "Suc j" i] * show ?thesis 2120 by simp 2121qed 2122 2123lemma diff_Suc_diff_eq2 [simp]: 2124 assumes "k \<le> j" 2125 shows "Suc (j - k) - i = Suc j - (k + i)" 2126proof - 2127 from assms obtain n where "j = k + n" 2128 by (auto dest: le_Suc_ex) 2129 moreover have "Suc n - i = (k + Suc n) - (k + i)" 2130 using add_diff_cancel_left [of k "Suc n" i] by simp 2131 ultimately show ?thesis by simp 2132qed 2133 2134lemma Suc_diff_Suc: 2135 assumes "n < m" 2136 shows "Suc (m - Suc n) = m - n" 2137proof - 2138 from assms obtain q where "m = n + Suc q" 2139 by (auto dest: less_imp_Suc_add) 2140 moreover define r where "r = Suc q" 2141 ultimately have "Suc (m - Suc n) = r" and "m = n + r" 2142 by simp_all 2143 then show ?thesis by simp 2144qed 2145 2146lemma one_less_mult: "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n" 2147 using less_1_mult [of n m] by (simp add: ac_simps) 2148 2149lemma n_less_m_mult_n: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n" 2150 using mult_strict_right_mono [of 1 m n] by simp 2151 2152lemma n_less_n_mult_m: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m" 2153 using mult_strict_left_mono [of 1 m n] by simp 2154 2155 2156text \<open>Induction starting beyond zero\<close> 2157 2158lemma nat_induct_at_least [consumes 1, case_names base Suc]: 2159 "P n" if "n \<ge> m" "P m" "\<And>n. n \<ge> m \<Longrightarrow> P n \<Longrightarrow> P (Suc n)" 2160proof - 2161 define q where "q = n - m" 2162 with \<open>n \<ge> m\<close> have "n = m + q" 2163 by simp 2164 moreover have "P (m + q)" 2165 by (induction q) (use that in simp_all) 2166 ultimately show "P n" 2167 by simp 2168qed 2169 2170lemma nat_induct_non_zero [consumes 1, case_names 1 Suc]: 2171 "P n" if "n > 0" "P 1" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)" 2172proof - 2173 from \<open>n > 0\<close> have "n \<ge> 1" 2174 by (cases n) simp_all 2175 moreover note \<open>P 1\<close> 2176 moreover have "\<And>n. n \<ge> 1 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)" 2177 using \<open>\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)\<close> 2178 by (simp add: Suc_le_eq) 2179 ultimately show "P n" 2180 by (rule nat_induct_at_least) 2181qed 2182 2183 2184text \<open>Specialized induction principles that work "backwards":\<close> 2185 2186lemma inc_induct [consumes 1, case_names base step]: 2187 assumes less: "i \<le> j" 2188 and base: "P j" 2189 and step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n" 2190 shows "P i" 2191 using less step 2192proof (induct "j - i" arbitrary: i) 2193 case (0 i) 2194 then have "i = j" by simp 2195 with base show ?case by simp 2196next 2197 case (Suc d n) 2198 from Suc.hyps have "n \<noteq> j" by auto 2199 with Suc have "n < j" by (simp add: less_le) 2200 from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp 2201 then have "d + 1 - 1 = j - n - 1" by simp 2202 then have "d = j - n - 1" by simp 2203 then have "d = j - (n + 1)" by (simp add: diff_diff_eq) 2204 then have "d = j - Suc n" by simp 2205 moreover from \<open>n < j\<close> have "Suc n \<le> j" by (simp add: Suc_le_eq) 2206 ultimately have "P (Suc n)" 2207 proof (rule Suc.hyps) 2208 fix q 2209 assume "Suc n \<le> q" 2210 then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le) 2211 moreover assume "q < j" 2212 moreover assume "P (Suc q)" 2213 ultimately show "P q" by (rule Suc.prems) 2214 qed 2215 with order_refl \<open>n < j\<close> show "P n" by (rule Suc.prems) 2216qed 2217 2218lemma strict_inc_induct [consumes 1, case_names base step]: 2219 assumes less: "i < j" 2220 and base: "\<And>i. j = Suc i \<Longrightarrow> P i" 2221 and step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i" 2222 shows "P i" 2223using less proof (induct "j - i - 1" arbitrary: i) 2224 case (0 i) 2225 from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0" 2226 by (auto dest!: less_imp_Suc_add) 2227 with 0 have "j = Suc i" 2228 by (auto intro: order_antisym simp add: Suc_le_eq) 2229 with base show ?case by simp 2230next 2231 case (Suc d i) 2232 from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i" 2233 by (simp add: diff_diff_add) 2234 then have "Suc d - 1 = j - Suc i - 1" by simp 2235 then have "d = j - Suc i - 1" by simp 2236 moreover from * have "j - Suc i \<noteq> 0" by auto 2237 then have "Suc i < j" by (simp add: not_le) 2238 ultimately have "P (Suc i)" by (rule Suc.hyps) 2239 with \<open>i < j\<close> show "P i" by (rule step) 2240qed 2241 2242lemma zero_induct_lemma: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P (k - i)" 2243 using inc_induct[of "k - i" k P, simplified] by blast 2244 2245lemma zero_induct: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P 0" 2246 using inc_induct[of 0 k P] by blast 2247 2248text \<open>Further induction rule similar to @{thm inc_induct}.\<close> 2249 2250lemma dec_induct [consumes 1, case_names base step]: 2251 "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j" 2252proof (induct j arbitrary: i) 2253 case 0 2254 then show ?case by simp 2255next 2256 case (Suc j) 2257 from Suc.prems consider "i \<le> j" | "i = Suc j" 2258 by (auto simp add: le_Suc_eq) 2259 then show ?case 2260 proof cases 2261 case 1 2262 moreover have "j < Suc j" by simp 2263 moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close> 2264 proof (rule Suc.hyps) 2265 fix q 2266 assume "i \<le> q" 2267 moreover assume "q < j" then have "q < Suc j" 2268 by (simp add: less_Suc_eq) 2269 moreover assume "P q" 2270 ultimately show "P (Suc q)" by (rule Suc.prems) 2271 qed 2272 ultimately show "P (Suc j)" by (rule Suc.prems) 2273 next 2274 case 2 2275 with \<open>P i\<close> show "P (Suc j)" by simp 2276 qed 2277qed 2278 2279lemma transitive_stepwise_le: 2280 assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)" 2281 shows "R m n" 2282using \<open>m \<le> n\<close> 2283 by (induction rule: dec_induct) (use assms in blast)+ 2284 2285 2286subsubsection \<open>Greatest operator\<close> 2287 2288lemma ex_has_greatest_nat: 2289 "P (k::nat) \<Longrightarrow> \<forall>y. P y \<longrightarrow> y \<le> b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x)" 2290proof (induction "b-k" arbitrary: b k rule: less_induct) 2291 case less 2292 show ?case 2293 proof cases 2294 assume "\<exists>n>k. P n" 2295 then obtain n where "n>k" "P n" by blast 2296 have "n \<le> b" using \<open>P n\<close> less.prems(2) by auto 2297 hence "b-n < b-k" 2298 by(rule diff_less_mono2[OF \<open>k<n\<close> less_le_trans[OF \<open>k<n\<close>]]) 2299 from less.hyps[OF this \<open>P n\<close> less.prems(2)] 2300 show ?thesis . 2301 next 2302 assume "\<not> (\<exists>n>k. P n)" 2303 hence "\<forall>y. P y \<longrightarrow> y \<le> k" by (auto simp: not_less) 2304 thus ?thesis using less.prems(1) by auto 2305 qed 2306qed 2307 2308lemma GreatestI_nat: 2309 "\<lbrakk> P(k::nat); \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)" 2310apply(drule (1) ex_has_greatest_nat) 2311using GreatestI2_order by auto 2312 2313lemma Greatest_le_nat: 2314 "\<lbrakk> P(k::nat); \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> k \<le> (Greatest P)" 2315apply(frule (1) ex_has_greatest_nat) 2316using GreatestI2_order[where P=P and Q=\<open>\<lambda>x. k \<le> x\<close>] by auto 2317 2318lemma GreatestI_ex_nat: 2319 "\<lbrakk> \<exists>k::nat. P k; \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)" 2320apply (erule exE) 2321apply (erule (1) GreatestI_nat) 2322done 2323 2324 2325subsection \<open>Monotonicity of \<open>funpow\<close>\<close> 2326 2327lemma funpow_increasing: "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>" 2328 for f :: "'a::{lattice,order_top} \<Rightarrow> 'a" 2329 by (induct rule: inc_induct) 2330 (auto simp del: funpow.simps(2) simp add: funpow_Suc_right 2331 intro: order_trans[OF _ funpow_mono]) 2332 2333lemma funpow_decreasing: "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>" 2334 for f :: "'a::{lattice,order_bot} \<Rightarrow> 'a" 2335 by (induct rule: dec_induct) 2336 (auto simp del: funpow.simps(2) simp add: funpow_Suc_right 2337 intro: order_trans[OF _ funpow_mono]) 2338 2339lemma mono_funpow: "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)" 2340 for Q :: "'a::{lattice,order_bot} \<Rightarrow> 'a" 2341 by (auto intro!: funpow_decreasing simp: mono_def) 2342 2343lemma antimono_funpow: "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)" 2344 for Q :: "'a::{lattice,order_top} \<Rightarrow> 'a" 2345 by (auto intro!: funpow_increasing simp: antimono_def) 2346 2347 2348subsection \<open>The divides relation on @{typ nat}\<close> 2349 2350lemma dvd_1_left [iff]: "Suc 0 dvd k" 2351 by (simp add: dvd_def) 2352 2353lemma dvd_1_iff_1 [simp]: "m dvd Suc 0 \<longleftrightarrow> m = Suc 0" 2354 by (simp add: dvd_def) 2355 2356lemma nat_dvd_1_iff_1 [simp]: "m dvd 1 \<longleftrightarrow> m = 1" 2357 for m :: nat 2358 by (simp add: dvd_def) 2359 2360lemma dvd_antisym: "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n" 2361 for m n :: nat 2362 unfolding dvd_def by (force dest: mult_eq_self_implies_10 simp add: mult.assoc) 2363 2364lemma dvd_diff_nat [simp]: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)" 2365 for k m n :: nat 2366 unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric]) 2367 2368lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m" 2369 for k m n :: nat 2370 apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst]) 2371 apply (blast intro: dvd_add) 2372 done 2373 2374lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n" 2375 for k m n :: nat 2376 by (drule_tac m = m in dvd_diff_nat) auto 2377 2378lemma dvd_mult_cancel: 2379 fixes m n k :: nat 2380 assumes "k * m dvd k * n" and "0 < k" 2381 shows "m dvd n" 2382proof - 2383 from assms(1) obtain q where "k * n = (k * m) * q" .. 2384 then have "k * n = k * (m * q)" by (simp add: ac_simps) 2385 with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel) 2386 then show ?thesis .. 2387qed 2388 2389lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1" 2390 for m n :: nat 2391 apply auto 2392 apply (subgoal_tac "m * n dvd m * 1") 2393 apply (drule dvd_mult_cancel) 2394 apply auto 2395 done 2396 2397lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1" 2398 for m n :: nat 2399 using dvd_mult_cancel1 [of m n] by (simp add: ac_simps) 2400 2401lemma dvd_imp_le: "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> n" 2402 for k n :: nat 2403 by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) 2404 2405lemma nat_dvd_not_less: "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m" 2406 for m n :: nat 2407 by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) 2408 2409lemma less_eq_dvd_minus: 2410 fixes m n :: nat 2411 assumes "m \<le> n" 2412 shows "m dvd n \<longleftrightarrow> m dvd n - m" 2413proof - 2414 from assms have "n = m + (n - m)" by simp 2415 then obtain q where "n = m + q" .. 2416 then show ?thesis by (simp add: add.commute [of m]) 2417qed 2418 2419lemma dvd_minus_self: "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n" 2420 for m n :: nat 2421 by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le) 2422 2423lemma dvd_minus_add: 2424 fixes m n q r :: nat 2425 assumes "q \<le> n" "q \<le> r * m" 2426 shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)" 2427proof - 2428 have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)" 2429 using dvd_add_times_triv_left_iff [of m r] by simp 2430 also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp 2431 also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp 2432 also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute) 2433 finally show ?thesis . 2434qed 2435 2436 2437subsection \<open>Aliasses\<close> 2438 2439lemma nat_mult_1: "1 * n = n" 2440 for n :: nat 2441 by (fact mult_1_left) 2442 2443lemma nat_mult_1_right: "n * 1 = n" 2444 for n :: nat 2445 by (fact mult_1_right) 2446 2447lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n" 2448 for k m n :: nat 2449 by (fact add_left_cancel) 2450 2451lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n" 2452 for k m n :: nat 2453 by (fact add_right_cancel) 2454 2455lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)" 2456 for k m n :: nat 2457 by (fact left_diff_distrib') 2458 2459lemma diff_mult_distrib2: "k * (m - n) = (k * m) - (k * n)" 2460 for k m n :: nat 2461 by (fact right_diff_distrib') 2462 2463lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k" 2464 for k m n :: nat 2465 by (fact le_add_diff) (* FIXME delete *) 2466 2467lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)" 2468 for i j k :: nat 2469 by (fact le_diff_conv2) (* FIXME delete *) 2470 2471lemma diff_self_eq_0 [simp]: "m - m = 0" 2472 for m :: nat 2473 by (fact diff_cancel) 2474 2475lemma diff_diff_left [simp]: "i - j - k = i - (j + k)" 2476 for i j k :: nat 2477 by (fact diff_diff_add) 2478 2479lemma diff_commute: "i - j - k = i - k - j" 2480 for i j k :: nat 2481 by (fact diff_right_commute) 2482 2483lemma diff_add_inverse: "(n + m) - n = m" 2484 for m n :: nat 2485 by (fact add_diff_cancel_left') 2486 2487lemma diff_add_inverse2: "(m + n) - n = m" 2488 for m n :: nat 2489 by (fact add_diff_cancel_right') 2490 2491lemma diff_cancel: "(k + m) - (k + n) = m - n" 2492 for k m n :: nat 2493 by (fact add_diff_cancel_left) 2494 2495lemma diff_cancel2: "(m + k) - (n + k) = m - n" 2496 for k m n :: nat 2497 by (fact add_diff_cancel_right) 2498 2499lemma diff_add_0: "n - (n + m) = 0" 2500 for m n :: nat 2501 by (fact diff_add_zero) 2502 2503lemma add_mult_distrib2: "k * (m + n) = (k * m) + (k * n)" 2504 for k m n :: nat 2505 by (fact distrib_left) 2506 2507lemmas nat_distrib = 2508 add_mult_distrib distrib_left diff_mult_distrib diff_mult_distrib2 2509 2510 2511subsection \<open>Size of a datatype value\<close> 2512 2513class size = 2514 fixes size :: "'a \<Rightarrow> nat" \<comment> \<open>see further theory \<open>Wellfounded\<close>\<close> 2515 2516instantiation nat :: size 2517begin 2518 2519definition size_nat where [simp, code]: "size (n::nat) = n" 2520 2521instance .. 2522 2523end 2524 2525lemmas size_nat = size_nat_def 2526 2527 2528subsection \<open>Code module namespace\<close> 2529 2530code_identifier 2531 code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 2532 2533hide_const (open) of_nat_aux 2534 2535end 2536