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