[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
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