Re: [isabelle] Problems with linear orders and strings

Hallo René,

>> Does this persists if you use the »official« Char_ord theory?
> Unfortunately: yes.
> theory Test
> imports Char_ord Code_Char_chr
> begin
> definition f where "f x \<equiv> (x :: char) <= x"
> export_code f in Haskell file -
> yields a similar error message as my own definition of <= on characters.

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.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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