*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] Problems with linear orders and strings*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Fri, 04 Mar 2011 17:36:58 +0100*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <A0466180-3201-43C9-9789-0C18963E7117@uibk.ac.at>*References*: <5A017623-D520-46E6-A9AB-FF49D7C0F025@uibk.ac.at> <4D6D5C79.4000503@informatik.tu-muenchen.de> <F274B8A7-1154-4B50-9DEC-ACE3B8353643@uibk.ac.at> <4D6F69FB.9030501@informatik.tu-muenchen.de> <A0466180-3201-43C9-9789-0C18963E7117@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20101125 SUSE/3.0.11 Thunderbird/3.0.11

> Peter, can you remove the pair-ordering in common/Misc and load Product_ord instead (it is the same definition)? > If it is the same definition, and Product_ord is in the Isabelle standard library, it should of course be changed to avoid duplication and clashes! @Rene: For the first time, you should change it in your local copy. If you are using the stable version, there is no other way. For the development version, someone (probably me or some of the afp maintainers) should setup a development snapshot, do the change, test if nothing breaks, and push it into the hg-repository. Otherwise, it highlights some general problem with type classes: If there is more than one way to say order a datatype, which one should go into the typeclass. I think there is such a problem for multisets, where there are two orderings that are both "the natural" one when viewed from the right perspective. And, if formalizations get large, there may be parts where one order is the "natural" one, and other parts where the other order is the "natural" one, and then things seems to clash ... Unfortunately, the ICF interfaces are currently not parameterizable by the used order, hash-function, equality-operator, ... @Andreas: What was the state of discussion there, is it possible/worth the effort to parameterize? Best, Peter > I have the following workaround, but of course this should be fixed in a better way. > > theory Linorders > imports List_lexord Char_nat (* but not Char_prod *) > begin > > instantiation char :: linorder > begin > fun less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool" where "less_eq_char c d = (nat_of_char c \<le> nat_of_char d)" > fun less_char :: "char \<Rightarrow> char \<Rightarrow> bool" where "less_char c d = (nat_of_char c < nat_of_char d)" > > instance > proof > fix x y :: char > assume "x \<le> y" and "y \<le> x" > hence "nat_of_char x = nat_of_char y" (is "?x = ?y") by auto > hence "char_of_nat ?x = char_of_nat ?y" by simp > thus "x = y" unfolding char_of_nat_of_char . > qed auto > end > > Afterwards strings are in class linorder, code-generation works also after Code_Char_chr, > and I can use RBTMapImpl as there is no conflict between Misc and Product_ord. > > Cheers, > René >

**Follow-Ups**:**Re: [isabelle] Problems with linear orders and strings***From:*Jeremy Siek

**Re: [isabelle] Problems with linear orders and strings***From:*Andreas Lochbihler

**References**:**[isabelle] Problems with linear orders and strings***From:*René Thiemann

**Re: [isabelle] Problems with linear orders and strings***From:*Florian Haftmann

**Re: [isabelle] Problems with linear orders and strings***From:*René Thiemann

**Re: [isabelle] Problems with linear orders and strings***From:*Florian Haftmann

**Re: [isabelle] Problems with linear orders and strings***From:*René Thiemann

- Previous by Date: Re: [isabelle] [isabelle-dev] Syntax.read_term ctxt
- Next by Date: Re: [isabelle] Problems with linear orders and strings
- Previous by Thread: Re: [isabelle] Problems with linear orders and strings
- Next by Thread: Re: [isabelle] Problems with linear orders and strings
- Cl-isabelle-users March 2011 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