src/HOL/Library/List_lexord.thy
 changeset 37474 ce943f9edf5e parent 30663 0b6aff7451b2 child 37765 26bdfb7b680b
```     1.1 --- a/src/HOL/Library/List_lexord.thy	Mon Jun 21 09:06:14 2010 +0200
1.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Jun 21 09:38:20 2010 +0200
1.3 @@ -12,10 +12,10 @@
1.4  begin
1.5
1.6  definition
1.7 -  list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
1.8 +  list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}"
1.9
1.10  definition
1.11 -  list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
1.12 +  list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
1.13
1.14  instance ..
1.15
1.16 @@ -91,13 +91,24 @@
1.17  lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
1.18    by (unfold list_le_def) auto
1.19
1.20 -lemma less_code [code]:
1.21 +instantiation list :: (order) bot
1.22 +begin
1.23 +
1.24 +definition
1.25 +  "bot = []"
1.26 +
1.27 +instance proof
1.29 +
1.30 +end
1.31 +
1.32 +lemma less_list_code [code]:
1.33    "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
1.34    "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
1.35    "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
1.36    by simp_all
1.37
1.38 -lemma less_eq_code [code]:
1.39 +lemma less_eq_list_code [code]:
1.40    "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
1.41    "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
1.42    "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
```