21 instance .. |
21 instance .. |
22 |
22 |
23 end |
23 end |
24 |
24 |
25 instance list :: (order) order |
25 instance list :: (order) order |
26 apply (intro_classes, unfold list_less_def list_le_def) |
26 proof |
27 apply safe |
27 fix xs :: "'a list" |
28 apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE]) |
28 show "xs \<le> xs" by (simp add: list_le_def) |
29 apply simp |
29 next |
30 apply assumption |
30 fix xs ys zs :: "'a list" |
31 apply (blast intro: lexord_trans transI order_less_trans) |
31 assume "xs \<le> ys" and "ys \<le> zs" |
32 apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE]) |
32 then show "xs \<le> zs" by (auto simp add: list_le_def list_less_def) |
33 apply simp |
33 (rule lexord_trans, auto intro: transI) |
34 apply (blast intro: lexord_trans transI order_less_trans) |
34 next |
35 done |
35 fix xs ys :: "'a list" |
|
36 assume "xs \<le> ys" and "ys \<le> xs" |
|
37 then show "xs = ys" apply (auto simp add: list_le_def list_less_def) |
|
38 apply (rule lexord_irreflexive [THEN notE]) |
|
39 defer |
|
40 apply (rule lexord_trans) apply (auto intro: transI) done |
|
41 next |
|
42 fix xs ys :: "'a list" |
|
43 show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" |
|
44 apply (auto simp add: list_less_def list_le_def) |
|
45 defer |
|
46 apply (rule lexord_irreflexive [THEN notE]) |
|
47 apply auto |
|
48 apply (rule lexord_irreflexive [THEN notE]) |
|
49 defer |
|
50 apply (rule lexord_trans) apply (auto intro: transI) done |
|
51 qed |
36 |
52 |
37 instance list :: (linorder) linorder |
53 instance list :: (linorder) linorder |
38 apply (intro_classes, unfold list_le_def list_less_def, safe) |
54 proof |
39 apply (cut_tac x = x and y = y and r = "{(a,b). a < b}" in lexord_linear) |
55 fix xs ys :: "'a list" |
40 apply force |
56 have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}" |
41 apply simp |
57 by (rule lexord_linear) auto |
42 done |
58 then show "xs \<le> ys \<or> ys \<le> xs" |
|
59 by (auto simp add: list_le_def list_less_def) |
|
60 qed |
43 |
61 |
44 instantiation list :: (linorder) distrib_lattice |
62 instantiation list :: (linorder) distrib_lattice |
45 begin |
63 begin |
46 |
64 |
47 definition |
65 definition |