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.28 +qed (simp add: bot_list_def)
    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"