# HG changeset patch
# User Christian Sternagel
# Date 1346301507 -32400
# Node ID cd73b439cbe535914b87b65707a2f4cf8ea4fd5d
# Parent  5cd8b4426a57dcbbfccd71ccb369dcf73b121955
added theory instantiating type class order for list prefixes

diff -r 5cd8b4426a57 -r cd73b439cbe5 src/HOL/Library/Prefix_Order.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Prefix_Order.thy	Thu Aug 30 13:38:27 2012 +0900
@@ -0,0 +1,40 @@
+(*  Title:      HOL/Library/Sublist.thy
+    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
+*)
+
+header {* Prefix order on lists as order class instance *}
+
+theory Prefix_Order
+imports Sublist
+begin
+
+instantiation list :: (type) order
+begin
+
+definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
+definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
+
+instance by (default, unfold less_eq_list_def less_list_def) auto
+
+end
+
+lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
+lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def]
+lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def]
+lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
+lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
+lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
+theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
+theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
+lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
+lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
+lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
+lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
+lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def]
+theorems prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
+theorems prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
+lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def]
+lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
+  not_prefixeq_induct [folded less_eq_list_def]
+
+end