author | wenzelm |
Mon, 15 Feb 2016 14:55:44 +0100 | |
changeset 62337 | d3996d5873dd |
parent 61076 | bdc1e2f0a86a |
child 62597 | b3f2b8c906a6 |
permissions | -rw-r--r-- |
15737 | 1 |
(* Title: HOL/Library/Char_ord.thy |
22805 | 2 |
Author: Norbert Voelker, Florian Haftmann |
15737 | 3 |
*) |
4 |
||
60500 | 5 |
section \<open>Order on characters\<close> |
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 |
||
60679 | 14 |
definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m" |
15 |
definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m" |
|
25764 | 16 |
|
60679 | 17 |
instance |
18 |
by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff) |
|
15737 | 19 |
|
25764 | 20 |
end |
21 |
||
22 |
instantiation nibble :: distrib_lattice |
|
23 |
begin |
|
24 |
||
61076 | 25 |
definition "(inf :: nibble \<Rightarrow> _) = min" |
26 |
definition "(sup :: nibble \<Rightarrow> _) = max" |
|
25764 | 27 |
|
60679 | 28 |
instance |
29 |
by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2) |
|
15737 | 30 |
|
25764 | 31 |
end |
32 |
||
33 |
instantiation char :: linorder |
|
34 |
begin |
|
35 |
||
60679 | 36 |
definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2" |
37 |
definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2" |
|
25764 | 38 |
|
60679 | 39 |
instance |
40 |
by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff) |
|
22805 | 41 |
|
25764 | 42 |
end |
15737 | 43 |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
44 |
lemma less_eq_char_Char: |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
45 |
"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
|
46 |
proof - |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
47 |
{ |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
48 |
assume "nat_of_nibble n1 * 16 + nat_of_nibble m1 |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
49 |
\<le> nat_of_nibble n2 * 16 + nat_of_nibble m2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
50 |
then have "nat_of_nibble n1 \<le> nat_of_nibble n2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
51 |
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
|
52 |
} |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
53 |
note * = this |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
54 |
show ?thesis |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
qed |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
58 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
59 |
lemma less_char_Char: |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
60 |
"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
|
61 |
proof - |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
62 |
{ |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
63 |
assume "nat_of_nibble n1 * 16 + nat_of_nibble m1 |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
64 |
< nat_of_nibble n2 * 16 + nat_of_nibble m2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
65 |
then have "nat_of_nibble n1 \<le> nat_of_nibble n2" |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
66 |
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
|
67 |
} |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
68 |
note * = this |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
69 |
show ?thesis |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
70 |
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
|
71 |
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
|
72 |
qed |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
73 |
|
25764 | 74 |
instantiation char :: distrib_lattice |
75 |
begin |
|
76 |
||
61076 | 77 |
definition "(inf :: char \<Rightarrow> _) = min" |
78 |
definition "(sup :: char \<Rightarrow> _) = max" |
|
25764 | 79 |
|
60679 | 80 |
instance |
81 |
by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2) |
|
22483 | 82 |
|
25764 | 83 |
end |
84 |
||
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
85 |
instantiation String.literal :: linorder |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
86 |
begin |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
87 |
|
55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset
|
88 |
context includes literal.lifting begin |
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
89 |
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
|
90 |
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
|
91 |
|
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
92 |
instance |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
93 |
proof - |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
94 |
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
|
95 |
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
|
96 |
show "PROP ?thesis" |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
97 |
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
|
98 |
qed |
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
99 |
|
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
100 |
end |
55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset
|
101 |
end |
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
102 |
|
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
103 |
lemma less_literal_code [code]: |
57437 | 104 |
"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
|
105 |
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
|
106 |
|
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
107 |
lemma less_eq_literal_code [code]: |
57437 | 108 |
"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
|
109 |
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
|
110 |
|
55426
90f2ceed2828
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
Andreas Lochbihler
parents:
54863
diff
changeset
|
111 |
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
|
112 |
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
|
113 |
|
60500 | 114 |
text \<open>Legacy aliasses\<close> |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
115 |
|
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
116 |
lemmas nibble_less_eq_def = less_eq_nibble_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
117 |
lemmas nibble_less_def = less_nibble_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
118 |
lemmas char_less_eq_def = less_eq_char_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
119 |
lemmas char_less_def = less_char_def |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
120 |
lemmas char_less_eq_simp = less_eq_char_Char |
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
121 |
lemmas char_less_simp = less_char_Char |
21871
9ce66839d9f1
added code generation syntax for some char combinators
haftmann
parents:
21404
diff
changeset
|
122 |
|
17200 | 123 |
end |
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
124 |