# Re: [isabelle] Automatic derivation of a total order on datatypes

```The add_simprocs mechanism from HOL/Orderings seems to be obscuring things.

Normally I would construct and name the simproc objects explicitly, e.g.:

val antisym_le_simproc = Simplifier.simproc_global_i
@{theory} "antisym le" [ at {term "(x::'a::order) <= y"}] prove_antisym_le

(etc)

These are later added to the global simpset, e.g.:

Simplifier.map_simpset_global (fn ss => ss addsimprocs [antisym_le_simproc])

You can then add the simprocs to custom simpsets any time you want, e.g.:

HOL_basic_ss addsimprocs [antisym_le_simproc]

```
I didn't read much of Orderings.thy. It may be that this is all more complicated because it depends on parameters which are here unknown. In that case you could produce a simproc function, or organise some Data object to store the instantiations as they are created so they can later be looked up, or similar.
```

```
It would be nice if it were easier to follow Brian's advice. This approach of custom simpsets is the norm in HOL4. Unfortunately in Isabelle I often find myself missing a name for, say, the simplifications needed for arithmetic on numeral natural numbers. I have often ended up working with the giant kludge of writing the simproc which spots a pattern (e.g. numeral + numeral), simplifies the pattern with a big unpredictable simpset (e.g. global_simpset_of @{theory Nat}) and then tries to normalise and check (e.g. rewrite Suc 0 -> 1, check we have a numeral).
```
Yours,
Thomas.

On 16/11/12 23:57, René Thiemann wrote:
```
```So the rule less_bool_def (x<  y == ~ x&  y) simplifies (op<  x_0) to (op&  (~ x_0))
in the goal, but not in the premise. This is what I do not understand when calling
asm_full_simp_tac.
```
```Perhaps the occurrence of "(op<  x_0)" in the goal was eta-expanded,
while other occurrences were not. You should disable eta-contraction
in the pretty-printer to see whether this is the case.

My general advice, when writing internal ML tactics, is to use
simp_tac only with purpose-built simpsets. Usually I start with
HOL_basic_ss and add only the rules I need; I never use the simpset
from the current context, as the behavior is just too unpredictable.
```
```Hi Brian,

thanks for the hints. It is definitely a good idea to use special-purpose simpsets,
however, it is not clear to me, how this can be built, since I had difficulties to integrate simprocs, etc. which were essential for the simplication.

E.g., in Orderings,

add_simprocs [
("antisym le", ["(x::'a::order)<= y"], prove_antisym_le),
("antisym less", ["~ (x::'a::linorder)<  y"], prove_antisym_less)
]

is used to add the locally defined "prove_antisym_le"-simproc to the global simpset.

It would be nice, if I can just add these simprocs to HOL_basic_ss, however I did not see a way to access them, so that afterwards I can add them via addsimprocs:

- using
simpset_of @{context} |>  dest_ss |>  #procs |>  List.find (fn a =>  fst a = "antisym le")
delivers an entry, however of type string * cterm list and not string * simproc!

- using
Simplifier.the_simproc @{context} "antisym le"
would deliver a simproc as return type, but
one gets an error message: Undefined simproc: "antisym le"

- so my current workaround is to use

val my_starting_simpset = simpset_of @{context}
delsimps (simpset_of @{context} |>  dest_ss |>  #simps |>  map snd)
addsimps @{thms HOL.simp_thms}

but I think this is not really a nice workaround.

Cheers,
René

```
```

```

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