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



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





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