# [isabelle] Weird nesting of Quantifiers

Hi List,
in my current formalization, I frequently end up with goals that I feel
should be solvable by auto or blast, but they get stuck due to
containing a precondition similar to this:
(∀a. (∃x y. a = f x y ∧ P x y) ⟶ Q a)
The exact precondition can vary in the number of universal and
existential quantified variables, and the position and number of the
determining a = ... conjuncts, e.g.
(∀a b. (∃x y. a = f x y ∧ P x y ∧ b=g x) ⟶ Q a b)
Anyway, the above preconditions are, obviously, equal to the following
simpler ones:
"∀x y. P x y ⟶ Q (f x y)"
"∀x y. P x y ⟶ Q (f x y) (g x)"
currently, I have to manually prove these equivalences, for every
instance of quantified variables, etc, and then can solve the goal
easily by rewriting and auto.
Is there any way, e.g. a simproc or so, to automate this process, or is
my only solution to bloat up the otherwise fully automatic proofs by
those weird auxiliary lemmas (of which I could, of course, prove
instances for the most common cases globally and add them to the
simpset)
--
Peter

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