*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, peter.lammich at uni-muenster.de*Subject*: Re: [isabelle] Problems with linear orders and strings*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Thu, 3 Mar 2011 13:04:16 +0100*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4D6F69FB.9030501@informatik.tu-muenchen.de>*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>

Dear Florian and Peter, > the key issue is that the code lemmas for less_eq, less on char should > use nat_of_char rather than relying on the exact representation of nats. > >> lemma [code]: >> "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2" > >> lemma [code]: >> "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2" > > I would appreciate if these would go to the Char_ord theory. thanks again. However, there now seems to be an incompatibility of Char_ord with RBTMapImpl from the AFP: If I try to load both modules (to use RBTMaps with strings as keys), then there is class conflict since the dependent theories of Char_ord and RBTMapImpl both define the ordering on pairs (Product_ord and AFP/common/Misc). Peter, can you remove the pair-ordering in common/Misc and load Product_ord instead (it is the same definition)? 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é -- René Thiemann mailto:rene.thiemann at uibk.ac.at Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Science phone: +43 512 507-6434 University of Innsbruck

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

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

- Previous by Date: Re: [isabelle] introducing local names in proofs
- Next by Date: [isabelle] PxTP, First CFP
- 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