equal
deleted
inserted
replaced
11 |
11 |
12 instance list :: (ord) ord |
12 instance list :: (ord) ord |
13 list_le_def: "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)" |
13 list_le_def: "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)" |
14 list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" .. |
14 list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" .. |
15 |
15 |
16 lemmas list_ord_defs = list_less_def list_le_def |
16 lemmas list_ord_defs [code nofunc] = list_less_def list_le_def |
17 |
17 |
18 instance list :: (order) order |
18 instance list :: (order) order |
19 apply (intro_classes, unfold list_ord_defs) |
19 apply (intro_classes, unfold list_ord_defs) |
20 apply safe |
20 apply safe |
21 apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE]) |
21 apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE]) |
37 instance list :: (linorder) distrib_lattice |
37 instance list :: (linorder) distrib_lattice |
38 "inf \<equiv> min" |
38 "inf \<equiv> min" |
39 "sup \<equiv> max" |
39 "sup \<equiv> max" |
40 by intro_classes |
40 by intro_classes |
41 (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1) |
41 (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1) |
|
42 |
|
43 lemmas [code nofunc] = inf_list_def sup_list_def |
42 |
44 |
43 lemma not_less_Nil [simp]: "\<not> (x < [])" |
45 lemma not_less_Nil [simp]: "\<not> (x < [])" |
44 by (unfold list_less_def) simp |
46 by (unfold list_less_def) simp |
45 |
47 |
46 lemma Nil_less_Cons [simp]: "[] < a # x" |
48 lemma Nil_less_Cons [simp]: "[] < a # x" |