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

On Feb 16, 2011 5:31am, Brian Huffman <brianh at> wrote:
On Tue, Feb 15, 2011 at 8:52 PM, John Munroe munddr at> wrote:

> Hi,


> Does anyone know of a good way to rewrite a definition wrt. other

> axioms? For example, given:


> a1: "ALL x. fx = gx + h x"

> a2: "ALL x. gx = mx * n x"


> I'm trying to get a new axiom:


> ax1': "ALL x. fx = (mx * nx) + h x", ie 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]

Thanks. Do you know what the ML functions are for getting the same result at the ML level?


- Brian

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