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