# [isabelle] Problem analysing cases

Hi

`I've got a function which takes two lists and a formula, and returns
``a formula, i.e.
`
absMany :: "'a list => 'b list => form => form"

`which I want to have the following behaviour (the two middle cases
``will never be used, since I want to use the function only after I've
``enforced length X = length Y)
`
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.
`
I've also tried coming at it from another angle, so that
absMany :: " 'a list => form => form"

`and "hiding" the second list in the formula, but again in the crucial
``case where both lists are non-empty I cannot break both lists down to
``talk of an expression involving x,y, xs and ys.
`

`I looked into mutual recursion, but because the datatypes are not
``mutually recursive, I didn't think it was applicable.
`
Does anyone know how to do this properly?
Cheers
Peter

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