src/HOL/Library/Char_ord.thy
author haftmann
Thu, 26 Apr 2007 13:33:15 +0200
changeset 22805 1166a966e7b4
parent 22483 86064f2f2188
child 22845 5f9138bcb3d7
permissions -rw-r--r--
moved stuff to Char_nat.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15737
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/Char_ord.thy
nipkow
parents:
diff changeset
     2
    ID:         $Id$
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
     3
    Author:     Norbert Voelker, Florian Haftmann
15737
nipkow
parents:
diff changeset
     4
*)
nipkow
parents:
diff changeset
     5
17200
3a4d03d1a31b tuned presentation;
wenzelm
parents: 15737
diff changeset
     6
header {* Order on characters *}
15737
nipkow
parents:
diff changeset
     7
nipkow
parents:
diff changeset
     8
theory Char_ord
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
     9
imports Product_ord Char_nat
15737
nipkow
parents:
diff changeset
    10
begin
nipkow
parents:
diff changeset
    11
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    12
instance nibble :: linorder
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    13
  nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    14
  nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    15
proof
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    16
  fix n :: nibble show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    17
next
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    18
  fix n m q :: nibble
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    19
  assume "n \<le> m"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    20
  and "m \<le> q"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    21
  then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    22
next
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    23
  fix n m :: nibble
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    24
  assume "n \<le> m"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    25
  and "m \<le> n"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    26
  then show "n = m" unfolding nibble_less_eq_def nibble_less_def by (auto simp add: nat_of_nibble_eq)
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    27
next
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    28
  fix n m :: nibble
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    29
  show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    30
  unfolding nibble_less_eq_def nibble_less_def less_le by (auto simp add: nat_of_nibble_eq)
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    31
next
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    32
  fix n m :: nibble
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    33
  show "n \<le> m \<or> m \<le> n"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    34
  unfolding nibble_less_eq_def by auto
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    35
qed
15737
nipkow
parents:
diff changeset
    36
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    37
instance nibble :: distrib_lattice
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    38
  "inf \<equiv> min"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    39
  "sup \<equiv> max"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    40
  by default
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    41
    (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
15737
nipkow
parents:
diff changeset
    42
19736
wenzelm
parents: 17200
diff changeset
    43
instance char :: linorder
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    44
  char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    45
    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    46
  char_less_def:    "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    47
    n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    48
  by default (auto simp: char_less_eq_def char_less_def split: char.splits)
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    49
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    50
lemmas [code nofunc] = char_less_eq_def char_less_def
15737
nipkow
parents:
diff changeset
    51
22483
86064f2f2188 added instance for lattice
haftmann
parents: 21911
diff changeset
    52
instance char :: distrib_lattice
86064f2f2188 added instance for lattice
haftmann
parents: 21911
diff changeset
    53
  "inf \<equiv> min"
86064f2f2188 added instance for lattice
haftmann
parents: 21911
diff changeset
    54
  "sup \<equiv> max"
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    55
  by default
22483
86064f2f2188 added instance for lattice
haftmann
parents: 21911
diff changeset
    56
    (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
86064f2f2188 added instance for lattice
haftmann
parents: 21911
diff changeset
    57
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    58
lemma [simp, code func]:
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    59
  shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    60
  and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    61
  unfolding char_less_eq_def char_less_def by simp_all
21871
9ce66839d9f1 added code generation syntax for some char combinators
haftmann
parents: 21404
diff changeset
    62
17200
3a4d03d1a31b tuned presentation;
wenzelm
parents: 15737
diff changeset
    63
end