src/HOL/Library/Char_ord.thy
author haftmann
Mon Jun 30 08:00:36 2014 +0200 (2014-06-30)
changeset 57437 0baf08c075b9
parent 55426 90f2ceed2828
child 58881 b9556a055632
permissions -rw-r--r--
qualified String.explode and String.implode
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@54863
    35
qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
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@54863
    93
qed (auto simp add: inf_char_def sup_char_def max_min_distrib2)
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@55426
   100
context includes literal.lifting begin
Andreas@54595
   101
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
Andreas@54595
   102
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
Andreas@54595
   103
Andreas@54595
   104
instance
Andreas@54595
   105
proof -
Andreas@54595
   106
  interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
Andreas@54595
   107
    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
Andreas@54595
   108
  show "PROP ?thesis"
Andreas@54595
   109
    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
Andreas@54595
   110
qed
Andreas@54595
   111
Andreas@54595
   112
end
Andreas@55426
   113
end
Andreas@54595
   114
Andreas@54595
   115
lemma less_literal_code [code]: 
haftmann@57437
   116
  "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
Andreas@54595
   117
by(simp add: less_literal.rep_eq fun_eq_iff)
Andreas@54595
   118
Andreas@54595
   119
lemma less_eq_literal_code [code]:
haftmann@57437
   120
  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
Andreas@54595
   121
by(simp add: less_eq_literal.rep_eq fun_eq_iff)
Andreas@54595
   122
Andreas@55426
   123
lifting_update literal.lifting
Andreas@55426
   124
lifting_forget literal.lifting
Andreas@55426
   125
haftmann@51160
   126
text {* Legacy aliasses *}
haftmann@51160
   127
haftmann@51160
   128
lemmas nibble_less_eq_def = less_eq_nibble_def
haftmann@51160
   129
lemmas nibble_less_def = less_nibble_def
haftmann@51160
   130
lemmas char_less_eq_def = less_eq_char_def
haftmann@51160
   131
lemmas char_less_def = less_char_def
haftmann@51160
   132
lemmas char_less_eq_simp = less_eq_char_Char
haftmann@51160
   133
lemmas char_less_simp = less_char_Char
haftmann@21871
   134
wenzelm@17200
   135
end
haftmann@51160
   136