src/HOL/Library/Char_ord.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 51160 599ff65b85e2
child 54595 a2eeeb335a48
permissions -rw-r--r--
more simplification rules on unary and binary minus
nipkow@15737
     1
(*  Title:      HOL/Library/Char_ord.thy
haftmann@22805
     2
    Author:     Norbert Voelker, Florian Haftmann
nipkow@15737
     3
*)
nipkow@15737
     4
wenzelm@17200
     5
header {* Order on characters *}
nipkow@15737
     6
nipkow@15737
     7
theory Char_ord
haftmann@51160
     8
imports Main
nipkow@15737
     9
begin
nipkow@15737
    10
haftmann@25764
    11
instantiation nibble :: linorder
haftmann@25764
    12
begin
haftmann@25764
    13
haftmann@25764
    14
definition
haftmann@51160
    15
  "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
haftmann@25764
    16
haftmann@25764
    17
definition
haftmann@51160
    18
  "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
haftmann@25764
    19
haftmann@25764
    20
instance proof
haftmann@51160
    21
qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
nipkow@15737
    22
haftmann@25764
    23
end
haftmann@25764
    24
haftmann@25764
    25
instantiation nibble :: distrib_lattice
haftmann@25764
    26
begin
haftmann@25764
    27
haftmann@25764
    28
definition
haftmann@25502
    29
  "(inf \<Colon> nibble \<Rightarrow> _) = min"
haftmann@25764
    30
haftmann@25764
    31
definition
haftmann@25502
    32
  "(sup \<Colon> nibble \<Rightarrow> _) = max"
haftmann@25764
    33
haftmann@51160
    34
instance proof
haftmann@51160
    35
qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
nipkow@15737
    36
haftmann@25764
    37
end
haftmann@25764
    38
haftmann@25764
    39
instantiation char :: linorder
haftmann@25764
    40
begin
haftmann@25764
    41
haftmann@25764
    42
definition
haftmann@51160
    43
  "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
haftmann@25764
    44
haftmann@25764
    45
definition
haftmann@51160
    46
  "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
haftmann@25764
    47
haftmann@51160
    48
instance proof
haftmann@51160
    49
qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
haftmann@22805
    50
haftmann@25764
    51
end
nipkow@15737
    52
haftmann@51160
    53
lemma less_eq_char_Char:
haftmann@51160
    54
  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
haftmann@51160
    55
proof -
haftmann@51160
    56
  {
haftmann@51160
    57
    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
haftmann@51160
    58
      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
haftmann@51160
    59
    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
haftmann@51160
    60
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
haftmann@51160
    61
  }
haftmann@51160
    62
  note * = this
haftmann@51160
    63
  show ?thesis
haftmann@51160
    64
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
haftmann@51160
    65
    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: *)
haftmann@51160
    66
qed
haftmann@51160
    67
haftmann@51160
    68
lemma less_char_Char:
haftmann@51160
    69
  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
haftmann@51160
    70
proof -
haftmann@51160
    71
  {
haftmann@51160
    72
    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
haftmann@51160
    73
      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
haftmann@51160
    74
    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
haftmann@51160
    75
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
haftmann@51160
    76
  }
haftmann@51160
    77
  note * = this
haftmann@51160
    78
  show ?thesis
haftmann@51160
    79
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
haftmann@51160
    80
    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: *)
haftmann@51160
    81
qed
haftmann@51160
    82
haftmann@25764
    83
instantiation char :: distrib_lattice
haftmann@25764
    84
begin
haftmann@25764
    85
haftmann@25764
    86
definition
haftmann@25502
    87
  "(inf \<Colon> char \<Rightarrow> _) = min"
haftmann@25764
    88
haftmann@25764
    89
definition
haftmann@25502
    90
  "(sup \<Colon> char \<Rightarrow> _) = max"
haftmann@25764
    91
haftmann@51160
    92
instance proof
haftmann@51160
    93
qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
haftmann@22483
    94
haftmann@25764
    95
end
haftmann@25764
    96
haftmann@51160
    97
text {* Legacy aliasses *}
haftmann@51160
    98
haftmann@51160
    99
lemmas nibble_less_eq_def = less_eq_nibble_def
haftmann@51160
   100
lemmas nibble_less_def = less_nibble_def
haftmann@51160
   101
lemmas char_less_eq_def = less_eq_char_def
haftmann@51160
   102
lemmas char_less_def = less_char_def
haftmann@51160
   103
lemmas char_less_eq_simp = less_eq_char_Char
haftmann@51160
   104
lemmas char_less_simp = less_char_Char
haftmann@21871
   105
wenzelm@17200
   106
end
haftmann@51160
   107