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
"less_bool_def". Please try again by reloading the .tgz or checking out
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.