Re: [isabelle] resolve current subgoal with matching premise



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.