equal
deleted
inserted
replaced
53 (* abstract constants and syntax *) |
53 (* abstract constants and syntax *) |
54 |
54 |
55 consts |
55 consts |
56 Suc :: nat => nat |
56 Suc :: nat => nat |
57 pred_nat :: "(nat * nat) set" |
57 pred_nat :: "(nat * nat) set" |
|
58 "1" :: nat ("1") |
58 |
59 |
59 syntax |
60 syntax |
60 "1" :: nat ("1") |
61 "1'" :: nat ("1'") |
61 "2" :: nat ("2") |
62 "2" :: nat ("2") |
62 |
63 |
63 translations |
64 translations |
64 "1" == "Suc 0" |
65 "1'" == "Suc 0" |
65 "2" == "Suc 1" |
66 "2" == "Suc 1'" |
66 |
67 |
67 |
68 |
68 local |
69 local |
69 |
70 |
70 defs |
71 defs |
71 Zero_def "0 == Abs_Nat(Zero_Rep)" |
72 Zero_def "0 == Abs_Nat(Zero_Rep)" |
72 Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" |
73 Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" |
|
74 One_def "1 == 1'" |
73 |
75 |
74 (*nat operations*) |
76 (*nat operations*) |
75 pred_nat_def "pred_nat == {(m,n). n = Suc m}" |
77 pred_nat_def "pred_nat == {(m,n). n = Suc m}" |
76 |
78 |
77 less_def "m<n == (m,n):trancl(pred_nat)" |
79 less_def "m<n == (m,n):trancl(pred_nat)" |