[isabelle] resolve current subgoal with matching premise



Dear all,

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.

The reason why I'm asking is that "blast_tac" is very slow on some goals of this shape that I obtain by another hand-written tactic and I hope to speed things up.

cheers

chris




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