src/HOL/Library/Char_ord.thy
author Andreas Lochbihler
Wed Nov 20 11:12:35 2013 +0100 (2013-11-20)
changeset 54595 a2eeeb335a48
parent 51160 599ff65b85e2
child 54863 82acc20ded73
permissions -rw-r--r--
instantiate linorder for String.literal by lexicographic order
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
Andreas@54595
    97
instantiation String.literal :: linorder
Andreas@54595
    98
begin
Andreas@54595
    99
Andreas@54595
   100
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
Andreas@54595
   101
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
Andreas@54595
   102
Andreas@54595
   103
instance
Andreas@54595
   104
proof -
Andreas@54595
   105
  interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
Andreas@54595
   106
    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
Andreas@54595
   107
  show "PROP ?thesis"
Andreas@54595
   108
    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
Andreas@54595
   109
qed
Andreas@54595
   110
Andreas@54595
   111
end
Andreas@54595
   112
Andreas@54595
   113
lemma less_literal_code [code]: 
Andreas@54595
   114
  "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
Andreas@54595
   115
by(simp add: less_literal.rep_eq fun_eq_iff)
Andreas@54595
   116
Andreas@54595
   117
lemma less_eq_literal_code [code]:
Andreas@54595
   118
  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
Andreas@54595
   119
by(simp add: less_eq_literal.rep_eq fun_eq_iff)
Andreas@54595
   120
haftmann@51160
   121
text {* Legacy aliasses *}
haftmann@51160
   122
haftmann@51160
   123
lemmas nibble_less_eq_def = less_eq_nibble_def
haftmann@51160
   124
lemmas nibble_less_def = less_nibble_def
haftmann@51160
   125
lemmas char_less_eq_def = less_eq_char_def
haftmann@51160
   126
lemmas char_less_def = less_char_def
haftmann@51160
   127
lemmas char_less_eq_simp = less_eq_char_Char
haftmann@51160
   128
lemmas char_less_simp = less_char_Char
haftmann@21871
   129
wenzelm@17200
   130
end
haftmann@51160
   131