src/ZF/Nat_ZF.thy
 author wenzelm Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago) changeset 49566 66cbf8bb4693 parent 46954 d8b3412cdb99 child 58860 fee7cfa69c50 permissions -rw-r--r--
basic integration of graphview into document model;
 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@46953 ` 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 ``` paulson@46953 ` 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@46953 ` 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@46953 ` 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]: ``` paulson@46953 ` 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: ``` paulson@46935 ` 94` ``` assumes "n \ nat" ``` paulson@46954 ` 95` ``` obtains ("0") "n=0" | (succ) x where "x \ nat" "n=succ(x)" ``` paulson@46935 ` 96` ```using assms ``` paulson@46935 ` 97` ```by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto ``` krauss@26056 ` 98` paulson@46935 ` 99` ```lemma nat_into_Ord [simp]: "n \ nat ==> Ord(n)" ``` krauss@26056 ` 100` ```by (erule nat_induct, auto) ``` krauss@26056 ` 101` paulson@46953 ` 102` ```(* @{term"i \ nat ==> 0 \ i"}; same thing as @{term"0 nat ==> i \ i"}; same thing as @{term"i nat ==> ~ Limit(a)" ``` krauss@26056 ` 123` ```by (induct a rule: nat_induct, auto) ``` krauss@26056 ` 124` paulson@46953 ` 125` ```lemma succ_natD: "succ(i): nat ==> i \ nat" ``` krauss@26056 ` 126` ```by (rule Ord_trans [OF succI1], auto) ``` krauss@26056 ` 127` paulson@46935 ` 128` ```lemma nat_succ_iff [iff]: "succ(n): nat \ n \ nat" ``` krauss@26056 ` 129` ```by (blast dest!: succ_natD) ``` krauss@26056 ` 130` paulson@46820 ` 131` ```lemma nat_le_Limit: "Limit(i) ==> nat \ i" ``` krauss@26056 ` 132` ```apply (rule subset_imp_le) ``` paulson@46820 ` 133` ```apply (simp_all add: Limit_is_Ord) ``` krauss@26056 ` 134` ```apply (rule subsetI) ``` krauss@26056 ` 135` ```apply (erule nat_induct) ``` paulson@46820 ` 136` ``` apply (erule Limit_has_0 [THEN ltD]) ``` krauss@26056 ` 137` ```apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord) ``` krauss@26056 ` 138` ```done ``` krauss@26056 ` 139` paulson@46953 ` 140` ```(* [| succ(i): k; k \ nat |] ==> i \ k *) ``` krauss@26056 ` 141` ```lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord] ``` krauss@26056 ` 142` paulson@46953 ` 143` ```lemma lt_nat_in_nat: "[| m nat |] ==> m \ nat" ``` krauss@26056 ` 144` ```apply (erule ltE) ``` paulson@46820 ` 145` ```apply (erule Ord_trans, assumption, simp) ``` krauss@26056 ` 146` ```done ``` krauss@26056 ` 147` paulson@46953 ` 148` ```lemma le_in_nat: "[| m \ n; n \ nat |] ==> m \ nat" ``` krauss@26056 ` 149` ```by (blast dest!: lt_nat_in_nat) ``` krauss@26056 ` 150` krauss@26056 ` 151` krauss@26056 ` 152` ```subsection{*Variations on Mathematical Induction*} ``` krauss@26056 ` 153` krauss@26056 ` 154` ```(*complete induction*) ``` krauss@26056 ` 155` krauss@26056 ` 156` ```lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1] ``` krauss@26056 ` 157` paulson@46820 ` 158` ```lemmas complete_induct_rule = ``` wenzelm@32960 ` 159` ``` complete_induct [rule_format, case_names less, consumes 1] ``` krauss@26056 ` 160` krauss@26056 ` 161` paulson@46820 ` 162` ```lemma nat_induct_from_lemma [rule_format]: ``` paulson@46953 ` 163` ``` "[| n \ nat; m \ nat; ``` paulson@46953 ` 164` ``` !!x. [| x \ nat; m \ x; P(x) |] ==> P(succ(x)) |] ``` paulson@46820 ` 165` ``` ==> m \ n \ P(m) \ P(n)" ``` paulson@46820 ` 166` ```apply (erule nat_induct) ``` krauss@26056 ` 167` ```apply (simp_all add: distrib_simps le0_iff le_succ_iff) ``` krauss@26056 ` 168` ```done ``` krauss@26056 ` 169` krauss@26056 ` 170` ```(*Induction starting from m rather than 0*) ``` paulson@46820 ` 171` ```lemma nat_induct_from: ``` paulson@46953 ` 172` ``` "[| m \ n; m \ nat; n \ nat; ``` paulson@46820 ` 173` ``` P(m); ``` paulson@46953 ` 174` ``` !!x. [| x \ nat; m \ x; P(x) |] ==> P(succ(x)) |] ``` krauss@26056 ` 175` ``` ==> P(n)" ``` krauss@26056 ` 176` ```apply (blast intro: nat_induct_from_lemma) ``` krauss@26056 ` 177` ```done ``` krauss@26056 ` 178` krauss@26056 ` 179` ```(*Induction suitable for subtraction and less-than*) ``` krauss@26056 ` 180` ```lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]: ``` paulson@46953 ` 181` ``` "[| m \ nat; n \ nat; ``` paulson@46953 ` 182` ``` !!x. x \ nat ==> P(x,0); ``` paulson@46953 ` 183` ``` !!y. y \ nat ==> P(0,succ(y)); ``` paulson@46953 ` 184` ``` !!x y. [| x \ nat; y \ nat; P(x,y) |] ==> P(succ(x),succ(y)) |] ``` krauss@26056 ` 185` ``` ==> P(m,n)" ``` krauss@26056 ` 186` ```apply (erule_tac x = m in rev_bspec) ``` paulson@46820 ` 187` ```apply (erule nat_induct, simp) ``` krauss@26056 ` 188` ```apply (rule ballI) ``` krauss@26056 ` 189` ```apply (rename_tac i j) ``` paulson@46820 ` 190` ```apply (erule_tac n=j in nat_induct, auto) ``` krauss@26056 ` 191` ```done ``` krauss@26056 ` 192` krauss@26056 ` 193` krauss@26056 ` 194` ```(** Induction principle analogous to trancl_induct **) ``` krauss@26056 ` 195` krauss@26056 ` 196` ```lemma succ_lt_induct_lemma [rule_format]: ``` paulson@46953 ` 197` ``` "m \ nat ==> P(m,succ(m)) \ (\x\nat. P(m,x) \ P(m,succ(x))) \ ``` paulson@46820 ` 198` ``` (\n\nat. m P(m,n))" ``` krauss@26056 ` 199` ```apply (erule nat_induct) ``` krauss@26056 ` 200` ``` apply (intro impI, rule nat_induct [THEN ballI]) ``` krauss@26056 ` 201` ``` prefer 4 apply (intro impI, rule nat_induct [THEN ballI]) ``` paulson@46820 ` 202` ```apply (auto simp add: le_iff) ``` krauss@26056 ` 203` ```done ``` krauss@26056 ` 204` krauss@26056 ` 205` ```lemma succ_lt_induct: ``` paulson@46935 ` 206` ``` "[| m nat; ``` paulson@46820 ` 207` ``` P(m,succ(m)); ``` paulson@46953 ` 208` ``` !!x. [| x \ nat; P(m,x) |] ==> P(m,succ(x)) |] ``` krauss@26056 ` 209` ``` ==> P(m,n)" ``` paulson@46820 ` 210` ```by (blast intro: succ_lt_induct_lemma lt_nat_in_nat) ``` krauss@26056 ` 211` krauss@26056 ` 212` ```subsection{*quasinat: to allow a case-split rule for @{term nat_case}*} ``` krauss@26056 ` 213` krauss@26056 ` 214` ```text{*True if the argument is zero or any successor*} ``` krauss@26056 ` 215` ```lemma [iff]: "quasinat(0)" ``` krauss@26056 ` 216` ```by (simp add: quasinat_def) ``` krauss@26056 ` 217` krauss@26056 ` 218` ```lemma [iff]: "quasinat(succ(x))" ``` krauss@26056 ` 219` ```by (simp add: quasinat_def) ``` krauss@26056 ` 220` krauss@26056 ` 221` ```lemma nat_imp_quasinat: "n \ nat ==> quasinat(n)" ``` krauss@26056 ` 222` ```by (erule natE, simp_all) ``` krauss@26056 ` 223` paulson@46820 ` 224` ```lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0" ``` paulson@46820 ` 225` ```by (simp add: quasinat_def nat_case_def) ``` krauss@26056 ` 226` krauss@26056 ` 227` ```lemma nat_cases_disj: "k=0 | (\y. k = succ(y)) | ~ quasinat(k)" ``` paulson@46820 ` 228` ```apply (case_tac "k=0", simp) ``` paulson@46820 ` 229` ```apply (case_tac "\m. k = succ(m)") ``` paulson@46820 ` 230` ```apply (simp_all add: quasinat_def) ``` krauss@26056 ` 231` ```done ``` krauss@26056 ` 232` krauss@26056 ` 233` ```lemma nat_cases: ``` krauss@26056 ` 234` ``` "[|k=0 ==> P; !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P" ``` paulson@46820 ` 235` ```by (insert nat_cases_disj [of k], blast) ``` krauss@26056 ` 236` krauss@26056 ` 237` ```(** nat_case **) ``` krauss@26056 ` 238` krauss@26056 ` 239` ```lemma nat_case_0 [simp]: "nat_case(a,b,0) = a" ``` krauss@26056 ` 240` ```by (simp add: nat_case_def) ``` krauss@26056 ` 241` paulson@46820 ` 242` ```lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)" ``` krauss@26056 ` 243` ```by (simp add: nat_case_def) ``` krauss@26056 ` 244` krauss@26056 ` 245` ```lemma nat_case_type [TC]: ``` paulson@46953 ` 246` ``` "[| n \ nat; a \ C(0); !!m. m \ nat ==> b(m): C(succ(m)) |] ``` paulson@46820 ` 247` ``` ==> nat_case(a,b,n) \ C(n)"; ``` paulson@46820 ` 248` ```by (erule nat_induct, auto) ``` krauss@26056 ` 249` krauss@26056 ` 250` ```lemma split_nat_case: ``` paulson@46821 ` 251` ``` "P(nat_case(a,b,k)) \ ``` paulson@46820 ` 252` ``` ((k=0 \ P(a)) & (\x. k=succ(x) \ P(b(x))) & (~ quasinat(k) \ P(0)))" ``` paulson@46820 ` 253` ```apply (rule nat_cases [of k]) ``` krauss@26056 ` 254` ```apply (auto simp add: non_nat_case) ``` krauss@26056 ` 255` ```done ``` krauss@26056 ` 256` krauss@26056 ` 257` krauss@26056 ` 258` ```subsection{*Recursion on the Natural Numbers*} ``` krauss@26056 ` 259` krauss@26056 ` 260` ```(** nat_rec is used to define eclose and transrec, then becomes obsolete. ``` krauss@26056 ` 261` ``` The operator rec, from arith.thy, has fewer typing conditions **) ``` krauss@26056 ` 262` krauss@26056 ` 263` ```lemma nat_rec_0: "nat_rec(0,a,b) = a" ``` krauss@26056 ` 264` ```apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) ``` paulson@46820 ` 265` ``` apply (rule wf_Memrel) ``` krauss@26056 ` 266` ```apply (rule nat_case_0) ``` krauss@26056 ` 267` ```done ``` krauss@26056 ` 268` paulson@46953 ` 269` ```lemma nat_rec_succ: "m \ nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))" ``` krauss@26056 ` 270` ```apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) ``` paulson@46820 ` 271` ``` apply (rule wf_Memrel) ``` krauss@26056 ` 272` ```apply (simp add: vimage_singleton_iff) ``` krauss@26056 ` 273` ```done ``` krauss@26056 ` 274` krauss@26056 ` 275` ```(** The union of two natural numbers is a natural number -- their maximum **) ``` krauss@26056 ` 276` paulson@46953 ` 277` ```lemma Un_nat_type [TC]: "[| i \ nat; j \ nat |] ==> i \ j \ nat" ``` krauss@26056 ` 278` ```apply (rule Un_least_lt [THEN ltD]) ``` paulson@46820 ` 279` ```apply (simp_all add: lt_def) ``` krauss@26056 ` 280` ```done ``` krauss@26056 ` 281` paulson@46953 ` 282` ```lemma Int_nat_type [TC]: "[| i \ nat; j \ nat |] ==> i \ j \ nat" ``` krauss@26056 ` 283` ```apply (rule Int_greatest_lt [THEN ltD]) ``` paulson@46820 ` 284` ```apply (simp_all add: lt_def) ``` krauss@26056 ` 285` ```done ``` krauss@26056 ` 286` krauss@26056 ` 287` ```(*needed to simplify unions over nat*) ``` paulson@46820 ` 288` ```lemma nat_nonempty [simp]: "nat \ 0" ``` krauss@26056 ` 289` ```by blast ``` krauss@26056 ` 290` krauss@26056 ` 291` ```text{*A natural number is the set of its predecessors*} ``` krauss@26056 ` 292` ```lemma nat_eq_Collect_lt: "i \ nat ==> {j\nat. j \ Le \ x \ y & x \ nat & y \ nat" ``` krauss@26056 ` 300` ```by (force simp add: Le_def) ``` krauss@26056 ` 301` krauss@26056 ` 302` ```end ```