author | paulson |
Mon, 30 Nov 2020 19:33:07 +0000 | |
changeset 72796 | d39a32cff5d7 |
parent 68028 | 1f9f973eed2a |
child 75600 | 6de655ccac19 |
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 |
|
63462 | 8 |
imports Main |
15737 | 9 |
begin |
10 |
||
25764 | 11 |
instantiation char :: linorder |
12 |
begin |
|
13 |
||
68028 | 14 |
definition less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool" |
15 |
where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)" |
|
16 |
||
17 |
definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool" |
|
18 |
where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)" |
|
19 |
||
25764 | 20 |
|
60679 | 21 |
instance |
62597 | 22 |
by standard (auto simp add: less_eq_char_def less_char_def) |
22805 | 23 |
|
25764 | 24 |
end |
15737 | 25 |
|
68028 | 26 |
lemma less_eq_char_simp [simp]: |
27 |
"Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7 |
|
28 |
\<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0 |
|
29 |
\<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)" |
|
30 |
by (simp add: less_eq_char_def) |
|
51160
599ff65b85e2
systematic conversions between nat and nibble/char;
haftmann
parents:
48926
diff
changeset
|
31 |
|
68028 | 32 |
lemma less_char_simp [simp]: |
33 |
"Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7 |
|
34 |
\<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0 |
|
35 |
< foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)" |
|
36 |
by (simp add: less_char_def) |
|
63462 | 37 |
|
25764 | 38 |
instantiation char :: distrib_lattice |
39 |
begin |
|
40 |
||
61076 | 41 |
definition "(inf :: char \<Rightarrow> _) = min" |
42 |
definition "(sup :: char \<Rightarrow> _) = max" |
|
25764 | 43 |
|
60679 | 44 |
instance |
45 |
by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2) |
|
22483 | 46 |
|
25764 | 47 |
end |
48 |
||
54595
a2eeeb335a48
instantiate linorder for String.literal by lexicographic order
Andreas Lochbihler
parents:
51160
diff
changeset
|
49 |
end |