*To*: Simon Foster <simon.foster at york.ac.uk>*Subject*: Re: [isabelle] Automatic derivation of a total order on datatypes*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Thu, 15 Nov 2012 10:32:08 +0100*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CALOYH0FLfej+JsENGuMjE=Jz8LNqXKUsyxRHyTLZr5QOK3DbHg@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>

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é

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

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

- Previous by Date: Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
- Next by Date: Re: [isabelle] Questions on type classes for lattices
- 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