declare-fun
and define-fun
can be used together.
The problem is that you have a missing parenthesis.
It should be
(declare-fun LEN ((Array Int Int)) Int)
instead of
(declare-fun LEN ((Array Int Int) Int)
Because of the missing parenthesis, the second is actually declaring a function LEN
with two arguments (array and integer), then Z3 generates an error when it can find the resulting sort for this declaration.
Here is a link to the complete example: http://rise4fun.com/Z3/TjNS