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