Email Gateway (Aug 18 2022 at 17:03): Email Gateway (Aug 18 2022 at 17:03):From: Brian Huffman <brianh@cs.pdx.edu>
Try using the "simplified" attribute, like this:
thm a1 [simplified a2]
Email Gateway (Aug 18 2022 at 17:03):From: munddr@gmail.com
On Feb 16, 2011 5:31am, Brian Huffman <brianh@cs.pdx.edu> wrote:
On Tue, Feb 15, 2011 at 8:52 PM, John Munroe munddr@gmail.com> 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?
Thanks
John
- Brian
Email Gateway (Aug 18 2022 at 17:04):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
John,
the ML functions are simplify, asm_full_simplify, etc (I think the
latter is the precise equivalent of thm a1 [simplified a2], see s9.4 of
the Reference Manual (ref.{dvi,pdf})
They take a simpset argument - I think to get the equivalent of
thm a1 [simplified a2] you would want something like
asm_full_simplify (HOL_basic_ss addsimps [a2]) a1 ;
Unfortunately HOL_basic_ss doesn't seem to exist anymore. You could try
empty_ss instead (I've never used it myself). (see s9.2.2)
Or try rewrite_rule [a2] a1 (see s4.1.3 of the Reference Manual)
Jeremy
Email Gateway (Aug 18 2022 at 17:04):From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Feb 16, 2011 at 4:57 AM, Jeremy Dawson
<jlcaadawson@netspeed.com.au> wrote:
Unfortunately HOL_basic_ss doesn't seem to exist anymore. You could try
empty_ss instead (I've never used it myself). (see s9.2.2)
HOL_basic_ss still exists! I am using it all over the place in the
implementation of the HOLCF domain package, and a quick grep of the
current sources shows that it is used in plenty of other places too.
Or try rewrite_rule [a2] a1 (see s4.1.3 of the Reference Manual)
I believe that Meta_Simplifier.rewrite_rule corresponds precisely to
the "unfolded" attribute, which is similar to "simplified", except
that it uses a more basic kind of rewriting (no pre-processing of
rules, no using local assumptions, no congruence rules, etc.)
Email Gateway (Aug 18 2022 at 17:04):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Brian Huffman wrote:
sorry - my mistake - I'd only loaded Pure (which was all I'd ever built
for Isabelle2009-2)
Jeremy
Last updated: Apr 25 2024 at 01:08 UTC