author | hoelzl |
Mon, 20 Oct 2014 18:33:14 +0200 | |
changeset 58729 | e8ecc79aee43 |
parent 57437 | 0baf08c075b9 |
child 58881 | b9556a055632 |
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 |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54595
diff
changeset
|
35 |
qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2) |
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 |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54595
diff
changeset
|
93 |
qed (auto simp add: inf_char_def sup_char_def max_min_distrib2) |
22483 | 94 |
|
25764 | 95 |
end |
96 |
||
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
97 |
instantiation String.literal :: linorder |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
98 |
begin |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
99 |
|
55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset
|
100 |
context includes literal.lifting begin |
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
101 |
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" . |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
102 |
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" . |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
103 |
|
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
104 |
instance |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
105 |
proof - |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
106 |
interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool" |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
107 |
by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales) |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
108 |
show "PROP ?thesis" |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
109 |
by(intro_classes)(transfer, simp add: less_le_not_le linear)+ |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
110 |
qed |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
111 |
|
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
112 |
end |
55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset
|
113 |
end |
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
114 |
|
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
115 |
lemma less_literal_code [code]: |
57437 | 116 |
"op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))" |
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
117 |
by(simp add: less_literal.rep_eq fun_eq_iff) |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
118 |
|
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
119 |
lemma less_eq_literal_code [code]: |
57437 | 120 |
"op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))" |
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
121 |
by(simp add: less_eq_literal.rep_eq fun_eq_iff) |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
122 |
|
55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset
|
123 |
lifting_update literal.lifting |
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset
|
124 |
lifting_forget literal.lifting |
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset
|
125 |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
126 |
text {* Legacy aliasses *} |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
127 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
128 |
lemmas nibble_less_eq_def = less_eq_nibble_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
129 |
lemmas nibble_less_def = less_nibble_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
130 |
lemmas char_less_eq_def = less_eq_char_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
131 |
lemmas char_less_def = less_char_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
132 |
lemmas char_less_eq_simp = less_eq_char_Char |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
133 |
lemmas char_less_simp = less_char_Char |
21871
9ce66839d9f1
added code generation syntax for some char combinators
haftmann
parents:
21404
diff
changeset
|
134 |
|
17200 | 135 |
end |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
136 |