Re: [isabelle] Problems with linear orders and strings



> Peter, can you remove the pair-ordering in common/Misc and load Product_ord instead (it is the same definition)?
>   

If it is the same definition, and Product_ord is in the Isabelle
standard library, it should of course be changed to avoid duplication
and clashes!
  @Rene: For the first time, you should change it in your local copy. If
you are using the stable version, there is no other way.
     For the development version, someone (probably me or some of the
afp maintainers) should setup a development snapshot, do the change,
test if nothing breaks, and push it into the hg-repository.

Otherwise, it highlights some general problem with type classes:
  If there is more than one way to say order a datatype, which one
should go into the typeclass.
  I think there is such a problem for multisets, where there are two
orderings that are both "the natural" one when viewed from the right
perspective.
  And, if formalizations get large, there may be parts where one order
is the "natural" one, and other parts where the other order is the
"natural" one, and
  then things seems to clash ...

Unfortunately, the ICF interfaces are currently not parameterizable by
the used order, hash-function, equality-operator, ...
  @Andreas: What was the state of discussion there, is it possible/worth
the effort to parameterize?

Best,
  Peter


> 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 *)
> begin
>
> instantiation char :: linorder
> begin
> 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)"
>
> instance
> proof
>   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
> end
>
> 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.
>
> Cheers,
> René
>   






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