author | haftmann |
Thu, 19 Jul 2007 21:47:39 +0200 | |
changeset 23854 | 688a8a7bcd4e |
parent 22845 | 5f9138bcb3d7 |
child 25502 | 9200b36280c0 |
permissions | -rw-r--r-- |
15737 | 1 |
(* Title: HOL/Library/List_lexord.thy |
2 |
ID: $Id$ |
|
3 |
Author: Norbert Voelker |
|
4 |
*) |
|
5 |
||
17200 | 6 |
header {* Lexicographic order on lists *} |
15737 | 7 |
|
8 |
theory List_lexord |
|
9 |
imports Main |
|
10 |
begin |
|
11 |
||
21458 | 12 |
instance list :: (ord) ord |
17200 | 13 |
list_le_def: "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)" |
21458 | 14 |
list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" .. |
15737 | 15 |
|
22845 | 16 |
lemmas list_ord_defs [code func del] = list_less_def list_le_def |
15737 | 17 |
|
17200 | 18 |
instance list :: (order) order |
15737 | 19 |
apply (intro_classes, unfold list_ord_defs) |
22316 | 20 |
apply safe |
15737 | 21 |
apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE]) |
22 |
apply simp |
|
17200 | 23 |
apply assumption |
22316 | 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 (blast intro: lexord_trans transI order_less_trans) |
|
17200 | 28 |
done |
15737 | 29 |
|
21458 | 30 |
instance list :: (linorder) linorder |
15737 | 31 |
apply (intro_classes, unfold list_le_def list_less_def, safe) |
17200 | 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 |
|
15737 | 36 |
|
22483 | 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 |
||
22845 | 43 |
lemmas [code func del] = inf_list_def sup_list_def |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22483
diff
changeset
|
44 |
|
22177 | 45 |
lemma not_less_Nil [simp]: "\<not> (x < [])" |
17200 | 46 |
by (unfold list_less_def) simp |
15737 | 47 |
|
22177 | 48 |
lemma Nil_less_Cons [simp]: "[] < a # x" |
17200 | 49 |
by (unfold list_less_def) simp |
15737 | 50 |
|
22177 | 51 |
lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y" |
17200 | 52 |
by (unfold list_less_def) simp |
15737 | 53 |
|
22177 | 54 |
lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []" |
55 |
by (unfold list_ord_defs, cases x) auto |
|
56 |
||
57 |
lemma Nil_le_Cons [simp]: "[] \<le> x" |
|
17200 | 58 |
by (unfold list_ord_defs, cases x) auto |
15737 | 59 |
|
22177 | 60 |
lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y" |
17200 | 61 |
by (unfold list_ord_defs) auto |
15737 | 62 |
|
22177 | 63 |
lemma less_code [code func]: |
64 |
"xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False" |
|
65 |
"[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True" |
|
66 |
"(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys" |
|
67 |
by simp_all |
|
68 |
||
69 |
lemma less_eq_code [code func]: |
|
70 |
"x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False" |
|
71 |
"[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True" |
|
72 |
"(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys" |
|
73 |
by simp_all |
|
74 |
||
17200 | 75 |
end |