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