3 *) |
3 *) |
4 |
4 |
5 header {* Order on characters *} |
5 header {* Order on characters *} |
6 |
6 |
7 theory Char_ord |
7 theory Char_ord |
8 imports Char_nat |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 instantiation nibble :: linorder |
11 instantiation nibble :: linorder |
12 begin |
12 begin |
13 |
13 |
14 definition |
14 definition |
15 nibble_less_eq_def: "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m" |
15 "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m" |
16 |
16 |
17 definition |
17 definition |
18 nibble_less_def: "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m" |
18 "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m" |
19 |
19 |
20 instance proof |
20 instance proof |
21 fix n :: nibble |
21 qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff) |
22 show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto |
|
23 next |
|
24 fix n m q :: nibble |
|
25 assume "n \<le> m" |
|
26 and "m \<le> q" |
|
27 then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto |
|
28 next |
|
29 fix n m :: nibble |
|
30 assume "n \<le> m" |
|
31 and "m \<le> n" |
|
32 then show "n = m" |
|
33 unfolding nibble_less_eq_def nibble_less_def |
|
34 by (auto simp add: nat_of_nibble_eq) |
|
35 next |
|
36 fix n m :: nibble |
|
37 show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" |
|
38 unfolding nibble_less_eq_def nibble_less_def less_le |
|
39 by (auto simp add: nat_of_nibble_eq) |
|
40 next |
|
41 fix n m :: nibble |
|
42 show "n \<le> m \<or> m \<le> n" |
|
43 unfolding nibble_less_eq_def by auto |
|
44 qed |
|
45 |
22 |
46 end |
23 end |
47 |
24 |
48 instantiation nibble :: distrib_lattice |
25 instantiation nibble :: distrib_lattice |
49 begin |
26 begin |
52 "(inf \<Colon> nibble \<Rightarrow> _) = min" |
29 "(inf \<Colon> nibble \<Rightarrow> _) = min" |
53 |
30 |
54 definition |
31 definition |
55 "(sup \<Colon> nibble \<Rightarrow> _) = max" |
32 "(sup \<Colon> nibble \<Rightarrow> _) = max" |
56 |
33 |
57 instance by default (auto simp add: |
34 instance proof |
58 inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) |
35 qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) |
59 |
36 |
60 end |
37 end |
61 |
38 |
62 instantiation char :: linorder |
39 instantiation char :: linorder |
63 begin |
40 begin |
64 |
41 |
65 definition |
42 definition |
66 char_less_eq_def: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> |
43 "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2" |
67 n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)" |
|
68 |
44 |
69 definition |
45 definition |
70 char_less_def: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> |
46 "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2" |
71 n1 < n2 \<or> n1 = n2 \<and> m1 < m2)" |
|
72 |
47 |
73 instance |
48 instance proof |
74 by default (auto simp: char_less_eq_def char_less_def split: char.splits) |
49 qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff) |
75 |
50 |
76 end |
51 end |
|
52 |
|
53 lemma less_eq_char_Char: |
|
54 "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" |
|
55 proof - |
|
56 { |
|
57 assume "nat_of_nibble n1 * 16 + nat_of_nibble m1 |
|
58 \<le> nat_of_nibble n2 * 16 + nat_of_nibble m2" |
|
59 then have "nat_of_nibble n1 \<le> nat_of_nibble n2" |
|
60 using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto |
|
61 } |
|
62 note * = this |
|
63 show ?thesis |
|
64 using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] |
|
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: *) |
|
66 qed |
|
67 |
|
68 lemma less_char_Char: |
|
69 "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2" |
|
70 proof - |
|
71 { |
|
72 assume "nat_of_nibble n1 * 16 + nat_of_nibble m1 |
|
73 < nat_of_nibble n2 * 16 + nat_of_nibble m2" |
|
74 then have "nat_of_nibble n1 \<le> nat_of_nibble n2" |
|
75 using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] by auto |
|
76 } |
|
77 note * = this |
|
78 show ?thesis |
|
79 using nat_of_nibble_less_16 [of m1] nat_of_nibble_less_16 [of m2] |
|
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: *) |
|
81 qed |
77 |
82 |
78 instantiation char :: distrib_lattice |
83 instantiation char :: distrib_lattice |
79 begin |
84 begin |
80 |
85 |
81 definition |
86 definition |
82 "(inf \<Colon> char \<Rightarrow> _) = min" |
87 "(inf \<Colon> char \<Rightarrow> _) = min" |
83 |
88 |
84 definition |
89 definition |
85 "(sup \<Colon> char \<Rightarrow> _) = max" |
90 "(sup \<Colon> char \<Rightarrow> _) = max" |
86 |
91 |
87 instance by default (auto simp add: |
92 instance proof |
88 inf_char_def sup_char_def min_max.sup_inf_distrib1) |
93 qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1) |
89 |
94 |
90 end |
95 end |
91 |
96 |
92 lemma [simp, code]: |
97 text {* Legacy aliasses *} |
93 shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" |
98 |
94 and char_less_simp: "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2" |
99 lemmas nibble_less_eq_def = less_eq_nibble_def |
95 unfolding char_less_eq_def char_less_def by simp_all |
100 lemmas nibble_less_def = less_nibble_def |
|
101 lemmas char_less_eq_def = less_eq_char_def |
|
102 lemmas char_less_def = less_char_def |
|
103 lemmas char_less_eq_simp = less_eq_char_Char |
|
104 lemmas char_less_simp = less_char_Char |
96 |
105 |
97 end |
106 end |
|
107 |