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