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?


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