TFL/test.sml
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
paulson@2112
     2
fun read thy = term_of o cread thy;
paulson@2112
     3
fun Term s = read WF1.thy s;
paulson@2112
     4
paulson@2112
     5
fun Rfunc thy R eqs =
paulson@2112
     6
   let val {induction,rules,theory,tcs} = 
paulson@2112
     7
              timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
paulson@2112
     8
   in {induction=induction, rules=rules, theory=theory, 
paulson@2112
     9
       tcs = map (cterm_of (sign_of theory)) tcs}
paulson@2112
    10
   end;
paulson@2112
    11
paulson@2112
    12
val Rfunction = Rfunc WF1.thy;
paulson@2112
    13
paulson@2112
    14
fun function tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
paulson@2112
    15
paulson@2112
    16
paulson@2112
    17
(*---------------------------------------------------------------------------
paulson@2112
    18
 * Factorial. Notice how functions without pattern matching are often harder 
paulson@2112
    19
 * to deal with than those with! Unfortunately, not all functions can be 
paulson@2112
    20
 * described purely by pattern matching, e.g., "variant" as below.
paulson@2112
    21
 *---------------------------------------------------------------------------*)
paulson@2112
    22
function "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
paulson@2112
    23
paulson@2112
    24
Rfunction"pred_nat"
paulson@2112
    25
         "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
paulson@2112
    26
paulson@2112
    27
function "(Fact 0 = (Suc 0)) & \
paulson@2112
    28
     \    (Fact (Suc x) = (Fact x * Suc x))";
paulson@2112
    29
paulson@2112
    30
Rfunction "pred_nat"
paulson@2112
    31
          "(Fact 0 = (Suc 0)) & \
paulson@2112
    32
      \    (Fact (Suc x) = (Fact x * Suc x))";
paulson@2112
    33
paulson@2112
    34
(*---------------------------------------------------------------------------
paulson@2112
    35
 * Fibonacci.
paulson@2112
    36
 *---------------------------------------------------------------------------*)
paulson@2112
    37
function "(Fib 0 = (Suc 0)) &  \
paulson@2112
    38
     \    (Fib (Suc 0) = (Suc 0)) & \
paulson@2112
    39
     \    (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
paulson@2112
    40
paulson@2112
    41
(* "<" doesn't currently work smoothly *)
paulson@2112
    42
Rfunction"{p::(nat*nat). fst p < snd p}"
paulson@2112
    43
         "(Fib 0 = (Suc 0)) & \
paulson@2112
    44
     \    (Fib (Suc 0) = (Suc 0)) & \
paulson@2112
    45
     \    (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
paulson@2112
    46
paulson@2112
    47
paulson@2112
    48
(* "trancl pred" means "<" and works better *)
paulson@2112
    49
Rfunction"trancl pred_nat"
paulson@2112
    50
         "(Fib 0 = (Suc 0)) & \
paulson@2112
    51
     \    (Fib (Suc 0) = (Suc 0)) & \
paulson@2112
    52
     \    (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
paulson@2112
    53
paulson@2112
    54
(*---------------------------------------------------------------------------
paulson@2112
    55
 * Ackermann.
paulson@2112
    56
 *---------------------------------------------------------------------------*)
paulson@2112
    57
Rfunction"pred_nat ** pred_nat"
paulson@2112
    58
         "(Ack (0,n) =  (n + Suc 0)) & \
paulson@2112
    59
    \    (Ack (Suc m,0) = (Ack (m, Suc 0))) & \
paulson@2112
    60
    \    (Ack (Suc m, Suc n) = Ack (m, Ack (Suc m, n)))";
paulson@2112
    61
paulson@2112
    62
(*---------------------------------------------------------------------------
paulson@2112
    63
 * Almost primitive recursion. 
paulson@2112
    64
 *---------------------------------------------------------------------------*)
paulson@2112
    65
function"(map2(f, [], L) = []) & \
paulson@2112
    66
    \    (map2(f, h#t, []) = []) & \
paulson@2112
    67
    \    (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
paulson@2112
    68
paulson@2112
    69
(* Swap arguments *)
paulson@2112
    70
function"(map2(([],L), f) = []) & \
paulson@2112
    71
    \    (map2((h#t, []), f) = []) &  \
paulson@2112
    72
    \    (map2((h1#t1, h2#t2), f) = f h1 h2 # map2((t1,t2),f))";
paulson@2112
    73
paulson@2112
    74
Rfunction
paulson@2112
    75
   "measure((length o fst o snd)::('a=>'b=>'c)*'a list*'b list => nat)"
paulson@2112
    76
    "(map2((f::'a=>'b=>'c), ([]::'a list), (L::'b list)) = [])  & \
paulson@2112
    77
\    (map2(f, h#t, []) = []) & \
paulson@2112
    78
\    (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
paulson@2112
    79
paulson@2112
    80
(*---------------------------------------------------------------------------
paulson@2112
    81
 * Relation "R" holds stepwise in a list
paulson@2112
    82
 *---------------------------------------------------------------------------*)
paulson@2112
    83
function"(finiteRchain ((R::'a=>'a=>bool),  ([]::'a list)) = True) & \
paulson@2112
    84
    \    (finiteRchain (R, [x]) = True) & \
paulson@2112
    85
    \    (finiteRchain (R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
paulson@2112
    86
paulson@2112
    87
paulson@2112
    88
Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
paulson@2112
    89
         "(finiteRchain((R::'a=>'a=>bool),  ([]::'a list)) = True) & \
paulson@2112
    90
     \    (finiteRchain(R, [x]) = True) & \
paulson@2112
    91
     \    (finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
paulson@2112
    92
paulson@2112
    93
(*---------------------------------------------------------------------------
paulson@2112
    94
 * Quicksort.
paulson@2112
    95
 *---------------------------------------------------------------------------*)
paulson@2112
    96
function"(qsort(ord,  []) = []) & \
paulson@2112
    97
    \    (qsort(ord, x#rst) = \
paulson@2112
    98
    \       qsort(ord,filter(not o ord x) rst) \
paulson@2112
    99
    \       @[x]@      \
paulson@2112
   100
    \       qsort(ord,filter(ord x) rst))";
paulson@2112
   101
paulson@2112
   102
Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
paulson@2112
   103
         "(qsort((ord::'a=>'a=>bool),  ([]::'a list))  = []) & \
paulson@2112
   104
     \    (qsort(ord, x#rst) = \
paulson@2112
   105
     \       qsort(ord,filter(not o ord x) rst) \
paulson@2112
   106
     \       @[x]@  \
paulson@2112
   107
     \       qsort(ord,filter(ord x) rst))";
paulson@2112
   108
paulson@2112
   109
(*---------------------------------------------------------------------------
paulson@2112
   110
 * Variant.
paulson@2112
   111
 *---------------------------------------------------------------------------*)
paulson@2112
   112
function"variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
paulson@2112
   113
paulson@2112
   114
Rfunction
paulson@2112
   115
 "measure(%(p::nat*nat list). length(filter(%y. fst(p) <= y) (snd p)))"
paulson@2112
   116
 "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
paulson@2112
   117
paulson@2112
   118
(*---------------------------------------------------------------------------
paulson@2112
   119
 * Euclid's algorithm
paulson@2112
   120
 *---------------------------------------------------------------------------*)
paulson@2112
   121
function"(gcd ((0::nat),(y::nat)) = y) & \
paulson@2112
   122
    \    (gcd (Suc x, 0) = Suc x) & \
paulson@2112
   123
    \    (gcd (Suc x, Suc y) =      \
paulson@2112
   124
    \        (if (y <= x) then gcd(x - y, Suc y) \
paulson@2112
   125
    \                     else gcd(Suc x, y - x)))";
paulson@2112
   126
paulson@2112
   127
paulson@2112
   128
(*---------------------------------------------------------------------------
paulson@2112
   129
 * Wrong answer because Isabelle rewriter (going bottom-up) attempts to
paulson@2112
   130
 * apply congruence rule for split to "split" but can't because split is only
paulson@2112
   131
 * partly applied. It then fails, instead of just not doing the rewrite.
paulson@2112
   132
 * Tobias has said he'll fix it.
paulson@2112
   133
 *
paulson@2112
   134
 * ... July 96 ... seems to have been fixed.
paulson@2112
   135
 *---------------------------------------------------------------------------*)
paulson@2112
   136
 
paulson@2112
   137
Rfunction"measure (split (op+) ::nat*nat=>nat)"
paulson@2112
   138
         "(gcd ((0::nat),(y::nat)) = y) & \
paulson@2112
   139
        \ (gcd (Suc x, 0) = Suc x) & \
paulson@2112
   140
        \ (gcd (Suc x, Suc y) = \
paulson@2112
   141
        \     (if (y <= x) then gcd(x - y, Suc y) \
paulson@2112
   142
        \                  else gcd(Suc x, y - x)))";
paulson@2112
   143
paulson@2112
   144
(*---------------------------------------------------------------------------
paulson@2112
   145
 * A simple nested function.
paulson@2112
   146
 *---------------------------------------------------------------------------*)
paulson@2112
   147
Rfunction"trancl pred_nat"
paulson@2112
   148
         "(g 0 = 0) & \
paulson@2112
   149
        \ (g(Suc x) = g(g x))";
paulson@2112
   150
paulson@2112
   151
(*---------------------------------------------------------------------------
paulson@2112
   152
 * A clever division algorithm. Primitive recursive.
paulson@2112
   153
 *---------------------------------------------------------------------------*)
paulson@2112
   154
function"(Div(0,x) = (0,0)) & \
paulson@2112
   155
       \ (Div(Suc x, y) =     \
paulson@2112
   156
       \     (let (q,r) = Div(x,y) \
paulson@2112
   157
       \      in if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
paulson@2112
   158
paulson@2112
   159
Rfunction"inv_image pred_nat (fst::nat*nat=>nat)"
paulson@2112
   160
         "(Div(0,x) = (0,0)) & \
paulson@2112
   161
        \ (Div(Suc x, y) =     \
paulson@2112
   162
        \    (let q = fst(Div(x,y)); \
paulson@2112
   163
        \         r = snd(Div(x,y))  \
paulson@2112
   164
        \     in                     \
paulson@2112
   165
        \     if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
paulson@2112
   166
paulson@2112
   167
(*---------------------------------------------------------------------------
paulson@2112
   168
 * Testing nested contexts.
paulson@2112
   169
 *---------------------------------------------------------------------------*)
paulson@2112
   170
function"(f(0,x) = (0,0)) & \
paulson@2112
   171
       \ (f(Suc x, y) = \
paulson@2112
   172
       \     (let z = x \
paulson@2112
   173
       \      in        \
paulson@2112
   174
       \      if (0<y) then (0,0) else f(z,y)))";
paulson@2112
   175
paulson@2112
   176
paulson@2112
   177
function"(f(0,x) = (0,0)) & \
paulson@2112
   178
       \ (f(Suc x, y) =     \
paulson@2112
   179
       \      (if y = x     \
paulson@2112
   180
       \       then (if (0<y) then (0,0) else f(x,y)) \
paulson@2112
   181
       \       else (x,y)))";
paulson@2112
   182
paulson@2112
   183
paulson@2112
   184
(*---------------------------------------------------------------------------
paulson@2112
   185
 * Naming trickery in lets.
paulson@2112
   186
 *---------------------------------------------------------------------------*)
paulson@2112
   187
paulson@2112
   188
(* No trick *)
paulson@2112
   189
function "(test(x, []) = x) & \
paulson@2112
   190
        \ (test(x,h#t) = (let y = Suc x in test(y,t)))";
paulson@2112
   191
paulson@2112
   192
(* Trick *)
paulson@2112
   193
function"(test(x, []) = x) & \
paulson@2112
   194
       \ (test(x,h#t) =      \
paulson@2112
   195
       \     (let x = Suc x  \
paulson@2112
   196
       \      in             \
paulson@2112
   197
       \      test(x,t)))";
paulson@2112
   198
paulson@2112
   199
(* Tricky naming, plus nested contexts *)
paulson@2112
   200
function "vary(x, L) =  \
paulson@2112
   201
        \   (if (x mem L) \
paulson@2112
   202
        \    then (let x = Suc x \
paulson@2112
   203
        \          in vary(x,L)) \
paulson@2112
   204
        \    else x)";
paulson@2112
   205
paulson@2112
   206
paulson@2112
   207
(*---------------------------------------------------------------------------
paulson@2112
   208
 * Handling paired lets of various kinds
paulson@2112
   209
 *---------------------------------------------------------------------------*)
paulson@2112
   210
function
paulson@2112
   211
    "(Fib(0) = Suc 0) &  \
paulson@2112
   212
   \ (Fib (Suc 0) = Suc 0) & \
paulson@2112
   213
   \ (Fib (Suc (Suc n)) =    \
paulson@2112
   214
   \     (let (x,y) = (Fib (Suc n), Fib n) in x+y))";
paulson@2112
   215
paulson@2112
   216
paulson@2112
   217
function
paulson@2112
   218
   "(qsort((ord::'a=>'a=>bool),  ([]::'a list))   = []) &  \
paulson@2112
   219
  \ (qsort(ord, x#rst) = \
paulson@2112
   220
  \     (let (L1,L2) = (filter(not o ord x) rst, \
paulson@2112
   221
  \                     filter (ord x) rst) \
paulson@2112
   222
  \      in  \
paulson@2112
   223
  \      qsort(ord,L1)@[x]@qsort(ord,L2)))";
paulson@2112
   224
paulson@2112
   225
function"(qsort((ord::'a=>'a=>bool),  ([]::'a list))   = []) & \
paulson@2112
   226
       \ (qsort(ord, x#rst) = \
paulson@2112
   227
       \    (let (L1,L2,P) = (filter(not o ord x) rst, \
paulson@2112
   228
       \                      filter (ord x) rst, x)   \
paulson@2112
   229
       \     in \
paulson@2112
   230
       \     qsort(ord,L1)@[x]@qsort(ord,L2)))";
paulson@2112
   231
paulson@2112
   232
function"(qsort((ord::'a=>'a=>bool),  ([]::'a list))   = []) & \
paulson@2112
   233
       \ (qsort(ord, x#rst) = \
paulson@2112
   234
       \     (let (L1,L2) = (filter(not o ord x) rst, \
paulson@2112
   235
       \                     filter (ord x) rst);     \
paulson@2112
   236
       \            (p,q) = (x,rst) \
paulson@2112
   237
       \      in \
paulson@2112
   238
       \      qsort(ord,L1)@[x]@qsort(ord,L2)))";
paulson@2112
   239
paulson@2112
   240
paulson@2112
   241
(*---------------------------------------------------------------------------
paulson@2112
   242
 * A biggish function
paulson@2112
   243
 *---------------------------------------------------------------------------*)
paulson@2112
   244
paulson@2112
   245
function"(acc1(A,[],s,xss,zs,xs) = \
paulson@2112
   246
\              (if xs=[] then (xss, zs) \
paulson@2112
   247
\                        else acc1(A, zs,s,(xss @ [xs]),[],[]))) & \
paulson@2112
   248
\         (acc1(A,(y#ys), s, xss, zs, xs) = \
paulson@2112
   249
\              (let s' = s; \
paulson@2112
   250
\                  zs' = (if fst A s' then [] else zs@[y]); \
paulson@2112
   251
\                  xs' = (if fst A s' then xs@zs@[y] else xs) \
paulson@2112
   252
\               in  \
paulson@2112
   253
\               acc1(A, ys, s', xss, zs', xs')))";
paulson@2112
   254
paulson@2112
   255
paulson@2112
   256
(*---------------------------------------------------------------------------
paulson@2112
   257
 * Nested, with context.
paulson@2112
   258
 *---------------------------------------------------------------------------*)
paulson@2112
   259
Rfunction"pred_nat"
paulson@2112
   260
  "(k 0 = 0) & \
paulson@2112
   261
\  (k (Suc n) = (let x = k (Suc 0)  \
paulson@2112
   262
\                in if (0=Suc 0) then k (Suc(Suc 0)) else n))";
paulson@2112
   263
paulson@2112
   264
paulson@2112
   265
(*---------------------------------------------------------------------------
paulson@2112
   266
 * A function that partitions a list into two around a predicate "P".
paulson@2112
   267
 *---------------------------------------------------------------------------*)
paulson@2112
   268
val {theory,induction,rules,tcs} = 
paulson@2112
   269
  Rfunction
paulson@2112
   270
   "inv_image pred_list \
paulson@2112
   271
    \  ((fst o snd)::('a=>bool)*'a list*'a list*'a list => 'a list)"
paulson@2112
   272
paulson@2112
   273
  "(part(P::'a=>bool, [], l1,l2) = (l1,l2)) & \
paulson@2112
   274
\  (part(P, h#rst, l1,l2) = \
paulson@2112
   275
\       (if P h then part(P,rst, h#l1,  l2) \
paulson@2112
   276
\               else part(P,rst,  l1,  h#l2)))";
paulson@2112
   277
paulson@2112
   278
  
paulson@2112
   279
(*---------------------------------------------------------------------------
paulson@2112
   280
 * Another quicksort. 
paulson@2112
   281
 *---------------------------------------------------------------------------*)
paulson@2112
   282
Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
paulson@2112
   283
 "(fqsort(ord,[]) = []) & \
paulson@2112
   284
\ (fqsort(ord, x#rst) = \
paulson@2112
   285
 \   (let less = fst(part((%y. ord y x), rst,([],[]))); \
paulson@2112
   286
  \       more = snd(part((%y. ord y x), rst,([],[]))) \
paulson@2112
   287
   \  in \
paulson@2112
   288
    \ fqsort(ord,less)@[x]@fqsort(ord,more)))";
paulson@2112
   289
paulson@2112
   290
Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
paulson@2112
   291
 "(fqsort(ord,[]) = []) & \
paulson@2112
   292
\  (fqsort(ord, x#rst) = \
paulson@2112
   293
 \   (let (less,more) = part((%y. ord y x), rst,([],[])) \
paulson@2112
   294
  \   in \
paulson@2112
   295
   \  fqsort(ord,less)@[x]@fqsort(ord,more)))";
paulson@2112
   296
paulson@2112
   297
paulson@2112
   298
(* Should fail on repeated variables. *)
paulson@2112
   299
function"(And(x,[]) = x) & \
paulson@2112
   300
      \  (And(y, y#t) = And(y, t))";
paulson@2112
   301