[isabelle] Code_String: linorder in String.literal



Dear all,

I needed linorder on String.literal, hence I came up with the theory as
in the attachment. It explicitly uses lexord, and only later lifts it to
op <, to explicitly show what the order is and not rely on 'magic' from
the (lin)ord(er) class.

It also defines op < and op <= using the target language operators (save
Scala, for I don't know it) for performance reasons.

Would this be useful for inclusion in HOL/Library?

I also noted, that there is something similiar (minus code-printing) in
AFP/Containers, but I can't tell if this is the same.

Regards,
René
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055
theory Code_String
imports
  "~~/src/HOL/Library/Code_Char"
  "~~/src/HOL/Library/List_lexord"
begin

text {* Instantiate linorder for String.literal and also use ordering on strings in the target language. This saves us casting between String.literal and string. *}

instantiation String.literal :: linorder
begin

(* Explicitly force lexicographic order *)
definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
where
  "less_literal s1 s2 \<longleftrightarrow> (explode s1, explode s2) \<in> lexord {(u,v). u < v}"

definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
where
  "less_eq_literal s1 s2 \<longleftrightarrow> s1 < s2 \<or> s1 = s2"

(* Lift to using class-operations *)
lemma less_literal_alt_def:
  "s1 < s2 \<longleftrightarrow> explode s1 < explode s2"
unfolding less_literal_def
by (simp add: list_less_def)

lemma less_eq_literal_alt_def:
  "s1 \<le> s2 \<longleftrightarrow> explode s1 \<le> explode s2"
unfolding less_eq_literal_def
by (simp add: less_literal_alt_def list_le_def explode_inject)

instance
  apply default
  apply (auto simp add: less_literal_alt_def less_eq_literal_alt_def)
  apply (metis explode_inject)
  done
end

code_printing
  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
    (SML) "!((_ : string) <= _)"
    and (OCaml) "!((_ : string) <= _)"
    and (Haskell) infix 4 "<="
| constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
    (SML) "!((_ : string) < _)"
    and (OCaml) "!((_ : string) < _)"
    and (Haskell) infix 4 "<"

end

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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