base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)

--- a/src/HOL/Library/Sublist_Order.thy	Wed Aug 29 12:23:14 2012 +0900
+++ b/src/HOL/Library/Sublist_Order.thy	Wed Aug 29 12:24:26 2012 +0900
@@ -6,7 +6,7 @@
 header {* Sublist Ordering *}
 
 theory Sublist_Order
-imports Main
+imports Main Sublist
 begin
 
 text {*
@@ -20,23 +20,35 @@
 instantiation list :: (type) ord
 begin
 
-inductive less_eq_list where
-  empty [simp, intro!]: "[] \<le> xs"
-  | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
-  | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
+definition
+  "(xs :: 'a list) \<le> ys \<longleftrightarrow> emb (op =) xs ys"
 
 definition
-  "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+  "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
 
 instance proof qed
 
 end
 
+lemma empty [simp, intro!]: "[] \<le> xs" by (auto simp: less_eq_list_def)
+
+lemma drop: "xs \<le> ys \<Longrightarrow> xs \<le> (y # ys)"
+  by (unfold less_eq_list_def) blast
+
+lemma take: "xs \<le> ys \<Longrightarrow> (x#xs) \<le> (x#ys)"
+  by (unfold less_eq_list_def) blast
+
+lemmas le_list_induct [consumes 1, case_names empty drop take] =
+  emb.induct [of "op =", folded less_eq_list_def]
+
+lemmas le_list_cases [consumes 1, case_names empty drop take] =
+  emb.cases [of "op =", folded less_eq_list_def]
+
 lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
-by (induct rule: less_eq_list.induct) auto
+  by (induct rule: le_list_induct) auto
 
 lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
-by (induct rule: less_eq_list.induct) (auto dest: le_list_length)
+  by (induct rule: le_list_induct) (auto dest: le_list_length)
 
 lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
 by (metis le_list_length linorder_not_less)
@@ -45,10 +57,10 @@
 by (auto dest: le_list_length)
 
 lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
-by (induct zs) (auto intro: drop)
+by (induct zs) (auto simp: less_eq_list_def)
 
 lemma [code]: "[] <= xs \<longleftrightarrow> True"
-by(metis less_eq_list.empty)
+by (simp add: less_eq_list_def)
 
 lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
 by simp
@@ -58,11 +70,13 @@
   { fix xs' ys'
     assume "xs' <= ys"
     hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
-    proof induct
+    proof (induct rule: le_list_induct)
       case empty thus ?case by simp
     next
-      case drop thus ?case by (metis less_eq_list.drop)
+      note drop' = drop
+      case drop thus ?case by (metis drop')
     next
+      note t = take
       case take thus ?case by (simp add: drop)
     qed }
   from this[OF assms] show ?thesis by simp
@@ -71,13 +85,13 @@
 lemma le_list_drop_Cons2:
 assumes "x#xs <= x#ys" shows "xs <= ys"
 using assms
-proof cases
+proof (cases rule: le_list_cases)
   case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
 qed simp_all
 
 lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
 shows "x ~= y \<Longrightarrow> x # xs <= ys"
-using assms proof cases qed auto
+using assms by (cases rule: le_list_cases) auto
 
 lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
   (if x=y then xs <= ys else (x#xs) <= ys)"
@@ -91,7 +105,7 @@
 proof-
   { fix xys zs :: "'a list" assume "xys <= zs"
     hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"
-    proof induct
+    proof (induct rule: le_list_induct)
       case empty show ?case by simp
     next
       case take thus ?case by (metis list.inject self_append_conv2)
@@ -109,12 +123,12 @@
   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
 next
   fix xs :: "'a list"
-  show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)
+  show "xs \<le> xs" by (induct xs) (auto intro!: drop)
 next
   fix xs ys :: "'a list"
   assume "xs <= ys"
   hence "ys <= xs \<longrightarrow> xs = ys"
-  proof induct
+  proof (induct rule: le_list_induct)
     case empty show ?case by simp
   next
     case take thus ?case by simp
@@ -128,14 +142,15 @@
   fix xs ys zs :: "'a list"
   assume "xs <= ys"
   hence "ys <= zs \<longrightarrow> xs <= zs"
-  proof (induct arbitrary:zs)
+  proof (induct arbitrary:zs rule: le_list_induct)
     case empty show ?case by simp
   next
-    case (take xs ys x) show ?case
+    note take' = take
+    case (take x y xs ys) show ?case
     proof
-      assume "x # ys <= zs"
+      assume "y # ys <= zs"
       with take show "x # xs <= zs"
-        by(metis le_list_Cons_EX le_list_drop_many less_eq_list.take local.take(2))
+        by(metis le_list_Cons_EX le_list_drop_many take')
     qed
   next
     case drop thus ?case by (metis le_list_drop_Cons)
@@ -150,7 +165,7 @@
 by (auto dest: le_list_length)
 
 lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
-apply (induct rule:less_eq_list.induct)
+apply (induct rule: le_list_induct)
   apply (metis eq_Nil_appendI le_list_drop_many)
  apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
 apply simp
@@ -166,7 +181,7 @@
 by (metis empty less_list_def)
 
 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
-by (unfold less_le) (auto intro: less_eq_list.drop)
+by (unfold less_le) (auto intro: drop)
 
 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
 by (metis le_list_Cons2_iff less_list_def)
@@ -184,23 +199,24 @@
 proof
   { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
     hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"
-    proof (induct arbitrary: xs ys zs)
+    proof (induct arbitrary: xs ys zs rule: le_list_induct)
       case empty show ?case by simp
     next
+      note drop' = drop
       case (drop xs' ys' x)
       { assume "ys=[]" hence ?case using drop(1) by auto }
       moreover
       { fix us assume "ys = x#us"
-        hence ?case using drop(2) by(simp add: less_eq_list.drop) }
+        hence ?case using drop(2) by(simp add: drop') }
       ultimately show ?case by (auto simp:Cons_eq_append_conv)
     next
-      case (take xs' ys' x)
+      case (take x y xs' ys')
       { assume "xs=[]" hence ?case using take(1) by auto }
       moreover
-      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take(2) by auto}
+      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take by auto}
       moreover
       { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
-      ultimately show ?case by (auto simp:Cons_eq_append_conv)
+      ultimately show ?case using `x = y` by (auto simp:Cons_eq_append_conv)
     qed }
   moreover assume ?L
   ultimately show ?R by blast
@@ -218,19 +234,19 @@
 subsection {* Relation to standard list operations *}
 
 lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
-by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
+by (induct rule: le_list_induct) (auto intro: drop)
 
 lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
-by (induct xs) (auto intro: less_eq_list.drop)
+by (induct xs) (auto intro: drop)
 
 lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
-by (induct rule: less_eq_list.induct) (auto intro: less_eq_list.drop)
+by (induct rule: le_list_induct) (auto intro: drop)
 
 lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
 proof
   assume ?L
   thus ?R
-  proof induct
+  proof (induct rule: le_list_induct)
     case empty show ?case by (metis sublist_empty)
   next
     case (drop xs ys x)
@@ -239,11 +255,11 @@
       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
     thus ?case by blast
   next
-    case (take xs ys x)
+    case (take x y xs ys)
     then obtain N where "xs = sublist ys N" by blast
     hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
-    thus ?case by blast
+    thus ?case unfolding `x = y` by blast
   qed
 next
   assume ?R