Re: [isabelle] [isabelle-dev] Rewriting wrt other axioms



On Tue, Feb 15, 2011 at 8:52 PM, John Munroe <munddr at gmail.com> wrote:
> Hi,
>
> Does anyone know of a good way to rewrite a definition wrt. other
> axioms? For example, given:
>
> a1: "ALL x. f x = g x + h x"
> a2: "ALL x. g x = m x * n x"
>
> I'm trying to get a new axiom:
>
> ax1': "ALL x. f x = (m x * n x) + h x", i.e. rewriting a1 using a2. Is
> there already an existing mechanism that does this? Otherwise, what is
> the best angle to approach this?

Try using the "simplified" attribute, like this:

thm a1 [simplified a2]

- Brian





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