src/HOL/Library/List_lexord.thy
 author haftmann Mon Jul 12 08:58:13 2010 +0200 (2010-07-12) changeset 37765 26bdfb7b680b parent 37474 ce943f9edf5e child 38857 97775f3e8722 permissions -rw-r--r--
dropped superfluous [code del]s
1 (*  Title:      HOL/Library/List_lexord.thy
2     Author:     Norbert Voelker
3 *)
5 header {* Lexicographic order on lists *}
7 theory List_lexord
8 imports List Main
9 begin
11 instantiation list :: (ord) ord
12 begin
14 definition
15   list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}"
17 definition
18   list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
20 instance ..
22 end
24 instance list :: (order) order
25 proof
26   fix xs :: "'a list"
27   show "xs \<le> xs" by (simp add: list_le_def)
28 next
29   fix xs ys zs :: "'a list"
30   assume "xs \<le> ys" and "ys \<le> zs"
31   then show "xs \<le> zs" by (auto simp add: list_le_def list_less_def)
32     (rule lexord_trans, auto intro: transI)
33 next
34   fix xs ys :: "'a list"
35   assume "xs \<le> ys" and "ys \<le> xs"
36   then show "xs = ys" apply (auto simp add: list_le_def list_less_def)
37   apply (rule lexord_irreflexive [THEN notE])
38   defer
39   apply (rule lexord_trans) apply (auto intro: transI) done
40 next
41   fix xs ys :: "'a list"
42   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
43   apply (auto simp add: list_less_def list_le_def)
44   defer
45   apply (rule lexord_irreflexive [THEN notE])
46   apply auto
47   apply (rule lexord_irreflexive [THEN notE])
48   defer
49   apply (rule lexord_trans) apply (auto intro: transI) done
50 qed
52 instance list :: (linorder) linorder
53 proof
54   fix xs ys :: "'a list"
55   have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
56     by (rule lexord_linear) auto
57   then show "xs \<le> ys \<or> ys \<le> xs"
58     by (auto simp add: list_le_def list_less_def)
59 qed
61 instantiation list :: (linorder) distrib_lattice
62 begin
64 definition
65   "(inf \<Colon> 'a list \<Rightarrow> _) = min"
67 definition
68   "(sup \<Colon> 'a list \<Rightarrow> _) = max"
70 instance
71   by intro_classes
72     (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
74 end
76 lemma not_less_Nil [simp]: "\<not> (x < [])"
77   by (unfold list_less_def) simp
79 lemma Nil_less_Cons [simp]: "[] < a # x"
80   by (unfold list_less_def) simp
82 lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
83   by (unfold list_less_def) simp
85 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
86   by (unfold list_le_def, cases x) auto
88 lemma Nil_le_Cons [simp]: "[] \<le> x"
89   by (unfold list_le_def, cases x) auto
91 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
92   by (unfold list_le_def) auto
94 instantiation list :: (order) bot
95 begin
97 definition
98   "bot = []"
100 instance proof