author | haftmann |
Fri, 15 Feb 2013 11:47:33 +0100 | |
changeset 51160 | 599ff65b85e2 |
parent 48926 | 8d7778a19857 |
child 54595 | a2eeeb335a48 |
permissions | -rw-r--r-- |
15737 | 1 |
(* Title: HOL/Library/Char_ord.thy |
22805 | 2 |
Author: Norbert Voelker, Florian Haftmann |
15737 | 3 |
*) |
4 |
||
17200 | 5 |
header {* Order on characters *} |
15737 | 6 |
|
7 |
theory Char_ord |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
8 |
imports Main |
15737 | 9 |
begin |
10 |
||
25764 | 11 |
instantiation nibble :: linorder |
12 |
begin |
|
13 |
||
14 |
definition |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
15 |
"n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m" |
25764 | 16 |
|
17 |
definition |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
18 |
"n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m" |
25764 | 19 |
|
20 |
instance proof |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
21 |
qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff) |
15737 | 22 |
|
25764 | 23 |
end |
24 |
||
25 |
instantiation nibble :: distrib_lattice |
|
26 |
begin |
|
27 |
||
28 |
definition |
|
25502 | 29 |
"(inf \<Colon> nibble \<Rightarrow> _) = min" |
25764 | 30 |
|
31 |
definition |
|
25502 | 32 |
"(sup \<Colon> nibble \<Rightarrow> _) = max" |
25764 | 33 |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
34 |
instance proof |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
35 |
qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) |
15737 | 36 |
|
25764 | 37 |
end |
38 |
||
39 |
instantiation char :: linorder |
|
40 |
begin |
|
41 |
||
42 |
definition |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
43 |
"c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2" |
25764 | 44 |
|
45 |
definition |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
46 |
"c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2" |
25764 | 47 |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
48 |
instance proof |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
49 |
qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff) |
22805 | 50 |
|
25764 | 51 |
end |
15737 | 52 |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
53 |
lemma less_eq_char_Char: |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
54 |
"Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
55 |
proof - |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
56 |
{ |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
57 |
assume "nat_of_nibble n1 * 16 + nat_of_nibble m1 |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
58 |
\<le> nat_of_nibble n2 * 16 + nat_of_nibble m2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
59 |
then have "nat_of_nibble n1 \<le> nat_of_nibble n2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
60 |
using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
61 |
} |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
62 |
note * = this |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
63 |
show ?thesis |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
64 |
using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
65 |
by (auto simp add: less_eq_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *) |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
66 |
qed |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
67 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
68 |
lemma less_char_Char: |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
69 |
"Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
70 |
proof - |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
71 |
{ |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
72 |
assume "nat_of_nibble n1 * 16 + nat_of_nibble m1 |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
73 |
< nat_of_nibble n2 * 16 + nat_of_nibble m2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
74 |
then have "nat_of_nibble n1 \<le> nat_of_nibble n2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
75 |
using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
76 |
} |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
77 |
note * = this |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
78 |
show ?thesis |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
79 |
using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
80 |
by (auto simp add: less_char_def nat_of_char_Char less_eq_nibble_def less_nibble_def not_less nat_of_nibble_eq_iff dest: *) |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
81 |
qed |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
82 |
|
25764 | 83 |
instantiation char :: distrib_lattice |
84 |
begin |
|
85 |
||
86 |
definition |
|
25502 | 87 |
"(inf \<Colon> char \<Rightarrow> _) = min" |
25764 | 88 |
|
89 |
definition |
|
25502 | 90 |
"(sup \<Colon> char \<Rightarrow> _) = max" |
25764 | 91 |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
92 |
instance proof |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
93 |
qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1) |
22483 | 94 |
|
25764 | 95 |
end |
96 |
||
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
97 |
text {* Legacy aliasses *} |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
98 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
99 |
lemmas nibble_less_eq_def = less_eq_nibble_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
100 |
lemmas nibble_less_def = less_nibble_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
101 |
lemmas char_less_eq_def = less_eq_char_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
102 |
lemmas char_less_def = less_char_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
103 |
lemmas char_less_eq_simp = less_eq_char_Char |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
104 |
lemmas char_less_simp = less_char_Char |
21871
9ce66839d9f1
added code generation syntax for some char combinators
haftmann
parents:
21404
diff
changeset
|
105 |
|
17200 | 106 |
end |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
107 |