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