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