[isabelle] Problems with linear orders and strings
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>
*** (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?
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