src/HOL/Library/Char_ord.thy
author haftmann
Mon Jun 30 08:00:36 2014 +0200 (2014-06-30)
changeset 57437 0baf08c075b9
parent 55426 90f2ceed2828
child 58881 b9556a055632
permissions -rw-r--r--
qualified String.explode and String.implode
     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 max_min_distrib2)
    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 max_min_distrib2)
    94 
    95 end
    96 
    97 instantiation String.literal :: linorder
    98 begin
    99 
   100 context includes literal.lifting begin
   101 lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
   102 lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
   103 
   104 instance
   105 proof -
   106   interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
   107     by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
   108   show "PROP ?thesis"
   109     by(intro_classes)(transfer, simp add: less_le_not_le linear)+
   110 qed
   111 
   112 end
   113 end
   114 
   115 lemma less_literal_code [code]: 
   116   "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
   117 by(simp add: less_literal.rep_eq fun_eq_iff)
   118 
   119 lemma less_eq_literal_code [code]:
   120   "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
   121 by(simp add: less_eq_literal.rep_eq fun_eq_iff)
   122 
   123 lifting_update literal.lifting
   124 lifting_forget literal.lifting
   125 
   126 text {* Legacy aliasses *}
   127 
   128 lemmas nibble_less_eq_def = less_eq_nibble_def
   129 lemmas nibble_less_def = less_nibble_def
   130 lemmas char_less_eq_def = less_eq_char_def
   131 lemmas char_less_def = less_char_def
   132 lemmas char_less_eq_simp = less_eq_char_Char
   133 lemmas char_less_simp = less_char_Char
   134 
   135 end
   136