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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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