# HG changeset patch
# User nipkow
# Date 1257322726 -3600
# Node ID a9a002f4b71551b0510002f1b51fe112648fe516
# Parent  c7dfeb7b0b0e9a9d081db5a15ab795bacfed9fdf# Parent  af516ed40e72879c04cf78c0998583e4bf9e8d87
merged

diff -r c7dfeb7b0b0e -r a9a002f4b715 src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Tue Nov 03 19:01:06 2009 -0800
+++ b/src/HOL/Library/Sublist_Order.thy	Wed Nov 04 09:18:46 2009 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Library/Sublist_Order.thy
     Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
-                Florian Haftmann, TU Muenchen
+                Florian Haftmann, Tobias Nipkow, TU Muenchen
 *)
 
 header {* Sublist Ordering *}
@@ -17,7 +17,7 @@
 
 subsection {* Definitions and basic lemmas *}
 
-instantiation list :: (type) order
+instantiation list :: (type) ord
 begin
 
 inductive less_eq_list where
@@ -25,162 +25,237 @@
   | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
   | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
 
-lemmas ileq_empty = empty
-lemmas ileq_drop = drop
-lemmas ileq_take = take
-
-lemma ileq_cases [cases set, case_names empty drop take]:
-  assumes "xs \<le> ys"
-    and "xs = [] \<Longrightarrow> P"
-    and "\<And>z zs. ys = z # zs \<Longrightarrow> xs \<le> zs \<Longrightarrow> P"
-    and "\<And>x zs ws. xs = x # zs \<Longrightarrow> ys = x # ws \<Longrightarrow> zs \<le> ws \<Longrightarrow> P"
-  shows P
-  using assms by (blast elim: less_eq_list.cases)
-
-lemma ileq_induct [induct set, case_names empty drop take]:
-  assumes "xs \<le> ys"
-    and "\<And>zs. P [] zs"
-    and "\<And>z zs ws. ws \<le> zs \<Longrightarrow>  P ws zs \<Longrightarrow> P ws (z # zs)"
-    and "\<And>z zs ws. ws \<le> zs \<Longrightarrow> P ws zs \<Longrightarrow> P (z # ws) (z # zs)"
-  shows "P xs ys" 
-  using assms by (induct rule: less_eq_list.induct) blast+
-
 definition
   [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
 
-lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
-  by (induct rule: ileq_induct) auto
-lemma ileq_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
-  by (auto dest: ileq_length)
+instance proof qed
+
+end
+
+lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
+by (induct rule: less_eq_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)
+
+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 intro: drop)
+
+lemma [code]: "[] <= xs \<longleftrightarrow> True"
+by(metis less_eq_list.empty)
+
+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
+      case empty thus ?case by simp
+    next
+      case drop thus ?case by (metis less_eq_list.drop)
+    next
+      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
+  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
+
+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
+      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
   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!: ileq_empty ileq_drop ileq_take)
+  show "xs \<le> xs" by (induct xs) (auto intro!: less_eq_list.drop)
 next
   fix xs ys :: "'a list"
-  (* TODO: Is there a simpler proof ? *)
-  { fix n
-    have "!!l l'. \<lbrakk>l\<le>l'; l'\<le>l; n=length l + length l'\<rbrakk> \<Longrightarrow> l=l'"
-    proof (induct n rule: nat_less_induct)
-      case (1 n l l') from "1.prems"(1) show ?case proof (cases rule: ileq_cases)
-        case empty with "1.prems"(2) show ?thesis by auto 
-      next
-        case (drop a l2') with "1.prems"(2) have "length l'\<le>length l" "length l \<le> length l2'" "1+length l2' = length l'" by (auto dest: ileq_length)
-        hence False by simp thus ?thesis ..
-      next
-        case (take a l1' l2') hence LEN': "length l1' + length l2' < length l + length l'" by simp
-        from "1.prems" have LEN: "length l' = length l" by (auto dest!: ileq_length)
-        from "1.prems"(2) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take'])
-          case empty' with take LEN show ?thesis by simp 
-        next
-          case (drop' ah l2h) with take LEN have "length l1' \<le> length l2h" "1+length l2h = length l2'" "length l2' = length l1'" by (auto dest: ileq_length)
-          hence False by simp thus ?thesis ..
-        next
-          case (take' ah l1h l2h)
-          with take have 2: "ah=a" "l1h=l2'" "l2h=l1'" "l1' \<le> l2'" "l2' \<le> l1'" by auto
-          with LEN' "1.hyps" "1.prems"(3) have "l1'=l2'" by blast
-          with take 2 show ?thesis by simp
-        qed
-      qed
-    qed
-  }
-  moreover assume "xs \<le> ys" "ys \<le> xs"
+  assume "xs <= ys"
+  hence "ys <= xs \<longrightarrow> xs = ys"
+  proof 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
 next
   fix xs ys zs :: "'a list"
-  {
-    fix n
-    have "!!x y z. \<lbrakk>x \<le> y; y \<le> z; n=length x + length y + length z\<rbrakk> \<Longrightarrow> x \<le> z" 
-    proof (induct rule: nat_less_induct[case_names I])
-      case (I n x y z)
-      from I.prems(2) show ?case proof (cases rule: ileq_cases)
-        case empty with I.prems(1) show ?thesis by auto
-      next
-        case (drop a z') hence "length x + length y + length z' < length x + length y + length z" by simp
-        with I.hyps I.prems(3,1) drop(2) have "x\<le>z'" by blast
-        with drop(1) show ?thesis by (auto intro: ileq_drop)
-      next
-        case (take a y' z') from I.prems(1) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take'])
-          case empty' thus ?thesis by auto
-        next
-          case (drop' ah y'h) with take have "x\<le>y'" "y'\<le>z'" "length x + length y' + length z' < length x + length y + length z" by auto
-          with I.hyps I.prems(3) have "x\<le>z'" by (blast)
-          with take(2) show ?thesis  by (auto intro: ileq_drop)
-        next
-          case (take' ah x' y'h) with take have 2: "x=a#x'" "x'\<le>y'" "y'\<le>z'" "length x' + length y' + length z' < length x + length y + length z" by auto
-          with I.hyps I.prems(3) have "x'\<le>z'" by blast
-          with 2 take(2) show ?thesis by (auto intro: ileq_take)
-        qed
-      qed
+  assume "xs <= ys"
+  hence "ys <= zs \<longrightarrow> xs <= zs"
+  proof (induct arbitrary:zs)
+    case empty show ?case by simp
+  next
+    case (take xs ys x) show ?case
+    proof
+      assume "x # 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))
     qed
-  }
-  moreover assume "xs \<le> ys" "ys \<le> zs"
-  ultimately show "xs \<le> zs" by blast
+  next
+    case drop thus ?case by (metis le_list_drop_Cons)
+  qed
+  moreover assume "ys <= zs"
+  ultimately show "xs <= zs" by blast
 qed
 
 end
 
-lemmas ileq_intros = ileq_empty ileq_drop ileq_take
+lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"
+by (auto dest: le_list_length)
 
-lemma ileq_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
-  by (induct zs) (auto intro: ileq_drop)
-lemma ileq_take_many: "xs \<le> ys \<Longrightarrow> zs @ xs \<le> zs @ ys"
-  by (induct zs) (auto intro: ileq_take)
+lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
+apply (induct rule:less_eq_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 ileq_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
-  by (induct rule: ileq_induct) (auto dest: ileq_length)
-lemma ileq_same_append [simp]: "x # xs \<le> xs \<longleftrightarrow> False"
-  by (auto dest: ileq_length)
+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)
 
-lemma ilt_length [intro]:
-  assumes "xs < ys"
-  shows "length xs < length ys"
-proof -
-  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_le)
-  moreover with ileq_length have "length xs \<le> length ys" by auto
-  ultimately show ?thesis by (auto intro: ileq_same_length)
-qed
+lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
+by (metis empty order_less_le)
+
+lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
+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)
 
-lemma ilt_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
-  by (unfold less_list_def, auto)
-lemma ilt_emptyI: "xs \<noteq> [] \<Longrightarrow> [] < xs"
-  by (unfold less_list_def, auto)
-lemma ilt_emptyD: "[] < xs \<Longrightarrow> xs \<noteq> []"
-  by (unfold less_list_def, auto)
-lemma ilt_below_empty[simp]: "xs < [] \<Longrightarrow> False"
-  by (auto dest: ilt_length)
-lemma ilt_drop: "xs < ys \<Longrightarrow> xs < x # ys"
-  by (unfold less_le) (auto intro: ileq_intros)
-lemma ilt_take: "xs < ys \<Longrightarrow> x # xs < x # ys"
-  by (unfold less_le) (auto intro: ileq_intros)
-lemma ilt_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
-  by (induct zs) (auto intro: ilt_drop)
-lemma ilt_take_many: "xs < ys \<Longrightarrow> zs @ xs < zs @ ys"
-  by (induct zs) (auto intro: ilt_take)
+lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
+by (metis le_list_Cons2_iff less_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)
+
+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 ileq_rev_take: "xs \<le> ys \<Longrightarrow> xs @ [x] \<le> ys @ [x]"
-  by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many)
-lemma ilt_rev_take: "xs < ys \<Longrightarrow> xs @ [x] < ys @ [x]"
-  by (unfold less_le) (auto dest: ileq_rev_take)
-lemma ileq_rev_drop: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ [x]"
-  by (induct rule: ileq_induct) (auto intro: ileq_intros)
-lemma ileq_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
-  by (induct zs rule: rev_induct) (auto dest: ileq_rev_drop)
+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)
+      case empty show ?case by simp
+    next
+      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) }
+      ultimately show ?case by (auto simp:Cons_eq_append_conv)
+    next
+      case (take xs' ys' x)
+      { 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}
+      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)
+    qed }
+  moreover assume ?L
+  ultimately show ?R by blast
+next
+  assume ?R thus ?L by(metis le_list_append_mono order_refl)
+qed
+
+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 ileq_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
-  by (induct rule: ileq_induct) (auto intro: ileq_intros)
-lemma ileq_filter_left[simp]: "filter f xs \<le> xs"
-  by (induct xs) (auto intro: ileq_intros)
-lemma ileq_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
-  by (induct rule: ileq_induct) (auto intro: ileq_intros) 
+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)
+
+lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
+by (induct xs) (auto intro: less_eq_list.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)
+
+
+lemma "xs <= ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
+proof
+  assume ?L
+  thus ?R
+  proof 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 xs ys x)
+    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
+  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
 
 end