[isabelle] Sequence case



Hello,
I'm trying to write a function that find the first occurrence of an action
in an automaton execution, where an execution is a lift sequence of pairs.
My idea is to use pattern matching and case.

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:
*** exception TERM raised: Error in case expression:
*** Not a datatype constructor: Cfun.Rep_CFun
*** Error in parse translation for "_case_syntax"
*** At command "primrec".

Where is the problem?

I tried to replace "x##xs" with "(x##xs)lift" but nothing change.

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.

Can you help me?
Excuse me for my frequent questions.

Thanks
Gabriele




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