src/HOL/Library/Char_ord.thy
author nipkow
Sun, 26 Aug 2012 10:20:26 +0200
changeset 48926 8d7778a19857
parent 37765 26bdfb7b680b
child 51160 599ff65b85e2
permissions -rw-r--r--
fixed theory dependency
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15737
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/Char_ord.thy
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
     2
    Author:     Norbert Voelker, Florian Haftmann
15737
nipkow
parents:
diff changeset
     3
*)
nipkow
parents:
diff changeset
     4
17200
3a4d03d1a31b tuned presentation;
wenzelm
parents: 15737
diff changeset
     5
header {* Order on characters *}
15737
nipkow
parents:
diff changeset
     6
nipkow
parents:
diff changeset
     7
theory Char_ord
48926
8d7778a19857 fixed theory dependency
nipkow
parents: 37765
diff changeset
     8
imports Char_nat
15737
nipkow
parents:
diff changeset
     9
begin
nipkow
parents:
diff changeset
    10
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    11
instantiation nibble :: linorder
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    12
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    13
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    14
definition
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    15
  nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    16
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    17
definition
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    18
  nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    19
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    20
instance proof
23394
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    21
  fix n :: nibble
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    22
  show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    23
next
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    24
  fix n m q :: nibble
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    25
  assume "n \<le> m"
23394
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    26
    and "m \<le> q"
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    27
  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
    28
next
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    29
  fix n m :: nibble
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    30
  assume "n \<le> m"
23394
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    31
    and "m \<le> n"
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    32
  then show "n = m"
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    33
    unfolding nibble_less_eq_def nibble_less_def
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    34
    by (auto simp add: nat_of_nibble_eq)
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    35
next
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    36
  fix n m :: nibble
27682
25aceefd4786 added class preorder
haftmann
parents: 27368
diff changeset
    37
  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
23394
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    38
    unfolding nibble_less_eq_def nibble_less_def less_le
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    39
    by (auto simp add: nat_of_nibble_eq)
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    40
next
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    41
  fix n m :: nibble
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    42
  show "n \<le> m \<or> m \<le> n"
23394
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    43
    unfolding nibble_less_eq_def by auto
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    44
qed
15737
nipkow
parents:
diff changeset
    45
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    46
end
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    47
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    48
instantiation nibble :: distrib_lattice
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    49
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    50
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    51
definition
25502
9200b36280c0 instance command as rudimentary class target
haftmann
parents: 23394
diff changeset
    52
  "(inf \<Colon> nibble \<Rightarrow> _) = min"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    53
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    54
definition
25502
9200b36280c0 instance command as rudimentary class target
haftmann
parents: 23394
diff changeset
    55
  "(sup \<Colon> nibble \<Rightarrow> _) = max"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    56
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    57
instance by default (auto simp add:
23394
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    58
    inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
15737
nipkow
parents:
diff changeset
    59
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    60
end
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    61
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    62
instantiation char :: linorder
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    63
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    64
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    65
definition
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 30663
diff changeset
    66
  char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    67
    n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    68
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    69
definition
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 30663
diff changeset
    70
  char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    71
    n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    72
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    73
instance
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    74
  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
    75
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    76
end
15737
nipkow
parents:
diff changeset
    77
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    78
instantiation char :: distrib_lattice
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    79
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    80
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    81
definition
25502
9200b36280c0 instance command as rudimentary class target
haftmann
parents: 23394
diff changeset
    82
  "(inf \<Colon> char \<Rightarrow> _) = min"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    83
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    84
definition
25502
9200b36280c0 instance command as rudimentary class target
haftmann
parents: 23394
diff changeset
    85
  "(sup \<Colon> char \<Rightarrow> _) = max"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    86
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    87
instance   by default (auto simp add:
23394
474ff28210c0 tuned proofs;
wenzelm
parents: 22845
diff changeset
    88
    inf_char_def sup_char_def min_max.sup_inf_distrib1)
22483
86064f2f2188 added instance for lattice
haftmann
parents: 21911
diff changeset
    89
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    90
end
878c37886eed removed some legacy instantiations
haftmann
parents: 25502
diff changeset
    91
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 27682
diff changeset
    92
lemma [simp, code]:
22805
1166a966e7b4 moved stuff to Char_nat.thy
haftmann
parents: 22483
diff changeset
    93
  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
    94
  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
    95
  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
    96
17200
3a4d03d1a31b tuned presentation;
wenzelm
parents: 15737
diff changeset
    97
end