src/HOL/Library/Char_ord.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 61076 bdc1e2f0a86a
child 62597 b3f2b8c906a6
permissions -rw-r--r--
more symbols;
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
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
wenzelm@60679
    14
definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
wenzelm@60679
    15
definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
haftmann@25764
    16
wenzelm@60679
    17
instance
wenzelm@60679
    18
  by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
nipkow@15737
    19
haftmann@25764
    20
end
haftmann@25764
    21
haftmann@25764
    22
instantiation nibble :: distrib_lattice
haftmann@25764
    23
begin
haftmann@25764
    24
wenzelm@61076
    25
definition "(inf :: nibble \<Rightarrow> _) = min"
wenzelm@61076
    26
definition "(sup :: nibble \<Rightarrow> _) = max"
haftmann@25764
    27
wenzelm@60679
    28
instance
wenzelm@60679
    29
  by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
nipkow@15737
    30
haftmann@25764
    31
end
haftmann@25764
    32
haftmann@25764
    33
instantiation char :: linorder
haftmann@25764
    34
begin
haftmann@25764
    35
wenzelm@60679
    36
definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
wenzelm@60679
    37
definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
haftmann@25764
    38
wenzelm@60679
    39
instance
wenzelm@60679
    40
  by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
haftmann@22805
    41
haftmann@25764
    42
end
nipkow@15737
    43
haftmann@51160
    44
lemma less_eq_char_Char:
haftmann@51160
    45
  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
haftmann@51160
    46
proof -
haftmann@51160
    47
  {
haftmann@51160
    48
    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
haftmann@51160
    49
      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
haftmann@51160
    50
    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
haftmann@51160
    51
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
haftmann@51160
    52
  }
haftmann@51160
    53
  note * = this
haftmann@51160
    54
  show ?thesis
haftmann@51160
    55
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
haftmann@51160
    56
    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
    57
qed
haftmann@51160
    58
haftmann@51160
    59
lemma less_char_Char:
haftmann@51160
    60
  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
haftmann@51160
    61
proof -
haftmann@51160
    62
  {
haftmann@51160
    63
    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
haftmann@51160
    64
      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
haftmann@51160
    65
    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
haftmann@51160
    66
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
haftmann@51160
    67
  }
haftmann@51160
    68
  note * = this
haftmann@51160
    69
  show ?thesis
haftmann@51160
    70
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
haftmann@51160
    71
    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
    72
qed
haftmann@51160
    73
haftmann@25764
    74
instantiation char :: distrib_lattice
haftmann@25764
    75
begin
haftmann@25764
    76
wenzelm@61076
    77
definition "(inf :: char \<Rightarrow> _) = min"
wenzelm@61076
    78
definition "(sup :: char \<Rightarrow> _) = max"
haftmann@25764
    79
wenzelm@60679
    80
instance
wenzelm@60679
    81
  by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
haftmann@22483
    82
haftmann@25764
    83
end
haftmann@25764
    84
Andreas@54595
    85
instantiation String.literal :: linorder
Andreas@54595
    86
begin
Andreas@54595
    87
Andreas@55426
    88
context includes literal.lifting begin
Andreas@54595
    89
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
Andreas@54595
    90
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
Andreas@54595
    91
Andreas@54595
    92
instance
Andreas@54595
    93
proof -
Andreas@54595
    94
  interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
Andreas@54595
    95
    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
Andreas@54595
    96
  show "PROP ?thesis"
Andreas@54595
    97
    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
Andreas@54595
    98
qed
Andreas@54595
    99
Andreas@54595
   100
end
Andreas@55426
   101
end
Andreas@54595
   102
Andreas@54595
   103
lemma less_literal_code [code]: 
haftmann@57437
   104
  "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
Andreas@54595
   105
by(simp add: less_literal.rep_eq fun_eq_iff)
Andreas@54595
   106
Andreas@54595
   107
lemma less_eq_literal_code [code]:
haftmann@57437
   108
  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
Andreas@54595
   109
by(simp add: less_eq_literal.rep_eq fun_eq_iff)
Andreas@54595
   110
Andreas@55426
   111
lifting_update literal.lifting
Andreas@55426
   112
lifting_forget literal.lifting
Andreas@55426
   113
wenzelm@60500
   114
text \<open>Legacy aliasses\<close>
haftmann@51160
   115
haftmann@51160
   116
lemmas nibble_less_eq_def = less_eq_nibble_def
haftmann@51160
   117
lemmas nibble_less_def = less_nibble_def
haftmann@51160
   118
lemmas char_less_eq_def = less_eq_char_def
haftmann@51160
   119
lemmas char_less_def = less_char_def
haftmann@51160
   120
lemmas char_less_eq_simp = less_eq_char_Char
haftmann@51160
   121
lemmas char_less_simp = less_char_Char
haftmann@21871
   122
wenzelm@17200
   123
end
haftmann@51160
   124