Email Gateway (Aug 18 2022 at 09:40): Email Gateway (Aug 18 2022 at 09:40):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
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
Email Gateway (Aug 18 2022 at 09:41):From: Lawrence Paulson <lp15@cam.ac.uk>
The "case" expression in Isabelle is rather restrictive: you have to
list the cases in the exact same order as they appear in the
corresponding datatype declaration, and _ is not allowed.
Larry Paulson
Email Gateway (Aug 18 2022 at 09:41):From: Brian Huffman <brianh@csee.ogi.edu>
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.
Email Gateway (Aug 18 2022 at 09:41):From: Tobias Nipkow <nipkow@in.tum.de>
Probably because "_" is not supported and the order of the cases must be
the same as in the domain definition.
Tobias
Email Gateway (Aug 18 2022 at 09:41):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Thank you very much, I have resolved any problem (for the moment) using
Dropwhile and HD.
Best regards
Gabriele
Last updated: May 03 2024 at 04:19 UTC