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.

theory Linorders
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 .
qed auto

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
Computational Logic Group
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.