*To*: Dominique Unruh <unruh at ut.ee>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Datatype definition can be slow*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 13 Apr 2021 18:11:47 +0200*In-reply-to*: <1dd40b38-5588-1583-2d5f-2f06d4eff609@ut.ee>*References*: <a0701ab.2b705.178c68638b8.Coremail.13061136@buaa.edu.cn> <9674D5AE-0AB1-476F-85EF-7E2964840F6F@di.ku.dk> <77d2e2ee-cfda-fbc7-3bdc-f6189bfff00a@in.tum.de> <1dd40b38-5588-1583-2d5f-2f06d4eff609@ut.ee>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.8.1

> "constructor_num x != constructor_num y ==> x != y" That works in this very simple case where your datatype is just an "enum"-like type. But in general, it should probably be something like "constructor_num x != constructor_num y ==> x a b c != y d e" because constructors, of course, can take parameters. In any case, I don't think that works because you cannot really quantify over constructors like this. In general, the constructors may not even have the same type. What I had in mind was that the simproc unfolds the internal construction that the datatype uses and then proves the inequality from that. I am not familiar with the details of that; there is probably a little bit of overhead involved, but probably not too much. Manuel On 13/04/2021 18:06, Dominique Unruh wrote: >> Somebody once voiced the possibility of making it possible to switch off >> the simplification lemmas (e.g. for constructor distinctness, of which >> there are quadratically many) and replace them by a simproc that proves >> them ad-hoc whenever one of them is needed. >> This would make applying the theorems slightly more expensive, but >> eliminate the need to prove all of them beforehand. >> >> Not sure if this becomes enough of a problem to be worth it or if the >> existing construction is fast enough for any reasonably-sized datatype. > > Maybe the following approach would be nice: > > Instead of generating pairwise inequalities, a function constructor_num > is generated with the simp-rules "constructor_num A00 = 1" > "constructor_num A01 = 2" "constructor_num A03 = 3" etc. (Where > "constructor_num" is an overloaded function like size.) > > Then we additionally add the simp-rule "constructor_num x != > constructor_num y ==> x != y". (For each datatype one instances because > the generic one would loop. Or alternatively, have a no-assumptions type > class for which that rule holds is added to the simplifier.) > > Now I believe that this would be enough to decide inequalities the same > way as simp can do now. (Haven't tested this.) > > To avoid unnecessary simplifications, maybe add a cong-rule that forbids > simplifications in the argument of constructor_num. > > (Sorry if this is obvious and anyway what you had in mind for the inner > workings of the simproc.) > > Best wishes, > Dominique. > >

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Datatype definition can be slow***From:*Jakub Kądziołka

**References**:**[isabelle] Datatype definition can be slow***From:*He, Shuhan

**Re: [isabelle] Datatype definition can be slow***From:*Dmitriy Traytel

**Re: [isabelle] Datatype definition can be slow***From:*Manuel Eberl

**Re: [isabelle] Datatype definition can be slow***From:*Dominique Unruh

- Previous by Date: Re: [isabelle] Datatype definition can be slow
- Next by Date: Re: [isabelle] Datatype definition can be slow
- Previous by Thread: Re: [isabelle] Datatype definition can be slow
- Next by Thread: Re: [isabelle] Datatype definition can be slow
- Cl-isabelle-users April 2021 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