equal
deleted
inserted
replaced
32 apply (cut_tac x = x and y = y and r = "{(a,b). a < b}" in lexord_linear) |
32 apply (cut_tac x = x and y = y and r = "{(a,b). a < b}" in lexord_linear) |
33 apply force |
33 apply force |
34 apply simp |
34 apply simp |
35 done |
35 done |
36 |
36 |
|
37 instance list :: (linorder) distrib_lattice |
|
38 "inf \<equiv> min" |
|
39 "sup \<equiv> max" |
|
40 by intro_classes |
|
41 (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1) |
|
42 |
37 lemma not_less_Nil [simp]: "\<not> (x < [])" |
43 lemma not_less_Nil [simp]: "\<not> (x < [])" |
38 by (unfold list_less_def) simp |
44 by (unfold list_less_def) simp |
39 |
45 |
40 lemma Nil_less_Cons [simp]: "[] < a # x" |
46 lemma Nil_less_Cons [simp]: "[] < a # x" |
41 by (unfold list_less_def) simp |
47 by (unfold list_less_def) simp |