*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] Automatic derivation of a total order on datatypes*From*: Brian Huffman <huffman.brian.c at gmail.com>*Date*: Thu, 15 Nov 2012 09:12:59 -0800*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Simon Foster <simon.foster at york.ac.uk>*In-reply-to*: <7B83ED65-3252-438E-A9E6-2D1F31241D18@uibk.ac.at>*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>

On Thu, Nov 15, 2012 at 1:32 AM, René Thiemann <rene.thiemann at uibk.ac.at> 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. - Brian

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

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

- Previous by Date: Re: [isabelle] Highlight sorry in jEdit
- Next by Date: Re: [isabelle] attribute: rule_format
- 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