equal
deleted
inserted
replaced
5 header {* Natural numbers with infinity *} |
5 header {* Natural numbers with infinity *} |
6 |
6 |
7 theory Nat_Infinity |
7 theory Nat_Infinity |
8 imports Plain "~~/src/HOL/Presburger" |
8 imports Plain "~~/src/HOL/Presburger" |
9 begin |
9 begin |
10 |
|
11 text {* FIXME: move to Nat.thy *} |
|
12 |
|
13 instantiation nat :: bot |
|
14 begin |
|
15 |
|
16 definition bot_nat :: nat where |
|
17 "bot_nat = 0" |
|
18 |
|
19 instance proof |
|
20 qed (simp add: bot_nat_def) |
|
21 |
10 |
22 subsection {* Type definition *} |
11 subsection {* Type definition *} |
23 |
12 |
24 text {* |
13 text {* |
25 We extend the standard natural numbers by a special value indicating |
14 We extend the standard natural numbers by a special value indicating |
26 infinity. |
15 infinity. |
27 *} |
16 *} |
28 |
|
29 end |
|
30 |
17 |
31 datatype inat = Fin nat | Infty |
18 datatype inat = Fin nat | Infty |
32 |
19 |
33 notation (xsymbols) |
20 notation (xsymbols) |
34 Infty ("\<infinity>") |
21 Infty ("\<infinity>") |