src/HOL/Library/Char_ord.thy
author haftmann
Fri Oct 10 06:45:53 2008 +0200 (2008-10-10)
changeset 28562 4e74209f113e
parent 27682 25aceefd4786
child 30663 0b6aff7451b2
permissions -rw-r--r--
`code func` now just `code`
     1 (*  Title:      HOL/Library/Char_ord.thy
     2     ID:         $Id$
     3     Author:     Norbert Voelker, Florian Haftmann
     4 *)
     5 
     6 header {* Order on characters *}
     7 
     8 theory Char_ord
     9 imports Plain Product_ord Char_nat
    10 begin
    11 
    12 instantiation nibble :: linorder
    13 begin
    14 
    15 definition
    16   nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
    17 
    18 definition
    19   nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    20 
    21 instance proof
    22   fix n :: nibble
    23   show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
    24 next
    25   fix n m q :: nibble
    26   assume "n \<le> m"
    27     and "m \<le> q"
    28   then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
    29 next
    30   fix n m :: nibble
    31   assume "n \<le> m"
    32     and "m \<le> n"
    33   then show "n = m"
    34     unfolding nibble_less_eq_def nibble_less_def
    35     by (auto simp add: nat_of_nibble_eq)
    36 next
    37   fix n m :: nibble
    38   show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
    39     unfolding nibble_less_eq_def nibble_less_def less_le
    40     by (auto simp add: nat_of_nibble_eq)
    41 next
    42   fix n m :: nibble
    43   show "n \<le> m \<or> m \<le> n"
    44     unfolding nibble_less_eq_def by auto
    45 qed
    46 
    47 end
    48 
    49 instantiation nibble :: distrib_lattice
    50 begin
    51 
    52 definition
    53   "(inf \<Colon> nibble \<Rightarrow> _) = min"
    54 
    55 definition
    56   "(sup \<Colon> nibble \<Rightarrow> _) = max"
    57 
    58 instance by default (auto simp add:
    59     inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    60 
    61 end
    62 
    63 instantiation char :: linorder
    64 begin
    65 
    66 definition
    67   char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    68     n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
    69 
    70 definition
    71   char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    72     n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
    73 
    74 instance
    75   by default (auto simp: char_less_eq_def char_less_def split: char.splits)
    76 
    77 end
    78 
    79 instantiation char :: distrib_lattice
    80 begin
    81 
    82 definition
    83   "(inf \<Colon> char \<Rightarrow> _) = min"
    84 
    85 definition
    86   "(sup \<Colon> char \<Rightarrow> _) = max"
    87 
    88 instance   by default (auto simp add:
    89     inf_char_def sup_char_def min_max.sup_inf_distrib1)
    90 
    91 end
    92 
    93 lemma [simp, code]:
    94   shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    95   and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    96   unfolding char_less_eq_def char_less_def by simp_all
    97 
    98 end