|
1246
|
1 |
(* Title: FOL/ex/NatClass.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
|
4 |
|
|
|
5 |
This is an abstract version of Nat.thy. Instead of axiomatizing a
|
|
|
6 |
single type "nat" we define the class of all these types (up to
|
|
|
7 |
isomorphism).
|
|
|
8 |
|
|
|
9 |
Note: The "rec" operator had to be made 'monomorphic', because class
|
|
|
10 |
axioms may not contain more than one type variable.
|
|
|
11 |
*)
|
|
|
12 |
|
|
|
13 |
NatClass = FOL +
|
|
|
14 |
|
|
|
15 |
consts
|
|
|
16 |
"0" :: "'a" ("0")
|
|
|
17 |
Suc :: "'a => 'a"
|
|
|
18 |
rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"
|
|
|
19 |
|
|
|
20 |
axclass
|
|
|
21 |
nat < term
|
|
|
22 |
induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
|
|
|
23 |
Suc_inject "Suc(m) = Suc(n) ==> m = n"
|
|
|
24 |
Suc_neq_0 "Suc(m) = 0 ==> R"
|
|
|
25 |
rec_0 "rec(0, a, f) = a"
|
|
|
26 |
rec_Suc "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
|
|
|
27 |
|
|
|
28 |
consts
|
|
|
29 |
"+" :: "['a::nat, 'a] => 'a" (infixl 60)
|
|
|
30 |
|
|
|
31 |
defs
|
|
|
32 |
add_def "m + n == rec(m, n, %x y. Suc(y))"
|
|
|
33 |
|
|
|
34 |
end
|