# HG changeset patch
# User haftmann
# Date 1277105900 -7200
# Node ID ce943f9edf5e495c291db877a6e03c0b38cfd705
# Parent  013f78aed840cf2fa1a3070a915ad507a94c7c86
added bot instances; tuned

diff -r 013f78aed840 -r ce943f9edf5e src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Mon Jun 21 09:06:14 2010 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Mon Jun 21 09:38:20 2010 +0200
@@ -10,17 +10,20 @@
 
 subsection {* Prefix order on lists *}
 
-instantiation list :: (type) order
+instantiation list :: (type) "{order, bot}"
 begin
 
 definition
-  prefix_def [code del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
+  prefix_def: "xs \<le> ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
 
 definition
-  strict_prefix_def [code del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
+  strict_prefix_def: "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
 
-instance
-  by intro_classes (auto simp add: prefix_def strict_prefix_def)
+definition
+  "bot = []"
+
+instance proof
+qed (auto simp add: prefix_def strict_prefix_def bot_list_def)
 
 end
 
@@ -77,6 +80,12 @@
 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
   by (auto simp add: prefix_def)
 
+lemma less_eq_list_code [code]:
+  "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
+  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
+  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
+  by simp_all
+
 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
   by (induct xs) simp_all
 
@@ -125,10 +134,10 @@
 lemma prefix_length_less: "xs < ys \<Longrightarrow> length xs < length ys"
   by (auto simp: strict_prefix_def prefix_def)
 
-lemma strict_prefix_simps [simp]:
-    "xs < [] = False"
-    "[] < (x # xs) = True"
-    "(x # xs) < (y # ys) = (x = y \<and> xs < ys)"
+lemma strict_prefix_simps [simp, code]:
+  "xs < [] \<longleftrightarrow> False"
+  "[] < x # xs \<longleftrightarrow> True"
+  "x # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
   by (simp_all add: strict_prefix_def cong: conj_cong)
 
 lemma take_strict_prefix: "xs < ys \<Longrightarrow> take n xs < ys"
@@ -301,7 +310,7 @@
     by (induct zs) (auto intro!: postfix_appendI postfix_ConsI)
 qed
 
-lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
+lemma postfix_to_prefix [code]: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs"
 proof
   assume "xs >>= ys"
   then obtain zs where "xs = zs @ ys" ..
@@ -370,21 +379,4 @@
   qed
 qed
 
-
-subsection {* Executable code *}
-
-lemma less_eq_code [code]:
-    "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
-    "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
-    "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
-  by simp_all
-
-lemma less_code [code]:
-    "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
-    "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
-    "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
-  unfolding strict_prefix_def by auto
-
-lemmas [code] = postfix_to_prefix
-
 end
diff -r 013f78aed840 -r ce943f9edf5e src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Mon Jun 21 09:06:14 2010 +0200
+++ b/src/HOL/Library/List_lexord.thy	Mon Jun 21 09:38:20 2010 +0200
@@ -12,10 +12,10 @@
 begin
 
 definition
-  list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
+  list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}"
 
 definition
-  list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
+  list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
 
 instance ..
 
@@ -91,13 +91,24 @@
 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
   by (unfold list_le_def) auto
 
-lemma less_code [code]:
+instantiation list :: (order) bot
+begin
+
+definition
+  "bot = []"
+
+instance proof
+qed (simp add: bot_list_def)
+
+end
+
+lemma less_list_code [code]:
   "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
   "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
   "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
   by simp_all
 
-lemma less_eq_code [code]:
+lemma less_eq_list_code [code]:
   "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
   "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
   "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"