[isabelle-dev] Rewriting wrt other axioms

John Munroe munddr at gmail.com
Wed Feb 16 05:52:57 CET 2011


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?


More information about the isabelle-dev mailing list