*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Problems with linear orders and strings*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Tue, 1 Mar 2011 20:33:36 +0100

Dear all, the problem I have is as follows: - I want to use the AFP/Collection/RBT... theories to have efficient implementations of sets. - to use this framework, the carrier has to be in the class linorder - moreover, I need to operate on sets of strings ==> strings (= char list) must be in the class linorder unfortunately, neither char nor list are contained in the linorder class. So here I have three questions: 1) are there already theories which make char and string members of linorder 2) I have defined my own class instance for char as follows: fun nibble_to_nat :: "nibble => nat" where "nibble_to_nat Nibble0 = 0" | "nibble_to_nat Nibble1 = 1" ... fun char_to_nat :: "char => nat" where "char_to_nat (Char n1 n2) = (16 * nibble_to_nat n1 + nibble_to_nat n2)" fun less_eq_char :: "char => char => bool" where "less_eq_char c d = (char_to_nat c <= char_to_nat d)" and then proven that this implementation satisfies the class conditions. Unfortunately, after loading Code_Char_chr I cannot export the code anymore since it is complains as follows: *** Illegal character expression, *** in equation char_to_nat (Char ?n1.0 ?n2.0) \<equiv> *** plus_nat_inst.plus_nat *** (times_nat_inst.times_nat *** (nat (number_int_inst.number_of_int *** (Int.Bit0 (Int.Bit0 (Int.Bit0 (Int.Bit0 (Int.Bit1 Int.Pls))))))) *** (nibble_to_nat ?n1.0)) *** (nibble_to_nat ?n2.0) 3) In reality I need linorder not only for strings, but also for more complex datatypes like the following for labeled symbols: datatype ('f,'l)lab = Lab "('f,'l)lab" 'l | Funlab "('f,'l)lab" "('f,'l)lab list" | Unlab 'f The generation of an arbitrary linearization of each datatype is trivial via a lexicographic comparison. However, the proof obligations are tedious to prove. Is there some automatic way to let Isabelles generate a linearization? Best regards, 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:*Florian Haftmann

- Previous by Date: [isabelle] CICM 2011: Final Call for Papers
- Next by Date: Re: [isabelle] Problems with linear orders and strings
- Previous by Thread: [isabelle] CICM 2011: Final Call for Papers
- 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