Theory Char_ord

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

header {* Order on characters *}

theory Char_ord
imports Main
begin

instantiation nibble :: linorder
begin

definition
  "n ≤ m <-> nat_of_nibble n ≤ nat_of_nibble m"

definition
  "n < m <-> nat_of_nibble n < nat_of_nibble m"

instance proof
qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)

end

instantiation nibble :: distrib_lattice
begin

definition
  "(inf :: nibble => _) = min"

definition
  "(sup :: nibble => _) = max"

instance proof
qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)

end

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 proof
qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)

end

lemma less_eq_char_Char:
  "Char n1 m1 ≤ Char n2 m2 <-> n1 < n2 ∨ n1 = n2 ∧ m1 ≤ m2"
proof -
  {
    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
      ≤ nat_of_nibble n2 * 16 + nat_of_nibble m2"
    then have "nat_of_nibble n1 ≤ nat_of_nibble n2"
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
  }
  note * = this
  show ?thesis
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    by (auto simp add: less_eq_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
qed

lemma less_char_Char:
  "Char n1 m1 < Char n2 m2 <-> n1 < n2 ∨ n1 = n2 ∧ m1 < m2"
proof -
  {
    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
    then have "nat_of_nibble n1 ≤ nat_of_nibble n2"
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
  }
  note * = this
  show ?thesis
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    by (auto simp add: less_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *)
qed

instantiation char :: distrib_lattice
begin

definition
  "(inf :: char => _) = min"

definition
  "(sup :: char => _) = max"

instance proof
qed (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))"
by(simp add: less_literal.rep_eq fun_eq_iff)

lemma less_eq_literal_code [code]:
  "op ≤ = (λxs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
by(simp add: less_eq_literal.rep_eq fun_eq_iff)

lifting_update literal.lifting
lifting_forget literal.lifting

text {* Legacy aliasses *}

lemmas nibble_less_eq_def = less_eq_nibble_def
lemmas nibble_less_def = less_nibble_def
lemmas char_less_eq_def = less_eq_char_def
lemmas char_less_def = less_char_def
lemmas char_less_eq_simp = less_eq_char_Char
lemmas char_less_simp = less_char_Char

end