src/ZF/Nat.thy
 author wenzelm Tue Jul 31 19:40:22 2007 +0200 (2007-07-31) changeset 24091 109f19a13872 parent 16417 9bc16273c2d4 child 24893 b8ef7afe3a6b permissions -rw-r--r--
 clasohm@1478 ` 1` ```(* Title: ZF/Nat.thy ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@1478 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@435 ` 4` ``` Copyright 1994 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```*) ``` clasohm@0 ` 7` paulson@13356 ` 8` ```header{*The Natural numbers As a Least Fixed Point*} ``` paulson@13356 ` 9` haftmann@16417 ` 10` ```theory Nat imports OrdQuant Bool begin ``` clasohm@0 ` 11` paulson@12789 ` 12` ```constdefs ``` paulson@12789 ` 13` ``` nat :: i ``` paulson@12789 ` 14` ``` "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})" ``` clasohm@0 ` 15` paulson@13269 ` 16` ``` quasinat :: "i => o" ``` paulson@13269 ` 17` ``` "quasinat(n) == n=0 | (\m. n = succ(m))" ``` paulson@13269 ` 18` paulson@13173 ` 19` ``` (*Has an unconditional succ case, which is used in "recursor" below.*) ``` paulson@12789 ` 20` ``` nat_case :: "[i, i=>i, i]=>i" ``` paulson@12789 ` 21` ``` "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))" ``` clasohm@0 ` 22` paulson@12789 ` 23` ``` nat_rec :: "[i, i, [i,i]=>i]=>i" ``` paulson@12789 ` 24` ``` "nat_rec(k,a,b) == ``` clasohm@1478 ` 25` ``` wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))" ``` clasohm@0 ` 26` paulson@12789 ` 27` ``` (*Internalized relations on the naturals*) ``` paulson@12789 ` 28` ``` ``` paulson@12789 ` 29` ``` Le :: i ``` paulson@12789 ` 30` ``` "Le == {:nat*nat. x le y}" ``` paulson@12789 ` 31` paulson@12789 ` 32` ``` Lt :: i ``` paulson@12789 ` 33` ``` "Lt == {:nat*nat. x < y}" ``` paulson@12789 ` 34` ``` ``` paulson@12789 ` 35` ``` Ge :: i ``` paulson@12789 ` 36` ``` "Ge == {:nat*nat. y le x}" ``` paulson@12789 ` 37` paulson@12789 ` 38` ``` Gt :: i ``` paulson@12789 ` 39` ``` "Gt == {:nat*nat. y < x}" ``` paulson@12789 ` 40` paulson@13171 ` 41` ``` greater_than :: "i=>i" ``` paulson@12789 ` 42` ``` "greater_than(n) == {i:nat. n < i}" ``` paulson@12789 ` 43` paulson@14046 ` 44` ```text{*No need for a less-than operator: a natural number is its list of ``` paulson@14046 ` 45` ```predecessors!*} ``` paulson@14046 ` 46` paulson@14046 ` 47` paulson@13171 ` 48` ```lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})" ``` paulson@13171 ` 49` ```apply (rule bnd_monoI) ``` paulson@13269 ` 50` ```apply (cut_tac infinity, blast, blast) ``` paulson@13171 ` 51` ```done ``` paulson@13171 ` 52` paulson@13171 ` 53` ```(* nat = {0} Un {succ(x). x:nat} *) ``` paulson@13171 ` 54` ```lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard] ``` paulson@13171 ` 55` paulson@13171 ` 56` ```(** Type checking of 0 and successor **) ``` paulson@13171 ` 57` paulson@13171 ` 58` ```lemma nat_0I [iff,TC]: "0 : nat" ``` paulson@13171 ` 59` ```apply (subst nat_unfold) ``` paulson@13171 ` 60` ```apply (rule singletonI [THEN UnI1]) ``` paulson@13171 ` 61` ```done ``` paulson@13171 ` 62` paulson@13171 ` 63` ```lemma nat_succI [intro!,TC]: "n : nat ==> succ(n) : nat" ``` paulson@13171 ` 64` ```apply (subst nat_unfold) ``` paulson@13171 ` 65` ```apply (erule RepFunI [THEN UnI2]) ``` paulson@13171 ` 66` ```done ``` paulson@13171 ` 67` paulson@13171 ` 68` ```lemma nat_1I [iff,TC]: "1 : nat" ``` paulson@13171 ` 69` ```by (rule nat_0I [THEN nat_succI]) ``` paulson@13171 ` 70` paulson@13171 ` 71` ```lemma nat_2I [iff,TC]: "2 : nat" ``` paulson@13171 ` 72` ```by (rule nat_1I [THEN nat_succI]) ``` paulson@13171 ` 73` paulson@13171 ` 74` ```lemma bool_subset_nat: "bool <= nat" ``` paulson@13171 ` 75` ```by (blast elim!: boolE) ``` paulson@13171 ` 76` paulson@13171 ` 77` ```lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard] ``` paulson@13171 ` 78` paulson@13171 ` 79` paulson@13356 ` 80` ```subsection{*Injectivity Properties and Induction*} ``` paulson@13171 ` 81` paulson@13171 ` 82` ```(*Mathematical induction*) ``` wenzelm@13524 ` 83` ```lemma nat_induct [case_names 0 succ, induct set: nat]: ``` paulson@13171 ` 84` ``` "[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)" ``` paulson@13203 ` 85` ```by (erule def_induct [OF nat_def nat_bnd_mono], blast) ``` paulson@13203 ` 86` paulson@13171 ` 87` ```lemma natE: ``` paulson@13171 ` 88` ``` "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P" ``` paulson@13203 ` 89` ```by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) ``` paulson@13171 ` 90` paulson@13171 ` 91` ```lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)" ``` paulson@13171 ` 92` ```by (erule nat_induct, auto) ``` paulson@13171 ` 93` paulson@13171 ` 94` ```(* i: nat ==> 0 le i; same thing as 0 i le i; same thing as i nat ==> ~ Limit(a)" ``` paulson@13628 ` 115` ```by (induct a rule: nat_induct, auto) ``` paulson@13628 ` 116` paulson@13823 ` 117` ```lemma succ_natD: "succ(i): nat ==> i: nat" ``` paulson@13171 ` 118` ```by (rule Ord_trans [OF succI1], auto) ``` paulson@13171 ` 119` paulson@13171 ` 120` ```lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat" ``` paulson@13823 ` 121` ```by (blast dest!: succ_natD) ``` paulson@13171 ` 122` paulson@13171 ` 123` ```lemma nat_le_Limit: "Limit(i) ==> nat le i" ``` paulson@13171 ` 124` ```apply (rule subset_imp_le) ``` paulson@13171 ` 125` ```apply (simp_all add: Limit_is_Ord) ``` paulson@13171 ` 126` ```apply (rule subsetI) ``` paulson@13171 ` 127` ```apply (erule nat_induct) ``` paulson@13171 ` 128` ``` apply (erule Limit_has_0 [THEN ltD]) ``` paulson@13171 ` 129` ```apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord) ``` paulson@13171 ` 130` ```done ``` paulson@13171 ` 131` paulson@13171 ` 132` ```(* [| succ(i): k; k: nat |] ==> i: k *) ``` paulson@13171 ` 133` ```lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord] ``` paulson@13171 ` 134` paulson@13171 ` 135` ```lemma lt_nat_in_nat: "[| m m: nat" ``` paulson@13171 ` 136` ```apply (erule ltE) ``` paulson@13269 ` 137` ```apply (erule Ord_trans, assumption, simp) ``` paulson@13171 ` 138` ```done ``` paulson@13171 ` 139` paulson@13171 ` 140` ```lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat" ``` paulson@13171 ` 141` ```by (blast dest!: lt_nat_in_nat) ``` paulson@13171 ` 142` paulson@13171 ` 143` paulson@13356 ` 144` ```subsection{*Variations on Mathematical Induction*} ``` paulson@13171 ` 145` paulson@13171 ` 146` ```(*complete induction*) ``` paulson@13203 ` 147` paulson@13203 ` 148` ```lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1] ``` paulson@13203 ` 149` paulson@13203 ` 150` ```lemmas complete_induct_rule = ``` paulson@13203 ` 151` ``` complete_induct [rule_format, case_names less, consumes 1] ``` paulson@13203 ` 152` paulson@13171 ` 153` paulson@13171 ` 154` ```lemma nat_induct_from_lemma [rule_format]: ``` paulson@13171 ` 155` ``` "[| n: nat; m: nat; ``` paulson@13171 ` 156` ``` !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |] ``` paulson@13171 ` 157` ``` ==> m le n --> P(m) --> P(n)" ``` paulson@13171 ` 158` ```apply (erule nat_induct) ``` paulson@13171 ` 159` ```apply (simp_all add: distrib_simps le0_iff le_succ_iff) ``` paulson@13171 ` 160` ```done ``` paulson@13171 ` 161` paulson@13171 ` 162` ```(*Induction starting from m rather than 0*) ``` paulson@13171 ` 163` ```lemma nat_induct_from: ``` paulson@13171 ` 164` ``` "[| m le n; m: nat; n: nat; ``` paulson@13171 ` 165` ``` P(m); ``` paulson@13171 ` 166` ``` !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |] ``` paulson@13171 ` 167` ``` ==> P(n)" ``` paulson@13171 ` 168` ```apply (blast intro: nat_induct_from_lemma) ``` paulson@13171 ` 169` ```done ``` paulson@13171 ` 170` paulson@13171 ` 171` ```(*Induction suitable for subtraction and less-than*) ``` wenzelm@13524 ` 172` ```lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]: ``` paulson@13171 ` 173` ``` "[| m: nat; n: nat; ``` paulson@13171 ` 174` ``` !!x. x: nat ==> P(x,0); ``` paulson@13171 ` 175` ``` !!y. y: nat ==> P(0,succ(y)); ``` paulson@13171 ` 176` ``` !!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) |] ``` paulson@13171 ` 177` ``` ==> P(m,n)" ``` paulson@13784 ` 178` ```apply (erule_tac x = m in rev_bspec) ``` paulson@13171 ` 179` ```apply (erule nat_induct, simp) ``` paulson@13171 ` 180` ```apply (rule ballI) ``` paulson@13171 ` 181` ```apply (rename_tac i j) ``` paulson@13171 ` 182` ```apply (erule_tac n=j in nat_induct, auto) ``` paulson@13171 ` 183` ```done ``` paulson@13171 ` 184` paulson@13203 ` 185` paulson@13171 ` 186` ```(** Induction principle analogous to trancl_induct **) ``` paulson@13171 ` 187` paulson@13171 ` 188` ```lemma succ_lt_induct_lemma [rule_format]: ``` paulson@13171 ` 189` ``` "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> ``` paulson@13171 ` 190` ``` (ALL n:nat. m P(m,n))" ``` paulson@13171 ` 191` ```apply (erule nat_induct) ``` paulson@13171 ` 192` ``` apply (intro impI, rule nat_induct [THEN ballI]) ``` paulson@13171 ` 193` ``` prefer 4 apply (intro impI, rule nat_induct [THEN ballI]) ``` paulson@13171 ` 194` ```apply (auto simp add: le_iff) ``` paulson@13171 ` 195` ```done ``` paulson@13171 ` 196` paulson@13171 ` 197` ```lemma succ_lt_induct: ``` paulson@13171 ` 198` ``` "[| m P(m,succ(x)) |] ``` paulson@13171 ` 201` ``` ==> P(m,n)" ``` paulson@13171 ` 202` ```by (blast intro: succ_lt_induct_lemma lt_nat_in_nat) ``` paulson@13171 ` 203` paulson@13269 ` 204` ```subsection{*quasinat: to allow a case-split rule for @{term nat_case}*} ``` paulson@13269 ` 205` paulson@13269 ` 206` ```text{*True if the argument is zero or any successor*} ``` paulson@13269 ` 207` ```lemma [iff]: "quasinat(0)" ``` paulson@13269 ` 208` ```by (simp add: quasinat_def) ``` paulson@13269 ` 209` paulson@13269 ` 210` ```lemma [iff]: "quasinat(succ(x))" ``` paulson@13269 ` 211` ```by (simp add: quasinat_def) ``` paulson@13269 ` 212` paulson@13269 ` 213` ```lemma nat_imp_quasinat: "n \ nat ==> quasinat(n)" ``` paulson@13269 ` 214` ```by (erule natE, simp_all) ``` paulson@13269 ` 215` paulson@13269 ` 216` ```lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0" ``` paulson@13269 ` 217` ```by (simp add: quasinat_def nat_case_def) ``` paulson@13269 ` 218` paulson@13269 ` 219` ```lemma nat_cases_disj: "k=0 | (\y. k = succ(y)) | ~ quasinat(k)" ``` paulson@14153 ` 220` ```apply (case_tac "k=0", simp) ``` paulson@14153 ` 221` ```apply (case_tac "\m. k = succ(m)") ``` paulson@14153 ` 222` ```apply (simp_all add: quasinat_def) ``` paulson@13269 ` 223` ```done ``` paulson@13269 ` 224` paulson@13269 ` 225` ```lemma nat_cases: ``` paulson@13269 ` 226` ``` "[|k=0 ==> P; !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P" ``` paulson@13356 ` 227` ```by (insert nat_cases_disj [of k], blast) ``` paulson@13269 ` 228` paulson@13171 ` 229` ```(** nat_case **) ``` paulson@13171 ` 230` paulson@13171 ` 231` ```lemma nat_case_0 [simp]: "nat_case(a,b,0) = a" ``` paulson@13174 ` 232` ```by (simp add: nat_case_def) ``` paulson@13173 ` 233` paulson@13173 ` 234` ```lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)" ``` paulson@13174 ` 235` ```by (simp add: nat_case_def) ``` paulson@13171 ` 236` paulson@13173 ` 237` ```lemma nat_case_type [TC]: ``` paulson@13173 ` 238` ``` "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |] ``` paulson@13173 ` 239` ``` ==> nat_case(a,b,n) : C(n)"; ``` paulson@13173 ` 240` ```by (erule nat_induct, auto) ``` paulson@13173 ` 241` paulson@13269 ` 242` ```lemma split_nat_case: ``` paulson@13269 ` 243` ``` "P(nat_case(a,b,k)) <-> ``` paulson@13269 ` 244` ``` ((k=0 --> P(a)) & (\x. k=succ(x) --> P(b(x))) & (~ quasinat(k) \ P(0)))" ``` paulson@13269 ` 245` ```apply (rule nat_cases [of k]) ``` paulson@13269 ` 246` ```apply (auto simp add: non_nat_case) ``` paulson@13171 ` 247` ```done ``` paulson@13171 ` 248` paulson@13173 ` 249` paulson@13356 ` 250` ```subsection{*Recursion on the Natural Numbers*} ``` paulson@13171 ` 251` paulson@13356 ` 252` ```(** nat_rec is used to define eclose and transrec, then becomes obsolete. ``` paulson@13356 ` 253` ``` The operator rec, from arith.thy, has fewer typing conditions **) ``` paulson@13171 ` 254` paulson@13171 ` 255` ```lemma nat_rec_0: "nat_rec(0,a,b) = a" ``` paulson@13171 ` 256` ```apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) ``` paulson@13171 ` 257` ``` apply (rule wf_Memrel) ``` paulson@13171 ` 258` ```apply (rule nat_case_0) ``` paulson@13171 ` 259` ```done ``` paulson@13171 ` 260` paulson@13171 ` 261` ```lemma nat_rec_succ: "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))" ``` paulson@13171 ` 262` ```apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) ``` paulson@13171 ` 263` ``` apply (rule wf_Memrel) ``` paulson@13171 ` 264` ```apply (simp add: vimage_singleton_iff) ``` paulson@13171 ` 265` ```done ``` paulson@13171 ` 266` paulson@13171 ` 267` ```(** The union of two natural numbers is a natural number -- their maximum **) ``` paulson@13171 ` 268` paulson@13173 ` 269` ```lemma Un_nat_type [TC]: "[| i: nat; j: nat |] ==> i Un j: nat" ``` paulson@13171 ` 270` ```apply (rule Un_least_lt [THEN ltD]) ``` paulson@13171 ` 271` ```apply (simp_all add: lt_def) ``` paulson@13171 ` 272` ```done ``` paulson@13171 ` 273` paulson@13173 ` 274` ```lemma Int_nat_type [TC]: "[| i: nat; j: nat |] ==> i Int j: nat" ``` paulson@13171 ` 275` ```apply (rule Int_greatest_lt [THEN ltD]) ``` paulson@13171 ` 276` ```apply (simp_all add: lt_def) ``` paulson@13171 ` 277` ```done ``` paulson@13171 ` 278` paulson@13171 ` 279` ```(*needed to simplify unions over nat*) ``` paulson@13171 ` 280` ```lemma nat_nonempty [simp]: "nat ~= 0" ``` paulson@13171 ` 281` ```by blast ``` paulson@13171 ` 282` paulson@14046 ` 283` ```text{*A natural number is the set of its predecessors*} ``` paulson@14046 ` 284` ```lemma nat_eq_Collect_lt: "i \ nat ==> {j\nat. j : Le <-> x le y & x : nat & y : nat" ``` paulson@14054 ` 292` ```by (force simp add: Le_def) ``` paulson@13203 ` 293` paulson@13171 ` 294` ```ML ``` paulson@13171 ` 295` ```{* ``` paulson@13171 ` 296` ```val Le_def = thm "Le_def"; ``` paulson@13171 ` 297` ```val Lt_def = thm "Lt_def"; ``` paulson@13171 ` 298` ```val Ge_def = thm "Ge_def"; ``` paulson@13171 ` 299` ```val Gt_def = thm "Gt_def"; ``` paulson@13171 ` 300` ```val greater_than_def = thm "greater_than_def"; ``` paulson@13171 ` 301` paulson@13171 ` 302` ```val nat_bnd_mono = thm "nat_bnd_mono"; ``` paulson@13171 ` 303` ```val nat_unfold = thm "nat_unfold"; ``` paulson@13171 ` 304` ```val nat_0I = thm "nat_0I"; ``` paulson@13171 ` 305` ```val nat_succI = thm "nat_succI"; ``` paulson@13171 ` 306` ```val nat_1I = thm "nat_1I"; ``` paulson@13171 ` 307` ```val nat_2I = thm "nat_2I"; ``` paulson@13171 ` 308` ```val bool_subset_nat = thm "bool_subset_nat"; ``` paulson@13171 ` 309` ```val bool_into_nat = thm "bool_into_nat"; ``` paulson@13171 ` 310` ```val nat_induct = thm "nat_induct"; ``` paulson@13171 ` 311` ```val natE = thm "natE"; ``` paulson@13171 ` 312` ```val nat_into_Ord = thm "nat_into_Ord"; ``` paulson@13171 ` 313` ```val nat_0_le = thm "nat_0_le"; ``` paulson@13171 ` 314` ```val nat_le_refl = thm "nat_le_refl"; ``` paulson@13171 ` 315` ```val Ord_nat = thm "Ord_nat"; ``` paulson@13171 ` 316` ```val Limit_nat = thm "Limit_nat"; ``` paulson@13171 ` 317` ```val succ_natD = thm "succ_natD"; ``` paulson@13171 ` 318` ```val nat_succ_iff = thm "nat_succ_iff"; ``` paulson@13171 ` 319` ```val nat_le_Limit = thm "nat_le_Limit"; ``` paulson@13171 ` 320` ```val succ_in_naturalD = thm "succ_in_naturalD"; ``` paulson@13171 ` 321` ```val lt_nat_in_nat = thm "lt_nat_in_nat"; ``` paulson@13171 ` 322` ```val le_in_nat = thm "le_in_nat"; ``` paulson@13171 ` 323` ```val complete_induct = thm "complete_induct"; ``` paulson@13171 ` 324` ```val nat_induct_from = thm "nat_induct_from"; ``` paulson@13171 ` 325` ```val diff_induct = thm "diff_induct"; ``` paulson@13171 ` 326` ```val succ_lt_induct = thm "succ_lt_induct"; ``` paulson@13171 ` 327` ```val nat_case_0 = thm "nat_case_0"; ``` paulson@13171 ` 328` ```val nat_case_succ = thm "nat_case_succ"; ``` paulson@13171 ` 329` ```val nat_case_type = thm "nat_case_type"; ``` paulson@13171 ` 330` ```val nat_rec_0 = thm "nat_rec_0"; ``` paulson@13171 ` 331` ```val nat_rec_succ = thm "nat_rec_succ"; ``` paulson@13171 ` 332` ```val Un_nat_type = thm "Un_nat_type"; ``` paulson@13171 ` 333` ```val Int_nat_type = thm "Int_nat_type"; ``` paulson@13171 ` 334` ```val nat_nonempty = thm "nat_nonempty"; ``` paulson@13171 ` 335` ```*} ``` paulson@13171 ` 336` clasohm@0 ` 337` ```end ```