TFL/test.sml

moved split_tac

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))";