10 begin |
10 begin |
11 |
11 |
12 typedecl nat |
12 typedecl nat |
13 arities nat :: "term" |
13 arities nat :: "term" |
14 |
14 |
15 consts |
15 axiomatization |
16 Zero :: nat ("0") |
16 Zero :: nat ("0") and |
17 Suc :: "nat => nat" |
17 Suc :: "nat => nat" and |
18 rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" |
18 rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" and |
19 add :: "[nat, nat] => nat" (infixl "+" 60) |
|
20 |
19 |
21 (*Proof terms*) |
20 (*Proof terms*) |
22 nrec :: "[nat, p, [nat, p] => p] => p" |
21 nrec :: "[nat, p, [nat, p] => p] => p" and |
23 ninj :: "p => p" |
22 ninj :: "p => p" and |
24 nneq :: "p => p" |
23 nneq :: "p => p" and |
25 rec0 :: "p" |
24 rec0 :: "p" and |
26 recSuc :: "p" |
25 recSuc :: "p" |
|
26 where |
|
27 induct: "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x)) |
|
28 |] ==> nrec(n,b,c):P(n)" and |
27 |
29 |
28 axioms |
30 Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n" and |
29 induct: "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x)) |
31 Suc_neq_0: "p:Suc(m)=0 ==> nneq(p) : R" and |
30 |] ==> nrec(n,b,c):P(n)" |
32 rec_0: "rec0 : rec(0,a,f) = a" and |
|
33 rec_Suc: "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))" and |
|
34 nrecB0: "b: A ==> nrec(0,b,c) = b : A" and |
|
35 nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A" |
31 |
36 |
32 Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n" |
37 definition add :: "[nat, nat] => nat" (infixl "+" 60) |
33 Suc_neq_0: "p:Suc(m)=0 ==> nneq(p) : R" |
38 where "m + n == rec(m, n, %x y. Suc(y))" |
34 rec_0: "rec0 : rec(0,a,f) = a" |
|
35 rec_Suc: "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
|
36 |
|
37 defs |
|
38 add_def: "m+n == rec(m, n, %x y. Suc(y))" |
|
39 |
|
40 axioms |
|
41 nrecB0: "b: A ==> nrec(0,b,c) = b : A" |
|
42 nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A" |
|
43 |
39 |
44 |
40 |
45 subsection {* Proofs about the natural numbers *} |
41 subsection {* Proofs about the natural numbers *} |
46 |
42 |
47 schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)" |
43 schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)" |