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