# Theory Char_ord

theory Char_ord
imports Main
```(*  Title:      HOL/Library/Char_ord.thy
Author:     Norbert Voelker, Florian Haftmann
*)

section ‹Order on characters›

theory Char_ord
imports Main
begin

instantiation char :: linorder
begin

definition "c1 ≤ c2 ⟷ nat_of_char c1 ≤ nat_of_char c2"
definition "c1 < c2 ⟷ nat_of_char c1 < nat_of_char c2"

instance
by standard (auto simp add: less_eq_char_def less_char_def)

end

lemma less_eq_char_simps:
"0 ≤ c"
"Char k ≤ 0 ⟷ numeral k mod 256 = (0 :: nat)"
"Char k ≤ Char l ⟷ numeral k mod 256 ≤ (numeral l mod 256 :: nat)"
for c :: char

lemma less_char_simps:
"¬ c < 0"
"0 < Char k ⟷ (0 :: nat) < numeral k mod 256"
"Char k < Char l ⟷ numeral k mod 256 < (numeral l mod 256 :: nat)"
for c :: char

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

instantiation String.literal :: linorder
begin

context includes literal.lifting
begin

lift_definition less_literal :: "String.literal ⇒ String.literal ⇒ bool"
is "ord.lexordp op <" .

lift_definition less_eq_literal :: "String.literal ⇒ String.literal ⇒ bool"
is "ord.lexordp_eq op <" .

instance
proof -
interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string ⇒ string ⇒ bool"
by (rule linorder.lexordp_linorder[where less_eq="op ≤"]) unfold_locales
show "PROP ?thesis"
by intro_classes (transfer, simp add: less_le_not_le linear)+
qed

end

end

lemma less_literal_code [code]:
"op < = (λxs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"