[isabelle] Problems with linear orders and strings



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.