|
1 | 1 | :js
|
2 | 2 | :import NofibPrelude.mls
|
3 |
| -//│ Imported 112 member(s) |
| 3 | +//│ Imported 109 member(s) |
4 | 4 |
|
5 | 5 |
|
6 | 6 | abstract class Id: A | B | C | D | X | Y | Z | U | W | ADD1 | AND | APPEND | CONS | CONSP | DIFFERENCE | DIVIDES | EQUAL | EVEN | EXP | F | FALSE | FOUR | GCD | GREATEREQP | GREATERP | IF | IFF | IMPLIES | LENGTH | LESSEQP | LESSP | LISTP | MEMBER | NIL | NILP | NLISTP | NOT | ODD | ONE | OR | PLUS | QUOTIENT | REMAINDER | REVERSE | SUB1 | TIMES | TRUE | TWO | ZERO | ZEROP
|
@@ -165,76 +165,116 @@ fun test0(xxxx) =
|
165 | 165 | let nil = Fun(NIL , Nil, lazy of () => Nil)
|
166 | 166 | let boyerTrue = Fun(TRUE , Nil, lazy of () => Nil)
|
167 | 167 | let zero = Fun(ZERO , Nil, lazy of () => Nil)
|
| 168 | + |
168 | 169 | fun one() = Fun(ONE, Nil, lazy of () => Cons(Tup2(one(), add1(zero)), Nil))
|
| 170 | + |
169 | 171 | fun two() = Fun(TWO, Nil, lazy of () => Cons(Tup2(two(), add1(one())), Nil))
|
| 172 | + |
170 | 173 | fun four() = Fun(FOUR, Nil, lazy of () => Cons(Tup2(four(), add1(add1(two()))), Nil))
|
| 174 | + |
171 | 175 | fun add1(a) = Fun(ADD1, a :: Nil, lazy of () => Nil)
|
| 176 | + |
172 | 177 | fun if_(a, b, c) = Fun(IF, Cons(a, Cons(b, Cons(c, Nil))), lazy of () => Cons(Tup2(if_(if_(x, y, z), u, w), if_(x, if_(y, u, w), if_(z, u, w))), Nil))
|
| 178 | + |
173 | 179 | fun not_(a) = Fun(NOT, a :: Nil, lazy of () => Tup2(not_(x), if_(x, boyerFalse, boyerTrue)) :: Nil)
|
| 180 | + |
174 | 181 | fun and_(a, b) =
|
175 | 182 | Fun(AND, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(and_(x, y), if_(x, if_(y, boyerTrue, boyerFalse), boyerFalse)), Nil))
|
| 183 | + |
176 | 184 | fun append_(a, b) =
|
177 | 185 | Fun(APPEND, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(append_(append_(x, y), z), append_(x, append_(y, z))), Nil))
|
| 186 | + |
178 | 187 | fun cons(a, b) =
|
179 | 188 | Fun(CONS, Cons(a, Cons(b, Nil)), lazy of () => Nil)
|
| 189 | + |
180 | 190 | fun consp(a) =
|
181 | 191 | Fun(CONSP, Cons(a, Nil), lazy of () => Cons(Tup2(consp(cons(x, y)), boyerTrue), Nil))
|
| 192 | + |
182 | 193 | fun difference(a, b) =
|
183 | 194 | Fun(DIFFERENCE, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(difference(x, x), zero), Cons(Tup2(difference(plus(x, y), x), y), Cons(Tup2(difference(plus(y, x), x), y), Cons(Tup2(difference(plus(x, y), plus(x, z)), difference(y, z)), Cons(Tup2(difference(plus(y, plus(x, z)), x), plus(y, z)), Cons(Tup2(difference(add1(plus(y, z)), z), add1(y)), Cons(Tup2(difference(add1(add1(x)), two()), x), Nil))))))))
|
| 195 | + |
184 | 196 | fun divides(a, b) =
|
185 | 197 | Fun(DIVIDES, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(divides(x, y), zerop(remainder(y, x))), Nil))
|
| 198 | + |
186 | 199 | fun equal(a, b) =
|
187 | 200 | Fun(EQUAL, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(equal(plus(x, y), zero), and_(zerop(x), zerop(y))), Cons(Tup2(equal(plus(x, y), plus(x, z)), equal(y, z)), Cons(Tup2(equal(zero, difference(x, y)), not_(lessp(y, x))), Cons(Tup2(equal(x, difference(x, y)), or_(equal(x, zero), zerop(y))), Cons(Tup2(equal(times(x, y), zero), or_(zerop(x), zerop(y))), Cons(Tup2(equal(append_(x, y), append_(x, z)), equal(y, z)), Cons(Tup2(equal(y, times(x, y)), or_(equal(y, zero), equal(x, one()))), Cons(Tup2(equal(x, times(x, y)), or_(equal(x, zero), equal(y, one()))), Cons(Tup2(equal(times(x, y), one()), and_(equal(x, one()), equal(y, one()))), Cons(Tup2(equal(difference(x, y), difference(z, y)), if_(lessp(x, y), not_(lessp(y, z)), if_(lessp(z, y), not_(lessp(y, x)), equal(x, z)))), Cons(Tup2(equal(lessp(x, y), z), if_(lessp(x, y), equal(boyerTrue, z), equal(boyerFalse, z))), Nil))))))))))))
|
| 201 | + |
188 | 202 | fun even_(a) =
|
189 | 203 | Fun(EVEN, Cons(a, Nil), lazy of () => Cons(Tup2(even_(x), if_(zerop(x), boyerTrue, odd_(sub1(x)))), Nil))
|
| 204 | + |
190 | 205 | fun exp_(a, b) =
|
191 | 206 | Fun(EXP, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(exp_(x, plus(y, z)), times(exp_(x, y), exp_(x, z))), Cons(Tup2(exp_(x, times(y, z)), exp_(exp_(x, y), z)), Nil)))
|
| 207 | + |
192 | 208 | fun f(a) =
|
193 | 209 | Fun(F, Cons(a, Nil), lazy of () => Nil)
|
| 210 | + |
194 | 211 | fun gcd_(a, b) =
|
195 | 212 | Fun(GCD, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(gcd_(x, y), gcd_(y, x)), Cons(Tup2(gcd_(times(x, z), times(y, z)), times(z, gcd_(x, y))), Nil)))
|
| 213 | + |
196 | 214 | fun greatereqp(a, b) =
|
197 | 215 | Fun(GREATEREQP, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(greatereqp(x, y), not_(lessp(x, y))), Nil))
|
| 216 | + |
198 | 217 | fun greaterp(a, b) =
|
199 | 218 | Fun(GREATERP, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(greaterp(x, y), lessp(y, x)), Nil))
|
| 219 | + |
200 | 220 | fun implies(a, b) =
|
201 | 221 | Fun(IMPLIES, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(implies(x, y), if_(x, if_(y, boyerTrue, boyerFalse), boyerTrue)), Nil))
|
| 222 | + |
202 | 223 | fun iff(a, b) =
|
203 | 224 | Fun(IFF, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(iff(x, y), and_(implies(x, y), implies(y, x))), Nil))
|
| 225 | + |
204 | 226 | fun length_(a) =
|
205 | 227 | Fun(LENGTH, Cons(a, Nil), lazy of () => Cons(Tup2(length_(reverse_(x)), length_(x)), Cons(Tup2(length_(cons(x, cons(y, cons(z, cons(u, w))))), plus(four(), length_(w))), Nil)))
|
| 228 | + |
206 | 229 | fun lesseqp(a, b) =
|
207 | 230 | Fun(LESSEQP, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(lesseqp(x, y), not_(lessp(y, x))), Nil))
|
| 231 | + |
208 | 232 | fun lessp(a, b) =
|
209 | 233 | Fun(LESSP, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(lessp(remainder(x, y), y), not_(zerop(y))), Cons(Tup2(lessp(quotient(x, y), x), and_(not_(zerop(x)), lessp(one(), y))), Cons(Tup2(lessp(plus(x, y), plus(x, z)), lessp(y, z)), Cons(Tup2(lessp(times(x, z), times(y, z)), and_(not_(zerop(z)), lessp(x, y))), Cons(Tup2(lessp(y, plus(x, y)), not_(zerop(x))), Nil))))))
|
| 234 | + |
210 | 235 | fun nilp(a) =
|
211 | 236 | Fun(NILP, Cons(a, Nil), lazy of () => Cons(Tup2(nilp(x), equal(x, nil)), Nil))
|
| 237 | + |
212 | 238 | fun listp(a) =
|
213 | 239 | Fun(LISTP, Cons(a, Nil), lazy of () => Cons(Tup2(listp(x), or_(nilp(x), consp(x))), Nil))
|
| 240 | + |
214 | 241 | fun member(a, b) =
|
215 | 242 | Fun(MEMBER, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(member(x, append_(y, z)), or_(member(x, y), member(x, z))), Cons(Tup2(member(x, reverse_(y)), member(x, y)), Nil)))
|
| 243 | + |
216 | 244 | fun nlistp(a) =
|
217 | 245 | Fun(NLISTP, Cons(a, Nil), lazy of () => Cons(Tup2(nlistp(x), not_(listp(x))), Nil))
|
| 246 | + |
218 | 247 | fun odd_(a) =
|
219 | 248 | Fun(ODD, Cons(a, Nil), lazy of () => Cons(Tup2(odd_(x), even_(sub1(x))), Nil))
|
| 249 | + |
220 | 250 | fun or_(a, b) =
|
221 | 251 | Fun(OR, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(or_(x, y), if_(x, boyerTrue, if_(y, boyerTrue, boyerFalse))), Nil))
|
| 252 | + |
222 | 253 | fun plus(a, b) =
|
223 | 254 | Fun(PLUS, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(plus(plus(x, y), z), plus(x, plus(y, z))), Cons(Tup2(plus(remainder(x, y), times(y, quotient(x, y))), x), Cons(Tup2(plus(x, add1(y)), add1(plus(x, y))), Nil))))
|
| 255 | + |
224 | 256 | fun quotient(a, b) =
|
225 | 257 | Fun(QUOTIENT, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(quotient(plus(x, plus(x, y)), two()), plus(x, quotient(y, two()))), Cons(Tup2(quotient(times(y, x), y), if_(zerop(y), zero, x)), Nil)))
|
| 258 | + |
226 | 259 | fun remainder(a, b) =
|
227 | 260 | Fun(REMAINDER, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(remainder(x, one()), zero), Cons(Tup2(remainder(x, x), zero), Cons(Tup2(remainder(times(x, y), x), zero), Cons(Tup2(remainder(times(x, y), y), zero), Nil)))))
|
| 261 | + |
228 | 262 | fun reverse_(a) =
|
229 | 263 | Fun(REVERSE, Cons(a, Nil), lazy of () => Cons(Tup2(reverse_(append_(x, y)), append_(reverse_(y), reverse_(x))), Nil))
|
| 264 | + |
230 | 265 | fun sub1(a) =
|
231 | 266 | Fun(SUB1, Cons(a, Nil), lazy of () => Cons(Tup2(sub1(add1(x)), x), Nil))
|
| 267 | + |
232 | 268 | fun times(a, b) =
|
233 | 269 | Fun(TIMES, Cons(a, Cons(b, Nil)), lazy of () => Cons(Tup2(times(x, plus(y, z)), plus(times(x, y), times(x, z))), Cons(Tup2(times(times(x, y), z), times(x, times(y, z))), Cons(Tup2(times(x, difference(y, z)), difference(times(y, x), times(z, x))), Cons(Tup2(times(x, add1(y)), plus(x, times(x, y))), Nil)))))
|
| 270 | + |
234 | 271 | fun zerop(a) =
|
235 | 272 | Fun(ZEROP, Cons(a, Nil), lazy of () => Cons(Tup2(zerop(x), equal(x, zero)), Nil))
|
| 273 | + |
236 | 274 | let subst0 = Cons(Tup2(X, f(plus(plus(a, b), plus(c, zero)))), Cons(Tup2(Y, f(times(times(a, b), plus(c, d)))), Cons(Tup2(Z, f(reverse_(append_(append_(a, b), nil)))), Cons(Tup2(U, equal(plus(a, b), difference(x, y))), Cons(Tup2(W, lessp(remainder(a, b), member(a, length_(b)))), Nil)))))
|
| 275 | + |
237 | 276 | let theorem = implies(and_(implies(xxxx, y), and_(implies(y, z), and_(implies(z, u), implies(u, w)))), implies(x, w))
|
| 277 | + |
238 | 278 | tautp(apply_subst(subst0, theorem))
|
239 | 279 |
|
240 | 280 | fun testBoyer_nofib(n) = all(test0, replicate(n, Var(X)))
|
|
0 commit comments