src/HOL/Library/Char_ord.thy
author haftmann
Tue Apr 24 14:17:58 2018 +0000 (15 months ago)
changeset 68028 1f9f973eed2a
parent 67399 eab6ce8368fa
permissions -rw-r--r--
proper datatype for 8-bit characters
nipkow@15737
     1
(*  Title:      HOL/Library/Char_ord.thy
haftmann@22805
     2
    Author:     Norbert Voelker, Florian Haftmann
nipkow@15737
     3
*)
nipkow@15737
     4
wenzelm@60500
     5
section \<open>Order on characters\<close>
nipkow@15737
     6
nipkow@15737
     7
theory Char_ord
wenzelm@63462
     8
  imports Main
nipkow@15737
     9
begin
nipkow@15737
    10
haftmann@25764
    11
instantiation char :: linorder
haftmann@25764
    12
begin
haftmann@25764
    13
haftmann@68028
    14
definition less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool"
haftmann@68028
    15
  where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)"
haftmann@68028
    16
haftmann@68028
    17
definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool"
haftmann@68028
    18
  where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)"
haftmann@68028
    19
haftmann@25764
    20
wenzelm@60679
    21
instance
haftmann@62597
    22
  by standard (auto simp add: less_eq_char_def less_char_def)
haftmann@22805
    23
haftmann@25764
    24
end
nipkow@15737
    25
haftmann@68028
    26
lemma less_eq_char_simp [simp]:
haftmann@68028
    27
  "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
haftmann@68028
    28
    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
haftmann@68028
    29
      \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
haftmann@68028
    30
  by (simp add: less_eq_char_def)
haftmann@51160
    31
haftmann@68028
    32
lemma less_char_simp [simp]:
haftmann@68028
    33
  "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
haftmann@68028
    34
    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
haftmann@68028
    35
      < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
haftmann@68028
    36
  by (simp add: less_char_def)
wenzelm@63462
    37
haftmann@25764
    38
instantiation char :: distrib_lattice
haftmann@25764
    39
begin
haftmann@25764
    40
wenzelm@61076
    41
definition "(inf :: char \<Rightarrow> _) = min"
wenzelm@61076
    42
definition "(sup :: char \<Rightarrow> _) = max"
haftmann@25764
    43
wenzelm@60679
    44
instance
wenzelm@60679
    45
  by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
haftmann@22483
    46
haftmann@25764
    47
end
haftmann@25764
    48
Andreas@54595
    49
end