src/HOL/Library/Char_ord.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 68028 1f9f973eed2a
permissions -rw-r--r--
tuned equation
     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 less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool"
    15   where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)"
    16 
    17 definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool"
    18   where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)"
    19 
    20 
    21 instance
    22   by standard (auto simp add: less_eq_char_def less_char_def)
    23 
    24 end
    25 
    26 lemma less_eq_char_simp [simp]:
    27   "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
    28     \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
    29       \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
    30   by (simp add: less_eq_char_def)
    31 
    32 lemma less_char_simp [simp]:
    33   "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
    34     \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
    35       < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
    36   by (simp add: less_char_def)
    37 
    38 instantiation char :: distrib_lattice
    39 begin
    40 
    41 definition "(inf :: char \<Rightarrow> _) = min"
    42 definition "(sup :: char \<Rightarrow> _) = max"
    43 
    44 instance
    45   by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
    46 
    47 end
    48 
    49 end