src/HOL/Library/Char_ord.thy
author wenzelm
Thu Jun 14 23:04:39 2007 +0200 (2007-06-14)
changeset 23394 474ff28210c0
parent 22845 5f9138bcb3d7
child 25502 9200b36280c0
permissions -rw-r--r--
tuned proofs;
     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 \<equiv> min"
    43     "sup \<equiv> 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 \<equiv> min"
    58     "sup \<equiv> 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