[isabelle] Tactic to force simplification?



Often, I have something I want to prove, say

f x = h x

and there is a simplification I want to use, say

P x => f x = g x

I would like Isabelle to replace the goal

1. f x = h x

by

1. P x
2. g x = h x.

Is there a simple way to do this (without a structured proof)? (Also note
that the x might be inside a !! quantifier, in which case I would want

1. !!x. Q x => f x = h x

would be replaced by

1. !!x. Q x => P x
2. !!x. Q x => g x = h x.)

Thanks,
Holden



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