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