src/ZF/Nat_ZF.thy
author paulson
Tue Mar 06 15:15:49 2012 +0000 (2012-03-06)
changeset 46820 c656222c4dc1
parent 45602 2a858377c3d2
child 46821 ff6b0c1087f2
permissions -rw-r--r--
mathematical symbols instead of ASCII
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@46820
    12
    "nat == lfp(Inf, %X. {0} \<union> {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 | (\<exists>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 | (\<exists>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 == {<x,y>:nat*nat. x \<le> y}"
krauss@26056
    33
krauss@26056
    34
definition
krauss@26056
    35
  Lt :: i  where
krauss@26056
    36
    "Lt == {<x, y>:nat*nat. x < y}"
paulson@46820
    37
krauss@26056
    38
definition
krauss@26056
    39
  Ge :: i  where
paulson@46820
    40
    "Ge == {<x,y>:nat*nat. y \<le> x}"
krauss@26056
    41
krauss@26056
    42
definition
krauss@26056
    43
  Gt :: i  where
krauss@26056
    44
    "Gt == {<x,y>:nat*nat. y < x}"
krauss@26056
    45
krauss@26056
    46
definition
krauss@26056
    47
  greater_than :: "i=>i"  where
krauss@26056
    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@46820
    54
lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} \<union> {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@46820
    59
(* @{term"nat = {0} \<union> {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 \<in> 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 \<in> nat ==> succ(n) \<in> 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 \<in> nat"
krauss@26056
    75
by (rule nat_0I [THEN nat_succI])
krauss@26056
    76
paulson@46820
    77
lemma nat_2I [iff,TC]: "2 \<in> nat"
krauss@26056
    78
by (rule nat_1I [THEN nat_succI])
krauss@26056
    79
paulson@46820
    80
lemma bool_subset_nat: "bool \<subseteq> 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]:
krauss@26056
    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:
krauss@26056
    94
    "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
paulson@46820
    95
by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
krauss@26056
    96
krauss@26056
    97
lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
krauss@26056
    98
by (erule nat_induct, auto)
krauss@26056
    99
paulson@46820
   100
(* @{term"i: nat ==> 0 \<le> i"}; same thing as @{term"0<succ(i)"}  *)
wenzelm@45602
   101
lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le]
krauss@26056
   102
paulson@46820
   103
(* @{term"i: nat ==> i \<le> i"}; same thing as @{term"i<succ(i)"}  *)
wenzelm@45602
   104
lemmas nat_le_refl = nat_into_Ord [THEN le_refl]
krauss@26056
   105
krauss@26056
   106
lemma Ord_nat [iff]: "Ord(nat)"
krauss@26056
   107
apply (rule OrdI)
krauss@26056
   108
apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
krauss@26056
   109
apply (unfold Transset_def)
krauss@26056
   110
apply (rule ballI)
paulson@46820
   111
apply (erule nat_induct, auto)
krauss@26056
   112
done
krauss@26056
   113
krauss@26056
   114
lemma Limit_nat [iff]: "Limit(nat)"
krauss@26056
   115
apply (unfold Limit_def)
krauss@26056
   116
apply (safe intro!: ltI Ord_nat)
krauss@26056
   117
apply (erule ltD)
krauss@26056
   118
done
krauss@26056
   119
krauss@26056
   120
lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
krauss@26056
   121
by (induct a rule: nat_induct, auto)
krauss@26056
   122
krauss@26056
   123
lemma succ_natD: "succ(i): nat ==> i: nat"
krauss@26056
   124
by (rule Ord_trans [OF succI1], auto)
krauss@26056
   125
krauss@26056
   126
lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
krauss@26056
   127
by (blast dest!: succ_natD)
krauss@26056
   128
paulson@46820
   129
lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
krauss@26056
   130
apply (rule subset_imp_le)
paulson@46820
   131
apply (simp_all add: Limit_is_Ord)
krauss@26056
   132
apply (rule subsetI)
krauss@26056
   133
apply (erule nat_induct)
paulson@46820
   134
 apply (erule Limit_has_0 [THEN ltD])
krauss@26056
   135
apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord)
krauss@26056
   136
done
krauss@26056
   137
krauss@26056
   138
(* [| succ(i): k;  k: nat |] ==> i: k *)
krauss@26056
   139
lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
krauss@26056
   140
krauss@26056
   141
lemma lt_nat_in_nat: "[| m<n;  n: nat |] ==> m: nat"
krauss@26056
   142
apply (erule ltE)
paulson@46820
   143
apply (erule Ord_trans, assumption, simp)
krauss@26056
   144
done
krauss@26056
   145
paulson@46820
   146
lemma le_in_nat: "[| m \<le> n; n:nat |] ==> m:nat"
krauss@26056
   147
by (blast dest!: lt_nat_in_nat)
krauss@26056
   148
krauss@26056
   149
krauss@26056
   150
subsection{*Variations on Mathematical Induction*}
krauss@26056
   151
krauss@26056
   152
(*complete induction*)
krauss@26056
   153
krauss@26056
   154
lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]
krauss@26056
   155
paulson@46820
   156
lemmas complete_induct_rule =
wenzelm@32960
   157
        complete_induct [rule_format, case_names less, consumes 1]
krauss@26056
   158
krauss@26056
   159
paulson@46820
   160
lemma nat_induct_from_lemma [rule_format]:
paulson@46820
   161
    "[| n: nat;  m: nat;
paulson@46820
   162
        !!x. [| x: nat;  m \<le> x;  P(x) |] ==> P(succ(x)) |]
paulson@46820
   163
     ==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
paulson@46820
   164
apply (erule nat_induct)
krauss@26056
   165
apply (simp_all add: distrib_simps le0_iff le_succ_iff)
krauss@26056
   166
done
krauss@26056
   167
krauss@26056
   168
(*Induction starting from m rather than 0*)
paulson@46820
   169
lemma nat_induct_from:
paulson@46820
   170
    "[| m \<le> n;  m: nat;  n: nat;
paulson@46820
   171
        P(m);
paulson@46820
   172
        !!x. [| x: nat;  m \<le> x;  P(x) |] ==> P(succ(x)) |]
krauss@26056
   173
     ==> P(n)"
krauss@26056
   174
apply (blast intro: nat_induct_from_lemma)
krauss@26056
   175
done
krauss@26056
   176
krauss@26056
   177
(*Induction suitable for subtraction and less-than*)
krauss@26056
   178
lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
paulson@46820
   179
    "[| m: nat;  n: nat;
paulson@46820
   180
        !!x. x: nat ==> P(x,0);
paulson@46820
   181
        !!y. y: nat ==> P(0,succ(y));
krauss@26056
   182
        !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
krauss@26056
   183
     ==> P(m,n)"
krauss@26056
   184
apply (erule_tac x = m in rev_bspec)
paulson@46820
   185
apply (erule nat_induct, simp)
krauss@26056
   186
apply (rule ballI)
krauss@26056
   187
apply (rename_tac i j)
paulson@46820
   188
apply (erule_tac n=j in nat_induct, auto)
krauss@26056
   189
done
krauss@26056
   190
krauss@26056
   191
krauss@26056
   192
(** Induction principle analogous to trancl_induct **)
krauss@26056
   193
krauss@26056
   194
lemma succ_lt_induct_lemma [rule_format]:
paulson@46820
   195
     "m: nat ==> P(m,succ(m)) \<longrightarrow> (\<forall>x\<in>nat. P(m,x) \<longrightarrow> P(m,succ(x))) \<longrightarrow>
paulson@46820
   196
                 (\<forall>n\<in>nat. m<n \<longrightarrow> P(m,n))"
krauss@26056
   197
apply (erule nat_induct)
krauss@26056
   198
 apply (intro impI, rule nat_induct [THEN ballI])
krauss@26056
   199
   prefer 4 apply (intro impI, rule nat_induct [THEN ballI])
paulson@46820
   200
apply (auto simp add: le_iff)
krauss@26056
   201
done
krauss@26056
   202
krauss@26056
   203
lemma succ_lt_induct:
paulson@46820
   204
    "[| m<n;  n: nat;
paulson@46820
   205
        P(m,succ(m));
krauss@26056
   206
        !!x. [| x: nat;  P(m,x) |] ==> P(m,succ(x)) |]
krauss@26056
   207
     ==> P(m,n)"
paulson@46820
   208
by (blast intro: succ_lt_induct_lemma lt_nat_in_nat)
krauss@26056
   209
krauss@26056
   210
subsection{*quasinat: to allow a case-split rule for @{term nat_case}*}
krauss@26056
   211
krauss@26056
   212
text{*True if the argument is zero or any successor*}
krauss@26056
   213
lemma [iff]: "quasinat(0)"
krauss@26056
   214
by (simp add: quasinat_def)
krauss@26056
   215
krauss@26056
   216
lemma [iff]: "quasinat(succ(x))"
krauss@26056
   217
by (simp add: quasinat_def)
krauss@26056
   218
krauss@26056
   219
lemma nat_imp_quasinat: "n \<in> nat ==> quasinat(n)"
krauss@26056
   220
by (erule natE, simp_all)
krauss@26056
   221
paulson@46820
   222
lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0"
paulson@46820
   223
by (simp add: quasinat_def nat_case_def)
krauss@26056
   224
krauss@26056
   225
lemma nat_cases_disj: "k=0 | (\<exists>y. k = succ(y)) | ~ quasinat(k)"
paulson@46820
   226
apply (case_tac "k=0", simp)
paulson@46820
   227
apply (case_tac "\<exists>m. k = succ(m)")
paulson@46820
   228
apply (simp_all add: quasinat_def)
krauss@26056
   229
done
krauss@26056
   230
krauss@26056
   231
lemma nat_cases:
krauss@26056
   232
     "[|k=0 ==> P;  !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P"
paulson@46820
   233
by (insert nat_cases_disj [of k], blast)
krauss@26056
   234
krauss@26056
   235
(** nat_case **)
krauss@26056
   236
krauss@26056
   237
lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
krauss@26056
   238
by (simp add: nat_case_def)
krauss@26056
   239
paulson@46820
   240
lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)"
krauss@26056
   241
by (simp add: nat_case_def)
krauss@26056
   242
krauss@26056
   243
lemma nat_case_type [TC]:
paulson@46820
   244
    "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |]
paulson@46820
   245
     ==> nat_case(a,b,n) \<in> C(n)";
paulson@46820
   246
by (erule nat_induct, auto)
krauss@26056
   247
krauss@26056
   248
lemma split_nat_case:
paulson@46820
   249
  "P(nat_case(a,b,k)) <->
paulson@46820
   250
   ((k=0 \<longrightarrow> P(a)) & (\<forall>x. k=succ(x) \<longrightarrow> P(b(x))) & (~ quasinat(k) \<longrightarrow> P(0)))"
paulson@46820
   251
apply (rule nat_cases [of k])
krauss@26056
   252
apply (auto simp add: non_nat_case)
krauss@26056
   253
done
krauss@26056
   254
krauss@26056
   255
krauss@26056
   256
subsection{*Recursion on the Natural Numbers*}
krauss@26056
   257
krauss@26056
   258
(** nat_rec is used to define eclose and transrec, then becomes obsolete.
krauss@26056
   259
    The operator rec, from arith.thy, has fewer typing conditions **)
krauss@26056
   260
krauss@26056
   261
lemma nat_rec_0: "nat_rec(0,a,b) = a"
krauss@26056
   262
apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
paulson@46820
   263
 apply (rule wf_Memrel)
krauss@26056
   264
apply (rule nat_case_0)
krauss@26056
   265
done
krauss@26056
   266
krauss@26056
   267
lemma nat_rec_succ: "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"
krauss@26056
   268
apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
paulson@46820
   269
 apply (rule wf_Memrel)
krauss@26056
   270
apply (simp add: vimage_singleton_iff)
krauss@26056
   271
done
krauss@26056
   272
krauss@26056
   273
(** The union of two natural numbers is a natural number -- their maximum **)
krauss@26056
   274
paulson@46820
   275
lemma Un_nat_type [TC]: "[| i: nat; j: nat |] ==> i \<union> j: nat"
krauss@26056
   276
apply (rule Un_least_lt [THEN ltD])
paulson@46820
   277
apply (simp_all add: lt_def)
krauss@26056
   278
done
krauss@26056
   279
paulson@46820
   280
lemma Int_nat_type [TC]: "[| i: nat; j: nat |] ==> i \<inter> j: nat"
krauss@26056
   281
apply (rule Int_greatest_lt [THEN ltD])
paulson@46820
   282
apply (simp_all add: lt_def)
krauss@26056
   283
done
krauss@26056
   284
krauss@26056
   285
(*needed to simplify unions over nat*)
paulson@46820
   286
lemma nat_nonempty [simp]: "nat \<noteq> 0"
krauss@26056
   287
by blast
krauss@26056
   288
krauss@26056
   289
text{*A natural number is the set of its predecessors*}
krauss@26056
   290
lemma nat_eq_Collect_lt: "i \<in> nat ==> {j\<in>nat. j<i} = i"
krauss@26056
   291
apply (rule equalityI)
paulson@46820
   292
apply (blast dest: ltD)
krauss@26056
   293
apply (auto simp add: Ord_mem_iff_lt)
paulson@46820
   294
apply (blast intro: lt_trans)
krauss@26056
   295
done
krauss@26056
   296
paulson@46820
   297
lemma Le_iff [iff]: "<x,y> \<in> Le <-> x \<le> y & x \<in> nat & y \<in> nat"
krauss@26056
   298
by (force simp add: Le_def)
krauss@26056
   299
krauss@26056
   300
end