src/HOL/Library/Sublist_Order.thy
author Christian Sternagel
Wed Aug 29 12:24:26 2012 +0900 (2012-08-29)
changeset 49084 e3973567ed4f
parent 37765 26bdfb7b680b
child 49085 4eef5c2ff5ad
permissions -rw-r--r--
base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)
     1 (*  Title:      HOL/Library/Sublist_Order.thy
     2     Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
     3                 Florian Haftmann, Tobias Nipkow, TU Muenchen
     4 *)
     5 
     6 header {* Sublist Ordering *}
     7 
     8 theory Sublist_Order
     9 imports Main Sublist
    10 begin
    11 
    12 text {*
    13   This theory defines sublist ordering on lists.
    14   A list @{text ys} is a sublist of a list @{text xs},
    15   iff one obtains @{text ys} by erasing some elements from @{text xs}.
    16 *}
    17 
    18 subsection {* Definitions and basic lemmas *}
    19 
    20 instantiation list :: (type) ord
    21 begin
    22 
    23 definition
    24   "(xs :: 'a list) \<le> ys \<longleftrightarrow> emb (op =) xs ys"
    25 
    26 definition
    27   "(xs :: 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
    28 
    29 instance proof qed
    30 
    31 end
    32 
    33 lemma empty [simp, intro!]: "[] \<le> xs" by (auto simp: less_eq_list_def)
    34 
    35 lemma drop: "xs \<le> ys \<Longrightarrow> xs \<le> (y # ys)"
    36   by (unfold less_eq_list_def) blast
    37 
    38 lemma take: "xs \<le> ys \<Longrightarrow> (x#xs) \<le> (x#ys)"
    39   by (unfold less_eq_list_def) blast
    40 
    41 lemmas le_list_induct [consumes 1, case_names empty drop take] =
    42   emb.induct [of "op =", folded less_eq_list_def]
    43 
    44 lemmas le_list_cases [consumes 1, case_names empty drop take] =
    45   emb.cases [of "op =", folded less_eq_list_def]
    46 
    47 lemma le_list_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    48   by (induct rule: le_list_induct) auto
    49 
    50 lemma le_list_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
    51   by (induct rule: le_list_induct) (auto dest: le_list_length)
    52 
    53 lemma not_le_list_length[simp]: "length ys < length xs \<Longrightarrow> ~ xs <= ys"
    54 by (metis le_list_length linorder_not_less)
    55 
    56 lemma le_list_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
    57 by (auto dest: le_list_length)
    58 
    59 lemma le_list_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
    60 by (induct zs) (auto simp: less_eq_list_def)
    61 
    62 lemma [code]: "[] <= xs \<longleftrightarrow> True"
    63 by (simp add: less_eq_list_def)
    64 
    65 lemma [code]: "(x#xs) <= [] \<longleftrightarrow> False"
    66 by simp
    67 
    68 lemma le_list_drop_Cons: assumes "x#xs <= ys" shows "xs <= ys"
    69 proof-
    70   { fix xs' ys'
    71     assume "xs' <= ys"
    72     hence "ALL x xs. xs' = x#xs \<longrightarrow> xs <= ys"
    73     proof (induct rule: le_list_induct)
    74       case empty thus ?case by simp
    75     next
    76       note drop' = drop
    77       case drop thus ?case by (metis drop')
    78     next
    79       note t = take
    80       case take thus ?case by (simp add: drop)
    81     qed }
    82   from this[OF assms] show ?thesis by simp
    83 qed
    84 
    85 lemma le_list_drop_Cons2:
    86 assumes "x#xs <= x#ys" shows "xs <= ys"
    87 using assms
    88 proof (cases rule: le_list_cases)
    89   case drop thus ?thesis by (metis le_list_drop_Cons list.inject)
    90 qed simp_all
    91 
    92 lemma le_list_drop_Cons_neq: assumes "x # xs <= y # ys"
    93 shows "x ~= y \<Longrightarrow> x # xs <= ys"
    94 using assms by (cases rule: le_list_cases) auto
    95 
    96 lemma le_list_Cons2_iff[simp,code]: "(x#xs) <= (y#ys) \<longleftrightarrow>
    97   (if x=y then xs <= ys else (x#xs) <= ys)"
    98 by (metis drop take le_list_drop_Cons2 le_list_drop_Cons_neq)
    99 
   100 lemma le_list_take_many_iff: "zs @ xs \<le> zs @ ys \<longleftrightarrow> xs \<le> ys"
   101 by (induct zs) (auto intro: take)
   102 
   103 lemma le_list_Cons_EX:
   104   assumes "x # ys <= zs" shows "EX us vs. zs = us @ x # vs & ys <= vs"
   105 proof-
   106   { fix xys zs :: "'a list" assume "xys <= zs"
   107     hence "ALL x ys. xys = x#ys \<longrightarrow> (EX us vs. zs = us @ x # vs & ys <= vs)"
   108     proof (induct rule: le_list_induct)
   109       case empty show ?case by simp
   110     next
   111       case take thus ?case by (metis list.inject self_append_conv2)
   112     next
   113       case drop thus ?case by (metis append_eq_Cons_conv)
   114     qed
   115   } with assms show ?thesis by blast
   116 qed
   117 
   118 instantiation list :: (type) order
   119 begin
   120 
   121 instance proof
   122   fix xs ys :: "'a list"
   123   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" unfolding less_list_def .. 
   124 next
   125   fix xs :: "'a list"
   126   show "xs \<le> xs" by (induct xs) (auto intro!: drop)
   127 next
   128   fix xs ys :: "'a list"
   129   assume "xs <= ys"
   130   hence "ys <= xs \<longrightarrow> xs = ys"
   131   proof (induct rule: le_list_induct)
   132     case empty show ?case by simp
   133   next
   134     case take thus ?case by simp
   135   next
   136     case drop thus ?case
   137       by(metis le_list_drop_Cons le_list_length Suc_length_conv Suc_n_not_le_n)
   138   qed
   139   moreover assume "ys <= xs"
   140   ultimately show "xs = ys" by blast
   141 next
   142   fix xs ys zs :: "'a list"
   143   assume "xs <= ys"
   144   hence "ys <= zs \<longrightarrow> xs <= zs"
   145   proof (induct arbitrary:zs rule: le_list_induct)
   146     case empty show ?case by simp
   147   next
   148     note take' = take
   149     case (take x y xs ys) show ?case
   150     proof
   151       assume "y # ys <= zs"
   152       with take show "x # xs <= zs"
   153         by(metis le_list_Cons_EX le_list_drop_many take')
   154     qed
   155   next
   156     case drop thus ?case by (metis le_list_drop_Cons)
   157   qed
   158   moreover assume "ys <= zs"
   159   ultimately show "xs <= zs" by blast
   160 qed
   161 
   162 end
   163 
   164 lemma le_list_append_le_same_iff: "xs @ ys <= ys \<longleftrightarrow> xs=[]"
   165 by (auto dest: le_list_length)
   166 
   167 lemma le_list_append_mono: "\<lbrakk> xs <= xs'; ys <= ys' \<rbrakk> \<Longrightarrow> xs@ys <= xs'@ys'"
   168 apply (induct rule: le_list_induct)
   169   apply (metis eq_Nil_appendI le_list_drop_many)
   170  apply (metis Cons_eq_append_conv le_list_drop_Cons order_eq_refl order_trans)
   171 apply simp
   172 done
   173 
   174 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
   175 by (metis le_list_length le_list_same_length le_neq_implies_less less_list_def)
   176 
   177 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
   178 by (metis empty order_less_le)
   179 
   180 lemma less_list_below_empty[simp]: "xs < [] \<longleftrightarrow> False"
   181 by (metis empty less_list_def)
   182 
   183 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   184 by (unfold less_le) (auto intro: drop)
   185 
   186 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
   187 by (metis le_list_Cons2_iff less_list_def)
   188 
   189 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   190 by(metis le_list_append_le_same_iff le_list_drop_many order_less_le self_append_conv2)
   191 
   192 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
   193 by (metis le_list_take_many_iff less_list_def)
   194 
   195 
   196 subsection {* Appending elements *}
   197 
   198 lemma le_list_rev_take_iff[simp]: "xs @ zs \<le> ys @ zs \<longleftrightarrow> xs \<le> ys" (is "?L = ?R")
   199 proof
   200   { fix xs' ys' xs ys zs :: "'a list" assume "xs' <= ys'"
   201     hence "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> xs <= ys"
   202     proof (induct arbitrary: xs ys zs rule: le_list_induct)
   203       case empty show ?case by simp
   204     next
   205       note drop' = drop
   206       case (drop xs' ys' x)
   207       { assume "ys=[]" hence ?case using drop(1) by auto }
   208       moreover
   209       { fix us assume "ys = x#us"
   210         hence ?case using drop(2) by(simp add: drop') }
   211       ultimately show ?case by (auto simp:Cons_eq_append_conv)
   212     next
   213       case (take x y xs' ys')
   214       { assume "xs=[]" hence ?case using take(1) by auto }
   215       moreover
   216       { fix us vs assume "xs=x#us" "ys=x#vs" hence ?case using take by auto}
   217       moreover
   218       { fix us assume "xs=x#us" "ys=[]" hence ?case using take(2) by bestsimp }
   219       ultimately show ?case using `x = y` by (auto simp:Cons_eq_append_conv)
   220     qed }
   221   moreover assume ?L
   222   ultimately show ?R by blast
   223 next
   224   assume ?R thus ?L by(metis le_list_append_mono order_refl)
   225 qed
   226 
   227 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
   228 by (unfold less_le) auto
   229 
   230 lemma le_list_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
   231 by (metis append_Nil2 empty le_list_append_mono)
   232 
   233 
   234 subsection {* Relation to standard list operations *}
   235 
   236 lemma le_list_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   237 by (induct rule: le_list_induct) (auto intro: drop)
   238 
   239 lemma le_list_filter_left[simp]: "filter f xs \<le> xs"
   240 by (induct xs) (auto intro: drop)
   241 
   242 lemma le_list_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
   243 by (induct rule: le_list_induct) (auto intro: drop)
   244 
   245 lemma "xs \<le> ys \<longleftrightarrow> (EX N. xs = sublist ys N)" (is "?L = ?R")
   246 proof
   247   assume ?L
   248   thus ?R
   249   proof (induct rule: le_list_induct)
   250     case empty show ?case by (metis sublist_empty)
   251   next
   252     case (drop xs ys x)
   253     then obtain N where "xs = sublist ys N" by blast
   254     hence "xs = sublist (x#ys) (Suc ` N)"
   255       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   256     thus ?case by blast
   257   next
   258     case (take x y xs ys)
   259     then obtain N where "xs = sublist ys N" by blast
   260     hence "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   261       by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   262     thus ?case unfolding `x = y` by blast
   263   qed
   264 next
   265   assume ?R
   266   then obtain N where "xs = sublist ys N" ..
   267   moreover have "sublist ys N <= ys"
   268   proof (induct ys arbitrary:N)
   269     case Nil show ?case by simp
   270   next
   271     case Cons thus ?case by (auto simp add:sublist_Cons drop)
   272   qed
   273   ultimately show ?L by simp
   274 qed
   275 
   276 end