equal
deleted
inserted
replaced
37 show "n \<le> m \<or> m \<le> n" |
37 show "n \<le> m \<or> m \<le> n" |
38 unfolding nibble_less_eq_def by auto |
38 unfolding nibble_less_eq_def by auto |
39 qed |
39 qed |
40 |
40 |
41 instance nibble :: distrib_lattice |
41 instance nibble :: distrib_lattice |
42 "inf \<equiv> min" |
42 "(inf \<Colon> nibble \<Rightarrow> _) = min" |
43 "sup \<equiv> max" |
43 "(sup \<Colon> nibble \<Rightarrow> _) = max" |
44 by default (auto simp add: |
44 by default (auto simp add: |
45 inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) |
45 inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) |
46 |
46 |
47 instance char :: linorder |
47 instance char :: linorder |
48 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> |
52 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) |
53 |
53 |
54 lemmas [code func del] = char_less_eq_def char_less_def |
54 lemmas [code func del] = char_less_eq_def char_less_def |
55 |
55 |
56 instance char :: distrib_lattice |
56 instance char :: distrib_lattice |
57 "inf \<equiv> min" |
57 "(inf \<Colon> char \<Rightarrow> _) = min" |
58 "sup \<equiv> max" |
58 "(sup \<Colon> char \<Rightarrow> _) = max" |
59 by default (auto simp add: |
59 by default (auto simp add: |
60 inf_char_def sup_char_def min_max.sup_inf_distrib1) |
60 inf_char_def sup_char_def min_max.sup_inf_distrib1) |
61 |
61 |
62 lemma [simp, code func]: |
62 lemma [simp, code func]: |
63 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" |