-
Notifications
You must be signed in to change notification settings - Fork 0
/
util.maude
104 lines (91 loc) · 2.29 KB
/
util.maude
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
set include BOOL off .
fmod PRED is
--- ########## SORTS ##########
sorts Pred .
--- ########## SUBSORTS ##########
--- ########## OPS ##########
op _and_ : Pred Pred -> Pred .
op _or_ : Pred Pred -> Pred .
op tt : -> Pred [ctor] .
op ff : -> Pred [ctor] .
op _~_ : Pred Pred -> Pred [comm] .
op !_ : Pred -> Pred .
--- ########## VARS ##########
vars P1 P2 : Pred .
--- ########## EQS ##########
eq P1 and ff = ff .
eq P1 and tt = P1 .
eq tt or ff = tt .
eq ff or tt = tt .
eq tt or tt = tt .
eq ff or ff = ff .
eq tt ~ tt = tt .
eq tt ~ ff = ff .
eq ff ~ tt = ff .
eq ff ~ ff = ff .
eq !(ff) = tt .
eq !(tt) = ff .
endfm
fmod INAT is
pr PRED .
sort iNat .
op 0 : -> iNat [ctor metadata "1"] .
op s_ : iNat -> iNat [ctor metadata "2"] .
vars N N’ M : iNat .
--- equality enrichment
op _~iN_ : iNat iNat -> Pred [comm metadata "3"] .
eq N ~iN N = tt .
eq s N ~iN s N’ = N ~iN N’ .
eq 0 ~iN s N = ff .
eq N ~iN s N = ff .
op _+_ : iNat iNat -> iNat .
eq N + 0 = N .
eq 0 + N = N .
eq N + (s M) = s (N + M) .
op _-_ : iNat iNat -> iNat .
eq N - 0 = N .
eq 0 - (s N) = 0 .
eq (s N) - (s M) = N - M .
endfm
***(
The following module is only to be used to make things easier to read
)
--- fmod NUMNAT is
--- protecting INAT .
--- protecting NAT .
--- --- converts a iNat number into a Nat number
--- op From(_) : iNat -> Nat .
--- op FromHelper(_,_,_) : iNat iNat Nat -> Nat .
--- --- converts a Nat to an iNat
--- op To(_) : Nat -> iNat .
--- op ToHelper(_,_,_) : Nat Nat iNat -> iNat .
--- vars iNA iNB : iNat .
--- vars NA NB : Nat .
--- eq From((0).iNat) = (0).Nat .
--- eq From(iNA) = FromHelper(iNA, (0).iNat, (0).Nat) .
--- eq FromHelper(iNA, iNB, NA) =
--- if iNA ~iN iNB == tt then
--- NA
--- else
--- FromHelper(iNA, s iNB, NA + 1)
--- fi .
--- eq To(NA) = ToHelper(NA, (0).Nat, (0).iNat) .
--- eq ToHelper(NA, NB, iNA) =
--- if NA == NB then
--- iNA
--- else
--- ToHelper(NA, NB + 1, s iNA)
--- fi .
--- endfm
--- red 0 .
--- red 0 + s(0) .
--- red s(0) + 0 .
--- red s(0) + s(s(0)) .
--- red (s(0) + s(s(0))) + s(0) .
--- red s(0) + (s(0) + s(s(0))) .
--- red !(ff) .
--- red !(tt) .
--- red (s (s 0)) - 0 .
--- red (s s 0) - (s 0) .
--- red (s s 0) - (s s 0) .
--- red (s 0) - (s s s 0) .