[isabelle] Problem analysing cases


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?



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