--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/test.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,301 @@
+fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
+fun read thy = term_of o cread thy;
+fun Term s = read WF1.thy s;
+
+fun Rfunc thy R eqs =
+ let val {induction,rules,theory,tcs} =
+ timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
+ in {induction=induction, rules=rules, theory=theory,
+ tcs = map (cterm_of (sign_of theory)) tcs}
+ end;
+
+val Rfunction = Rfunc WF1.thy;
+
+fun function tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
+
+
+(*---------------------------------------------------------------------------
+ * Factorial. Notice how functions without pattern matching are often harder
+ * to deal with than those with! Unfortunately, not all functions can be
+ * described purely by pattern matching, e.g., "variant" as below.
+ *---------------------------------------------------------------------------*)
+function "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
+
+Rfunction"pred_nat"
+ "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
+
+function "(Fact 0 = (Suc 0)) & \
+ \ (Fact (Suc x) = (Fact x * Suc x))";
+
+Rfunction "pred_nat"
+ "(Fact 0 = (Suc 0)) & \
+ \ (Fact (Suc x) = (Fact x * Suc x))";
+
+(*---------------------------------------------------------------------------
+ * Fibonacci.
+ *---------------------------------------------------------------------------*)
+function "(Fib 0 = (Suc 0)) & \
+ \ (Fib (Suc 0) = (Suc 0)) & \
+ \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
+
+(* "<" doesn't currently work smoothly *)
+Rfunction"{p::(nat*nat). fst p < snd p}"
+ "(Fib 0 = (Suc 0)) & \
+ \ (Fib (Suc 0) = (Suc 0)) & \
+ \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
+
+
+(* "trancl pred" means "<" and works better *)
+Rfunction"trancl pred_nat"
+ "(Fib 0 = (Suc 0)) & \
+ \ (Fib (Suc 0) = (Suc 0)) & \
+ \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
+
+(*---------------------------------------------------------------------------
+ * Ackermann.
+ *---------------------------------------------------------------------------*)
+Rfunction"pred_nat ** pred_nat"
+ "(Ack (0,n) = (n + Suc 0)) & \
+ \ (Ack (Suc m,0) = (Ack (m, Suc 0))) & \
+ \ (Ack (Suc m, Suc n) = Ack (m, Ack (Suc m, n)))";
+
+(*---------------------------------------------------------------------------
+ * Almost primitive recursion.
+ *---------------------------------------------------------------------------*)
+function"(map2(f, [], L) = []) & \
+ \ (map2(f, h#t, []) = []) & \
+ \ (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
+
+(* Swap arguments *)
+function"(map2(([],L), f) = []) & \
+ \ (map2((h#t, []), f) = []) & \
+ \ (map2((h1#t1, h2#t2), f) = f h1 h2 # map2((t1,t2),f))";
+
+Rfunction
+ "measure((length o fst o snd)::('a=>'b=>'c)*'a list*'b list => nat)"
+ "(map2((f::'a=>'b=>'c), ([]::'a list), (L::'b list)) = []) & \
+\ (map2(f, h#t, []) = []) & \
+\ (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
+
+(*---------------------------------------------------------------------------
+ * Relation "R" holds stepwise in a list
+ *---------------------------------------------------------------------------*)
+function"(finiteRchain ((R::'a=>'a=>bool), ([]::'a list)) = True) & \
+ \ (finiteRchain (R, [x]) = True) & \
+ \ (finiteRchain (R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
+
+
+Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
+ "(finiteRchain((R::'a=>'a=>bool), ([]::'a list)) = True) & \
+ \ (finiteRchain(R, [x]) = True) & \
+ \ (finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
+
+(*---------------------------------------------------------------------------
+ * Quicksort.
+ *---------------------------------------------------------------------------*)
+function"(qsort(ord, []) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ qsort(ord,filter(not o ord x) rst) \
+ \ @[x]@ \
+ \ qsort(ord,filter(ord x) rst))";
+
+Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
+ "(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ qsort(ord,filter(not o ord x) rst) \
+ \ @[x]@ \
+ \ qsort(ord,filter(ord x) rst))";
+
+(*---------------------------------------------------------------------------
+ * Variant.
+ *---------------------------------------------------------------------------*)
+function"variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
+
+Rfunction
+ "measure(%(p::nat*nat list). length(filter(%y. fst(p) <= y) (snd p)))"
+ "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
+
+(*---------------------------------------------------------------------------
+ * Euclid's algorithm
+ *---------------------------------------------------------------------------*)
+function"(gcd ((0::nat),(y::nat)) = y) & \
+ \ (gcd (Suc x, 0) = Suc x) & \
+ \ (gcd (Suc x, Suc y) = \
+ \ (if (y <= x) then gcd(x - y, Suc y) \
+ \ else gcd(Suc x, y - x)))";
+
+
+(*---------------------------------------------------------------------------
+ * Wrong answer because Isabelle rewriter (going bottom-up) attempts to
+ * apply congruence rule for split to "split" but can't because split is only
+ * partly applied. It then fails, instead of just not doing the rewrite.
+ * Tobias has said he'll fix it.
+ *
+ * ... July 96 ... seems to have been fixed.
+ *---------------------------------------------------------------------------*)
+
+Rfunction"measure (split (op+) ::nat*nat=>nat)"
+ "(gcd ((0::nat),(y::nat)) = y) & \
+ \ (gcd (Suc x, 0) = Suc x) & \
+ \ (gcd (Suc x, Suc y) = \
+ \ (if (y <= x) then gcd(x - y, Suc y) \
+ \ else gcd(Suc x, y - x)))";
+
+(*---------------------------------------------------------------------------
+ * A simple nested function.
+ *---------------------------------------------------------------------------*)
+Rfunction"trancl pred_nat"
+ "(g 0 = 0) & \
+ \ (g(Suc x) = g(g x))";
+
+(*---------------------------------------------------------------------------
+ * A clever division algorithm. Primitive recursive.
+ *---------------------------------------------------------------------------*)
+function"(Div(0,x) = (0,0)) & \
+ \ (Div(Suc x, y) = \
+ \ (let (q,r) = Div(x,y) \
+ \ in if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
+
+Rfunction"inv_image pred_nat (fst::nat*nat=>nat)"
+ "(Div(0,x) = (0,0)) & \
+ \ (Div(Suc x, y) = \
+ \ (let q = fst(Div(x,y)); \
+ \ r = snd(Div(x,y)) \
+ \ in \
+ \ if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
+
+(*---------------------------------------------------------------------------
+ * Testing nested contexts.
+ *---------------------------------------------------------------------------*)
+function"(f(0,x) = (0,0)) & \
+ \ (f(Suc x, y) = \
+ \ (let z = x \
+ \ in \
+ \ if (0<y) then (0,0) else f(z,y)))";
+
+
+function"(f(0,x) = (0,0)) & \
+ \ (f(Suc x, y) = \
+ \ (if y = x \
+ \ then (if (0<y) then (0,0) else f(x,y)) \
+ \ else (x,y)))";
+
+
+(*---------------------------------------------------------------------------
+ * Naming trickery in lets.
+ *---------------------------------------------------------------------------*)
+
+(* No trick *)
+function "(test(x, []) = x) & \
+ \ (test(x,h#t) = (let y = Suc x in test(y,t)))";
+
+(* Trick *)
+function"(test(x, []) = x) & \
+ \ (test(x,h#t) = \
+ \ (let x = Suc x \
+ \ in \
+ \ test(x,t)))";
+
+(* Tricky naming, plus nested contexts *)
+function "vary(x, L) = \
+ \ (if (x mem L) \
+ \ then (let x = Suc x \
+ \ in vary(x,L)) \
+ \ else x)";
+
+
+(*---------------------------------------------------------------------------
+ * Handling paired lets of various kinds
+ *---------------------------------------------------------------------------*)
+function
+ "(Fib(0) = Suc 0) & \
+ \ (Fib (Suc 0) = Suc 0) & \
+ \ (Fib (Suc (Suc n)) = \
+ \ (let (x,y) = (Fib (Suc n), Fib n) in x+y))";
+
+
+function
+ "(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ (let (L1,L2) = (filter(not o ord x) rst, \
+ \ filter (ord x) rst) \
+ \ in \
+ \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
+
+function"(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ (let (L1,L2,P) = (filter(not o ord x) rst, \
+ \ filter (ord x) rst, x) \
+ \ in \
+ \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
+
+function"(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
+ \ (qsort(ord, x#rst) = \
+ \ (let (L1,L2) = (filter(not o ord x) rst, \
+ \ filter (ord x) rst); \
+ \ (p,q) = (x,rst) \
+ \ in \
+ \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
+
+
+(*---------------------------------------------------------------------------
+ * A biggish function
+ *---------------------------------------------------------------------------*)
+
+function"(acc1(A,[],s,xss,zs,xs) = \
+\ (if xs=[] then (xss, zs) \
+\ else acc1(A, zs,s,(xss @ [xs]),[],[]))) & \
+\ (acc1(A,(y#ys), s, xss, zs, xs) = \
+\ (let s' = s; \
+\ zs' = (if fst A s' then [] else zs@[y]); \
+\ xs' = (if fst A s' then xs@zs@[y] else xs) \
+\ in \
+\ acc1(A, ys, s', xss, zs', xs')))";
+
+
+(*---------------------------------------------------------------------------
+ * Nested, with context.
+ *---------------------------------------------------------------------------*)
+Rfunction"pred_nat"
+ "(k 0 = 0) & \
+\ (k (Suc n) = (let x = k (Suc 0) \
+\ in if (0=Suc 0) then k (Suc(Suc 0)) else n))";
+
+
+(*---------------------------------------------------------------------------
+ * A function that partitions a list into two around a predicate "P".
+ *---------------------------------------------------------------------------*)
+val {theory,induction,rules,tcs} =
+ Rfunction
+ "inv_image pred_list \
+ \ ((fst o snd)::('a=>bool)*'a list*'a list*'a list => 'a list)"
+
+ "(part(P::'a=>bool, [], l1,l2) = (l1,l2)) & \
+\ (part(P, h#rst, l1,l2) = \
+\ (if P h then part(P,rst, h#l1, l2) \
+\ else part(P,rst, l1, h#l2)))";
+
+
+(*---------------------------------------------------------------------------
+ * Another quicksort.
+ *---------------------------------------------------------------------------*)
+Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
+ "(fqsort(ord,[]) = []) & \
+\ (fqsort(ord, x#rst) = \
+ \ (let less = fst(part((%y. ord y x), rst,([],[]))); \
+ \ more = snd(part((%y. ord y x), rst,([],[]))) \
+ \ in \
+ \ fqsort(ord,less)@[x]@fqsort(ord,more)))";
+
+Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
+ "(fqsort(ord,[]) = []) & \
+\ (fqsort(ord, x#rst) = \
+ \ (let (less,more) = part((%y. ord y x), rst,([],[])) \
+ \ in \
+ \ fqsort(ord,less)@[x]@fqsort(ord,more)))";
+
+
+(* Should fail on repeated variables. *)
+function"(And(x,[]) = x) & \
+ \ (And(y, y#t) = And(y, t))";
+