(* Title: ZF/Nat.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
section‹The Natural numbers As a Least Fixed Point
›
theory Nat
imports OrdQuant Bool
begin
definition
nat :: i
where
"nat \ lfp(Inf, \X. {0} \ {succ(i). i \ X})"
definition
quasinat ::
"i \ o" where
"quasinat(n) \ n=0 | (\m. n = succ(m))"
definition
(*Has an unconditional succ case, which is used in "recursor" below.*)
nat_case ::
"[i, i\i, i]\i" where
"nat_case(a,b,k) \ THE y. k=0 \ y=a | (\x. k=succ(x) \ y=b(x))"
definition
nat_rec ::
"[i, i, [i,i]\i]\i" where
"nat_rec(k,a,b) \
wfrec(Memrel(nat), k, λn f. nat_case(a, λm. b(m, f`m), n))
"
(*Internalized relations on the naturals*)
definition
Le :: i
where
"Le \ {\x,y\:nat*nat. x \ y}"
definition
Lt :: i
where
"Lt \ {\x, y\:nat*nat. x < y}"
definition
Ge :: i
where
"Ge \ {\x,y\:nat*nat. y \ x}"
definition
Gt :: i
where
"Gt \ {\x,y\:nat*nat. y < x}"
definition
greater_than ::
"i\i" where
"greater_than(n) \ {i \ nat. n < i}"
text‹No need
for a less-than operator: a natural number
is its list of
predecessors!
›
lemma nat_bnd_mono:
"bnd_mono(Inf, \X. {0} \ {succ(i). i \ X})"
apply (rule bnd_monoI)
apply (cut_tac infinity, blast, blast)
done
(* @{term"nat = {0} \<union> {succ(x). x \<in> nat}"} *)
lemmas nat_unfold = nat_bnd_mono [
THEN nat_def [
THEN def_lfp_unfold]]
(** Type checking of 0 and successor **)
lemma nat_0I [iff,TC]:
"0 \ nat"
apply (subst nat_unfold)
apply (rule singletonI [
THEN UnI1])
done
lemma nat_succI [intro!,TC]:
"n \ nat \ succ(n) \ nat"
apply (subst nat_unfold)
apply (erule RepFunI [
THEN UnI2])
done
lemma nat_1I [iff,TC]:
"1 \ nat"
by (rule nat_0I [
THEN nat_succI])
lemma nat_2I [iff,TC]:
"2 \ nat"
by (rule nat_1I [
THEN nat_succI])
lemma bool_subset_nat:
"bool \ nat"
by (blast elim!: boolE)
lemmas bool_into_nat = bool_subset_nat [
THEN subsetD]
subsection‹Injectivity Properties
and Induction›
(*Mathematical induction*)
lemma nat_induct [case_names 0 succ, induct set: nat]:
"\n \ nat; P(0); \x. \x \ nat; P(x)\ \ P(succ(x))\ \ P(n)"
by (erule def_induct [OF nat_def nat_bnd_mono], blast)
lemma natE:
assumes "n \ nat"
obtains (
"0")
"n=0" | (succ) x
where "x \ nat" "n=succ(x)"
using assms
by (rule nat_unfold [
THEN equalityD1,
THEN subsetD,
THEN UnE]) auto
lemma nat_into_Ord [simp]:
"n \ nat \ Ord(n)"
by (erule nat_induct, auto)
(* @{term"i \<in> nat \<Longrightarrow> 0 \<le> i"}; same thing as @{term"0<succ(i)"} *)
lemmas nat_0_le = nat_into_Ord [
THEN Ord_0_le]
(* @{term"i \<in> nat \<Longrightarrow> i \<le> i"}; same thing as @{term"i<succ(i)"} *)
lemmas nat_le_refl = nat_into_Ord [
THEN le_refl]
lemma Ord_nat [iff]:
"Ord(nat)"
apply (rule OrdI)
apply (erule_tac [2] nat_into_Ord [
THEN Ord_is_Transset])
unfolding Transset_def
apply (rule ballI)
apply (erule nat_induct, auto)
done
lemma Limit_nat [iff]:
"Limit(nat)"
unfolding Limit_def
apply (safe intro!: ltI Ord_nat)
apply (erule ltD)
done
lemma naturals_not_limit:
"a \ nat \ \ Limit(a)"
by (induct a rule: nat_induct, auto)
lemma succ_natD:
"succ(i): nat \ i \ nat"
by (rule Ord_trans [OF succI1], auto)
lemma nat_succ_iff [iff]:
"succ(n): nat \ n \ nat"
by (blast dest!: succ_natD)
lemma nat_le_Limit:
"Limit(i) \ nat \ i"
apply (rule subset_imp_le)
apply (simp_all add: Limit_is_Ord)
apply (rule subsetI)
apply (erule nat_induct)
apply (erule Limit_has_0 [
THEN ltD])
apply (blast intro: Limit_has_succ [
THEN ltD] ltI Limit_is_Ord)
done
(* \<lbrakk>succ(i): k; k \<in> nat\<rbrakk> \<Longrightarrow> i \<in> k *)
lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
lemma lt_nat_in_nat:
"\m nat\ \ m \ nat"
apply (erule ltE)
apply (erule Ord_trans, assumption, simp)
done
lemma le_in_nat:
"\m \ n; n \ nat\ \ m \ nat"
by (blast dest!: lt_nat_in_nat)
subsection‹Variations on Mathematical
Induction›
(*complete induction*)
lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]
lemma complete_induct_rule [case_names less, consumes 1]:
"i \ nat \ (\x. x \ nat \ (\y. y \ x \ P(y)) \ P(x)) \ P(i)"
using complete_induct [of i P]
by simp
(*Induction starting from m rather than 0*)
lemma nat_induct_from:
assumes "m \ n" "m \ nat" "n \ nat"
and "P(m)"
and "\x. \x \ nat; m \ x; P(x)\ \ P(succ(x))"
shows "P(n)"
proof -
from assms(3)
have "m \ n \ P(m) \ P(n)"
by (rule nat_induct) (
use assms(5)
in ‹simp_all add: distrib_simps le_succ_iff
›)
with assms(1,2,4)
show ?thesis
by blast
qed
(*Induction suitable for subtraction and less-than*)
lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
"\m \ nat; n \ nat;
∧x. x
∈ nat
==> P(x,0);
∧y. y
∈ nat
==> P(0,succ(y));
∧x y.
[x
∈ nat; y
∈ nat; P(x,y)
] ==> P(succ(x),succ(y))
]
==> P(m,n)
"
apply (erule_tac x = m
in rev_bspec)
apply (erule nat_induct, simp)
apply (rule ballI)
apply (rename_tac i j)
apply (erule_tac n=j
in nat_induct, auto)
done
(** Induction principle analogous to trancl_induct **)
lemma succ_lt_induct_lemma [rule_format]:
"m \ nat \ P(m,succ(m)) \ (\x\nat. P(m,x) \ P(m,succ(x))) \
(
∀n
∈nat. m<n
⟶ P(m,n))
"
apply (erule nat_induct)
apply (intro impI, rule nat_induct [
THEN ballI])
prefer 4
apply (intro impI, rule nat_induct [
THEN ballI])
apply (auto simp add: le_iff)
done
lemma succ_lt_induct:
"\m nat;
P(m,succ(m));
∧x.
[x
∈ nat; P(m,x)
] ==> P(m,succ(x))
]
==> P(m,n)
"
by (blast intro: succ_lt_induct_lemma lt_nat_in_nat)
subsection‹quasinat:
to allow a case-split rule
for 🍋‹nat_case
››
text‹True
if the argument
is zero or any successor
›
lemma [iff]:
"quasinat(0)"
by (simp add: quasinat_def)
lemma [iff]:
"quasinat(succ(x))"
by (simp add: quasinat_def)
lemma nat_imp_quasinat:
"n \ nat \ quasinat(n)"
by (erule natE, simp_all)
lemma non_nat_case:
"\ quasinat(x) \ nat_case(a,b,x) = 0"
by (simp add: quasinat_def nat_case_def)
lemma nat_cases_disj:
"k=0 | (\y. k = succ(y)) | \ quasinat(k)"
apply (case_tac
"k=0", simp)
apply (case_tac
"\m. k = succ(m)")
apply (simp_all add: quasinat_def)
done
lemma nat_cases:
"\k=0 \ P; \y. k = succ(y) \ P; \ quasinat(k) \ P\ \ P"
by (insert nat_cases_disj [of k], blast)
(** nat_case **)
lemma nat_case_0 [simp]:
"nat_case(a,b,0) = a"
by (simp add: nat_case_def)
lemma nat_case_succ [simp]:
"nat_case(a,b,succ(n)) = b(n)"
by (simp add: nat_case_def)
lemma nat_case_type [TC]:
"\n \ nat; a \ C(0); \m. m \ nat \ b(m): C(succ(m))\
==> nat_case(a,b,n)
∈ C(n)
"
by (erule nat_induct, auto)
lemma split_nat_case:
"P(nat_case(a,b,k)) \
((k=0
⟶ P(a))
∧ (
∀x. k=succ(x)
⟶ P(b(x)))
∧ (
¬ quasinat(k)
⟶ P(0)))
"
apply (rule nat_cases [of k])
apply (auto simp add: non_nat_case)
done
subsection‹Recursion on the Natural Numbers
›
(** nat_rec is used to define eclose and transrec, then becomes obsolete.
The operator rec, from arith.thy, has fewer typing conditions **)
lemma nat_rec_0:
"nat_rec(0,a,b) = a"
apply (rule nat_rec_def [
THEN def_wfrec,
THEN trans])
apply (rule wf_Memrel)
apply (rule nat_case_0)
done
lemma nat_rec_succ:
"m \ nat \ nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"
apply (rule nat_rec_def [
THEN def_wfrec,
THEN trans])
apply (rule wf_Memrel)
apply (simp add: vimage_singleton_iff)
done
(** The union of two natural numbers is a natural number -- their maximum **)
lemma Un_nat_type [TC]:
"\i \ nat; j \ nat\ \ i \ j \ nat"
apply (rule Un_least_lt [
THEN ltD])
apply (simp_all add: lt_def)
done
lemma Int_nat_type [TC]:
"\i \ nat; j \ nat\ \ i \ j \ nat"
apply (rule Int_greatest_lt [
THEN ltD])
apply (simp_all add: lt_def)
done
(*needed to simplify unions over nat*)
lemma nat_nonempty [simp]:
"nat \ 0"
by blast
text‹A natural number
is the set of its predecessors
›
lemma nat_eq_Collect_lt:
"i \ nat \ {j\nat. j
apply (rule equalityI)
apply (blast dest: ltD)
apply (auto simp add: Ord_mem_iff_lt)
apply (blast intro: lt_trans)
done
lemma Le_iff [iff]: "\x,y\ \ Le \ x \ y \ x \ nat \ y \ nat"
by (force simp add: Le_def)
end
