*To*: Brian Huffman <huffman.brian.c at gmail.com>*Subject*: Re: [isabelle] Automatic derivation of a total order on datatypes*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Fri, 16 Nov 2012 13:57:51 +0100*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAMXsiYPJkwpXQd2XVtpfLcesY+NC5q674PSSvHjKe+rDjhaxA@mail.gmail.com>*References*: <50A2D9ED.7060406@in.tum.de> <50A343ED.2060501@kit.edu> <48D999C6-55BE-45B4-99BA-62B571846791@uibk.ac.at> <CALOYH0FLfej+JsENGuMjE=Jz8LNqXKUsyxRHyTLZr5QOK3DbHg@mail.gmail.com> <7B83ED65-3252-438E-A9E6-2D1F31241D18@uibk.ac.at> <CAAMXsiYPJkwpXQd2XVtpfLcesY+NC5q674PSSvHjKe+rDjhaxA@mail.gmail.com>

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

**Follow-Ups**:**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*Thomas Sewell

**References**:**[isabelle] Automatic derivation of a total order on datatypes***From:*René Neumann

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*Andreas Lochbihler

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*René Thiemann

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*Simon Foster

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*René Thiemann

**Re: [isabelle] Automatic derivation of a total order on datatypes***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Type restrictions; document preparation [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Date: [isabelle] Introduction rule for quantifiers over sets of pairs
- Previous by Thread: Re: [isabelle] Automatic derivation of a total order on datatypes
- Next by Thread: Re: [isabelle] Automatic derivation of a total order on datatypes
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list