src/HOL/Library/Char_ord.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 67399 eab6ce8368fa
child 68028 1f9f973eed2a
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     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 (<)" .
    55 
    56 lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    57   is "ord.lexordp_eq (<)" .
    58 
    59 instance
    60 proof -
    61   interpret linorder "ord.lexordp_eq (<)" "ord.lexordp (<) :: string \<Rightarrow> string \<Rightarrow> bool"
    62     by (rule linorder.lexordp_linorder[where less_eq="(\<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   "(<) = (\<lambda>xs ys. ord.lexordp (<) (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   "(\<le>) = (\<lambda>xs ys. ord.lexordp_eq (<) (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