equal
deleted
inserted
replaced
45 (* abstract constants and syntax *) |
45 (* abstract constants and syntax *) |
46 |
46 |
47 consts |
47 consts |
48 "0" :: nat ("0") |
48 "0" :: nat ("0") |
49 Suc :: nat => nat |
49 Suc :: nat => nat |
50 nat_case :: ['a, nat => 'a, nat] => 'a |
|
51 pred_nat :: "(nat * nat) set" |
50 pred_nat :: "(nat * nat) set" |
52 nat_rec :: ['a, [nat, 'a] => 'a, nat] => 'a |
|
53 |
51 |
54 syntax |
52 syntax |
55 "1" :: nat ("1") |
53 "1" :: nat ("1") |
56 "2" :: nat ("2") |
54 "2" :: nat ("2") |
57 |
55 |
58 translations |
56 translations |
59 "1" == "Suc 0" |
57 "1" == "Suc 0" |
60 "2" == "Suc 1" |
58 "2" == "Suc 1" |
61 "case p of 0 => a | Suc y => b" == "nat_case a (%y. b) p" |
|
62 |
59 |
63 |
60 |
64 local |
61 local |
65 |
62 |
66 defs |
63 defs |
67 Zero_def "0 == Abs_Nat(Zero_Rep)" |
64 Zero_def "0 == Abs_Nat(Zero_Rep)" |
68 Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" |
65 Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" |
69 |
66 |
70 (*nat operations and recursion*) |
67 (*nat operations and recursion*) |
71 nat_case_def "nat_case a f n == @z. (n=0 --> z=a) |
|
72 & (!x. n=Suc x --> z=f(x))" |
|
73 pred_nat_def "pred_nat == {(m,n). n = Suc m}" |
68 pred_nat_def "pred_nat == {(m,n). n = Suc m}" |
74 |
69 |
75 less_def "m<n == (m,n):trancl(pred_nat)" |
70 less_def "m<n == (m,n):trancl(pred_nat)" |
76 |
71 |
77 le_def "m<=(n::nat) == ~(n<m)" |
72 le_def "m<=(n::nat) == ~(n<m)" |
78 |
73 |
79 nat_rec_def "nat_rec c d == |
|
80 wfrec pred_nat (%f. nat_case c (%m. d m (f m)))" |
|
81 end |
74 end |