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

with

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.
>
> 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.