author | wenzelm |
Thu, 06 May 2004 14:14:18 +0200 | |
changeset 14706 | 71590b7733b7 |
parent 14691 | e1eedc8cad37 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
11355 | 1 |
(* Title: HOL/Library/Nat_Infinity.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb, TU Muenchen |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
5 |
*) |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
6 |
|
14706 | 7 |
header {* Natural numbers with infinity *} |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
8 |
|
11355 | 9 |
theory Nat_Infinity = Main: |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
10 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
11 |
subsection "Definitions" |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
12 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
13 |
text {* |
11355 | 14 |
We extend the standard natural numbers by a special value indicating |
15 |
infinity. This includes extending the ordering relations @{term "op |
|
16 |
<"} and @{term "op \<le>"}. |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
17 |
*} |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
18 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
19 |
datatype inat = Fin nat | Infty |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
20 |
|
14691 | 21 |
instance inat :: "{ord, zero}" .. |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
22 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
23 |
consts |
11355 | 24 |
iSuc :: "inat => inat" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
25 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
26 |
syntax (xsymbols) |
11355 | 27 |
Infty :: inat ("\<infinity>") |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
28 |
|
14565 | 29 |
syntax (HTML output) |
30 |
Infty :: inat ("\<infinity>") |
|
31 |
||
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
32 |
defs |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset
|
33 |
Zero_inat_def: "0 == Fin 0" |
11355 | 34 |
iSuc_def: "iSuc i == case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>" |
35 |
iless_def: "m < n == |
|
36 |
case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True) |
|
37 |
| \<infinity> => False" |
|
38 |
ile_def: "(m::inat) \<le> n == \<not> (n < m)" |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
39 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset
|
40 |
lemmas inat_defs = Zero_inat_def iSuc_def iless_def ile_def |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
41 |
lemmas inat_splits = inat.split inat.split_asm |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
42 |
|
11355 | 43 |
text {* |
11357 | 44 |
Below is a not quite complete set of theorems. Use the method |
45 |
@{text "(simp add: inat_defs split:inat_splits, arith?)"} to prove |
|
46 |
new theorems or solve arithmetic subgoals involving @{typ inat} on |
|
47 |
the fly. |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
48 |
*} |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
49 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
50 |
subsection "Constructors" |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
51 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
52 |
lemma Fin_0: "Fin 0 = 0" |
11357 | 53 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
54 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
55 |
lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0" |
11357 | 56 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
57 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
58 |
lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>" |
11357 | 59 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
60 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
61 |
lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)" |
11357 | 62 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
63 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
64 |
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>" |
11357 | 65 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
66 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
67 |
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0" |
11357 | 68 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
69 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
70 |
lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)" |
11357 | 71 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
72 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
73 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
74 |
subsection "Ordering relations" |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
75 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
76 |
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R" |
11357 | 77 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
78 |
|
11355 | 79 |
lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)" |
11357 | 80 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
81 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
82 |
lemma iless_not_refl [simp]: "\<not> n < (n::inat)" |
11357 | 83 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
84 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
85 |
lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)" |
11357 | 86 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
87 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
88 |
lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)" |
11357 | 89 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
90 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
91 |
lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)" |
11357 | 92 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
93 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
94 |
lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>" |
11357 | 95 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
96 |
|
11655 | 97 |
lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)" |
11357 | 98 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
99 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
100 |
lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)" |
11357 | 101 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
102 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
103 |
lemma i0_iless_iSuc [simp]: "0 < iSuc n" |
11357 | 104 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
105 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
106 |
lemma not_ilessi0 [simp]: "\<not> n < (0::inat)" |
11357 | 107 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
108 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
109 |
lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k" |
11357 | 110 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
111 |
|
11655 | 112 |
lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)" |
11357 | 113 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
114 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
115 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
116 |
(* ----------------------------------------------------------------------- *) |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
117 |
|
11655 | 118 |
lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))" |
11357 | 119 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
120 |
|
11355 | 121 |
lemma ile_refl [simp]: "n \<le> (n::inat)" |
11357 | 122 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
123 |
|
11355 | 124 |
lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)" |
11357 | 125 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
126 |
|
11355 | 127 |
lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)" |
11357 | 128 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
129 |
|
11355 | 130 |
lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)" |
11357 | 131 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
132 |
|
11355 | 133 |
lemma Infty_ub [simp]: "n \<le> \<infinity>" |
11357 | 134 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
135 |
|
11355 | 136 |
lemma i0_lb [simp]: "(0::inat) \<le> n" |
11357 | 137 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
138 |
|
11355 | 139 |
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R" |
11357 | 140 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
141 |
|
11355 | 142 |
lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)" |
11357 | 143 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
144 |
|
11355 | 145 |
lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)" |
11357 | 146 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
147 |
|
11355 | 148 |
lemma ileI1: "m < n ==> iSuc m \<le> n" |
11357 | 149 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
150 |
|
11655 | 151 |
lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)" |
11357 | 152 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
153 |
|
11655 | 154 |
lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)" |
11357 | 155 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
156 |
|
11655 | 157 |
lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)" |
11357 | 158 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
159 |
|
11355 | 160 |
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" |
11357 | 161 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
162 |
|
11355 | 163 |
lemma ile_iSuc [simp]: "n \<le> iSuc n" |
11357 | 164 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
165 |
|
11355 | 166 |
lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k" |
11357 | 167 |
by (simp add: inat_defs split:inat_splits, arith?) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
168 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
169 |
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j" |
11355 | 170 |
apply (induct_tac k) |
171 |
apply (simp (no_asm) only: Fin_0) |
|
172 |
apply (fast intro: ile_iless_trans i0_lb) |
|
173 |
apply (erule exE) |
|
174 |
apply (drule spec) |
|
175 |
apply (erule exE) |
|
176 |
apply (drule ileI1) |
|
177 |
apply (rule iSuc_Fin [THEN subst]) |
|
178 |
apply (rule exI) |
|
179 |
apply (erule (1) ile_iless_trans) |
|
180 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
181 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
182 |
end |