On Tuesday 19 September 2006 06:41, Gabriele Pozzani wrote:
> So I wrote:
> consts first_occur::"('a × 'b) lift seq => 'a => 'b"
> primrec
> "first_occur ex a == (case ex of
> x##xs => if (fst(x)=a) then snd(x) else (first_occur xs a)
>
> | _ => arbitrary)"
>
> But it don't work and Isabelle stops with the follow error:
Even if you get around the parse error, it is still impossible to define
this
function using primrec, because 'a seq is not an inductive datatype: The
type
also includes infinite sequences, so the recursion may not even terminate.
To
define a new recursive function, you could use the least-fixed-point
operator
"fix", but you would have to manually prove that the recursion is
continuous.
> I tried to write another solution using the function Filter but Isabelle
> tell me that
> "Filter P"::('a × 'b) lift seq -> ('a × 'b) lift seq
> is not of function type.
The type 'a -> 'b is the HOLCF type of continuous functions (it is a
predicate
subtype of 'a => 'b). So you need to use the HOLCF continuous application
operator with it, which is written as an infix $ or \<cdot> in xsymbol
syntax. Similarly for the HD constant, which you will also probably need.
The term "HD $ (Filter (%x. fst(x)=a) $ xs)" returns a value of type ('a *
'b)
lift, which is probably pretty close to what you want.
- Brian