Theory Char_ord
section ‹Order on characters›
theory Char_ord
imports Main
begin
instantiation char :: linorder
begin
definition less_eq_char :: ‹char ⇒ char ⇒ bool›
where ‹c1 ≤ c2 ⟷ of_char c1 ≤ (of_char c2 :: nat)›
definition less_char :: ‹char ⇒ char ⇒ bool›
where ‹c1 < c2 ⟷ of_char c1 < (of_char c2 :: nat)›
instance
by standard (auto simp add: less_eq_char_def less_char_def)
end
lemma less_eq_char_simp [simp, code]:
‹Char b0 b1 b2 b3 b4 b5 b6 b7 ≤ Char c0 c1 c2 c3 c4 c5 c6 c7
⟷ lexordp_eq [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]›
by (simp only: less_eq_char_def of_char_def char.sel horner_sum_less_eq_iff_lexordp_eq list.size) simp
lemma less_char_simp [simp, code]:
‹Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
⟷ ord_class.lexordp [b7, b6, b5, b4, b3, b2, b1, b0] [c7, c6, c5, c4, c3, c2, c1, c0]›
by (simp only: less_char_def of_char_def char.sel horner_sum_less_iff_lexordp list.size) simp
instantiation char :: distrib_lattice
begin
definition ‹(inf :: char ⇒ _) = min›
definition ‹(sup :: char ⇒ _) = max›
instance
by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
end
code_identifier
code_module Char_ord ⇀
(SML) Str and (OCaml) Str and (Haskell) Str and (Scala) Str
end