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
```