9 |
9 |
10 INCOMPATIBLE with nat2.thy, Nipkow's example |
10 INCOMPATIBLE with nat2.thy, Nipkow's example |
11 *) |
11 *) |
12 |
12 |
13 Nat = FOL + |
13 Nat = FOL + |
14 types nat 0 |
14 types nat |
15 arities nat :: term |
15 arities nat :: term |
16 consts "0" :: "nat" ("0") |
16 consts "0" :: "nat" ("0") |
17 Suc :: "nat=>nat" |
17 Suc :: "nat=>nat" |
18 rec :: "[nat, 'a, [nat,'a]=>'a] => 'a" |
18 rec :: "[nat, 'a, [nat,'a]=>'a] => 'a" |
19 "+" :: "[nat, nat] => nat" (infixl 60) |
19 "+" :: "[nat, nat] => nat" (infixl 60) |
20 rules induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" |
20 rules induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" |
21 Suc_inject "Suc(m)=Suc(n) ==> m=n" |
21 Suc_inject "Suc(m)=Suc(n) ==> m=n" |
22 Suc_neq_0 "Suc(m)=0 ==> R" |
22 Suc_neq_0 "Suc(m)=0 ==> R" |
23 rec_0 "rec(0,a,f) = a" |
23 rec_0 "rec(0,a,f) = a" |
24 rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
24 rec_Suc "rec(Suc(m), a, f) = f(m, rec(m,a,f))" |