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