Re: [isabelle] Sequence case



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





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