src/HOL/Library/Char_ord.thy
author haftmann
Sun May 06 21:50:17 2007 +0200 (2007-05-06)
changeset 22845 5f9138bcb3d7
parent 22805 1166a966e7b4
child 23394 474ff28210c0
permissions -rw-r--r--
changed code generator invocation syntax
     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 show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
    17 next
    18   fix n m q :: nibble
    19   assume "n \<le> m"
    20   and "m \<le> q"
    21   then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
    22 next
    23   fix n m :: nibble
    24   assume "n \<le> m"
    25   and "m \<le> n"
    26   then show "n = m" unfolding nibble_less_eq_def nibble_less_def by (auto simp add: nat_of_nibble_eq)
    27 next
    28   fix n m :: nibble
    29   show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
    30   unfolding nibble_less_eq_def nibble_less_def less_le by (auto simp add: nat_of_nibble_eq)
    31 next
    32   fix n m :: nibble
    33   show "n \<le> m \<or> m \<le> n"
    34   unfolding nibble_less_eq_def by auto
    35 qed
    36 
    37 instance nibble :: distrib_lattice
    38   "inf \<equiv> min"
    39   "sup \<equiv> max"
    40   by default
    41     (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    42 
    43 instance char :: linorder
    44   char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    45     n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    46   char_less_def:    "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
    47     n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    48   by default (auto simp: char_less_eq_def char_less_def split: char.splits)
    49 
    50 lemmas [code func del] = char_less_eq_def char_less_def
    51 
    52 instance char :: distrib_lattice
    53   "inf \<equiv> min"
    54   "sup \<equiv> max"
    55   by default
    56     (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
    57 
    58 lemma [simp, code func]:
    59   shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
    60   and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
    61   unfolding char_less_eq_def char_less_def by simp_all
    62 
    63 end