11 |
11 |
12 instance nibble :: linorder |
12 instance nibble :: linorder |
13 nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m" |
13 nibble_less_eq_def: "n \<le> m \<equiv> nat_of_nibble n \<le> nat_of_nibble m" |
14 nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m" |
14 nibble_less_def: "n < m \<equiv> nat_of_nibble n < nat_of_nibble m" |
15 proof |
15 proof |
16 fix n :: nibble show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto |
16 fix n :: nibble |
|
17 show "n \<le> n" unfolding nibble_less_eq_def nibble_less_def by auto |
17 next |
18 next |
18 fix n m q :: nibble |
19 fix n m q :: nibble |
19 assume "n \<le> m" |
20 assume "n \<le> m" |
20 and "m \<le> q" |
21 and "m \<le> q" |
21 then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto |
22 then show "n \<le> q" unfolding nibble_less_eq_def nibble_less_def by auto |
22 next |
23 next |
23 fix n m :: nibble |
24 fix n m :: nibble |
24 assume "n \<le> m" |
25 assume "n \<le> m" |
25 and "m \<le> n" |
26 and "m \<le> n" |
26 then show "n = m" unfolding nibble_less_eq_def nibble_less_def by (auto simp add: nat_of_nibble_eq) |
27 then show "n = m" |
|
28 unfolding nibble_less_eq_def nibble_less_def |
|
29 by (auto simp add: nat_of_nibble_eq) |
27 next |
30 next |
28 fix n m :: nibble |
31 fix n m :: nibble |
29 show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m" |
32 show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m" |
30 unfolding nibble_less_eq_def nibble_less_def less_le by (auto simp add: nat_of_nibble_eq) |
33 unfolding nibble_less_eq_def nibble_less_def less_le |
|
34 by (auto simp add: nat_of_nibble_eq) |
31 next |
35 next |
32 fix n m :: nibble |
36 fix n m :: nibble |
33 show "n \<le> m \<or> m \<le> n" |
37 show "n \<le> m \<or> m \<le> n" |
34 unfolding nibble_less_eq_def by auto |
38 unfolding nibble_less_eq_def by auto |
35 qed |
39 qed |
36 |
40 |
37 instance nibble :: distrib_lattice |
41 instance nibble :: distrib_lattice |
38 "inf \<equiv> min" |
42 "inf \<equiv> min" |
39 "sup \<equiv> max" |
43 "sup \<equiv> max" |
40 by default |
44 by default (auto simp add: |
41 (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) |
45 inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) |
42 |
46 |
43 instance char :: linorder |
47 instance char :: linorder |
44 char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> |
48 char_less_eq_def: "c1 \<le> c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> |
45 n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" |
49 n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" |
46 char_less_def: "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> |
50 char_less_def: "c1 < c2 \<equiv> case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow> |
48 by default (auto simp: char_less_eq_def char_less_def split: char.splits) |
52 by default (auto simp: char_less_eq_def char_less_def split: char.splits) |
49 |
53 |
50 lemmas [code func del] = char_less_eq_def char_less_def |
54 lemmas [code func del] = char_less_eq_def char_less_def |
51 |
55 |
52 instance char :: distrib_lattice |
56 instance char :: distrib_lattice |
53 "inf \<equiv> min" |
57 "inf \<equiv> min" |
54 "sup \<equiv> max" |
58 "sup \<equiv> max" |
55 by default |
59 by default (auto simp add: |
56 (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1) |
60 inf_char_def sup_char_def min_max.sup_inf_distrib1) |
57 |
61 |
58 lemma [simp, code func]: |
62 lemma [simp, code func]: |
59 shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" |
63 shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2" |
60 and char_less_simp: "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2" |
64 and char_less_simp: "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2" |
61 unfolding char_less_eq_def char_less_def by simp_all |
65 unfolding char_less_eq_def char_less_def by simp_all |