Re: [isabelle] Problems with linear orders and strings
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.
imports List_lexord Char_nat (* but not Char_prod *)
instantiation char :: linorder
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)"
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 .
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.
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