# HG changeset patch
# User Christian Sternagel
# Date 1346225135 -32400
# Node ID 4eef5c2ff5add42894e1c4c88e631579d7600239
# Parent  e3973567ed4f6215dc1c807ea6e0602c7cb49417
introduced "sub" as abbreviation for "emb (op =)";
Sublist_Order is now based on Sublist.sub;
simplified and moved most lemmas on sub from Sublist_Order to Sublist;
Sublist_Order merely contains ord and order instances for sub plus some lemmas on the strict part of the order

diff -r e3973567ed4f -r 4eef5c2ff5ad src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Wed Aug 29 12:24:26 2012 +0900
+++ b/src/HOL/Library/Sublist.thy	Wed Aug 29 16:25:35 2012 +0900
@@ -433,6 +433,17 @@
   assumes "emb P xs []" shows "xs = []"
   using assms by (cases rule: emb.cases) auto
 
+lemma emb_Cons_Nil [simp]:
+  "emb P (x#xs) [] = False"
+proof -
+  { assume "emb P (x#xs) []"
+    from emb_Nil2 [OF this] have False by simp
+  } moreover {
+    assume False
+    hence "emb P (x#xs) []" by simp
+  } ultimately show ?thesis by blast
+qed
+
 lemma emb_append2 [intro]:
   "emb P xs ys \<Longrightarrow> emb P xs (zs @ ys)"
   by (induct zs) auto
@@ -479,4 +490,202 @@
 lemma emb_length: "emb P xs ys \<Longrightarrow> length xs \<le> length ys"
   by (induct rule: emb.induct) auto
 
+(*FIXME: move*)
+definition transp_on :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
+  "transp_on P A \<equiv> \<forall>a\<in>A. \<forall>b\<in>A. \<forall>c\<in>A. P a b \<and> P b c \<longrightarrow> P a c"
+lemma transp_onI [Pure.intro]:
+  "(\<And>a b c. \<lbrakk>a \<in> A; b \<in> A; c \<in> A; P a b; P b c\<rbrakk> \<Longrightarrow> P a c) \<Longrightarrow> transp_on P A"
+  unfolding transp_on_def by blast
+
+lemma transp_on_emb:
+  assumes "transp_on P A"
+  shows "transp_on (emb P) (lists A)"
+proof
+  fix xs ys zs
+  assume "emb P xs ys" and "emb P ys zs"
+    and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
+  thus "emb P xs zs"
+  proof (induction arbitrary: zs)
+    case emb_Nil show ?case by blast
+  next
+    case (emb_Cons xs ys y)
+    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
+      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
+    hence "emb P ys (v#vs)" by blast
+    hence "emb P ys zs" unfolding zs by (rule emb_append2)
+    from emb_Cons.IH [OF this] and emb_Cons.prems show ?case by simp
+  next
+    case (emb_Cons2 x y xs ys)
+    from emb_ConsD [OF `emb P (y#ys) zs`] obtain us v vs
+      where zs: "zs = us @ v # vs" and "P y v" and "emb P ys vs" by blast
+    with emb_Cons2 have "emb P xs vs" by simp
+    moreover have "P x v"
+    proof -
+      from zs and `zs \<in> lists A` have "v \<in> A" by auto
+      moreover have "x \<in> A" and "y \<in> A" using emb_Cons2 by simp_all
+      ultimately show ?thesis using `P x y` and `P y v` and assms
+        unfolding transp_on_def by blast
+    qed
+    ultimately have "emb P (x#xs) (v#vs)" by blast
+    thus ?case unfolding zs by (rule emb_append2)
+  qed
+qed
+
+
+subsection {* Sublists (special case of embedding) *}
+
+abbreviation sub :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "sub xs ys \<equiv> emb (op =) xs ys"
+
+lemma sub_Cons2: "sub xs ys \<Longrightarrow> sub (x#xs) (x#ys)" by auto
+
+lemma sub_same_length:
+  assumes "sub xs ys" and "length xs = length ys" shows "xs = ys"
+  using assms by (induct) (auto dest: emb_length)
+
+lemma not_sub_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sub xs ys"
+  by (metis emb_length linorder_not_less)
+
+lemma [code]:
+  "emb P [] ys \<longleftrightarrow> True"
+  "emb P (x#xs) [] \<longleftrightarrow> False"
+  by (simp_all)
+
+lemma sub_Cons': "sub (x#xs) ys \<Longrightarrow> sub xs ys"
+  by (induct xs) (auto dest: emb_ConsD)
+
+lemma sub_Cons2':
+  assumes "sub (x#xs) (x#ys)" shows "sub xs ys"
+  using assms by (cases) (rule sub_Cons')
+
+lemma sub_Cons2_neq:
+  assumes "sub (x#xs) (y#ys)"
+  shows "x \<noteq> y \<Longrightarrow> sub (x#xs) ys"
+  using assms by (cases) auto
+
+lemma sub_Cons2_iff [simp, code]:
+  "sub (x#xs) (y#ys) = (if x = y then sub xs ys else sub (x#xs) ys)"
+  by (metis emb_Cons emb_Cons2 [of "op =", OF refl] sub_Cons2' sub_Cons2_neq)
+
+lemma sub_append': "sub (zs @ xs) (zs @ ys) \<longleftrightarrow> sub xs ys"
+  by (induct zs) simp_all
+
+lemma sub_refl [simp, intro!]: "sub xs xs" by (induct xs) simp_all
+
+lemma sub_antisym:
+  assumes "sub xs ys" and "sub ys xs"
+  shows "xs = ys"
+using assms
+proof (induct)
+  case emb_Nil
+  from emb_Nil2 [OF this] show ?case by simp
+next
+  case emb_Cons2 thus ?case by simp
+next
+  case emb_Cons thus ?case
+    by (metis sub_Cons' emb_length Suc_length_conv Suc_n_not_le_n)
+qed
+
+lemma transp_on_sub: "transp_on sub UNIV"
+proof -
+  have "transp_on (op =) UNIV" by (simp add: transp_on_def)
+  from transp_on_emb [OF this] show ?thesis by simp
+qed
+
+lemma sub_trans: "sub xs ys \<Longrightarrow> sub ys zs \<Longrightarrow> sub xs zs"
+  using transp_on_sub [unfolded transp_on_def] by blast
+
+lemma sub_append_le_same_iff: "sub (xs @ ys) ys \<longleftrightarrow> xs = []"
+  by (auto dest: emb_length)
+
+lemma emb_append_mono:
+  "\<lbrakk> emb P xs xs'; emb P ys ys' \<rbrakk> \<Longrightarrow> emb P (xs@ys) (xs'@ys')"
+apply (induct rule: emb.induct)
+  apply (metis eq_Nil_appendI emb_append2)
+ apply (metis append_Cons emb_Cons)
+by (metis append_Cons emb_Cons2)
+
+
+subsection {* Appending elements *}
+
+lemma sub_append [simp]:
+  "sub (xs @ zs) (ys @ zs) \<longleftrightarrow> sub xs ys" (is "?l = ?r")
+proof
+  { fix xs' ys' xs ys zs :: "'a list" assume "sub xs' ys'"
+    hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sub xs ys"
+    proof (induct arbitrary: xs ys zs)
+      case emb_Nil show ?case by simp
+    next
+      case (emb_Cons xs' ys' x)
+      { assume "ys=[]" hence ?case using emb_Cons(1) by auto }
+      moreover
+      { fix us assume "ys = x#us"
+        hence ?case using emb_Cons(2) by(simp add: emb.emb_Cons) }
+      ultimately show ?case by (auto simp:Cons_eq_append_conv)
+    next
+      case (emb_Cons2 x y xs' ys')
+      { assume "xs=[]" hence ?case using emb_Cons2(1) by auto }
+      moreover
+      { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using emb_Cons2 by auto}
+      moreover
+      { fix us assume "xs=x#us" "ys=[]" hence ?case using emb_Cons2(2) by bestsimp }
+      ultimately show ?case using `x = y` by (auto simp: Cons_eq_append_conv)
+    qed }
+  moreover assume ?l
+  ultimately show ?r by blast
+next
+  assume ?r thus ?l by (metis emb_append_mono sub_refl)
+qed
+
+lemma sub_drop_many: "sub xs ys \<Longrightarrow> sub xs (zs @ ys)"
+  by (induct zs) auto
+
+lemma sub_rev_drop_many: "sub xs ys \<Longrightarrow> sub xs (ys @ zs)"
+  by (metis append_Nil2 emb_Nil emb_append_mono)
+
+
+subsection {* Relation to standard list operations *}
+
+lemma sub_map:
+  assumes "sub xs ys" shows "sub (map f xs) (map f ys)"
+  using assms by (induct) auto
+
+lemma sub_filter_left [simp]: "sub (filter P xs) xs"
+  by (induct xs) auto
+
+lemma sub_filter [simp]:
+  assumes "sub xs ys" shows "sub (filter P xs) (filter P ys)"
+  using assms by (induct) auto
+
+lemma "sub xs ys \<longleftrightarrow> (\<exists> N. xs = sublist ys N)" (is "?L = ?R")
+proof
+  assume ?L
+  thus ?R
+  proof (induct)
+    case emb_Nil show ?case by (metis sublist_empty)
+  next
+    case (emb_Cons xs ys x)
+    then obtain N where "xs = sublist ys N" by blast
+    hence "xs = sublist (x#ys) (Suc ` N)"
+      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
+    thus ?case by blast
+  next
+    case (emb_Cons2 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 unfolding `x = y` by blast
+  qed
+next
+  assume ?R
+  then obtain N where "xs = sublist ys N" ..
+  moreover have "sub (sublist ys N) ys"
+  proof (induct ys arbitrary:N)
+    case Nil show ?case by simp
+  next
+    case Cons thus ?case by (auto simp: sublist_Cons)
+  qed
+  ultimately show ?L by simp
+qed
+
 end
diff -r e3973567ed4f -r 4eef5c2ff5ad src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Wed Aug 29 12:24:26 2012 +0900
+++ b/src/HOL/Library/Sublist_Order.thy	Wed Aug 29 16:25:35 2012 +0900
@@ -6,7 +6,9 @@
 header {* Sublist Ordering *}
 
 theory Sublist_Order
-imports Main Sublist
+imports
+  Main
+  Sublist
 begin
 
 text {*
@@ -21,256 +23,54 @@
 begin
 
 definition
-  "(xs :: 'a list) \<le> ys \<longleftrightarrow> emb (op =) xs ys"
+  "(xs :: 'a list) \<le> ys \<longleftrightarrow> sub xs ys"
 
 definition
   "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
 
-instance proof qed
+instance ..
 
 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: le_list_induct) auto
-
-lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
-  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)
-
-lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
-by (auto dest: le_list_length)
-
-lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
-by (induct zs) (auto simp: less_eq_list_def)
-
-lemma [code]: "[] <= xs \<longleftrightarrow> True"
-by (simp add: less_eq_list_def)
-
-lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
-by simp
-
-lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"
-proof-
-  { fix xs' ys'
-    assume "xs' <= ys"
-    hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
-    proof (induct rule: le_list_induct)
-      case empty thus ?case by simp
-    next
-      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
-qed
-
-lemma le_list_drop_Cons2:
-assumes "x#xs <= x#ys" shows "xs <= ys"
-using assms
-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 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)"
-by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)
-
-lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys"
-by (induct zs) (auto intro: take)
-
-lemma le_list_Cons_EX:
-  assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"
-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 rule: le_list_induct)
-      case empty show ?case by simp
-    next
-      case take thus ?case by (metis list.inject self_append_conv2)
-    next
-      case drop thus ?case by (metis append_eq_Cons_conv)
-    qed
-  } with assms show ?thesis by blast
-qed
-
-instantiation list :: (type) order
-begin
-
-instance proof
+instance list :: (type) order
+proof
   fix xs ys :: "'a list"
   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!: drop)
+  show "xs \<le> xs" by (simp add: less_eq_list_def)
 next
   fix xs ys :: "'a list"
-  assume "xs <= ys"
-  hence "ys <= xs \<longrightarrow> xs = ys"
-  proof (induct rule: le_list_induct)
-    case empty show ?case by simp
-  next
-    case take thus ?case by simp
-  next
-    case drop thus ?case
-      by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)
-  qed
-  moreover assume "ys <= xs"
-  ultimately show "xs = ys" by blast
+  assume "xs <= ys" and "ys <= xs"
+  thus "xs = ys" by (unfold less_eq_list_def) (rule sub_antisym)
 next
   fix xs ys zs :: "'a list"
-  assume "xs <= ys"
-  hence "ys <= zs \<longrightarrow> xs <= zs"
-  proof (induct arbitrary:zs rule: le_list_induct)
-    case empty show ?case by simp
-  next
-    note take' = take
-    case (take x y xs ys) show ?case
-    proof
-      assume "y # ys <= zs"
-      with take show "x # xs <= zs"
-        by(metis le_list_Cons_EX le_list_drop_many take')
-    qed
-  next
-    case drop thus ?case by (metis le_list_drop_Cons)
-  qed
-  moreover assume "ys <= zs"
-  ultimately show "xs <= zs" by blast
+  assume "xs <= ys" and "ys <= zs"
+  thus "xs <= zs" by (unfold less_eq_list_def) (rule sub_trans)
 qed
 
-end
-
-lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"
-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: 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
-done
-
 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
-by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)
+  by (metis emb_length sub_same_length le_neq_implies_less less_list_def less_eq_list_def)
 
 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
-by (metis empty order_less_le)
+  by (metis less_eq_list_def emb_Nil order_less_le)
 
-lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
-by (metis empty less_list_def)
+lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
+  by (metis emb_Nil less_eq_list_def less_list_def)
 
 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
-by (unfold less_le) (auto intro: drop)
+  by (unfold less_le less_eq_list_def) (auto)
 
 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
-by (metis le_list_Cons2_iff less_list_def)
+  by (metis sub_Cons2_iff less_list_def less_eq_list_def)
 
 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
-by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)
+  by (metis sub_append_le_same_iff sub_drop_many order_less_le self_append_conv2 less_eq_list_def)
 
 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
-by (metis le_list_take_many_iff less_list_def)
-
-
-subsection {* Appending elements *}
-
-lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")
-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 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: drop') }
-      ultimately show ?case by (auto simp:Cons_eq_append_conv)
-    next
-      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 by auto}
-      moreover
-      { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
-      ultimately show ?case using `x = y` by (auto simp:Cons_eq_append_conv)
-    qed }
-  moreover assume ?L
-  ultimately show ?R by blast
-next
-  assume ?R thus ?L by(metis le_list_append_mono order_refl)
-qed
+  by (metis less_list_def less_eq_list_def sub_append')
 
 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
-by (unfold less_le) auto
-
-lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
-by (metis append_Nil2 empty le_list_append_mono)
-
-
-subsection {* Relation to standard list operations *}
-
-lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
-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: drop)
-
-lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
-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 rule: le_list_induct)
-    case empty show ?case by (metis sublist_empty)
-  next
-    case (drop xs ys x)
-    then obtain N where "xs = sublist ys N" by blast
-    hence "xs = sublist (x#ys) (Suc ` N)"
-      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
-    thus ?case by blast
-  next
-    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 unfolding `x = y` by blast
-  qed
-next
-  assume ?R
-  then obtain N where "xs = sublist ys N" ..
-  moreover have "sublist ys N <= ys"
-  proof (induct ys arbitrary:N)
-    case Nil show ?case by simp
-  next
-    case Cons thus ?case by (auto simp add:sublist_Cons drop)
-  qed
-  ultimately show ?L by simp
-qed
+  by (unfold less_le less_eq_list_def) auto
 
 end