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