# Re: [isabelle] Tactic to force simplification?

Dear Holden,
you might use trans[OF ...] as follows.
context
fixes P :: "'a => bool" and f g h :: "'a => 'a"
begin
lemma simp_me: "P x ==> f x = g x" sorry
lemma to_prove: "f x = h x"
apply (rule trans[OF simp_me])
sorry
end
Cheers,
René
Am 04.08.2014 um 14:04 schrieb Holden Lee <hl422 at cam.ac.uk>:
> 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.*