author | blanchet |
Wed, 06 Nov 2013 22:50:12 +0100 | |
changeset 54284 | 0b53378080d9 |
parent 46954 | d8b3412cdb99 |
child 58860 | fee7cfa69c50 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26056
diff
changeset
|
1 |
(* Title: ZF/Nat_ZF.thy |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
3 |
Copyright 1994 University of Cambridge |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
4 |
*) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
5 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
6 |
header{*The Natural numbers As a Least Fixed Point*} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
7 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
8 |
theory Nat_ZF imports OrdQuant Bool begin |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
9 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
10 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
11 |
nat :: i where |
46953 | 12 |
"nat == lfp(Inf, %X. {0} \<union> {succ(i). i \<in> X})" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
13 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
14 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
15 |
quasinat :: "i => o" where |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
16 |
"quasinat(n) == n=0 | (\<exists>m. n = succ(m))" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
17 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
18 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
19 |
(*Has an unconditional succ case, which is used in "recursor" below.*) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
20 |
nat_case :: "[i, i=>i, i]=>i" where |
46820 | 21 |
"nat_case(a,b,k) == THE y. k=0 & y=a | (\<exists>x. k=succ(x) & y=b(x))" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
22 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
23 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
24 |
nat_rec :: "[i, i, [i,i]=>i]=>i" where |
46820 | 25 |
"nat_rec(k,a,b) == |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
26 |
wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
27 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
28 |
(*Internalized relations on the naturals*) |
46820 | 29 |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
30 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
31 |
Le :: i where |
46820 | 32 |
"Le == {<x,y>:nat*nat. x \<le> y}" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
33 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
34 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
35 |
Lt :: i where |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
36 |
"Lt == {<x, y>:nat*nat. x < y}" |
46820 | 37 |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
38 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
39 |
Ge :: i where |
46820 | 40 |
"Ge == {<x,y>:nat*nat. y \<le> x}" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
41 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
42 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
43 |
Gt :: i where |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
44 |
"Gt == {<x,y>:nat*nat. y < x}" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
45 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
46 |
definition |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
47 |
greater_than :: "i=>i" where |
46953 | 48 |
"greater_than(n) == {i \<in> nat. n < i}" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
49 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
50 |
text{*No need for a less-than operator: a natural number is its list of |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
51 |
predecessors!*} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
52 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
53 |
|
46953 | 54 |
lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} \<union> {succ(i). i \<in> X})" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
55 |
apply (rule bnd_monoI) |
46820 | 56 |
apply (cut_tac infinity, blast, blast) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
57 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
58 |
|
46953 | 59 |
(* @{term"nat = {0} \<union> {succ(x). x \<in> nat}"} *) |
45602 | 60 |
lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold]] |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
61 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
62 |
(** Type checking of 0 and successor **) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
63 |
|
46820 | 64 |
lemma nat_0I [iff,TC]: "0 \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
65 |
apply (subst nat_unfold) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
66 |
apply (rule singletonI [THEN UnI1]) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
67 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
68 |
|
46820 | 69 |
lemma nat_succI [intro!,TC]: "n \<in> nat ==> succ(n) \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
70 |
apply (subst nat_unfold) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
71 |
apply (erule RepFunI [THEN UnI2]) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
72 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
73 |
|
46820 | 74 |
lemma nat_1I [iff,TC]: "1 \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
75 |
by (rule nat_0I [THEN nat_succI]) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
76 |
|
46820 | 77 |
lemma nat_2I [iff,TC]: "2 \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
78 |
by (rule nat_1I [THEN nat_succI]) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
79 |
|
46820 | 80 |
lemma bool_subset_nat: "bool \<subseteq> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
81 |
by (blast elim!: boolE) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
82 |
|
45602 | 83 |
lemmas bool_into_nat = bool_subset_nat [THEN subsetD] |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
84 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
85 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
86 |
subsection{*Injectivity Properties and Induction*} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
87 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
88 |
(*Mathematical induction*) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
89 |
lemma nat_induct [case_names 0 succ, induct set: nat]: |
46953 | 90 |
"[| n \<in> nat; P(0); !!x. [| x \<in> nat; P(x) |] ==> P(succ(x)) |] ==> P(n)" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
91 |
by (erule def_induct [OF nat_def nat_bnd_mono], blast) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
92 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
93 |
lemma natE: |
46935 | 94 |
assumes "n \<in> nat" |
46954 | 95 |
obtains ("0") "n=0" | (succ) x where "x \<in> nat" "n=succ(x)" |
46935 | 96 |
using assms |
97 |
by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
98 |
|
46935 | 99 |
lemma nat_into_Ord [simp]: "n \<in> nat ==> Ord(n)" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
100 |
by (erule nat_induct, auto) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
101 |
|
46953 | 102 |
(* @{term"i \<in> nat ==> 0 \<le> i"}; same thing as @{term"0<succ(i)"} *) |
45602 | 103 |
lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le] |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
104 |
|
46953 | 105 |
(* @{term"i \<in> nat ==> i \<le> i"}; same thing as @{term"i<succ(i)"} *) |
45602 | 106 |
lemmas nat_le_refl = nat_into_Ord [THEN le_refl] |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
107 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
108 |
lemma Ord_nat [iff]: "Ord(nat)" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
109 |
apply (rule OrdI) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
110 |
apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset]) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
111 |
apply (unfold Transset_def) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
112 |
apply (rule ballI) |
46820 | 113 |
apply (erule nat_induct, auto) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
114 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
115 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
116 |
lemma Limit_nat [iff]: "Limit(nat)" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
117 |
apply (unfold Limit_def) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
118 |
apply (safe intro!: ltI Ord_nat) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
119 |
apply (erule ltD) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
120 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
121 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
122 |
lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
123 |
by (induct a rule: nat_induct, auto) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
124 |
|
46953 | 125 |
lemma succ_natD: "succ(i): nat ==> i \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
126 |
by (rule Ord_trans [OF succI1], auto) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
127 |
|
46935 | 128 |
lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
129 |
by (blast dest!: succ_natD) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
130 |
|
46820 | 131 |
lemma nat_le_Limit: "Limit(i) ==> nat \<le> i" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
132 |
apply (rule subset_imp_le) |
46820 | 133 |
apply (simp_all add: Limit_is_Ord) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
134 |
apply (rule subsetI) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
135 |
apply (erule nat_induct) |
46820 | 136 |
apply (erule Limit_has_0 [THEN ltD]) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
137 |
apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
138 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
139 |
|
46953 | 140 |
(* [| succ(i): k; k \<in> nat |] ==> i \<in> k *) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
141 |
lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord] |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
142 |
|
46953 | 143 |
lemma lt_nat_in_nat: "[| m<n; n \<in> nat |] ==> m \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
144 |
apply (erule ltE) |
46820 | 145 |
apply (erule Ord_trans, assumption, simp) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
146 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
147 |
|
46953 | 148 |
lemma le_in_nat: "[| m \<le> n; n \<in> nat |] ==> m \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
149 |
by (blast dest!: lt_nat_in_nat) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
150 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
151 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
152 |
subsection{*Variations on Mathematical Induction*} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
153 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
154 |
(*complete induction*) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
155 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
156 |
lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1] |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
157 |
|
46820 | 158 |
lemmas complete_induct_rule = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26056
diff
changeset
|
159 |
complete_induct [rule_format, case_names less, consumes 1] |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
160 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
161 |
|
46820 | 162 |
lemma nat_induct_from_lemma [rule_format]: |
46953 | 163 |
"[| n \<in> nat; m \<in> nat; |
164 |
!!x. [| x \<in> nat; m \<le> x; P(x) |] ==> P(succ(x)) |] |
|
46820 | 165 |
==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)" |
166 |
apply (erule nat_induct) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
167 |
apply (simp_all add: distrib_simps le0_iff le_succ_iff) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
168 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
169 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
170 |
(*Induction starting from m rather than 0*) |
46820 | 171 |
lemma nat_induct_from: |
46953 | 172 |
"[| m \<le> n; m \<in> nat; n \<in> nat; |
46820 | 173 |
P(m); |
46953 | 174 |
!!x. [| x \<in> nat; m \<le> x; P(x) |] ==> P(succ(x)) |] |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
175 |
==> P(n)" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
176 |
apply (blast intro: nat_induct_from_lemma) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
177 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
178 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
179 |
(*Induction suitable for subtraction and less-than*) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
180 |
lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]: |
46953 | 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)) |] |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
185 |
==> P(m,n)" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
186 |
apply (erule_tac x = m in rev_bspec) |
46820 | 187 |
apply (erule nat_induct, simp) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
188 |
apply (rule ballI) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
189 |
apply (rename_tac i j) |
46820 | 190 |
apply (erule_tac n=j in nat_induct, auto) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
191 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
192 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
193 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
194 |
(** Induction principle analogous to trancl_induct **) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
195 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
196 |
lemma succ_lt_induct_lemma [rule_format]: |
46953 | 197 |
"m \<in> nat ==> P(m,succ(m)) \<longrightarrow> (\<forall>x\<in>nat. P(m,x) \<longrightarrow> P(m,succ(x))) \<longrightarrow> |
46820 | 198 |
(\<forall>n\<in>nat. m<n \<longrightarrow> P(m,n))" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
199 |
apply (erule nat_induct) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
200 |
apply (intro impI, rule nat_induct [THEN ballI]) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
201 |
prefer 4 apply (intro impI, rule nat_induct [THEN ballI]) |
46820 | 202 |
apply (auto simp add: le_iff) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
203 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
204 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
205 |
lemma succ_lt_induct: |
46935 | 206 |
"[| m<n; n \<in> nat; |
46820 | 207 |
P(m,succ(m)); |
46953 | 208 |
!!x. [| x \<in> nat; P(m,x) |] ==> P(m,succ(x)) |] |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
209 |
==> P(m,n)" |
46820 | 210 |
by (blast intro: succ_lt_induct_lemma lt_nat_in_nat) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
211 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
212 |
subsection{*quasinat: to allow a case-split rule for @{term nat_case}*} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
213 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
214 |
text{*True if the argument is zero or any successor*} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
215 |
lemma [iff]: "quasinat(0)" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
216 |
by (simp add: quasinat_def) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
217 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
218 |
lemma [iff]: "quasinat(succ(x))" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
219 |
by (simp add: quasinat_def) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
220 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
221 |
lemma nat_imp_quasinat: "n \<in> nat ==> quasinat(n)" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
222 |
by (erule natE, simp_all) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
223 |
|
46820 | 224 |
lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0" |
225 |
by (simp add: quasinat_def nat_case_def) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
226 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
227 |
lemma nat_cases_disj: "k=0 | (\<exists>y. k = succ(y)) | ~ quasinat(k)" |
46820 | 228 |
apply (case_tac "k=0", simp) |
229 |
apply (case_tac "\<exists>m. k = succ(m)") |
|
230 |
apply (simp_all add: quasinat_def) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
231 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
232 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
233 |
lemma nat_cases: |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
234 |
"[|k=0 ==> P; !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P" |
46820 | 235 |
by (insert nat_cases_disj [of k], blast) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
236 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
237 |
(** nat_case **) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
238 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
239 |
lemma nat_case_0 [simp]: "nat_case(a,b,0) = a" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
240 |
by (simp add: nat_case_def) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
241 |
|
46820 | 242 |
lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
243 |
by (simp add: nat_case_def) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
244 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
245 |
lemma nat_case_type [TC]: |
46953 | 246 |
"[| n \<in> nat; a \<in> C(0); !!m. m \<in> nat ==> b(m): C(succ(m)) |] |
46820 | 247 |
==> nat_case(a,b,n) \<in> C(n)"; |
248 |
by (erule nat_induct, auto) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
249 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
250 |
lemma split_nat_case: |
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
251 |
"P(nat_case(a,b,k)) \<longleftrightarrow> |
46820 | 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]) |
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
254 |
apply (auto simp add: non_nat_case) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
255 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
256 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
257 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
258 |
subsection{*Recursion on the Natural Numbers*} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
259 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
260 |
(** nat_rec is used to define eclose and transrec, then becomes obsolete. |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
261 |
The operator rec, from arith.thy, has fewer typing conditions **) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
262 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
263 |
lemma nat_rec_0: "nat_rec(0,a,b) = a" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
264 |
apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) |
46820 | 265 |
apply (rule wf_Memrel) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
266 |
apply (rule nat_case_0) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
267 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
268 |
|
46953 | 269 |
lemma nat_rec_succ: "m \<in> nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
270 |
apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) |
46820 | 271 |
apply (rule wf_Memrel) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
272 |
apply (simp add: vimage_singleton_iff) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
273 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
274 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
275 |
(** The union of two natural numbers is a natural number -- their maximum **) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
276 |
|
46953 | 277 |
lemma Un_nat_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> i \<union> j \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
278 |
apply (rule Un_least_lt [THEN ltD]) |
46820 | 279 |
apply (simp_all add: lt_def) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
280 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
281 |
|
46953 | 282 |
lemma Int_nat_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> i \<inter> j \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
283 |
apply (rule Int_greatest_lt [THEN ltD]) |
46820 | 284 |
apply (simp_all add: lt_def) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
285 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
286 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
287 |
(*needed to simplify unions over nat*) |
46820 | 288 |
lemma nat_nonempty [simp]: "nat \<noteq> 0" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
289 |
by blast |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
290 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
291 |
text{*A natural number is the set of its predecessors*} |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
292 |
lemma nat_eq_Collect_lt: "i \<in> nat ==> {j\<in>nat. j<i} = i" |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
293 |
apply (rule equalityI) |
46820 | 294 |
apply (blast dest: ltD) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
295 |
apply (auto simp add: Ord_mem_iff_lt) |
46820 | 296 |
apply (blast intro: lt_trans) |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
297 |
done |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
298 |
|
46821
ff6b0c1087f2
Using mathematical notation for <-> and cardinal arithmetic
paulson
parents:
46820
diff
changeset
|
299 |
lemma Le_iff [iff]: "<x,y> \<in> Le \<longleftrightarrow> x \<le> y & x \<in> nat & y \<in> nat" |
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
300 |
by (force simp add: Le_def) |
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
301 |
|
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff
changeset
|
302 |
end |