Re: [isabelle] resolve current subgoal with matching premise



In "$AFP/Automatic_Refinement/Lib/Refine_Util", there is a method 
rprems.

apply (rprems)  -- resolve with the first matching premise
apply (rprems n) -- resolve with the nth premise

I frequently use this to apply induction hypothesis in 
apply-style/automatic proofs.

Cheers,
  Peter


On Do, 2014-12-04 at 22:37 +0100, Jasmin Christian Blanchette wrote:
> Hi Chris,
> 
> > is there an easy way in Isabelle/ML to replace the current subgoal by the assumptions of the first premise whose conclusion matches it?
> > 
> > Example:
> > I have a subgoal of the shape
> > 
> > !! a1 ... aN.
> >  (!! b1 ... bK. ...) ==>
> >  ...
> >  (!! i1 ... iM. ... ==> P iI) (*[*]*) ==>
> >  ...
> >  (!! z1 ... zL. ...) ==> P aJ
> > 
> > and would like to replace it by the premises of [*]. I think this should be easy but could figure it out immediately.
> 
> You could try
> 
>     apply ((drule meta_spec)+, erule meta_mp)
> 
> E.g.:
> 
>     lemma "!! a1 aJ aN.
>      (!! b1 bK. q b1 bK) ==>
>      (!! i1 iI iM. r i1 iI iM ==> P iI) ==>
>      (!! z1 zL. s z1 zL) ==> P aJ"
>     apply ((drule meta_spec)+, erule meta_mp)
> 
> If you do this at the tactic level (or use the "back" command), the built-in nondeterminism will make it work more generally for any premise whose conclusion matches the subgoal's conclusion.
> 
> I hope this helps.
> 
> Cheers,
> 
> Jasmin
> 
> 






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