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



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