Re: [isabelle] Sequence case

Thank you very much, I have resolved any problem (for the moment) using
Dropwhile and HD.

Best regards

On 9/20/06, Brian Huffman <brianh at> wrote:

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
function using primrec, because 'a seq is not an inductive datatype: The
also includes infinite sequences, so the recursion may not even terminate.
define a new recursive function, you could use the least-fixed-point
"fix", but you would have to manually prove that the recursion is

> 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
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 *
lift, which is probably pretty close to what you want.

- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.