*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Weird nesting of Quantifiers*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 14 Feb 2021 18:58:26 +0100*In-reply-to*: <53699b30cd2bda58ebb26792bacc4e37ac66d5e0.camel@in.tum.de>*References*: <53699b30cd2bda58ebb26792bacc4e37ac66d5e0.camel@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:78.0) Gecko/20100101 Thunderbird/78.7.1

Hi Peter,

Tobias On 14/02/2021 16:44, Peter Lammich wrote:

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

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Weird nesting of Quantifiers***From:*Thomas Sewell

**References**:**[isabelle] Weird nesting of Quantifiers***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Some more polishing of the multiset theory
- Next by Date: [isabelle] Isabelle2021-RC6 available for applications
- Previous by Thread: [isabelle] Weird nesting of Quantifiers
- Next by Thread: Re: [isabelle] Weird nesting of Quantifiers
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list