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
     1 (*  Title:      HOL/Library/Char_ord.thy
     2     Author:     Norbert Voelker, Florian Haftmann
     3 *)
     4 
     5 header {* Order on characters *}
     6 
     7 theory Char_ord
     8 imports Main
     9 begin
    10 
    11 instantiation nibble :: linorder
    12 begin
    13 
    14 definition
    15   "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
    16 
    17 definition
    18   "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    19 
    20 instance proof
    21 qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
    22 
    23 end
    24 
    25 instantiation nibble :: distrib_lattice
    26 begin
    27 
    28 definition
    29   "(inf \<Colon> nibble \<Rightarrow> _) = min"
    30 
    31 definition
    32   "(sup \<Colon> nibble \<Rightarrow> _) = max"
    33 
    34 instance proof
    35 qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    36 
    37 end
    38 
    39 instantiation char :: linorder
    40 begin
    41 
    42 definition
    43   "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
    44 
    45 definition
    46   "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
    47 
    48 instance proof
    49 qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
    50 
    51 end
    52 
    53 lemma less_eq_char_Char:
    54   "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    55 proof -
    56   {
    57     assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
    58       \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2"
    59     then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
    60     using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
    61   }
    62   note * = this
    63   show ?thesis
    64     using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    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: *)
    66 qed
    67 
    68 lemma less_char_Char:
    69   "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    70 proof -
    71   {
    72     assume "nat_of_nibble n1 * 16 + nat_of_nibble m1
    73       < nat_of_nibble n2 * 16 + nat_of_nibble m2"
    74     then have "nat_of_nibble n1 \<le> nat_of_nibble n2"
    75     using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto
    76   }
    77   note * = this
    78   show ?thesis
    79     using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2]
    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: *)
    81 qed
    82 
    83 instantiation char :: distrib_lattice
    84 begin
    85 
    86 definition
    87   "(inf \<Colon> char \<Rightarrow> _) = min"
    88 
    89 definition
    90   "(sup \<Colon> char \<Rightarrow> _) = max"
    91 
    92 instance proof
    93 qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
    94 
    95 end
    96 
    97 instantiation String.literal :: linorder
    98 begin
    99 
   100 lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
   101 lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
   102 
   103 instance
   104 proof -
   105   interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
   106     by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
   107   show "PROP ?thesis"
   108     by(intro_classes)(transfer, simp add: less_le_not_le linear)+
   109 qed
   110 
   111 end
   112 
   113 lemma less_literal_code [code]: 
   114   "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
   115 by(simp add: less_literal.rep_eq fun_eq_iff)
   116 
   117 lemma less_eq_literal_code [code]:
   118   "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
   119 by(simp add: less_eq_literal.rep_eq fun_eq_iff)
   120 
   121 text {* Legacy aliasses *}
   122 
   123 lemmas nibble_less_eq_def = less_eq_nibble_def
   124 lemmas nibble_less_def = less_nibble_def
   125 lemmas char_less_eq_def = less_eq_char_def
   126 lemmas char_less_def = less_char_def
   127 lemmas char_less_eq_simp = less_eq_char_Char
   128 lemmas char_less_simp = less_char_Char
   129 
   130 end
   131