Re: [isabelle] Problem analysing cases



Hi Peter,

absMany [ ] [ ] A = A
absMany (x # xs ) [ ] A = A
absMany  [ ] (y # ys) A = A
absMany (x # xs) (y # ys) A = abs x (Ex y. (absMany xs ys A))

I've tried doing this via primrec, with case expressions, let
expressions and if-then-else expressions, but I can't analyse the
second argument.

Primrec cannot do this kind of thing, since it only allows pattern matching on a single argument. However, you should be able to use recdef (or, if you happen to
have a developer's version, the new "fun" command) for this.

Alternatively, you should be able to use case expressions. What did you try exactly, and why didn't it work?

Alex






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