1.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Jun 21 09:06:14 2010 +0200
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Jun 21 09:38:20 2010 +0200
     1.3 @@ -10,17 +10,20 @@
     1.4  
     1.5  subsection {* Prefix order on lists *}
     1.6  
     1.7 -instantiation list :: (type) order
     1.8 +instantiation list :: (type) "{order, bot}"
     1.9  begin
    1.10  
    1.11  definition
    1.12 -  prefix_def [code del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
    1.13 +  prefix_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
    1.14  
    1.15  definition
    1.16 -  strict_prefix_def [code del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
    1.17 +  strict_prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    1.18  
    1.19 -instance
    1.20 -  by intro_classes (auto simp add: prefix_def strict_prefix_def)
    1.21 +definition
    1.22 +  "bot = []"
    1.23 +
    1.24 +instance proof
    1.25 +qed (auto simp add: prefix_def strict_prefix_def bot_list_def)
    1.26  
    1.27  end
    1.28  
    1.29 @@ -77,6 +80,12 @@
    1.30  lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
    1.31    by (auto simp add: prefix_def)
    1.32  
    1.33 +lemma less_eq_list_code [code]:
    1.34 +  "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
    1.35 +  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
    1.36 +  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
    1.37 +  by simp_all
    1.38 +
    1.39  lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
    1.40    by (induct xs) simp_all
    1.41  
    1.42 @@ -125,10 +134,10 @@
    1.43  lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
    1.44    by (auto simp: strict_prefix_def prefix_def)
    1.45  
    1.46 -lemma strict_prefix_simps [simp]:
    1.47 -    "xs < [] = False"
    1.48 -    "[] < (x # xs) = True"
    1.49 -    "(x # xs) < (y # ys) = (x = y \<and> xs < ys)"
    1.50 +lemma strict_prefix_simps [simp, code]:
    1.51 +  "xs < [] \<longleftrightarrow> False"
    1.52 +  "[] < x # xs \<longleftrightarrow> True"
    1.53 +  "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
    1.54    by (simp_all add: strict_prefix_def cong: conj_cong)
    1.55  
    1.56  lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys"
    1.57 @@ -301,7 +310,7 @@
    1.58      by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
    1.59  qed
    1.60  
    1.61 -lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
    1.62 +lemma postfix_to_prefix [code]: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
    1.63  proof
    1.64    assume "xs >>= ys"
    1.65    then obtain zs where "xs = zs @ ys" ..
    1.66 @@ -370,21 +379,4 @@
    1.67    qed
    1.68  qed
    1.69  
    1.70 -
    1.71 -subsection {* Executable code *}
    1.72 -
    1.73 -lemma less_eq_code [code]:
    1.74 -    "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
    1.75 -    "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
    1.76 -    "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
    1.77 -  by simp_all
    1.78 -
    1.79 -lemma less_code [code]:
    1.80 -    "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
    1.81 -    "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
    1.82 -    "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
    1.83 -  unfolding strict_prefix_def by auto
    1.84 -
    1.85 -lemmas [code] = postfix_to_prefix
    1.86 -
    1.87  end

     2.1 --- a/src/HOL/Library/List_lexord.thy	Mon Jun 21 09:06:14 2010 +0200
     2.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Jun 21 09:38:20 2010 +0200
     2.3 @@ -12,10 +12,10 @@
     2.4  begin
     2.5  
     2.6  definition
     2.7 -  list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
     2.8 +  list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}"
     2.9  
    2.10  definition
    2.11 -  list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
    2.12 +  list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
    2.13  
    2.14  instance ..
    2.15  
    2.16 @@ -91,13 +91,24 @@
    2.17  lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
    2.18    by (unfold list_le_def) auto
    2.19  
    2.20 -lemma less_code [code]:
    2.21 +instantiation list :: (order) bot
    2.22 +begin
    2.23 +
    2.24 +definition
    2.25 +  "bot = []"
    2.26 +
    2.27 +instance proof
    2.28 +qed (simp add: bot_list_def)
    2.29 +
    2.30 +end
    2.31 +
    2.32 +lemma less_list_code [code]:
    2.33    "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
    2.34    "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
    2.35    "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
    2.36    by simp_all
    2.37  
    2.38 -lemma less_eq_code [code]:
    2.39 +lemma less_eq_list_code [code]:
    2.40    "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
    2.41    "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
    2.42    "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"