src/HOL/Library/Char_ord.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63462 c1fe30f2bc32
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned proofs;
     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 char :: linorder
    12 begin
    13 
    14 definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
    15 definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
    16 
    17 instance
    18   by standard (auto simp add: less_eq_char_def less_char_def)
    19 
    20 end
    21 
    22 lemma less_eq_char_simps:
    23   "0 \<le> c"
    24   "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
    25   "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
    26   for c :: char
    27   by (simp_all add: Char_def less_eq_char_def)
    28 
    29 lemma less_char_simps:
    30   "\<not> c < 0"
    31   "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
    32   "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
    33   for c :: char
    34   by (simp_all add: Char_def less_char_def)
    35 
    36 instantiation char :: distrib_lattice
    37 begin
    38 
    39 definition "(inf :: char \<Rightarrow> _) = min"
    40 definition "(sup :: char \<Rightarrow> _) = max"
    41 
    42 instance
    43   by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
    44 
    45 end
    46 
    47 instantiation String.literal :: linorder
    48 begin
    49 
    50 context includes literal.lifting
    51 begin
    52 
    53 lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    54   is "ord.lexordp op <" .
    55 
    56 lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    57   is "ord.lexordp_eq op <" .
    58 
    59 instance
    60 proof -
    61   interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
    62     by (rule linorder.lexordp_linorder[where less_eq="op \<le>"]) unfold_locales
    63   show "PROP ?thesis"
    64     by intro_classes (transfer, simp add: less_le_not_le linear)+
    65 qed
    66 
    67 end
    68 
    69 end
    70 
    71 lemma less_literal_code [code]:
    72   "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
    73   by (simp add: less_literal.rep_eq fun_eq_iff)
    74 
    75 lemma less_eq_literal_code [code]:
    76   "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
    77   by (simp add: less_eq_literal.rep_eq fun_eq_iff)
    78 
    79 lifting_update literal.lifting
    80 lifting_forget literal.lifting
    81 
    82 end