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


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).


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


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