*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Weird nesting of Quantifiers*From*: Thomas Sewell <tals4 at cam.ac.uk>*Date*: Mon, 15 Feb 2021 10:16:41 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <f40dc7cd-ca92-2e98-ff5e-0b86554e02a2@in.tum.de>*References*: <53699b30cd2bda58ebb26792bacc4e37ac66d5e0.camel@in.tum.de> <f40dc7cd-ca92-2e98-ff5e-0b86554e02a2@in.tum.de>*User-agent*: Roundcube Webmail/1.4.11

You can pull the existentials up so that there are only foralls using the symmetric versions of the all_simps rewrites. Try out apply (simp only: all_simps[symmetric] cong: imp_cong) I'm not sure how consistently that will work, but that followed by regular simplification got me the expected result in all the simple test cases I typed. BTW, I have a dim recollection that I used to see goals like this more often. The "a = .." and "b = .." looks like it came from "(a, b)" being in the image of some projection, maybe. I think I managed to get more

Best regards, Thomas. On 2021-02-14 17:58, Tobias Nipkow wrote:

Hi Peter, I don't think there is any automation for this. I automated "(∀x. x = t --> P x) = P t" and variations on this, but without nested quantifiers. I am sure the latter could be added and it would be worth it, but somebody would need to do it. I am happy to provide pointers... Tobias On 14/02/2021 16:44, Peter Lammich wrote:Hi List,in my current formalization, I frequently end up with goals that Ifeelshould 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, orismy 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

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

**Re: [isabelle] Weird nesting of Quantifiers***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] RC5: Sledgehammer and HOL-Library.Word problems
- Next by Date: Re: [isabelle] Weird nesting of Quantifiers
- Previous by Thread: Re: [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