src/HOL/Library/Char_ord.thy
author haftmann
Thu Nov 29 17:08:26 2007 +0100 (2007-11-29)
changeset 25502 9200b36280c0
parent 23394 474ff28210c0
child 25764 878c37886eed
permissions -rw-r--r--
instance command as rudimentary class target
     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 Product_ord Char_nat
    10 begin
    11 
    12 instance nibble :: linorder
    13   nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m"
    14   nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m"
    15 proof
    16   fix n :: nibble
    17   show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
    18 next
    19   fix n m q :: nibble
    20   assume "n \<le> m"
    21     and "m \<le> q"
    22   then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
    23 next
    24   fix n m :: nibble
    25   assume "n \<le> m"
    26     and "m \<le> n"
    27   then show "n = m"
    28     unfolding nibble_less_eq_def nibble_less_def
    29     by (auto simp add: nat_of_nibble_eq)
    30 next
    31   fix n m :: nibble
    32   show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
    33     unfolding nibble_less_eq_def nibble_less_def less_le
    34     by (auto simp add: nat_of_nibble_eq)
    35 next
    36   fix n m :: nibble
    37   show "n \<le> m \<or> m \<le> n"
    38     unfolding nibble_less_eq_def by auto
    39 qed
    40 
    41 instance nibble :: distrib_lattice
    42   "(inf \<Colon> nibble \<Rightarrow> _) = min"
    43   "(sup \<Colon> nibble \<Rightarrow> _) = max"
    44   by default (auto simp add:
    45     inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    46 
    47 instance char :: linorder
    48   char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    49     n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    50   char_less_def:    "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    51     n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    52   by default (auto simp: char_less_eq_def char_less_def split: char.splits)
    53 
    54 lemmas [code func del] = char_less_eq_def char_less_def
    55 
    56 instance char :: distrib_lattice
    57   "(inf \<Colon> char \<Rightarrow> _) = min"
    58   "(sup \<Colon> char \<Rightarrow> _) = max"
    59   by default (auto simp add:
    60     inf_char_def sup_char_def min_max.sup_inf_distrib1)
    61 
    62 lemma [simp, code func]:
    63   shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    64   and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    65   unfolding char_less_eq_def char_less_def by simp_all
    66 
    67 end