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.