Re: [isabelle] Normalizing Pure.conjunction/Pure.all



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






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