src/HOL/Library/List_lexord.thy
 author haftmann Wed Nov 22 10:20:18 2006 +0100 (2006-11-22) changeset 21458 475b321982f7 parent 17200 3a4d03d1a31b child 22177 515021e98684 permissions -rw-r--r--
1 (*  Title:      HOL/Library/List_lexord.thy
2     ID:         \$Id\$
3     Author:     Norbert Voelker
4 *)
6 header {* Lexicographic order on lists *}
8 theory List_lexord
9 imports Main
10 begin
12 instance list :: (ord) ord
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}" ..
16 lemmas list_ord_defs = list_less_def list_le_def
18 instance list :: (order) order
19   apply (intro_classes, unfold list_ord_defs)
20      apply (rule disjI2, safe)
21     apply (blast intro: lexord_trans transI order_less_trans)
22    apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
23     apply simp
24    apply (blast intro: lexord_trans transI order_less_trans)
25   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
26   apply simp
27   apply assumption
28   done
30 instance list :: (linorder) linorder
31   apply (intro_classes, unfold list_le_def list_less_def, safe)
32   apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
33    apply force
34   apply simp
35   done
37 lemma not_less_Nil [simp, code func]: "~(x < [])"
38   by (unfold list_less_def) simp
40 lemma Nil_less_Cons [simp, code func]: "[] < a # x"
41   by (unfold list_less_def) simp
43 lemma Cons_less_Cons [simp, code func]: "(a # x < b # y) = (a < b | a = b & x < y)"
44   by (unfold list_less_def) simp
46 lemma le_Nil [simp, code func]: "(x <= []) = (x = [])"
47   by (unfold list_ord_defs, cases x) auto
49 lemma Nil_le_Cons [simp, code func]: "([] <= x)"
50   by (unfold list_ord_defs, cases x) auto
52 lemma Cons_le_Cons [simp, code func]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
53   by (unfold list_ord_defs) auto
55 end