src/HOL/Library/Char_ord.thy
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 61076 bdc1e2f0a86a
child 62597 b3f2b8c906a6
permissions -rw-r--r--
proper syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15737
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/Char_ord.thy
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
     2
    Author:     Norbert Voelker, Florian Haftmann
15737
nipkow
parents:
diff changeset
     3
*)
nipkow
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Order on characters\<close>
15737
nipkow
parents:
diff changeset
     6
nipkow
parents:
diff changeset
     7
theory Char_ord
51160
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
     8
imports Main
15737
nipkow
parents:
diff changeset
     9
begin
nipkow
parents:
diff changeset
    10
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    11
instantiation nibble :: linorder
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    12
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    13
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    14
definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    15
definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    16
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    17
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    18
  by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
15737
nipkow
parents:
diff changeset
    19
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    20
end
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    21
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    22
instantiation nibble :: distrib_lattice
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    23
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    24
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
    25
definition "(inf :: nibble \<Rightarrow> _) = min"
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
    26
definition "(sup :: nibble \<Rightarrow> _) = max"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    27
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    28
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    29
  by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
15737
nipkow
parents:
diff changeset
    30
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    31
end
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    32
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    33
instantiation char :: linorder
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    34
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    35
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    36
definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    37
definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    38
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    39
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    40
  by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    41
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    42
end
15737
nipkow
parents:
diff changeset
    43
51160
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    44
lemma less_eq_char_Char:
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    45
  "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    46
proof -
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    47
  {
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    48
    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    49
      \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    50
    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    51
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    52
  }
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    53
  note * = this
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    54
  show ?thesis
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    55
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    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: *)
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    57
qed
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    58
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    59
lemma less_char_Char:
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    60
  "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    61
proof -
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    62
  {
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    63
    assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    64
      < nat_of_nibble n2 * 16 + nat_of_nibble m2"
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    65
    then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    66
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    67
  }
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    68
  note * = this
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    69
  show ?thesis
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    70
    using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    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: *)
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    72
qed
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
    73
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    74
instantiation char :: distrib_lattice
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    75
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    76
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
    77
definition "(inf :: char \<Rightarrow> _) = min"
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
    78
definition "(sup :: char \<Rightarrow> _) = max"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    79
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    80
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    81
  by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
22483
86064f2f2188 added instance for lattice
haftmann
parents: 21911
diff changeset
    82
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    83
end
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    84
54595
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    85
instantiation String.literal :: linorder
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    86
begin
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    87
55426
90f2ceed2828 make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents: 54863
diff changeset
    88
context includes literal.lifting begin
54595
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    89
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    90
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    91
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    92
instance
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    93
proof -
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    94
  interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    95
    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    96
  show "PROP ?thesis"
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    97
    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    98
qed
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
    99
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
   100
end
55426
90f2ceed2828 make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents: 54863
diff changeset
   101
end
54595
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
   102
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
   103
lemma less_literal_code [code]: 
57437
0baf08c075b9 qualified String.explode and String.implode
haftmann
parents: 55426
diff changeset
   104
  "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
54595
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
   105
by(simp add: less_literal.rep_eq fun_eq_iff)
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
   106
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
   107
lemma less_eq_literal_code [code]:
57437
0baf08c075b9 qualified String.explode and String.implode
haftmann
parents: 55426
diff changeset
   108
  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
54595
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
   109
by(simp add: less_eq_literal.rep_eq fun_eq_iff)
a2eeeb335a48 instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents: 51160
diff changeset
   110
55426
90f2ceed2828 make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents: 54863
diff changeset
   111
lifting_update literal.lifting
90f2ceed2828 make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents: 54863
diff changeset
   112
lifting_forget literal.lifting
90f2ceed2828 make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents: 54863
diff changeset
   113
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   114
text \<open>Legacy aliasses\<close>
51160
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
   115
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
   116
lemmas nibble_less_eq_def = less_eq_nibble_def
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
   117
lemmas nibble_less_def = less_nibble_def
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
   118
lemmas char_less_eq_def = less_eq_char_def
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
   119
lemmas char_less_def = less_char_def
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
   120
lemmas char_less_eq_simp = less_eq_char_Char
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
   121
lemmas char_less_simp = less_char_Char
21871
9ce66839d9f1 added code generation syntax for some char combinators
haftmann
parents: 21404
diff changeset
   122
17200
3a4d03d1a31b tuned presentation;
wenzelm
parents: 15737
diff changeset
   123
end
51160
599ff65b85e2 systematic conversions between nat and nibble/char;
haftmann
parents: 48926
diff changeset
   124