*To*: Lars Hupel <hupel at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Normalizing Pure.conjunction/Pure.all*From*: Makarius <makarius at sketis.net>*Date*: Thu, 23 Mar 2017 17:17:30 +0100*In-reply-to*: <91404e66-4565-45b7-ce52-ac091a4f44e0@in.tum.de>*References*: <91404e66-4565-45b7-ce52-ac091a4f44e0@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

On 21/03/17 15:47, Lars Hupel wrote: > > let's say I have a goal state that looks like this: > > 1. (âx. P x) > 2. (âx. Q x) > > I want to perform mutual induction on "P" and "Q". To use the "induct" > tactic effectively I need to obtain a goal state more like this: > > 1. âx y. P x &&& Q y You did not say how you got there. Note that Goal.recover_conjunction_tac happens to be available for this, because it is occasionally needed in obscure situations. > That is, quantification is outside. Then, I can use the usual mechanisms > ("Subgoal.FOCUS_PARAMS") to set up a local context, which makes my goal > state look like this: > > 1. P :000 &&& Q :001 > > ... which in turn can be fed to "induct". > > I currently have a solution which goes from my initial goal state to the > desired goal state by applying these rewrite rules: > > âP Q. ((âx. PROP P x) &&& PROP Q) â (âx. PROP P x &&& PROP Q) > âP Q. (PROP P &&& (âx. PROP Q x)) â (âx. PROP P &&& PROP Q x) > > Is there anything out there that already does what I want? The last two rewrite rules look OK for such special rearrangements. E.g. when wrapped-up into a separate proof method. There are very few such tools to operate in Pure rule or goal structure, because the usual Isar way is to operate on the problem structure as provided by the user, and avoid loosing that structure in the first place. Sometimes that is difficult or impossible, then special tweaks need to be applied. So looking from a distance, the canonical question is: Where does the situation of two separate subgoals with separate parameter scopes come from? Is that the result of another tool? Makarius

**Follow-Ups**:**Re: [isabelle] Normalizing Pure.conjunction/Pure.all***From:*Lars Hupel

**References**:**[isabelle] Normalizing Pure.conjunction/Pure.all***From:*Lars Hupel

- Previous by Date: [isabelle] CFP: The 11th International Workshop on Reachability Problems (RP'17)
- Next by Date: Re: [isabelle] Normalizing Pure.conjunction/Pure.all
- Previous by Thread: [isabelle] Normalizing Pure.conjunction/Pure.all
- Next by Thread: Re: [isabelle] Normalizing Pure.conjunction/Pure.all
- Cl-isabelle-users March 2017 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