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

```Hi Simon,

> The derive linorder works really well,

Thanks.

> but I've come across an odd example
> which doesn't work, namely:
>
> datatype vbasic = BoolI bool | ListI "vbasic list"
> derive linorder vbasic
>
> Fails to prove. If I replace the bool with an int or remove the list
> constructor, it works fine. There seems to be an odd interaction between
> bool and list. The following works fine:
>
> datatype vbasic = TrueI | FalseI | IntI "int" | ListI "vbasic list"
>
> Do you know what's causing this?

I have figured out the problem, which was the simplification rule
the latest development version of the AFP, since this rule is explicitly deleted
for simplification in the tactics.

However, I'm not completely sure why this simplification rule was so
harmful. In principle, I had to prove the lemma

vbasic_rec (%x_0. vbasic_case (op < x_0) (%y_0. True)) (%x_0. vbasic_case (%y_0. False)) (RecursiveI a) (RecursiveI b) ==>
vbasic_rec (%x_0. vbasic_case (op < x_0) (%y_0. True)) (%x_0. vbasic_case (%y_0. False)) a b

which works via the "tactic {* asm_full_simp_tac (simpset_of ctxt) 1 *}".
However, when invoking this tactic within the larger ML tactic,
then it happens that premise gets simplified to

vbasic_rec (%x_0. vbasic_case (op < x_0) (%y_0. True)) (%x_0. vbasic_case (%y_0. False)) a b

(as expected), but then the proof goal is simplified further to

vbasic_rec (%x_0. vbasic_case (op & (~ x_0)) (%y_0. True)) (%x_0. vbasic_case (%y_0. False)) a b

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 someone else can comment on this?

Cheers,
René

```

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