Re: [isabelle] Tactic to force simplification?
Thanks. One more wrinkle: In general I would like this to work if there
were other terms present. For example, to replace
1. f x + f1 x = h x + h1 x
1. P x
2. g x + f1 x = h x + h1 x. [in full generality, it would be some function
F x (f x) on the LHS, to be replaced by F x (g x).]
Would this be possible?
2014-08-04 13:23 GMT+01:00 René Thiemann <rene.thiemann at uibk.ac.at>:
> Dear Holden,
> you might use trans[OF ...] as follows.
> fixes P :: "'a => bool" and f g h :: "'a => 'a"
> lemma simp_me: "P x ==> f x = g x" sorry
> lemma to_prove: "f x = h x"
> apply (rule trans[OF simp_me])
> 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