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

```On 02/16/2011 10:25 PM, munddr at gmail.com wrote:
```
```On Feb 16, 2011 5:31am, Brian Huffman <brianh at cs.pdx.edu> wrote:
```
```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. 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
```
```

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

```

• References:

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