src/HOL/Library/Char_ord.thy
author haftmann
Tue Feb 19 19:44:10 2013 +0100 (2013-02-19)
changeset 51188 9b5bf1a9a710
parent 51160 599ff65b85e2
child 54595 a2eeeb335a48
permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
     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 text {* Legacy aliasses *}
    98 
    99 lemmas nibble_less_eq_def = less_eq_nibble_def
   100 lemmas nibble_less_def = less_nibble_def
   101 lemmas char_less_eq_def = less_eq_char_def
   102 lemmas char_less_def = less_char_def
   103 lemmas char_less_eq_simp = less_eq_char_Char
   104 lemmas char_less_simp = less_char_Char
   105 
   106 end
   107