equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 Nat = Ord + Bool + |
9 Nat = Ord + Bool + |
10 consts |
10 consts |
11 nat :: "i" |
11 nat :: "i" |
12 nat_case :: "[i, i, i=>i]=>i" |
12 nat_case :: "[i, i=>i, i]=>i" |
13 nat_rec :: "[i, i, [i,i]=>i]=>i" |
13 nat_rec :: "[i, i, [i,i]=>i]=>i" |
14 |
14 |
15 rules |
15 rules |
16 |
16 |
17 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})" |
17 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})" |
18 |
18 |
19 nat_case_def |
19 nat_case_def |
20 "nat_case(k,a,b) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))" |
20 "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))" |
21 |
21 |
22 nat_rec_def |
22 nat_rec_def |
23 "nat_rec(k,a,b) == \ |
23 "nat_rec(k,a,b) == \ |
24 \ wfrec(Memrel(nat), k, %n f. nat_case(n, a, %m. b(m, f`m)))" |
24 \ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))" |
25 |
25 |
26 end |
26 end |